[Haskell] Announce: revamped free theorems generator

Sebastian Fischer sebf at informatik.uni-kiel.de
Sat Jun 19 08:09:03 EDT 2010


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}` ?


Underestimating the novelty of the future is a time-honored tradition.

More information about the Haskell mailing list