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