archives

GADT vs. Type Classes

I'm looking for a paper or tutorial which compares/contrasts generalized algebraic data types and type classes (as found in GHC/Haskell). I get the feeling that they are some how duals of each other, and that there may be some overlap of the capabilities of each, but I don't know if I understand the essential differences which makes both desirable. For example, the standard GADT example of a tagless interpreter looks pretty similar to an equivalent built using type classes. In fact, the code for "eval" is identical, only the type annotations differ. Any thoughts, comments?
data Term a where
    Lit  :: Int -> Term Int
    Inc  :: Term Int -> Term Int
    IsZ  :: Term Int -> Term Bool
    If   :: Term Bool -> Term a -> Term a -> Term a
    Pair :: Term a -> Term b -> Term (a,b)
    Fst  :: Term (a,b) -> Term a
    Snd  :: Term (a,b) -> Term b 
  
eval :: Term a -> a
eval (Lit i)    = i
eval (Inc t)    = eval t + 1
eval (IsZ t)    = eval t == 0
eval (If b t e) = if eval b then eval t else eval e
eval (Pair a b) = (eval a, eval b)
eval (Fst t)    = fst (eval t)
eval (Snd t)    = snd (eval t)
data Inc a    = Inc a    
data Lit a    = Lit a   
data IsZ a    = IsZ a   
data Pair a b = Pair a b
data If p t e = If p t e
data Fst a    = Fst a   
data Snd a    = Snd a  

class    Eval a b | a -> b                      where eval :: a -> b
instance Eval (Lit a) a                         where eval (Lit i)    = i
instance (Num b, Eval a b) => Eval (Inc a) b    where eval (Inc t)    = eval t + 1 
instance (Num b, Eval a b) => Eval (IsZ a) Bool where eval (IsZ t)    = eval t == 0
instance (Eval a Bool, Eval b d, Eval c d) => 
          Eval (If a b c) d                     where eval (If p t e) = if eval p 
                                                                         then eval t
                                                                         else eval e
instance (Eval a c, Eval b d) =>    
          Eval (Pair a b) (c,d)                 where eval (Pair a b) = (eval a, eval b)
instance (Eval a (b,c)) => Eval (Fst a) b       where eval (Fst t)    = fst (eval t)
instance (Eval a (b,c)) => Eval (Snd a) c       where eval (Snd t)    = snd (eval t)
...and here's a driver program which will work for either snippet...
{-# OPTIONS -fglasgow-exts #-}  
{-# OPTIONS -fallow-undecidable-instances #-}  

main = print $ (eval stuff)

stuff = Pair (If (IsZ (Inc (Inc (Lit 5))))
                 (Lit 6)
                 (Lit 7))
             (Fst (Snd (Pair (Lit 42)
                             (Pair (Lit 8) (Lit 9)))))

The Type of 42

The following is a reposting from my blog at http://www.artima.com/weblogs/viewpost.jsp?thread=182140.

When I was designing Cat I started with the assumption that the type of a number such as 42, must be a function which pushes a primitive integer type onto the stack. So the type of 42 would be:

42 : ()->(int)

The type of a function which yielded 42 would be:

[42] : ()->(()->(int))

In Joy the operation for evaluating functions is "i". The equivalent in Cat is "eval". The type of eval in Cat currently is:

eval : (A (A:any*)->(B:any*))->(B)

This meant that the following was badly typed in Cat:

42 eval

This is because eval expected a function on the top of the stack, but 42 produced a primitive on the top of the stack. You would have to instead write:

[42] eval

The decision for this type design was based on two things:

  1. That kind of type system was more familiar to me
  2. The programs more closely mapped to assembly language as-is

In assembly an operation which yields 42 and the value 42 are very different things. My thought was that I wanted to be able to trivially map Cat functions to assembly code. My concern is that the execution loop of an assembly program where values were executable would be non-trivial. I assumed you would need a switch statement and this would signficiantly hurt performance (Cat is striving to become a full competitor with real assembly code, so performance is a big concern). I am no longer convinced that this would actually be a problem.

The first issue is writing the type of numbers. It appears that what is needed is the ability to name new types and express them recursively:

42 : int;
int = ()->(int);

The next challenge is converting to assembly code. I haven't worked out all of the details, but I believe that when generating assembly, I need to simply insert type conversion routines at key places (i.e. where an integer is being executed, or treated like a function).

Do all this seem sane and rational?