[Haskell] Announce: revamped free theorems generator

[Janis Voigtländer]

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.

In personal communication, Jean-Philippe added that for your type "(Bool
-> 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
mentioned above about countability of type a, and additionally involve a
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