Metatypes

In Avail, types are also values. Types are not simply the province of the compiler, and do not just occur as scaffolding in the source code of a program. Rather, they may also flow through a running program as values. A rich set of operations is provided for the purpose of navigating the type lattice, interrogating the relationships between types, and deriving types from values.

Given that every value is an instance of some number of types, and that types themselves are also values, types are therefore instances of other types. These other types are metatypes: types whose instances are also types. Each type has its own most specific metatype. For example, 5's type's type ≝ {{5}ᵀ}ᵀ. A value may be recursively interrogated for its type ad infinitum, and every step of this interrogation produces a value that is distinct from those produced by previous (or subsequent) steps. So 5's type, 5's type's type, 5's type's type's type, … are all distinct types:

The integer 5 is the sole instance of {5}ᵀ. It is also an instance of {…, -1, 0, 1, …}ᵀ, of which {5}ᵀ is a subtype. So what is the relationship between {{…, -1, 0, 1, …}ᵀ}ᵀ and {{5}ᵀ}ᵀ? In the design of a type system, there are many logically consistent answers to this question, but not all answers have equal utility. In Avail, a simple rule universally answers questions of this form: given two types A and B, if A is a subtype of B, then A's type is a subtype of B's type: ∀A,B ∈ type: A ⊆ B → {A}ᵀ ⊆ {B}ᵀ. This is the law of metacovariance.