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

[Lennart Augustsson]

For Bool, I'm not sure, but for, e.g., () it's certainly true.
Take this definition of ==
  () == _  =  True
Using case analysis of just the constructors, ignoring the value
bottom, you can easily prove symmetry.
But '() == undefined' terminates, whereas 'undefined == ()' does not.

Ignore bottom at your own peril.

BTW, the id function works fine on bottom, both from a semantic and
implementation point of view.

  -- Lennart

On Sun, May 23, 2010 at 11:23 AM, Alexander Solla <ajs at 2piix.com> wrote:
>
> On May 23, 2010, at 1:35 AM, Jon Fairbairn wrote:
>
>> It seems to me relevant here, because one of the uses to which
>> one might put the symmetry rule is to replace an expression “e1
>> == e2” with “e2 == e1”, which can turn a programme that
>> terminates into a programme that does not.
>
> I don't see how that can be (but if you have a counter example, please show
> us).  Even if we extend == to apply to equivalence classes of bottom values,
> we would have to evaluate both e1 and e2 to determine the value of e1 == e2
> or e2 == e1.
>
> Prelude> undefined == True
> *** Exception: Prelude.undefined
> Prelude> True == undefined
> *** Exception: Prelude.undefined
> Prelude> undefined == undefined
> *** Exception: Prelude.undefined
>
> That is, if one case is exceptional, so is the other.
>
> You can't really even quantify over bottoms in Haskell, as a language.  The
> language runtime is able to do some evaluation and sometimes figure out that
> a bottom is undefined.  Sometimes.  But the runtime isn't a part of the
> language.  The runtime is an implementation of the language's interpetation
> function.  Bottoms are equivalent by conceptual fiat (in other words,
> vacuously) since not even the id :: a -> a function applies to
> them._______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>