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

9 Nov 2008

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

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

Ryan Ingram