On May 23, 2010, at 2:53 AM, Lennart Augustsson wrote:
BTW, the id function works fine on bottom, both from a semantic and implementation point of view.
Yes, but only because it doesn't work at all. Consider that calling
id undefined
requires evaluating undefined before you can call id. The program will "crash" before you ever call id. Of course, the identity function "should" have produced a value that crashed in exactly the same way. But we never got there. It works in same way (==) works on bottoms. Vacuously. Indeed, functions only work on values. There is no value of type (forall a . a). Ergo, id does not work on undefined, as a function applying to a value. It is happy coincidence that the behavior of the runtime can be made mostly compatible with our familiar semantics. But not entirely. Consider: *Main> let super_undefined = super_undefined *Main> undefined == super_undefined *** Exception: Prelude.undefined *Main> super_undefined == super_undefined (wait forever) *Main> id super_undefined (wait forever) *Main> id undefined *** Exception: Prelude.undefined From a mathematical perspective, super_undefined is Prelude.undefined. But it takes some runtime level hackery to make undefined an exceptional "value". Without it, super_undefined loops, despite the fact that their definitions are exactly the same (The "value" defined by itself). I did not suggest those are the wrong semantics. Only that the study of their semantics doesn't belong to the study of Haskell as a logic/ language.