[Haskell-cafe] Eta-expansion and existentials (or: types destroy my laziness)

[Max Bolingbroke]

Hi Cafe,

I've run across a problem with my use of existential data types,
whereby programs using them are forced to become too strict, and I'm
looking for possible solutions to the problem.

I'm going to explain what I mean by using a literate Haskell program.
First, the preliminaries:

> {-# LANGUAGE ExistentialQuantification #-}
> import Control.Arrow (second)
> import Unsafe.Coerce

Let's start with a simple example of an existential data type:

> data Stream a = forall s. Stream s (s -> Maybe (a, s))

This is a simplified version of the type of streams from the stream
fusion paper by Coutts et al. The idea is that if you have a stream,
you have some initial state s,
which you can feed to a step function. The step function either says
"Stop! The stream has ended!", or yields an element of the stream and
an updated state.

The use of an existential quantifier is essential to this code,
because it means that we can write most functions on Streams in a
non-recursive fashion. This in turn makes them amenable to inlining
and simplification by GHC, which gives the us the loop fusion we need.

An example stream is that of natural numbers:

> nats :: Stream Int
> nats = Stream 0 (\n -> Just (n, n + 1))

Here, the state is just the next natural number to output.

We can also build the list constructors as functions on streams:

> nil :: Stream a
> nil = Stream () (const Nothing)

> cons :: a -> Stream a -> Stream a
> cons a (Stream s step) = Stream Nothing (maybe (Just (a, Just s)) (fmap (second Just) . step))

List functions can also easily be expressed:

> taken :: Int -> Stream a -> Stream a
> taken n (Stream s step) = Stream (n, s) (\(n, s) -> if n <= 0 then Nothing else maybe Nothing (\(a, s) -> Just (a, (n - 1, s))) (step s))

To see this all in action, we will need a Show instance for streams.
Note how this code implements a loop where it repeatedly steps the
stream (starting from
the initial state):

> instance Show a => Show (Stream a) where
>     showsPrec _ (Stream s step) k = '[' : go s
>       where go s = maybe (']' : k) (\(a, s) -> shows a . showString ", " $ go s) (step s)

We can now run code like this:

> test1 = do
>     print $ (nil :: Stream Int)            -- []
>     print $ cons 1 nil                     -- [1, ]
>     print $ taken 1 $ cons 1 $ cons 2 nil  -- [1, ]

Now we may wish to define infinite streams using value recursion:

> ones :: Stream Int
> ones = cons 1 ones

Unfortunately, 'ones' is just _|_! The reason is that cons is strict
in its second argument. The problem I have is that there is no way to
define cons which is
simultaneously:

  1. Lazy in the tail of the list
  2. Type safe
  3. Non-recursive

If you relax any of these constraints it becomes possible. For
example, if we don't care about using only non-recursive functions we
can get the cons we want
by taking a roundtrip through the skolemized (existiental-eliminated -
see http://okmij.org/ftp/Computation/Existentials.html) version of
streams:

> data StreamSK a = StreamSK (Maybe (a, StreamSK a))
>
> skolemize :: Stream a -> StreamSK a
> skolemize (Stream s step) = StreamSK (fmap (\(a, s') -> (a, skolemize (Stream s' step))) $ step s)
>
> unskolemize :: StreamSK a -> Stream a
> unskolemize streamsk = Stream streamsk (\(StreamSK next) -> next)
>
> instance Show a => Show (StreamSK a) where
>     showsPrec _ (StreamSK mb_next) k = maybe (']' : k) (\(a, ssk) -> shows a . showString ", " $ shows ssk k)  mb_next

Now we can define:

> cons_internally_recursive x stream = cons x (unskolemize (skolemize stream))

This works because unskolemize (skolemize stream) != _|_ even if
stream is bottom. However, this is a non-starter because GHC isn't
able to fuse together the (recursive) skolemize function with any
consumer of it (e.g. unskolemize).

In fact, to define a correct cons it would be sufficient to have some
function (eta :: Stream a -> Stream a) such that (eta s) has the same
semantics as s, except
that eta s /= _|_ for any s. I call this function eta because it
corresponds to classical eta expansion. We can define a type class for
such operations with a number
of interesting instances:

> class Eta a where
>     -- eta a /= _|_
>     eta :: a -> a
>
> instance Eta (a, b) where
>     eta ~(a, b) = (a, b)
>
> instance Eta (a -> b) where
>     eta f = \x -> f x
>
> instance Eta (StreamSK a) where
>     eta ~(StreamSK a) = StreamSK a

If we had an instance for Eta (Stream a) we could define a lazy cons function:

> cons_lazy :: a -> Stream a -> Stream a
> cons_lazy x stream = cons x (eta stream)

As we have already seen, one candidate instance is that where eta =
unskolemize . skolemize, but I've already ruled that possibility out.
Given that constraint, the
only option that I see is this:

> instance Eta (Stream a) where
>     -- Doesn't type check, even though it "can't go wrong":
>     --eta stream = Stream (case stream of Stream s _ -> s) (case stream of Stream _ step -> step)
>     eta stream = Stream (case stream of Stream s _ -> unsafeCoerce s :: ()) (case stream of Stream _ step -> unsafeCoerce step)

I've had to use unsafeCoerce to make this go through, because I can't
see any type-correct way of defining eta-expansion of existential data
types - and indeed GHC
complains if you try to use the ~pattern notation to define it.
Nonetheless, it is "obvious" that 'eta' can't actually go wrong (in
Milners's sense of the term).

Now we can define the infinite stream we originally wanted:

> lazy_ones :: Stream Int
> lazy_ones = cons_lazy 1 lazy_ones
>
> test2 = print $ taken 2 $ lazy_ones -- [1, 1, ]

Finally, here is some code to actually run the tests:

> main = do
>     test1
>     test2

So, cafe: is there any way to define a cons that satisfies my three
earlier conditions:

  1. Lazy in the tail of the list
  2. Type safe
  3. Non-recursive

Or am I going to have to stick with my slightly unsafe eta that uses
unsafeCoerce?

Cheers,
Max