Paolo Capriotti p.capriotti at gmail.com
Sun Mar 11 14:46:52 CET 2012

```On Sun, Mar 11, 2012 at 1:25 PM, Twan van Laarhoven <twanvl at gmail.com> wrote:
> On 2012-03-11 14:09, 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 ()
>
>
> 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.

> 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'

To
> do that you would need the inverse of p. You can get around this by having a
> special constructor for the identity. But then
>
>    id !== arr id
>
> IMO, neither of these failed laws would be a big problem in practice, since
> no one will actually use identity pipes in combination with unawait.

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.

BR,
Paolo

```