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:

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.