[Haskell-cafe] Lazy Lambda Calculus implementation

[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