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 <a...@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@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
