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

[ajb at spamcop.net]

G'day.

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

Cheers,
Andrew Bromage