Type Parameterization

Some types depend on other values to specify their membership. While it is useful to talk about the type whose values are sets, it is typically more useful to talk about the type whose values are, say, sets of integers. Knowing that a set contains only integers, it is possible to specify operations that produce the sum of the members, find the minimum or maximum member, or ascertain whether each member is even. If it is only known that the instances of a type are sets, then it is unclear what operations may be performed with the instances; only the most basic operations that are meaningful for all sets are guaranteed valid.

A type that depends upon one or more other values is incomplete. Given an incomplete type A that depends upon a value B, it is said that B is a type parameter of A or, alternatively, that A is parametric on B. A type is considered complete if it either 1) does not have any type parameters or 2) has an actual value bound to each of its type parameters.

Consider the type set. In Avail, this type is incomplete. It has a type parameter, the element type, that restricts the membership of each instance to values of a particular type. The type set of {…}ᵀ is the most general completion, imposing no membership restrictions on its instances. The type set of {…, −1, 0, 1, …}ᵀ, on the other hand, has as instances only those sets whose members are exclusively integers.

It is clear to see that set of {…}ᵀ is a supertype of set of {…, -1, 0, 1, …}ᵀ. The former has all sets as its instances, and so trivially includes all sets whose members are integers. And in turn, set of {…, -1, 0, 1, …}ᵀ is a supertype of set of {1, 2, 3, …}ᵀ, whose instances are precisely the subsets of the set of strictly positive integers. Note that {1, 2, 3, …}ᵀ ⊆ {…, -1, 0, 1, …}ᵀ ⊆ {…}ᵀ and set of {1, 2, 3, …}ᵀ ⊆ set of {…, -1, 0, 1, …}ᵀ ⊆ set of {…}ᵀ. As the element type becomes more specific, the set type also becomes more specific: the complete type covaries with the type parameter.

Formally, given an incomplete type T, a complete type TX is covariant on type parameter X when, for two types A and B, A is a subtype of B implies that TA is a subtype of TB: ∀T,A,B ∈ type: A ⊆ B → TA ⊆ TB.

Not every relationship between a complete type and a type parameter is covariant. Consider the following code example, which (incorrectly) treats a function type as covariant with respect to its parameter types.

The actual function, [s : string | s[1]], requires that its argument be a string. Attempting to apply this function to something other than a string must therefore be illegal. But the variable firstChar holds a function that accepts any argument, so on its face firstChar(15) must be legal because 15 is an instance of any. And the application is, in fact, legal. So what is wrong here?

The problem is this: the initialization of firstChar is invalid. It implicitly reasons that because string is a subtype of any, then [string]→character must be a subtype of [any]→character. Though seductive, this reasoning is erroneous. Consider the following code snippet as a correction to the previous one:

The assignment is now correct. The actual function's parameter type may be more general than the one declared by firstChar because the actual function will only be applied to values of a type more specific than the one that it requires. As long as the parameter type of the actual function is no more specific than what firstChar specifies, then all applications of firstChar to instances of nonempty string must be correct. In fact, the parameter type of the actual function could be considerably more general; even if it were any, then all applications of firstChar would still need to conform to nonempty string, one of any's infinitely many subtypes. So as the parameter type of a function type becomes more general, the function type itself becomes more specific: the complete type contravaries with the type parameter.

Formally, given an incomplete type T, a complete type TX is contravariant on type parameter X when, for two types A and B, A is a subtype of B implies that TB is a subtype of TA: ∀T,A,B ∈ type: A ⊆ B → TB ⊆ TA.

Avail provides no access to incomplete types. Parameterized types are constructed, ultimately, using primitive operations that accept the required type parameters and answer completed types.