[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
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
More information about the Haskell
mailing list