\chapter{Types and Terms}
\label{chap:types-and-terms}

We begin our journey by studying the basics of Lean, starting with terms
(also called expressions) and their types.

Lean's logical foundation is a rich logic called the \emph{calculus of inductive
constructions}, which supports \emph{dependent types}. Lean's logic is
inspired by the \li{λ}-calculus and resembles typed functional programming
languages such as Haskell, OCaml, and Standard ML. Even if you have not been
exposed to these languages, you will recognize many of the concepts from modern
languages (e.g., Python, C++11, Java 8). In a first approximation:
%
\[\text{Lean \texttt{=} functional programming \texttt{+} logic}\]

If your background is in mathematics, you probably already know most of the
key concepts underlying functional programming, sometimes under different
names. For example, the Haskell program
%
\begin{lstlisting}[language=]
fib 0 = 0
fib 1 = 1
fib n = fib (n - 2) + fib (n - 1)
\end{lstlisting}
%
closely matches the mathematical definition
%
\[\text{\textit{fib}(\textit{n})} = \begin{cases}
  \text{0} & \text{if~}\textit{n} = \text{0} \\[-\jot]
  \text{1} & \text{if~}\textit{n} = \text{1} \\[-\jot]
  \textit{fib}\text{(}\textit{n} - \text{2)} + \textit{fib}\text{(}\textit{n} - \text{1)} & \text{if~\textit{n}} \ge \text{2}
\end{cases}\]

In this chapter, we restrict our attention to a fragment without dependent
types, called \emph{simple type theory} (or \emph{higher-order logic}). It
corresponds roughly to the simply typed \li{λ}-calculus
\cite{barendregt-et-al-2013} extended with an equality operator (\li{=}). It is
an abstract, extremely simplified version of a programming language with a
function-calling mechanism that prefigures functional programming.

\section{Types}
\label{sec:types}

\emph{Types} can be basic types such as \li{ℤ}, \li{ℚ}, and \li{Bool} or
total functions \hbox{\li{σ → τ}}, where \li{σ} and \li{τ} are themselves
types. Types indicate which values an expression may evaluate to. They
introduce a discipline that is followed somewhat implicitly in mathematics. In
principle, nothing prevents a mathematician from stating \li{1 ∈ 2}, but a
typing discipline would mark this as the error it likely is.

Semantically, types can be viewed as sets. We would normally define the types
\li{ℤ}, \li{ℚ}, and \li{Bool} so that they faithfully capture the
mathematicians' $\mathbb{Z}$ and $\mathbb{Q}$ and the computer scientists'
Booleans, and similarly for the function arrow (\li{→}). But despite their
similarities, Lean and mathematics are distinct languages. Lean's types may be
\emph{interpreted} as sets, but they are not sets.

\emph{Higher-order types} are types containing \li{→} arrows that are nested on
the left of \li{→}, as in the type \li{(ℤ → ℤ) → ℚ}. Values of such types are
functions that take other functions as arguments. Accordingly, \li{(ℤ → ℤ) → ℚ}
is the type of unary functions that take a function of type \li{ℤ → ℤ} as
argument and that return a value of type \li{ℚ}.

\section{Terms}
\label{sec:terms}

The \emph{terms}, or expressions, of simple type theory consist of
\begin{itemize}
\item \emph{constants}~\li{c};
\item \emph{variables} \li{x};
\item \emph{applications} \li{t u};
\item \emph{anonymous functions} \li{fun x ↦ t} (also called \li{λ}-expressions).
\end{itemize}
%
Above, \li{t} and \li{u} denote arbitrary terms. We can also write
\li{t : σ} to indicate that the term \li{t} has the type \li{σ}.

Let us review the kinds of terms in turn:

\begin{itemize}
\item
A \relax{constant} \li{c : σ} is a symbol of type \li{σ} whose meaning is
fixed in the current global context. For example, an arithmetic theory
might contain constants such as \li{0 : ℤ}, \li{1 : ℤ},
\li{abs : ℤ → ℕ}, \li{square} \li{: ℕ → ℕ}, and \li{prime} {\li{:}} \li{ℕ → Bool}.
Constants include functions (e.g., \li{abs}) and predicates (e.g., \li{prime}).

\item
A \relax{variable} \li{x : σ} is either \emph{bound} or \emph{free}. A bound
variable refers back to the input of an anonymous function \li{fun x : σ ↦ t}
enclosing it. By contrast, a free variable is declared in the local context---a
concept that will be explained below.

\item
An \relax{application} \li{t u}, where \li{t : σ → τ} and \li{u : σ}, is a term
of type \li{τ} denoting the result of applying the function \li{t} to the
argument \li{u}. For example, if \li{t} is \li{abs} and \li{u} is \li{0}, then
the application is \li{abs 0}. No parentheses are needed around the
argument, unless it is a complex term---e.g., \li{prime (abs 0)}.

\item
Given a term \li{t : τ}, an anonymous function \hbox{\li{fun x : σ ↦ t}} denotes the
total function of type \li{σ} \li{→} \li{τ} that maps each input value \li{x}
of type \li{σ} to the body \li{t}, where \li{x} may occur in
\li{t}\nobreak. Thus, \hbox{\li{fun x : ℤ ↦}} \li{square (abs x)} denotes the
function that maps (the value denoted by) \li{0} to (the value denoted by)
\li{square} \hbox{\li{(abs 0)},} that maps \li{1} to \li{square (abs 1)}, and
so on. The variable \li{x} is said to be bound by \li{fun}. Accordingly,
\li{fun} is called a \emph{binder}. For mathematicians, a more familiar syntax
would have been \li{x ↦ square} \li{(abs x)}, without the \li{fun} keyword.
\end{itemize}

Constants and variables look syntactically similar, but they are considered
different. Constants are declared globally, whereas variables are introduced
locally by \li{fun} or some other binder.

Applications and anonymous functions mirror each other: An
anonymous function ``builds'' a function; an application ``destructs''
a function. What happens if we combine the two? If we apply an argument \li{u}
of type \li{σ} to an anonymous function \li{fun x : σ ↦ t[x]}, where \li{t[x]}
represents some term that may contain \li{x}, then we obtain the term \li{t[u]}.
(This is a slightly simplified view. Actually, if \li{t[x]} contains some
binders, the bound variables might have to be renamed to avoid capturing
\li{u}'s free variables. In Lean, this renaming takes place automatically.)
Here are a few examples of applying an anonymous function:
%
\begin{center}
\begin{tabular}{@{}r@{\quad}c@{\quad}l@{}}
\li|(fun n : ℕ ↦ n) 4| & yields & \li|4| \\
\li|(fun n : ℕ ↦ square (square n)) 5| & yields & \li|square (square 5)| \\
\li|(fun y : ℤ ↦ 1) 0| & yields & \li|1| \\
\li|(fun x : ℤ ↦ (fun y : ℤ ↦ x)) 1| & yields & \li|fun y : ℤ ↦ 1|
\end{tabular}
\end{center}

Although our functions are unary (i.e., they take one argument),
we can build \textit{n}-ary functions by nesting \li{fun}s, using an ingenious
technique called \emph{currying}. For example, \li{fun x} \li{:}
\li{σ} \li{↦} \hbox{\li{(fun y}} \li{: τ ↦ x)} denotes the function of type
\li{σ → (τ → σ)} that takes two arguments and returns the first one. Strictly speaking,
\li{σ → (τ →} \hbox{\li{σ)}} takes a single argument and returns a function,
which in turn takes an argument.

Applications work in the same way: If
\li{K := (fun x : ℤ ↦ (fun y : ℤ ↦ x))}, then
\li{K 1 = (fun} \li{y : ℤ ↦ 1)} and \li{(K 1) 0 = 1}. The function \li{K} in
\li{K 1}, which is applied to a single argument, is said to be \emph{partially
applied}, because it can take an additional argument.

Currying is so useful a concept that we will omit most parentheses, writing
%
\begin{center}
\begin{tabular}{@{}r@{\quad}c@{\quad}l@{}}
\li|σ → τ → υ| & for & \li|σ → (τ → υ)| \\
\li|t u v| & for & \li|(t u) v| \\
\hphantom{\li|()|}\li|fun x : σ ↦ fun y : τ ↦ t| & for & \li|fun x : σ ↦ (fun y : τ ↦ t)|\hphantom{\li|,|} \\
\end{tabular}
\end{center}
%
and also
%
\begin{center}
\begin{tabular}{@{}r@{\quad}c@{\quad}l@{}}
\hphantom{\li|,|}\li|fun (x : σ) (y : τ) ↦ t| & for & \li|fun x : σ ↦ fun y : τ ↦ t| \\
\li|fun x y : σ ↦ t| & for & \li|fun (x : σ) (y : σ) ↦ t| \\
\end{tabular}
\end{center}

Moreover, in an anonymous function \li{fun x : σ ↦ t}, we can usually omit the type
annotation \li{: σ}, writing
\begin{center}
\begin{tabular}{@{}r@{\quad}c@{\quad}l@{}}
\li|fun x ↦ t| & for & \li|fun x : σ ↦ t| \\
\end{tabular}
\end{center}
%
Lean will then try to infer the type based on the body \li{t} and on the context
surrounding the anonymous function. Type inference lightens
notations and saves some keystrokes.

In mathematics, it is customary to write binary operators in infix
syntax (e.g., \hbox{\li{x + y}).} Such notations are also possible in Lean, as
syntactic sugar for curried function application (e.g., \li{add x y}).

One way to work with Lean is to declare the types and constants we need using
the \li{opaque} command. Consider the following declarations:

\lstinputlisting[linerange=abfg_def-q]{../lean/LoVe/LoVe01_TypesAndTerms_DemoMaster.lean}
\betweenlistings
\lstinputlisting[linerange=abfg_check-q]{../lean/LoVe/LoVe01_TypesAndTerms_DemoMaster.lean}
%
The first four lines declare four constants (\li{a}, \li{b}, \li{f},
\li{g}), which can be used to form terms. The last two lines use the
\li{#check} command to type-check terms and show their types.
Using traditional
mathematical notations, the term on the last line would be written
%
$\textit{x} \mapsto \textit{g}(\textit{f}(\textit{g}(\textit{a}, \textit{x})), \textit{g}(\textit{x}, \textit{b}))$.
The \li{#} prefix identifies diagnosis commands:\ commands that are useful for
debugging but that we would normally not keep in our Lean files.

%The constants thus introduced have no definition. They are fully unspecified.
%For example, we cannot tell whether \li{a} and \li{b} are equal or not.

\section{Type Checking and Type Inference}
\label{sec:type-checking-and-type-inference}

When Lean parses a term, it checks whether the term is well typed. In the
process, it tries to infer the types of bound variables if those are
omitted---e.g., the type of \li{x} in \li{fun x ↦ square (square x)}.

For simple type theory, type checking and type inference are decidable
problems. Advanced features such as overloading (the possibility to reuse the
same name for several constants---e.g., \li{0 : ℕ} and \li{0 : ℝ}) can lead to
undecidability \cite{pierce-2002}. Lean takes a pragmatic,
computer-science-oriented approach and assumes that numerals \li{0}, \li{1},
\li{2}, \ldots{} are of type \li{ℕ} if several types are possible.

Lean's type system can be expressed as a formal system. A \emph{formal system}
consists of \emph{judgments} and of \emph{derivation rules} for producing
judgments. A typing judgment has the form \li{C ⊢ t : σ} and means that term
\li{t} has type \li{σ} in local context~\hbox{\li{C}.} For example, the judgment
\li{⊢ abs : ℤ → ℕ} states that the constant \li{abs} has type \li{ℤ → ℕ} in
the empty local context.

The local context gives the types of the variables in \li{t} that are not bound
by a~\li{fun}. It is used to keep track of the variables bound by
binders \emph{outside}~\li{t}. If the same variable \li{x} is bound multiple
times, the last occurrence shadows the other ones. For example, the judgment
\li{x : ℤ, y : ℕ, y : ℤ  ⊢ y : ℤ} states that the variable \li{y} has type \li{ℤ} in the local context \li{x : ℤ, y : ℕ, y : ℤ}.

For simple type theory, the typing judgments are produced by four typing rules,
one per kind of term:

\vskip\abovedisplayskip

\centerline{\prftree[r]{\textsc{Cst}\quad if \lic{c} is globally declared with type~\lic|\σ|}
  {\strut\text{\lic{C ⊢ c : σ}}}}

\vskip2\jot

\centerline{\prftree[r]{\textsc{Var}\quad if \lic{x : σ} is the rightmost occurrence of \lic{x} in \lic{C}}
  {\strut\text{\lic{C ⊢ x : σ}}}}

\vskip2\jot

\centerline{\prftree[r]{\textsc{App}}
  {\strut\text{\lic{C ⊢ t : σ → τ}}}
  {\strut\text{\lic{C ⊢ u : σ}}}
  {\strut\text{\lic{C ⊢ t u : τ}}}}

\vskip2\jot

\centerline{\prftree[r]{\textsc{Fun}}
  {\strut\text{\lic|C, x : σ ⊢ t : τ|}}
  {\strut\text{\lic|C ⊢ (fun x : σ ↦ t) : σ → τ|}}}

\vskip\belowdisplayskip

Each rule has zero or more premises (above the horizontal bar), a conclusion
(below the bar), and possibly a side condition (on the right). The premises are
typing judgments, whereas the side conditions are arbitrary mathematical
conditions on the mathematical variables occurring in the rule. To show the
premises, we need to continue performing a derivation upward, as we will see in
a moment. As for the side conditions, we can use the entire arsenal of
mathematics to show that they are true.

The first two rules, labeled \textsc{Cst} and \textsc{Var}, have no premises,
but they have side conditions
that must be satisfied for the rules to apply. The last two rules take one or
two judgments as premises and produce a new judgment. \textsc{Fun} is the only
rule that modifies the local context: As we enter the body~\li{t} of an
anonymous function, we need to record the existence of the bound variable~\li{x}
and its type to be ready when we meet \li{x} in~\li{t}.

We can use this rule system to prove that a given term is well typed by
working our way backwards (i.e., upwards) and applying the rules, building a
\emph{formal derivation} of a typing judgment. Like natural trees, derivation
trees are drawn with the root at the bottom. The derived judgment appears at
the root, and each branch ends with the application of a premise-less rule.
Rule applications are indicated by a horizontal bar and a label. The following
typing derivation establishes that the term \li{fun x : ℤ ↦ abs x} has type
\li{ℤ → ℕ} in an arbitrary local context \li{C}:
%
\begin{gather*}
\prftree[r]{\textsc{Fun}}
  {\prftree[r]{\textsc{App}}
    {\prftree[r]{\textsc{Cst}}
      {\strut\text{\lic{C, x : ℤ ⊢ abs : ℤ → ℕ}}}}
    {\prftree[r]{\textsc{Var}}
      {\strut\text{\lic{C, x : ℤ ⊢ x : ℤ}}}}
    {\strut\text{\lic{C, x : ℤ ⊢ abs x : ℕ}}}}
  {\strut\text{\lic{C ⊢ (fun x : ℤ ↦ abs x) : ℤ → ℕ}}}
\end{gather*}
%
Reading the proof from the root upwards, notice how the local context is
threaded through and how it is extended by the \textsc{Fun} rule. The rule
moves the variable bound by \li{fun} to the local context, making an application
of \textsc{Var} possible further up the tree. If the variable~\li{x} is already
declared in \li{C}, it becomes shadowed by \li{x : ℤ} after entering the
\li{fun} expression.

In summary, the type system consists of derivation rules that can be
(1)~instantiated with arbitrary values for their mathematical variables and
(2)~connected to form derivation trees.

Here is a second example, this time starting with an empty local context:
%
\begin{gather*}
\prftree[r]{\textsc{Fun}}
  {\prftree[r]{\textsc{Fun}}
    {\prftree[r]{\textsc{Var}}
      {\strut\text{\lic{x : ℤ, y : ℤ : ⊢ x : ℤ}}}}
    {\strut\text{\lic{x : ℤ ⊢ (fun y : ℤ ↦ x) : ℤ → ℤ}}}}
  {\strut\text{\lic{\⊢ (fun x : ℤ ↦ fun y : ℤ ↦ x) : ℤ → ℤ → ℤ}}}
\end{gather*}

Both examples so far were well typed. If we start with an ill-typed term, or if
we specify the wrong type or context in the judgment at the root of the
derivation tree, we will find that we cannot complete the derivation. A
derivation constitutes a proof that a term is well typed and has the specified
type in the given context.

The above type system checks only that terms are well typed. It does not check
that types are well formed. For example, given the unary type constructor
\hbox{\li{List},} \hbox{\li{List ℤ}} (the type of lists of integers) is well formed,
whereas \hbox{\li{ℤ List}} and \hbox{\li{List}} \hbox{\li{List}} are ill-formed.
For simple type theory, well-formedness is easy to check: Only declared type
constructors should be used, and each \textit{n}-ary type constructor should be
passed exactly \textit{n}~type arguments.

\section{Type Inhabitation}
\label{sec:type-inhabitation}

Given a type~\li{σ}, the type inhabitation problem consists of finding an
``inhabitant'' of that type---a term of type~\li{σ}---within the empty
local context. It may seem like a
pointless exercise, but as we will see in Chapter~\ref{chap:forward-proofs},
this problem is closely related to that of finding a proof of a proposition.
Seemingly silly exercises of the form ``find a term of type \li{σ}'' are good
practice towards mastery of theorem proving.

Although this problem is in general undecidable, with the right strategy we can
go a long way. To create a term of a given type, start with the placeholder
\li{_} and recursively apply a combination of the following two steps:
%
\begin{itemize}
\item[1.] If the type is of the form \li{σ → τ}, a possible inhabitant is an
  anonymous function, of the form \li{fun x : σ ↦ _}, where \li{_} is a
  placeholder for a missing term of type \li{τ}. Lean will mark \li{_} as an
  error; if you hover over it in Visual Studio Code, a tooltip will show the
  missing term's type as well as any variables declared in the local context.

\item[2.] Given a type \li{σ} (which may be a function type), you can use any
  constant~\li{c} or variable \li{x} of type \li{τ}$_\texttt{1}$ \li{→} \li{⋯}
  \li{→} \li{τ}$_\ttvar{n}$ \li{→} \li{σ} to build a term of type \li{σ}.
  For each argument, you need to put a placeholder, yielding \li{c} \li{_}
  \li{…} \li{_} or \li{x} \li{_} \li{…} \li{_}.
\end{itemize}
%
The placeholders can be eliminated recursively using the same strategy.

As an example, we will apply the strategy to find a term of type
%
\[\hbox{\li{(α → β → γ) → ((β → α) → β) → α → γ}}\]
%
Initially, only step~1 is applicable, with

\begin{center}
\begin{tabular}{@{}r@{\quad}c@{\quad}l@{}}
\li|σ := α → β → γ| & and & \li|τ := ((β → α) → β) → α → γ|
\end{tabular}
\end{center}
(Recall that \li{→} is right-associative.) This results in the term
\li{fun f ↦ _}, which has the right type but has a placeholder left. Since the
argument \li{f} has type \hbox{\li{σ},} a function type, it makes sense to use the name
\li{f} for it. Then we continue recursively with the placeholder, of
type~\li{τ}. Again, only step~1 is possible, so we end up with the term
\li{fun f g ↦ _}, where \li{g} has type \hbox{\li{(β →}} \li{α) → β} and the
placeholder has type \li{α → γ}. A third application of step~1 yields
\hbox{\li{fun f g a ↦ _},} where \li{a} has type~\li{α} and the
placeholder has type~\hbox{\li{γ}.}

At this point, step~1 no longer applies. Let us see if step~2 is possible. The
context surrounding the placeholder contains the following variables:
%
\[\hbox{\ctxt{f} \lic|: α → β → γ,| \,\ctxt{g} \lic|: (β → α) → β,| \,\ctxt{a} \lic|: α|}\]
%
Recall that we are trying to build a term of type \li{γ}. The only variable we
can use to achieve this is \li{f}: It takes two arguments and returns a value
of type~\li{γ}. So we replace the placeholder with the term \li{f _ _}, where
the two new placeholders stand for the two missing arguments. Putting
everything together, we now have the term \li{fun f g a ↦ f _ _}.

Following \li{f}'s type, the placeholders are of type \li{α} and \li{β},
respectively. The first placeholder is easy to fill in, using step~2 again, by
simply supplying \li{a}, of type \li{α}, with no arguments. For the
second placeholder, we apply step~2 with the variable~\hbox{\li{g},}
which is the only source of \li{β}s. Since \li{g} takes an argument, we must
supply a placeholder. This means our current term is \li{fun f g a ↦ f a (g _)}.

We are almost done. The only placeholder left has type \hbox{\li{β →}}
\li{α}, which is \li{g}'s argument type. Applying step~1, we replace the
placeholder with \li{fun b ↦ _}, where \li{_} has type \li{α}. Here, we can
simply supply \li{a}. Our final term is \li{fun f g a ↦ f a (g}
\li{(fun b ↦ a))}.

The above derivation was tedious but deterministic: At each point, either step
1~or~2 was applicable, but not both. In general, this will not always be the
case. For some other types, we might encounter dead ends and need to backtrack.
We might also fail altogether, with nowhere to backtrack to.

\thekeyidea{term}{software}{program}

\section{Summary of New Lean Constructs}

At the end of this and most other chapters, we include a brief summary of the
constructs introduced in the chapter.
Some syntaxes have multiple meanings, which will be introduced gradually.
We refer to \emph{The Lean 4 Manual}
\cite{lean-reference-manual}, the \emph{Theorem Proving in Lean 4}
\cite{theorem-proving-in-lean} tutorial, and the \li{mathlib} documentation%
\footnote{\url{https://leanprover-community.github.io/mathlib4_docs/}} for
details.

\begingroup
\summarysize

\subsection*{Diagnosis Command}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\lic|#check| & checks and prints type of a term \\
\end{xltabular}

\subsection*{Declaration}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\lic|opaque| & declares an unspecified new constant or type \\
\end{xltabular}

\endgroup
