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

[wren ng thornton]

On 6/21/11 10:48 PM, Casey McCann wrote:
> On Tue, Jun 21, 2011 at 9:51 PM, wren ng thornton<wren at freegeek.org> 
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