On Wed, Jun 22, 2011 at 1:25 PM, pipoca 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)?

On Wed, Jun 22, 2011 at 1:25 PM, pipoca wrote:

Is there any reason why we don't have either anonymous disjoint union types, or why some of the proposals here (e.g. type (:|:) a b = Either a b ) haven't been implemented, or put into the standard libraries (and publicised in beginner texts)?

I know that {-# LANGUAGE TypeOperators #-} has been in GHC for a while, but I'm not sure how widely accepted among other Haskell implementations it is. It seems to me that you'd need an additional function:

either' :: (a -> c) -> (b -> d) -> Either a b -> Either c d

import Control.Arrow (+++, |||) The '+++' operator from ArrowChoice already does what you need here. And the '|||' operator is a more generic form of the '???' operator I mentioned earlier.

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)] instead, which is presumably not what we wanted...

Actually, we do want [(B :|: C) :|: (E :|: F)] in this case. It's important for generic programming. However, these types are associative, so we could develop a standard set of re-association operators.