[Haskell] Announce: revamped free theorems generator

[Janis Voigtländer]

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.

Oh, I guess it was not so easy to recognize because Sebastian wasn't
really interested in that isomorphism, but in the number (and structure)
of inhabitants of the original type. But of course, that should follow
from the way the isomorphism is set up, in your proof or in general.

Anyway,...
Janis.

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