rossberg@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:
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@iai.uni-bonn.de