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

[Alexander Solla]

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.