On 11/03/12 23:41, Chris Smith wrote:
On Sun, Mar 11, 2012 at 2:33 PM, Twan van Laarhoven
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