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