The Avail Programming Language
Mobile Users: Click here to view our text rendering warning.


A type is a classification of values by conceptual similarity. In practice, this demarcation occurs along operational boundaries. It is meaningful to compute the sum, difference, or product of any two integers, so it stands to reason that 1) there exists some type whose instances support all three operations (addition, subtraction, and multiplication) and 2) at least some instances of this type are integers. As a general rule, the instances of a type should support the same operations, albeit providing potentially different results; for example, each pairwise permutation of 3, 5, 7, and 9 supports addition, and 5 + 7 and 3 + 9 yield equal values while 3 + 5 and 7 + 9 yield different values.

There may be circumstances, however, where some combination of instances of a common type are not valid for a particular operation. Such a combination of instances is a singularity. Consider the case of division. Though 0 is always an acceptable numerator, it can never serve as the denominator. It is still fair to say that the type whose instances are integers supports the four basic arithmetic operations even though division exhibits singularity whenever 0 is the denominator.

Curly brackets ({}) enclosing a comma-separated list and ultimately followed by a superscript T denote a type as an enumeration of its instances; in this context, a leading horizontal ellipsis () within the curly brackets indicates an infinite leading progression and a trailing horizontal ellipsis indicates an infinite trailing progression. Conceptually then, a type is analogous to a set of values whose members are its instances. For example, {1, 2, 3}ᵀ denotes the type whose instances are the integers 1, 2, and 3; {…, -3, -2, -1}ᵀ denotes the type whose instances are the negative integers; {1, 2, 3, …}ᵀ denotes the type whose instances are the positive integers; and {…, -1, 0, 1, …}ᵀ denotes the type whose instances are the integers. The element-of operator (U+2208) indicates that a value is an instance of a type; for example, 3 ∈ {1, 3, 5}ᵀ.

There is no requirement that a value belong to only one type. In fact, every value belongs to infinitely many types, the most specific of which has that value as its only instance. The most specific type of the integer 5 then is 5's type{5}ᵀ. This is the instance type. Additionally, any number of types may include some value as an instance. The fact of 5's membership in {5}ᵀ does not preclude its membership in {1, 5, 9}ᵀ, {1, 2, 3, …}ᵀ, or {…, -1, 0, 1, …}ᵀ. There is also no requirement that a type comprise only values considered to have a natural affinity. Though the examples have focused on integers thus far, this is for brevity only. {5, ∅, "rhododendron", [Print: "Howdy!\n";]}ᵀ is a perfectly valid type, though perhaps not obviously a useful one.

‹ Values | Return to Type System | Type Relations ›