[Haskell-cafe] ANNOUNCE: pipes-core 0.0.1

[Twan van Laarhoven]

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