To: dylan-partners@cambridge.apple.com
Subject: union types & exhaustive unions
fcc: out-copy
--------

Design note 7 says:
   union(T1, T2) = T3 when T1 and T2 form an exhaustive partition of T3,
   for example, union(<integer>, <ratio>) = <rational>

This does seem plausible, at least in the case of this example, and it
might even be in there because I suggested it "ought to work" (in a strict
extensional view of types.)  But it isn't so clear what this means when
classes can be added at run-time.

One issue is defining when a type is "exhaustively partitioned"; my
intuitive extensional definition is:
    There can be no generalized instance of T3 when is not also a
    generalized instance of either T1 or T2.

Note that this definition can only be true when T3 is an abstract class,
since otherwise one could always do make(<T3>), which would not be of
either subtype.

Even with abstract class, there is a problem with determining whether all
direct subclasses are enumerated, since classes could be added at run-time.