[Haskell] Announce: revamped free theorems generator

[Janis Voigtländer]

rossberg at mpi-sws.org schrieb:
>> The online free theorems generator, previously announced here:
>>
>>    http://www.haskell.org/pipermail/haskell/2007-October/019917.html
>>
>> now runs at:
>>
>>    http://www-ps.iai.uni-bonn.de/ft
> 
> I don't quite understand. Isn't that tool basically just giving you the
> (unfolded) definition of logical relatedness at the type you enter? Although
> pretty "free", that is not yet a "free theorem", at least not as I am used
> to see this term used. For example, a free theorem for type a -> a would be
> the property forall f :: a -> a, forall e, f e = e.

I wouldn't say that statements of this form, completely determining the
function definition from the function's type, are what it needs to
qualify as a free theorem.

For one thing, that's only possible for very simple types. For example,
what would you say is a "not just unfolding the definition of the
logical relation"-style free theorem for the type [a] -> [a]?

For the type a -> a you mention, the generator gives the property forall
f :: a -> a, forall g, forall x, g (f x) = f (g x). I wouldn't say that
this is just unfolding the definition of logical relatedness. But maybe
more interestingly, consider type (a -> Bool) -> [a] -> [a]. The
generator answers:

forall f :: (a -> Bool) -> [a] -> [a], forall g, forall p, forall q,
  (forall x, p x = q (g x))
  => (forall y, map g (f p y) = f q (map g y))

I'd say that this *is* typically referred to as the free theorem
corresponding to filter's type, namely that the property

   map g . filter (q . g) = filter q . map g

holds for all like-wise typed functions.

In any case, I would be very interested in learning more about for what
and where you are used to see the term "free theorems" used, as I am
always interested in new applications of parametricity.

I can just say that myself I am very used to calling statements like the
one about filter above "free theorems".

Ciao,
Janis.

-- 
Jun.-Prof. Dr. Janis Voigtländer
http://www.iai.uni-bonn.de/~jv/
mailto:jv at iai.uni-bonn.de