## 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 `T`

is _{X}**covariant** on type parameter `X`

when, for two types `A`

and `B`

, `A`

is a subtype of `B`

implies that `T`

is a subtype of _{A}`T`

: _{B}`∀`

.
_{T,A,B ∈ type}: A ⊆ B → T_{A} ⊆ T_{B}

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 `T`

is _{X}**contravariant** on type parameter `X`

when, for two types `A`

and `B`

, `A`

is a subtype of `B`

implies that `T`

is a subtype of _{B}`T`

: _{A}`∀`

.
_{T,A,B ∈ type}: A ⊆ B → T_{B} ⊆ T_{A}

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.

‹ Type Compatibility | | | Return to Type System | | | Metatypes › |