Lazy Lambda Calculus implementation
Hello all, I've written the following implementation of Lambda Calculus, which will evaluate its Terms non-strictly. I've verified this since the Y combinator works without diverging: data Term a = Const a | Var Nat | Lam (Term a) | Term a :@ Term a data Val a = C a | F (Partial (Val a) -> Partial (Val a)) type Env a = [Partial (Val a)] eval' :: Term a -> Env a -> Partial (Val a) eval' (Const c) env = Now (C c) eval' (Var n) env = let Just x = lookUp env n in x eval' (Lam f) env = Now (F (\a -> eval' f (a:env))) eval' (f :@ x) env = do F f' <- eval' f env Later (f' (eval' x env)) eval t = eval' [] t Nat, Partial, lookUp, etc. have pretty obvious implementations. My question is, will this behave lazily? In other words will the contents of the 'env' lists be shared between the different contexts, such that forcing an element the be evaluated twice will only perform the evaluation once? Note that the first "do" line is the only place where evaluation is forced. If anyone could point out an 'obvious' reason why it will or will not be shared, or approaches I can take to check or infer this myself (eg. a Term which would show wildly different RAM usage in each case), I'd be very interested to know. I'd also be interested if someone spots a bug ;) For those who are curious, the code is living at https://gitorious.org/lazy-lambda-calculus and I've written a blog post detailing the iteration's I've been through at http://chriswarbo.net/index.php?page=news&type=view&id=admin-s-blog%2Flazy-lambda-calculus Cheers, Chris
Hello Chris, it looks to me like it should be shared. One approach to test this is "println-debugging". The Module Debug.Trace has functions to let you write to stdout as side-effect, outside the IO monad. import Debug.Trace(trace) eval' (Lam f) env = Now (F (\a -> eval' f (trace "evaluating element" a:env))) With this, you would get the output "evaluating element" whenever an entry in the list env is evaluated. HTH Thomas Am 07.02.2014 15:27, schrieb Chris Warburton:
Hello all, I've written the following implementation of Lambda Calculus, which will evaluate its Terms non-strictly. I've verified this since the Y combinator works without diverging:
data Term a = Const a | Var Nat | Lam (Term a) | Term a :@ Term a
data Val a = C a | F (Partial (Val a) -> Partial (Val a))
type Env a = [Partial (Val a)]
eval' :: Term a -> Env a -> Partial (Val a) eval' (Const c) env = Now (C c) eval' (Var n) env = let Just x = lookUp env n in x eval' (Lam f) env = Now (F (\a -> eval' f (a:env))) eval' (f :@ x) env = do F f' <- eval' f env Later (f' (eval' x env))
eval t = eval' [] t
Nat, Partial, lookUp, etc. have pretty obvious implementations.
My question is, will this behave lazily? In other words will the contents of the 'env' lists be shared between the different contexts, such that forcing an element the be evaluated twice will only perform the evaluation once? Note that the first "do" line is the only place where evaluation is forced.
If anyone could point out an 'obvious' reason why it will or will not be shared, or approaches I can take to check or infer this myself (eg. a Term which would show wildly different RAM usage in each case), I'd be very interested to know. I'd also be interested if someone spots a bug ;)
For those who are curious, the code is living at https://gitorious.org/lazy-lambda-calculus and I've written a blog post detailing the iteration's I've been through at http://chriswarbo.net/index.php?page=news&type=view&id=admin-s-blog%2Flazy-lambda-calculus
Cheers, Chris _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
participants (2)
-
Chris Warburton -
Thomas Horstmeyer