[Haskell] Announce: revamped free theorems generator

[Sebastian Fischer]

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

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

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.

Sebastian

-- 
Underestimating the novelty of the future is a time-honored tradition.
(D.G.)