[Haskell] Announce: revamped free theorems generator
jv at informatik.uni-bonn.de
Fri Jun 18 14:29:09 EDT 2010
rossberg at mpi-sws.org schrieb:
>> The online free theorems generator, previously announced here:
>> now runs at:
> 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
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".
Jun.-Prof. Dr. Janis Voigtländer
mailto:jv at iai.uni-bonn.de
More information about the Haskell