Re: [Haskell-cafe] ANNOUNCE: pipes-core 0.0.1

11 Mar 2012

      On 2012-03-11 14:46, Paolo Capriotti wrote:
...
On Sun, Mar 11, 2012 at 1:25 PM, Twan van Laarhoven  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