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.