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

[Derek Elkins]

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.