\documentclass[report]{article}
%% Narrow margins
-\usepackage{fullpage}
+% \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}}}
-\definecolor{AgdaBound} {HTML}{000000}
+\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{?}{=}}}
+\DeclareUnicodeCharacter{9655}{\ensuremath{\rhd}}
+
%% -----------------------------------------------------------------------------
%% Commands
\newcommand{\mysyn}{\AgdaKeyword}
\newcommand{\mytyc}{\AgdaDatatype}
-\newcommand{\myind}{\AgdaInductiveConstructor}
+\newcommand{\mydc}{\AgdaInductiveConstructor}
\newcommand{\myfld}{\AgdaField}
\newcommand{\myfun}{\AgdaFunction}
-\newcommand{\myb}{\AgdaBound}
+% TODO make this use AgdaBound
+\newcommand{\myb}[1]{\AgdaBound{#1}}
\newcommand{\myfield}{\AgdaField}
+\newcommand{\myind}{\AgdaIndent}
+\newcommand{\mykant}{\textsc{Kant}}
+\newcommand{\mysynel}[1]{#1}
+\newcommand{\myse}{\mysynel}
+\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]{
+ {\small
+ \vspace{0.3cm}
+ \hfill \textbf{#1} $#2$
+ \vspace{-0.3cm}
+ \begin{framed}
+ #3
+ \end{framed}
+}
+}
+
+% TODO is \mathbin the correct thing for arrow and times?
+
+\newcommand{\mytmt}{\mysynel{t}}
+\newcommand{\mytmm}{\mysynel{m}}
+\newcommand{\mytmn}{\mysynel{n}}
+\newcommand{\myred}{\leadsto}
+\newcommand{\mysub}[3]{#1[#2 / #3]}
+\newcommand{\mytysyn}{\mysynel{type}}
+\newcommand{\mybasetys}{K}
+% TODO change this name
+\newcommand{\mybasety}[1]{B_{#1}}
+\newcommand{\mytya}{\myse{A}}
+\newcommand{\mytyb}{\myse{B}}
+\newcommand{\mytycc}{\myse{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{$\langle\rangle$}}
+\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}{\myse{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{\mytrue}{\mydc{true}}
+\newcommand{\myfalse}{\mydc{false}}
+\newcommand{\myitee}[5]{\myfun{if}\,#1 / {#2.#3}\,\myfun{then}\,#4\,\myfun{else}\,#5}
+\newcommand{\mynat}{\mytyc{$\mathbb{N}$}}
+\newcommand{\myrat}{\mytyc{$\mathbb{R}$}}
+\newcommand{\myite}[3]{\myfun{if}\,#1\,\myfun{then}\,#2\,\myfun{else}\,#3}
+\newcommand{\myfora}[3]{(#1 {:} #2) \myarr #3}
+\newcommand{\myexi}[3]{(#1 {:} #2) \myprod #3}
+\newcommand{\mypairr}[4]{\mathopen{\mydc{$\langle$}}#1\mathpunct{\mydc{,}} #4\mathclose{\mydc{$\rangle$}}_{#2{.}#3}}
+\newcommand{\mylist}{\mytyc{List}}
+\newcommand{\mynil}[1]{\mydc{[]}_{#1}}
+\newcommand{\mycons}{\mathbin{\mydc{∷}}}
+\newcommand{\myfoldr}{\myfun{foldr}}
+\newcommand{\myw}[3]{\myapp{\myapp{\mytyc{W}}{(#1 {:} #2)}}{#3}}
+\newcommand{\mynode}[2]{\mathbin{\mydc{$\lhd$}_{#1.#2}}}
+\newcommand{\myrec}[4]{\myfun{rec}\,#1 / {#2.#3}\,\myfun{with}\,#4}
+\newcommand{\mylub}{\sqcup}
+\newcommand{\mydefeq}{\cong}
%% -----------------------------------------------------------------------------
-\title{\textsc{Kant}: Implementing Observational Equality}
-% TODO remove double @ if we get rid of lhs2TeX
+\title{\mykant: Implementing Observational Equality}
\author{Francesco Mazzoli \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{<fm2209@ic.ac.uk>}}}
\date{June 2013}
\begin{document}
-%if False
+\iffalse
\begin{code}
module thesis where
-open import Level
\end{code}
-%endif
+\fi
\maketitle
principles described.
\end{abstract}
+\clearpage
+
\tableofcontents
+\clearpage
+
\section{Simple and not-so-simple types}
\label{sec:types}
-\section{Intuitionistic Type Theory and dependent 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}
+ $
+}
+
+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}{\myb{x}}{\mytmn}\text{, where} \\
+ \myind{1}
+ \begin{array}{l@{\ }c@{\ }l}
+ \mysub{\myb{x}}{\myb{x}}{\mytmn} & = & \mytmn \\
+ \mysub{\myb{y}}{\myb{x}}{\mytmn} & = & y\text{, with } \myb{x} \neq y \\
+ \mysub{(\myapp{\mytmt}{\mytmm})}{\myb{x}}{\mytmn} & = & (\myapp{\mysub{\mytmt}{\myb{x}}{\mytmn}}{\mysub{\mytmm}{\myb{x}}{\mytmn}}) \\
+ \mysub{(\myabs{\myb{x}}{\mytmm})}{\myb{x}}{\mytmn} & = & \myabs{\myb{x}}{\mytmm} \\
+ \mysub{(\myabs{\myb{y}}{\mytmm})}{\myb{x}}{\mytmn} & = & \myabs{\myb{z}}{\mysub{\mysub{\mytmm}{\myb{y}}{\myb{z}}}{\myb{x}}{\mytmn}}, \\
+ \multicolumn{3}{l}{\myind{1} \text{with $\myb{x} \neq \myb{y}$ and $\myb{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}, whose
+rules are shown in figure \ref{fig:stlc}.
+
+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.
+
+\begin{figure}[t]
+ \mydesc{syntax}{ }{
+ $
+ \begin{array}{r@{\ }c@{\ }l}
+ \mytmsyn & ::= & \myb{x} \mysynsep \myabss{\myb{x}}{\mytysyn}{\mytmsyn} \mysynsep
+ (\myapp{\mytmsyn}{\mytmsyn}) \\
+ \mytysyn & ::= & \myse{\phi} \mysynsep \mytysyn \myarr \mytysyn \mysynsep \\
+ \myb{x} & \in & \text{Some enumerable set of symbols} \\
+ \myse{\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}
+ }
+}
+ \caption{Syntax and typing rules for the STLC. Reduction is unchanged from
+ the untyped $\lambda$-calculus.}
+ \label{fig:stlc}
+\end{figure}
+
+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. Also
+ known as \emph{subject reduction}.
+\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{\myb{x}}{\myhole{?}}{\myapp{\myb{x}}{\myb{x}}})}{(\myabss{\myb{x}}{\myhole{?}}{\myapp{\myb{x}}{\myb{x}}})}
+\end{equation*}
+
+This makes the STLC Turing incomplete. We can recover the ability to loop by
+adding a combinator that recurses:
+
+\noindent
+\begin{minipage}{0.5\textwidth}
+\mydesc{syntax}{ } {
+ $ \mytmsyn ::= \dotsb \mysynsep \myfix{\myb{x}}{\mytysyn}{\mytmsyn} $
+ \vspace{0.4cm}
+}
+\end{minipage}
+\begin{minipage}{0.5\textwidth}
+\mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}} {
+ \centering{
+ \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytmt}{\mytya}$}
+ \UnaryInfC{$\myjud{\myfix{\myb{x}}{\mytya}{\mytmt}}{\mytya}$}
+ \DisplayProof
+ }
+}
+\end{minipage}
+
+\mydesc{reduction:}{\myjud{\mytmsyn}{\mytmsyn}}{
+ \centering{
+ $ \myfix{\myb{x}}{\mytya}{\mytmt} \myred \mysub{\mytmt}{\myb{x}}{(\myfix{\myb{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{\myb{f}}{(\mytya \myarr \mytyb)}{\myabss{\myb{g}}{(\mytyb \myarr \mytycc)}{\myabss{\myb{x}}{\mytya}{\myapp{\myb{g}}{(\myapp{\myb{f}}{\myb{x}})}}}}
+\]
+That is, function composition. Going beyond arrow types, we can extend our bare
+lambda calculus with useful types to represent other logical constructs, as
+shown in figure \ref{fig:natded}.
+
+\begin{figure}[t]
+\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{\phantom{$\myjud{\mytmt}{\myempty}$}}
+ \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}
+ }
+}
+\caption{Rules for the extendend STLC. Only the new features are shown, all the
+ rules and syntax for the STLC apply here too.}
+ \label{fig:natded}
+\end{figure}
+
+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.
+
+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.}.
+
+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 $\mysyn{fix}$ combinator, it is easy to see how it ruins our
+desire for consistency. The following term works for every type $\mytya$,
+including bottom:
+\[
+(\myfix{\myb{x}}{\mytya}{\myb{x}}) : \mytya
+\]
+
+\subsection{Inductive data}
+
+To make the STLC more useful as a programming language or reasoning tool it is
+common to include (or let the user define) inductive data types. These comprise
+of a type former, various constructors, and an eliminator (or destructor) that
+serves as primitive recursor.
+
+For example, we might add a $\mylist$ type constructor, along with an `empty
+list' ($\mynil{ }$) and `cons cell' ($\mycons$) constructor. The eliminator for
+lists will be the usual folding operation ($\myfoldr$). See figure
+\ref{fig:list}.
+
+\begin{figure}[h]
+\mydesc{syntax}{ }{
+ $
+ \begin{array}{r@{\ }c@{\ }l}
+ \mytmsyn & ::= & \dots \mysynsep \mynil{\mytysyn} \mysynsep \mytmsyn \mycons \mytmsyn
+ \mysynsep
+ \myapp{\myapp{\myapp{\myfoldr}{\mytmsyn}}{\mytmsyn}}{\mytmsyn} \\
+ \mytysyn & ::= & \dots \mysynsep \myapp{\mylist}{\mytysyn}
+ \end{array}
+ $
+}
+\mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
+ \centering{
+ $
+ \begin{array}{l@{\ }c@{\ }l}
+ \myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{\mynil{\mytya}} & \myred & \mytmt \\
+
+ \myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{(\mytmm \mycons \mytmn)} & \myred &
+ \myapp{\myapp{\myse{f}}{\mytmm}}{(\myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{\mytmn})}
+ \end{array}
+ $
+}
+}
+\mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
+ \centering{
+ \begin{tabular}{cc}
+ \AxiomC{\phantom{$\myjud{\mytmm}{\mytya}$}}
+ \UnaryInfC{$\myjud{\mynil{\mytya}}{\myapp{\mylist}{\mytya}}$}
+ \DisplayProof
+ &
+ \AxiomC{$\myjud{\mytmm}{\mytya}$}
+ \AxiomC{$\myjud{\mytmn}{\myapp{\mylist}{\mytya}}$}
+ \BinaryInfC{$\myjud{\mytmm \mycons \mytmn}{\myapp{\mylist}{\mytya}}$}
+ \DisplayProof
+ \end{tabular}
+ }
+ \myderivsp
+ \centering{
+ \AxiomC{$\myjud{\mysynel{f}}{\mytya \myarr \mytyb \myarr \mytyb}$}
+ \AxiomC{$\myjud{\mytmm}{\mytyb}$}
+ \AxiomC{$\myjud{\mytmn}{\myapp{\mylist}{\mytya}}$}
+ \TrinaryInfC{$\myjud{\myapp{\myapp{\myapp{\myfoldr}{\mysynel{f}}}{\mytmm}}{\mytmn}}{\mytyb}$}
+ \DisplayProof
+ }
+}
+\caption{Rules for lists in the STLC.}
+\label{fig:list}
+\end{figure}
+
+In section \ref{sec:well-order} we will see how to give a general account of
+inductive data. %TODO does this make sense to have here?
+
+\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 expressivity:
+
+$$
+\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 define a polymorphic
+ identity function:
+ \[\displaystyle
+ (\myabss{\myb{A}}{\mytyp}{\myabss{\myb{x}}{\myb{A}}{\myb{x}}}) : (\myb{A} : \mytyp) \myarr \myb{A} \myarr \myb{A}
+ \]
+ The first and most famous instance of this idea has been System F. This 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{\myb{A} \myar \myb{R}}{\mytyp}{(\myb{A}
+ \myarr \myb{R}) \myarr \myb{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{\myb{x}}{\mybool}{\myite{\myb{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'. It will serve as the logical `core' of all the other
+extensions that we will present and ultimately our implementation of a similar
+logic.
+
+\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:term-types} 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 simple 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}. The system's syntax and reduction rules are presented
+in their entirety in figure \ref{fig:core-tt-syn}. The typing rules are
+presented piece by piece. An Agda rendition of the presented theory is
+reproduced in appendix \ref{app:agda-code}.
+
+\begin{figure}[t]
+\mydesc{syntax}{ }{
+ $
+ \begin{array}{r@{\ }c@{\ }l}
+ \mytmsyn & ::= & \myb{x} \mysynsep
+ \mytyp_{l} \mysynsep
+ \myunit \mysynsep \mytt \mysynsep
+ \myempty \mysynsep \myapp{\myabsurd{\mytmsyn}}{\mytmsyn} \\
+ & | & \mybool \mysynsep \mytrue \mysynsep \myfalse \mysynsep
+ \myitee{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
+ & | & \myfora{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
+ \myabss{\myb{x}}{\mytmsyn}{\mytmsyn} \\
+ & | & \myexi{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
+ \mypairr{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn} \\
+ & | & \myapp{\myfst}{\mytmsyn} \mysynsep \myapp{\mysnd}{\mytmsyn} \\
+ & | & \myw{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
+ \mytmsyn \mynode{\myb{x}}{\mytmsyn} \mytmsyn \\
+ & | & \myrec{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn} \\
+ l & \in & \mathbb{N}
+ \end{array}
+ $
+}
+
+\mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
+ \centering{
+ \begin{tabular}{cc}
+ $
+ \begin{array}{l@{ }l@{\ }c@{\ }l}
+ \myitee{\mytrue &}{\myb{x}}{\myse{P}}{\mytmm}{\mytmn} & \myred & \mytmm \\
+ \myitee{\myfalse &}{\myb{x}}{\myse{P}}{\mytmm}{\mytmn} & \myred & \mytmn \\
+ \end{array}
+ $
+ &
+ $
+ \myapp{(\myabss{\myb{x}}{\mytya}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{\myb{x}}{\mytmn}
+ $
+ \myderivsp
+ \end{tabular}
+ $
+ \begin{array}{l@{ }l@{\ }c@{\ }l}
+ \myapp{\myfst &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmm \\
+ \myapp{\mysnd &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmn
+ \end{array}
+ $
+ \myderivsp
+
+ $
+ \myrec{(\myse{s} \mynode{\myb{x}}{\myse{T}} \myse{f})}{\myb{y}}{\myse{P}}{\myse{p}} \myred
+ \myapp{\myapp{\myapp{\myse{p}}{\myse{s}}}{\myse{f}}}{(\myabss{\myb{t}}{\mysub{\myse{T}}{\myb{x}}{\myse{s}}}{
+ \myrec{\myapp{\myse{f}}{\myb{t}}}{\myb{y}}{\myse{P}}{\mytmt}
+ })}
+ $
+ }
+}
+\caption{Syntax and reduction rules for our type theory.}
+\label{fig:core-tt-syn}
+\end{figure}
+
+\subsubsection{Types are terms, some terms are types}
+\label{sec:term-types}
+
+\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
+ \centering{
+ \begin{tabular}{cc}
+ \AxiomC{$\myjud{\mytmt}{\mytya}$}
+ \AxiomC{$\mytya \mydefeq \mytyb$}
+ \BinaryInfC{$\myjud{\mytmt}{\mytyb}$}
+ \DisplayProof
+ &
+ \AxiomC{\phantom{$\myjud{\mytmt}{\mytya}$}}
+ \UnaryInfC{$\myjud{\mytyp_l}{\mytyp_{l + 1}}$}
+ \DisplayProof
+ \end{tabular}
+ }
+}
+
+The first thing to notice is that a barrier between values and types that we had
+in the STLC is gone: values can appear in types, and the two are treated
+uniformly in the syntax.
+
+While the usefulness of doing this will become clear soon, a consequence is that
+since types can be the result of computation, deciding type equality is not
+immediate as in the STLC. For this reason we define \emph{definitional
+ equality}, $\mydefeq$, as the congruence relation extending $\myred$. Types
+that are definitionally equal can be used interchangeably. Here the
+`conversion' rule is not syntax directed, however we will see how it is possible
+to employ $\myred$ to decide term equality in a systematic way. % TODO add section
+Another thing to notice is that considering the need to reduce terms to decide
+equality, it is essential for a dependently type system to be terminating and
+confluent for type checking to be decidable.
+
+Moreover, we specify a \emph{type hierarchy} to talk about `large' types:
+$\mytyp_0$ will be the type of types inhabited by data: $\mybool$, $\mynat$,
+$\mylist$, etc. $\mytyp_1$ will be the type of $\mytyp_0$, and so on---for
+example we have $\mytrue : \mybool : \mytyp_0 : \mytyp_1 : \dots$. Each type
+`level' is often called a universe in the literature. While it is possible, to
+simplify things by having only one universe $\mytyp$ with $\mytyp : \mytyp$,
+this plan is inconsistent for much the same reason that impredicative na\"{\i}ve
+set theory is \citep{Hurkens1995}. Moreover, various techniques can be employed
+to lift the burden of explicitly handling universes.
+% TODO add sectioon about universes
+
+\subsubsection{Contexts}
+
+\begin{minipage}{0.5\textwidth}
+ \mydesc{context validity:}{\myvalid{\myctx}}{
+ \centering{
+ \begin{tabular}{cc}
+ \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
+ \UnaryInfC{$\myvalid{\myemptyctx}$}
+ \DisplayProof
+ &
+ \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
+ \UnaryInfC{$\myvalid{\myctx ; \myb{x} : \mytya}$}
+ \DisplayProof
+ \end{tabular}
+ }
+ }
+\end{minipage}
+\begin{minipage}{0.5\textwidth}
+ \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
+ \centering{
+ \AxiomC{$\myctx(x) = \mytya$}
+ \UnaryInfC{$\myjud{\myb{x}}{\mytya}$}
+ \DisplayProof
+ }
+ }
+\end{minipage}
+\vspace{0.1cm}
+
+We need to refine the notion context to make sure that every variable appearing
+is typed correctly, or that in other words each type appearing in the context is
+indeed a type and not a value. In every other rule, if no premises are present,
+we assume the context in the conclusion to be valid.
+
+Then we can re-introduce the old rule to get the type of a variable for a
+context.
+
+\subsubsection{$\myunit$, $\myempty$}
+
+\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
+ \centering{
+ \begin{tabular}{ccc}
+ \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
+ \UnaryInfC{$\myjud{\myunit}{\mytyp_0}$}
+ \noLine
+ \UnaryInfC{$\myjud{\myempty}{\mytyp_0}$}
+ \DisplayProof
+ &
+ \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
+ \UnaryInfC{$\myjud{\mytt}{\myunit}$}
+ \noLine
+ \UnaryInfC{\phantom{$\myjud{\myempty}{\mytyp_0}$}}
+ \DisplayProof
+ &
+ \AxiomC{$\myjud{\mytmt}{\myempty}$}
+ \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
+ \BinaryInfC{$\myjud{\myapp{\myabsurd{\mytya}}{\mytmt}}{\mytya}$}
+ \noLine
+ \UnaryInfC{\phantom{$\myjud{\myempty}{\mytyp_0}$}}
+ \DisplayProof
+ \end{tabular}
+ }
+}
+
+Nothing surprising here: $\myunit$ and $\myempty$ are unchanged from the STLC,
+with the added rules to type $\myunit$ and $\myempty$ themselves, and to make
+sure that we are invoking $\myabsurd{}$ over a type.
+
+\subsubsection{$\mybool$, and dependent $\myfun{if}$}
+
+\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
+ \centering{
+ \begin{tabular}{ccc}
+ \AxiomC{}
+ \UnaryInfC{$\myjud{\mybool}{\mytyp_0}$}
+ \DisplayProof
+ &
+ \AxiomC{}
+ \UnaryInfC{$\myjud{\mytrue}{\mybool}$}
+ \DisplayProof
+ &
+ \AxiomC{}
+ \UnaryInfC{$\myjud{\myfalse}{\mybool}$}
+ \DisplayProof
+ \end{tabular}
+ \myderivsp
+
+ \AxiomC{$\myjud{\mytmt}{\mybool}$}
+ \AxiomC{$\myjudd{\myctx : \mybool}{\mytya}{\mytyp_l}$}
+ \noLine
+ \BinaryInfC{$\myjud{\mytmm}{\mysub{\mytya}{x}{\mytrue}}$ \hspace{0.7cm} $\myjud{\mytmn}{\mysub{\mytya}{x}{\myfalse}}$}
+ \UnaryInfC{$\myjud{\myitee{\mytmt}{\myb{x}}{\mytya}{\mytmm}{\mytmn}}{\mysub{\mytya}{\myb{x}}{\mytmt}}$}
+ \DisplayProof
+
+ }
+}
+
+With booleans we get the first taste of `dependent' in `dependent types'. While
+the two introduction rules ($\mytrue$ and $\myfalse$) are not surprising, the
+typing rules for $\myfun{if}$ are. In most strongly typed languages we expect
+the branches of an $\myfun{if}$ statements to be of the same type, to preserve
+subject reduction, since execution could take both paths. This is a pity, since
+the type system does not reflect the fact that in each branch we gain knowledge
+on the term we are branching on. Which means that programs along the lines of
+\begin{verbatim}
+if null xs then head xs else 0
+\end{verbatim}
+are a necessary, well typed, danger.
+
+However, in a more expressive system, we can do better: the branches' type can
+depend on the value of the scrutinised boolean. This is what the typing rule
+expresses: the user provides a type $\mytya$ ranging over an $\myb{x}$
+representing the scrutinised boolean type, and the branches are typechecked with
+the updated knowledge on the value of $\myb{x}$.
+
+\subsubsection{$\myarr$, or dependent function}
+
+ \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
+ \centering{
+ \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
+ \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
+ \BinaryInfC{$\myjud{\myfora{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
+ \DisplayProof
+
+ \myderivsp
+
+ \begin{tabular}{cc}
+ \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytmt}{\mytyb}$}
+ \UnaryInfC{$\myjud{\myabss{\myb{x}}{\mytya}{\mytmt}}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
+ \DisplayProof
+ &
+ \AxiomC{$\myjud{\mytmm}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
+ \AxiomC{$\myjud{\mytmn}{\mytya}$}
+ \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mysub{\mytyb}{\myb{x}}{\mytmn}}$}
+ \DisplayProof
+ \end{tabular}
+ }
+}
+
+Dependent functions are one of the two key features that perhaps most
+characterise dependent types---the other being dependent products. With
+dependent functions, the result type can depend on the value of the argument.
+This feature, together with the fact that the result type might be a type
+itself, brings a lot of interesting possibilities. Keeping the correspondence
+with logic alive, dependent functions are much like universal quantifiers
+($\forall$) in logic.
+
+Again, we need to make sure that the type hierarchy is respected, which is the
+reason why a type formed by $\myarr$ will live in the least upper bound of the
+levels of argument and return type. This trend will continue with the other
+type-level binders, $\myprod$ and $\mytyc{W}$.
+
+% TODO maybe examples?
+
+\subsubsection{$\myprod$, or dependent product}
+
+
+\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
+ \centering{
+ \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
+ \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
+ \BinaryInfC{$\myjud{\myexi{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
+ \DisplayProof
+
+ \myderivsp
+
+ \begin{tabular}{cc}
+ \AxiomC{$\myjud{\mytmm}{\mytya}$}
+ \AxiomC{$\myjud{\mytmn}{\mysub{\mytyb}{\myb{x}}{\mytmm}}$}
+ \BinaryInfC{$\myjud{\mypairr{\mytmm}{\myb{x}}{\mytyb}{\mytmn}}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
+ \noLine
+ \UnaryInfC{\phantom{$--$}}
+ \DisplayProof
+ &
+ \AxiomC{$\myjud{\mytmt}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
+ \UnaryInfC{$\hspace{0.7cm}\myjud{\myapp{\myfst}{\mytmt}}{\mytya}\hspace{0.7cm}$}
+ \noLine
+ \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mysub{\mytyb}{\myb{x}}{\myapp{\myfst}{\mytmt}}}$}
+ \DisplayProof
+ \end{tabular}
+
+ }
+}
+
+
+\subsubsection{$\mytyc{W}$, or well-order}
+\label{sec:well-order}
+
+\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
+ \centering{
+ \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
+ \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
+ \BinaryInfC{$\myjud{\myw{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
+ \DisplayProof
+
+ \myderivsp
+
+ \AxiomC{$\myjud{\mytmt}{\mytya}$}
+ \AxiomC{$\myjud{\mysynel{f}}{\mysub{\mytyb}{\myb{x}}{\mytmt} \myarr \myw{\myb{x}}{\mytya}{\mytyb}}$}
+ \BinaryInfC{$\myjud{\mytmt \mynode{\myb{x}}{\mytyb} \myse{f}}{\myw{\myb{x}}{\mytya}{\mytyb}}$}
+ \DisplayProof
+
+ \myderivsp
+
+ \AxiomC{$\myjud{\myse{u}}{\myw{\myb{x}}{\myse{S}}{\myse{T}}}$}
+ \AxiomC{$\myjudd{\myctx; \myb{w} : \myw{\myb{x}}{\myse{S}}{\myse{T}}}{\myse{P}}{\mytyp_l}$}
+ \noLine
+ \BinaryInfC{$\myjud{\myse{p}}{
+ \myfora{\myb{s}}{\myse{S}}{\myfora{\myb{f}}{\mysub{\myse{T}}{\myb{x}}{\myse{s}} \myarr \myw{\myb{x}}{\myse{S}}{\myse{T}}}{(\myfora{\myb{t}}{\mysub{\myse{T}}{\myb{x}}{\myb{s}}}{\mysub{\myse{P}}{\myb{w}}{\myapp{\myb{f}}{\myb{t}}}}) \myarr \mysub{\myse{P}}{\myb{w}}{\myb{f}}}}
+ }$}
+ \UnaryInfC{$\myjud{\myrec{\myse{u}}{\myb{w}}{\myse{P}}{\myse{p}}}{\mysub{\myse{P}}{\myb{w}}{\myse{u}}}$}
+ \DisplayProof
+ }
+}
+
+
\section{The struggle for equality}
\label{sec:equality}
-\section{A more useful language}
+\subsection{Propositional equality...}
+
+\subsection{...and its limitations}
+
+eta law
+
+congruence
+
+UIP
+
+\subsection{Equality reflection}
+
+\subsection{Observational equality}
+
+\subsection{Univalence foundations}
+
+\section{Augmenting ITT}
\label{sec:practical}
-\section{Kant}
+\subsection{A more liberal hierarchy}
+
+\subsection{Type inference}
+
+\subsubsection{Bidirectional type checking}
+
+\subsubsection{Pattern unification}
+
+\subsection{Pattern matching and explicit fixpoints}
+
+\subsection{Induction-recursion}
+
+\subsection{Coinduction}
+
+\subsection{Dealing with partiality}
+
+\subsection{Type holes}
+
+\section{\mykant}
\label{sec:kant}
+
\appendix
\section{Notation and syntax}
-In the languages presented I will also use different fonts and colors for
-different things:
+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 and Agda code samples I also highlight the syntax,
+following a uniform color and font convention:
\begin{center}
\begin{tabular}{c | l}
- $\mytyc{Sans}$ & Type constructors. \\
- $\myind{sans}$ & Data constructors. \\
- $\myfld{sans}$ & Field accessors (e.g. \myfld{fst} and \myfld{snd} for products). \\
- $\mysyn{roman}$ & Syntax of the language. \\
- $\myfun{roman}$ & Defined values. \\
- $\myb{math}$ & Bound variables.
+ $\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 rendition of a core ITT}
+Moreover, I will from time to time give examples in the Haskell programming
+language as defined in \citep{Haskell2010}, which I will typeset in
+\texttt{teletype} font. I assume that the reader is already familiar with
+Haskell, plenty of good introductions are available \citep{LYAH,ProgInHask}.
+
+When presenting grammars, I will use a word in $\mysynel{math}$ font
+(e.g. $\mytmsyn$ or $\mytysyn$) to indicate indicate nonterminals. Additionally,
+I will use quite flexibly a $\mysynel{math}$ font to indicate a syntactic
+element. More specifically, terms are usually indicated by lowercase letters
+(often $\mytmt$, $\mytmm$, or $\mytmn$); and types by an uppercase letter (often
+$\mytya$, $\mytyb$, or $\mytycc$).
+
+When presenting type derivations, I will often abbreviate and present multiple
+conclusions, each on a separate line:
+
+\begin{prooftree}
+ \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
+ \UnaryInfC{$\myjud{\myapp{\myfst}{\mytmt}}{\mytya}$}
+ \noLine
+ \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mytyb}$}
+\end{prooftree}
+
+\section{Agda rendition of core ITT}
\label{app:agda-code}
\begin{code}
module ITT where
- data Empty : Set where
+ open import Level
+
+ data ⊥ : Set where
- absurd : ∀ {a} {A : Set a} → Empty → A
+ absurd : ∀ {a} {A : Set a} → ⊥ → A
absurd ()
- record Unit : Set where
+ 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
- open _×_ public
+ fst : A
+ snd : B fst
data Bool : Set where
true false : Bool
- if_/_then_else_ : ∀ {a} (x : Bool) → (P : Bool → Set a) → P true → P false → P x
- if true / _ then x else _ = x
- if false / _ then _ else x = x
+ 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.
+ (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}