74 Comparable Types

Definition (disjoint):
Types A and B are disjoint if they are comparable and their carrier sets are disjoint.

Definition (incomparable):
Types A and B are incomparable if equality between them is undefined and any attempt to compare them, implicitly or explicitly, produces a type error.

Definition (comparable):
Two types A and B are comparable iff they share a unique least common supertype T with defined equality. If multiple candidate supertypes exist and none is a subtype of the others, A and B are incomparable.

In the following example, types B and C have a unique least common supertype A, but A is abstract and therefore does not define equality. B and C also have a non-empty common subtype D. Nevertheless, B and C are incomparable. This is based on static typing: attempting to compare expressions of static types B and C produces a type error, even if the expressions denote values lying in the common subtype D.

abstract value A {};
value B { Integer x; };
value C { Integer x; };
value D { Integer x; };
B,C isa A;
// D isa B,C;
B(D:d) { x = d.x; }
C(D:d) { x = d.x; }
var b = B { x=1 };
var c = C { x=1 };
print b = c;        // type error:  B and C are incomparable

Declaring disjointness for B and C, and naming their union type, records that their carrier sets do not overlap. This makes cross-member equality available as false:

value B { Integer x; };
value C { Integer x; };
disjoint B, C;
type A = union { B, C };
var b = B { x=1 };
var c = C { x=1 };
print b = c;        // prints false

Naming the same union type multiple times does not create distinct supertypes.

value B { Integer x; };
value C { Integer x; };
disjoint B, C;
type A1 = union { B, C };
type A2 = union { B, C };
var b = B { x=1 };
var c = C { x=1 };
print b = c;        // prints false