Using "syntactic" to implement the lambda calculus

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
2 messages Options
Reply | Threaded
Open this post in threaded view
|

Using "syntactic" to implement the lambda calculus

Alex Rozenshteyn
(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


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

Re: Using "syntactic" to implement the lambda calculus

Emil Axelsson-2
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


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe