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)))))

GADTization

And if there are any GADT experts out there who are looking for a challenge, you might try to use GADTs in the following data structure to eliminate the existential types (which make writing functions like "tail" problematic). The "Fancy" data structure is statically constrained to contain linearly increasing runs of elements of alternating types. So for example, you can start out with one Int and then two Strings, then three Ints, four Strings, etc.

 data Fancy a b left next =
     forall c d left' next' lz decleft .
     (Show c, Show d,
      Zerop left lz,
      If lz (Succ next) next next',
      Pre left decleft,
      If lz next decleft left',
      If lz b a c,
      If lz a b d
     ) => Cons a (Fancy c d left' next') | Nil

 fancy :: Fancy Integer String Zero (Succ Zero)
 fancy = (Cons 1
         (Cons "a" (Cons "b"
         (Cons  2  (Cons  3  (Cons 4
         (Cons "c" (Cons "d" (Cons "e" (Cons "f"
         (Cons  5  (Cons  6  (Cons  7  (Cons  8  (Cons 9 Nil)))))))))))))))

 instance (Show a, Show b) => Show (Fancy a b c d) where
     show (Cons x xs) = "(Cons " ++ (show x) ++ " " ++ (show xs) ++ ")"
     show Nil = "Nil"

 data Succ a = S a deriving Show
 data Zero = Z deriving Show

 data TTrue
 data TFalse

 class Pre a b | a -> b
 instance Pre (Succ a) a
 instance Pre Zero Zero

 class If p t e result | p t e -> result
 instance If TTrue  a b a
 instance If TFalse a b b

 class Zerop a b | a -> b
 instance Zerop Zero TTrue
 instance Zerop (Succ a) TFalse

By Greg Buchholz at Thu, 2006-10-26 15:12 | login or register to post comments

Detailedness of the types

I am not competent enough to really characterize the difference, but I guess one important difference in your example is that the type class solution requires "deep" types, i.e., the structure of the terms is fully reified at the type level. This is not the case in the GADT solution.

If you consider, say, a parsing function, then I would imagine that you can only give a reasonable implementation using the GADT approach since the structure (and hence type) of the expressions cannot be predicted by the type system in the type class approach.

By Klaus Ostermann at Thu, 2006-10-26 20:01 | login or register to post comments

Parser

Just to follow up, here's a thread with a couple of different parsers for the GADT example over on the Haskell-Cafe mailing list.

By Greg Buchholz at Fri, 2006-11-03 16:35 | login or register to post comments

GADTs are closed?

I was just rewriting a function that used GADTs to use type classes and one obvious difference is that GADTs are closed, while type classes allow you to extend them as you want.

Can't tell you more, though..

By Thomas Schilling at Fri, 2006-10-27 20:10 | login or register to post comments

Encoding type classes into GADTs

This answer is really a bit late, but I just stumbled across your post by chance. My paper "polymorphic typed defunctionalization and concretization" (with Nadji Gauthier) shows a type-preserving encoding of type classes into GADTs. This proves, in a way, that "anything that can be done with type classes can be done with GADTs". However, for the encoding to be used in practice, you need either a closed world assumption or a form of extensible GADTs.

By Francois Pottier at Mon, 2008-01-28 17:38 | login or register to post comments

Lambda the Ultimate

User login

Navigation