[PRL] IOP and disjoint unions

[Felix S Klock]

On Apr 28, 2005, at 6:37 PM, William D Clinger 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.)

Now, what about requiring that the factors of a product type be 
*super*-types of the product type?

(To be fair, I do believe such a requirement is questionable as well; 
records make this much easier to swallow, and since we are dealing with 
tagged-sums here, perhaps records are the appropriate dual to 
consider.)

-Felix, who knows that he has at least one better thing to be doing 
than replying to PRL.

----
"graph coloring is not cool"  -josh