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

ajb@spamcop.net wrote:

G'day.

Quoting Janis Voigtlaender :

...

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

Okay, it is quite natural to take this stand. But as you say, there is no such commitment in the language definition. And even if there were, I doubt it would be possible to enforce such invariants in a compiler. So there would be "illegal" programs that are nevertheless accepted by the compilers. Not what we want, do we, in Haskell land?

Many invariants of this form are expressed as default instances, and if not, they should be.

Agreed. I was about to answer that the situation is the same with the monad laws not being valid for some monad we all love, and still we do not consider the resulting programs illegal. But your point about the associativity law for Monoid is correct: these laws do not turn up as preconditions for a free theorem. So we are back to those invariants that are expressed as default instances. For Eq the invariant is quite obvious. But what about Ord? Certainly there is also an invariant that can be observed from its default instances, but I don't see how it could be read off mechanically. And that's really the point of free theorems: to get as far as possible with an automated process. Afterwards, one can always simplify by using knowledge not possibly available to the generation algorithm. So if for the Eq-instances we are actually interested in we really know that the invariant holds, we can of course do away with one of the two (==)-, (/=)-conditions. Alternatively, it would be possible to hard-code special treatment of Haskell's standard type classes into Sascha's tool, so that for Eq, Ord, and so on, a minimal set of conditions is imposed from the outset. But that would not help in general with type classes specified by the user. A more general solution here would really be welcome.

...

Of course, it does not affect the correctness of the generated theorem, just its legibility.

Of course. Consider this user feedback. :-)

Sure. More wanted :-) Ciao, Janis. -- Dr. Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/ mailto:voigt@tcs.inf.tu-dresden.de