[Haskell-cafe] Re: lambda evaluator in GADT

[Stefan Monnier]

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


        Stefan