[PRL] IOP and disjoint unions

[William D Clinger]

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])

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

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

Will