...

[bitonic-mengthesis.git] / thesis.lagda

\documentclass[report]{article}

%% Narrow margins
% \usepackage{fullpage}

%% Bibtex
\usepackage{natbib}

%% Links
\usepackage{hyperref}

%% Frames
\usepackage{framed}

%% Symbols
\usepackage[fleqn]{amsmath}

%% Proof trees
\usepackage{bussproofs}

%% Diagrams
\usepackage[all]{xy}

%% -----------------------------------------------------------------------------
%% Commands for Agda
\usepackage[english]{babel}
\usepackage[conor]{agda}
\renewcommand{\AgdaKeywordFontStyle}[1]{\ensuremath{\mathrm{\underline{#1}}}}
\renewcommand{\AgdaFunction}[1]{\textbf{\textcolor{AgdaFunction}{#1}}}
\renewcommand{\AgdaField}{\AgdaFunction}
\definecolor{AgdaBound} {HTML}{000000}
\definecolor{AgdaHole} {HTML} {FFFF33}

\DeclareUnicodeCharacter{9665}{\ensuremath{\lhd}}
\DeclareUnicodeCharacter{964}{\ensuremath{\tau}}
\DeclareUnicodeCharacter{963}{\ensuremath{\sigma}}
\DeclareUnicodeCharacter{915}{\ensuremath{\Gamma}}
\DeclareUnicodeCharacter{8799}{\ensuremath{\stackrel{?}{=}}}


%% -----------------------------------------------------------------------------
%% Commands

\newcommand{\mysyn}{\AgdaKeyword}
\newcommand{\mytyc}{\AgdaDatatype}
\newcommand{\mydc}{\AgdaInductiveConstructor}
\newcommand{\myfld}{\AgdaField}
\newcommand{\myfun}{\AgdaFunction}
% TODO make this use AgdaBound
\newcommand{\myb}[1]{\ensuremath{#1}}
\newcommand{\myfield}{\AgdaField}
\newcommand{\myind}{\AgdaIndent}
\newcommand{\mykant}{\textsc{Kant}}
\newcommand{\mysynel}[1]{#1}
\newcommand{\mytmsyn}{\mysynel{term}}
\newcommand{\mysp}{\ }
% TODO \mathbin or \mathre here?
\newcommand{\myabs}[2]{\mydc{$\lambda$} #1 \mathrel{\mydc{$\mapsto$}} #2}
\newcommand{\myappsp}{\hspace{0.07cm}}
\newcommand{\myapp}[2]{#1 \myappsp #2}
\newcommand{\mysynsep}{\ \ |\ \ }

\FrameSep0.2cm
\newcommand{\mydesc}[3]{
  \hfill \textbf{#1} $#2$
  \vspace{-0.2cm}
  \begin{framed}
    #3
  \end{framed}
}

% TODO is \mathbin the correct thing for arrow and times?

\newcommand{\mytmt}{\myb{T}}
\newcommand{\mytmm}{\myb{M}}
\newcommand{\mytmn}{\myb{N}}
\newcommand{\myred}{\leadsto}
\newcommand{\mysub}[3]{#1[#2 \mapsto #3]}
\newcommand{\mytysyn}{\mysynel{type}}
\newcommand{\mybasetys}{K}
% TODO change this name
\newcommand{\mybasety}[1]{B_{#1}}
\newcommand{\mytya}{\myb{A}}
\newcommand{\mytyb}{\myb{B}}
\newcommand{\mytycc}{\myb{C}}
\newcommand{\myarr}{\mathrel{\textcolor{AgdaDatatype}{\to}}}
\newcommand{\myprod}{\mathrel{\textcolor{AgdaDatatype}{\times}}}
\newcommand{\myctx}{\Gamma}
\newcommand{\myvalid}[1]{#1 \vdash \underline{\mathrm{valid}}}
\newcommand{\myjudd}[3]{#1 \vdash #2 : #3}
\newcommand{\myjud}[2]{\myjudd{\myctx}{#1}{#2}}
% TODO \mathbin or \mathrel here?
\newcommand{\myabss}[3]{\mydc{$\lambda$} #1 {:} #2 \mathrel{\mydc{$\mapsto$}} #3}
\newcommand{\mytt}{\mydc{tt}}
\newcommand{\myunit}{\mytyc{$\top$}}
\newcommand{\mypair}[2]{\mathopen{\mydc{$\langle$}}#1\mathpunct{\mydc{,}} #2\mathclose{\mydc{$\rangle$}}}
\newcommand{\myfst}{\myfld{fst}}
\newcommand{\mysnd}{\myfld{snd}}
\newcommand{\myconst}{\myb{c}}
\newcommand{\myemptyctx}{\cdot}
\newcommand{\myhole}{\AgdaHole}
\newcommand{\myfix}[3]{\mysyn{fix} \myappsp #1 {:} #2 \mapsto #3}
\newcommand{\mysum}{\mathbin{\textcolor{AgdaDatatype}{+}}}
\newcommand{\myleft}[1]{\mydc{left}_{#1}}
\newcommand{\myright}[1]{\mydc{right}_{#1}}
\newcommand{\myempty}{\mytyc{$\bot$}}
\newcommand{\mycase}[2]{\mathopen{\myfun{[}}#1\mathpunct{\myfun{,}} #2 \mathclose{\myfun{]}}}
\newcommand{\myabsurd}[1]{\myfun{absurd}_{#1}}
\newcommand{\myarg}{\_}
\newcommand{\myderivsp}{\vspace{0.3cm}}
\newcommand{\mytyp}{\mytyc{Type}}
\newcommand{\myneg}{\myfun{$\neg$}}
\newcommand{\myar}{\,}
\newcommand{\mybool}{\mytyc{Bool}}
\newcommand{\mynat}{\mytyc{$\mathbb{N}$}}
\newcommand{\myrat}{\mytyc{$\mathbb{R}$}}
\newcommand{\myite}[3]{\mysyn{if}\,#1\,\mysyn{then}\,#2\,\mysyn{else}\,#3}
\newcommand{\myfora}[3]{(#1 {:} #2) \myarr #3}
\newcommand{\myexi}[3]{(#1 {:} #2) \mysum #3}

%% -----------------------------------------------------------------------------

\title{\mykant: Implementing Observational Equality}
\author{Francesco Mazzoli \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{<fm2209@ic.ac.uk>}}}
\date{June 2013}

\begin{document}

\iffalse
\begin{code}
module thesis where
\end{code}
\fi

\maketitle

\begin{abstract}
  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.

  Section \ref{sec:types} will give a very brief overview of STLC, and then
  illustrate how it can be interpreted as a natural deduction system.  Section
  \ref{sec:itt} will introduce Inutitionistic Type Theory (ITT), which expands
  on this concept, employing a more expressive logic.  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}.
  Section \ref{sec:equality} will explain why equality has always been a tricky
  business in these theories, and talk about the various attempts that have been
  made to make the situation better.  One interesting development has recently
  emerged: Observational Type theory.

  Section \ref{sec:practical} will describe common extensions found in the
  systems currently in use.  Finally, section \ref{sec:kant} will describe a
  system developed by the author that implements a core calculus based on the
  principles described.
\end{abstract}

\tableofcontents

\section{Simple and not-so-simple types}
\label{sec:types}

\subsection{The 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 syntax and no `data' in the
traditional sense, but just functions.  Here we give a brief overview of the
language, which will give the chance to introduce concepts central to the
analysis of all the following calculi.  The exposition follows the one found in
chapter 5 of \cite{Queinnec2003}.

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

\mydesc{syntax}{ }{
  $
  \begin{array}{r@{\ }c@{\ }l}
    \mytmsyn & ::= & \myb{x} \mysynsep \myabs{\myb{x}}{\mytmsyn} \mysynsep (\myapp{\mytmsyn}{\mytmsyn}) \\
    x          & \in & \text{Some enumerable set of symbols}
  \end{array}
  $
}

Through this text, I will use $\mytmt$, $\mytmm$, $\mytmn$ to indicate a generic
term, and $x$, $y$ to refer to variables.  Parenthesis will be omitted in the
usual way: $\myapp{\myapp{\mytmt}{\mytmm}}{\mytmn} =
\myapp{(\myapp{\mytmt}{\mytmm})}{\mytmn}$.

Abstractions roughly corresponds to functions, and their semantics is more
formally explained by the $\beta$-reduction rule:

\mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
  $
  \begin{array}{l}
    \myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{x}{\mytmn}\text{, where} \\
    \myind{1}
    \begin{array}{l@{\ }c@{\ }l}
      \mysub{x}{x}{\mytmn} & = & \mytmn \\
      \mysub{y}{x}{\mytmn} & = & y\text{, with } x \neq y \\
      \mysub{\myapp{\mytmt}{\mytmm}}{x}{\mytmn} & = & (\myapp{\mysub{\mytmt}{x}{\mytmn}}{\mysub{\mytmm}{x}{\mytmn}}) \\
      \mysub{(\myabs{x}{\mytmm})}{x}{\mytmn} & = & \myabs{x}{\mytmm} \\
      \mysub{(\myabs{y}{\mytmm})}{x}{\mytmn} & = & \myabs{z}{\mysub{\mysub{\mytmm}{y}{z}}{x}{\mytmn}}, \\
      \multicolumn{3}{l}{\myind{1} \text{with $x \neq y$ and $z$ not free in $\myapp{\mytmm}{\mytmn}$}}
    \end{array}
  \end{array}
  $
}

The care required during substituting variables for terms is required to avoid
name capturing.  We will use substitution in the future for other name-binding
constructs assuming similar precautions.

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):
\[
  (\myapp{\omega}{\omega}) \myred (\myapp{\omega}{\omega}) \myred \dots\text{, with $\omega = \myabs{x}{\myapp{x}{x}}$}
\]

A \emph{redex} is a term that can be reduced.  In the untyped $\lambda$-calculus
this will be the case for an application in which the first term is an
abstraction, but in general we call aterm reducible if it appears to the left of
a reduction rule.  When a term contains no redexes it's said to be in
\emph{normal form}.  Given the observation above, not all terms reduce to a
normal forms: we call the ones that do \emph{normalising}, and the ones that
don't \emph{non-normalising}.

The reduction rule presented is not syntax directed, but \emph{evaluation
  strategies} can be employed to reduce term systematically. Common evaluation
strategies include \emph{call by value} (or \emph{strict}), where arguments of
abstractions are reduced before being applied to the abstraction; and conversely
\emph{call by name} (or \emph{lazy}), where we reduce only when we need to do so
to proceed---in other words when we have an application where the function is
still not a $\lambda$. In both these reduction strategies we never reduce under
an abstraction: for this reason a weaker form of normalisation is used, where
both abstractions and normal forms are said to be in \emph{weak head normal
  form}.

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

A convenient way to `discipline' and reason about $\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}.  The first most basic instance
of this idea takes the name of \emph{simply typed $\lambda$ calculus}.

Our types contain a set of \emph{type variables} $\Phi$, which might correspond
to some `primitive' types; and $\myarr$, the type former for `arrow' types, the
types of functions.  The language is explicitly typed: when we bring a variable
into scope with an abstraction, we explicitly declare its type. $\mytya$,
$\mytyb$, $\mytycc$, will be used to refer to a generic type.  Reduction is
unchanged from the untyped $\lambda$-calculus.

\mydesc{syntax}{ }{
  $
  \begin{array}{r@{\ }c@{\ }l}
    \mytmsyn   & ::= & \myb{x} \mysynsep \myabss{\myb{x}}{\mytysyn}{\mytmsyn} \mysynsep
                       (\myapp{\mytmsyn}{\mytmsyn}) \\
    \mytysyn   & ::= & \myb{\phi} \mysynsep \mytysyn \myarr \mytysyn  \mysynsep \\
    \myb{x}    & \in & \text{Some enumerable set of symbols} \\
    \myb{\phi} & \in & \Phi
  \end{array}
  $
}

\mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
  \centering{
    \begin{tabular}{ccc}
      \AxiomC{$\myctx(x) = A$}
      \UnaryInfC{$\myjud{\myb{x}}{A}$}
      \DisplayProof
      &
      \AxiomC{$\myjudd{\myctx;\myb{x} : A}{\mytmt}{\mytyb}$}
      \UnaryInfC{$\myjud{\myabss{x}{A}{\mytmt}}{\mytyb}$}
      \DisplayProof
      &
      \AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$}
      \AxiomC{$\myjud{\mytmn}{\mytya}$}
      \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mytyb}$}
      \DisplayProof
    \end{tabular}
  }
}

In the typing rules, a context $\myctx$ is used to store the types of bound
variables: $\myctx; \myb{x} : \mytya$ adds a variable to the context and
$\myctx(x)$ returns the type of the rightmost occurrence of $x$.

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
\citep{Pierce2002}:
\begin{description}
\item[Progress] A well-typed term is not stuck---it is either a variable, or its
  constructor does not appear on the left of the $\myred$ relation (currently
  only $\lambda$), or it can take a step according to the evaluation rules.
\item[Preservation] If a well-typed term takes a step of evaluation, then the
  resulting term is also well-typed, and preserves the previous type.
\end{description}

However, STLC buys us much more: every well-typed term is normalising
\citep{Tait1967}.  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*}
  \myapp{(\myabss{x}{\myhole{?}}{\myapp{x}{x}})}{(\myabss{x}{\myhole{?}}{\myapp{x}{x}})}
\end{equation*}

This makes the STLC Turing incomplete.  We can recover the ability to loop by
adding a combinator that recurses:

% TODO make this more compact

\mydesc{syntax}{ } {
  $ \mytmsyn ::= \dotsb \mysynsep \myfix{x}{\mytysyn}{\mytmsyn} $
}

\mydesc{typing:}{ } {
  \AxiomC{$\myjudd{\myctx; x : \mytya}{\mytmt}{\mytya}$}
  \UnaryInfC{$\myjud{\myfix{x}{\mytya}{\mytmt}}{\mytya}$}
  \DisplayProof
}

\mydesc{reduction:}{ }{
  $ \myfix{x}{\mytya}{\mytmt} \myred \mysub{\mytmt}{x}{(\myfix{x}{\mytya}{\mytmt})}$
}

This will deprive us of normalisation, which is a particularly bad thing if we
want to use the STLC as described in the next section.

\subsection{The Curry-Howard correspondence}

It turns out that the STLC can be seen a natural deduction system for
intuitionistic 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 ($\myarr$) type corresponds to implication.  If we wish to prove that
that $(\mytya \myarr \mytyb) \myarr (\mytyb \myarr \mytycc) \myarr (\mytya
\myarr \mytycc)$, all we need to do is to devise a $\lambda$-term that has the
correct type:
\[
  \myabss{f}{(\mytya \myarr \mytyb)}{\myabss{g}{(\mytyb \myarr \mytycc)}{\myabss{x}{\mytya}{\myapp{g}{(\myapp{f}{x})}}}}
\]
That is, function composition.  We can extend our bare lambda calculus with
useful types to represent other logical constructs.

\mydesc{syntax}{ }{
  $
  \begin{array}{r@{\ }c@{\ }l}
    \mytmsyn & ::= & \dots \\
             &  |  & \mytt \mysynsep \myapp{\myabsurd{\mytysyn}}{\mytmsyn} \\
             &  |  & \myapp{\myleft{\mytysyn}}{\mytmsyn} \mysynsep
                     \myapp{\myright{\mytysyn}}{\mytmsyn} \mysynsep
                     \myapp{\mycase{\mytmsyn}{\mytmsyn}}{\mytmsyn} \\
             &  |  & \mypair{\mytmsyn}{\mytmsyn} \mysynsep
                     \myapp{\myfst}{\mytmsyn} \mysynsep \myapp{\mysnd}{\mytmsyn} \\
    \mytysyn & ::= & \dots \mysynsep \myunit \mysynsep \myempty \mysynsep \mytmsyn \mysum \mytmsyn \mysynsep \mytysyn \myprod \mytysyn
  \end{array}
  $
}

\mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
  \centering{
    \begin{tabular}{cc}
      $
      \begin{array}{l@{ }l@{\ }c@{\ }l}
        \myapp{\mycase{\mytmm}{\mytmn}}{(\myapp{\myleft{\mytya} &}{\mytmt})} & \myred &
          \myapp{\mytmm}{\mytmt} \\
        \myapp{\mycase{\mytmm}{\mytmn}}{(\myapp{\myright{\mytya} &}{\mytmt})} & \myred &
          \myapp{\mytmn}{\mytmt}
      \end{array}
      $
      &
      $
      \begin{array}{l@{ }l@{\ }c@{\ }l}
        \myapp{\myfst &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmm \\
        \myapp{\mysnd &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmn
      \end{array}
      $
    \end{tabular}
  }
}

\mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
  \centering{
    \begin{tabular}{cc}
      \AxiomC{}
      \UnaryInfC{$\myjud{\mytt}{\myunit}$}
      \DisplayProof
      &
      \AxiomC{$\myjud{\mytmt}{\myempty}$}
      \UnaryInfC{$\myjud{\myapp{\myabsurd{\mytya}}{\mytmt}}{\mytya}$}
      \DisplayProof
    \end{tabular}
  }
  \myderivsp
  \centering{
    \begin{tabular}{cc}
      \AxiomC{$\myjud{\mytmt}{\mytya}$}
      \UnaryInfC{$\myjud{\myapp{\myleft{\mytyb}}{\mytmt}}{\mytya \mysum \mytyb}$}
      \DisplayProof
      &
      \AxiomC{$\myjud{\mytmt}{\mytyb}$}
      \UnaryInfC{$\myjud{\myapp{\myright{\mytya}}{\mytmt}}{\mytya \mysum \mytyb}$}
      \DisplayProof

    \end{tabular}
  }
  \myderivsp
  \centering{
    \begin{tabular}{cc}
      \AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$}
      \AxiomC{$\myjud{\mytmn}{\mytya \myarr \mytycc}$}
      \AxiomC{$\myjud{\mytmt}{\mytya \mysum \mytyb}$}
      \TrinaryInfC{$\myjud{\myapp{\mycase{\mytmm}{\mytmn}}{\mytmt}}{\mytycc}$}
      \DisplayProof
    \end{tabular}
  }
  \myderivsp
  \centering{
    \begin{tabular}{ccc}
      \AxiomC{$\myjud{\mytmm}{\mytya}$}
      \AxiomC{$\myjud{\mytmn}{\mytyb}$}
      \BinaryInfC{$\myjud{\mypair{\mytmm}{\mytmn}}{\mytya \myprod \mytyb}$}
      \DisplayProof
      &
      \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
      \UnaryInfC{$\myjud{\myapp{\myfst}{\mytmt}}{\mytya}$}
      \DisplayProof
      &
      \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
      \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mytyb}$}
      \DisplayProof
    \end{tabular}
  }
}

Tagged unions (or sums, or coproducts---$\mysum$ here, \texttt{Either} in
Haskell) correspond to disjunctions, and dually tuples (or pairs, or
products---$\myprod$ here, tuples in Haskell) correspond to conjunctions.  This
is apparent looking at the ways to construct and destruct the values inhabiting
those types: for $\mysum$ $\myleft{ }$ and $\myright{ }$ correspond to $\vee$
introduction, and $\mycase{\_}{\_}$ to $\vee$ elimination; for $\myprod$
$\mypair{\_}{\_}$ corresponds to $\wedge$ introduction, $\myfst$ and $\mysnd$ to
$\wedge$ elimination.

The trivial type $\myunit$ corresponds to the logical $\top$, and dually
$\myempty$ corresponds to the logical $\bot$.  $\myunit$ has one introduction
rule ($\mytt$), and thus one inhabitant; and no eliminators.  $\myempty$ has no
introduction rules, and thus no inhabitants; and one eliminator ($\myabsurd{
}$), corresponding to the logical \emph{ex falso quodlibet}.  Note that in the
constructors for the sums and the destructor for $\myempty$ we need to include
some type information to keep type checking decidable.

As in logic, if we want to keep our system consistent, we must make sure that no
closed terms (in other words terms not under a $\lambda$) inhabit $\myempty$.
The variant of STLC presented here is indeed consistent, a result that follows
from the fact that it is normalising. % TODO explain
Going back to our $\myfix{ }{ }{ }$ combinator, it is easy to see how it breaks
our desire for consistency.  The following term works for every type $\mytya$,
including bottom:
\[
(\myfix{x}{\mytya}{x}) : \mytya
\]

With these rules, our STLC now looks remarkably similar in power and use to the
natural deduction we already know.  $\myneg \mytya$ can be expressed as $\mytya
\myarr \myempty$.  However, there is an important omission: there is no term of
the type $\mytya \mysum \myneg \mytya$ (excluded middle), or equivalently
$\myneg \myneg \mytya \myarr \mytya$ (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 I will not touch those subjects.}.


\section{Intuitionistic Type Theory}
\label{sec:itt}

\subsection{Extending the STLC}

The STLC can be made more expressive in various ways.  \cite{Barendregt1991}
succinctly expressed geometrically how we can add expressively:

$$
\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]
}
$$
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}$)] We can quantify over
  types in our type signatures.  For example, we can defined a polymorphic
  identity function:
  $\displaystyle
  (\myabss{\mytya}{\mytyp}{\myabss{x}{A}{x}}) : (\mytya : \mytyp) \myarr \mytya \myarr \mytya
  $.
  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}}$)] We have
  type operators.  For example we could define a function that given types $R$
  and $\mytya$ forms the type that represents a value of type $\mytya$ in
  continuation passing style: $\displaystyle(\myabss{A \myar R}{\mytyp}{(\mytya
    \myarr R) \myarr R}) : \mytyp \myarr \mytyp \myarr \mytyp$.
\item[Types depending on terms (towards $\lambda{P}$)] Also known as `dependent
  types', give great expressive power.  For example, we can have values of whose
  type depend on a boolean:
  $\displaystyle(\myabss{x}{\mybool}{\myite{x}{\mynat}{\myrat}}) : \mybool
  \myarr \mytyp$.
\end{description}

All the systems preserve the properties that make the STLC well behaved.  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'.

\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 inconsistent due to its
impredicativity\footnote{In the early version there was only one universe
  $\mytyp$ and $\mytyp : \mytyp$, 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 polymorphic $\lambda$-calculus, and specifically
the previously mentioned System F, which was developed 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} 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 is
quite close to the original formulation of predicative ITT as found in
\citep{Martin-Lof1984}.

\mydesc{syntax}{ }{
  $
  \begin{array}{r@{\ }c@{\ }l}
    \mytmsyn & ::= & \myb{x} \\
             &  |  & \myunit \mysynsep \mytt \\
             &  |  & \myempty \mysynsep \myapp{\myabsurd{\mytmsyn}}{\mytmsyn} \\
             &  |  & \myfora{x}{\mytmsyn}{\mytmsyn} \mysynsep
                     \myabss{x}{\mytmsyn}{\mytmsyn} \\
             &  |  & \myexi{x}{\mytmsyn}{\mytmsyn} \mysynsep
                     \mypair{\mytmsyn}{\mytmsyn} \mysynsep \myapp{\myfst}{\mytmsyn}
  \end{array}
  $
}

\mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{

}

\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{

}

\section{The struggle for equality}
\label{sec:equality}

\section{Extending ITT}
\label{sec:practical}

\section{\mykant}
\label{sec:kant}

\appendix

\section{Notation and syntax}

Syntax, derivation rules, and reduction rules, are enclosed in frames describing
the type of relation being established and the syntactic elements appearing,
for example

\mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
  Typing derivations here.
}

In the languages presented I also highlight the syntax, following a uniform
color and font convention:

\begin{center}
  \begin{tabular}{c | l}
    $\mytyc{Sans}$  & Type constructors. \\
    $\mydc{sans}$  & Data constructors. \\
    % $\myfld{sans}$  & Field accessors (e.g. \myfld{fst} and \myfld{snd} for products). \\
    $\mysyn{roman}$ & Keywords of the language. \\
    $\myfun{roman}$ & Defined values and destructors. \\
    $\myb{math}$    & Bound variables.
  \end{tabular}
\end{center}

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

\subsection{ITT}

\begin{code}
module ITT where
  open import Level

  data ⊥ : Set where

  absurd : ∀ {a} {A : Set a} → ⊥ → A
  absurd ()

  record ⊤ : Set where
    constructor tt

  record _×_ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
    constructor _,_
    field
      fst  : A
      snd  : B fst

  data Bool : Set where
    true false : Bool

  if_then_else_ : ∀ {a} {P : Bool → Set a} (x : Bool) → P true → P false → P x
  if true then x else _ = x
  if false then _ else x = x

  data W {s p} (S : Set s) (P : S → Set p) : Set (s ⊔ p) where
    _◁_ : (s : S) → (P s → W S P) → W S P

  rec : ∀ {a b} {S : Set a} {P : S → Set b}
    (C : W S P → Set) →       -- some conclusion we hope holds
    ((s : S) →                -- given a shape...
     (f : P s → W S P) →      -- ...and a bunch of kids...
     ((p : P s) → C (f p)) →  -- ...and C for each kid in the bunch...
     C (s ◁ f)) →             -- ...does C hold for the node?
    (x : W S P) →             -- If so, ...
    C x                       -- ...C always holds.
  rec C c (s ◁ f) = c s f (λ p → rec C c (f p))
\end{code}

\nocite{*}
\bibliographystyle{authordate1}
\bibliography{thesis}

\end{document}