chapter02.tex

\chapter{Type Systems}\label{cha:typesystems}

\coloredlettrine{F}{unction} definition in mathematics usually involves
specifying the~kind of inputs it accepts, and the~kind of output it produces.
For example, at the~start of the~previous chapter, we saw the~function $f(x) =
x + y$ applied to an~integer 0. Although we did not mention the~domain nor
the~range of the~function then, we can now pick some and say that $f$ is
a~function from integers to integers, or
\[
  f: \Int \to \Int.
\]
Corresponding to the~mathematical intuition, the~pure \lc can be modified by
attaching expressions called \emph{types} to terms, like labels to denote their
intended input and output. While conventionally the~term \emph{type} is used to
refer to an~abstraction of a~set of values, generally, a~type can be any
property of a~term, that we can establish without executing it.

We are looking to formulate the~procedure of assigning the~type annotations to
\lts, such that the~terms for which this procedure fails will be deemed
invalid. Hence, thanks to the~type system we are able to reject faulty programs
that exhibit unwanted behaviour before they are executed. As a~consequence of
the~\emph{Halting Problem} though, the~conclusions a~type system can make are
necessarily just approximations. Either it must reject programs that might have
run without an~error, or accept programs that may error when executed. With more
expressive type systems, we are able to more precisely decide whether to reject
a~given program.

In this chapter, we will formulate gradually more expressive type systems,
but to do that effectively, we need to introduce a~bit of new notation first.

\sectionwithtoc{Natural deduction}\label{sec:natural_deduction}

Conventionally, type systems are presented using \emph{natural deduction}, which
was first introduced by \citet{gentzen_1935} as a~new formulation of logic.
Natural deduction is a deductive system and is thus specified by a~collection of
\emph{judgments} and a~collection of \emph{rules}. A~rule takes a~list of
judgments and produces a~new judgment.

\emph{Judgment} is a~proposition in the~metalanguage. For example, in
first-order logic, judgment can say that a~certain string of symbols $A$ is
a~\emph{well-formed proposition}, written \emph{$A$ prop}. Another judgment may
say that these symbols form a~\emph{proposition that is true}, written
\emph{$A$ true}.

A~\emph{rule} is written as a~horizontal line with its \emph{premises}, or
\emph{antecedents}, above the~line and its \emph{conclusion}, or
\emph{consequent}, below the~line. There can be zero or more premises, but
conclusion is exactly one. The~interpretation of a~rule is that if all premises
hold, then the~conclusion follows. An~example of a~rule may be the~rule of
implication elimination, or \emph{modus ponens}, which can be stated as:
\begin{mathpar}
  \inferrule*[right=Mp]
  {A \supset B \\ A}
  {B}
\end{mathpar}
It says that if ``$A$ implies $B$,'' written $A \supset B$, and ``$A$,'' then
``$B$.'' Note that some rules have a~name, which is attached to the~right side
of the~horizontal line. In our example the~name is \ir{Mp}.

Given a~set of rules, we are able to combine them to form a~tree, where every
node is an~instance of a~rule. We say we can \emph{deduce}, or \emph{derive},
a~formula if there exists a~tree where the~formula is at the~root and all leaves
are \emph{axioms}, that is rules that have no premises.

Natural deduction also often involves \emph{hypothetical judgments}, or
\emph{reasoning from assumptions}. To express hypothetical reasoning within
the~rules of a~deductive system, we indicate in each judgment on which
hypotheses it depends. To denote the~hypothetical judgment of $B$ assuming $A$,
we write
\[
  A \vdash B.
\]
The~list of assumptions on which a~judgment depends, denoted by $\Gamma$, can be
extended by appending an~assumption $A$ to the~end of the~list with a~comma:
$\Gamma, A$. We can also combine lists of assumptions; the~list that results
from appending the~assumptions from $\Gamma_2$ to the~list $\Gamma_1$ is written
$\Gamma_1, \Gamma_2.$

For example, the~derivation tree of the~judgment that given that ``$A$ implies
$B$'' and given ``$A$,'' one may deduce ``$A$ and $B$,'' written $A \wedge B$:
\begin{mathpar}
  \inferrule*
  {
    \inferrule*
    { }
    { A \supset B, A \vdash A } \\
    \inferrule*[right=Mp]
    {
      \inferrule*
      { }
      {A \supset B, A \vdash A \supset B} \\
      \inferrule*
      { }
      {A \supset B, A \vdash A }
    }
    { A \supset B, A \vdash B }
  }
  { A \supset B, A \vdash A \wedge B }
\end{mathpar}

Notice that in the~definition of \ir{Mp} we have elided the~ambient
assumptions that could have been added to every judgment, i.e. we could have
written:
\begin{mathpar}
  \inferrule*[right=Mp$'$]
  {\Gamma_1 \vdash A \supset B \\ \Gamma_2 \vdash A}
  {\Gamma_1, \Gamma_2 \vdash B}
\end{mathpar}

\sectionwithtoc{Simple types}

We will present a~few different type systems throughout the~text, each
an~extension of some previous ones. So to start at the~beginning, we will
define a~basic type system that utilises the~\emph{simple types}.

\begin{definition}\label{def:simple_type}
  Assume that we are given a finite or infinite sequence of symbols called
  \emph{atomic types}; then we define \emph{simple types} as follows:
  \begin{enumerate}
    \item every atomic type is a~simple type;
    \item if $S$ and $T$ are simple types, then $(S \to T)$ is a~simple type,
      called a~\emph{function type};
    \item if $S$ and $T$ are simple types, then $(S \times T)$ is a~simple type,
      called a~\emph{pair type};
  \end{enumerate}
\end{definition}

Throughout the~text we use the~letters $S$, $T$, $U$, and $V$ to denote
arbitrary types.

Atomic types are intended to denote a~particular set. For example we may have
the~atomic type \Int for the~set of integers, and \Bool for the~set of Boolean
values $\{ \mathtt{true}, \mathtt{false} \}$. A~special kind of atomic types are
\emph{unit types}, which denote singleton sets. In particular, our
\mbox{λ-calculi} use the~unit types $\1$, read ``one,'' with its value $\munit$
and $\top$, read ``top,'' with its value $\aunit$.

A~function type $(S \to T)$ is intended to denote some given set of
\emph{functions from $S$ to $T$}. That is, functions that accept as input
a~member of its \emph{domain}, the~set denoted by $S$, and produce an~output in
its \emph{range}, a~subset of the~set denoted by $T$. The~exact set of functions
denoted by $(S \to T)$ depends on the~intended use of the~type system we are
trying to build. It might be the~set of \emph{all} functions from $S$ to $T$, or
just some subset. Some examples of simple types are:
\begin{align*}
  &(\Int \to \Int) && \text{functions from integers to integers;} \\
  &(\Int \to \Bool) && \text{functions from integers to Boolean values;} \\
  &(\Int \to (\Int \to \Int)) && \text{functions from integers to functions;} \\
  &((\Int \to \Int) \to \Int) && \text{functions from functions to integers;} \\
  &((\Int \to \Int) \to (\Int \to \Int)) && \text{functions from functions to
    functions.}
\end{align*}
In contrast with the~\lt application, the~function type is right-associative
and we will abbreviate accordingly:
\begin{align*}
  &S \to T  &  &\text{for} &  &(S \to T); \\
  &S \to T \to U  &  &\text{for} &  &(S \to (T \to U)); \\
  &S_1 \to \dotsb \to S_n \to T  &  &\text{for} &
    &(S_2 \to ( \dotsb \to (S_n \to T) \dotsb )); \\
  &S \times T  &  &\text{for} &  &(S \times T).
\end{align*}
We do not define any order of precedence between the~function and pair types.
Note that an~expression like $S \to T$, which contains type variables $S$ and
$T$, is not itself a~type. It is only a~name in the~metalanguage for a~type of
unspecified functions.

A~pair type, or a~\emph{product type}, $(S \times T)$ denotes the~Cartesian
product of the~sets denoted by $S$ and $T$. For example, $((\Int \to \Int)
\times \Bool)$ denotes the~set of ordered pairs $(f, b)$, where $f$ is
a~function from integers to integers, and $b$ is a Boolean value.

There is also a~dual notion of a~pair type, the~\emph{sum type} $(S + T)$, which
is used to denote the~set of members of either $S$, or $T$. In this text
however, we are focused on the~pair type, so we will not be working with the~sum
type further.

\sectionwithtoc{Type judgment}

When we apply the~natural deduction in the~context of types, we are able to
formulate deduction trees that assign types to terms.

\begin{definition}
  For any \lt $M$ and type $T$, define a~\emph{type assignment} formula as
  \[
    M \is{} T.
  \]
\end{definition}

The~formula $M \is{} T$ can be read informally as ``$M$ has type $T$,'' or ``we
assign to $M$ the~type $T$.'' Then, \emph{type judgment} is the~formula
\[
  \Gamma \vdash M \is{} T,
\]
which is defined to mean that there is a~deduction-tree, whose root formula is
$M \is{} T$, and whose leaves are members of $\Gamma$. The~sequence of
assumptions $\Gamma$ is called the~\emph{context} of the~typing judgment. When
the~context is empty, we write
\[
  \vdash M \is{} T.
\]

\sectionwithtoc{Simply typed \lc}\label{sec:stlc}

Generally, there are two ways we can attach types to terms. The~\emph{implicit},
or \emph{Curry-style}, semantics use the~\lts as we have seen them in
\autoref{def:lambda_calculus} and assign type to a~term after it had been built.
The~type then sits next to the~term. In the~other approach, called
\emph{explicit}, or \emph{Church-style}, the~term's type is a~built-in part of
the~term itself.

We expect to present complex enough systems later, for which finding the types
in the~implicit version may not be computable~\citep{wells_1999}, hence we will
use the~explicit semantics.

We define a~new version of \lts, where binding variables are annotated with
their types:
\begin{definition}[Simply typed \lts]\label{def:stlc}
  Assume that we are given an~infinite sequence of expressions $\mathbf{v}_0,
  \mathbf{v}_1, \mathbf{v}_2, \dots$ called \emph{variables}. The~set of
  \emph{\lts} is defined inductively; if $x$ and $y$ are variables, $S$ and $T$
  are types, and $M$ and $N$ are \lts, then:
  \begin{enumerate}
    \item every variable is a~\lt;
    \item function constructor and eliminator, also called abstraction and
      application, are \lts:
      \begin{mathpar}
        \lam {x \is{} S} M \and M \: N
      \end{mathpar}
    \item \label{def:stlc:let_item} pair constructor and eliminator are \lts:
      \begin{mathpar}
        \mpair M N \and \letpair{S \times T} x y M N
      \end{mathpar}
    \item unit constructor and eliminator are \lts:
      \begin{mathpar}
        \munit \and \letu M N
      \end{mathpar}
  \end{enumerate}
\end{definition}
The~function abstraction now contains a~type annotation $S$ of its binding
variable $x$ as part of its syntax.

The~pair constructor encloses the~two terms $M$ and $N$ that form its elements.
The~pair eliminator binds the~variables $x$ and $y$ to the~elements of the~pair
given by the~term $M$ and makes them bound in the~scope of $N$. The~subscript
type annotation specifies the~expected type of the~pair.

Substitution on simply typed \lts works analogously to
\autoref{def:substitution}: we disregard the~type annotations on the~binding
variables and substitute in the~sub-terms recursively, while taking care that we
do not change the~semantics of the~term by applying α-conversions where
necessary.

Similarly, we extend the~definition of β-contraction. Generally β-contraction
tells us how to simplify a~term that involves an~eliminator directly applied to
a~constructor.
\begin{definition}
  In a~given term, every occurrence of a~β-redex on the~left hand side of
  $\triangleright_{1\beta}$ can be replaced by the~contractum on the~right side:
  \begin{align*}
    (\lam {x \is{} S} M) \: N \quad &\triangleright_{1\beta} \quad M[N/x] \\
    \letpair {S \times T} x y {\mpair M N} O \quad &\triangleright_{1\beta}
      \quad O[M/x, \: N/y] \\
    \letu \munit N \quad &\triangleright_{1\beta} \quad N
  \end{align*}
\end{definition}

The~\emph{type system} of simply typed \lc consists of two parts. First are
the~\lts we have just defined and second are the~deduction rules. These rules
are called \emph{typing rules} and they determine how a~type gets assigned to
a~term. If a~type is assigned to a~term, we call this term \emph{well-typed} and
it is the~point of the~type system to fail to assign a~type to as many terms,
which could be ``misbehaving'' during the~evaluation, as possible.

Now we will go over the~set of rules in this type system. We start with an~axiom
which says that we can pick a~variable from the~context:
\begin{mathpar}
  \inferrule*[right=Var]
  { }
  {\Gamma_1, x \is{} S, \Gamma_2 \vdash x \is{} S}
\end{mathpar}

Next, there are three pairs of rules that judge the~introduction and elimination
of λ-abstractions, pairs, and units; hence the~suffixes \ir{-I} and \ir{-E} in
their names.

For the~function type, the~eliminator \ir{$\to$-E} says that the~term $M$ can be
applied to any value $N$ of type $S$. Conversely, to construct a~term of type
$S \to T$, the~introduction rule \ir{$\to$-I} expects a~description of how
the~term behaves upon applying eliminator to it; meaning, we should provide
a~term of type $T$ which may contain a~free variable $x$ of type $S$:
\begin{mathpar}
  \inferrule*[right=$\to$-I]
  {\Gamma, x \is{} S \vdash M \is{} T}
  {\Gamma \vdash (\lam {x \is{} S} M) \is{} S \to T}

  \inferrule*[right=$\to$-E]
  {\Gamma \vdash M \is{} S \to T \\ \Gamma \vdash N \is{} S}
  {\Gamma \vdash M \: N \is{} T}
\end{mathpar}

The~introduction rule \ir{$\times$-I} for the~pair type says that to construct
a~term of type $S \times T$, it needs terms supplying the~two elements of
the~pair. The~eliminator \ir{$\times$-E} specifies that to use the~pair $M$, we
need to describe the~resulting term for all possible pairs; that is, we assume
that $M$ takes the~form $\mpair x y$ and we provide a~term $N$ in the~context of
variables $x$ and $y$, then the~eliminator binds those variables to the~two
elements of $M$:
\begin{mathpar}
  \inferrule*[right=$\times$-I]
  {\Gamma \vdash M \is{} S \\ \Gamma \vdash N \is{} T}
  {\Gamma \vdash \mpair M N \is{} S \times T}

  \inferrule*[right=$\times$-E]
  {
    \Gamma \vdash M \is{} S \times T \\
    \Gamma, x \is{} S, y \is{} T \vdash N \is{} U
  }
  {
    \Gamma \vdash \letpair{S \times T} x y M N \is{} U
  }
\end{mathpar}

The~introduction rule for the~unit is an~axiom, saying there is exactly one way
of constructing something of type \1. The~eliminator says that to use a~term of
type \1, we need to specify what happens when $M$ turns out to be $\munit$,
which covers all possible values like \ir{$\times$-E} does for pairs:
\begin{mathpar}
  \inferrule*[right=\1-I]
  { }
  {\Gamma \vdash \munit \is{} \1}

  \inferrule*[right=\1-E]
  {
    \Gamma \vdash M \is{} \1 \\
    \Gamma \vdash N \is{} S
  }
  {
    \Gamma \vdash \letu M N \is{} S
  }
\end{mathpar}

\sectionwithtoc{Dependent types}

The Church-style system from the~previous chapter has lost some of
the~versatility of the~pure \lc. The~term $\lam {x \is{} S} x$ represents
the~one operation of doing nothing, the~identity function, yet this one
operation is represented by different terms for different types $S$. We want our
formalism to keep track of the~fact that identity does the~same thing regardless
of the~type. An~ability to universally quantify the~types, which we will gain
with the~introduction of dependent types, will allow us to express this; then
the~type of an~identity function will, in effect, be ``for all types $S$,\,
$S \to S$.''

To properly talk about dependent types, we feel we need to first touch on one
important observation; it is the~correspondence between computer programs and
mathematical proofs, known as the~\emph{Curry–Howard isomorphism}.
\citet{curry_1934} observed that every type of a~function, $S \to T$,
can be read as a~proposition of an~implication, $S \supset T$. Then there exists
a~function of a~given type if and only if, the~corresponding proposition is
provable. \citet{curry_1958} later extended the~observation to also include
the~correspondence between terms and proofs. Finally, in 1969, in manuscript not
published until much later, \citet{howard_1980} described the~relation between
the~natural deduction and the~simply typed \lc, as well as shown that
the~simplification of proofs corresponds to the~evaluation of programs.
\citet{wadler_2015} provides a~detailed yet approachable introduction to
the~topic. We will now generalise the~simple types into their dependent
counterparts and use the~Curry–Howard correspondence to form a~better intuition
around them.

The~dependent analogue of the~type $S \to T$ is the~\emph{dependent
function type}, in the~academic literature usually written as ${(\Pi x \is{}
S \, . \: T)}$, but we will write:
\[
  \dep x S T.
\]
Here $S$ and $T$ are types, but $T$ may contain an~occurrence of $x$; meaning,
$T$ may depend on a~value of type $S$ to form a~type. Thus, a~term of type
$\dep x S T$ represents function that for an~argument $N$ of type $S$ produces
a~value of type \,$T[N/x]$. In the~special case that \,$T$ does not contain
an~occurrence of $x$, $\dep x S T$ is the~type $S \to T$.

On the~logic side, the~dependent function type corresponds to a~universal
quantification; hence, we can read it as ``for all $s$ in $S$, $T[s/x]$ is
inhabited,'' where \emph{inhabited} means that the~type contains some value.
The~$\Pi$ in the~notation of the~dependent function type references the~fact
that we can interpret it as a~\emph{product} of \,$T$, for every $s \in S$; that
is, a~value of type $\dep x S T$ can be interpreted as a~tuple of size $|S|$,
where the~$s$th element is of type \,$T[s/x]$, for $s$ of type $S$.

The~dependent analogue of type $S \times T$ is the~\emph{dependent pair type},
again, usually written as ${(\Sigma x \is{} S \, . \: T)}$, but we will write:
\[
  (x \is{} S) \times T.
\]
The value of this type is a~pair $\mpair x y$, where $x$ is of type $S$ and $y$
is of type $T$, which is again a~function parametrised by $x$; hence, the~type
of the~second element is determined by the~value of the~first.

This type corresponds to the~existential quantification in logic. It uses
$\Sigma$ in its notation because we can interpret it as a~\emph{disjoint union}
of all $T$, with an~index from $S$; meaning, a~value of type
$(x \is{} S) \times T$ can be interpreted as a~member of the~set
\[
  \bigcup_{s \, \in \, S} \{ \mpair s t \mid t \in T[s/x] \}.
\]
By having a~value of this dependent pair type, we are therefore \emph{proving}
that ``there exists an~$s \in S$, such that $T[s/x]$ is inhabited.''

In dependent types, terms can occur in place of types so we must scrap
the~distinction between terms and types. Thus, we will define
\emph{pseudo-terms} which will subsume both the~terms from \autoref{def:stlc}
and types.

\sectionwithtoc{Pseudo-terms}

For the~following type systems, we will use the~general notion of
\emph{pseudo-terms}. First, we define a~generous \emph{pseudo-terms} grammar and
then we will construct typing rules, that identify the~well-typed terms within
pseudo-terms.

\begin{definition}\label{def:pseudo-term}
  Assume that we are given an~infinite sequence of expressions $\mathbf{v}_0,
  \mathbf{v}_1, \mathbf{v}_2, \dots$ called \emph{variables}. The~set of
  \emph{pseudo-terms} is defined inductively; if $x, x', y$ and $z$ are
  variables and $M, N, O, P$ and $Q$ are pseudo-terms, then:
  \begin{enumerate}
    \item every variable is a~pseudo-term;
    \item every atomic type is a~pseudo-term;
    \item dependent function type formation, abstraction, and application
      are pseudo-terms:
      \begin{mathpar}
        \dep x M N \and \lam {x \is{} M} N \and M \: N
      \end{mathpar}
    \item dependent pair type formation, its constructor and eliminator are
      pseudo-terms:
      \begin{mathpar}
        (x \is{} M) \times N \and \mpair M N \and \letpair{(x' \is{} O)\times P}
        [z] x y M [Q] N
      \end{mathpar}
    \item unit type, unit and its eliminator are pseudo-terms:
      \begin{mathpar}
        \1 \and \munit \and \letu [x] M [O] N
      \end{mathpar}
  \end{enumerate}
\end{definition}
Analogously to how $N$ is the~\emph{scope} of $x$ in the~function abstraction,
$N$ is also the~scope of $x$ in the~dependent type formation and dependent pair
formation.

The~dependent pair eliminator takes the~pair given by the~term $M$ and binds
the~variables $x$ and $y$ to its elements. The~scope of these variables is $N$.
The~variable $z$ binds the~whole pair and its scope is $Q$, which is a~type
annotation specifying the~type of $N$. The~subscript type annotation
$(x' \is{} O)\times P$ specifies the~expected type of the~pair, where $x'$ is
a~bound variable in $P$ referencing the value of the~first element. Usually $x$
and $x'$ will be the~same variable since they both describe the~same value; we
distinguish them here only to point out that $x$ is bound in $N$ and $x'$ is
bound in $P$.

Similarly to the~pair eliminator, the~unit eliminator also binds a~variable $x$
to the~unit given by the~term $M$. The~scope of $x$ is $O$, which is the~type
annotation of $N$.

Although \autoref{def:pseudo-term} mentions the~unit type \1 separately, it is
also an~atomic type. Let us consider what other atomic types can a~given system
have. First, there are all the~familiar types, like the~type of integers $\Int$,
or the~type of Boolean values $\Bool$, or indeed \1 and $\top$. These depend on
the~intended use of the~type system and they are not theoretically interesting.
Conversely, the~second kind of atomic types determines some of the~properties of
the~type system; these types are called \emph{sorts}. Our type systems will use
only one sort, \univ, called \emph{Universe}, representing the~type of types.
These systems will be able to derive the~judgment $\vdash \univ \is{} \univ$,
which states that the~type of types is itself a~type. The~choice of a~single
sort lets us simplify the~implementation of our type system, but it also has
some downsides; when interpreted under the~Curry–Howard correspondence, the~type
system yields an~inconsistent logic, which is a~logic that lets us derive
a~contraction. This, in the~type-theoretic terms, means that every type is
inhabited.

For a~type system to correspond to a~consistent logic, we would have to have at
least two sorts~\citep{hurkens_1995}. \citet{barendregt_1993} introduced a~group
of eight typing systems, known as the~\emph{λ-cube} due to their mutual
relationships, all of which use the~sorts $\star$ and $\square$ related by
the~rule:
\begin{mathpar}
  \inferrule*
  { }
  {\vdash \star \is{} \square}
\end{mathpar}
Another option is to have an~infinite sequence of sorts $\star_0, \star_1,
\dots$ related by the~rule:
\begin{mathpar}
  \inferrule*
  { }
  {\vdash \star_i \is{} \star_{i+1}}
\end{mathpar}

\sectionwithtoc{Pseudo-contexts}

With dependent types in mind, we need to revisit the~semantics of the~judgment
$\Gamma \vdash M \is{} S$. In typing systems, the~list of assumptions $\Gamma$,
henceforth called \emph{context}, contains only type assignments. We, however,
need to make sure that these assignments are well-formed; that is, for every
$x \is{} S$ in $\Gamma$, we want to make sure that $S$ is a~proper type. For
example, we want to reject the~list
\[
  a \is{} \univ, \; f \is{} \dep x b a,
\]
because we do not know the~type of the~variable $b$. A~valid context would be:
\[
  a \is{} \univ, \; b \is{} \univ, \; f \is{} \dep x b a.
\]
Hence, we first define \emph{pseudo-contexts} and then identify the~contexts
within.

\begin{definition}
  A~\emph{pseudo-context} is a~sequence of formulas of the~form
  \[
    x_1 \is{} S_1, \dotsc , x_n \is{} S_n,
  \]
  where $x_1, \dotsc , x_n$ are distinct variables and $S_1, \dotsc, S_n$ are
  pseudo-terms.
\end{definition}

Empty pseudo-context is denoted by $\diamond$, or it is omitted when no
confusion is likely.

\sectionwithtoc{Dependently typed \lc}\label{sec:dtlc}

Using  pseudo-contexts and pseudo-terms, we are able to define a~type-assignment
system, that assigns the~dependent types, and is thus more expressive then
the~simply typed \lc, since we can model the~simple type $S \to T$ by defining
it as $\dep x S T$, where $x \notin \fv T$.

The~rules that identify contexts within pseudo-contexts and terms within
pseudo-terms are mutually recursive. Contexts are identified by the~judgment
$\Gamma \vdash$, defined by the~following rules:
\begin{mathpar}
  \inferrule*
  { }
  {\diamond \vdash}

  \inferrule*
  {\Gamma \vdash \\ \Gamma \vdash S : \univ}
  {\Gamma, x \is{} S \vdash}
\end{mathpar}

Terms are identified by the~judgment $\Gamma \vdash M \is{} S$. First, a rule
that derives the~type of type is type:
\begin{mathpar}
  \inferrule*
  {\Gamma \vdash}
  {\Gamma \vdash \univ \is{} \univ}
\end{mathpar}

In dependently typed \lc the~types are formed by terms, so we have three
\emph{type formation} rules, hence the~\ir{-F} suffix, which state when a~type
former can be applied:
\begin{mathpar}
  \inferrule*[right=$\to$-F]
  {
    \Gamma \vdash S \is{} \univ \\\\
    \Gamma, x \is{} S \vdash T \is{} \univ
  }
  {\Gamma \vdash \dep x S T \is{} \univ}

  \inferrule*[right=$\times$-F]
  {
    \Gamma \vdash S \is{} \univ \\\\
    \Gamma, x \is{} S \vdash T \is{} \univ
  }
  {\Gamma \vdash (x \is{} S) \times T \is{} \univ}

  \inferrule*[right=\1-F]
  {\Gamma \vdash}
  {\Gamma \vdash \1 \is{} \univ}
\end{mathpar}
The~type formation rules make sure that $S$ and $T$ are types, before judging
that their combination is also a~type. Note that with dependent types, we can
use the~value $x$ when judging the~type of $T$.

Next, there are the~introduction and elimination rules for functions and pairs,
which are analogous to their counterparts in the~\nameref{sec:stlc}, except that
they use the~dependent versions of the~types:
\begin{mathpar}
  \inferrule*[right=$\to$-I]
  {
    \Gamma \vdash \dep x S T \is{} \univ \\
    \Gamma, x \is{} S \vdash M \is{} T
  }
  {\Gamma \vdash (\lam {x \is{} S} M) \is{} \dep x S T}

  \inferrule*[right=$\to$-E]
  {
    \Gamma \vdash M \is{} \dep x S T \\\\
    \Gamma \vdash N \is{} S
  }
  {\Gamma \vdash M \: N \is{} T[N/x]}

  \inferrule*[Right=$\times$-I]
  {
    \Gamma \vdash M \is{} S \\\\
    \Gamma \vdash N \is{} T[M/x]
  }
  {\Gamma \vdash \mpair M N \is{} (x \is{} S) \times T}

  \inferrule*[right=$\times$-E]
  {
    \Gamma, z \is{} (x \is{} S) \times T \vdash U \is{} \univ \\
    \Gamma \vdash M \is{} (x \is{} S) \times T \\\\
    \Gamma, x \is{} S, y \is{} T \vdash N \is{} U[(x, y)/z]
  }
  {
    \Gamma \vdash \letpair{(x \is{} S) \times T}[z] x y M [U] N \is{} U[M/z]
  }
\end{mathpar}

The~introduction rule for the~unit type is the~same as the~one in
\nameref{sec:stlc}, but the~elimination rule allows for $U$ to depend on
the~unit:
\begin{mathpar}
  \inferrule*[Right=\1-I]
  {\Gamma \vdash}
  {\Gamma \vdash \munit \is{} \1}

  \inferrule*[right=\1-E]
  {
    \Gamma, x \is{} \1 \vdash U \is{} \univ \\
    \Gamma \vdash M \is{} \1 \\
    \Gamma \vdash N \is{} U[\munit/x]
  }
  {
    \Gamma \vdash \letu [x] M [U] N \is{} U[M/x]
  }
\end{mathpar}

With terms forming types, there is the~possibility of writing the~same type in
different ways. For example, the~following terms all describe the same type:
\begin{mathpar}
  \dep x \Int \Bool \and \dep x {(\lam {y \is{} \univ} y) \: \Int} \Bool \\
  \dep x \Int {(\letpair{(a \is{} \univ) \times \Int} [c] a b {\mpair\Bool{42}}
    [\univ] a)}
\end{mathpar}

To judge the~equivalence of types, we employ the~following rule:
\begin{mathpar}
\inferrule*[right=Conv]
  {
    \Gamma \vdash M \is{} S \\
    \Gamma \vdash S \is{} \univ \\
    \Gamma \vdash T \is{} \univ \\
    S =_\beta T
  }
  {\Gamma \vdash M \is{} T}
\end{mathpar}
If a~term has type $S$ and if $S$ is β-equal to $T$, then the~term has also type
$T$.

As an~example of the~increased expressiveness of dependently typed \lc, we
consider the~type we are now able to assign to the~identity function. To assign
a~type to identity function, we need the~ability to quantify over \univ.
Function $\lam {x \is{} s} x$ is the~identity on type $s$, so if we view $s$ as
a~function parameter, the~term
\[
  \mathtt{id} \defeq \lam {s \is{} \univ} {\lam {x \is{} s} x}
\]
is a~function which, when applied to any type of type \univ, gives the~identity
function over that type. So, for example, we have:
\[
  \mathtt{id} \: \Bool \: \mathtt{true} =_\beta \mathtt{true}.
\]

To derive the~type of $\mathtt{id}$, we need dependent function types: given
derivations of judgments
\begin{mathpar}
  s \is{} \univ \vdash \dep x s s \is{} \univ \and
  s \is{} \univ \vdash (\lam {x \is{} s} x) \is{} \dep x s s
\end{mathpar}
which can be found even with only simple types, we need to combine them using
\ir{$\to$-I} like so:
\begin{mathpar}
  \inferrule*[right=$\to$-I]
  {
    \inferrule*[right=$\to$-F]
    {
      \inferrule*
      {\diamond \vdash}
      {\vdash \univ \is{} \univ} \\
      \inferrule*
      { \vdots }
      {s \is{} \univ \vdash \dep x s s \is{} \univ}
    }
    {\vdash \dep s \univ {\dep x s s} \is{} \univ} \\
    \inferrule*
    { \vdots }
    {s \is{} \univ \vdash (\lam {x \is{} s} x) \is{} \dep x s s}
  }
  {
    \vdash (\lam {s \is{} \univ} {\lam {x \is{} s} x}) \is{}
      \dep s \univ {\dep x s s}
  }
\end{mathpar}