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
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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe