22 - Constructors and Kinds

Summary

The types nat → nat and nat list may be thought of as being built from other types by the application of a type constructor, or type operator. These two examples differ from each other in that the function space type constructor takes two arguments, whereas the list type constructor takes only one. We may, for the sake of uniformity, think of types such as nat as being built by a type constructor of no arguments. More subtly, we may even think of the types ∀(t · τ) and ∃(t. τ) as being built up in the same way by regarding the quantifiers as higher-order type operators.

These seemingly disparate cases may be treated uniformly by enriching the syntactic structure of a language with a new layer of constructors. To ensure that constructors are used properly (for example, that the list constructor is given only one argument and that the function constructor is given two), we classify constructors by kinds. Constructors of a distinguished kind T are types, which may be used to classify expressions. To allow for multiargument and higher-order constructors, we also consider finite product and function kinds. (Later we consider even richer kinds.)

The distinction between constructors and kinds on one hand and types and expressions on the other reflects a fundamental separation between the static, and the dynamic phase of processing of a programming language, called the phase distinction. The static phase implements the statics, and the dynamic phase implements the dynamics.