<p><strong>Counter-question:</strong> why should every type be inhabited by a term? You could not have the Curry-Howard correspondence between typing systems and logic if every type was inhabited.</p>

<p><strong>Concrete answer:</strong> I don't have Pierce's book handy, but I think you are talking about the system $\lambda\underline{\omega}$ in <a href="https://en.wikipedia.org/wiki/Lambda_cube" rel="nofollow noreferrer">Barendregt's $\lambda$-cube</a>, a classification of typing systems along three orthogonal axes. (Please correct me if I'm wrong.)</p>

<p><img src="https://i.sstatic.net/H01bJ.png" alt="Barendregt&#39;s $\lambda$-cube."></p>

<p>$\lambda\underline{\omega}$ is the simplest extension of the simply typed $\lambda$-calculus allowing <strong>type-level computation</strong>. Note that $\lambda\underline{\omega}$  doesn't have parametric polymorphism or
type dependency. One way of thinking about $\lambda\underline{\omega}$ is that type-level computation is carried out by having another $\lambda$-calculus, but this time at the type level.
You can think of type-level computation as being run at 'compile time'.
 Why use a typed language to run type-level computation? Why not use the untyped $\lambda$-calculus at the type level? Because the things that could go wrong at the term level with untyped terms (e.g.  ill-formed programs like $3   + hello$) could now go wrong at the type level (e.g. $\mathbb{B}\; Pair$). So $\lambda\underline{\omega}$ needs a way of preventing ill-formed type-level computation. </p>

<p>But how? Well, let's use the simply typed $\lambda$-calculus again, but now at the type-level, to carry out, and constrain type-level computation? In order to avoid terminological confusion, we speak of kinds of for this second simply typed $\lambda$-calculus. In summary:</p>

<ul>
<li><p>Terms are classified by types.</p></li>
<li><p>Types are classified by kinds.</p></li>
</ul>

<p>(As an aside, you can iterate this and have kind-level computation in the same way and so on, but that's not done in $\lambda\underline{\omega}$.)</p>

<p>So far, I've said that kinds classify types. That's another way of saying that well-formed programs for type-level computation inhabit kinds. In $\lambda\underline{\omega}$ kinds are given by the grammar </p>

<p>$$
\newcommand{\TY}{\mathsf{Ty}}
\kappa\quad ::= \quad \TY\ \ |\ \  \kappa \rightarrow \kappa
$$</p>

<p>Here $\kappa \rightarrow \kappa'$ is the kind of type-level functions such as
$\lambda t^{\kappa}. \mathbb{N} \rightarrow \kappa$.
But what is $\TY$?
Answer: the base kind. The kind that is inhabited by 
all types that can potentially be inhabited by terms, e.g. types like $\mathbb{B}$
or $\mathbb{N} \rightarrow \mathbb{B}$. It is the only kind that is
inhabited by types. This gives  a neat classification of type-level programs into
types usable to be inhabited by terms, and type-level programs that are only used as components in the computation of such types.</p>

<p>Operators like $Pair$ are not kinded by $\TY$ and so cannot be
inhabited by terms. Instead $Pair$ has the kind $\TY$ $\rightarrow$
$\TY$ $\rightarrow$ $\TY$, which, by its very shape, cannot be
inhabited by types, it can only be used as a program  in a type-level
computation.  Now $\mathbb{N}$ (integers) and $\mathbb{B}$ (Booleans)
both are kinded $\TY$, hence the type level program $Pair
\;\mathbb{N} \;\mathbb{B}$ also has kind $\TY$ and can therefore be
inhabited by a program.</p>

CC BY-SA 3.0
2015-06-12T01:02:20.910Z
Thanks for the explanations on Kinds. But I'm afraid 'Kind' classification is not the final reason that _Pair_ is not inhabited. This classification must have been the result for incomprehensible extensions on type system. You've mentioned Curry-Howard correspondence and I guess that should be a better reason to make theoretical researchers create things like _Pair_. Am I right?
xywang
CC BY-SA 3.0
2015-06-12T05:39:59.190Z
@xywang I'm not sure I understand your question. You can invent all sorts of crazy typing systems, but that's not how $\lambda\underline{\omega}$ works. What do you think *should* be the inhabitants of $Pair$?
Martin Berger
CC BY-SA 3.0
2015-06-12T06:14:57.987Z
Sorry for my poor English...My previous comment was on two things: 1) being in different kinds seems to be the result of with/no inhabitants, but not the reason. 2) The counter-question is more interesting: what proposition can be matched to a type with no terms? Any false propositions?
xywang
CC BY-SA 3.0
2015-06-12T06:50:12.387Z
@xywang Regarding (1) I'd say being "in different kinds" is the cause why $Pair$ has no *term* inhabitants. That's the choice the designers of $\lambda\underline{\omega}$ made. As to (2), under the Curry-Howard interpretation of type theory, Falsity (if it is represented as a type) has no inhabitants. But not the other way round. Consider the type / proposition $(A \vee B) \rightarrow (A \wedge B)$. It is not equivalent to Falsity, but what program could have this type?
Martin Berger
CC BY-SA 3.0
2015-06-11T15:39:17.820Z
2015-06-11T21:37:24.887Z
2015-06-11T21:37:24.887Z
Martin Berger
<p>The best way to understand this is to have a second level of "types above types" which we then call <em>kinds</em>. Kinds can be formed by the following rules:</p>

<ol>
<li><code>Type</code> is a kind.</li>
<li>If <code>K</code> and <code>L</code> are kinds then so is <code>K → L</code>.</li>
</ol>

<p>Kinds have elements:</p>

<ol>
<li>The elements of <code>Type</code> are types, such as <code>nat</code>, <code>bool</code>, <code>nat → nat</code>, <code>nat × nat</code>, etc.</li>
<li>The elements of <code>K → L</code> are functions which map elements of <code>K</code> to elements of <code>L</code>.</li>
</ol>

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

<p>A very fancy kind is <code>(Type → Type) → Type</code> 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:</p>

<pre><code>type t = Φ(t)
</code></pre>

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

<pre><code>type natlist = Nil | Cons of nat * natlist
</code></pre>

<p>This is a special case of the general recursive type definition if we take</p>

<pre><code>Φ(a) = Nil | Cons of nat * a
</code></pre>

<p>We could actually define an operator <code>rectype</code> and then write</p>

<pre><code>type t = rectype Φ
</code></pre>

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

<p>In Haskell <code>Type</code> is written as <code>*</code> so sometimes Haskell tells you that something has type <code>* → *</code>. 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).</p>

<p>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).</p>

CC BY-SA 3.0
2015-06-12T01:08:36.140Z
Can we treat operators like _Pair_ not a type? I know the three levels on term-type-kind requires _Pair_ only lies in the type world. How about create another hierarchy which there are two worlds between terms and kinds? It seems that 'functions on types are type' is similar with 'functions on terms are terms'. Is that the reason we treat type operators as types?
xywang
CC BY-SA 3.0
2015-06-12T06:14:16.187Z
Isn't this what I said? `Pair` is a *function* at the kind-level and should not be treated as a type (but rather as a type operator, in other words a function). The reason you are treating type operators as types is probably pedagogical (I am guessing). Why don't you ask prof. Pierce?
Andrej Bauer
CC BY-SA 3.0
2015-06-12T06:32:37.283Z
I'm now clear about your point. I'm not sure whether treat type operator as type or not is a 'do as my wish' question... After reading the other replies it seems that the agreement is we should treat type operator as type and try to explain why there could be inhabited types.
xywang
CC BY-SA 3.0
2015-06-12T06:47:08.417Z
Type operators are clearly *not* types, unless you stretch the meaning of "type" beyond anything reasonable. They are functions from types to types. Why you call them improper types in your class I do not know.
Andrej Bauer
CC BY-SA 3.0
2015-06-11T15:42:26.510Z
2015-06-12T07:32:59.583Z
2015-06-12T07:32:59.583Z
Andrej Bauer
<p>The fact that a type operator doesn't describe a set of terms or values is precisely the reason that type operators aren't called proper types, but only improper types. Type operators are somewhat like types (because they are used for typing), but they are also somewhat unlike types (because they don't describe terms or values directly).</p>

<p>BTW, all proper types describe a set of values or terms, but that doesn't mean the set has to actually contain any values or terms. A proper type might also describe an empty set!</p>

CC BY-SA 3.0
2015-06-11T15:36:41.150Z
For now I treat type as something with practical use - semantic specification, formal helper on unstuckness etc. Why the theory researchers create types with no use?
xywang
CC BY-SA 3.0
2015-06-11T15:40:30.940Z
@xywang Type-theory researchers have many interests, one of them being the use of types as logical specifications. In that use case it is vital that not all types are inhabited.
Martin Berger
CC BY-SA 3.0
2015-06-11T15:17:19.430Z
2015-06-11T15:17:19.430Z
Toxaris
<p>Whether "Pair" is a type or not is mostly a naming question.  "Pair" is not a proper type in the sense that it makes no sense to talk about an object having type "Pair", but "Pair" exists in the language where types are described, and for this reason it can be described as being a type expression.</p>

<p>IOW, the language of types includes expressions like "Int" and "Pair Int Int" which are proper types, and this second expression is an instance of the general form "t1 t2" which is basically an application, but at the type-level.  So from this point of view "Pair" is an expression in the language of types, although it is not what is usually considered "a type" (which usually means "a proper type").</p>

CC BY-SA 3.0
2015-06-12T05:09:06.540Z
I used to think 'type' is defined after 'term' is defined. But now the type system can be free to go beyond 'term'...?
xywang
CC BY-SA 3.0
2015-06-12T08:33:05.797Z
@xywang Your original thinking works for simple programming languages, but not for more complicated ones. Think of type-level computation as a new programming language, executed at compile time, whose programs return -- at compile time -- a type. This returned type is used in the type-checking process.
Martin Berger
CC BY-SA 3.0
2015-06-12T05:04:31.537Z
2015-06-12T05:04:31.537Z
Stefan
<p>I'm attending a course on Type Theory. The textbook is 'Types and Programming Languages' by Prof. Benjamin C. Pierce.</p>

<p>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$.</p>

<p>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.</p>

<p>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?</p>

<type-theory>
Why do non-proper types have no terms?
xywang
# Why do non-proper types have no terms?

(Asked by: username_0 on 2015-06-11)

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?

**Tags:** type-theory

---

## 4 answers

### Answer by username_1 on 2015-06-11. Score: 3 | Accepted answer

**Counter-question:** why should every type be inhabited by a term? You could not have the Curry-Howard correspondence between typing systems and logic if every type was inhabited.

**Concrete answer:** I don't have Pierce's book handy, but I think you are talking about the system $\lambda\underline{\omega}$ in [Barendregt's $\lambda$-cube](https://en.wikipedia.org/wiki/Lambda_cube), a classification of typing systems along three orthogonal axes. (Please correct me if I'm wrong.)

![Barendregt's $\lambda$-cube.](https://i.sstatic.net/H01bJ.png)

$\lambda\underline{\omega}$ is the simplest extension of the simply typed $\lambda$-calculus allowing **type-level computation**. Note that $\lambda\underline{\omega}$ doesn't have parametric polymorphism or
type dependency. One way of thinking about $\lambda\underline{\omega}$ is that type-level computation is carried out by having another $\lambda$-calculus, but this time at the type level.
You can think of type-level computation as being run at 'compile time'.
Why use a typed language to run type-level computation? Why not use the untyped $\lambda$-calculus at the type level? Because the things that could go wrong at the term level with untyped terms (e.g. ill-formed programs like $3 + hello$) could now go wrong at the type level (e.g. $\mathbb{B}\; Pair$). So $\lambda\underline{\omega}$ needs a way of preventing ill-formed type-level computation.

But how? Well, let's use the simply typed $\lambda$-calculus again, but now at the type-level, to carry out, and constrain type-level computation? In order to avoid terminological confusion, we speak of kinds of for this second simply typed $\lambda$-calculus. In summary:

* Terms are classified by types.
* Types are classified by kinds.

(As an aside, you can iterate this and have kind-level computation in the same way and so on, but that's not done in $\lambda\underline{\omega}$.)

So far, I've said that kinds classify types. That's another way of saying that well-formed programs for type-level computation inhabit kinds. In $\lambda\underline{\omega}$ kinds are given by the grammar

$$
\newcommand{\TY}{\mathsf{Ty}}
\kappa\quad ::= \quad \TY\ \ |\ \ \kappa \rightarrow \kappa
$$

Here $\kappa \rightarrow \kappa'$ is the kind of type-level functions such as
$\lambda t^{\kappa}. \mathbb{N} \rightarrow \kappa$.
But what is $\TY$?
Answer: the base kind. The kind that is inhabited by
all types that can potentially be inhabited by terms, e.g. types like $\mathbb{B}$
or $\mathbb{N} \rightarrow \mathbb{B}$. It is the only kind that is
inhabited by types. This gives a neat classification of type-level programs into
types usable to be inhabited by terms, and type-level programs that are only used as components in the computation of such types.

Operators like $Pair$ are not kinded by $\TY$ and so cannot be
inhabited by terms. Instead $Pair$ has the kind $\TY$ $\rightarrow$
$\TY$ $\rightarrow$ $\TY$, which, by its very shape, cannot be
inhabited by types, it can only be used as a program in a type-level
computation. Now $\mathbb{N}$ (integers) and $\mathbb{B}$ (Booleans)
both are kinded $\TY$, hence the type level program $Pair
\;\mathbb{N} \;\mathbb{B}$ also has kind $\TY$ and can therefore be
inhabited by a program.

> **Comments:**
> **username_0**: Thanks for the explanations on Kinds. But I'm afraid 'Kind' classification is not the final reason that _Pair_ is not inhabited. This classification must have been the result for incomprehensible extensions on type system. You've mentioned Curry-Howard correspondence and I guess that should be a better reason to make theoretical researchers create things like _Pair_. Am I right?  
> **username_1**: @xywang I'm not sure I understand your question. You can invent all sorts of crazy typing systems, but that's not how $\lambda\underline{\omega}$ works. What do you think *should* be the inhabitants of $Pair$?  
> **username_0**: Sorry for my poor English...My previous comment was on two things: 1) being in different kinds seems to be the result of with/no inhabitants, but not the reason. 2) The counter-question is more interesting: what proposition can be matched to a type with no terms? Any false propositions?  
> **username_1**: @xywang Regarding (1) I'd say being "in different kinds" is the cause why $Pair$ has no *term* inhabitants. That's the choice the designers of $\lambda\underline{\omega}$ made. As to (2), under the Curry-Howard interpretation of type theory, Falsity (if it is represented as a type) has no inhabitants. But not the other way round. Consider the type / proposition $(A \vee B) \rightarrow (A \wedge B)$. It is not equivalent to Falsity, but what program could have this type?  

---

### Answer by username_2 on 2015-06-11. Score: 6

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).

> **Comments:**
> **username_0**: Can we treat operators like _Pair_ not a type? I know the three levels on term-type-kind requires _Pair_ only lies in the type world. How about create another hierarchy which there are two worlds between terms and kinds? It seems that 'functions on types are type' is similar with 'functions on terms are terms'. Is that the reason we treat type operators as types?  
> **username_2**: Isn't this what I said? `Pair` is a *function* at the kind-level and should not be treated as a type (but rather as a type operator, in other words a function). The reason you are treating type operators as types is probably pedagogical (I am guessing). Why don't you ask prof. Pierce?  
> **username_0**: I'm now clear about your point. I'm not sure whether treat type operator as type or not is a 'do as my wish' question... After reading the other replies it seems that the agreement is we should treat type operator as type and try to explain why there could be inhabited types.  
> **username_2**: Type operators are clearly *not* types, unless you stretch the meaning of "type" beyond anything reasonable. They are functions from types to types. Why you call them improper types in your class I do not know.  

---

### Answer by username_3 on 2015-06-11. Score: 2

The fact that a type operator doesn't describe a set of terms or values is precisely the reason that type operators aren't called proper types, but only improper types. Type operators are somewhat like types (because they are used for typing), but they are also somewhat unlike types (because they don't describe terms or values directly).

BTW, all proper types describe a set of values or terms, but that doesn't mean the set has to actually contain any values or terms. A proper type might also describe an empty set!

> **Comments:**
> **username_0**: For now I treat type as something with practical use - semantic specification, formal helper on unstuckness etc. Why the theory researchers create types with no use?  
> **username_1**: @xywang Type-theory researchers have many interests, one of them being the use of types as logical specifications. In that use case it is vital that not all types are inhabited.  

---

### Answer by username_4 on 2015-06-12. Score: 0

Whether "Pair" is a type or not is mostly a naming question. "Pair" is not a proper type in the sense that it makes no sense to talk about an object having type "Pair", but "Pair" exists in the language where types are described, and for this reason it can be described as being a type expression.

IOW, the language of types includes expressions like "Int" and "Pair Int Int" which are proper types, and this second expression is an instance of the general form "t1 t2" which is basically an application, but at the type-level. So from this point of view "Pair" is an expression in the language of types, although it is not what is usually considered "a type" (which usually means "a proper type").

> **Comments:**
> **username_0**: I used to think 'type' is defined after 'term' is defined. But now the type system can be free to go beyond 'term'...?  
> **username_1**: @xywang Your original thinking works for simple programming languages, but not for more complicated ones. Think of type-level computation as a new programming language, executed at compile time, whose programs return -- at compile time -- a type. This returned type is used in the type-checking process.  

---

