On Tue, Jun 22, 2010 at 1:32 PM, Janis Voigtländer <j...@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. _______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell