Re: [Haskell-cafe] Why aren't there anonymous sum types in Haskell?

On 6/21/11 10:48 PM, Casey McCann wrote:

On Tue, Jun 21, 2011 at 9:51 PM, wren ng thornton wrote:

...

I don't think there are any problems[1]. (...) [1] modulo the A:+:A ~ A issue.

Oops, I should've said A:*:A there.

That issue is exactly my concern, though, and it seems a bit too thorny to handwave aside.

Indeed. If we have A:*:A ~ A, then A:*:A is not a categorical product. The reasoning is as follows. An object A*B with morphisms fst :: A*B->A and snd :: A*B->B is a product iff for all objects P with morphisms p1 :: P -> A and p2 :: P -> B, there is a unique morphism p1&&&p2 :: P -> A*B, such that p1 = fst . p1&&&p2 and p2 = snd . p1&&&p2. Given the definition, if we further say that A*A ~ A, then it's clear that we can't come up with any satisfactory definitions of fst and snd which obey the laws--- unless there can be only one morphism between any two objects, in which case we know that p1 = p2 and so it's okay for fst = snd; or unless there can be only two morphisms between any two objects and we have a canonical property for distinguishing them so that we can correlate p1 with fst and p2 with snd. In all other cases, there are simply too many possible choices of p1 and p2, and there's no way for fst and snd to carry enough information to make the equations hold. What that means then is that the category which tries to use :*: to make products would only have products in the cases where the first and second component are different; which would be a strange category indeed. Alternatively, it could always have products but would only allow one morphism between objects; in which case the category is just a meet-semilattice (actually, the preorder generalization thereof).

In contrast, ordered pairs and disjoint unions are tidy, simple, and obvious.

Disjoint pairs are sufficient; they needn't be ordered. All we need is that they are "tagged" in the same way that disjoint unions are, so that we can distinguish the components of A*A. -- Live well, ~wren