On 2012-03-11 14:46, Paolo Capriotti wrote:
On Sun, Mar 11, 2012 at 1:25 PM, Twan van Laarhoven<twa...@gmail.com> wrote:
I would expect that
(id>>> unawait x)>>> await !== unawait x>>> await === return x
There are several type errors in this equation, so I'm not exactly
sure what you mean. If you intended to write something like:
(id>>> (unawait x>> return y))>>> await
!==
(unawait x>> return y)>>> await
then I disagree, because both sides should evaluate to 'return y'. I'm
not sure why you would expect x to be returned, since there is no
'await' after 'unawait' in the middle pipe.
Oops, I got confused by (>>) and (>>>). The intended semantics of unawait is
unawait x >> await === return x
So what I was trying to write is
(id >+> unawait x) >> await
=== {by identity law}
unawait x >> await
=== {by behavior of unawait}
return x
But that this is impossible to implement, and instead what you get is
(id >+> unawait x) >> await === return () >> await === await
because in the general case of
(p >>> unawait x)
if is impossible to transform the unawaited value out of the composition.
Why? The natual definition would be:
p >+> (unawait x >> p') == (yield x >> p) >+> p'
Right, but then take p==id, which gives
(id >+> (unawait x >> return ())) >> p'
===
((yield x >> id) >+> return ()) >> p'
===
return () >> p'
===
p'
So the unawait is not seen by p', whereas the identity law would give
(id >+> (unawait x >> return ())) >> p'
===
(unawait x >> return ()) >> p'
===
unawait x >> p'
I would like to get this latter semantics, and if the left side is id, it is
fine. However, in
(p :: Pipe a b r) >+> (unawait x >> q :: Pipe b c r) :: Pipe a c r
x has type b. You can not write this in a form like
unawait x' >> q :: Pipe a c r
because here x' would have type a. But if p == id, this is exactly what you
would like to get.
I'm extremely wary of this sort of reasoning, because failure of
invariants in simple situations are a symptom of something being
conceptually wrong in the abstraction.
Or perhaps we should be satisfied when Pipe is a Semigroupoid?
I don't think so, since we can always add formal identities. Usually,
though, failure of the identity law implies failure of associativity,
by just putting the "failing identity" in the middle of a composition.
A simple way to implement unawait that fails the identity law is by discarding
left-over unawaits inside a vertical composition. I.e.
unawait x >+> p === return () >+> p
q >+> unawait y === q >+> return ()
As long as you do this consistently for *all* vertical compositions, I don't see
how associativity is broken.
In the first case, with unawait on the left, you don't need to discard the
await. But I think it is probably more consistent if you do.
Anway, 'purePipe id' is now a failing identity, in the sense that composing with
it discards trailing awaits from the other thing composed with.
Twan
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
