> So, as Lennart says, if we allow constructors to be strict in functions
> then we have to change the semantics to distinguish _|_ from (\x -> _|_).
> I, for one, am deeply reluctant to do so; I certainly have no good handle on
> the consequences of doing so. Does anyone else?
I thought this inequality was one of the distinguishing characteristics of
lazy functional programming relative to the standard lambda-calculus. To
quote from Abramsky's contribution to "Research Topics in Functional
Programming", Addison-Wesley 1990:
Let O == (\x.xx)(\x.xx) be the standard unsolvable term. Then
\x.O = O
in the standard theory, since \x.O is also unsolvable; but \x.O is in
weak head normal form and hence should be distinguished from O in our
"lazy" theory.
Gerald
