G'day. Quoting Janis Voigtlaender <[EMAIL PROTECTED]>:
Hmm, but I can easily define an instance of Eq that does not satisfy this invariant. And I want the generated free theorem to be true for any legal Haskell program.
I would think that if x == y isn't the same as not (x /= y) for some type, then it isn't a legal Haskell program, because it breaks a fairly obvious invariant of Eq. (The consensus on #haskell is that this is even true for NaNs, but I'd like to get an official ruling on that.) Unfortunately, the H98 report doesn't say this explicitly, so you're technically correct that such a misbehaving program is "legal". Many invariants of this form are expressed as default instances, and if not, they should be. Obviously that's impossible in the case of, say, the associative law of Monoid. However, that isn't a precondition for a free theorem.
Of course, it does not affect the correctness of the generated theorem, just its legibility.
Of course. Consider this user feedback. :-) Cheers, Andrew Bromage _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
