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

Good!

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:

http://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt

Ciao,
Janis.

--
Jun.-Prof. Dr. Janis Voigtländer
http://www.iai.uni-bonn.de/~jv/
mailto:j...@iai.uni-bonn.de
_______________________________________________
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

Reply via email to