# [Haskell] Announce: revamped free theorems generator

Janis Voigtländer jv at informatik.uni-bonn.de
Tue Jun 22 07:32:38 EDT 2010

```Sebastian Fischer schrieb:
>
> On Jun 20, 2010, at 12:47 PM, Janis Voigtländer wrote:
>
>>> 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?
>
> Now it seems you did it for me, thanks!
>
> I am interested in a more general statement like
>
> For every given type  a  and function  f :: forall b . (a -> b) -> b
> there exists an  x :: a  such that  f = (\$x)  .

My gut feeling is that this statement indeed holds. To prove it, one
might have to use a generalization of the logical relations proof
technique from binary relations to n-ary relations, where n is the
number of inhabitants of your fixed type a.

For finite n, the mentioned generalization is unproblematic, so the
argument easily transfers from a=Bool to all finite a. For countable n,
I am not aware of the proper formal development, but again I think that
the statement holds. Whether to prove this via a generalization to
relations with countable arity, or whether via some encoding into list
types or so, I don't know...

> Jean-Philippe's remark
>
>> Using the main result of our ESOP paper (Testing Polymorphic Properties),
>> you can get there for a large class of input types.
>
> suggests that this may not be true for certain types  a  .
>
> I need to read his paper again for the proof idea. Maybe I'll find a
> counter example then.

-> a) -> a" the statement that any such function is either (\$True) or
(\$False) does *not* follow from the results in that paper. So I gather
that you will find neither proof nor counterexample for the more general
statement in that paper either. (It's worth reading nevertheless!)

> A variant of the above statement incorporating type classes is:
>
> For every given type  a  and function
>
>     f :: forall b . Monoid b => ((a -> b) -> b)
>
> one of the following cases holds:
>
>     there exists  x  such that  f = \k -> k x
>
>     f = \_ -> mempty
>
>     there exists  g  and  h  such that  f = \k -> g k `mappend` h k

My take would be: for any a and f as you mention, there is a list l::[a]
such that

f k = foldr mappend mempty (map k l)

That would be under the precondition (only) that all Monoid instances
satisfy the monoid laws.

If we don't have this precondition, then instead of l::[a] I would
demand the existence of some binary (or empty) tree with leaf nodes of
type a, and in the definition of f above, I would replace the map and
foldr by the corresponding operations over such trees.

In both cases, your statement that f is either (\$x) for some x::a or is
const mempty or can be "factored" into some g and h via mappend, is a
relatively direct consequence of my statement(s).

> I find these statements plausible and would be interested in counter
> examples. If they are true, I'd feel that they may be easily shown by
> type information only, that is via free theorems.

I'm pretty confident that there are no counterexamples. A proof via
type-based reasoning would of course have to solve the problems I
free theorem involving type class Monoid (which the online generator can
derive, albeit for the case of binary relations/functions only, of course).

Ciao,
Janis.

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