GADTs vs. MultiParamTypeClasses

Question

Ich versuche zu verstehen GADTs, und ich habe die GADTs example in GHC-Handbuch angeschaut. Soweit ich das beurteilen kann, ist es möglich, die gleiche Sache mit MultiParamTypeClasses zu tun:

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

Beachten Sie, dass wir genau die gleichen Konstrukteure und den exakt gleichen Code für eval (Spread überquert die Instanzdefinitionen) haben, wie in GHC's GADTs Beispiel.

Also was ist der ganze Fuzz über GADTs? Gibt es etwas, was ich mit GADTs tun kann, dass ich nicht mit MultiParamTypeClasses tun kann? Oder bieten sie nur einen präziseren Weg, Dinge zu tun, die ich mit MultiParamTypeClasses stattdessen tun könnte?

Answer 1

Sie GADT Werte des gleichen Typs setzen können, aber mit unterschiedlichen Herstellern in einen Behälter bequem,

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

ist einfach, aber das gleiche mit unterschiedlichen Typen und MPTCs mit funktionalen Abhängigkeiten zu erhalten, ist zumindest schwierig . In Ihrem Multiparameter-Klassenklassenansatz sind Lit und If Konstruktoren verschiedener Typen. Daher würde man einen Wrappertyp benötigen, um sie in denselben Container zu legen. Der Wrapper-Typ wäre, soweit ich sehen kann, hat eine existentielle Art à la

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

mit einem

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

sein, um irgendeine Art Sicherheit und die Fähigkeit, map Funktionen wie eval über zu gewährleisten Die Liste. Du bist also halbwegs zurück zu GADTs, ohne die Bequemlichkeit.

Ich bin mir nicht sicher, es gibt etwas GADTs können Sie tun, dass Sie ohne sie nicht erreichen können, aber einige Dinge würden viel von Eleganz opfern.

Answer 2

GADTs ermöglicht es Ihnen nur, natürlichere Art und Weise des Konstruktors zu definieren, und ermöglicht die Verwendung von Matching auf Typ-Ebene und Konstruktoren alle zusammen (ist etwas, das Sie ohne es nicht tun können, denke ich).

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