There's a natural relation between higher rank types and existentials; one way to think about it is this: if you have some existential type t (subject to some constraints), you cannot operate on it except with some function that accepts any type t subject to those constraints. There is a simple encoding of existential types using higher rank types: Given

data E a1..an = forall e1...en. (constraints) => E t1..tn where t1..tn are types in terms of a1..an, we replace with data E' a1..an = E' (forall b. (forall e1..en. t1 -> t2 -> ... -> tn -> b) -> b)

Any function f that pattern matches on E can use E' instead in the following way:

f (E v1..vn) = exp becomes f (E' exist) = exist f' where f' v1..vn = exp

An example:

data HasShow = forall a. Show a => HasShow a data HasShow' = HasShow' (forall b. (forall a. Show a => (a -> b)) -> b)

useShow :: HasShow -> String useShow (HasShow x) = show x

useShow' :: HasShow' -> String useShow' (HasShow' f) = f (\x -> show x)

I don't think there is much a link between fusion and the type system; stream fusion is a compilation technology, like inlining. To demonstrate, here's a simple fusion engine using this encoding:

{-# LANGUAGE RankNTypes #-} module Fusion where

data StreamR s a = Done | Skip s | Yield a s newtype Stream a = Stream (forall b. (forall s. s -> (s -> StreamR s a) -> b) -> b)

stream :: [a] -> Stream a stream xs = Stream (\f -> f xs go) where go [] = Done go (x:xs) = Yield x xs {-# NOINLINE[1] stream #-}

unstream :: Stream a -> [a] unstream (Stream k) = k loop where loop s next = case (next s) of Done -> [] Skip s' -> loop s' next Yield a s' -> a : loop s' next {-# NOINLINE[1] unstream #-}

You then end up with the same (stream (unstream s) = s) rule:

{-# RULES "stream/unstream" forall s. stream (unstream s) = s #-}

Now lets implement a stream version of map:

mapS f = unstream . mapStream f . stream mapStream :: (a -> b) -> Stream a -> Stream b mapStream f (Stream k) = k mapStream' where mapStream' s0 next = Stream (\g -> g s0 go) where go s = case next s of Done -> Done Skip s' -> Skip s' Yield a s' -> Yield (f a) s'

test :: [Int] -> [Int] test = mapS (+1) . mapS (*2)

Looking at the core generated for "test", we see that the loops are indeed fused: (case x_ag7 of wild1_anS { GHC.Types.I# x1_anU -> GHC.Types.I# (GHC.Prim.+# (GHC.Prim.*# x1_anU 2) 1) }) (which basically says "x_ag7 * 2 + 1") I don't think there is an encoding that goes from higher rank types to existentials, however. Existentials lose information which cannot be recovered. I can't think of a way to use existentials to encode, for example, natural transformations on functors, while maintaining that the type "inside" the functor remains the same. Here's some code to make this idea concrete:

type Trans f g = (forall a. f a -> g a) compose :: Trans g h -> Trans f g -> Trans f h compose g2h f2g = \fa -> g2h (f2g fa)

You can represent a "lossy" transformation between functors as:

data Any f = forall a. Any (f a) type LossyTrans f g = Any f -> Any g

But then there is no way to know that the "a" held in the "Any f" matches the "a" in the "Any g".