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

[Roman Leshchinskiy]

On 16/10/2010, at 12:00, Max Bolingbroke wrote:

> 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))
> 
> [...]
> 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.

That's easy.

eta :: Stream a -> Stream a
eta s = Stream s next
   where
     next (Stream s next') = case next' s of
                               Just (x,s') -> Just (x,Stream s' next')
                               Nothing     -> Nothing

Making GHC optimise stream code involving eta properly is hard :-)

Roman