The introduction to GADT usually starts with a little expression evaluator. So I gave it a try, but there are some troubles. A little data type for lambda expression
data E a where Lit :: a -> E a App :: E (a -> b) -> E a -> E b Lam :: Var a -> E b -> E (a -> b) Val :: Var a -> E a
data Var a = Var String
some sample values
e1 = Lit 1 plus = Lit (\x y -> x + y)
Next, plus' demonstrate a pitfall in my data definition, i.e., the variable introduced by Lam has type forall a . a, which is is too general force a constraint on its occurrances. I wonder if there a way to make it work.
plus' = let v1 = Var "x" v2 = Var "y" in Lam v1 (Lam v2 (App (App plus (Val v1)) (Val v2)))
evaluation
eval :: E a -> a eval (Lit x) = x eval (App f x) = (eval f) (eval x) eval (Lam (Var v) e) = \x -> eval (sub v (Lit x) e) eval (Val (Var v)) = undefined
substituation
sub :: String -> E b -> E c -> E c sub v e e1@(Lit x) = e1 sub v e (App f x) = App (sub v e f) (sub v e x) sub v e e'@(Lam w'@(Var w) x) = if v == w then e' else Lam w' (sub v e x)
the above all works fine, except for the following
{-- sub v e e'@(Val (Var w)) = if v == w then e else e' --}
It seems the last case requires a unification of b and c, which is simply too strong for other cases. What should I do here? Instead of substituting on term level, an alternative way to implement eval is to use an environment to map variables to its values, but that requires all expression values to have a uniform type, which is a conflict to GADT. I'm sure this could be a common issue encountered by GADT beginners, how does one get around it? One solution on top of my head is to use a sum type (or even type class) and stuff every possible value types under it, but that defeats the purpose of using GADT in the first place. Any help is greatly appreciated! Regards, Paul Liu