Re: [Haskell-cafe] Are arbitrary rank types and existentials equivalent?

Thank you, everyone. You have addressed my concerns very accurately. So in short, higer rank types subsume existentials. Good. And the burden of emulating existentials can be lowered by a suitable macro system. Very good. 2008/11/9 Derek Elkins <derek.a.elkins@gmail.com>:

There are various rules for moving quantifiers around. Any text on intuitionistic predicate logic should list the rules.

Err, where can I find such texts? I don't even understand "intuitionistic predicate logic" :-( Cheers, Loup