[Haskell] Announce: revamped free theorems generator

Janis Voigtländer jv at informatik.uni-bonn.de
Tue Jun 22 10:56:19 EDT 2010

Jean-Philippe Bernardy schrieb:
> 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

I like your use of the word "simpler" here. :-)

And this now reminds me of Wadler's note "Recursive types for free!"
which is of course just that, and should be able to answer Sebastian's
question in many cases:



Jun.-Prof. Dr. Janis Voigtländer
mailto:jv at iai.uni-bonn.de

More information about the Haskell mailing list