[Haskell] Announce: revamped free theorems generator

[Sebastian Fischer]

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.)