
On Sun, Mar 11, 2012 at 10:41 PM, Chris Smith
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).
I completely agree with this. For the subset consisting of pipes that never terminate (basically stream processors), it might be possible to add 'unawait'. However, the example (idP >+> unawait x) >> await shows that it's impossible to implement on general pipes without changing the Pipe type in some deeper way. ChunkPipe can be somewhat awkward to use because of the newtype wrapping/unwrapping, but from my experience, there's no need to use it very much in practice. What you can usually do is insert a 'regularize' Pipe (using ChunkPipe) early in the pipeline which splits chunks that cross "logical boundaries", so that the rest of the pipeline can deal with chunked input without worrying about leftovers. BR, Paolo