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

[Janis Voigtlaender]

ajb at spamcop.net wrote:
> 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.)

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 at tcs.inf.tu-dresden.de