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:j...@iai.uni-bonn.de
_______________________________________________
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
