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