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