[PRL] IOP and disjoint unions

[William D Clinger]

Felix wrote:
> > I see no more justification for requiring the terms of a
> > sum type to be subtypes of the sum type than for requiring
> > the factors of a product type to be subtypes of the product
> > type.
> 
> Of course there's no justification for that.  When you take the dual of 
> something, you have to reverse all the arrows.  (or some such category 
> theory argument.)

Touche!

Felix is quite right, of course.  Structural subtyping is sound
if the summands of a sum type are subtypes of the sum type, while
record subtyping goes the other way.  (Barring assignment to record
fields, etc.)

I was assuming a nominal type system with nominal subtyping as in
Java and most other OO languages.  Perhaps this assumption was
unjustified.

Will