(This is intended as a simplification of the problem I actually need to solve.)

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.

I've read this post from the archives, but I still seem to be missing something.

Does anyone have any suggestions?

> -- Lambda calculus
> type Ident = String
> data Value = VLam Ident Expr
> data Expr = Var Ident | Lam Ident Expr | App Expr Expr
> eval :: Expr -> Value
> eval e =
>   case e of
>     Var _ -> error "not closed"
>     Lam i e' -> VLam i e'
>     App e1 e2 ->
>       case eval e1 of
>         Lam i e' -> subst e' (eval e2) i
>         _ -> error "illegal application"

> -- Lambda calculus with integers and addition
> data Value = VLam Ident Expr | VInt Integer
> data Expr = Var Ident | Lam Ident Expr | App Expr Expr | Plus Expr Expr
> eval e =
>   case e of
>     ...
>     Plus e1 e2 ->
>       case (eval e1, eval e2) of
>         (VInt x1, VInt x2) -> VInt $ x1 + x2
>         _ -> error "illegal addition"

--
          Alex R