\documentclass[report]{article}
%% Narrow margins
-\usepackage{fullpage}
+% \usepackage{fullpage}
%% Bibtex
\usepackage{natbib}
%% Links
\usepackage{hyperref}
+%% Frames
+\usepackage{framed}
+
+%% Symbols
+\usepackage[fleqn]{amsmath}
+\usepackage{stmaryrd} %llbracket
+
+%% Proof trees
+\usepackage{bussproofs}
+
+%% Diagrams
+\usepackage[all]{xy}
+
+%% Quotations
+\usepackage{epigraph}
+
+%% Images
+\usepackage{graphicx}
+
+%% diagrams
+\usepackage{tikz}
+\usetikzlibrary{shapes,arrows,positioning}
+% \usepackage{tikz-cd}
+% \usepackage{pgfplots}
+
+
%% -----------------------------------------------------------------------------
%% Commands for Agda
\usepackage[english]{babel}
\renewcommand{\AgdaKeywordFontStyle}[1]{\ensuremath{\mathrm{\underline{#1}}}}
\renewcommand{\AgdaFunction}[1]{\textbf{\textcolor{AgdaFunction}{#1}}}
\renewcommand{\AgdaField}{\AgdaFunction}
-\definecolor{AgdaBound} {HTML}{000000}
+% \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]{
+ \noindent
+ \mbox{
+ \parbox{\textwidth}{
+ {\small
+ \vspace{0.3cm}
+ \hfill \textbf{#1} $#2$
+
+ \framebox[\textwidth]{
+ \parbox{\textwidth}{
+ \vspace{0.1cm}
+ #3
+ \vspace{0.1cm}
+ }
+ }
+ }
+ }
+ }
+}
+
+% 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{Unit}}
+\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{Empty}}
+\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}
+\newcommand{\myrefl}{\mydc{refl}}
+\newcommand{\mypeq}[1]{\mathrel{\mytyc{=}_{#1}}}
+\newcommand{\myjeqq}{\myfun{=-elim}}
+\newcommand{\myjeq}[3]{\myapp{\myapp{\myapp{\myjeqq}{#1}}{#2}}{#3}}
+\newcommand{\mysubst}{\myfun{subst}}
+\newcommand{\myprsyn}{\myse{prop}}
+\newcommand{\myprdec}[1]{\llbracket #1 \rrbracket}
+\newcommand{\myand}{\wedge}
+\newcommand{\myprfora}[3]{\forall #1 {:} #2. #3}
+\newcommand{\mybot}{\bot}
+\newcommand{\mytop}{\top}
+\newcommand{\mycoe}{\myfun{coe}}
+\newcommand{\mycoee}[4]{\myapp{\myapp{\myapp{\myapp{\mycoe}{#1}}{#2}}{#3}}{#4}}
+\newcommand{\mycoh}{\myfun{coh}}
+\newcommand{\mycohh}[4]{\myapp{\myapp{\myapp{\myapp{\mycoh}{#1}}{#2}}{#3}}{#4}}
+\newcommand{\myjm}[4]{(#1 {:} #2) = (#3 {:} #4)}
+\newcommand{\myprop}{\mytyc{Prop}}
%% -----------------------------------------------------------------------------
-\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}
\iffalse
\begin{code}
module thesis where
-open import Level
\end{code}
\fi
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).
+
+Most widely used interactive theorem provers are based on ITT. Popular ones
+include Agda \citep{Norell2007, Bove2009}, Coq \citep{Coq}, and Epigram
+\citep{McBride2004, EpigramTut}.
+
+\subsection{A note on inference}
+
+% TODO do this, adding links to the sections about bidi type checking and
+% implicit universes.
+In the following text I will often omit explicit typing for abstractions or
+
+Moreover, I will use $\mytyp$ without bothering to specify a
+universe, with the silent assumption that the definition is consistent
+regarding to the hierarchy.
+
+\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$---moreover, when comparing types syntactically we do it up to
+renaming of bound names ($\alpha$-renaming). For example under this
+discipline we will find that
+\[
+\myabss{\myb{x}}{\mytya}{\myb{x}} \mydefeq \myabss{\myb{y}}{\mytya}{\myb{y}}
+\]
+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}
+In the previous section we saw how a type checker (or a human) needs a notion of
+\emph{definitional equality}. Beyond this meta-theoretic notion, in this
+section we will explore the ways of expressing equality \emph{inside} the
+theory, as a reasoning tool available to the user. This area is the main
+concern of this thesis, and in general a very active research topic, since we do
+not have a fully satisfactory solution, yet.
+
+\subsection{Propositional equality}
+
+\noindent
+\begin{minipage}{0.5\textwidth}
+\mydesc{syntax}{ }{
+ $
+ \begin{array}{r@{\ }c@{\ }l}
+ \mytmsyn & ::= & \dots \\
+ & | & \mytmsyn \mypeq{\mytmsyn} \mytmsyn \mysynsep
+ \myapp{\myrefl}{\mytmsyn} \\
+ & | & \myjeq{\mytmsyn}{\mytmsyn}{\mytmsyn}
+ \end{array}
+ $
+}
+\end{minipage}
+\begin{minipage}{0.5\textwidth}
+\mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
+ \centering{
+ $
+ \myjeq{\myse{P}}{(\myapp{\myrefl}{\mytmm})}{\mytmn} \myred \mytmn
+ $
+ }
+ \vspace{0.9cm}
+}
+\end{minipage}
+
+\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
+ \centering{
+ \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
+ \AxiomC{$\myjud{\mytmm}{\mytya}$}
+ \AxiomC{$\myjud{\mytmn}{\mytya}$}
+ \TrinaryInfC{$\myjud{\mytmm \mypeq{\mytya} \mytmn}{\mytyp_l}$}
+ \DisplayProof
+
+ \myderivsp
+
+ \begin{tabular}{cc}
+ \AxiomC{\phantom{$\myctx P \mytyp_l$}}
+ \noLine
+ \UnaryInfC{$\myjud{\mytmt}{\mytya}$}
+ \UnaryInfC{$\myjud{\myapp{\myrefl}{\mytmt}}{\mytmt \mypeq{\mytya} \mytmt}$}
+ \DisplayProof
+ &
+ \AxiomC{$\myjud{\myse{P}}{\myfora{\myb{x}\ \myb{y}}{\mytya}{\myfora{q}{\myb{x} \mypeq{\mytya} \myb{y}}{\mytyp_l}}}$}
+ \noLine
+ \UnaryInfC{$\myjud{\myse{q}}{\mytmm \mypeq{\mytya} \mytmn}\hspace{1.2cm}\myjud{\myse{p}}{\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmm}}{(\myapp{\myrefl}{\mytmm})}}$}
+ \UnaryInfC{$\myjud{\myjeq{\myse{P}}{\myse{q}}{\myse{p}}}{\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmn}}{q}}$}
+ \DisplayProof
+ \end{tabular}
+ }
+}
+
+To express equality between two terms inside ITT, the obvious way to do so is
+to have the equality construction to be a type-former. Here we present what
+has survived as the dominating form of equality in systems based on ITT up to
+the present day.
+
+Our type former is $\mypeq{\mytya}$, which given a type (in this case
+$\mytya$) relates equal terms of that type. $\mypeq{}$ has one introduction
+rule, $\myrefl$, which introduces an equality relation between definitionally
+equal terms---in the typing rule we display the term as `the same', meaning
+`the same up to $\mydefeq$'. % TODO maybe mention this earlier
+
+Finally, we have one eliminator for $\mypeq{}$, $\myjeqq$. $\myjeq{\myse{P}}{\myse{q}}{\myse{p}}$ takes
+\begin{itemize}
+\item $\myse{P}$, a predicate working with two terms of a certain type (say
+ $\mytya$) and a proof of their equality
+\item $\myse{q}$, a proof that two terms in $\mytya$ (say $\myse{m}$ and
+ $\myse{n}$) are equal
+\item and $\myse{p}$, an inhabitant of $\myse{P}$ applied to $\myse{m}$, plus
+ the trivial proof by reflexivity showing that $\myse{m}$ is equal to itself
+\end{itemize}
+Given these ingredients, $\myjeqq$ retuns a member of $\myse{P}$ applied to
+$\mytmm$, $\mytmn$, and $\myse{q}$. In other words $\myjeqq$ takes a
+witness that $\myse{P}$ works with \emph{definitionally equal} terms, and
+returns a witness of $\myse{P}$ working with \emph{propositionally equal}
+terms. Invokations of $\myjeqq$ will vanish when the equality proofs will
+reduce to invocations to reflexivity, at which point the arguments must be
+definitionally equal, and thus the provided
+$\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmm}}{(\myapp{\myrefl}{\mytmm})}$
+can be returned.
+
+While the $\myjeqq$ rule is slightly convoluted, ve can derive many more
+`friendly' rules from it, for example a more obvious `substitution' rule, that
+replaces equal for equal in predicates:
+\[
+\begin{array}{l}
+(\myabs{\myb{A}\ \myb{P}\ \myb{x}\ \myb{y}\ \myb{q}\ \myb{p}}{
+ \myjeq{(\myabs{\myb{x}\ \myb{y}\ \myb{q}}{\myapp{\myb{P}}{\myb{y}}})}{\myb{q}}{\myb{p}}}) : \\
+\myind{1} \myfora{\myb{A}}{\mytyp}{\myfora{\myb{P}}{\myb{A} \myarr \mytyp}{\myfora{\myb{x}\ \myb{y}}{\myb{A}}{\myb{x} \mypeq{\myb{A}} \myb{y} \myarr \myapp{\myb{P}}{\myb{x}} \myarr \myapp{\myb{P}}{\myb{y}}}}}
+\end{array}
+\]
+This rule is often called $\myfun{subst}$---here we will invoke it without
+specifying the type ($\myb{A}$) and the sides of the equality
+($\myb{x},\myb{y}$).
+
+Once we have $\myfun{subst}$, we can easily prove more familiar laws regarding
+equality, such as symmetry, transitivity, and a congruence law:
+
+% TODO finish this
+
+\subsection{Common extensions}
+
+eta law
+
+congruence
+
+UIP
+
+\subsection{Limitations}
+
+\epigraph{\emph{Half of my time spent doing research involves thinking up clever
+ schemes to avoid needing functional extensionality.}}{@larrytheliquid}
+
+However, propositional equality as described is quite restricted when
+reasoning about equality beyond the term structure, which is what definitional
+equality gives us (extension notwithstanding).
+
+The problem is best exemplified by \emph{function extensionality}. In
+mathematics, we would expect to be able to treat functions that give equal
+output for equal input as the same. When reasoning in a mechanised framework
+we ought to be able to do the same: in the end, without considering the
+operational behaviour, all functions equal extensionally are going to be
+replaceable with one another.
+
+However this is not the case, or in other words with the tools we have we have
+no term of type
+\[
+\myfun{ext} : \myfora{\myb{A}\ \myb{B}}{\mytyp}{\myfora{\myb{f}\ \myb{g}}{
+ \myb{A} \myarr \myb{B}}{
+ (\myfora{\myb{x}}{\myb{A}}{\myapp{\myb{f}}{\myb{x}} \mypeq{\myb{B}} \myapp{\myb{g}}{\myb{x}}}) \myarr
+ \myb{f} \mypeq{\myb{A} \myarr \myb{B}} \myb{g}
+ }
+}
+\]
+To see why this is the case, consider the functions
+\[\myabs{\myb{x}}{0 \mathrel{\myfun{+}} \myb{x}}$ and $\myabs{\myb{x}}{\myb{x} \mathrel{\myfun{+}} 0}\]
+where $\myfun{+}$ is defined by recursion on the first argument, gradually
+destructing it to build up successors of the second argument. The two
+functions are clearly denotationally the same, and we can in fact prove that
+\[
+\myfora{\myb{x}}{\mynat}{(0 \mathrel{\myfun{+}} \myb{x}) \mypeq{\mynat} (\myb{x} \mathrel{\myfun{+}} 0)}
+\]
+By analysis on the $\myb{x}$. However, the two functions are not
+definitionally equal, and thus we won't be able to get rid of the
+quantification.
+
+For the reasons above, theories that offer a propositional equality similar to
+what we presented are called \emph{intensional}, as opposed to
+\emph{extensional}. Most systems in wide use today (such as Agda, Coq and
+Epigram) are of this kind.
+
+This is quite an annoyance that often makes reasoning awkward to execute. It
+also extends to other fields, for example proving bisimulation between
+processes specified by coinduction, or in general proving equivalences based
+on the behaviour on a term.
+
+\subsection{Equality reflection}
+
+One way to `solve' this problem is by identifying propositional equality with
+definitional equality:
+
+\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
+ \centering{
+ \AxiomC{$\myjud{\myse{q}}{\mytmm \mypeq{\mytya} \mytmn}$}
+ \UnaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\mytya}$}
+ \DisplayProof
+ }
+}
+
+This rule takes the name of \emph{equality reflection}, and is a very
+different rule from the ones we saw up to now: it links a typing judgement
+internal to the type theory to a meta-theoretic judgement that the type
+checker uses to work with terms. It is easy to see the dangerous consequences
+that this causes:
+\begin{itemize}
+\item The rule is syntax directed, and the type checker is presumably expected
+ to come up with equality proofs when needed.
+\item More worryingly, type checking becomes undecidable also because
+ computing under false assumptions becomes unsafe.
+ Consider for example
+ \[
+ \myabss{\myb{q}}{\mytya \mypeq{\mytyp} (\mytya \myarr \mytya)}{\myhole{?}}
+ \]
+ Using the assumed proof in tandem with equality reflection we could easily
+ write a classic Y combinator, sending the compiler into a loop.
+\end{itemize}
+
+Given these facts theories employing equality reflection, like NuPRL
+\citep{NuPRL}, carry the derivations that gave rise to each typing judgement
+to keep the systems manageable. % TODO more info, problems with that.
+
+For all its faults, equality reflection does allow us to prove extensionality,
+using the extensions we gave above. Assuming that $\myctx$ contains
+\[\myb{A}, \myb{B} : \mytyp; \myb{f}, \myb{g} : \myb{A} \myarr \myb{B}; \myb{q} : \myfora{\myb{x}}{\myb{A}}{\myapp{\myb{f}}{\myb{x}} \mypeq{} \myapp{\myb{g}}{\myb{x}}}\]
+We can then derive
+\begin{prooftree}
+ \AxiomC{$\myjudd{\myctx; \myb{x} : \myb{A}}{\myapp{\myb{q}}{\myb{x}}}{\myapp{\myb{f}}{\myb{x}} \mypeq{} \myapp{\myb{g}}{\myb{x}}}$}
+ \RightLabel{equality reflection}
+ \UnaryInfC{$\myjudd{\myctx; \myb{x} : \myb{A}}{\myapp{\myb{f}}{\myb{x}} \mydefeq \myapp{\myb{g}}{\myb{x}}}{\myb{B}}$}
+ \RightLabel{congruence for $\lambda$s}
+ \UnaryInfC{$\myjud{(\myabs{\myb{x}}{\myapp{\myb{f}}{\myb{x}}}) \mydefeq (\myabs{\myb{x}}{\myapp{\myb{g}}{\myb{x}}})}{\myb{A} \myarr \myb{B}}$}
+ \RightLabel{$\eta$-law for $\lambda$}
+ \UnaryInfC{$\myjud{\myb{f} \mydefeq \myb{g}}{\myb{A} \myarr \myb{B}}$}
+ \RightLabel{$\myrefl$}
+ \UnaryInfC{$\myjud{\myapp{\myrefl}{\myb{f}}}{\myb{f} \mypeq{} \myb{g}}$}
+\end{prooftree}
+
+Now, the question is: do we need to give up well-behavedness of our theory to
+gain extensionality?
+
+\subsection{Observational equality}
+\ref{sec:ott}
+
+% TODO should we explain this in detail?
+A recent development by \citet{Altenkirch2007}, \emph{Observational Type
+ Theory} (OTT), promises to keep the well behavedness of ITT while being able
+to gain many useful equality proofs\footnote{It is suspected that OTT gains
+ \emph{all} the equality proofs of ETT, but no proof exists yet.}, including
+function extensionality. The main idea is to give the user the possibility to
+\emph{coerce} (or transport) values from a type $\mytya$ to a type $\mytyb$,
+if the type checker can prove structurally that $\mytya$ and $\mytya$ are
+equal; and providing a value-level equality based on similar principles. A
+brief overview is given below,
+
+\mydesc{syntax}{ }{
+ $
+ \begin{array}{r@{\ }c@{\ }l}
+ \mytmsyn & ::= & \dots \\
+ & | & \myprdec{\myprsyn} \mysynsep
+ \mycoee{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \mysynsep
+ \mycohh{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
+ \myprsyn & ::= & \mybot \mysynsep \mytop \mysynsep \myprsyn \myand \myprsyn
+ \mysynsep \myprfora{\myb{x}}{\mytmsyn}{\myprsyn} \\\
+ & | & \mytmsyn = \mytmsyn \mysynsep
+ \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn}
+ \end{array}
+ $
+}
+\mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
+ \centering{
+ }
+}
+
+The original presentation of OTT employs the theory presented above. It is
+close to the one presented in section \ref{sec:itt}, with the additions
+presented above, and the change that only one the `first' universe, the type
+of small types ($\mytyp_0$), is present.
+
+The propositional universe is meant to be where equality proofs live in. The
+equality proofs are respectively between types ($\mytya = \mytyb$), and
+between values
+
+
+
+However, only one universe is present ($\mytyp_0$), and a \emph{propositional}
+universe is isolated, intended to be the universe where equality proofs live
+in. Propositions (as long as our system is consistent) are inhabited only by
+one element, and thus can all be treated as definitionally equal.
+
+
+
+\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}
+\mykant is an interactive theorem prover developed as part of this thesis.
+The plan is to present a core language which would be capable of serving as
+the basis for a more featureful system, while still presenting interesting
+features and more importantly observational equality.
+
+The author learnt the hard way the implementations challenges for such a
+project, and while there is a solid and working base to work on, observational
+equality is not currently implemented. However, a detailed plan on how to add
+it this functionality is provided, and should not prove to be too much work.
+
+\subsection{High level overview}
+
+\subsubsection{Features}
+
+The features currently implemented in \mykant are:
+
+\begin{description}
+\item[Full dependent types] As we would expect, we have dependent a system
+ which is as expressive as the `best' corner in the lambda cube described in
+ section \ref{sec:itt}.
+
+\item[Implicit, cumulative universe hierarchy] The user does not need to
+ specify universe level explicitly, and universes are \emph{cumulative}.
+
+\item[User defined data types and records] Instead of forcing the user to
+ choose from a restricted toolbox, we let her define inductive data types,
+ with associated primitive recursion operators; or records, with associated
+ projections for each field.
+
+\item[Bidirectional type checking] While no `fancy' inference via unification
+ is present, we take advantage of an type synthesis system in the style of
+ \cite{Pierce2000}, extending the concept for user defined data types.
+
+\item[Type holes] When building up programs interactively, it is useful to
+ leave parts unfinished while exploring the current context. This is what
+ type holes are for.
+\end{description}
+
+The planned features are:
+
+\begin{description}
+\item[Observational equality] As described in section \label{sec:ott} but
+ extended to work with the type hierarchy and to admit equality between
+ arbitrary data types.
+
+\item[Coinductive data] ...
+\end{description}
+
+We will analyse the features one by one, along with motivations and tradeoffs
+for the design decisions made.
+
+\subsubsection{Implementation}
+
+The codebase consists of around 2500 lines of Haskell, as reported by the
+\texttt{cloc} utility. The high level design is heavily inspired by Conor
+McBride's work on various incarnations of Epigram, and specifically by the
+first version as described \citep{McBride2004} and the codebase for the new
+version \footnote{Available intermittently as a \texttt{darcs} repository at
+ \url{http://sneezy.cs.nott.ac.uk/darcs/Pig09}.}. In many ways \mykant is
+something in between the first and second version of Epigram.
+
+The interaction happens in a read-eval-print loop (REPL). The repl is a
+available both as a commandline application and in a web interface, which is
+available at \url{kant.mazzo.li} and presents itself as in figure
+\ref{fig:kant-web}.
+
+\begin{figure}
+ \centering{
+ \includegraphics[scale=1.0]{kant-web.png}
+ }
+ \caption{The \mykant web prompt.}
+ \label{fig:kant-web}
+\end{figure}
+
+The interaction with the user takes place in a loop living in and updating a
+context \mykant declarations. The user inputs a new declaration that goes
+through various stages starts with the user inputing a \mykant declaration,
+which then goes through various stages that can end up in a context update, or
+in failures of various kind. The process is described in figure
+\ref{fig:kant-process}. The workings of each phase will be illustrated in the
+next sections.
+
+\begin{figure}
+ {\small
+ \tikzstyle{block} = [rectangle, draw, text width=5em, text centered, rounded
+ corners, minimum height=2.5em, node distance=0.7cm]
+
+ \tikzstyle{decision} = [diamond, draw, text width=4.5em, text badly
+ centered, inner sep=0pt, node distance=0.7cm]
+
+ \tikzstyle{line} = [draw, -latex']
+
+ \tikzstyle{cloud} = [draw, ellipse, minimum height=2em, text width=5em, text
+ centered, node distance=1.5cm]
+
+
+ \begin{tikzpicture}[auto]
+ \node [cloud] (user) {User};
+ \node [block, below left=1cm and 0.1cm of user] (parse) {Parse};
+ \node [block, below=of parse] (desugar) {Desugar};
+ \node [block, below=of desugar] (reference) {Reference};
+ \node [block, below=of reference] (elaborate) {Elaborate};
+ \node [block, below=of elaborate] (tycheck) {Typecheck};
+ \node [decision, right=of elaborate] (error) {Error?};
+ \node [block, right=of parse] (distill) {Distill};
+ \node [block, right=of desugar] (update) {Update context};
+
+ \path [line] (user) -- (parse);
+ \path [line] (parse) -- (desugar);
+ \path [line] (desugar) -- (reference);
+ \path [line] (reference) -- (elaborate);
+ \path [line] (elaborate) edge[bend right] (tycheck);
+ \path [line] (tycheck) edge[bend right] (elaborate);
+ \path [line] (elaborate) -- (error);
+ \path [line] (error) edge[out=0,in=0] node [near start] {yes} (distill);
+ \path [line] (error) -- node [near start] {no} (update);
+ \path [line] (update) -- (distill);
+ \path [line] (distill) -- (user);
+
+
+ \end{tikzpicture}
+ }
+ \caption{High level overview of the life of a \mykant prompt cycle.}
+ \label{fig:kant-process}
+\end{figure}
+
+\subsection{Bidirectional type checking}
+
+We start by describing bidirectional type checking since it calls for fairly
+different typing rules that what we have seen up to now. The idea is to have
+two kind of terms: terms for which a type can always be inferred, and terms
+that need to be checked against a type. A nice observation is that this
+duality runs through the semantics of the terms: data destructors (function
+application, record projections, primitive recursors) \emph{infer} types,
+while data constructors (abstractions, record/data types data constructors)
+need to be checked.
+
+To introduce the concept and notation, we will revisit the STLC in a
+bidirectional style.
+
\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}}{
+ \centering{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. \\
+ $\mytyc{Sans}$ & Type constructors. \\
+ $\mydc{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.
+ $\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
+ 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))
+
+ data _≡_ {a} {A : Set a} : A → A → Set a where
+ refl : ∀ x → x ≡ x
+
+ J : ∀ {a b} {A : Set a}
+ (P : (x y : A) → x ≡ y → Set b) →
+ ∀ {x y} → P x x (refl x) → (x≡y : x ≡ y) → P x y x≡y
+ J P p (refl x) = p
+
+ subst : ∀ {a b} {A : Set a}
+ (P : A → Set b) →
+ ∀ {x y} → (x≡y : x ≡ y) → P x → P y
+ subst P q p = J (λ _ y _ → P y) p q
\end{code}
\nocite{*}
projects / bitonic-mengthesis.git / blobdiff