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

[Janis Voigtlaender]

ajb at spamcop.net wrote:
> Some of these respects-restrictions arent as useful as they might be,
> because they don't take into account easily-predictable invariants.
> 
> For example, the type:
> 
>     (Eq a) => [a] -> [a]
> 
> generates the following restriction:
> 
>     g respects Eq if
>       forall x :: t1. forall y :: t1. (==) x y = (==) (g x) (g y)
>       forall x :: t1. forall y :: t1. (/=) x y = (/=) (g x) (g y)
> 
> Thats correct, but redundant, because (x == y) = (g x == g y) if and only
> if (x /= y) = (g x /= g y).  Crucially, you can work this out from the
> definition of Eq, because (/=) has a default implementation defined in
> terms of (==) alone.

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. If just requiring one of the two conditions
above, it is possible to write a function and instances of Eq so that
the theorem supposedly guaranteed by the function's type gets wrong.
The same applies to the Monoid example.

Also, the implementation is made for arbitrary user-declared type
classes, not just the ones from the standard libraries. It is easy to
parse the type signatures in a type class declaration. But to take
default method definitions into account as well, and automatically
working out the kind of redundancies that would allow to simplify
necessary restrictions, is next to impossible, I think.

> Even more curiously, though, map
> appears in the theorem, but lift{[]} appears in the class restriction.

Well-spotted. This was one of the small deficiencies that Sascha did not
come around to fix when time was running out towards the end of his MSc
thesis work on this project ;-)

Of course, it does not affect the correctness of the generated theorem,
just its legibility. In general, there are some other corners where one
could beneficially improve the amount of simplifications done. But my
most important point was to get *correct* statements out of the tool.
Overzealous simplification can easily compromise this aim (see above).

Ciao, Janis.

-- 
Dr. Janis Voigtlaender
http://wwwtcs.inf.tu-dresden.de/~voigt/
mailto:voigt at tcs.inf.tu-dresden.de