GADTs frente a MultiParamTypeClasses

Question

Estoy tratando de comprender GADTs, y he visto el GADTs example en el manual de GHC. Por lo que yo puedo decir, que es posible hacer lo mismo 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, que tenemos exactamente los mismos constructores y el mismo código exacto para eval (diseminación cruzar las definiciones de instancia) como en Ejemplo de GADTs de GHC.

Entonces, ¿qué es todo el pelusa sobre GADTs? ¿Hay algo que pueda hacer con GADTs que no puedo hacer con MultiParamTypeClasses? ¿O simplemente ofrecen una forma más concisa de hacer las cosas que yo podría hacer con MultiParamTypeClasses?

Answer 1

Usted puede poner valores GADT del mismo tipo pero con diferentes constructores en un recipiente convenientemente,

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

es sencillo, pero para obtener los mismos usando tipos y MPTCs distintas con dependencias funcionales es difícil al menos . En su enfoque de clase de tipo Multiparameter, Lit y If son constructores de diferentes tipos, por lo que uno necesitaría un tipo de envoltura para colocarlos en el mismo contenedor. El tipo de envoltorio sería, por lo que yo puedo ver, tiene que ser un tipo existencial a la

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

con un

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

para garantizar cierta seguridad de tipos y la capacidad de map funciones como eval sobre la lista. Así que estás a medio camino o más de vuelta a las GADT, menos la comodidad.

No estoy seguro de que haya algo que GADT le permita hacer y que no pueda lograr sin ellos, pero algunas cosas sacrificarían mucho de la elegancia.

Answer 2

GADTs simplemente le permite proporcionar una forma más natural de constructor definido y permite usar la coincidencia en el nivel de tipo y constructores todos juntos (es algo que no puede hacer sin él, creo).

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