On 11/03/12 23:41, Chris Smith wrote:
On Sun, Mar 11, 2012 at 2:33 PM, Twan van Laarhoven<twa...@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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
