[PRL] IOP and disjoint unions

[William D Clinger]

Richard wrote:
> 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.

Consider what happens when two or more summands are the same type.
(If you're going to allow two or more factors of a product type to
be the same type (e.g. tuples or records), then why not allow two
or more summands to be the same type?)

> 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.

Returning to the running example, let's add selection notation
(e.g. x.f) to the sum type:

LambdaTerm = (LambdaTerm x LambdaTerm)        // Application
           + String
           + double
           + (String x LambdaTerm)            // Abstraction
           + (LambdaTerm x LambdaTerm)        // Selection

Is this really going to save you from writing a lot of code?

Will