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

type ≝ {⊤}ᵀ

An overview of the Avail's metatypes. any any ⊤--any nontype nontype any--nontype type type = {⊤}ᵀ any--type nontype--⊥ any meta {any}ᵀ type--any meta meta {type}ᵀ = {{⊤}ᵀ}ᵀ any meta--meta nontype meta {nontype}ᵀ any meta--nontype meta atom meta {atom}ᵀ ⊥ meta {⊥}ᵀ atom meta--⊥ meta character meta {character}ᵀ character meta--⊥ meta continuation meta {continuation}ᵀ continuation meta--⊥ meta fiber meta {fiber}ᵀ fiber meta--⊥ meta function meta {function}ᵀ function meta--⊥ meta function implementation meta {function implementation}ᵀ function implementation meta--⊥ meta map meta {map}ᵀ map meta--⊥ meta meta--⊥ meta method meta {method}ᵀ method meta--⊥ meta method definition meta {method definition}ᵀ method definition meta--⊥ meta module meta {module}ᵀ module meta--⊥ meta number meta {number}ᵀ object meta {object}ᵀ object meta--⊥ meta nontype meta--atom meta nontype meta--character meta nontype meta--continuation meta nontype meta--fiber meta nontype meta--function meta nontype meta--function implementation meta nontype meta--map meta nontype meta--method meta nontype meta--method definition meta nontype meta--module meta nontype meta--number meta nontype meta--object meta phrase meta {phrase}ᵀ nontype meta--phrase meta pojo meta {pojo}ᵀ nontype meta--pojo meta token meta {token}ᵀ nontype meta--token meta tuple meta {tuple}ᵀ nontype meta--tuple meta set meta {set}ᵀ nontype meta--set meta variable meta {variable}ᵀ nontype meta--variable meta phrase meta--⊥ meta pojo meta--⊥ meta token meta--⊥ meta set meta--⊥ meta variable meta--⊥ meta ⊥ meta--⊥

Since is the most general type, then, by the law of metacovariance, {⊤}ᵀ is the most general metatype. This type is usually referred to as type in Avail code. Every type is an instance of type and every metatype is a subtype of type. It is a sibling of nontype, and every value is either an instance of nontype or type.

Consider , any, and nontype. None of these are subtypes of type. In fact, the first two are supertypes of type and the third is a sibling. Yet these are types, and therefore instances of type. Every type is a value, so type must be an instance of both and any. These facts taken together imply that any and type are mutually instances of each other! This is natural enough, given the criteria for membership in each, but it does not necessarily sit well with intuition.

Assert: type = {⊤}ᵀ; Assert: type ⊆ any; Assert: type ∈ any; Assert: any ∈ type;
any | Return to Type System | nontype