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)))
> 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
> 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.
> The introduction to GADT usually starts with a little expression
> evaluator. So I gave it a try, but there are some troubles.
Actually, the generalization is not necessarily trivial at all, depending on
what you need to do with your ASTs.
>> 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
You're using a first-order abstract syntax. Each GADT branch corresponds to
one of the typing rule of your language, and when you introduce variables,
your typing rules end up needing an extra environment (which maps each var
to its type), which you also need to add here: E env a. Building up `env'
is left as an exercise.
An alternative is to use higher-order abstract syntax, which correspond to
using hypothetic judgments in your typing rules instead of an
extra environment. I.e. something like:
data E a where
Lit :: a -> E a
App :: E (a -> b) -> E a -> E b
Lam :: (E a -> E b) -> E (a -> b)
eval (Lit x) = x
eval (App f x) = (eval f) (eval x)
eval (Lam f) x = f (Lit x)