Announce: revamped free theorems generator
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 Thanks to Matthias Bartsch, there are now additional features in the online tool. In particular, one can declare one's own algebraic data types, type synonyms, type renamings, and type classes, and then generate free theorems for types involving those. Also, the tool now outputs inline graphics with nicely typeset theorems. (Plain text output, as well as .pdf and corresponding .tex, are still possible.) Ciao, Janis. -- Jun.-Prof. Dr. Janis Voigtländer http://www.iai.uni-bonn.de/~jv/ mailto:jv@iai.uni-bonn.de
Hello, I tried to use the free theorem generator in order to check whether the only values of type `(Bool -> a) -> a` are `($True)` and `($False)`. However, I don't manage to interpret the result: forall t1,t2 in TYPES, g :: t1 -> t2. forall p :: Bool -> t1. forall q :: Bool -> t2. (forall x :: Bool. g (p x) = q x) ==> (g (f_{t1} p) = f_{t2} q) What are `f_{t1}` and `f_{t2}` ? Regards, Sebastian -- Underestimating the novelty of the future is a time-honored tradition. (D.G.)
Sebastian Fischer schrieb:
Hello,
I tried to use the free theorem generator in order to check whether the only values of type `(Bool -> a) -> a` are `($True)` and `($False)`. However, I don't manage to interpret the result:
forall t1,t2 in TYPES, g :: t1 -> t2. forall p :: Bool -> t1. forall q :: Bool -> t2. (forall x :: Bool. g (p x) = q x) ==> (g (f_{t1} p) = f_{t2} q)
What are `f_{t1}` and `f_{t2}` ?
... the instantiations of polymorphic function f :: (Bool -> a) -> a at types "a = t1" and "a = t2". In some situations, it is nice or even necessary to see this made explicit. In Haskell, the instantiation will happen silently, of course, so you can simply read f_{t1} and f_{t2} both as f. Indeed, by making a tick in the "hide type instantiations" option box, the generator will omit the instantiations in the output. Ciao, Janis. -- Jun.-Prof. Dr. Janis Voigtländer http://www.iai.uni-bonn.de/~jv/ mailto:jv@iai.uni-bonn.de
Sebastian Fischer schrieb:
Hello,
I tried to use the free theorem generator in order to check whether the only values of type `(Bool -> a) -> a` are `($True)` and `($False)`.
Did you manage to do this now? Driven by Andreas' comment about what he considers "free theorems", statements like the above about an exhaustive enumeration of possible values of a given type, like - ($True) and ($False) for type (Bool -> a) -> a - id for type a -> a I thought a bit about whether it would be easy to add a strategy to the online generator to produce such results in addition to the current output. (BTW, regarding Andreas' concern about what should actually be called a "free theorem": Wadler's original paper lists numerous examples in the introduction of what *he* considers to be free theorems, and they *all* can be automatically generated by our online generator as is.) In any case, for additional possibilities like "exhaustive value enumeration (where possible at all)", I don't yet have a generic strategy. For Andreas' example, actually the generator already leads almost there. It gives: forall f :: a -> a. forall t1,t2 in TYPES, g :: t1 -> t2. forall x :: t1. g (f x) = f (g x) Simply set g = const e for any e, and we get: forall f :: a -> a. forall e. e = f e For your example, it's a bit more difficult. The free theorems generator gives: forall f :: (Bool -> a) -> a. forall t1,t2 in TYPES, R in REL(t1,t2). forall p :: Bool -> t1. forall q :: Bool -> t2. (forall x :: Bool. (p x, q x) in R) ==> ((f p, f q) in R) Assume there were an f :: (Bool -> a) -> a that is neither ($True) nor ($False). Then there would have to be some p and q such that f p /= p True f q /= q False Now set R = {(p True, q True), (p False, q False)}. Clearly, the condition (forall x :: Bool. (p x, q x) in R) is fulfilled. So by the above statement, we should also have (f p, f q) in R. But that's clearly not possible, because it would mean (f p, f q) = (p True, q True) or (f p, f q) = (p False, q False) which are both in contradiction to f p /= p True, f q /= q False. Ciao, Janis. -- Jun.-Prof. Dr. Janis Voigtländer http://www.iai.uni-bonn.de/~jv/ mailto:jv@iai.uni-bonn.de
On Sun, Jun 20, 2010 at 12:47 PM, Janis Voigtländer <jv@informatik.uni-bonn.de> wrote:
Sebastian Fischer schrieb:
Hello,
I tried to use the free theorem generator in order to check whether the only values of type `(Bool -> a) -> a` are `($True)` and `($False)`.
Did you manage to do this now?
Driven by Andreas' comment about what he considers "free theorems", statements like the above about an exhaustive enumeration of possible values of a given type, like
- ($True) and ($False) for type (Bool -> a) -> a - id for type a -> a
In any case, for additional possibilities like "exhaustive value enumeration (where possible at all)", I don't yet have a generic strategy.
Using the main result of our ESOP paper (Testing Polymorphic Properties), you can get there for a large class of input types. http://publications.lib.chalmers.se/cpl/record/index.xsql?pubid=99387 Cheers, JP.
Jean-Philippe Bernardy schrieb:
On Sun, Jun 20, 2010 at 12:47 PM, Janis Voigtländer <jv@informatik.uni-bonn.de> wrote:
Sebastian Fischer schrieb:
Hello,
I tried to use the free theorem generator in order to check whether the only values of type `(Bool -> a) -> a` are `($True)` and `($False)`. Did you manage to do this now?
Driven by Andreas' comment about what he considers "free theorems", statements like the above about an exhaustive enumeration of possible values of a given type, like
- ($True) and ($False) for type (Bool -> a) -> a - id for type a -> a
In any case, for additional possibilities like "exhaustive value enumeration (where possible at all)", I don't yet have a generic strategy.
Using the main result of our ESOP paper (Testing Polymorphic Properties), you can get there for a large class of input types.
http://publications.lib.chalmers.se/cpl/record/index.xsql?pubid=99387
Yes, kind of. I had this in mind when asking Andreas for a kind of characterization akin to his "f :: a -> a can only be identity" example, but for the type [a] -> [a]. The point being that one doesn't get a finite enumeration of possible values, except in very few cases. BTW, can one get a characterization from your results, establishing *when* the class of possible (semantic) values of a type is finite? Ciao, Janis. -- Jun.-Prof. Dr. Janis Voigtländer http://www.iai.uni-bonn.de/~jv/ mailto:jv@iai.uni-bonn.de
On Jun 20, 2010, at 12:47 PM, Janis Voigtländer wrote:
I tried to use the free theorem generator in order to check whether the only values of type `(Bool -> a) -> a` are `($True)` and `($False)`.
Did you manage to do this now?
Now it seems you did it for me, thanks! I am interested in a more general statement like For every given type a and function f :: forall b . (a -> b) -> b there exists an x :: a such that f = ($x) . Jean-Philippe's remark
Using the main result of our ESOP paper (Testing Polymorphic Properties), you can get there for a large class of input types.
suggests that this may not be true for certain types a . I need to read his paper again for the proof idea. Maybe I'll find a counter example then. A variant of the above statement incorporating type classes is: For every given type a and function f :: forall b . Monoid b => ((a -> b) -> b) one of the following cases holds: there exists x such that f = \k -> k x f = \_ -> mempty there exists g and h such that f = \k -> g k `mappend` h k I find these statements plausible and would be interested in counter examples. If they are true, I'd feel that they may be easily shown by type information only, that is via free theorems. Sebastian -- Underestimating the novelty of the future is a time-honored tradition. (D.G.)
Sebastian Fischer schrieb:
On Jun 20, 2010, at 12:47 PM, Janis Voigtländer wrote:
I tried to use the free theorem generator in order to check whether the only values of type `(Bool -> a) -> a` are `($True)` and `($False)`.
Did you manage to do this now?
Now it seems you did it for me, thanks!
I am interested in a more general statement like
For every given type a and function f :: forall b . (a -> b) -> b there exists an x :: a such that f = ($x) .
My gut feeling is that this statement indeed holds. To prove it, one might have to use a generalization of the logical relations proof technique from binary relations to n-ary relations, where n is the number of inhabitants of your fixed type a. For finite n, the mentioned generalization is unproblematic, so the argument easily transfers from a=Bool to all finite a. For countable n, I am not aware of the proper formal development, but again I think that the statement holds. Whether to prove this via a generalization to relations with countable arity, or whether via some encoding into list types or so, I don't know...
Jean-Philippe's remark
Using the main result of our ESOP paper (Testing Polymorphic Properties), you can get there for a large class of input types.
suggests that this may not be true for certain types a .
I need to read his paper again for the proof idea. Maybe I'll find a counter example then.
In personal communication, Jean-Philippe added that for your type "(Bool -> a) -> a" the statement that any such function is either ($True) or ($False) does *not* follow from the results in that paper. So I gather that you will find neither proof nor counterexample for the more general statement in that paper either. (It's worth reading nevertheless!)
A variant of the above statement incorporating type classes is:
For every given type a and function
f :: forall b . Monoid b => ((a -> b) -> b)
one of the following cases holds:
there exists x such that f = \k -> k x
f = \_ -> mempty
there exists g and h such that f = \k -> g k `mappend` h k
My take would be: for any a and f as you mention, there is a list l::[a] such that f k = foldr mappend mempty (map k l) That would be under the precondition (only) that all Monoid instances satisfy the monoid laws. If we don't have this precondition, then instead of l::[a] I would demand the existence of some binary (or empty) tree with leaf nodes of type a, and in the definition of f above, I would replace the map and foldr by the corresponding operations over such trees. In both cases, your statement that f is either ($x) for some x::a or is const mempty or can be "factored" into some g and h via mappend, is a relatively direct consequence of my statement(s).
I find these statements plausible and would be interested in counter examples. If they are true, I'd feel that they may be easily shown by type information only, that is via free theorems.
I'm pretty confident that there are no counterexamples. A proof via type-based reasoning would of course have to solve the problems I mentioned above about countability of type a, and additionally involve a free theorem involving type class Monoid (which the online generator can derive, albeit for the case of binary relations/functions only, of course). Ciao, Janis. -- Jun.-Prof. Dr. Janis Voigtländer http://www.iai.uni-bonn.de/~jv/ mailto:jv@iai.uni-bonn.de
On Tue, Jun 22, 2010 at 1:32 PM, Janis Voigtländer <jv@informatik.uni-bonn.de> wrote:
I need to read his paper again for the proof idea. Maybe I'll find a counter example then.
In personal communication, Jean-Philippe added that for your type "(Bool -> a) -> a" the statement that any such function is either ($True) or ($False) does *not* follow from the results in that paper. So I gather that you will find neither proof nor counterexample for the more general statement in that paper either. (It's worth reading nevertheless!)
Actually I had misread the type. Transforming forall a. (Bool -> a) -> a into Bool is a direct consequence of our main theorem. In fact it is a consequence of the simpler theorem: forall a. (F a -> a) -> a = μ F Cheers, JP.
Jean-Philippe Bernardy schrieb:
On Tue, Jun 22, 2010 at 1:32 PM, Janis Voigtländer <jv@informatik.uni-bonn.de> wrote:
I need to read his paper again for the proof idea. Maybe I'll find a counter example then. In personal communication, Jean-Philippe added that for your type "(Bool -> a) -> a" the statement that any such function is either ($True) or ($False) does *not* follow from the results in that paper. So I gather that you will find neither proof nor counterexample for the more general statement in that paper either. (It's worth reading nevertheless!)
Actually I had misread the type. Transforming
forall a. (Bool -> a) -> a
into
Bool
is a direct consequence of our main theorem.
Good!
In fact it is a consequence of the simpler theorem:
forall a. (F a -> a) -> a = μ F
I like your use of the word "simpler" here. :-) And this now reminds me of Wadler's note "Recursive types for free!" which is of course just that, and should be able to answer Sebastian's question in many cases: http://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt Ciao, Janis. -- Jun.-Prof. Dr. Janis Voigtländer http://www.iai.uni-bonn.de/~jv/ mailto:jv@iai.uni-bonn.de
Jean-Philippe Bernardy schrieb:
On Tue, Jun 22, 2010 at 1:32 PM, Janis Voigtländer <jv@informatik.uni-bonn.de> wrote:
I need to read his paper again for the proof idea. Maybe I'll find a counter example then. In personal communication, Jean-Philippe added that for your type "(Bool -> a) -> a" the statement that any such function is either ($True) or ($False) does *not* follow from the results in that paper. So I gather that you will find neither proof nor counterexample for the more general statement in that paper either. (It's worth reading nevertheless!)
Actually I had misread the type. Transforming
forall a. (Bool -> a) -> a
into
Bool
is a direct consequence of our main theorem.
Oh, I guess it was not so easy to recognize because Sebastian wasn't really interested in that isomorphism, but in the number (and structure) of inhabitants of the original type. But of course, that should follow from the way the isomorphism is set up, in your proof or in general. Anyway,... Janis. -- Jun.-Prof. Dr. Janis Voigtländer http://www.iai.uni-bonn.de/~jv/ mailto:jv@iai.uni-bonn.de
On Jun 22, 2010, at 1:32 PM, Janis Voigtländer wrote:
A variant of the above statement incorporating type classes is: For every given type a and function f :: forall b . Monoid b => ((a -> b) -> b) one of the following cases holds: there exists x such that f = \k -> k x f = \_ -> mempty there exists g and h such that f = \k -> g k `mappend` h k
My take would be: for any a and f as you mention, there is a list l:: [a] such that
f k = foldr mappend mempty (map k l)
That makes sense because (I think) the type newtype FreeMonoid a = FreeMonoid { (>>-) :: forall m . Monoid m => (a -> m) -> m } is a free monoid over a and, thus, isomorphic to [a] : First, `FreeMonoid a` is a monoid via instance Monoid (FreeMonoid a) where mempty = FreeMonoid (\_ -> mempty) a `mappend` b = FreeMonoid (\k -> (a >>- k) `mappend` (b >>- k)) Second, for every monoid m and mapping `f :: a -> m` there is a unique monoid homomorphism from `FreeMonoid a` to m , namely `(>>- f)` . It follows that `(>>-(:[]))` and `foldr mappend mempty` are monoid isomorphisms. I am interested in the mentioned laws because I want to show the monad laws for the definition instance Monad FreeMonoid where return x = FreeMonoid ($x) a >>= f = a >>- f This definition of `>>=` is *not* the usual one for continuation monads, but if the mentioned properties hold, I think it also satisfies the monad laws. The theorem
forall a. (F a -> a) -> a = μ F
looks interesting. I wonder whether it could be adapted to incorporate a type-class constraint. I'll also look into Phil Wadler's draft on Recursive types for free. Thanks! Sebastian -- Underestimating the novelty of the future is a time-honored tradition. (D.G.)
On Jun 22, 2010, at 5:20 PM, Sebastian Fischer wrote:
It follows that `(>>-(:[]))` and `foldr mappend mempty` are monoid isomorphisms.
I meant (>>-(:[])) :: FreeMonoid a -> [a] and foldr mappend mempty . map return :: [a] -> FreeMonoid a -- Underestimating the novelty of the future is a time-honored tradition. (D.G.)
Sebastian Fischer wrote:
I am interested in the mentioned laws because I want to show the monad laws for the definition
instance Monad FreeMonoid where return x = FreeMonoid ($x) a >>= f = a >>- f
This definition of `>>=` is *not* the usual one for continuation monads, but if the mentioned properties hold, I think it also satisfies the monad laws.
Yes, it does satisfy the monad laws because FreeMonoid is the "free algebra functor" T for monoids as a T-algebra. In other words, a type A is a monoid exactly when there is a map T A -> A . I've learned this idea from Dan Piponi: http://blog.sigfpe.com/2007/02/monads-for-vector-spaces-probability.html http://blog.sigfpe.com/2007/06/monads-from-algebra-and-the-gray-code.html Regards, Heinrich Apfelmus -- http://apfelmus.nfshost.com
participants (4)
-
Heinrich Apfelmus -
Janis Voigtländer -
Jean-Philippe Bernardy -
Sebastian Fischer