# [Haskell-cafe] Using "syntactic" to implement the lambda calculus

Emil Axelsson emax at chalmers.se
Thu Jul 5 09:36:06 CEST 2012

```Hi Alex!

2012-07-03 20:18, Alex Rozenshteyn skrev:
> I'm trying to implement the lambda calculus (with CBV evaluation) using
> the "syntactic" package, in such a way that a simple extension is also
> simple to implement.
>
> I am stuck on the fact that it seems that the Value type needs to be
> parametrized over the Expr type and I can't seem to figure out how to do it.

The trick is to see that your `Expr` and `Value` can be merged to a
single type:

data Expr group
where
Var :: Ident -> Expr NONVAL
Lam :: Ident -> Expr any -> Expr VAL
App :: Expr any1 -> Expr any2 -> Expr NONVAL

data VAL
data NONVAL

type Value = Expr VAL

eval :: Expr any -> Value
...

(Here I'm using polymorphic constructors to emulate that `Value` is a
sub-type of `Expr`. I could have made a more direct translation with two
lambda constructors. Then all constructors would have been monomorphic.)

Once this is done, the conversion to Syntactic is easy:

data Var :: * -> * where Var :: Ident -> Var (Full NONVAL)
data Lam :: * -> * where Lam :: Ident -> Lam (any :-> Full VAL)
data App :: * -> * where App :: App (any1 :-> any2 :-> Full NONVAL)

type Expr group = ASTF (Lam :+: Var :+: App) group
type Value      = ASTF (Lam :+: Var :+: App) VAL

eval :: Expr any -> Value
eval var
| Just (Var _) <- prj var = error "not closed"
eval e@(lam :\$ _)
| Just (Lam _) <- prj lam = e
eval (app :\$ e1 :\$ e2)
| Just App <- prj app = case eval e1 of
(lam :\$ e) | Just (Lam i) <- prj lam   -> subst e (eval e2) i
_ -> error "illegal application"

subst :: Expr any -> Value -> Ident -> Value
subst = undefined

Of course, you need to generalize the types of `eval` and `subst` in
order to make them extensible. For more details, see this paper:

http://www.cse.chalmers.se/~emax/documents/axelsson2012generic.pdf

(The paper refers to syntactic-1.0 which hasn't been uploaded yet, so
there are some small differences.)

/ Emil

```