## 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.

‹ Types | | | Return to Type System | | | Type Compatibility › |