75 Union types

A union type expression denotes the union of the carrier sets of its member types:

type Contact = union { EmailContact, PhoneContact };
type VisibleContact = subtype (union { EmailContact, PhoneContact }) where visible;

The syntax for union types is deliberately parallel to the syntax for intersection types:

type Contact = union { EmailContact, PhoneContact };
type ShapeTexture = intersection { Shape, Texture };

Both forms are recursive type expressions. A union may appear anywhere a type expression is accepted: in a type alias, an attribute declaration, a generic argument, a refinement base, or as a member of another union or intersection expression.

Union syntax does not assert disjointness

The declaration:

type A = union { B, C };

does not assert that B and C are disjoint. It only names the type whose carrier is the union of the carriers of B and C.

Pairwise disjointness is a separate type-graph fact. It can be declared directly when intended:

disjoint B, C;
type A = union { B, C };

The disjointness declaration is rejected if it contradicts facts already known to the type graph. For example, two types with a known non-empty common subtype cannot also be declared disjoint.

value B { Integer x; };
value C { Integer x; };
value D { Integer x; };

B(D d) { x = d.x; }
C(D d) { x = d.x; }

disjoint B, C;        // Error: B and C have a common subtype.

Likewise, intrinsic and structural rules may already imply that two types necessarily overlap, or that they are necessarily disjoint. The union expression itself does not add either fact.

Equality is a separate concern

For equality to be available on a union type, equality must be defined for all relevant member pairs. Those definitions are not part of the union type-expression syntax. They are declared separately, as described in the chapter on equality between types.

This keeps the syntax of union { ... } simple and recursive. The parser recognises the union type expression without also parsing equality definitions, and the type checker later verifies that the equality operations needed by a particular use are available.

Union is non-nominal

Union types are non-nominal: the identity of a union type is determined solely by its member types. Therefore:

type A1 = union { B, C };
type A2 = union { B, C };

means A1 and A2 are aliases of the same union type, equivalent to:

type A1 = union { B, C };
type A2 = A1;