[PRL] IOP and disjoint unions

[Richard Cobbe]

On Thu, Apr 28, 2005 at 07:27:38PM -0400, William D Clinger wrote:
> 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.

Well, Honu certainly uses nominal subtyping, so that's most relevant to
my current research project.  That said, I don't want to limit the
discussion solely to that; I'd be interested in hearing about
these design issues in the context of other languages as well.

And you're right, Will, in that there's no intrinsic reason why the
summands should be subtypes of the sum type.  It is, however, often more
convenient when that is the case.  Returning to the running example, the
Application class is likely to have two fields (assuming the object
language has only unary functions), which are most likely going to have
type LambdaTerm.  Without this subtyping relationship, you have to write
the injections as well as the projections.  As the number of variants
(or sum types, for that matter) increases, that can be a lot of really
annoying code to write.

I haven't actually done that much coding in a setting that requires the
level of data abstraction that Will describes, so I'm not in a position
to evaluate the convenience/maintainability tradeoffs more fully.

Richard