Typing Rules

Contexts and judgments

A term such as $f\;p$ cannot be checked in isolation: its type depends on what $f$ and $p$ are. A context $\Gamma$ records that information. It is an ordered list of assumptions

giving the type of each variable in scope, and $\dom(\Gamma)$ denotes the set of names $\{x_1, \ldots, x_n\}$. The empty context is written $\cdot$.

Order matters. A later type may mention an earlier variable, as in $P : \Sort{0},\; h : P$: the assumption $h : P$ only makes sense once $P$ is known to be a proposition. Names in a context will be required to be distinct, so a context can be used like a dictionary from names to types; but it is a dictionary whose entries depend on each other in sequence.

Two judgments are defined together.

• $\ctxok{\Gamma}$ means that the context $\Gamma$ is well formed: each assumed type is a type in the context before it.
• $\Gamma \vdash t : A$ means that under the assumptions in $\Gamma$, the term $t$ has type $A$.

Through the Curry-Howard lens, $\Gamma \vdash t : A$ says that $t$ is a proof of $A$ from the hypotheses $\Gamma$.

The rules

Figure 3.1 lists all the rules. Each rule has premises above the line and a conclusion below it; the conclusion holds whenever every premise does. The rule names on the right are used throughout the book.

Two of the rules use operations on terms that the next chapters treat as black boxes.

Substitution. T-App writes $\subst{B}{x}{a}$ for the result of replacing every free occurrence of $x$ in $B$ by $a$. For example, $\subst{(P \to P)}{P}{Q} = Q \to Q$. Replacing names inside binders needs care, which Chapter 11 explains; until then the intuitive meaning is enough.

Definitional equality. T-Conv writes $A \conv B$ when $A$ and $B$ are "the same type" in a sense the kernel can decide mechanically. Two kinds of difference are ignored.

• The names of bound variables. $\tPi{P}{\Sort{0}}{P \to P}$ and $\tPi{Q}{\Sort{0}}{Q \to Q}$ state the same proposition. Terms that differ only in this way are alpha-equivalent, written $A \alphaeq B$.
• Computation. If $\mathit{Id} = \tLam{X}{\Sort{0}}{X}$, then $\mathit{Id}\;P$ computes to $P$ by plugging $P$ in for $X$, so a proof of $\mathit{Id}\;P$ should count as a proof of $P$. The computation step $(\tLam{x}{A}{t})\;s \betared \subst{t}{x}{s}$ is called beta-reduction.

The kernel decides $A \conv B$ by computing both sides as far as possible and then checking whether the results are alpha-equivalent. Chapter 12 defines this precisely.

Reading the rules

The rules are best read from the bottom up, as a recipe: to establish the conclusion, establish the premises.

C-Empty and C-Ext. A context is built one assumption at a time, and each new assumption must have a type as its type. The side condition $x \notin \dom(\Gamma)$ forbids two assumptions with the same name. Since the names of bound variables do not matter, this restricts nothing: a binder that would clash can always be renamed first. Chapter 11 shows what goes wrong in a kernel that skips this condition.

T-Sort. Every universe lives in the next one: $\Sort{0} : \Sort{1}$, $\Sort{1} : \Sort{2}$, and so on. Chapter 13 explains why a universe cannot be its own type.

T-Var. A variable has the type the context assigns to it. Logically: use a hypothesis.

T-Pi. $\tPi{x}{A}{B}$ is a type if $A$ is a type and $B$ is a type once $x : A$ is assumed. The resulting universe is $\imax(u, v)$, which is $0$ if $v = 0$ and $\max(u, v)$ otherwise. In words: a $\Pi$-type is a proposition whenever its body is a proposition, no matter what it quantifies over; otherwise it lives in the larger of the two universes. Logically, this rule says when $A \to B$ and $\forall x{:}A.\,B$ are well-formed statements.

T-Lam. To build a function from $A$ to $B$, assume $x : A$ and build a term $t$ of type $B$. The body's type $B$ may mention $x$, and it is kept as is in the resulting $\Pi$-type, which is where dependency enters. Logically, this is the introduction rule for implication and for the universal quantifier: to prove $A \to B$, assume $A$ and prove $B$.

T-App. If $f$ maps each $x : A$ to an element of $B$, and $a : A$, then $f\;a$ has type $B$ with $x$ replaced by $a$. When $B$ does not mention $x$ this is modus ponens: from $A \to B$ and $A$, conclude $B$. When it does, it is instantiation of a universal statement. For example, if $f : \tPi{n}{\Nat}{n + 0 = n}$, then $f\;3 : 3 + 0 = 3$ (natural numbers arrive in Chapter 7).

T-Conv. Types that are equal up to computation are interchangeable: from $h : \mathit{Id}\;P$ we may conclude $h : P$. The premise $\Gamma \vdash B : \Sort{u}$ ensures that the new type is itself a type. This is the only rule whose use is not determined by the shape of $t$, a fact that matters for the algorithm in Chapter 5.

Why application matters

The rules that build things (T-Lam and T-Pi) may seem more important than T-App, but without application a proof can return a hypothesis without ever using it. Roughly, only propositions whose conclusion is literally one of the hypotheses, such as $P \to Q \to P$, would be provable. Composition,

has the proof $\tLam{f}{P \to Q}{\tLam{g}{Q \to R}{\tLam{p}{P}{g\,(f\,p)}}}$, which applies $f$ and then $g$. Every proof that does more than restate an assumption goes through T-App, and in a dependent type theory T-App is also where substitution, and therefore most of the subtlety, lives.

A first derivation

A derivation is a tree of rule instances whose root is the judgment being established. Here is the derivation that $\tLam{P}{\Sort{0}}{\tLam{h}{P}{h}}$ proves $\tPi{P}{\Sort{0}}{P \to P}$. Write $\Gamma_1 = P : \Sort{0}$ and $\Gamma_2 = \Gamma_1, h : P$, and omit the well-formedness premises $\ctxok{\Gamma}$, which are routine.

The kernel builds this tree. Below, each node is one application of a rule, with the judgment it establishes; switch to the call view to read it top-down as the recursion that produces it. Replace the term with your own to see which rules fire.

Two observations. First, the shape of the tree follows the shape of the term: a $\lambda$ at the root, a $\lambda$ below it, variables at the leaves. Second, the type at the root is $\tPi{P}{\Sort{0}}{\tPi{h}{P}{P}}$, whereas the stated proposition was $\tPi{P}{\Sort{0}}{P \to P}$. These differ only in the name of a bound variable ($h$ versus the anonymous _ of the arrow), so they are alpha-equivalent, and T-Conv bridges the gap. Chapter 6 revisits this example with the algorithm.

Exercises