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

[ajb at spamcop.net]

[Ccing to haskell-cafe; please direct any replies there instead of haskell]

G'day all.

First of all, once again well done to Sascha on a great tool.

Just a few comments.

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

> - support for type classes
>   (e.g., enter "elem" and note the generated respects-restrictions)

This is a great feature, and it'll be even better when constructor
classes are done.

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.

The type (Monoid a) => [a] -> a gives:

     forall t1,t2 in TYPES(Monoid), g :: t1 -> t2, g
     respects Monoid.
      forall x :: [t1]. g (f x) = f (map g x)

     The class restriction occurring therein is defined as follows:

     g respects Monoid if
       g mempty = mempty
       forall x :: t1.
        forall y :: t1. g (mappend x y) = mappend (g x) (g y)
       forall (x, y) in lift{[]}(g). g (mconcat x) = mconcat y

Again, mconcat is redundant.  Even more curiously, though, map
appears in the theorem, but lift{[]} appears in the class restriction.

Cheers,
Andrew Bromage