(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 |
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 |
Free forum by Nabble | Edit this page |