# [Haskell] Announce: revamped free theorems generator

Janis Voigtländer jv at informatik.uni-bonn.de
Sun Jun 20 06:47:28 EDT 2010

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