On Wed, Jun 22, 2011 at 1:25 PM, pipoca <eliyahu.ben.miney@gmail.com> wrote:

Also, I don't think that the formulation of (:|:) above is
sufficient.  Suppose:

foo :: Foo -> Bar
baz :: Baz -> Quux

foobaz :: [Foo :|: Baz]

-- map foo and baz over foobaz
barquux :: [Bar :|: Quux]
barquux = map f foobaz
how would  f be implemented?

It seems to me that you'd need an additional function:
either' :: (a -> c) -> (b -> d) -> Either a b -> Either c d


Sure, you would want to treat Either as a bifunctor.  Your either' function is usually called bimap.  So the call would look like:

map (bimap f g) foobaz

for some f and g.
 
However, it still seems to me that that isn't sufficient.  Suppose
instead:

a :: A -> B :|: C
d :: D -> E :|: F

ad :: [A :|: D]

if we want to map a and d over ad using either' to get
bcef :: [B :|: C :|: E :|: F]
it wouldn't work, we'd get
bcef :: [(B :|: C) :|: (E :|: F)]
i.e.
bcef :: [Either (Either B C) (Either E F)]
instead, which is presumably not what we wanted...
 

You need is a proof that :|: is associative.  In other words, we need to pick a "normal form" for expressions like (a :|: (b :|: c)) and ((a :|: b) :|: c) and show that they can all be normalized into the normal form.  I use a typeclass:

class Monic a b where inject :: a -> b

for that kind of work.  I always have an instance

instance Monic a a where inject = id

so I might pick to write:

instance Monic  ((a :|: b) :|: c) (a :|: (b :|: c)) where 
    inject (Left (Left a)) = Left a
    inject (Left (Right b)) = (Right (Left b))
    inject (Right c) = (Right (Right c))  

If you do that, you will soon run into two other problems I can think of (relating to MacLane's coherence conditions, which I think would be fixed by judicious composition with "inject").  

You're building up (Either a b) into a monoidal category.  There used to be a package called category-extras for this kind of stuff.  I think it has been broken up.  Does anybody know the status of its replacement(s)?