program lazylam; // -*-C-*-ish /* [Unfinished] evaluator for the untyped lambda calculus with integers, lazy version. */ // Raw values data Expr = Var(Int x) // de Bruijn indexed variable | Lam(Expr scope) // Binding | App(Expr f, Expr s) // Function application | Const(Int val) | Inc(Expr ni) | Dec(Expr nd) | PrimRec(Expr target,Expr mzero,Expr msuc) | If(Expr i, Expr t, Expr e); // Semantic representation of values. Difference from eager version is // that each recursive value is a suspension - Sem() rather than Sem. // We only evaluate these when we need them data Sem = SemLam(Sem(Sem()) scope) | SemConst(Int val) | SemPrimRec(Sem() target, Sem() mzero, Sem() msuc) | SemInc(Sem() ni) | SemDec(Sem() nd) | Blocked(Blocked f, [Sem()] args); // Irreducible terms data Blocked = BVar(Int x); data Spine<a> = Lin | Snoc(Spine<a> init, a last); type Ctxt = Spine<Sem()>; Exception FellOffEndOfContext; Sem lookup(Int v, Ctxt ctxt) { if (v==0) { return force(ctxt.last); // Evaluate it } else if (v>0) { return lookup(v-1,ctxt.init); } else { throw(FellOffEndOfContext); } } Sem eval(Ctxt ctxt, Expr e) { case e of { Var(v) -> return lookup(v,ctxt); | Lam(sc) -> return SemLam(lambda(arg) -> { eval(Snoc(ctxt,@arg),sc) }); | App(f,a) -> return app(ctxt,eval@(ctxt,f),eval@(ctxt,a)); | Const(c) -> return SemConst(c); | Inc(n) -> return increment(eval(ctxt,n)); | Dec(n) -> return decrement(eval(ctxt,n)); | PrimRec(t,z,s) -> return primrec(ctxt, eval@(ctxt,t),eval@(ctxt,z),eval@(ctxt,s)); | If(i,t,e) -> return runIf(ctxt, eval@(ctxt,i),eval@(ctxt,t),eval@(ctxt,e)); } } Sem app(Ctxt ctxt, Sem() f, Sem() a) { case f of { // Evaluate f SemLam(scfun) -> return scfun(@a); } } Sem increment(Sem n) { case n of { SemConst(c) -> return (SemConst(c+1)); } } Sem decrement(Sem n) { case n of { SemConst(c) -> return (SemConst(c-1)); } } Sem primrec(Ctxt ctxt, Sem() t, Sem() z, Sem() s) { case t of { // Evaluate t SemConst(x) -> if (x==0) { return z; // Evaluate z } else { dec = SemConst@(x-1); rec = primrec@(ctxt,dec,@z,@s); return app(ctxt,app@(ctxt,@s,@dec),@rec); } } } Sem runIf(Ctxt ctxt, Sem() i, Sem() t, Sem() e) { case i of { // Evaluate i, then t or e, but not both. SemConst(x) -> if (x!=0) { return t; } else { return e; } } } Void showSem(Sem v) { case v of { SemConst(x) -> putStrLn(String(x)); } } Void main() { // plus = \m n. primrec n m (\k ih. inc(ih)) plus = Lam(Lam(PrimRec(Var(0),Var(1), Lam(Lam(Inc(Var(0))))))); // mult = \m n. primrec n 0 (\k ih. plus m ih) mult = Lam(Lam(PrimRec(Var(0),Const(0), Lam(Lam(App(App(plus,Var(3)),Var(0))))))); // Wow, this works when we evaluate lazily! // y = \f . (\x. f (x x)) (\x. f (x x)) y = Lam(App(Lam(App(Var(1),App(Var(0),Var(0)))), Lam(App(Var(1),App(Var(0),Var(0)))))); // add4 = \x. y (\add4 x. if x==0 then 4 else 1+(add4 (x-1))) x addbody = Lam(Lam(If(Var(0),Inc(App(Var(1),(Dec(Var(0))))),Const(4)))); add4 = Lam(App(App(y,addbody),Var(0))); showSem(eval(Lin,App(App(mult, Const(6)),Const(7)))); // Wow, it works! showSem(eval(Lin,App(add4,Const(3)))); }