>But just because they call it `lazy' doesn't mean that it really is
>the essence of laziness. I prefer to use the more neutral name `lifted
>lambda calculus' for their calculus.
I disagree. In the simplest case (just lambdas, variables and applications,
i.e. no explicit constructors), it is *essential* that the function space
is lifted, otherwise lazy constructors cannot be programmed (the type
system needs to be sufficiently flexible e.g. untyped or system F etc.).
If lazy constructors are added to the calculus (distinct from functions),
then they achieve the behaviour that lifted functions achieved in the
simplest version of the calculus. Note however that, unless function spaces
are lifted, the calculus is more complex than simply being a weak lambda
calculus. In particular, I wouldn't like to guess what the canonical model
is, or even if one exists.
John.
