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

[Ryan Ingram]

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".