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

[wren ng thornton]

On 6/21/11 6:54 PM, Casey McCann wrote:
> That said, I don't think either retains the tidy algebraic properties
> that disjoint unions and tuples have, so I'm not sure if calling them
> sums and products is actually correct.

I don't think there are any problems[1]. Categorically speaking, a product
of A and B is simply a thing, which we can call Foo[2], along with two
projections, f :: Foo -> A and oo :: Foo -> B[3], such that the Foo is the
"closest" thing to A and B[4].

I chose the funny names intentionally. Nothing in the definition of
products says that there has to be any kind of notion of order between the
components, only that the composite has projections for each component and
that it has no extra junk. Consequently A*B is isomorphic to B*A, which
means they are essentially the same thing[5]. The choice of order is just
a convention.

For a slightly stronger notion of products we can look to monoidal
categories which have that A*(B*C) is isomorphic to (A*B)*C, again meaning
that they're essentially the same thing.

Outside of category theory, we can look to domain theory (or the
associated CPO categories), but domain products and smash products both
have the same order independence as categorical products.

For coproducts, dually.


[1] modulo the A:+:A ~ A issue.
[2] More conventionally called A*B, but remember: that's just a name.
[3] More traditionally, pi_1 and pi_2, or fst and snd, or...
[4] That is, for any other Bar with b :: Bar -> A and ar :: Bar -> B,
there is a unique function from Bar to Foo such that everything commutes.
[5] The clever reader will notice that they are not *exactly* the same
thing, not identical; however, category theorists rarely care about the
differences between isomorphic things unless it's mucking up a proof.

-- 
Live well,
~wren