On Sun, Mar 11, 2012 at 1:25 PM, Twan van Laarhoven
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