Quantification in free theorems (Was: [Haskell-cafe] Exercise in point free-style)

[ajb at spamcop.net]

G'day all.

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

> I find the omission of quantifications in the produced theorems
> problematic.

I agree.  Indeed, if you look at the source code, the quantifications
_are_ generated, they're just not printed.  The reason is that the
output was (re-)designed for use on IRC where space is at a premium.

However, you're correct that sometimes they're semantically important.
Fixed.

> For this, you produce the following theorem:
>
>    g x = h (f x)
>    =>
>    $map f . filter g = filter h . $map f

It now produces:

    filter (f . g) . $map f = $map f . filter g

Cheers,
Andrew Bromage