[PRL] IOP and disjoint unions

[William D Clinger]

Richard wrote:
> Under those circumstances, would you still regard the use of casts as
> exposing too much of the representation?

That's a moral judgement, of the sort I have been careful
not to make (so far; see below) in this discussion.

> One could argue that, with IOP's identification of interfaces and types,
> the subtyping hierarchy is an important part of the interface
> specification, so it's already exposed.

One could indeed argue that, although I believe one would
be wrong to argue that.  (That's my first moral judgement.)

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.  In particular, I note that such a requirement would
be inconsistent with Java and several similar languages,
although I readily admit this fact is all tangled up with
some obvious design bugs in those languages.  Perhaps a
concrete example of Java code will make this clearer:

// LambdaTerm = Abstraction + String + double + Application
// with predicates:  isAbs     isVar    isNum    isApp
// and conversions:  toAbs     toVar    toNum    toApp

interface LambdaTerm {

    // Predicates that report whether this term is of the queried form.
    boolean isAbs();
    boolean isVar();
    boolean isNum();
    boolean isApp();

    // Conversions from LambdaTerm to its summands.

    Abstraction toAbs () throws IllegalConversion;
    String toVar () throws IllegalConversion;       // note String
    double toNum () throws IllegalConversion;       // note double
    Application toApp () throws IllegalConversion;
}

Will