[Haskell] Announce: revamped free theorems generator

[Janis Voigtländer]

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 at iai.uni-bonn.de