GADTs vs. MultiParamTypeClasses

14
votes

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?

2
haskellgadt
In your sample you are able to construct If (Lit 3) (IntTerm 1) (IntTerm 2). Consider using of data If a = If BoolTerm a a. – ony
GADTs don't offer anything that could not be simulated by existential types and type equality. But your particular example is not an instance of this. – augustss
GADTs are closed at definition time, which can be a very big difference. – Ptharien's Flame

2 Answers

13
votes

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.

0
votes

GADTs just allows you to provide more natural way of constructor defined and allows to use matching on type level and constructors all together (is something that you can't do without it, I think).

{-# LANGUAGE GADTs #-}
data Term a = (a ~ Bool) => IsZero (Term Int)
            | (a ~ Int) => Lit Int
eval :: Term a -> a
eval (IsZero t) = eval t == 0
eval (Lit a) = a