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

[oleg at okmij.org]

Max Bolingbroke wrote:
> Let's start with a simple example of an existential data type:
> > data Stream a = forall s. Stream s (s -> Maybe (a, s))
> > 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

Really? Here are two 'cons' that seem to satisfy all the criteria

> {-# LANGUAGE ExistentialQuantification #-}
>
> data Stream a = forall s. Stream s (s -> Maybe (a, s))
>
> nil :: Stream a
> nil = Stream () (const Nothing)
>
> -- One version
> -- cons :: a -> Stream a -> Stream a
> -- cons a str = Stream Nothing (maybe (Just (a, Just str)) run)
> --  where run (Stream s step) = 
> --         step s >>= (\ (a,s) -> return (a, Just (Stream s step)))
>
> -- the second version
> cons :: a -> Stream a -> Stream a
> cons a str = Stream (Just (a,str)) step
>  where step Nothing = Nothing
>        step (Just (a, (Stream s step'))) = Just (a,
>            case step' s of
>              Nothing      -> Nothing
>              Just (a',s') -> Just (a',(Stream s' step')))
>
>
> 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)
>
> 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))
>
> ones :: Stream Int
> ones = cons 1 ones
>
> test2 = taken 5 $ ones
> -- [1, 1, 1, 1, 1, ]

	Finally, if one doesn't like existentials, one can try
universals:
	http://okmij.org/ftp/Algorithms.html#zip-folds
	http://okmij.org/ftp/Haskell/zip-folds.lhs

The code implements the whole list library, including zip and
zipWith. None of the list operations use value recursion. We still can
use value recursion to define infinite streams, which are processed
lazily. In fact, the sample stream2 of the example is the infinite
stream.