|22||Constructors and Kinds|
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.