[PRL] IOP and disjoint unions

[Mitchell Wand]

WDC> Mitch wrote:
>> Obviously I've been thinking in category theory too long. There a sum
>> type can always be represented by its polymorphic _case_ function:
>> 
>> A+B ~=~ (all C)([A->C]x[B->C])

WDC> Obviously A+A is not equivalent to A in category theory.

WDC> If you try to use OO inheritance and nominal subtyping to model
WDC> sum types, however, then you're liable to end up with A+A being
WDC> indistinguishable from A.

Erm, when I wrote +, I meant "disjoint sum" (aka "coproduct"), which is I
think what you all meant by it also.

--Mitch