GADTs vs. MultiParamTypeClasses

Question

I'm trying to grasp GADTs, and I have looked at the GADTs example in GHC's manual. As far as I can tell, it is possible to do the same thing with MultiParamTypeClasses:

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies,
    FlexibleInstances, UndecidableInstances #-}

class IsTerm a b | a -> b where
  eval :: a -> b

data IntTerm  = Lit Int
              | Succ IntTerm
data BoolTerm = IsZero IntTerm
data If p a   = If p a a
data Pair a b = Pair a b

instance IsTerm IntTerm Int where
  eval (Lit i)      = i
  eval (Succ t)     = 1 + eval t

instance IsTerm BoolTerm Bool where
  eval (IsZero t)   = eval t == 0

instance (IsTerm p Bool, IsTerm a r) => IsTerm (If p a) r where
  eval (If b e1 e2) = if eval b then eval e1 else eval e2

instance (IsTerm a c, IsTerm b d) => IsTerm (Pair a b) (c, d) where
  eval (Pair e1 e2) = (eval e1, eval e2)

Note, that we have the exact same constructors and the exact same code for eval (spread cross the instance definitions) as in GHC's GADTs example.

So what's all the fuzz about GADTs? Is there anything that I can do with GADTs that I can't do with MultiParamTypeClasses? Or do they just provide a more concise way of doing things that I could do with MultiParamTypeClasses instead?

Answer 1

You can put GADT values of the same type but with different constructors into a container conveniently,

map eval [Lit 1, If (IsZero (Lit 3)) (Lit 4) (Succ (Lit 6))]

is straightforward, but to obtain the same using distinct types and MPTCs with functional dependencies is difficult at the least. In your Multiparameter type class approach, Lit and If are constructors of different types, so one would need a wrapper type to put them into the same container. The wrapper type would, as far as I can see, have to be an existential type à la

data Wrap t = forall a. (IsTerm a t) => Wrapper a

with an

instance IsTerm (Wrap t) t where
    eval (Wrapper e) = eval e

to ensure some type safety and the ability to map functions like eval over the list. So you're half-way or more back to GADTs, minus the convenience.

I'm not sure there's anything GADTs allow you to do that you can't achieve without them, but some things would sacrifice a lot of elegance.