69 Type graph

Type graph

The types form a type graph under the subtype as subset relationship.

Definition: (subtype): Type A is a subtype of B if A ⊆ B.

Note that every type is a subtype of itself.

The predefined types include intrinsic subtype edges. For example, Integer and the fixed-width integer types are subtypes of Real, and UnicodeScalar is a subtype of UnicodeCodePoint, which is a subtype of Integer.

Structural subtyping

Structural subtyping is componentwise. A structural type { S1 a1 q1; ...; Sk ak qk; } is a subtype of { T1 a1 r1; ...; Tk ak rk; } when the attribute names occur in the same order, each Si is a subtype of the corresponding Ti, and each cardinality range qi is contained in the corresponding range ri.

For example, { Integer x; } is a subtype of { Real x; }, and { Integer x?; } is a subtype of { Real x*; }.

Structural types whose ordered attribute-name sequences differ are necessarily disjoint. For example, { Integer x; String y; } and { String y; Integer x; } are distinct structural types because the attribute order differs.

The following illustrate the six possible ways of establishing a subtype relationship between two types:


// 1) Declare concrete type A to be a subtype of an abstract type B as A is declared
value A isa B { ... };

// 2) Declare existing concrete type A to be a subtype of an existing abstract type B
A isa B;

// 3) Embed existing type A in existing type B, so that A ⊆ B
embed A a isa B = expressionOfTypeB;

// 4) Create new subtype A as an intersection of existing comparable types B and C
type A = intersection { B, C };

// 5) Define a supertype A of existing types B and C
type A = union { B, C };

// 6) Name the subtype of B satisfying a predicate
type A = subtype B where p(this);

Only the nominal declarations create a fresh carrier set. subtype T where p refinements, intersections, and unions name or transform existing carrier sets. A subtype T where p expression denotes the subset of its base type satisfying its predicate.

A disjointness declaration such as disjoint B, C; also records a type-graph fact, but it does not establish a subtype relationship between B and C.

Type aliases do not add graph facts

A declaration such as:


type A = subtype B where p(this);

binds the name A to the refinement type expression subtype B where p(this). It does not introduce a nominal type, a fresh carrier set, or an additional semantic fact in the type graph. In particular, the declaration does not assert that A is inhabited, and the mere existence of the name A must not be used as evidence that other types necessarily overlap. The subtype relationship A ⊆ B follows from the meaning of the refinement expression, not from an added graph edge.

Refinement equivalence is extensional

Given declarations of the form:


type A1 = subtype B where p1(x);
type A2 = subtype B where p2(x);

the compiler cannot, in general, determine whether the predicates p1 and p2 define the same subset of B. Establishing extensional equality between arbitrary predicates would require solving the predicate-equivalence problem, which is undecidable in the general case. Therefore, an implementation is not required to prove that two refinement predicates define the same subset. Two refinement type expressions are automatically equal when their base type expressions are equal and their normalised predicate forms are identical. Otherwise, the implementation must not infer equality between them unless the programmer explicitly establishes equivalence.

Nominal declarations such as value and entity create fresh carrier sets. A subtype B where p expression does not create new values; it denotes a subset of an existing base type. The name introduced by type A1 = ... is an alias for that type expression, not a nominal type.

Do we need static types which understand intersection of types?

Consider:


value A {Integer x};

type B = subtype A where p1(x);
type C = subtype A where p2(x);

void foo(b*:B) 
{ 
    print b;
}

var B b* = { A { x = 1 }, A { x = 2 } };
var C c* = { A { x = 2 }, A { x = 3 } };

foo(b ∩ c);     // type error if static type of b ∩ c is A

When two values of refined types are combined using set-theoretic operations such as intersection, the static type of the result is the intersection of the operand types. For refined types, this corresponds to conjoining their predicates. The compiler must therefore support intersection types internally, even if they are not exposed as a surface-level type expression form.

Naming a refinement must not change the static meaning of set operations. For example, if type B = subtype A where p1(x); and type C = subtype A where p2(x);, then an intersection may have the refined type subtype A where p1(x) ∧ p2(x). A union of values of type B and C does not acquire a special named union type merely because B and C have names; its principal type is determined from the denoted type expressions. Likewise, a value-level difference operation does not generally infer a complement refinement such as subtype A where ¬p1(x), because subtracting one value does not prove that all values satisfying p1 have been removed.

In effect there is a (conjunctive) set of static types for any value-expression.

Every expression has a set of static types that is closed under intersection and subtyping. The compiler reports a principal type, which is the greatest lower bound (meet) of all types known to apply. For refined types, this corresponds to conjoining all predicates known to hold for the expression.

There is no need for a disjunctive set of static types because the union of two sets already requires existence of a unique least common supertype with defined equality.

For a union expression e1 ∪ e2 to be to be well-typed, the static types T1 of e1 and T2 of e2 must be comparable, meaning they share a unique least common supertype U, and equality is defined at U. This ensures e1 ∪ e2 has a single static type U. There is no ambiguity for equality when computing e1 ∪ e2, and no need to track either T1 or T2. So there is no need for a disjunctive set of static types to represent the static type of e1 ∪ e2.

The idea that an expression inhabits many static types simultaneously, closed under intersection and subtyping, appears in the literature in:

Refinement type systems (Freeman & Pfenning 1991)
Intersection type systems (Coppo–Dezani lineage)
Flow-sensitive type systems (e.g., occurrence typing)
Liquid types (Vazou et al.)
Algebraic subtyping (Ostermann et al.)

The source type expression for explicit type intersections is intersection { T1, T2 }. It denotes the semantic intersection of the two types. This form is purely extensional and corresponds to conjoining refinement predicates when both operands are refined types. A type declaration may bind a name to the intersection expression, but it does not introduce new type identity.


value Rectangle
{ 
    Real width;
    Real height;
}

value Rhombus
{ 
    Real side;
    Real θ;
}

// Error: Rectangle and Rhombus are incomparable
type Square = intersection { Rectangle, Rhombus };

var a* = SomeRectangles();
var b* = SomeRhombuses();

// Error: need unique least common supertype of Rectangle and Rhombus with defined equality
var c* = a.Σ ∩ b.Σ;

The type hierarchy

Together, these forms of subtyping allow types to be organised into a semantic hierarchy. Abstract types define shared predicates, concrete types introduce structure, constrained subtypes refine domains, and intersection subtypes capture overlapping classifications. This provides a unified foundation for open variants, domain refinement, and compositional modelling.

PreviousPart VI: Subtypes Next70 Necessarily disjoint and non-disjoint