Why do non-proper types have no terms? I'm attending a course on Type Theory. The textbook is 'Types and Programming Languages' by Prof. Benjamin C. Pierce.

In Chapter 29, Prof. Pierce introduces 'type operator', which can generate another type with an input type. For example, 'Pair' can be a type operator which accepts any two types $X$ and $Y$ to form a type $Pair\; X\; Y$.

However, the 'type operator' itself is a type - a special type which is different from 'proper type' such as $Nat$ and $Nat \rightarrow Nat$. It seems that all 'proper types' have terms of it. For example, $Nat \rightarrow Nat$ has at least $(\lambda x : Nat. x)$. But type operator like $Pair$ does not have any term of it.

Prof. Pierce doesn't explain why $Pair$ has no term. Why 'non-proper' types can be called a 'type' when it does not correspond to any collection of programming language terms?
The best way to understand this is to have a second level of "types above types" which we then call kinds. Kinds can be formed by the following rules:


Type is a kind.
If K and L are kinds then so is K → L.


Kinds have elements:


The elements of Type are types, such as nat, bool, nat → nat, nat × nat, etc.
The elements of K → L are functions which map elements of K to elements of L.


For instance, Pair is an element of Type → Type → Type. It is a "kind-level" function which maps types A and B to type A × B. Another example is List which is an element of Type → Type and it maps a type A to the type List A of lists of As.

A very fancy kind is (Type → Type) → Type which takes a function on types and returns a type. An example of this is "recursive type definition". To see this, consider the most general form of a recursive type definition:

type t = Φ(t)


For instance, we could define lists of numbers like this (using OCaml notation):

type natlist = Nil | Cons of nat * natlist


This is a special case of the general recursive type definition if we take

Φ(a) = Nil | Cons of nat * a


We could actually define an operator rectype and then write

type t = rectype Φ


to define the type t which is equal to Φ(t). Now it takes a moment's thought that rectype is of kind  (Type → Type) → Type. (At this point, if you have never seen this before, you should be having a minor epiphany.)

In Haskell Type is written as * so sometimes Haskell tells you that something has type * → *. This means that the thing is a type-level function taking types to types. In Ocaml there are kinds under the hood but they are never shown to the user (well, kind of since they get exposed through module types).

Professor Pierce of course knows all these things much better than I do, but most likely at this point in the course he does not want to burden you with another layer of $\lambda$-calculus on top of $\lambda$-calculus. A quick and dirty solution is to just put all the kinds together in one big messy pile and call them "improper types". The trouble with such things is that the smart students will get confused (and rightfully so).