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

[wren ng thornton]

On 6/22/11 6:00 PM, Casey McCann wrote:
> On Wed, Jun 22, 2011 at 2:19 PM, wren ng thornton<wren at freegeek.org> 
wrote:
>>>> [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.
> (...)
>
> Thank you, that clarified my intuitive sense of why it didn't seem to
> work. The same argument, with arrows flipped appropriately, would
> apply to a hypothetical coproduct where A :+: A ~ A, wouldn't it?

It should. But let's make sure...

A coproduct of A and B is an object A+B along with morphisms inl :: A ->
A+B and inr :: B -> A+B, such that for any object C and morphisms c1 :: A
-> C and c2 :: B -> C, there exists a unique c1|||c2 :: A+B -> C such that
c1|||c2 . inl = c1 and c1|||c2 . inr = c2. All of this is the
straightforward dualizing of products.

So, lets assume A ~ A+A. And lets assume we have some functions inl and
inr. Now, for every pair of functions f, g :: A -> C we must come up with
a unique function h :: A+A -> C such that h . inl = f and h . inr = g. By
isomorphism this is the same as coming up with a unique function h' :: A
-> C such that h' . iso . inl = f and h' . iso . inr = g.

If inl = inr, then it follows that f = g. Consequently there can only be
one morphism between any two objects, so the category is a preorder. If
the category has all coproducts then it's a join-semilattice--- exactly
dual to the meet-semilattice case for products.

If we want a category more interesting than a preorder, then we must have
that inl and inr are different. We must find two injection functions which
keep their images in A+A apart, so that we can define partial functions
-|||g and f|||- which don't conflict with each other (so that they can be
combined into the total function f|||g). The obvious way to do that is to
use tagged/disjoint unions, but we can't do that since we've assumed A ~
A+A. Basically, the type A+A isn't big enough (whereas before, the values
of type A*A weren't big/informative enough).


I'm playing a bit fast and loose with the notion of "big/informative
enough". Perhaps someone more familiar with large ordinals can come up
with a counter example. But if they do, I'm sure it wouldn't be a very
intuitive place to program in.

-- 
Live well,
~wren