[Haskell-cafe] Re: Proof question -- (==) over Bool

[Alexander Solla]

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.