[Haskell] Announce: revamped free theorems generator

[Jean-Philippe Bernardy]

On Tue, Jun 22, 2010 at 1:32 PM, Janis Voigtländer
<jv at informatik.uni-bonn.de> wrote:

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

Actually I had misread the type. Transforming

forall a. (Bool -> a) -> a

into

Bool

is a direct consequence of our main theorem.
In fact it is a consequence of the simpler theorem:

forall a. (F a -> a) -> a = μ F

Cheers,
JP.