[Haskell-cafe] Re: [Haskell] Announce: generating free theorems, online and offline

ajb at spamcop.net ajb at spamcop.net
Thu Oct 18 02:13:44 EDT 2007


Quoting Janis Voigtlaender <voigt at tcs.inf.tu-dresden.de>:

> 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. :-)

Andrew Bromage

More information about the Haskell-Cafe mailing list