O'Reilly logo

Practical Foundations for Programming Languages by Robert Harper

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

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.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required