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