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

Type Names

A type may be named for convenience and comprehensibility, but a name is never regarded as part of a type. This distinguishes Avail's types from those found in other programming languages. When a name constitutes an intrinsic property of a type, then nominative typing is at play. In nominative typing, two types that have otherwise identical properties are considered unequal if they are differently named. In Avail, membership is the only intrinsic property of a type. Type names are extrinsic, and therefore many names may be given to the same type without altering its own value. Both integer and are perfectly reasonable names for {…, -1, 0, 1, …}ᵀ, and Avail permits both simultaneously; the former will probably be favored for common usage, but the second may add value to code that is highly number theoretic.

A type name is a source code construct only, a chiefly linguistic expression that features a method, constant, or variable that happens to yield a type. Because the widest possible scope for a constant or variable is a single module, a type name meant to span several modules must correspond to a method invocation. It will usually be the case that such broad visibility is desired, so a type name will usually be a method invocation. The following example illustrates type names:

/* This binds the primitive type {…, -1, 0, 1, …}ᵀ to the constant "_integer" so * that the compiler can use its exact value for inference in the method below. * There's no rhyme or reason to the value 13; it's just where the integer type * happens to live in the virtual machine's table of primitive values. An Avail * programmer won't need to know anything about this table, so don't sweat the * details. */ _integer ::= special object 13; /* Whenever the type name "integer" appears in source code, this method will be * invoked. Its answer is the value bound to "_integer". Because this constant * is defined at module scope, the compiler can infer that the return type of the * method implementation is {{…, -1, 0, 1, …}ᵀ}ᵀ. */ Method "integer" is [ _integer ]; /* Following are equivalent variable declarations, except of course that they * result in three different variables. Each of "integer", "_integer", and "special * object 13" are type expressions that reference the same primitive type {…, -1, * 0, 1, …}ᵀ. The first two are easily construed as type names. */ x : integer; y : _integer; z : special object 13; Assert: x's type = y's type = z's type;

As the above declaration of z indicates, even an expression that requires arguments may serve as a type name. This particular usage might stretch intuition about what constitutes a name, but highlights something more important: in reality, there are no type names in Avail; merely expressions that happen to produce types.

‹ Metatypes | Return to Type System | Type Annotations ›