70 Necessarily disjoint and non-disjoint

Predica distinguishes nominal and structural types. Structural types are identified by their ordered sequence of attribute declarations; nominal types are identified by their declaration. The rules for necessary overlap and necessary disjointness formalise this distinction.

Predica uses the word necessary in a technical sense. When we say that two types necessarily overlap or are necessarily disjoint, the term necessary acts as a modal operator: the stated relationship holds in all interpretations consistent with the type graph and the intrinsic rules of the language. Necessary overlap is the smallest relation closed upward under supertyping, and necessary disjointness is the smallest relation closed downward under subtyping. This duality reflects the underlying semantics: overlap is an existential property that propagates to supertypes, while disjointness is a universal property that propagates to subtypes. The compiler uses these modal closures to determine when a disjointness declaration is permissible and when a common subtype is forbidden.

Formally:

  • Overlap is a relation on types: overlap(A,B).
  • Necessary overlap is the modal lifting: ☐overlap(A,B).
  • Disjointness is a relation: disjoint(A,B).
  • Necessary disjointness is: ☐disjoint(A,B).

The modal operator □ (“necessarily”) means: True in all models consistent with the type graph and intrinsic rules. In other words:

  • Necessary overlap = overlap in every model the compiler cannot rule out.
  • Necessary disjointness = disjointness in every model the compiler cannot rule out.

This is why:

  • Overlap propagates upward (monotone in supertypes).
  • Disjointness propagates downward (monotone in subtypes).

These are exactly the modal closure rules.

Necessary overlap

Two types necessarily overlap if:

  • They are the same type.
  • They are supertypes of types that necessarily overlap.
  • They have a declared non-empty common subtype.
  • One is a known subtype of the other, such as Integer and Real, or a componentwise structural subtype.

Necessary disjointness

Two types are necessarily disjoint if:

  • They belong to different intrinsic disjoint families. The predefined families are Boolean, String, and the Real family, where the Real family includes Integer, the fixed-width integer types, finite floating-point types, UnicodeCodePoint, and UnicodeScalar through intrinsic subtyping.
  • They are structural types whose ordered attribute-name sequences differ.
  • They are structural types with the same ordered attribute names, and some corresponding attribute declarations cannot be satisfied by any common finite set. For example, their cardinality ranges may be disjoint, or their attribute types may be necessarily disjoint while every common cardinality requires at least one value.
  • They are subtypes of types which are necessarily disjoint.
  • One of the types is the empty type Null.
  • They appear together in a declared disjointness declaration.

It is an error to declare a non-empty common subtype of two types which are necessarily disjoint.