GADTs vs MultiParamTypeClasses

Question

Sto cercando di afferrare GADTs e ho guardato il GADTs example nel manuale di GHC. Per quanto posso dire, è possibile fare la stessa cosa con 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) 

nota, che abbiamo gli stessi costruttori esatte e lo stesso codice esatto per eval (spread attraversare le definizioni esempio) come in Esempio di GHC GADTs.

Quindi cos'è tutta la fuzz su GADTs? C'è qualcosa che posso fare con GADTs che non posso fare con MultiParamTypeClasses? Oppure forniscono semplicemente un modo più conciso di fare cose che potrei fare con MultiParamTypeClasses?

Answer 1

È possibile inserire valori GADT dello stesso tipo, ma con differenti costruttori in un contenitore conveniente,

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

è semplice, ma per ottenere lo stesso utilizzando tipi distinti e MPTCs con dipendenze funzionali è difficile almeno . Nell'approccio classe di tipo Multiparametro, Lit e If sono costruttori di tipi diversi, quindi è necessario un tipo di wrapper per inserirli nello stesso contenitore. Il tipo di involucro sarebbe, per quanto posso vedere, deve essere un tipo esistenziale à la

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

un

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

per garantire una certa sicurezza tipo e la capacità di map funzioni come eval over la lista. Quindi sei a metà strada o più indietro ai GADT, meno la convenienza.

Non sono sicuro che ci sia qualcosa che i GADT ti permettono di fare senza di loro, ma alcune cose potrebbero sacrificare un sacco di eleganza.

Answer 2

GADTs solo consente di fornire un modo più naturale di definizione del costruttore e consente di utilizzare la corrispondenza a livello di tipo e costruttori tutti insieme (è qualcosa che non si può fare a meno di esso, credo).

{-# 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