[Haskell-cafe] ANNOUNCE: pipes-core 0.0.1
Twan van Laarhoven
twanvl at gmail.com
Sun Mar 11 21:16:46 CET 2012
On 2012-03-11 14:46, Paolo Capriotti wrote:
> On Sun, Mar 11, 2012 at 1:25 PM, Twan van Laarhoven<twanvl at 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
More information about the Haskell-Cafe
mailing list