On Sun, 2008-11-09 at 13:46 +0100, Loup Vaillant wrote:
Maybe one subsumes the other?
What I want to know is if there is an easy way to emulate one with the other, and how much convenience is lost in doing so.
For instance, is it possible to implement stream fusion with rank2 types, or the ST monad with existantials?
Is there any paper discussing this kind of things?
exists a. F a ~ forall r. (forall a. F a -> r) -> r runST :: exist s. ST s a -> a -- this type is implied by runST's but does not imply runST's so it is less general There are various rules for moving quantifiers around. Any text on intuitionistic predicate logic should list the rules. However, this is replacing existentials with higher rank uses of universals. Higher rank types applies to any quantifier, and so to attempt to replace higher rank uses of universals would require higher rank uses of existentials in general.