On 12-03-11 09:09 AM, Paolo Capriotti wrote:
The Category law would be broken, though:
unawait x>>> id == yield x !== unawait x
How did you get this equation? It's not even well-typed:
unawait :: a -> Pipe a b m ()
yield :: b -> Pipe a b m ()
You're right, it's completely wrong. I was confused last night.
Someone actually implemented a variation of Pipes with unawait:
https://github.com/duairc/pipes/blob/master/src/Control/Pipe/Common.hs
(it's called 'unuse' there).
I actually agree that it might break associativity or identity, but I
don't have a counterexample in mind yet.
It's difficult to say without having the implementation of both
unawait and all the combinators in one package. I'll assume the
following equations hold:
unawait x >> await = return x
unawait x >> yield y = yield y >> unawait x
(p1 >> unawait x) >>> p2 = (p1 >>> p2) <* unawait x -- this
one tripped me up
first (unawait (x, y)) = unawait x
The first two equations would let us move all the unawaits that are
not immediately re-awaited to the end of their monadic pipeline stage:
the unawait can always be performed as the last operation in bulk. The
third equation let allows us to move these unawaits to the end of the
pipeline.
If these equations hold, unawait now appears to be law-abiding to
me. I apologize for my unsubstantiated smears.
The 'unuse' implementation you linked to drops the unmatched Unuse
suspensions, so it doesn't follow the third equation.
go i True u (Free (Unuse a d)) = go i True u d
go True o (Free (Unuse a u)) d@(Free (Await _)) = go True o u d
I think this implemanteation does break the Category law, but I'm
having trouble testing it in GHCi.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
