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
