Type Relations

Types do not exist in isolation, but rather are related one to another by an algebra of binary operations that manipulate membership set theoretically in order to derive another type.

Consider the types A = {1, 2}ᵀ and B = {1, 2, 3}ᵀ. Every instance of A is also an instance of B; in other words, the membership of A is a subset of the membership of B. When this condition holds for two types A and B, then A is a subtype of B (A ⊆ B) and B is a supertype of A (B ⊇ A). If the membership sets differ, then A is a strict subtype of B (A ⊂ B) and B is a strict supertype of A (B ⊃ A). In the case that A ⊂ B, A is more specific than B, and similarly, B is more general than A; alternatively, A is stronger than B, and B is weaker than A. Every type is trivially a subtype and supertype of itself, but never strictly.

Avail’s types are organized into a singular type lattice. That is, given any two types, there exists 1) a unique type that is the most specific type more general than both and 2) a unique type that is the most general type more specific than both. The most specific type more general than two types A and B is the type union of A and B: A ∪ B. The membership of the type union is the set union of the memberships of the two input types. For example, {1, 3, 5}ᵀ ∪ {2, 4}ᵀ = {1, 2, 3, 4, 5}ᵀ. The type union operation is idempotent, A ∪ A = A; commutative, A ∪ B = B ∪ A; and associative, A ∪ (B ∪ C) = (A ∪ B) ∪ C.

The most general type more specific than two types A and B is the type intersection of A and B: A ∩ B. The membership of the type intersection is the set intersection of the memberships of the two input types. For example, {3, 4, 5}ᵀ ∩ {4, 5, 6}ᵀ = {4, 5}ᵀ. The type intersection operation is idempotent (A ∩ A = A), commutative (A ∩ B = B ∩ A), and associative (A ∩ (B ∩ C) = (A ∩ B) ∩ C). The type union and type intersection operations are connected by the absorption law A ∪ (A ∩ B) = A ∩ (A ∪ B) = A.

The type lattice is bounded by a globally most general type and a globally most specific type. The former is ⊤, and is pronounced top; the latter is ⊥, and is pronounced bottom. The membership of ⊤ includes every value, whereas the membership of ⊥ is the empty set; roughly then, ⊤ = {…}ᵀ and ⊥ = ∅ᵀ. These bounding types establish the basis for several identity laws that hold for every type A: A ∪ ⊥ = A; A ∩ ⊥ = ⊥; A ∪ ⊤ = ⊤; and A ∩ ⊤ = A.

Two types are disjoint when no instance of one is an instance of the other. The type intersection of disjoint types is always ⊥. For example, there does not exist a value which is both a negative integer and a positive integer, so the intersection of these types is ⊥: {…, -3, -2, -1}ᵀ ∩ {1, 2, 3, …}ᵀ = ∅ᵀ = ⊥.

A near subtype of ⊤ called any is treated as the most general type by many operations, but some important distinctions between the two types will be made later. Every value available to an Avail programmer is an instance of any. This type will be used frequently hereinafter, and so is introduced here.