# lambda evaluator in GADT Classic List Threaded 2 messages Reply | Threaded
Open this post in threaded view
|

## lambda evaluator in GADT

 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 _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

## Re: lambda evaluator in GADT

 > 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 _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe