more stuff

[bitonic-mengthesis.git] / docs / background.tex

\documentclass[article, a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage{fixltx2e}
\usepackage{enumitem}
\usepackage[normalem]{ulem}
\usepackage{graphicx}
\usepackage{subcaption}

% Unicode
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
% \usepackage{autofe}

%% -----------------------------------------------------------------------------
%% Fonts
%% \usepackage[osf]{libertine}
%% \usepackage{helvet}
%% \usepackage{lmodern}
%% \IfFileExists{microtype.sty}{\usepackage{microtype}}{}

%% -----------------------------------------------------------------------------
%% Diagrams
% \usepackage{tikz}
% \usetikzlibrary{positioning}
%% \usetikzlibrary{shapes}
%% \usetikzlibrary{arrows}
%% \usepackage{tikz-cd}
%% \usepackage{pgfplots}
\usepackage[all]{xy}

%% -----------------------------------------------------------------------------
%% Symbols
\usepackage[fleqn]{amsmath}
\usepackage{amssymb}
\usepackage{wasysym}
\usepackage{turnstile}
\usepackage{centernot}

%% -----------------------------------------------------------------------------
%% Utils
\usepackage{bussproofs}
\usepackage{umoline}
\usepackage[export]{adjustbox}
\usepackage{multicol}
\usepackage{listings}
\lstset{
  basicstyle=\footnotesize\ttfamily,
  extendedchars=\true,
  inputencoding=utf8x
}

%% -----------------------------------------------------------------------------
%% Bibtex
\usepackage{natbib}

%% Numbering depth
%% \setcounter{secnumdepth}{0}

%% -----------------------------------------------------------------------------
% We will generate all images so they have a width \maxwidth. This means
% that they will get their normal width if they fit onto the page, but
% are scaled down if they would overflow the margins.
\makeatletter
\def\maxwidth{
  \ifdim\Gin@nat@width>\linewidth\linewidth
  \else\Gin@nat@width\fi
}
\makeatother

%% -----------------------------------------------------------------------------
%% Links
\usepackage[
  setpagesize=false, % page size defined by xetex
  unicode=false, % unicode breaks when used with xetex
  xetex
]{hyperref}

\hypersetup{
  breaklinks=true,
  bookmarks=true,
  pdfauthor={Francesco Mazzoli <fm2209@ic.ac.uk>},
  pdftitle={The Paths Towards Observational Equality},
  colorlinks=false,
  pdfborder={0 0 0}
}

% Make links footnotes instead of hotlinks:
% \renewcommand{\href}[2]{#2\footnote{\url{#1}}}

% avoid problems with \sout in headers with hyperref:
\pdfstringdefDisableCommands{\renewcommand{\sout}{}}

\title{The Paths Towards Observational Equality}
\author{Francesco Mazzoli \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{<fm2209@ic.ac.uk>}}}
\date{December 2012}

\begin{document}

\maketitle

\setlength{\tabcolsep}{12pt}

The marriage between programming and logic has been a very fertile one.  In
particular, since the simply typed lambda calculus (STLC), a number of type
systems have been devised with increasing expressive power.

In the next sections I will give a very brief overview of STLC, and then
describe how to augment it to reach the theory I am interested in,
Inutitionistic Type Theory (ITT), also known as Martin-L\"{o}f Type Theory after
its inventor.  The exposition is quite dense since there is a lot of material to
cover, for a more complete treatment of the material the reader can refer to
\citep{Thompson1991, Pierce2002}.

I will then explain why equality has been a tricky business in these theories,
and talk about the various attempts have been made to make the situation better.
One interesting development has recently emerged: Observational Type theory.  I
propose to explore the ways to turn these ideas into useful practices for
programming and theorem proving.

\section{Simple and not-so-simple types}

\subsection{Untyped $\lambda$-calculus}

Along with Turing's machines, the earliest attempts to formalise computation
lead to the $\lambda$-calculus \citep{Church1936}.  This early programming
language encodes computation with a minimal sintax and most notably no `data'
in the traditional sense, but just functions.

The syntax of $\lambda$-terms consists of just three things: variables,
abstractions, and applications:

\newcommand{\appsp}{\hspace{0.07cm}}
\newcommand{\app}[2]{#1\appsp#2}
\newcommand{\absspace}{\hspace{0.03cm}}
\newcommand{\abs}[2]{\lambda #1\absspace.\absspace#2}
\newcommand{\termt}{t}
\newcommand{\termm}{m}
\newcommand{\termn}{n}
\newcommand{\termp}{p}
\newcommand{\termf}{f}
\newcommand{\separ}{\ \ |\ \ }
\newcommand{\termsyn}{\mathit{term}}
\newcommand{\axname}[1]{\textbf{#1}}
\newcommand{\axdesc}[2]{\axname{#1} \fbox{$#2$}}
\newcommand{\lcsyn}[1]{\mathrm{\underline{#1}}}

\begin{center}
\axname{syntax}
$$
\begin{array}{rcl}
  \termsyn & ::= & x \separ (\abs{x}{\termsyn}) \separ (\app{\termsyn}{\termsyn}) \\
         x & \in & \text{Some enumerable set of symbols, e.g.}\ \{x, y, z, \dots , x_1, x_2, \dots\}
\end{array}
$$
\end{center}


% I will omit parethesis in the usual manner. %TODO explain how

I will use $\termt,\termm,\termn,\dots$ to indicate a generic term, and $x,y$
for variables.  I will also assume that all variable names in a term are unique
to avoid problems with name capturing.  Intuitively, abstractions
($\abs{x}{\termt}$) introduce functions with a named parameter ($x$), and
applications ($\app{\termt}{\termm}$) apply a function ($\termt$) to an argument
($\termm$).

The `applying' is more formally explained with a reduction rule:

\newcommand{\bred}{\leadsto}
\newcommand{\bredc}{\bred^*}

\begin{center}
\axdesc{reduction}{\termsyn \bred \termsyn}
$$\app{(\abs{x}{\termt})}{\termm} \bred \termt[\termm ]$$
\end{center}

Where $\termt[\termm ]$ expresses the operation that substitutes all
occurrences of $x$ with $\termm$ in $\termt$.  In the future, I will use
$[\termt]$ as an abbreviation for $[\termt ]$.  In the systems presented, the
$\bred$ relation also includes reduction of subterms, for example if $\termt
\bred \termm$ then $\app{\termt}{\termn} \bred \app{\termm}{\termn}$, and so on.

% % TODO put the trans closure

These few elements are of remarkable expressiveness, and in fact Turing
complete.  As a corollary, we must be able to devise a term that reduces forever
(`loops' in imperative terms):
\[
  \app{(\abs{x}{\app{x}{x}})}{(\abs{x}{\app{x}{x}})} \bred \app{(\abs{x}{\app{x}{x}})}{(\abs{x}{\app{x}{x}})} \bred \dotsb
\]
Terms that can be reduced only a finite number of times (the non-looping ones)
are said to be \emph{normalising}, and the `final' term is called \emph{normal
  form}.  These concepts (reduction and normal forms) will run through all the
material analysed.

\subsection{The simply typed $\lambda$-calculus}

\newcommand{\tya}{A}
\newcommand{\tyb}{B}
\newcommand{\tyc}{C}

One way to `discipline' $\lambda$-terms is to assign \emph{types} to them, and
then check that the terms that we are forming make sense given our typing rules
\citep{Curry1934}.

We wish to introduce rules of the form $\Gamma \vdash \termt : \tya$, which
reads `in context $\Gamma$, term $\termt$ has type $\tya$'.

The syntax for types is as follows:

\newcommand{\tyarr}{\to}
\newcommand{\tysyn}{\mathit{type}}
\newcommand{\ctxsyn}{\mathit{context}}
\newcommand{\emptyctx}{\cdot}

\begin{center}
  \axname{syntax}
   $$\tysyn ::= x \separ \tysyn \tyarr \tysyn$$
\end{center}

I will use $\tya,\tyb,\dots$ to indicate a generic type.

A context $\Gamma$ is a map from variables to types.  We use the notation
$\Gamma; x : \tya$ to augment it, and to `extract' pairs from it.

Predictably, $\tya \tyarr \tyb$ is the type of a function from $\tya$ to
$\tyb$.  We need to be able to decorate our abstractions with
types\footnote{Actually, we don't need to: computers can infer the right type
  easily, but that is another story.}:
\begin{center}
  \axname{syntax}
   $$\termsyn ::= x \separ (\abs{x : \tysyn}{\termsyn}) \separ (\app{\termsyn}{\termsyn})$$
\end{center}
Now we are ready to give the typing judgements:

\begin{center}
  \axdesc{typing}{\Gamma \vdash \termsyn : \tysyn}

  \vspace{0.5cm}

  \begin{tabular}{c c c}
    \AxiomC{}
    \UnaryInfC{$\Gamma; x : \tya \vdash x : \tya$}
    \DisplayProof
    &
    \AxiomC{$\Gamma; x : \tya \vdash \termt : \tyb$}
    \UnaryInfC{$\Gamma \vdash \abs{x : \tya}{\termt} : \tya \tyarr \tyb$}
    \DisplayProof
  \end{tabular}

  \vspace{0.5cm}

  \begin{tabular}{c}
    \AxiomC{$\Gamma \vdash \termt : \tya \tyarr \tyb$}
    \AxiomC{$\Gamma \vdash \termm : \tya$}
    \BinaryInfC{$\Gamma \vdash \app{\termt}{\termm} : \tyb$}
    \DisplayProof
  \end{tabular}
\end{center}

This typing system takes the name of `simply typed lambda calculus' (STLC),
and enjoys a number of properties.  Two of them are expected in most type
systems: %TODO add credit to pierce
\begin{description}
\item[Progress] A well-typed term is not stuck - either it is a value or it can
  take a step according to the evaluation rules.  With `value' we mean a term
  whose subterms (including itself) don't appear to the left of the $\bred$
  relation.
\item[Preservation] If a well-typed term takes a step of evaluation, then the
  resulting term is also well typed.
\end{description}

However, STLC buys us much more: every well-typed term
is normalising.  It is easy to see that we can't fill the blanks if we want to
give types to the non-normalising term shown before:
\begin{equation*}
  \app{(\abs{x : ?}{\app{x}{x}})}{(\abs{x : ?}{\app{x}{x}})}
\end{equation*}

\newcommand{\lcfix}[2]{\mathsf{fix} \appsp #1\absspace.\absspace #2}

This makes the STLC Turing incomplete.  We can recover the ability to loop by
adding a combinator that recurses:
$$
  \termsyn ::= \dots \separ  \lcfix{x : \tysyn}{\termsyn}
$$
\begin{center}
  \begin{prooftree}
    \AxiomC{$\Gamma;x : \tya \vdash \termt : \tya$}
    \UnaryInfC{$\Gamma \vdash \lcfix{x : \tya}{\termt} : \tya$}
  \end{prooftree}
\end{center}
$$
  \lcfix{x : \tya}{\termt} \bred \termt[(\lcfix{x : \tya}{\termt}) ]
$$

However, we will keep STLC without such a facility. In the next section we shall
see why that is preferable for our needs.

\subsection{The Curry-Howard correspondence}
\label{sec:curry-howard}

\newcommand{\lcunit}{\mathsf{\langle\rangle}}

It turns out that the STLC can be seen a natural deduction system for
propositional logic.  Terms are proofs, and their types are the propositions
they prove.  This remarkable fact is known as the Curry-Howard correspondence,
or isomorphism.

The `arrow' ($\to$) type corresponds to implication.  If we wished to
prove that $(\tya \tyarr \tyb) \tyarr (\tyb \tyarr \tyc) \tyarr (\tya
\tyarr \tyc)$, all we need to do is to devise a $\lambda$-term that has the
correct type:
\begin{equation*}
  \abs{f : (\tya \tyarr \tyb)}{\abs{g : (\tyb \tyarr \tyc)}{\abs{x : \tya}{\app{g}{(\app{f}{x})}}}}
\end{equation*}
That is, function composition.  We might want extend our bare lambda calculus
with a couple of terms to make our natural deduction more pleasant to use.  For
example, tagged unions (\texttt{Either} in Haskell) are disjunctions, and tuples
(or products) are conjunctions.  We also want to be able to express falsity, and
that is done by introducing a type inhabited by no terms.  If evidence of such a
type is presented, then we can derive any type, which expresses absurdity.
Conversely, $\top$ is the type with just one trivial element, $\lcunit$.

\newcommand{\lcinl}{\mathsf{inl}\appsp}
\newcommand{\lcinr}{\mathsf{inr}\appsp}
\newcommand{\lccase}[3]{\lcsyn{case}\appsp#1\appsp\lcsyn{of}\appsp#2\appsp#3}
\newcommand{\lcfst}{\mathsf{fst}\appsp}
\newcommand{\lcsnd}{\mathsf{snd}\appsp}
\newcommand{\orint}{\vee I_{1,2}}
\newcommand{\orintl}{\vee I_{1}}
\newcommand{\orintr}{\vee I_{2}}
\newcommand{\orel}{\vee E}
\newcommand{\andint}{\wedge I}
\newcommand{\andel}{\wedge E_{1,2}}
\newcommand{\botel}{\bot E}
\newcommand{\lcabsurd}{\mathsf{absurd}\appsp}
\newcommand{\lcabsurdd}[1]{\mathsf{absurd}_{#1}\appsp}


\begin{center}
  \axname{syntax}
  $$
  \begin{array}{rcl}
    \termsyn & ::= & \dots \\
             &  |  & \lcinl \termsyn \separ \lcinr \termsyn \separ \lccase{\termsyn}{\termsyn}{\termsyn} \\
             &  |  & (\termsyn , \termsyn) \separ \lcfst \termsyn \separ \lcsnd \termsyn \\
             &  |  & \lcunit \\
    \tysyn & ::= & \dots \separ \tysyn \vee \tysyn \separ \tysyn \wedge \tysyn \separ \bot \separ \top
  \end{array}
  $$
\end{center}
\begin{center}
  \axdesc{typing}{\Gamma \vdash \termsyn : \tysyn}
  \begin{prooftree}
    \AxiomC{$\Gamma \vdash \termt : \tya$}
    \RightLabel{$\orint$}
    \UnaryInfC{$\Gamma \vdash \lcinl \termt : \tya \vee \tyb$}
    \noLine
    \UnaryInfC{$\Gamma \vdash \lcinr \termt : \tyb \vee \tya$}
  \end{prooftree}
  \begin{prooftree}
    \AxiomC{$\Gamma \vdash \termt : \tya \vee \tyb$}
    \AxiomC{$\Gamma \vdash \termm : \tya \tyarr \tyc$}
    \AxiomC{$\Gamma \vdash \termn : \tyb \tyarr \tyc$}
    \RightLabel{$\orel$}
    \TrinaryInfC{$\Gamma \vdash \lccase{\termt}{\termm}{\termn} : \tyc$}
  \end{prooftree}

  \begin{tabular}{c c}
    \AxiomC{$\Gamma \vdash \termt : \tya$}
    \AxiomC{$\Gamma \vdash \termm : \tyb$}
    \RightLabel{$\andint$}
    \BinaryInfC{$\Gamma \vdash (\tya , \tyb) : \tya \wedge \tyb$}
    \DisplayProof
    &
    \AxiomC{$\Gamma \vdash \termt : \tya \wedge \tyb$}
    \RightLabel{$\andel$}
    \UnaryInfC{$\Gamma \vdash \lcfst \termt : \tya$}
    \noLine
    \UnaryInfC{$\Gamma \vdash \lcsnd \termt : \tyb$}
    \DisplayProof
  \end{tabular}

  \vspace{0.5cm}

  \begin{tabular}{c c}
    \AxiomC{$\Gamma \vdash \termt : \bot$}
    \RightLabel{$\botel$}
    \UnaryInfC{$\Gamma \vdash \lcabsurdd{\tya} \termt : \tya$}
    \DisplayProof
    &
    \AxiomC{}
    \RightLabel{$\top I$}
    \UnaryInfC{$\Gamma \vdash \lcunit : \top$}
    \DisplayProof
  \end{tabular}
\end{center}
\begin{center}
  \axdesc{reduction}{\termsyn \bred \termsyn}
  \begin{eqnarray*}
    \lccase{(\lcinl \termt)}{\termm}{\termn} & \bred & \app{\termm}{\termt} \\
    \lccase{(\lcinr \termt)}{\termm}{\termn} & \bred & \app{\termn}{\termt} \\
    \lcfst (\termt , \termm)                 & \bred & \termt \\
    \lcsnd (\termt , \termm)                 & \bred & \termm
  \end{eqnarray*}
\end{center}

With these rules, our STLC now looks remarkably similar in power and use to the
natural deduction we already know.  $\neg A$ can be expressed as $A \tyarr
\bot$.  However, there is an important omission: there is no term of the type $A
\vee \neg A$ (excluded middle), or equivalently $\neg \neg A \tyarr A$ (double
negation), or indeed any term with a type equivalent to those.

This has a considerable effect on our logic and it's no coincidence, since there
is no obvious computational behaviour for laws like the excluded middle.
Theories of this kind are called \emph{intuitionistic}, or \emph{constructive},
and all the systems analysed will have this characteristic since they build on
the foundation of the STLC\footnote{There is research to give computational
  behaviour to classical logic, but we will not touch those subjects.}.

Finally, going back to our $\mathsf{fix}$ combinator, it's now easy to see how
we would want to exclude such a thing if we want to use STLC as a logic, since
it allows us to prove everything: $(\lcfix{x : \tya}{x}) : \tya$ clearly works
for any $A$!  This is a crucial point: in general we wish to have systems that
do not let the user devise a term of type $\bot$, otherwise our logic will be
unsound\footnote{Obviously such a term can be present under a $\lambda$.}.

\subsection{Extending the STLC}

\newcommand{\lctype}{\mathsf{Type}}
\newcommand{\lcite}[3]{\lcsyn{if}\appsp#1\appsp\lcsyn{then}\appsp#2\appsp\lcsyn{else}\appsp#3}
\newcommand{\lcbool}{\mathsf{Bool}}
\newcommand{\lcforallz}[2]{\forall #1 \absspace.\absspace #2}
\newcommand{\lcforall}[3]{(#1 : #2) \tyarr #3}
\newcommand{\lcexists}[3]{\exists #1 : #2 \absspace.\absspace #3}

The STLC can be made more expressive in various ways.  Henk Barendregt
succinctly expressed geometrically how we can expand our type system:

\begin{equation*}
\xymatrix@!0@=1.5cm{
  & \lambda\omega \ar@{-}[rr]\ar@{-}'[d][dd]
  & & \lambda C \ar@{-}[dd]
  \\
  \lambda2 \ar@{-}[ur]\ar@{-}[rr]\ar@{-}[dd]
  & & \lambda P2 \ar@{-}[ur]\ar@{-}[dd]
  \\
  & \lambda\underline\omega \ar@{-}'[r][rr]
  & & \lambda P\underline\omega
  \\
  \lambda{\to} \ar@{-}[rr]\ar@{-}[ur]
  & & \lambda P \ar@{-}[ur]
}
\end{equation*}
Here $\lambda{\to}$, in the bottom left, is the STLC.  From there can move along
3 dimensions:
\begin{description}
\item[Terms depending on types (towards $\lambda{2}$)] In other words, we can
  quantify over types in our type signatures: $(\abs{A : \lctype}{\abs{x :
      A}{x}}) : \lcforallz{A}{A \tyarr A}$.  The first and most famous instance
  of this idea has been System F.  This gives us a form of polymorphism and has
  been wildly successful, also thanks to a well known inference algorithm for a
  restricted version of System F known as Hindley-Milner.  Languages like
  Haskell and SML are based on this discipline.
\item[Types depending on types (towards $\lambda{\underline{\omega}}$)] In other
  words, we have type operators: $(\abs{A : \lctype}{\abs{R : \lctype}{(A \to R) \to R}}) : \lctype \to \lctype \to \lctype$.
\item[Types depending on terms (towards $\lambda{P}$)] Also known as `dependent
  types', give great expressive power: $(\abs{x : \lcbool}{\lcite{x}{\mathbb{N}}{\mathbb{Q}}}) : \lcbool \to \lctype$.
\end{description}

All the systems preserve the properties that make the STLC well behaved (some of
which I haven't mentioned yet).  The system we are going to focus on,
Intuitionistic Type Theory, has all of the above additions, and thus would sit
where $\lambda{C}$ sits in the `$\lambda$-cube' above.

\section{Intuitionistic Type Theory and dependent types}

\newcommand{\lcset}[1]{\mathsf{Type}_{#1}}
\newcommand{\lcsetz}{\mathsf{Type}}
\newcommand{\defeq}{\equiv}

\subsection{A Bit of History}

Logic frameworks and programming languages based on type theory have a long
history.  Per Martin-L\"{o}f described the first version of his theory in 1971,
but then revised it since the original version was too impredicative and thus
inconsistent\footnote{In the early version $\lcsetz : \lcsetz$, see section
  \ref{sec:core-tt} for an explanation on why this causes problems.}.  For this
reason he gave a revised and consistent definition later \citep{Martin-Lof1984}.

A related development is the one of the polymorphic $\lambda$-calculus, and
specifically the previously mentioned System F, which was invented independently
by Girard and Reynolds.  An overview can be found in \citep{Reynolds1994}.  The
surprising fact is that while System F is impredicative it is still consistent
and strongly normalising.  \cite{Coquand1986} Huet further extended this line of
work with the Calculus of Constructions (CoC).

\subsection{A Core Type Theory}
\label{sec:core-tt}

The calculus I present follows the exposition in \citep{Thompson1991}, and as
said previously is quite close to the original formulation of predicative ITT as
found in \citep{Martin-Lof1984}.

\begin{center}
  \axname{syntax}
  \begin{eqnarray*}
  \termsyn & ::= & x \\
         &  |  & \lcforall{x}{\termsyn}{\termsyn} \separ \abs{x : \termsyn}{\termsyn} \separ \app{\termsyn}{\termsyn} \\
         &  |  & \lcexists{x}{\termsyn}{\termsyn} \separ (\termsyn , \termsyn)_{x.\termsyn} \separ \lcfst \termsyn \separ \lcsnd \termsyn \\
         &  |  & \bot \separ \lcabsurd_{\termsyn} \termsyn \\
         &  |  & \lcset{n} \\
   n     & \in & \mathbb{N}
 \end{eqnarray*}

  \axdesc{typing}{\Gamma \vdash \termsyn : \termsyn}

  \vspace{0.5cm}

  \begin{tabular}{c c c}
    \AxiomC{}
    \RightLabel{var}
    \UnaryInfC{$\Gamma;x : \tya \vdash x : \tya$}
    \DisplayProof
    &
    \AxiomC{$\Gamma \vdash \termt : \bot$}
    \UnaryInfC{$\Gamma \vdash \lcabsurdd{\tya} \termt : \tya$}
    \DisplayProof
    &
    \AxiomC{$\Gamma \vdash \termt : \tya$}
    \AxiomC{$\tya \defeq \tyb$}
    \BinaryInfC{$\Gamma \vdash \termt : \tyb$}
    \DisplayProof
  \end{tabular}

  \vspace{0.5cm}

  \begin{tabular}{c c}
    \AxiomC{$\Gamma;x : \tya \vdash \termt : \tya$}
    \UnaryInfC{$\Gamma \vdash \abs{x : \tya}{\termt} : \lcforall{x}{\tya}{\tyb}$}
    \DisplayProof
    &
    \AxiomC{$\Gamma \vdash \termt : \lcforall{x}{\tya}{\tyb}$}
    \AxiomC{$\Gamma \vdash \termm : \tya$}
    \BinaryInfC{$\Gamma \vdash \app{\termt}{\termm} : \tyb[\termm ]$}
    \DisplayProof
  \end{tabular}

  \vspace{0.5cm}

  \begin{tabular}{c c}
    \AxiomC{$\Gamma \vdash \termt : \tya$}
    \AxiomC{$\Gamma \vdash \termm : \tyb[\termt ]$}
    \BinaryInfC{$\Gamma \vdash (\termt, \termm)_{x.\tyb} : \lcexists{x}{\tya}{\tyb}$}
    \DisplayProof
    &
    \AxiomC{$\Gamma \vdash \termt: \lcexists{x}{\tya}{\tyb}$}
    \UnaryInfC{$\hspace{0.7cm} \Gamma \vdash \lcfst \termt : \tya \hspace{0.7cm}$}
    \noLine
    \UnaryInfC{$\Gamma \vdash \lcsnd \termt : \tyb[\lcfst \termt ]$}
    \DisplayProof
  \end{tabular}

  \vspace{0.5cm}

  \begin{tabular}{c c}
    \AxiomC{}
    \UnaryInfC{$\Gamma \vdash \lcset{n} : \lcset{n + 1}$}
    \DisplayProof
    &
    \AxiomC{$\Gamma \vdash \tya : \lcset{n}$}
    \AxiomC{$\Gamma; x : \tya \vdash \tyb : \lcset{m}$}
    \BinaryInfC{$\Gamma \vdash \lcforall{x}{\tya}{\tyb} : \lcset{n \sqcup m}$}
    \noLine
    \UnaryInfC{$\Gamma \vdash \lcexists{x}{\tya}{\tyb} : \lcset{n \sqcup m}$}
    \DisplayProof
  \end{tabular}

  \vspace{0.5cm}

  \axdesc{reduction}{\termsyn \bred \termsyn}
  \begin{eqnarray*}
    \app{(\abs{x}{\termt})}{\termm} & \bred & \termt[\termm ] \\
    \lcfst (\termt, \termm) & \bred & \termt \\
    \lcsnd (\termt, \termm) & \bred & \termm
  \end{eqnarray*}
\end{center}

There are a lot of new factors at play here. The first thing to notice is that
the separation between types and terms is gone.  All we have is terms, that
include both values (terms of type $\lcset{0}$) and types (terms of type
$\lcset{n}$, with $n > 0$).  This change is reflected in the typing rules.
While in the STLC values and types are kept well separated (values never go
`right of the colon'), in ITT types can freely depend on values.

This relation is expressed in the typing rules for $\tyarr$ and $\exists$: if a
function has type $\lcforall{x}{\tya}{\tyb}$, $\tyb$ can depend on $x$.
Examples will make this clearer once some base types are added in section
\ref{sec:base-types}.

$\tyarr$ and $\exists$ are at the core of the machinery of ITT:

\begin{description}
\item[`forall' ($\tyarr$)] is a generalisation of $\tyarr$ in the STLC and
  expresses universal quantification in our logic.  It is often written with a
  syntax closer to logic, e.g. $\forall x : \mathsf{Bool}. \dotsb$.  In the
  literature this is also known as `dependent product' and shown as $\Pi$,
  following the interpretation of functions as infinitary products. We will just
  call it `dependent function', reserving `product' for $\exists$.

\item[`exists' ($\exists$)] is a generalisation of $\wedge$ in the extended
  STLC of section \ref{sec:curry-howard}, and thus we will call it `dependent
  product'.  Like $\wedge$, it is formed by providing a pair of things.  In our
  logic, it represents existential quantification.

  For added confusion, in the literature that calls forall $\Pi$, $\exists$ is
  often named `dependent sum' and shown as $\Sigma$.  This is following the
  interpretation of $\exists$ as a generalised, infinitary $\vee$, where the
  first element of the pair is the `tag' that decides which type the second
  element will have.
\end{description}

Another thing to notice is that types are very `first class': we are free to
create functions that accept and return types.  For this reason we $\defeq$ as
the smallest equivalence relation extending $\bredc$, where $\bredc$ is the
reflexive transitive closure of $\bred$; and we treat types that are equal
according to $\defeq$ as the same.  Another way of seeing $\defeq$ is this: when
we want to compare two types for equality, we reduce them as far as possible and
then check if they are equal\footnote{Note that when comparing terms we do it up
  to $\alpha$-renaming.  That is, we do not consider relabelling of variables as
  a difference - for example $\abs{x : A}{x} \defeq \abs{y : A}{y}$.}.  This
works since not only each term has a normal form (ITT is strongly normalising),
but the normal form is also unique; or in other words $\bred$ is confluent (if
$\termt \bredc \termm$ and $\termt \bredc \termn$, then $\termm \bredc \termp$
and $\termn \bredc \termp$).  This measure makes sure that, for instance,
$\app{(\abs{x : \lctype}{x})}{\lcbool} \defeq \lcbool$.  The theme of equality
is central and will be analysed better later.

The theory presented is \emph{stratified}.  We have a hierarchy of types
$\lcset{0} : \lcset{1} : \lcset{2} : \dots$, so that there is no `type of all
types', and our theory is predicative.  The layers of the hierarchy are called
`universes'.  $\lcsetz : \lcsetz$ ITT is inconsistent due to Girard's paradox
\citep{Hurkens1995}, and thus loses its well-behavedness.  Some impredicativity
sometimes has its place, either because the theory retain good properties
(normalization, consistency, etc.) anyway, like in System F and CoC; or because
we are at a stage at which we do not care - we will see instances of the last
motivation later.  Moreover, universes can be inferred mechanically
\citep{Pollack1990}. It is also convenient to have a \emph{cumulative} theory,
where $\lcset{n} : \lcset{m}$ iff $n < m$.  We eschew these measures to keep the
presentation simple.

Lastly, the theory I present is fully explicit in the sense that the user has to
specify every type when forming abstractions, products, etc.  This can be a
great burden if one wants to use the theory directly.  Complete inference is
undecidable (which is hardly surprising considering the role that types play)
but partial inference (also called `bidirectional type checking' in this
context) in the style of \cite{Pierce2000} will have to be deployed in a
practical system.  When showing examples types will be omitted when this can be
done without loss of clarity, for example $\abs{x}{x}$ in place of $\abs{A :
  \lcsetz}{\abs{x : A}{x}}$.

Note that the Curry-Howard correspondence runs through ITT as it did with the
STLC with the difference that ITT corresponds to an higher order propositional
logic.

% TODO describe abbreviations somewhere
% I will use various abbreviations:
% \begin{itemize}
%   \item $\lcsetz$ for $\lcset{0}$
%   \item $\tya \tyarr \tyb$ for $\lcforall{-}{\tya}{\tyb}$, when $\tyb$ does not
%     depend on the value of type $\tya$
%   \item $(

\subsection{Base Types}
\label{sec:base-types}

\newcommand{\lctrue}{\mathsf{true}}
\newcommand{\lcfalse}{\mathsf{false}}
\newcommand{\lcw}[3]{\mathsf{W} #1 : #2 \absspace.\absspace #3}
\newcommand{\lcnode}[4]{#1 \lhd_{#2 . #3} #4}
\newcommand{\lcnodez}[2]{#1 \lhd #2}
\newcommand{\lcited}[5]{\lcsyn{if}\appsp#1/#2\appsp.\appsp#3\appsp\lcsyn{then}\appsp#4\appsp\lcsyn{else}\appsp#5}
\newcommand{\lcrec}[4]{\lcsyn{rec}\appsp#1/#2\appsp.\appsp#3\appsp\lcsyn{with}\appsp#4}
\newcommand{\lcrecz}[2]{\lcsyn{rec}\appsp#1\appsp\lcsyn{with}\appsp#2}
\newcommand{\AxiomL}[1]{\Axiom$\fCenter #1$}
\newcommand{\UnaryInfL}[1]{\UnaryInf$\fCenter #1$}

While the ITT presented is a fairly complete logic, it is not that useful for
programming.  If we wish to make it better, we can add some base types to
represent the data structures we know and love, such as numbers, lists, and
trees.  Apart from some unsurprising data types, we introduce $\mathsf{W}$, a
very general tree-like structure useful to represent inductively defined types.

\begin{center}
  \axname{syntax}
  \begin{eqnarray*}
  \termsyn & ::= & \dots \\
           &  |  & \top \separ \lcunit \\
           &  |  & \lcbool \separ \lctrue \separ \lcfalse \separ \lcited{\termsyn}{x}{\termsyn}{\termsyn}{\termsyn} \\
           &  |  & \lcw{x}{\termsyn}{\termsyn} \separ \lcnode{\termsyn}{x}{\termsyn}{\termsyn} \separ \lcrec{\termsyn}{x}{\termsyn}{\termsyn}
 \end{eqnarray*}

  \axdesc{typing}{\Gamma \vdash \termsyn : \termsyn}

  \vspace{0.5cm}

  \begin{tabular}{c c c}
    \AxiomC{}
    \UnaryInfC{$\hspace{0.2cm}\Gamma \vdash \top : \lcset{0} \hspace{0.2cm}$}
    \noLine
    \UnaryInfC{$\Gamma \vdash \lcbool : \lcset{0}$}
    \DisplayProof
    &
    \AxiomC{}
    \UnaryInfC{$\Gamma \vdash \lcunit : \top$}
    \DisplayProof
    &
    \AxiomC{}
    \UnaryInfC{$\Gamma \vdash \lctrue : \lcbool$}
    \noLine
    \UnaryInfC{$\Gamma \vdash \lcfalse : \lcbool$}
    \DisplayProof
  \end{tabular}

  \vspace{0.5cm}

  \begin{tabular}{c}
    \AxiomC{$\Gamma \vdash \termt : \lcbool$}
    \AxiomC{$\Gamma \vdash \termm : \tya[\lctrue]$}
    \AxiomC{$\Gamma \vdash \termn : \tya[\lcfalse]$}
    \TrinaryInfC{$\Gamma \vdash \lcited{\termt}{x}{\tya}{\termm}{\termn} : \tya[\termt]$}
    \DisplayProof
  \end{tabular}

  \vspace{0.5cm}

  \begin{tabular}{c}
    \AxiomC{$\Gamma \vdash \tya : \lcset{n}$}
    \AxiomC{$\Gamma; x : \tya \vdash \tyb : \lcset{m}$}
    \BinaryInfC{$\Gamma \vdash \lcw{x}{\tya}{\tyb} : \lcset{n \sqcup m}$}
    \DisplayProof
  \end{tabular}

  \vspace{0.5cm}

  \begin{tabular}{c}
    \AxiomC{$\Gamma \vdash \termt : \tya$}
    \AxiomC{$\Gamma \vdash \termf : \tyb[\termt ] \tyarr \lcw{x}{\tya}{\tyb}$}
    \BinaryInfC{$\Gamma \vdash \lcnode{\termt}{x}{\tyb}{\termf} : \lcw{x}{\tya}{\tyb}$}
    \DisplayProof
  \end{tabular}

  \vspace{0.5cm}

  \begin{tabular}{c}
    \AxiomC{$\Gamma \vdash \termt: \lcw{x}{\tya}{\tyb}$}
    \noLine
    \UnaryInfC{$\Gamma \vdash \lcforall{\termm}{\tya}{\lcforall{\termf}{(\tyb[\termm] \tyarr \lcw{x}{\tya}{\tyb})}{(\lcforall{\termn}{\tyb[\termm]}{\tyc[\app{\termf}{\termn}]}) \tyarr \tyc[\lcnodez{\termm}{\termf}]}}$}
    \UnaryInfC{$\Gamma \vdash \lcrec{\termt}{x}{\tyc}{\termp} : \tyc[\termt]$}
    \DisplayProof
  \end{tabular}

  \vspace{0.5cm}

  \axdesc{reduction}{\termsyn \bred \termsyn}
  \begin{eqnarray*}
    \lcited{\lctrue}{x}{\tya}{\termt}{\termm} & \bred & \termt \\
    \lcited{\lcfalse}{x}{\tya}{\termt}{\termm} & \bred & \termm \\
    \lcrec{\lcnodez{\termt}{\termf}}{x}{\tya}{\termp} & \bred & \app{\app{\app{\termp}{\termt}}{\termf}}{(\abs{\termm}{\lcrec{\app{f}{\termm}}{x}{\tya}{\termp}})}
  \end{eqnarray*}
\end{center}

The introduction and elimination for $\top$ and $\lcbool$ are unsurprising.
Note that in the $\lcite{\dotsb}{\dotsb}{\dotsb}$ construct the type of the
branches are dependent on the value of the conditional.

The rules for $\mathsf{W}$, on the other hand, are quite an eyesore.  The idea
behind $\mathsf{W}$ types is to build up `trees' where shape of the number of
`children' of each node is dependent on the value in the node.  This is
captured by the $\lhd$ constructor, where the argument on the left is the value,
and the argument on the right is a function that returns a child for each
possible value of $\tyb[\text{node value}]$, if $\lcw{x}{\tya}{\tyb}$.  The
recursor $\lcrec{\termt}{x}{\tyc}{\termp}$ uses $p$ to inductively prove that
$\tyc[\termt]$ holds.

\subsection{Some examples}

Now we can finally provide some meaningful examples.  Apart from omitting types,
I will also use some abbreviations:
\begin{itemize}
  \item $\_\mathit{operator}\_$ to define infix operators
  \item $\abs{x\appsp y\appsp z : \tya}{\dotsb}$ to define multiple abstractions at the same
    time
\end{itemize}

\subsubsection{Sum types}

We would like to recover our sum type, or disjunction, $\vee$.  This is easily
done with $\exists$:
\[
\begin{array}{rcl}
  \_\vee\_ & = &  \abs{\tya\appsp\tyb : \lcsetz}{\lcexists{x}{\lcbool}{\lcite{x}{\tya}{\tyb}}} \\
  \lcinl   & = & \abs{x}{(\lctrue, x)} \\
  \lcinr   & = & \abs{x}{(\lcfalse, x)} \\
  \mathsf{case} & = & \abs{x : \tya \vee \tyb}{\abs{f : \tya \tyarr \tyc}{\abs{g : \tyb \tyarr \tyc}{ \\
           &   & \hspace{0.5cm} \app{(\lcited{\lcfst x}{b}{(\lcite{b}{A}{B}) \tyarr C}{f}{g})}{(\lcsnd x)}}}}
\end{array}
\]
What is going on here?  We are using $\exists$ with $\lcbool$ as a tag, so that
we can choose between one of two types in the second element.  In
$\mathsf{case}$ we use $\lcite{\lcfst x}{\dotsb}{\dotsb}$ to discriminate on the
tag, that is, the first element of $x : \tya \vee \tyb$.  If the tag is true,
then we know that the second element is of type $\tya$, and we will apply $f$.
The same applies to the other branch, with $\tyb$ and $g$.

\subsubsection{Naturals}

Now it's time to showcase the power of $\mathsf{W}$ types.
\begin{eqnarray*}
  \mathsf{Nat}  & = & \lcw{b}{\lcbool}{\lcite{b}{\top}{\bot}}  \\
  \mathsf{zero} & = & \lcfalse \lhd \abs{z}{\lcabsurd z} \\
  \mathsf{suc}  & = & \abs{n}{(\lctrue \lhd \abs{\_}{n})}  \\
  \mathsf{plus} & = & \abs{x\appsp y}{\lcrecz{x}{(\abs{b}{\lcite{b}{\abs{\_\appsp f}{\app{\mathsf{suc}}{(\app{f}{\lcunit})}}}{\abs{\_\appsp\_}{y}}})}}
\end{eqnarray*}
Here we encode natural numbers through $\mathsf{W}$ types.  Each node contains a
$\lcbool$.  If the $\lcbool$ is $\lcfalse$, then there are no children, since we
have a function $\bot \tyarr \mathsf{Nat}$: this is our $0$.  If it's $\lctrue$,
we need one child only: the predecessor.  Similarly, we recurse giving to
$\lcsyn{rec}$ a function that handles the `base case' 0 when the $\lcbool$ is
$\lctrue$, and the inductive case otherwise.

We postpone more complex examples after the introduction of inductive families
and pattern matching, since $\mathsf{W}$ types get unwieldy very quickly.

\subsubsection{Propositional Equality}

We can finally introduce one of the central subjects of my project:
propositional equality.

\newcommand{\lceq}[3]{#2 =_{#1} #3}
\newcommand{\lceqz}[2]{#1 = #2}
\newcommand{\lcrefl}[2]{\mathsf{refl}_{#1}\appsp #2}
\newcommand{\lcsubst}[3]{\mathsf{subst}\appsp#1\appsp#2\appsp#3}

\begin{center}
  \axname{syntax}
  \begin{eqnarray*}
  \termsyn & ::= & ... \\
           &  |  & \lceq{\termsyn}{\termsyn}{\termsyn} \separ \lcrefl{\termsyn}{\termsyn} \separ \lcsubst{\termsyn}{\termsyn}{\termsyn}
 \end{eqnarray*}

  \axdesc{typing}{\Gamma \vdash \termsyn : \termsyn}

  \vspace{0.5cm}

  \begin{tabular}{c c}
    \AxiomC{$\Gamma \vdash \termt : \tya$}
    \UnaryInfC{$\Gamma \vdash \lcrefl{\tya}{\termt} : \lceq{\tya}{\termt}{\termt}$}
    \DisplayProof
    &
    \AxiomC{$\Gamma \vdash \termp : \lceq{\tya}{\termt}{\termm}$}
    \AxiomC{$\Gamma \vdash \tyb : \tya \tyarr \lcsetz$}
    \AxiomC{$\Gamma \vdash \termn : \app{\tyb}{\termt}$}
    \TrinaryInfC{$\Gamma \vdash \lcsubst{\termp}{\tyb}{\termn} : \app{\tyb}{\termm}$}
    \DisplayProof
  \end{tabular}

  \vspace{0.5cm}

  \axdesc{reduction}{\termsyn \bred \termsyn}
  \begin{eqnarray*}
    \lcsubst{(\lcrefl{\tya}{\termt})}{\tyb}{\termm} \bred \termm
  \end{eqnarray*}
\end{center}

Propositional equality internalises equality as a type.  This lets us prove
useful things.  The only way to introduce an equality proof is by reflexivity
($\mathsf{refl}$).  The eliminator is in the style of `Leibnitz's law' of
equality: `equals can be substituted for equals' ($\mathsf{subst}$).  The
computation rule refers to the fact that every canonical proof of equality will
be a $\mathsf{refl}$.  We can use $\neg (\lceq{\tya}{x}{y})$ to express
inequality.

These elements conclude our presentation of a `core' type theory.  For an
extended example see Section 6.2 of \cite{Thompson1991}\footnote{Note that while I
  attempted to formalise the proof in Agda, I found a bug in the book!  See the
  errata for details:
  \url{http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/errata.html}.}.  The above
language and examples have been codified in Agda\footnote{More on Agda in
  the next section.}, see appendix \ref{app:agda-code}.

\section{A more useful language}

While our core type theory equipped with $\mathsf{W}$ types is very usefully
conceptually as a simple but complete language, things get messy very fast.  In
this section we will present the elements that are usually include in theorem
provers or programming languages to make them usable by mathematicians or
programmers.

All the features presented, except for quotient types, are present in the second
version of the Agda system, which is described in the PhD thesis of the author
\citep{Norell2007}.  Agda follows a tradition of theorem provers based on ITT
with inductive families and pattern matching.  The closest relative of Agda,
apart from previous versions, is Epigram, whose type theory is described in
\cite{McBride2004}.  Coq is another notable theorem prover based on the same
concepts, and the first and most popular \cite{Coq}.

The main difference between Coq and Agda/Epigram is that the former focuses on
theorem proving, while the latter also want to be useful as functional
programming languages, while still offering good tools to express
mathematics\footnote{In fact, currently, Agda is used almost exclusively to
  express mathematics, rather than to program.}.  This is reflected in a series
of differences that I will not discuss here (most notably the absence of tactics
but better support for pattern matching in Agda/Epigram).  I will take the same
approach as Agda/Epigram and will give a perspective focused on functional
programming rather than theorem proving.  Every feature will be presented as it
is present in Agda (if possible, since some features are not present in Agda
yet).

\subsection{Inductive families}

\newcommand{\lcdata}[1]{\lcsyn{data}\appsp #1}
\newcommand{\lcdb}{\ |\ }
\newcommand{\lcind}{\hspace{0.2cm}}
\newcommand{\lcwhere}{\appsp \lcsyn{where}}
\newcommand{\lclist}[1]{\app{\mathsf{List}}{#1}}
\newcommand{\lcnat}{\app{\mathsf{Nat}}}
\newcommand{\lcvec}[2]{\app{\app{\mathsf{Vec}}{#1}}{#2}}

Inductive families were first introduced by \cite{Dybjer1991}.  For the reader
familiar with the recent developments present in the GHC compiler for Haskell,
inductive families will look similar to GADTs (Generalised Abstract Data Types).
% TODO: add citation
Haskell style data types provide \emph{parametric polymorphism}, so that we can
define types that range over type parameters:
\[
\begin{array}{l}
\lcdata{\lclist{A}} = \mathsf{Nil} \lcdb A :: \lclist{A}
\end{array}
\]
In this way we define the $\mathsf{List}$ type once while allowing elements to
be of any type.  $\mathsf{List}$ will be a type constructor of type $\lcsetz
\tyarr \lcsetz$, while $\mathsf{nil} : \lcforall{A}{\lcsetz}{\lclist{A}}$ and
$\_::\_ : \lcforall{A}{\lcsetz}{A \tyarr \lclist{A} \tyarr \lclist{A}}$.

Inductive families bring this concept one step further by allowing some of the
parameters to be constrained in constructors.  We call these parameters
`indices'.  For example we might define natural numbers
\[
\begin{array}{l}
\lcdata{\lcnat} : \lcsetz \lcwhere \\
  \begin{array}{l@{\ }l}
    \lcind \mathsf{zero} &: \lcnat \\
    \lcind \mathsf{suc}  &: \lcnat \tyarr \lcnat
  \end{array}
\end{array}
\]
And then define a type for lists indexed by length:
\[
\begin{array}{l}
\lcdata{\mathsf{Vec}}\appsp (A : \lcsetz) : \lcnat \tyarr \lcsetz \lcwhere \\
  \begin{array}{l@{\ }l}
    \lcind \mathsf{nil} &: \lcvec{A}{\mathsf{zero}} \\
    \lcind \_::\_ &: \{n : \mathsf{Nat}\} \tyarr A \tyarr \lcvec{A}{n} \tyarr \lcvec{A}{\app{(\mathsf{suc}}{n})}
  \end{array}
\end{array}
\]
Note that contrary to the Haskell ADT notation, with inductive families we
explicitly list the types for the type constructor and data constructors.  In
$\mathsf{Vec}$, $A$ is a parameter (same across all constructors) while the
$\lcnat$ is an integer.  In our syntax, in the $\lcsyn{data}$ declaration,
things to the left of the colon are parameters, while on the right we can define
the type of indices.  Also note that the parameters can be named across all
constructors, while indices can't.

In this $\mathsf{Vec}$ example, when we form a new list the length is
$\mathsf{zero}$.  When we append a new element to an existing list of length
$n$, the new list is of length $\app{\mathsf{suc}}{n}$, that is, one more than
the previous length.  Also note that we are using the $\{n : \lcnat\} \tyarr
\dotsb$ syntax to indicate an argument that we will omit when using $\_::\_$.
In the future I shall also omit the type of these implicit parameters, in line
how Agda works.

Once we have our $\mathsf{Vec}$ we can do things much more safely than with
normal lists.  For example, we can define an $\mathsf{head}$ function that
returns the first element of the list:
\[
\begin{array}{l}
\mathsf{head} : \{A\ n\} \tyarr \lcvec{A}{(\app{\mathsf{suc}}{n})} \tyarr A
\end{array}
\]
Note that we will not be able to provide this function with a
$\lcvec{A}{\mathsf{zero}}$, since it needs an index which is a successor of some
number.

\newcommand{\lcfin}[1]{\app{\mathsf{Fin}}{#1}}

If we wish to index a $\mathsf{Vec}$ safely, we can define an inductive family
$\lcfin{n}$, which represents the family of numbers smaller than a given number
$n$:
\[
\begin{array}{l}
  \lcdata{\mathsf{Fin}} : \lcnat \tyarr \lcsetz \lcwhere \\
  \begin{array}{l@{\ }l}
    \lcind \mathsf{fzero} &: \{n\} \tyarr \lcfin{n} \\
    \lcind \mathsf{fsuc}  &: \{n\} \tyarr (i : \lcfin{n}) \tyarr \lcfin{(\app{\mathsf{suc}}{n})}
  \end{array}
\end{array}
\]
$\mathsf{fzero}$ is smaller than any number apart from $\mathsf{zero}$.  Given
the family of numbers smaller than $i$, we can produce the family of numbers
smaller than $\app{\mathsf{suc}}{n}$.  Now we can define an `indexing' operation
for our $\mathsf{Vec}$:
\[
\begin{array}{l}
\_\mathsf{!!}\_ : \{A\ n\} \tyarr \lcvec{A}{n} \tyarr \lcfin{n} \tyarr A
\end{array}
\]
In this way we will be sure that the number provided as an index will be smaller
than the length of the $\mathsf{Vec}$ provided.


\subsection{Pattern matching}

\subsection{Guarded recursion}

\subsection{Corecursion}

\subsection{Quotient types}


\section{Why dependent types?}

\section{Many equalities}

\subsection{Revision}

\subsection{Extensional equality and its problems}

\subsection{Observational equality}

\section{What to do}


\bibliographystyle{authordate1}
\bibliography{background}

\appendix
\section{Agda code}
\label{app:agda-code}

\end{document}