[Haskell-cafe] ANNOUNCE: pipes-core 0.0.1
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'
> 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.
More information about the Haskell-Cafe