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

Did you manage to do this now?

Driven by Andreas' comment about what he considers "free theorems",
statements like the above about an exhaustive enumeration of possible
values of a given type, like

- ($True) and ($False) for type (Bool -> a) -> a
- id for type a -> a

I thought a bit about whether it would be easy to add a strategy to the
online generator to produce such results in addition to the current
output. (BTW, regarding Andreas' concern about what should actually be
called a "free theorem": Wadler's original paper lists numerous examples
in the introduction of what *he* considers to be free theorems, and
they *all* can be automatically generated by our online generator as is.)

In any case, for additional possibilities like "exhaustive value
enumeration (where possible at all)", I don't yet have a generic
strategy. For Andreas' example, actually the generator already leads
almost there. It gives:

   forall f :: a -> a.
    forall t1,t2 in TYPES, g :: t1 -> t2.
     forall x :: t1. g (f x) = f (g x)

Simply set g = const e for any e, and we get:

   forall f :: a -> a. forall e. e = f e

For your example, it's a bit more difficult. The free theorems generator
gives:

   forall f :: (Bool -> a) -> a.
    forall t1,t2 in TYPES, R in REL(t1,t2).
     forall p :: Bool -> t1.
      forall q :: Bool -> t2.
       (forall x :: Bool. (p x, q x) in R) ==> ((f p, f q) in R)

Assume there were an f :: (Bool -> a) -> a that is neither ($True) nor
($False). Then there would have to be some p and q such that

   f p /= p True
   f q /= q False

Now set R = {(p True, q True), (p False, q False)}.

Clearly, the condition (forall x :: Bool. (p x, q x) in R) is fulfilled.

So by the above statement, we should also have (f p, f q) in R. But
that's clearly not possible, because it would mean

   (f p, f q) = (p True, q True)

or

   (f p, f q) = (p False, q False)

which are both in contradiction to f p /= p True, f q /= q False.

Ciao,
Janis.

-- 
Jun.-Prof. Dr. Janis Voigtländer
http://www.iai.uni-bonn.de/~jv/
mailto:jv at iai.uni-bonn.de