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

Jonas Almström Duregård jonas.duregard at gmail.com
Mon May 24 09:48:14 EDT 2010


>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.

In which sense does id need to evaluate its argument? If evaluating
the statement "id undefined" in ghci, then the print function (and
ultimately the show function) evaluates the undefined. I suppose that
if the show function does not evaluate its argument then there will be
no error, right?

/Jonas

On 24 May 2010 09:05, Alexander Solla <ajs at 2piix.com> wrote:
>
> 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.
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>


More information about the Haskell-Cafe mailing list