[Haskell-cafe] ANNOUNCE: pipes-core 0.0.1

[Twan van Laarhoven]

On 11/03/12 23:41, Chris Smith wrote:
> On Sun, Mar 11, 2012 at 2:33 PM, Twan van Laarhoven<twanvl at gmail.com>  wrote:
>> I think you should instead move unwaits in and out of the composition on the
>> left side:
>>
>>     unawait x>>  (p1>+>  p2) === (unawait x>>  p1)>+>  p2
>>
>> This makes idP a left-identity for (>+>), but not a right-identity, since
>> you can't move unawaits in and out of p2.
>
> Not sure how we got to the point of debating which of the category
> laws pipes should break... messy business there.  I'm going to be in
> favor of not breaking the laws at all.  The problem here is that
> composition of chunked pipes requires agreement on the chunk type,
> which gives the type-level guarantees you need that all chunked pipes
> in a horizontal composition (by which I mean composition in the
> category... I think you were calling that vertical?  no matter...)
> share the same chunk type.  Paolo's pipes-extra does this by inventing
> a newtype for chunked pipes, in which the input type appears in the
> result as well.  There are probably some details to quibble with, but
> I think the idea there is correct.  I don't like this idea of
> implicitly just throwing away perfectly good data because the types
> are wrong.  It shows up in the category-theoretic properties of the
> package as a result, but it also shows up in the fact that you're
> *throwing* *away* perfectly good data just because the type system
> doesn't give you a place to put it!  What's become obvious from this
> is that a (ChunkedPipe a b m r) can NOT be modelled correctly as a
> (Pipe a b m r).

Agreed. There are many things to be said for making sure that Pipe is a 
real category. I suppose the morally correct thing to do is, as you 
said, have a separate ChunkedPipe type. That would make the type system 
guarantee that there are no calls to 'unawait' in the second part of a 
categorical composition.

The API could even look something like this:

     data Chunk
     data NoChunk
     data Pipe chunkiness a b m r

     await :: Pipe anyChunk a b m a
     yield :: b -> Pipe anyChunk a b m ()
     unawait :: a -> Pipe Chunk a b m ()

     runChunkedPipe :: Pipe Chunk a b m r -> Pipe NoChunk a b m r

     -- composition in the category
     (>+>) :: Pipe NoChunk a b m r -> Pipe NoChunk b c m r
           -> Pipe NoChunk a c m r

The following generalization of category composition is still fine:

     compose :: Pipe anyChunk a b m r -> Pipe NoChunk b c m r
             -> Pipe anyChunk a c m r

But this would not be:

     almostEntirelyNotUnlikeCompose :: Pipe anyChunk a b m r
          -> Pipe discardChunksHere b c m r -> Pipe anyChunk a c m r


By the way, a ChunkedPipe can be implemented not only as
     type ChunkedPipe a b m r = StateT [a] (Pipe a b m) r
but also as
     type ChunkedPipe a b m r = CodensityT (Pipe a b m) r
by using the 'feed' function to implement unawait.


Twan