...

[bitonic-mengthesis.git] / thesis.lagda

\documentclass[11pt, fleqn]{article}
\usepackage{etex}

\usepackage[sc,slantedGreek]{mathpazo}
% \linespread{1.05}
% \usepackage{times}

\oddsidemargin  0in
\evensidemargin 0in
\textheight 9.5in 
\textwidth      6.2in
\topmargin      -7mm  
%% \parindent   10pt

\headheight 0pt
\headsep 0pt


%% Narrow margins
% \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}

%% Subfigure
\usepackage{subcaption}

\usepackage{verbatim}
\usepackage{fancyvrb}

\RecustomVerbatimEnvironment
  {Verbatim}{Verbatim}
  {xleftmargin=9mm}

%% diagrams
\usepackage{tikz}
\usetikzlibrary{shapes,arrows,positioning}
% \usepackage{tikz-cd}
% \usepackage{pgfplots}


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

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

\renewenvironment{code}%
{\noindent\ignorespaces\advance\leftskip\mathindent\AgdaCodeStyle\pboxed\small}%
{\endpboxed\par\noindent%
\ignorespacesafterend\small}


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

\newcommand{\mysmall}{}
\newcommand{\mysyn}{\AgdaKeyword}
\newcommand{\mytyc}{\AgdaDatatype}
\newcommand{\mydc}{\AgdaInductiveConstructor}
\newcommand{\myfld}{\AgdaField}
\newcommand{\myfun}{\AgdaFunction}
\newcommand{\myb}[1]{\AgdaBound{$#1$}}
\newcommand{\myfield}{\AgdaField}
\newcommand{\myind}{\AgdaIndent}
\newcommand{\mykant}{\textsc{Bertus}}
\newcommand{\mysynel}[1]{#1}
\newcommand{\myse}{\mysynel}
\newcommand{\mytmsyn}{\mysynel{term}}
\newcommand{\mysp}{\ }
\newcommand{\myabs}[2]{\mydc{$\lambda$} #1 \mathrel{\mydc{$\mapsto$}} #2}
\newcommand{\myappsp}{\hspace{0.07cm}}
\newcommand{\myapp}[2]{#1 \myappsp #2}
\newcommand{\mysynsep}{\ \ |\ \ }
\newcommand{\myITE}[3]{\myfun{If}\, #1\, \myfun{Then}\, #2\, \myfun{Else}\, #3}
\newcommand{\mycumul}{\preceq}

\FrameSep0.2cm
\newcommand{\mydesc}[3]{
  \noindent
  \mbox{
    \parbox{\textwidth}{
      {\mysmall
        \vspace{0.2cm}
        \hfill \textbf{#1} $#2$
        \framebox[\textwidth]{
          \parbox{\textwidth}{
            \vspace{0.1cm}
            \centering{
              #3
            }
            \vspace{0.2cm}
          }
        }
        \vspace{0.2cm}
      }
    }
  }
}

\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}
\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}}
\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}{\varepsilon}
\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}{}
\newcommand{\myderivspp}{\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{\mynodee}{\mathbin{\mydc{$\lhd$}}}
\newcommand{\mynode}[2]{\mynodee_{#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]{\mathopen{\mytyc{$\llbracket$}} #1 \mathclose{\mytyc{$\rrbracket$}}}
\newcommand{\myand}{\mathrel{\mytyc{$\wedge$}}}
\newcommand{\mybigand}{\mathrel{\mytyc{$\bigwedge$}}}
\newcommand{\myprfora}[3]{\forall #1 {:} #2. #3}
\newcommand{\myimpl}{\mathrel{\mytyc{$\Rightarrow$}}}
\newcommand{\mybot}{\mytyc{$\bot$}}
\newcommand{\mytop}{\mytyc{$\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) \mathrel{\mytyc{=}} (#3 {:} #4)}
\newcommand{\myeq}{\mathrel{\mytyc{=}}}
\newcommand{\myprop}{\mytyc{Prop}}
\newcommand{\mytmup}{\mytmsyn\uparrow}
\newcommand{\mydefs}{\Delta}
\newcommand{\mynf}{\Downarrow}
\newcommand{\myinff}[3]{#1 \vdash #2 \Rightarrow #3}
\newcommand{\myinf}[2]{\myinff{\myctx}{#1}{#2}}
\newcommand{\mychkk}[3]{#1 \vdash #2 \Leftarrow #3}
\newcommand{\mychk}[2]{\mychkk{\myctx}{#1}{#2}}
\newcommand{\myann}[2]{#1 : #2}
\newcommand{\mydeclsyn}{\myse{decl}}
\newcommand{\myval}[3]{#1 : #2 \mapsto #3}
\newcommand{\mypost}[2]{\mysyn{abstract}\ #1 : #2}
\newcommand{\myadt}[4]{\mysyn{data}\ #1 #2\ \mysyn{where}\ #3\{ #4 \}}
\newcommand{\myreco}[4]{\mysyn{record}\ #1 #2\ \mysyn{where}\ \{ #4 \}}
\newcommand{\myelabt}{\vdash}
\newcommand{\myelabf}{\rhd}
\newcommand{\myelab}[2]{\myctx \myelabt #1 \myelabf #2}
\newcommand{\mytele}{\Delta}
\newcommand{\mytelee}{\delta}
\newcommand{\mydcctx}{\Gamma}
\newcommand{\mynamesyn}{\myse{name}}
\newcommand{\myvec}{\overrightarrow}
\newcommand{\mymeta}{\textsc}
\newcommand{\myhyps}{\mymeta{hyps}}
\newcommand{\mycc}{;}
\newcommand{\myemptytele}{\varepsilon}
\newcommand{\mymetagoes}{\Longrightarrow}
% \newcommand{\mytesctx}{\
\newcommand{\mytelesyn}{\myse{telescope}}
\newcommand{\myrecs}{\mymeta{recs}}
\newcommand{\myle}{\mathrel{\lcfun{$\le$}}}
\newcommand{\mylet}{\mysyn{let}}
\newcommand{\myhead}{\mymeta{head}}
\newcommand{\mytake}{\mymeta{take}}
\newcommand{\myix}{\mymeta{ix}}
\newcommand{\myapply}{\mymeta{apply}}
\newcommand{\mydataty}{\mymeta{datatype}}
\newcommand{\myisreco}{\mymeta{record}}
\newcommand{\mydcsep}{\ |\ }
\newcommand{\mytree}{\mytyc{Tree}}
\newcommand{\myproj}[1]{\myfun{$\pi_{#1}$}}
\newcommand{\mysigma}{\mytyc{$\Sigma$}}
\newcommand{\mynegder}{\vspace{-0.3cm}}
\newcommand{\myquot}{\Uparrow}
\newcommand{\mynquot}{\, \Downarrow}

\renewcommand{\[}{\begin{equation*}}
\renewcommand{\]}{\end{equation*}}
\newcommand{\mymacol}[2]{\text{\textcolor{#1}{$#2$}}}

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

\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
  \end{code}
  \fi

\begin{document}

\begin{titlepage}  
  \centering

  \maketitle
  \thispagestyle{empty}

  \begin{minipage}{0.4\textwidth}
  \begin{flushleft} \large
    \emph{Supervisor:}\\
    Dr. Steffen \textsc{van Bakel}
  \end{flushleft}
\end{minipage}
\begin{minipage}{0.4\textwidth}
  \begin{flushright} \large
    \emph{Co-marker:} \\
    Dr. Philippa \textsc{Gardner}
  \end{flushright}
\end{minipage}

\end{titlepage}

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

  Among this systems, Inutitionistic Type Theory (ITT) has been a very
  popular framework for theorem provers and programming languages.
  However, equality has always been a tricky business in ITT and related
  theories.

  In these thesis we will explain why this is the case, and present
  Observational Type Theory (OTT), a solution to some of the problems
  with equality.  We then describe $\mykant$, a theorem prover featuring
  OTT in a setting more close to the one found in current systems.
  Having implemented part of $\mykant$ as a Haskell program, we describe
  some of the implementation issues faced.
\end{abstract}

\clearpage

\renewcommand{\abstractname}{Acknowledgements}
\begin{abstract}
  I would like to thank Steffen van Backel, my supervisor, who was brave
  enough to believe in my project and who provided much advice and
  support.

  I would also like to thank the Haskell and Agda community on
  \texttt{IRC}, which guided me through the strange world of types; and
  in particular Andrea Vezzosi and James Deikun, with whom I entertained
  countless insightful discussions in the past year.  Andrea suggested
  Observational Type Theory as a topic of study: this thesis would not
  exist without him.  Before them, Tony Fields introduced me to Haskell,
  unknowingly filling most of my free time from that time on.

  Finally, much of the work stems from the research of Conor McBride,
  who answered many of my doubts through these months.  I also owe him
  the colours.
\end{abstract}

\clearpage

\tableofcontents

\clearpage

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

\subsection{The untyped $\lambda$-calculus}
\label{sec:untyped}

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{2}
    \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{2} \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 \cdots \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
declare its 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}}{
      \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:
\[
  \myapp{(\myabss{\myb{x}}{\myhole{?}}{\myapp{\myb{x}}{\myb{x}}})}{(\myabss{\myb{x}}{\myhole{?}}{\myapp{\myb{x}}{\myb{x}}})}
\]

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 ::= \cdots b \mysynsep \myfix{\myb{x}}{\mytysyn}{\mytmsyn} $
  \vspace{0.4cm}
}
\end{minipage} 
\begin{minipage}{0.5\textwidth}
\mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}} {
    \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytmt}{\mytya}$}
    \UnaryInfC{$\myjud{\myfix{\myb{x}}{\mytya}{\mytmt}}{\mytya}$}
    \DisplayProof
}
\end{minipage} 

\mydesc{reduction:}{\myjud{\mytmsyn}{\mytmsyn}}{
    $ \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 & ::= & \cdots \\
             &  |  & \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 & ::= & \cdots \mysynsep \myunit \mysynsep \myempty \mysynsep \mytmsyn \mysum \mytmsyn \mysynsep \mytysyn \myprod \mytysyn
  \end{array}
  $
}

\mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
    \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}}{
    \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}

  \myderivspp

    \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}

  \myderivspp

    \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}

  \myderivspp

    \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{\myarg}{\myarg}$ to $\vee$ elimination; for $\myprod$
$\mypair{\myarg}{\myarg}$ 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}.

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.
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}
\label{sec:ind-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 & ::= & \cdots \mysynsep \mynil{\mytysyn} \mysynsep \mytmsyn \mycons \mytmsyn
                     \mysynsep
                     \myapp{\myapp{\myapp{\myfoldr}{\mytmsyn}}{\mytmsyn}}{\mytmsyn} \\
    \mytysyn & ::= & \cdots \mysynsep \myapp{\mylist}{\mytysyn}
  \end{array}
  $
}
\mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
  $
  \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}}{
    \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}
  \myderivspp

    \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.

\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 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.  Agda and \mykant\
renditions of the presented theory and all the examples is reproduced in
appendix \ref{app:itt-code}.

\begin{figure}[t]
\mydesc{syntax}{ }{
  $
  \begin{array}{r@{\ }c@{\ }l}
    \mytmsyn & ::= & \myb{x} \mysynsep
                     \mytyp_{level} \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} \mysynsep
                     (\myapp{\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} \\
    level    & \in & \mathbb{N}
  \end{array}
  $
}

\mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
    \begin{tabular}{ccc}
      $
      \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}
      $
      &
    $
    \begin{array}{l@{ }l@{\ }c@{\ }l}
      \myapp{\myfst &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmm \\
      \myapp{\mysnd &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmn
    \end{array}
    $
    \end{tabular}

    \myderivspp

    $
    \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}}{
    \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, but it is possible to
employ $\myred$ to decide term equality in a systematic way, by always
reducing terms to their normal forms before comparing them, so that a
separate conversion rule is not needed.
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 : \cdots$.  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}.  However various techniques can be
employed to lift the burden of explicitly handling universes, as we will
see in Section \ref{sec:term-hierarchy}.

\subsubsection{Contexts}

\begin{minipage}{0.5\textwidth}
  \mydesc{context validity:}{\myvalid{\myctx}}{
      \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}}{
      \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}}{
    \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}}{
   \begin{tabular}{ccc}
     \AxiomC{}
     \UnaryInfC{$\myjud{\mybool}{\mytyp_0}$}
     \DisplayProof
     &
     \AxiomC{}
     \UnaryInfC{$\myjud{\mytrue}{\mybool}$}
     \DisplayProof
     &
     \AxiomC{}
      \UnaryInfC{$\myjud{\myfalse}{\mybool}$}
      \DisplayProof
    \end{tabular}
    \myderivspp

    \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 the `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}}{
     \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

     \myderivspp

    \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.
Following this intuition, in the introduction rule, the return type is
typechecked in a context with an abstracted variable of lhs' type, and
in the elimination rule the actual argument is substituted in the return
type.  Keeping the correspondence with logic alive, dependent functions
are much like universal quantifiers ($\forall$) in logic.

For example, assuming that we have lists and natural numbers in our
language, using dependent functions we would be able to
write:
\[
\begin{array}{l}
\myfun{length} : (\myb{A} {:} \mytyp_0) \myarr \myapp{\mylist}{\myb{A}} \myarr \mynat \\
\myarg \myfun{$>$} \myarg : \mynat \myarr \mynat \myarr \mytyp_0 \\
\myfun{head} : (\myb{A} {:} \mytyp_0) \myarr (\myb{l} {:} \myapp{\mylist}{\myb{A}})
               \myarr \myapp{\myapp{\myfun{length}}{\myb{A}}}{\myb{l}} \mathrel{\myfun{$>$}} 0 \myarr
               \myb{A}
\end{array}
\]

\myfun{length} is the usual polymorphic length
function. $\myarg\myfun{$>$}\myarg$ is a function that takes two naturals
and returns a type: if the lhs is greater then the rhs, $\myunit$ is
returned, $\myempty$ otherwise.  This way, we can express a
`non-emptyness' condition in $\myfun{head}$, by including a proof that
the length of the list argument is non-zero.  This allows us to rule out
the `empty list' case, so that we can safely return the first element.

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}$.

\subsubsection{$\myprod$, or dependent product}
\label{sec:disju}

\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
     \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

     \myderivspp

    \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}
}

If dependent functions are a generalisation of $\myarr$ in the STLC,
dependent products are a generalisation of $\myprod$ in the STLC.  The
improvement is that the second element's type can depend on the value of
the first element.  The corrispondence with logic is through the
existential quantifier: $\exists x \in \mathbb{N}. even(x)$ can be
expressed as $\myexi{\myb{x}}{\mynat}{\myapp{\myfun{even}}{\myb{x}}}$.
The first element will be a number, and the second evidence that the
number is even.  This highlights the fact that we are working in a
constructive logic: if we have an existence proof, we can always ask for
a witness.  This means, for instance, that $\neg \forall \neg$ is not
equivalent to $\exists$.

Another perhaps more `dependent' application of products, paired with
$\mybool$, is to offer choice between different types.  For example we
can easily recover disjunctions:
\[
\begin{array}{l}
  \myarg\myfun{$\vee$}\myarg : \mytyp_0 \myarr \mytyp_0 \myarr \mytyp_0 \\
  \myb{A} \mathrel{\myfun{$\vee$}} \myb{B} \mapsto \myexi{\myb{x}}{\mybool}{\myite{\myb{x}}{\myb{A}}{\myb{B}}} \\ \ \\
  \myfun{case} : (\myb{A}\ \myb{B}\ \myb{C} {:} \mytyp_0) \myarr (\myb{A} \myarr \myb{C}) \myarr (\myb{B} \myarr \myb{C}) \myarr \myb{A} \mathrel{\myfun{$\vee$}} \myb{B} \myarr \myb{C} \\
  \myfun{case} \myappsp \myb{A} \myappsp \myb{B} \myappsp \myb{C} \myappsp \myb{f} \myappsp \myb{g} \myappsp \myb{x} \mapsto \\
  \myind{2} \myapp{(\myitee{\myapp{\myfst}{\myb{x}}}{\myb{b}}{(\myite{\myb{b}}{\myb{A}}{\myb{B}})}{\myb{f}}{\myb{g}})}{(\myapp{\mysnd}{\myb{x}})}
\end{array}
\]

\subsubsection{$\mytyc{W}$, or well-order}
\label{sec:well-order}

\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
  \begin{tabular}{cc}
     \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

     &

     \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
   \end{tabular}

     \myderivspp

     \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
}

Finally, the well-order type, or in short $\mytyc{W}$-type, which will
let us represent inductive data in a general (but clumsy) way.  We can
form `nodes' of the shape $\mytmt \mynode{\myb{x}}{\mytyb} \myse{f} :
\myw{\myb{x}}{\mytya}{\mytyb}$ that contain data ($\mytmt$) of type and
one `child' for each member of $\mysub{\mytyb}{\myb{x}}{\mytmt}$.  The
$\myfun{rec}\ \myfun{with}$ acts as an induction principle on
$\mytyc{W}$, given a predicate an a function dealing with the inductive
case---we will gain more intuition about inductive data in ITT in
Section \ref{sec:user-type}.

For example, if we want to form natural numbers, we can take
\[
  \begin{array}{@{}l}
    \mytyc{Tr} : \mybool \myarr \mytyp_0 \\
    \mytyc{Tr} \myappsp \myb{b} \mapsto \myfun{if}\, \myb{b}\, \myunit\, \myfun{else}\, \myempty \\
    \ \\
    \mynat : \mytyp_0 \\
    \mynat \mapsto \myw{\myb{b}}{\mybool}{(\mytyc{Tr}\myappsp\myb{b})}
  \end{array}
\]
Each node will contain a boolean.  If $\mytrue$, the number is non-zero,
and we will have one child representing its predecessor, given that
$\mytyc{Tr}$ will return $\myunit$.  If $\myfalse$, the number is zero,
and we will have no predecessors (children), given the $\myempty$:
\[
  \begin{array}{@{}l}
    \mydc{zero} : \mynat \\
    \mydc{zero} \mapsto \myfalse \mynodee (\myabs{\myb{z}}{\myabsurd{\mynat} \myappsp \myb{x}}) \\
    \ \\
    \mydc{suc} : \mynat \myarr \mynat \\
    \mydc{suc}\myappsp \myb{x} \mapsto \mytrue \mynodee (\myabs{\myarg}{\myb{x}})
  \end{array}
\]
And with a bit of effort, we can recover addition:
\[
  \begin{array}{@{}l}
    \myfun{plus} : \mynat \myarr \mynat \myarr \mynat \\
    \myfun{plus} \myappsp \myb{x} \myappsp \myb{y} \mapsto \\
    \myind{2} \myfun{rec}\, \myb{x} / \myb{b}.\mynat \, \\
    \myind{2} \myfun{with}\, \myabs{\myb{b}}{\\
      \myind{2}\myind{2}\myfun{if}\, \myb{b} / \myb{b'}.((\mytyc{Tr} \myappsp \myb{b'} \myarr \mynat) \myarr (\mytyc{Tr} \myappsp \myb{b'} \myarr \mynat) \myarr \mynat) \\
      \myind{2}\myind{2}\myfun{then}\,(\myabs{\myarg\, \myb{f}}{\mydc{suc}\myappsp (\myapp{\myb{f}}{\mytt})})\, \myfun{else}\, (\myabs{\myarg\, \myarg}{\myb{y}})}
  \end{array}
  \]
Note how we explicitly have to type the branches to make them
match with the definition of $\mynat$---which gives a taste of the
`clumsiness' of $\mytyc{W}$-types, which while useful as a reasoning
tool are useless to the user modelling data types.

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

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.  As in the previous section, everything presented is
formalised in Agda in appendix \ref{app:agda-itt}.

\subsection{Propositional equality}

\noindent
\begin{minipage}{0.5\textwidth}
\mydesc{syntax}{ }{
  $
  \begin{array}{r@{\ }c@{\ }l}
    \mytmsyn & ::= & \cdots \\
             &  |  & \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}{
    $
    \myjeq{\myse{P}}{(\myapp{\myrefl}{\mytmm})}{\mytmn} \myred \mytmn
    $
  \vspace{1.1cm}
}
\end{minipage}
\mynegder
\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
    \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
    \AxiomC{$\myjud{\mytmm}{\mytya}$}
    \AxiomC{$\myjud{\mytmn}{\mytya}$}
    \TrinaryInfC{$\myjud{\mytmm \mypeq{\mytya} \mytmn}{\mytyp_l}$}
    \DisplayProof

    \myderivspp

    \begin{tabular}{cc}
      \AxiomC{$\begin{array}{c}\ \\\myjud{\mytmm}{\mytya}\hspace{1.1cm}\mytmm \mydefeq \mytmn\end{array}$}
      \UnaryInfC{$\myjud{\myapp{\myrefl}{\mytmm}}{\mytmm \mypeq{\mytya} \mytmn}$}
      \DisplayProof
      &
      \AxiomC{$
        \begin{array}{c}
          \myjud{\myse{P}}{\myfora{\myb{x}\ \myb{y}}{\mytya}{\myfora{q}{\myb{x} \mypeq{\mytya} \myb{y}}{\mytyp_l}}} \\
          \myjud{\myse{q}}{\mytmm \mypeq{\mytya} \mytmn}\hspace{1.1cm}\myjud{\myse{p}}{\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmm}}{(\myapp{\myrefl}{\mytmm})}}
        \end{array}
        $}
      \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.

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}$
  twice, 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}
\myfun{subst} : \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}}}}} \\
\myfun{subst}\myappsp \myb{A}\myappsp\myb{P}\myappsp\myb{x}\myappsp\myb{y}\myappsp\myb{q}\myappsp\myb{p} \mapsto
  \myjeq{(\myabs{\myb{x}\ \myb{y}\ \myb{q}}{\myapp{\myb{P}}{\myb{y}}})}{\myb{p}}{\myb{q}}
\end{array}
\]
Once we have $\myfun{subst}$, we can easily prove more familiar laws regarding
equality, such as symmetry, transitivity, congruence laws, etc.

\subsection{Common extensions}

Our definitional and propositional equalities can be enhanced in various
ways.  Obviously if we extend the definitional equality we are also
automatically extend propositional equality, given how $\myrefl$ works.

\subsubsection{$\eta$-expansion}
\label{sec:eta-expand}

A simple extension to our definitional equality is $\eta$-expansion.
Given an abstract variable $\myb{f} : \mytya \myarr \mytyb$ the aim is
to have that $\myb{f} \mydefeq
\myabss{\myb{x}}{\mytya}{\myapp{\myb{f}}{\myb{x}}}$.  We can achieve
this by `expanding' terms based on their types, a process also known as
\emph{quotation}---a term borrowed from the practice of
\emph{normalisation by evaluation}, where we embed terms in some host
language with an existing notion of computation, and then reify them
back into terms, which will `smooth out' differences like the one above
\citep{Abel2007}.

The same concept applies to $\myprod$, where we expand each inhabitant
by reconstructing it by getting its projections, so that $\myb{x}
\mydefeq \mypair{\myfst \myappsp \myb{x}}{\mysnd \myappsp \myb{x}}$.
Similarly, all one inhabitants of $\myunit$ and all zero inhabitants of
$\myempty$ can be considered equal. Quotation can be performed in a
type-directed way, as we will witness in Section \ref{sec:kant-irr}.

To justify this process in our type system we will add a congruence law
for abstractions and a similar law for products, plus the fact that all
elements of $\myunit$ or $\myempty$ are equal.

\mydesc{definitional equality:}{\myjud{\mytmm \mydefeq \mytmn}{\mytmsyn}}{
  \begin{tabular}{cc}
    \AxiomC{$\myjudd{\myctx; \myb{y} : \mytya}{\myapp{\myse{f}}{\myb{x}} \mydefeq \myapp{\myse{g}}{\myb{x}}}{\mysub{\mytyb}{\myb{x}}{\myb{y}}}$}
    \UnaryInfC{$\myjud{\myse{f} \mydefeq \myse{g}}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
    \DisplayProof
    &
    \AxiomC{$\myjud{\mypair{\myapp{\myfst}{\mytmm}}{\myapp{\mysnd}{\mytmm}} \mydefeq \mypair{\myapp{\myfst}{\mytmn}}{\myapp{\mysnd}{\mytmn}}}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
    \UnaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
    \DisplayProof
  \end{tabular}

  \myderivspp

  \begin{tabular}{cc}
  \AxiomC{$\myjud{\mytmm}{\myunit}$}
  \AxiomC{$\myjud{\mytmn}{\myunit}$}
  \BinaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\myunit}$}
  \DisplayProof
  &
  \AxiomC{$\myjud{\mytmm}{\myempty}$}
  \AxiomC{$\myjud{\mytmn}{\myempty}$}
  \BinaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\myempty}$}
  \DisplayProof
  \end{tabular}
}

\subsubsection{Uniqueness of identity proofs}

Another common but controversial addition to propositional equality is
the $\myfun{K}$ axiom, which essentially states that all equality proofs
are by reflexivity.

\mydesc{typing:}{\myjud{\mytmm \mydefeq \mytmn}{\mytmsyn}}{
  \AxiomC{$
    \begin{array}{@{}c}
      \myjud{\myse{P}}{\myfora{\myb{x}}{\mytya}{\myb{x} \mypeq{\mytya} \myb{x} \myarr \mytyp}} \\\
      \myjud{\mytmt}{\mytya} \hspace{1cm}
      \myjud{\myse{p}}{\myse{P} \myappsp \mytmt \myappsp (\myrefl \myappsp \mytmt)} \hspace{1cm}
      \myjud{\myse{q}}{\mytmt \mypeq{\mytya} \mytmt}
    \end{array}
    $}
  \UnaryInfC{$\myjud{\myfun{K} \myappsp \myse{P} \myappsp \myse{t} \myappsp \myse{p} \myappsp \myse{q}}{\myse{P} \myappsp \mytmt \myappsp \myse{q}}$}
  \DisplayProof
}

\cite{Hofmann1994} showed that $\myfun{K}$ is not derivable from the
$\myjeqq$ axiom that we presented, and \cite{McBride2004} showed that it is
needed to implement `dependent pattern matching', as first proposed by
\cite{Coquand1992}.  Thus, $\myfun{K}$ is derivable in the systems that
implement dependent pattern matching, such as Epigram and Agda; but for
example not in Coq.

$\myfun{K}$ is controversial mainly because it is at odds with
equalities that include computational behaviour, most notably
Voevodsky's `Univalent Foundations', which includes a \emph{univalence}
axiom that identifies isomorphisms between types with propositional
equality.  For example we would have two isomorphisms, and thus two
equalities, between $\mybool$ and $\mybool$, corresponding to the two
permutations---one is the identity, and one swaps the elements.  Given
this, $\myfun{K}$ and univalence are inconsistent, and thus a form of
dependent pattern matching that does not imply $\myfun{K}$ is subject of
research.\footnote{More information about univalence can be found at
  \url{http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations.html}.}

\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 extensionally equal, 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}}{
    \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, since we derive any
  equality proof and then use equality reflection and the conversion
  rule to have terms of any type.
\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.

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}
  \mysmall
  \AxiomC{$\hspace{1.1cm}\myjudd{\myctx; \myb{x} : \myb{A}}{\myapp{\myb{q}}{\myb{x}}}{\myapp{\myb{f}}{\myb{x}} \mypeq{} \myapp{\myb{g}}{\myb{x}}}\hspace{1.1cm}$}
  \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{$\hspace{1.45cm}\myjud{\myb{f} \mydefeq \myb{g}}{\myb{A} \myarr \myb{B}}\hspace{1.45cm}$}
  \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{Some alternatives}

% TODO finish
% TODO add `extentional axioms' (Hoffman), setoid models (Thorsten)

\section{Observational equality}
\label{sec:ott}

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.  Here we give an
exposition which follows closely the original paper.

\subsection{A simpler theory, a propositional fragment}

\mydesc{syntax}{ }{
    $\mytyp_l$ is replaced by $\mytyp$. \\\ \\
    $
    \begin{array}{r@{\ }c@{\ }l}
      \mytmsyn & ::= & \cdots \mysynsep \myprdec{\myprsyn} \mysynsep
                       \myITE{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
      \myprsyn & ::= & \mybot \mysynsep \mytop \mysynsep \myprsyn \myand \myprsyn
      \mysynsep \myprfora{\myb{x}}{\mytmsyn}{\myprsyn}
    \end{array}
    $
}

\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
  \begin{tabular}{cc}
    \AxiomC{$\myjud{\myse{P}}{\myprop}$}
    \UnaryInfC{$\myjud{\myprdec{\myse{P}}}{\mytyp}$}
    \DisplayProof
    &
    \AxiomC{$\myjud{\mytmt}{\mybool}$}
    \AxiomC{$\myjud{\mytya}{\mytyp}$}
    \AxiomC{$\myjud{\mytyb}{\mytyp}$}
    \TrinaryInfC{$\myjud{\myITE{\mytmt}{\mytya}{\mytyb}}{\mytyp}$}
    \DisplayProof
  \end{tabular}
}

\mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
    \begin{tabular}{ccc}
      \AxiomC{\phantom{$\myjud{\myse{P}}{\myprop}$}}
      \UnaryInfC{$\myjud{\mytop}{\myprop}$}
      \noLine
      \UnaryInfC{$\myjud{\mybot}{\myprop}$}
      \DisplayProof
      &
      \AxiomC{$\myjud{\myse{P}}{\myprop}$}
      \AxiomC{$\myjud{\myse{Q}}{\myprop}$}
      \BinaryInfC{$\myjud{\myse{P} \myand \myse{Q}}{\myprop}$}
      \noLine
      \UnaryInfC{\phantom{$\myjud{\mybot}{\myprop}$}}
      \DisplayProof
      &
      \AxiomC{$\myjud{\myse{A}}{\mytyp}$}
      \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\myse{P}}{\myprop}$}
      \BinaryInfC{$\myjud{\myprfora{\myb{x}}{\mytya}{\myse{P}}}{\myprop}$}
      \noLine
      \UnaryInfC{\phantom{$\myjud{\mybot}{\myprop}$}}
      \DisplayProof
    \end{tabular}
}

Our foundation will be a type theory like the one of section
\ref{sec:itt}, with only one level: $\mytyp_0$.  In this context we will
drop the $0$ and call $\mytyp_0$ $\mytyp$.  Moreover, since the old
$\myfun{if}\myarg\myfun{then}\myarg\myfun{else}$ was able to return
types thanks to the hierarchy (which is gone), we need to reintroduce an
ad-hoc conditional for types, where the reduction rule is the obvious
one.

However, we have an addition: a universe of \emph{propositions},
$\myprop$.  $\myprop$ isolates a fragment of types at large, and
indeed we can `inject' any $\myprop$ back in $\mytyp$ with $\myprdec{\myarg}$: \\
\mydesc{proposition decoding:}{\myprdec{\mytmsyn} \myred \mytmsyn}{
    \begin{tabular}{cc}
    $
    \begin{array}{l@{\ }c@{\ }l}
      \myprdec{\mybot} & \myred & \myempty \\
      \myprdec{\mytop} & \myred & \myunit
    \end{array}
    $
    &
    $
    \begin{array}{r@{ }c@{ }l@{\ }c@{\ }l}
      \myprdec{&\myse{P} \myand \myse{Q} &} & \myred & \myprdec{\myse{P}} \myprod \myprdec{\myse{Q}} \\
      \myprdec{&\myprfora{\myb{x}}{\mytya}{\myse{P}} &} & \myred &
             \myfora{\myb{x}}{\mytya}{\myprdec{\myse{P}}}
    \end{array}
    $
    \end{tabular}
  } \\
  Propositions are what we call the types of \emph{proofs}, or types
  whose inhabitants contain no `data', much like $\myunit$.  The goal of
  doing this is twofold: erasing all top-level propositions when
  compiling; and to identify all equivalent propositions as the same, as
  we will see later.

  Why did we choose what we have in $\myprop$?  Given the above
  criteria, $\mytop$ obviously fits the bill.  A pair of propositions
  $\myse{P} \myand \myse{Q}$ still won't get us data. Finally, if
  $\myse{P}$ is a proposition and we have
  $\myprfora{\myb{x}}{\mytya}{\myse{P}}$ , the decoding will be a
  function which returns propositional content.  The only threat is
  $\mybot$, by which we can fabricate anything we want: however if we
  are consistent there will be nothing of type $\mybot$ at the top
  level, which is what we care about regarding proof erasure.

\subsection{Equality proofs}

\mydesc{syntax}{ }{
    $
    \begin{array}{r@{\ }c@{\ }l}
      \mytmsyn & ::= & \cdots \mysynsep
      \mycoee{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \mysynsep
      \mycohh{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
      \myprsyn & ::= & \cdots \mysynsep \mytmsyn \myeq \mytmsyn \mysynsep
      \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn}
    \end{array}
    $
}

\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
  \begin{tabular}{cc}
    \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
    \AxiomC{$\myjud{\mytmt}{\mytya}$}
    \BinaryInfC{$\myjud{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}$}
    \DisplayProof
    &
  \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
  \AxiomC{$\myjud{\mytmt}{\mytya}$}
  \BinaryInfC{$\myjud{\mycohh{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\myprdec{\myjm{\mytmt}{\mytya}{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}}}$}
  \DisplayProof

  \end{tabular}
}

\mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
    \begin{tabular}{cc}
      \AxiomC{$
        \begin{array}{l}
          \ \\
          \myjud{\myse{A}}{\mytyp} \hspace{1cm} \myjud{\myse{B}}{\mytyp}
        \end{array}
        $}
      \UnaryInfC{$\myjud{\mytya \myeq \mytyb}{\myprop}$}
      \DisplayProof
      &
      \AxiomC{$
        \begin{array}{c}
          \myjud{\myse{A}}{\mytyp} \hspace{1cm} \myjud{\mytmm}{\myse{A}} \\
          \myjud{\myse{B}}{\mytyp} \hspace{1cm} \myjud{\mytmn}{\myse{B}}
        \end{array}
        $}
    \UnaryInfC{$\myjud{\myjm{\mytmm}{\myse{A}}{\mytmn}{\myse{B}}}{\myprop}$}
    \DisplayProof

    \end{tabular}
}


While isolating a propositional universe as presented can be a useful
exercises on its own, what we are really after is a useful notion of
equality.  In OTT we want to maintain the notion that things judged to
be equal are still always repleaceable for one another with no
additional changes.  Note that this is not the same as saying that they
are definitionally equal, since as we saw extensionally equal functions,
while satisfying the above requirement, are not definitionally equal.

Towards this goal we introduce two equality constructs in
$\myprop$---the fact that they are in $\myprop$ indicates that they
indeed have no computational content.  The first construct, $\myarg
\myeq \myarg$, relates types, the second,
$\myjm{\myarg}{\myarg}{\myarg}{\myarg}$, relates values.  The
value-level equality is different from our old propositional equality:
instead of ranging over only one type, we might form equalities between
values of different types---the usefulness of this construct will be
clear soon.  In the literature this equality is known as `heterogeneous'
or `John Major', since

\begin{quote}
  John Major's `classless society' widened people's aspirations to
  equality, but also the gap between rich and poor. After all, aspiring
  to be equal to others than oneself is the politics of envy. In much
  the same way, forms equations between members of any type, but they
  cannot be treated as equals (ie substituted) unless they are of the
  same type. Just as before, each thing is only equal to
  itself. \citep{McBride1999}.
\end{quote}

Correspondingly, at the term level, $\myfun{coe}$ (`coerce') lets us
transport values between equal types; and $\myfun{coh}$ (`coherence')
guarantees that $\myfun{coe}$ respects the value-level equality, or in
other words that it really has no computational component: if we
transport $\mytmm : \mytya$ to $\mytmn : \mytyb$, $\mytmm$ and $\mytmn$
will still be the same.

Before introducing the core ideas that make OTT work, let us distinguish
between \emph{canonical} and \emph{neutral} types.  Canonical types are
those arising from the ground types ($\myempty$, $\myunit$, $\mybool$)
and the three type formers ($\myarr$, $\myprod$, $\mytyc{W}$).  Neutral
types are those formed by
$\myfun{If}\myarg\myfun{Then}\myarg\myfun{Else}\myarg$.
Correspondingly, canonical terms are those inhabiting canonical types
($\mytt$, $\mytrue$, $\myfalse$, $\myabss{\myb{x}}{\mytya}{\mytmt}$,
...), and neutral terms those formed by eliminators.\footnote{Using the
  terminology from Section \ref{sec:types}, we'd say that canonical
  terms are in \emph{weak head normal form}.}  In the current system
(and hopefully in well-behaved systems), all closed terms reduce to a
canonical term, and all canonical types are inhabited by canonical
terms.

\subsubsection{Type equality, and coercions}

The plan is to decompose type-level equalities between canonical types
into decodable propositions containing equalities regarding the
subterms, and to use coerce recursively on the subterms using the
generated equalities.  This interplay between type equalities and
\myfun{coe} ensures that invocations of $\myfun{coe}$ will vanish when
we have evidence of the structural equality of the types we are
transporting terms across.  If the type is neutral, the equality won't
reduce and thus $\myfun{coe}$ won't reduce either.  If we come an
equality between different canonical types, then we reduce the equality
to bottom, making sure that no such proof can exist, and providing an
`escape hatch' in $\myfun{coe}$.

\begin{figure}[t]

\mydesc{equality reduction:}{\myprsyn \myred \myprsyn}{
    $
      \begin{array}{c@{\ }c@{\ }c@{\ }l}
        \myempty & \myeq & \myempty & \myred \mytop \\
        \myunit  & \myeq &  \myunit & \myred  \mytop \\
        \mybool  & \myeq &  \mybool &   \myred  \mytop \\
        \myexi{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myexi{\myb{x_2}}{\mytya_2}{\mytya_2} & \myred \\
        \multicolumn{4}{l}{
          \myind{2} \mytya_1 \myeq \mytyb_1 \myand 
                  \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{\myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2}} \myimpl \mytyb_1[\myb{x_1}] \myeq \mytyb_2[\myb{x_2}]}
                  } \\
      \myfora{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myfora{\myb{x_2}}{\mytya_2}{\mytyb_2} & \myred \cdots \\
      \myw{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myw{\myb{x_2}}{\mytya_2}{\mytyb_2} & \myred \cdots \\
      \mytya & \myeq & \mytyb & \myred \mybot\ \text{if $\mytya$ and $\mytyb$ are canonical.}
      \end{array}
    $
}
\myderivsp
\mydesc{reduction}{\mytmsyn \myred \mytmsyn}{
  $
  \begin{array}[t]{@{}l@{\ }l@{\ }l@{\ }l@{\ }l@{\ }c@{\ }l@{\ }}
    \mycoe & \myempty & \myempty & \myse{Q} & \myse{t} & \myred & \myse{t} \\
    \mycoe & \myunit  & \myunit  & \myse{Q} & \myse{t} & \myred & \mytt \\
    \mycoe & \mybool  & \mybool  & \myse{Q} & \mytrue & \myred & \mytrue \\
    \mycoe & \mybool  & \mybool  & \myse{Q} & \myfalse & \myred & \myfalse \\
    \mycoe & (\myexi{\myb{x_1}}{\mytya_1}{\mytyb_1}) &
             (\myexi{\myb{x_2}}{\mytya_2}{\mytyb_2}) & \myse{Q} &
             \mytmt_1 & \myred & \\
             \multicolumn{7}{l}{
             \myind{2}\begin{array}[t]{l@{\ }l@{\ }c@{\ }l}
               \mysyn{let} & \myb{\mytmm_1} & \mapsto & \myapp{\myfst}{\mytmt_1} : \mytya_1 \\
                           & \myb{\mytmn_1} & \mapsto & \myapp{\mysnd}{\mytmt_1} : \mysub{\mytyb_1}{\myb{x_1}}{\myb{\mytmm_1}} \\
                           & \myb{Q_A}      & \mapsto & \myapp{\myfst}{\myse{Q}} : \mytya_1 \myeq \mytya_2 \\
                           & \myb{\mytmm_2} & \mapsto & \mycoee{\mytya_1}{\mytya_2}{\myb{Q_A}}{\myb{\mytmm_1}} : \mytya_2 \\
                           & \myb{Q_B}      & \mapsto & (\myapp{\mysnd}{\myse{Q}}) \myappsp \myb{\mytmm_1} \myappsp \myb{\mytmm_2} \myappsp (\mycohh{\mytya_1}{\mytya_2}{\myb{Q_A}}{\myb{\mytmm_1}}) : \myprdec{\mysub{\mytyb_1}{\myb{x_1}}{\myb{\mytmm_1}} \myeq \mysub{\mytyb_2}{\myb{x_2}}{\myb{\mytmm_2}}} \\
                           & \myb{\mytmn_2} & \mapsto & \mycoee{\mysub{\mytyb_1}{\myb{x_1}}{\myb{\mytmm_1}}}{\mysub{\mytyb_2}{\myb{x_2}}{\myb{\mytmm_2}}}{\myb{Q_B}}{\myb{\mytmn_1}} : \mysub{\mytyb_2}{\myb{x_2}}{\myb{\mytmm_2}} \\
               \mysyn{in}  & \multicolumn{3}{@{}l}{\mypair{\myb{\mytmm_2}}{\myb{\mytmn_2}}}
              \end{array}} \\

    \mycoe & (\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}) &
             (\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}) & \myse{Q} &
             \mytmt & \myred &
           \cdots \\

    \mycoe & (\myw{\myb{x_1}}{\mytya_1}{\mytyb_1}) &
             (\myw{\myb{x_2}}{\mytya_2}{\mytyb_2}) & \myse{Q} &
             \mytmt & \myred &
           \cdots \\

    \mycoe & \mytya & \mytyb & \myse{Q} & \mytmt & \myred & \myapp{\myabsurd{\mytyb}}{\myse{Q}}\ \text{if $\mytya$ and $\mytyb$ are canonical.}
  \end{array}
  $
}
\caption{Reducing type equalities, and using them when
  $\myfun{coe}$rcing.}
\label{fig:eqred}
\end{figure}

Figure \ref{fig:eqred} illustrates this idea in practice.  For ground
types, the proof is the trivial element, and \myfun{coe} is the
identity.  For $\myunit$, we can do better: we return its only member
without matching on the term.  For the three type binders, things are
similar but subtly different---the choices we make in the type equality
are dictated by the desire of writing the $\myfun{coe}$ in a natural
way.

$\myprod$ is the easiest case: we decompose the proof into proofs that
the first element's types are equal ($\mytya_1 \myeq \mytya_2$), and a
proof that given equal values in the first element, the types of the
second elements are equal too
($\myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{\myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2}}
  \myimpl \mytyb_1 \myeq \mytyb_2}$).\footnote{We are using $\myimpl$ to
  indicate a $\forall$ where we discard the first value.  We write
  $\mytyb_1[\myb{x_1}]$ to indicate that the $\myb{x_1}$ in $\mytyb_1$
  is re-bound to the $\myb{x_1}$ quantified by the $\forall$, and
  similarly for $\myb{x_2}$ and $\mytyb_2$.}  This also explains the
need for heterogeneous equality, since in the second proof it would be
awkward to express the fact that $\myb{A_1}$ is the same as $\myb{A_2}$.
In the respective $\myfun{coe}$ case, since the types are canonical, we
know at this point that the proof of equality is a pair of the shape
described above.  Thus, we can immediately coerce the first element of
the pair using the first element of the proof, and then instantiate the
second element with the two first elements and a proof by coherence of
their equality, since we know that the types are equal.

The cases for the other binders are omitted for brevity, but they follow
the same principle with some twists to make $\myfun{coe}$ work with the
generated proofs; the reader can refer to the paper for details.

\subsubsection{$\myfun{coe}$, laziness, and $\myfun{coh}$erence}

It is important to notice that in the reduction rules for $\myfun{coe}$
are never obstructed by the proofs: with the exception of comparisons
between different canonical types we never `pattern match' on the proof
pairs, but always look at the projections.  This means that, as long as
we are consistent, and thus as long as we don't have $\mybot$-inducing
proofs, we can add propositional axioms for equality and $\myfun{coe}$
will still compute.  Thus, we can take $\myfun{coh}$ as axiomatic, and
we can add back familiar useful equality rules:

\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
  \AxiomC{$\myjud{\mytmt}{\mytya}$}
  \UnaryInfC{$\myjud{\myapp{\myrefl}{\mytmt}}{\myprdec{\myjm{\mytmt}{\mytya}{\mytmt}{\mytya}}}$}
  \DisplayProof

  \myderivspp

  \AxiomC{$\myjud{\mytya}{\mytyp}$}
  \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytyb}{\mytyp}$}
  \BinaryInfC{$\myjud{\mytyc{R} \myappsp (\myb{x} {:} \mytya) \myappsp \mytyb}{\myfora{\myb{y}\, \myb{z}}{\mytya}{\myprdec{\myjm{\myb{y}}{\mytya}{\myb{z}}{\mytya} \myimpl \mysub{\mytyb}{\myb{x}}{\myb{y}} \myeq \mysub{\mytyb}{\myb{x}}{\myb{z}}}}}$}
  \DisplayProof
}

$\myrefl$ is the equivalent of the reflexivity rule in propositional
equality, and $\mytyc{R}$ asserts that if we have a we have a $\mytyp$
abstracting over a value we can substitute equal for equal---this lets
us recover $\myfun{subst}$.  Note that while we need to provide ad-hoc
rules in the restricted, non-hierarchical theory that we have, if our
theory supports abstraction over $\mytyp$s we can easily add these
axioms as abstracted variables.

\subsubsection{Value-level equality}

\mydesc{equality reduction:}{\myprsyn \myred \myprsyn}{
  $
  \begin{array}{r@{ }c@{\ }c@{\ }c@{}l@{\ }c@{\ }r@{}c@{\ }c@{\ }c@{}l@{\ }l}
    (&\mytmt_1 & : & \myempty&) & \myeq & (&\mytmt_2 & : & \myempty &) & \myred \mytop \\
    (&\mytmt_1 & : & \myunit&) & \myeq & (&\mytmt_2 & : & \myunit&) & \myred \mytop \\
    (&\mytrue & : & \mybool&) & \myeq & (&\mytrue & : & \mybool&) & \myred \mytop \\
    (&\myfalse & : & \mybool&) & \myeq & (&\myfalse & : & \mybool&) & \myred \mytop \\
    (&\mytrue & : & \mybool&) & \myeq & (&\myfalse & : & \mybool&) & \myred \mybot \\
    (&\myfalse & : & \mybool&) & \myeq & (&\mytrue & : & \mybool&) & \myred \mybot \\
    (&\mytmt_1 & : & \myexi{\mytya_1}{\myb{x_1}}{\mytyb_1}&) & \myeq & (&\mytmt_2 & : & \myexi{\mytya_2}{\myb{x_2}}{\mytyb_2}&) & \myred \\
     & \multicolumn{11}{@{}l}{
      \myind{2} \myjm{\myapp{\myfst}{\mytmt_1}}{\mytya_1}{\myapp{\myfst}{\mytmt_2}}{\mytya_2} \myand
      \myjm{\myapp{\mysnd}{\mytmt_1}}{\mysub{\mytyb_1}{\myb{x_1}}{\myapp{\myfst}{\mytmt_1}}}{\myapp{\mysnd}{\mytmt_2}}{\mysub{\mytyb_2}{\myb{x_2}}{\myapp{\myfst}{\mytmt_2}}}
    } \\
   (&\myse{f}_1 & : & \myfora{\mytya_1}{\myb{x_1}}{\mytyb_1}&) & \myeq & (&\myse{f}_2 & : & \myfora{\mytya_2}{\myb{x_2}}{\mytyb_2}&) & \myred \\
     & \multicolumn{11}{@{}l}{
       \myind{2} \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{
           \myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2} \myimpl
           \myjm{\myapp{\myse{f}_1}{\myb{x_1}}}{\mytyb_1[\myb{x_1}]}{\myapp{\myse{f}_2}{\myb{x_2}}}{\mytyb_2[\myb{x_2}]}
         }}
    } \\
   (&\mytmt_1 \mynodee \myse{f}_1 & : & \myw{\mytya_1}{\myb{x_1}}{\mytyb_1}&) & \myeq & (&\mytmt_1 \mynodee \myse{f}_1 & : & \myw{\mytya_2}{\myb{x_2}}{\mytyb_2}&) & \myred \cdots \\
    (&\mytmt_1 & : & \mytya_1&) & \myeq & (&\mytmt_2 & : & \mytya_2 &) & \myred \mybot\ \text{if $\mytya_1$ and $\mytya_2$ are canonical.}
  \end{array}
  $
}

As with type-level equality, we want value-level equality to reduce
based on the structure of the compared terms.  When matching
propositional data, such as $\myempty$ and $\myunit$, we automatically
return the trivial type, since if a type has zero one members, all
members will be equal.  When matching on data-bearing types, such as
$\mybool$, we check that such data matches, and return bottom otherwise.

\subsection{Proof irrelevance and stuck coercions}
\label{sec:ott-quot}

The last effort is required to make sure that proofs (members of
$\myprop$) are \emph{irrelevant}.  Since they are devoid of
computational content, we would like to identify all equivalent
propositions as the same, in a similar way as we identified all
$\myempty$ and all $\myunit$ as the same in section
\ref{sec:eta-expand}.

Thus we will have a quotation that will not only perform
$\eta$-expansion, but will also identify and mark proofs that could not
be decoded (that is, equalities on neutral types).  Then, when
comparing terms, marked proofs will be considered equal without
analysing their contents, thus gaining irrelevance.

Moreover we can safely advance `stuck' $\myfun{coe}$rcions between
non-canonical but definitionally equal types.  Consider for example
\[
\mycoee{(\myITE{\myb{b}}{\mynat}{\mybool})}{(\myITE{\myb{b}}{\mynat}{\mybool})}{\myb{x}}
\]
Where $\myb{b}$ and $\myb{x}$ are abstracted variables.  This
$\myfun{coe}$ will not advance, since the types are not canonical.
However they are definitionally equal, and thus we can safely remove the
coerce and return $\myb{x}$ as it is.

This process of identifying every proof as equivalent and removing
$\myfun{coe}$rcions is known as \emph{quotation}.

\section{\mykant : the theory}
\label{sec:kant-theory}

\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.

We will first present the features of the system, and then describe the
implementation we have developed in Section \ref{sec:kant-practice}.

The defining features of \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 a type synthesis system
  in the style of \cite{Pierce2000}, extending the concept for user
  defined data types.

\item[Observational equality] As described in Section \ref{sec:ott} but
  extended to work with the type hierarchy and to admit equality between
  arbitrary data types.
\end{description}

We will analyse the features one by one, along with motivations and
tradeoffs for the design decisions made.

\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 kinds 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: neutral terms (abstracted or defined variables, function
application, record projections, primitive recursors, etc.) \emph{infer}
types, canonical terms (abstractions, record/data types data
constructors, etc.) need to be \emph{checked}.

To introduce the concept and notation, we will revisit the STLC in a
bidirectional style.  The presentation follows \cite{Loh2010}.  The
syntax for our bidirectional STLC is the same as the untyped
$\lambda$-calculus, but with an extra construct to annotate terms
explicitly---this will be necessary when having top-level canonical
terms.  The types are the same as those found in the normal STLC.

\mydesc{syntax}{ }{
  $
  \begin{array}{r@{\ }c@{\ }l}
    \mytmsyn & ::= & \myb{x} \mysynsep \myabs{\myb{x}}{\mytmsyn} \mysynsep (\myapp{\mytmsyn}{\mytmsyn}) \mysynsep (\mytmsyn : \mytysyn)
  \end{array}
  $
}
We will have two kinds of typing judgements: \emph{inference} and
\emph{checking}.  $\myinf{\mytmt}{\mytya}$ indicates that $\mytmt$
infers the type $\mytya$, while $\mychk{\mytmt}{\mytya}$ can be checked
against type $\mytya$.  The type of variables in context is inferred,
and so are annotate terms.  The type of applications is inferred too,
propagating types down the applied term.  Abstractions are checked.
Finally, we have a rule to check the type of an inferrable term.

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

  \myderivspp

  \begin{tabular}{cc}
    \AxiomC{$\mychk{\mytmt}{\mytya}$}
    \UnaryInfC{$\myinf{\myann{\mytmt}{\mytya}}{\mytya}$}
    \DisplayProof
    &
    \AxiomC{$\myinf{\mytmt}{\mytya}$}
    \UnaryInfC{$\mychk{\mytmt}{\mytya}$}
    \DisplayProof
  \end{tabular}
}

For example, if we wanted to type function composition (in this case for
naturals), we would have to annotate the term:
\[
  \myfun{comp} \mapsto (\myabs{\myb{f}\, \myb{g}\, \myb{x}}{\myb{f}\myappsp(\myb{g}\myappsp\myb{x})}) : (\mynat \myarr \mynat) \myarr (\mynat \myarr \mynat) \myarr \mynat \myarr \mynat
\]
But we would not have to annotate functions passed to it, since the type would be propagated to the arguments:
\[
   \myfun{comp}\myappsp (\myabs{\myb{x}}{\myb{x} \mathrel{\myfun{$+$}} 3}) \myappsp (\myabs{\myb{x}}{\myb{x} \mathrel{\myfun{$*$}} 4}) \myappsp 42
\]

\subsection{Base terms and types}

Let us begin by describing the primitives available without the user
defining any data types, and without equality.  The way we handle
variables and substitution is left unspecified, and explained in section
\ref{sec:term-repr}, along with other implementation issues.  We are
also going to give an account of the implicit type hierarchy separately
in Section \ref{sec:term-hierarchy}, so as not to clutter derivation
rules too much, and just treat types as impredicative for the time
being.

\mydesc{syntax}{ }{
  $
  \begin{array}{r@{\ }c@{\ }l}
    \mytmsyn & ::= & \mynamesyn \mysynsep \mytyp \\
    &  |  & \myfora{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
    \myabs{\myb{x}}{\mytmsyn} \mysynsep
    (\myapp{\mytmsyn}{\mytmsyn}) \mysynsep
    (\myann{\mytmsyn}{\mytmsyn}) \\
    \mynamesyn & ::= & \myb{x} \mysynsep \myfun{f}
  \end{array}
  $
}

The syntax for our calculus includes just two basic constructs:
abstractions and $\mytyp$s.  Everything else will be provided by
user-definable constructs.  Since we let the user define values, we will
need a context capable of carrying the body of variables along with
their type.

Bound names and defined names are treated separately in the syntax, and
while both can be associated to a type in the context, only defined
names can be associated with a body:

\mydesc{context validity:}{\myvalid{\myctx}}{
    \begin{tabular}{ccc}
      \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
      \UnaryInfC{$\myvalid{\myemptyctx}$}
      \DisplayProof
      &
      \AxiomC{$\myjud{\mytya}{\mytyp}$}
      \AxiomC{$\mynamesyn \not\in \myctx$}
      \BinaryInfC{$\myvalid{\myctx ; \mynamesyn : \mytya}$}
      \DisplayProof
      &
      \AxiomC{$\myjud{\mytmt}{\mytya}$}
      \AxiomC{$\myfun{f} \not\in \myctx$}
      \BinaryInfC{$\myvalid{\myctx ; \myfun{f} \mapsto \mytmt : \mytya}$}
      \DisplayProof
    \end{tabular}
}

Now we can present the reduction rules, which are unsurprising.  We have
the usual function application ($\beta$-reduction), but also a rule to
replace names with their bodies ($\delta$-reduction), and one to discard
type annotations.  For this reason reduction is done in-context, as
opposed to what we have seen in the past:

\mydesc{reduction:}{\myctx \vdash \mytmsyn \myred \mytmsyn}{
    \begin{tabular}{ccc}
      \AxiomC{\phantom{$\myb{x} \mapsto \mytmt : \mytya \in \myctx$}}
      \UnaryInfC{$\myctx \vdash \myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn}
                  \myred \mysub{\mytmm}{\myb{x}}{\mytmn}$}
      \DisplayProof
      &
      \AxiomC{$\myfun{f} \mapsto \mytmt : \mytya \in \myctx$}
      \UnaryInfC{$\myctx \vdash \myfun{f} \myred \mytmt$}
      \DisplayProof
      &
      \AxiomC{\phantom{$\myb{x} \mapsto \mytmt : \mytya \in \myctx$}}
      \UnaryInfC{$\myctx \vdash \myann{\mytmm}{\mytya} \myred \mytmm$}
      \DisplayProof
    \end{tabular}
}

We can now give types to our terms.  Although we include the usual
conversion rule, we defer a detailed account of definitional equality to
Section \ref{sec:kant-irr}.

\mydesc{typing:}{\myctx \vdash \mytmsyn \Leftrightarrow \mytmsyn}{   
    \begin{tabular}{cccc}
      \AxiomC{$\myse{name} : A \in \myctx$}
      \UnaryInfC{$\myinf{\myse{name}}{A}$}
      \DisplayProof
      &
      \AxiomC{$\myfun{f} \mapsto \mytmt : A \in \myctx$}
      \UnaryInfC{$\myinf{\myfun{f}}{A}$}
      \DisplayProof
      &
      \AxiomC{$\mychk{\mytmt}{\mytya}$}
      \UnaryInfC{$\myinf{\myann{\mytmt}{\mytya}}{\mytya}$}
      \DisplayProof
      &
      \AxiomC{$\myinf{\mytmt}{\mytya}$}
      \AxiomC{$\myctx \vdash \mytya \mydefeq \mytyb$}
      \BinaryInfC{$\mychk{\mytmt}{\mytyb}$}
      \DisplayProof
    \end{tabular}
    \myderivspp

    \begin{tabular}{ccc}
      \AxiomC{$\myinf{\mytmm}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
      \AxiomC{$\mychk{\mytmn}{\mytya}$}
      \BinaryInfC{$\myinf{\myapp{\mytmm}{\mytmn}}{\mysub{\mytyb}{\myb{x}}{\mytmn}}$}
      \DisplayProof

      &

      \AxiomC{$\mychkk{\myctx; \myb{x}: \mytya}{\mytmt}{\mytyb}$}
      \UnaryInfC{$\mychk{\myabs{\myb{x}}{\mytmt}}{\myfora{\myb{x}}{\mytyb}{\mytyb}}$}
      \DisplayProof
    \end{tabular}
}

\subsection{Elaboration}

As we mentioned, $\mykant$\ allows the user to define not only values
but also custom data types and records.  \emph{Elaboration} consists of
turning these declarations into workable syntax, types, and reduction
rules.  The treatment of custom types in $\mykant$\ is heavily inspired
by McBride and McKinna early work on Epigram \citep{McBride2004},
although with some differences.

\subsubsection{Term vectors, telescopes, and assorted notation}

We use a vector notation to refer to a series of term applied to
another, for example $\mytyc{D} \myappsp \vec{A}$ is a shorthand for
$\mytyc{D} \myappsp \mytya_1 \cdots \mytya_n$, for some $n$.  $n$ is
consistently used to refer to the length of such vectors, and $i$ to
refer to an index in such vectors.  We also often need to `build up'
terms vectors, in which case we use $\myemptyctx$ for an empty vector
and add elements to an existing vector with $\myarg ; \myarg$, similarly
to what we do for context.

To present the elaboration and operations on user defined data types, we
frequently make use what de Bruijn called \emph{telescopes}
\citep{Bruijn91}, a construct that will prove useful when dealing with
the types of type and data constructors.  A telescope is a series of
nested typed bindings, such as $(\myb{x} {:} \mynat); (\myb{p} {:}
\myapp{\myfun{even}}{\myb{x}})$.  Consistently with the notation for
contexts and term vectors, we use $\myemptyctx$ to denote an empty
telescope and $\myarg ; \myarg$ to add a new binding to an existing
telescope.

We refer to telescopes with $\mytele$, $\mytele'$, $\mytele_i$, etc.  If
$\mytele$ refers to a telescope, $\mytelee$ refers to the term vector
made up of all the variables bound by $\mytele$.  $\mytele \myarr
\mytya$ refers to the type made by turning the telescope into a series
of $\myarr$.  Returning to the examples above, we have that
\[
   (\myb{x} {:} \mynat); (\myb{p} : \myapp{\myfun{even}}{\myb{x}}) \myarr \mynat =
   (\myb{x} {:} \mynat) \myarr (\myb{p} : \myapp{\myfun{even}}{\myb{x}}) \myarr \mynat
\]

We make use of various operations to manipulate telescopes:
\begin{itemize}
\item $\myhead(\mytele)$ refers to the first type appearing in
  $\mytele$: $\myhead((\myb{x} {:} \mynat); (\myb{p} :
  \myapp{\myfun{even}}{\myb{x}})) = \mynat$.  Similarly,
  $\myix_i(\mytele)$ refers to the $i^{th}$ type in a telescope
  (1-indexed).
\item $\mytake_i(\mytele)$ refers to the telescope created by taking the
  first $i$ elements of $\mytele$:  $\mytake_1((\myb{x} {:} \mynat); (\myb{p} :
  \myapp{\myfun{even}}{\myb{x}})) = (\myb{x} {:} \mynat)$.
\item $\mytele \vec{A}$ refers to the telescope made by `applying' the
  terms in $\vec{A}$ on $\mytele$: $((\myb{x} {:} \mynat); (\myb{p} :
  \myapp{\myfun{even}}{\myb{x}}))42 = (\myb{p} :
  \myapp{\myfun{even}}{42})$.
\end{itemize}

Additionally, when presenting syntax elaboration, I'll use $\mytmsyn^n$
to indicate a term vector composed of $n$ elements, or
$\mytmsyn^{\mytele}$ for one composed by as many elements as the
telescope.

\subsubsection{Declarations syntax}

\mydesc{syntax}{ }{
  $
  \begin{array}{r@{\ }c@{\ }l}
      \mydeclsyn & ::= & \myval{\myb{x}}{\mytmsyn}{\mytmsyn} \\
                 &  |  & \mypost{\myb{x}}{\mytmsyn} \\
                 &  |  & \myadt{\mytyc{D}}{\myappsp \mytelesyn}{}{\mydc{c} : \mytelesyn\ |\ \cdots } \\
                 &  |  & \myreco{\mytyc{D}}{\myappsp \mytelesyn}{}{\myfun{f} : \mytmsyn,\ \cdots } \\

      \mytelesyn & ::= & \myemptytele \mysynsep \mytelesyn \mycc (\myb{x} {:} \mytmsyn) \\
      \mynamesyn & ::= & \cdots \mysynsep \mytyc{D} \mysynsep \mytyc{D}.\mydc{c} \mysynsep \mytyc{D}.\myfun{f}
  \end{array}
  $
}

In \mykant\ we have four kind of declarations:

\begin{description}
\item[Defined value] A variable, together with a type and a body.
\item[Abstract variable] An abstract variable, with a type but no body.
\item[Inductive data] A datatype, with a type constructor and various data
  constructors---somewhat similar to what we find in Haskell.  A primitive
  recursor (or `destructor') will be generated automatically.
\item[Record] A record, which consists of one data constructor and various
  fields, with no recursive occurrences.
\end{description}

Elaborating defined variables consists of type checking body against the
given type, and updating the context to contain the new binding.
Elaborating abstract variables and abstract variables consists of type
checking the type, and updating the context with a new typed variable:

\mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
    \begin{tabular}{cc}
      \AxiomC{$\myjud{\mytmt}{\mytya}$}
      \AxiomC{$\myfun{f} \not\in \myctx$}
      \BinaryInfC{
        $\myctx \myelabt \myval{\myfun{f}}{\mytya}{\mytmt} \ \ \myelabf\ \  \myctx; \myfun{f} \mapsto \mytmt : \mytya$
      }
      \DisplayProof
      &
      \AxiomC{$\myjud{\mytya}{\mytyp}$}
      \AxiomC{$\myfun{f} \not\in \myctx$}
      \BinaryInfC{
        $
          \myctx \myelabt \mypost{\myfun{f}}{\mytya}
          \ \ \myelabf\ \  \myctx; \myfun{f} : \mytya
        $
      }
      \DisplayProof
    \end{tabular}
}

\subsubsection{User defined types}
\label{sec:user-type}

Elaborating user defined types is the real effort.  First, let's explain
what we can defined, with some examples.

\begin{description}
\item[Natural numbers] To define natural numbers, we create a data type
  with two constructors: one with zero arguments ($\mydc{zero}$) and one
  with one recursive argument ($\mydc{suc}$):
  \[
  \begin{array}{@{}l}
    \myadt{\mynat}{ }{ }{
      \mydc{zero} \mydcsep \mydc{suc} \myappsp \mynat
    }
  \end{array}
  \]
  This is very similar to what we would write in Haskell:
  \begin{Verbatim}
data Nat = Zero | Suc Nat
  \end{Verbatim}
  Once the data type is defined, $\mykant$\ will generate syntactic
  constructs for the type and data constructors, so that we will have
  \begin{center}
    \mysmall
    \begin{tabular}{ccc}
      \AxiomC{\phantom{$\mychk{\mytmt}{\mynat}$}}
      \UnaryInfC{$\myinf{\mynat}{\mytyp}$}
      \DisplayProof
    &
      \AxiomC{\phantom{$\mychk{\mytmt}{\mynat}$}}
      \UnaryInfC{$\myinf{\mytyc{\mynat}.\mydc{zero}}{\mynat}$}
      \DisplayProof
    &
      \AxiomC{$\mychk{\mytmt}{\mynat}$}
      \UnaryInfC{$\myinf{\mytyc{\mynat}.\mydc{suc} \myappsp \mytmt}{\mynat}$}
      \DisplayProof
    \end{tabular}
  \end{center}
  While in Haskell (or indeed in Agda or Coq) data constructors are
  treated the same way as functions, in $\mykant$\ they are syntax, so
  for example using $\mytyc{\mynat}.\mydc{suc}$ on its own will be a
  syntax error.  This is necessary so that we can easily infer the type
  of polymorphic data constructors, as we will see later.

  Moreover, each data constructor is prefixed by the type constructor
  name, since we need to retrieve the type constructor of a data
  constructor when type checking.  This measure aids in the presentation
  of various features but it is not needed in the implementation, where
  we can have a dictionary to lookup the type constructor corresponding
  to each data constructor.  When using data constructors in examples I
  will omit the type constructor prefix for brevity.

  Along with user defined constructors, $\mykant$\ automatically
  generates an \emph{eliminator}, or \emph{destructor}, to compute with
  natural numbers: If we have $\mytmt : \mynat$, we can destruct
  $\mytmt$ using the generated eliminator `$\mynat.\myfun{elim}$':
  \begin{prooftree}
    \mysmall
    \AxiomC{$\mychk{\mytmt}{\mynat}$}
    \UnaryInfC{$
      \myinf{\mytyc{\mynat}.\myfun{elim} \myappsp \mytmt}{
        \begin{array}{@{}l}
          \myfora{\myb{P}}{\mynat \myarr \mytyp}{ \\ \myapp{\myb{P}}{\mydc{zero}} \myarr (\myfora{\myb{x}}{\mynat}{\myapp{\myb{P}}{\myb{x}} \myarr \myapp{\myb{P}}{(\myapp{\mydc{suc}}{\myb{x}})}}) \myarr \\ \myapp{\myb{P}}{\mytmt}}
          \end{array}
        }$}
  \end{prooftree}
  $\mynat.\myfun{elim}$ corresponds to the induction principle for
  natural numbers: if we have a predicate on numbers ($\myb{P}$), and we
  know that predicate holds for the base case
  ($\myapp{\myb{P}}{\mydc{zero}}$) and for each inductive step
  ($\myfora{\myb{x}}{\mynat}{\myapp{\myb{P}}{\myb{x}} \myarr
    \myapp{\myb{P}}{(\myapp{\mydc{suc}}{\myb{x}})}}$), then $\myb{P}$
  holds for any number.  As with the data constructors, we require the
  eliminator to be applied to the `destructed' element.

  While the induction principle is usually seen as a mean to prove
  properties about numbers, in the intuitionistic setting it is also a
  mean to compute.  In this specific case we will $\mynat.\myfun{elim}$
  will return the base case if the provided number is $\mydc{zero}$, and
  recursively apply the inductive step if the number is a
  $\mydc{suc}$cessor:
  \[
  \begin{array}{@{}l@{}l}
    \mytyc{\mynat}.\myfun{elim} \myappsp \mydc{zero} & \myappsp \myse{P} \myappsp \myse{pz} \myappsp \myse{ps} \myred \myse{pz} \\
    \mytyc{\mynat}.\myfun{elim} \myappsp (\mydc{suc} \myappsp \mytmt) & \myappsp \myse{P} \myappsp \myse{pz} \myappsp \myse{ps} \myred \myse{ps} \myappsp \mytmt \myappsp (\mynat.\myfun{elim} \myappsp \mytmt \myappsp \myse{P} \myappsp \myse{pz} \myappsp \myse{ps})
  \end{array}
  \]
  The Haskell equivalent would be
  \begin{Verbatim}
elim :: Nat -> a -> (Nat -> a -> a) -> a
elim Zero    pz ps = pz
elim (Suc n) pz ps = ps n (elim n pz ps)
\end{Verbatim}
  Which buys us the computational behaviour, but not the reasoning power.

\item[Binary trees] Now for a polymorphic data type: binary trees, since
  lists are too similar to natural numbers to be interesting.
  \[
  \begin{array}{@{}l}
    \myadt{\mytree}{\myappsp (\myb{A} {:} \mytyp)}{ }{
      \mydc{leaf} \mydcsep \mydc{node} \myappsp (\myapp{\mytree}{\myb{A}}) \myappsp \myb{A} \myappsp (\myapp{\mytree}{\myb{A}})
    }
  \end{array}
  \]
  Now the purpose of constructors as syntax can be explained: what would
  the type of $\mydc{leaf}$ be?  If we were to treat it as a `normal'
  term, we would have to specify the type parameter of the tree each
  time the constructor is applied:
  \[
  \begin{array}{@{}l@{\ }l}
    \mydc{leaf} & : \myfora{\myb{A}}{\mytyp}{\myapp{\mytree}{\myb{A}}} \\
    \mydc{node} & : \myfora{\myb{A}}{\mytyp}{\myapp{\mytree}{\myb{A}} \myarr \myb{A} \myarr \myapp{\mytree}{\myb{A}} \myarr \myapp{\mytree}{\myb{A}}}
  \end{array}
  \]
  The problem with this approach is that creating terms is incredibly
  verbose and dull, since we would need to specify the type parameters
  each time.  For example if we wished to create a $\mytree \myappsp
  \mynat$ with two nodes and three leaves, we would have to write
  \[
  \mydc{node} \myappsp \mynat \myappsp (\mydc{node} \myappsp \mynat \myappsp (\mydc{leaf} \myappsp \mynat) \myappsp (\myapp{\mydc{suc}}{\mydc{zero}}) \myappsp (\mydc{leaf} \myappsp \mynat)) \myappsp \mydc{zero} \myappsp (\mydc{leaf} \myappsp \mynat)
  \]
  The redundancy of $\mynat$s is quite irritating.  Instead, if we treat
  constructors as syntactic elements, we can `extract' the type of the
  parameter from the type that the term gets checked against, much like
  we get the type of abstraction arguments:
  \begin{center}
    \mysmall
    \begin{tabular}{cc}
      \AxiomC{$\mychk{\mytya}{\mytyp}$}
      \UnaryInfC{$\mychk{\mydc{leaf}}{\myapp{\mytree}{\mytya}}$}
      \DisplayProof
      &
      \AxiomC{$\mychk{\mytmm}{\mytree \myappsp \mytya}$}
      \AxiomC{$\mychk{\mytmt}{\mytya}$}
      \AxiomC{$\mychk{\mytmm}{\mytree \myappsp \mytya}$}
      \TrinaryInfC{$\mychk{\mydc{node} \myappsp \mytmm \myappsp \mytmt \myappsp \mytmn}{\mytree \myappsp \mytya}$}
      \DisplayProof
    \end{tabular}
  \end{center}
  Which enables us to write, much more concisely
  \[
  \mydc{node} \myappsp (\mydc{node} \myappsp \mydc{leaf} \myappsp (\myapp{\mydc{suc}}{\mydc{zero}}) \myappsp \mydc{leaf}) \myappsp \mydc{zero} \myappsp \mydc{leaf} : \myapp{\mytree}{\mynat}
  \]
  We gain an annotation, but we lose the myriad of types applied to the
  constructors.  Conversely, with the eliminator for $\mytree$, we can
  infer the type of the arguments given the type of the destructed:
  \begin{prooftree}
    \small
    \AxiomC{$\myinf{\mytmt}{\myapp{\mytree}{\mytya}}$}
    \UnaryInfC{$
      \myinf{\mytree.\myfun{elim} \myappsp \mytmt}{
        \begin{array}{@{}l}
          (\myb{P} {:} \myapp{\mytree}{\mytya} \myarr \mytyp) \myarr \\
          \myapp{\myb{P}}{\mydc{leaf}} \myarr \\
          ((\myb{l} {:} \myapp{\mytree}{\mytya}) (\myb{x} {:} \mytya) (\myb{r} {:} \myapp{\mytree}{\mytya}) \myarr \myapp{\myb{P}}{\myb{l}} \myarr
          \myapp{\myb{P}}{\myb{r}} \myarr \myb{P} \myappsp (\mydc{node} \myappsp \myb{l} \myappsp \myb{x} \myappsp \myb{r})) \myarr \\
          \myapp{\myb{P}}{\mytmt}
        \end{array}
      }
      $}
  \end{prooftree}
  As expected, the eliminator embodies structural induction on trees.

\item[Empty type] We have presented types that have at least one
  constructors, but nothing prevents us from defining types with
  \emph{no} constructors:
  \[\myadt{\mytyc{Empty}}{ }{ }{ }\]
  What shall the `induction principle' on $\mytyc{Empty}$ be?  Does it
  even make sense to talk about induction on $\mytyc{Empty}$?
  $\mykant$\ does not care, and generates an eliminator with no `cases',
  and thus corresponding to the $\myfun{absurd}$ that we know and love:
  \begin{prooftree}
    \mysmall
    \AxiomC{$\myinf{\mytmt}{\mytyc{Empty}}$}
    \UnaryInfC{$\myinf{\myempty.\myfun{elim} \myappsp \mytmt}{(\myb{P} {:} \mytmt \myarr \mytyp) \myarr \myapp{\myb{P}}{\mytmt}}$}
  \end{prooftree}

\item[Ordered lists] Up to this point, the examples shown are nothing
  new to the \{Haskell, SML, OCaml, functional\} programmer.  However
  dependent types let us express much more than that.  A useful example
  is the type of ordered lists. There are many ways to define such a
  thing, we will define our type to store the bounds of the list, making
  sure that $\mydc{cons}$ing respects that.

  First, using $\myunit$ and $\myempty$, we define a type expressing the
  ordering on natural numbers, $\myfun{le}$---`less or equal'.
  $\myfun{le}\myappsp \mytmm \myappsp \mytmn$ will be inhabited only if
  $\mytmm \le \mytmn$:
  \[
    \begin{array}{@{}l}
      \myfun{le} : \mynat \myarr \mynat \myarr \mytyp \\
      \myfun{le} \myappsp \myb{n} \mapsto \\
          \myind{2} \mynat.\myfun{elim} \\
            \myind{2}\myind{2} \myb{n} \\
            \myind{2}\myind{2} (\myabs{\myarg}{\mynat \myarr \mytyp}) \\
            \myind{2}\myind{2} (\myabs{\myarg}{\myunit}) \\
            \myind{2}\myind{2} (\myabs{\myb{n}\, \myb{f}\, \myb{m}}{
              \mynat.\myfun{elim} \myappsp \myb{m} \myappsp (\myabs{\myarg}{\mytyp}) \myappsp \myempty \myappsp (\myabs{\myb{m'}\, \myarg}{\myapp{\myb{f}}{\myb{m'}}})
                              })
    \end{array}
    \]
  We return $\myunit$ if the scrutinised is $\mydc{zero}$ (every
  number in less or equal than zero), $\myempty$ if the first number is
  a $\mydc{suc}$cessor and the second a $\mydc{zero}$, and we recurse if
  they are both successors.  Since we want the list to have possibly
  `open' bounds, for example for empty lists, we create a type for
  `lifted' naturals with a bottom (less than everything) and top
  (greater than everything) elements, along with an associated comparison
  function:
  \[
    \begin{array}{@{}l}
    \myadt{\mytyc{Lift}}{ }{ }{\mydc{bot} \mydcsep \mydc{lift} \myappsp \mynat \mydcsep \mydc{top}}\\
    \myfun{le'} : \mytyc{Lift} \myarr \mytyc{Lift} \myarr \mytyp\\
    \myfun{le'} \myappsp \myb{l_1} \mapsto \\
          \myind{2} \mytyc{Lift}.\myfun{elim} \\
            \myind{2}\myind{2} \myb{l_1} \\
            \myind{2}\myind{2} (\myabs{\myarg}{\mytyc{Lift} \myarr \mytyp}) \\
            \myind{2}\myind{2} (\myabs{\myarg}{\myunit}) \\
            \myind{2}\myind{2} (\myabs{\myb{n_1}\, \myb{n_2}}{
              \mytyc{Lift}.\myfun{elim} \myappsp \myb{l_2} \myappsp (\myabs{\myarg}{\mytyp}) \myappsp \myempty \myappsp (\myabs{\myb{n_2}}{\myfun{le} \myappsp \myb{n_1} \myappsp \myb{n_2}}) \myappsp \myunit
            }) \\
            \myind{2}\myind{2} (\myabs{\myb{n_1}\, \myb{n_2}}{
              \mytyc{Lift}.\myfun{elim} \myappsp \myb{l_2} \myappsp (\myabs{\myarg}{\mytyp}) \myappsp \myempty \myappsp (\myabs{\myarg}{\myempty}) \myappsp \myunit
            })
    \end{array}
    \]
  Finally, we can defined a type of ordered lists.  The type is
  parametrised over two values representing the lower and upper bounds
  of the elements, as opposed to the type parameters that we are used
  to.  Then, an empty list will have to have evidence that the bounds
  are ordered, and each time we add an element we require the list to
  have a matching lower bound:
  \[
    \begin{array}{@{}l}
      \myadt{\mytyc{OList}}{\myappsp (\myb{low}\ \myb{upp} {:} \mytyc{Lift})}{\\ \myind{2}}{
          \mydc{nil} \myappsp (\myfun{le'} \myappsp \myb{low} \myappsp \myb{upp}) \mydcsep \mydc{cons} \myappsp (\myb{n} {:} \mynat) \myappsp (\mytyc{OList} \myappsp (\myfun{lift} \myappsp \myb{n}) \myappsp \myb{upp}) \myappsp (\myfun{le'} \myappsp \myb{low} \myappsp (\myfun{lift} \myappsp \myb{n})
        }
    \end{array}
  \]
  If we want we can then employ this structure to write and prove
  correct various sorting algorithms.\footnote{See this presentation by
    Conor McBride:
    \url{https://personal.cis.strath.ac.uk/conor.mcbride/Pivotal.pdf},
    and this blog post by the author:
    \url{http://mazzo.li/posts/AgdaSort.html}.}

\item[Dependent products] Apart from $\mysyn{data}$, $\mykant$\ offers
  us another way to define types: $\mysyn{record}$.  A record is a
  datatype with one constructor and `projections' to extract specific
  fields of the said constructor.

  For example, we can recover dependent products:
  \[
  \begin{array}{@{}l}
    \myreco{\mytyc{Prod}}{\myappsp (\myb{A} {:} \mytyp) \myappsp (\myb{B} {:} \myb{A} \myarr \mytyp)}{\\ \myind{2}}{\myfst : \myb{A}, \mysnd : \myapp{\myb{B}}{\myb{fst}}}
  \end{array}
  \]
  Here $\myfst$ and $\mysnd$ are the projections, with their respective
  types.  Note that each field can refer to the preceding fields.  A
  constructor will be automatically generated, under the name of
  $\mytyc{Prod}.\mydc{constr}$.  Dually to data types, we will omit the
  type constructor prefix for record projections.

  Following the bidirectionality of the system, we have that projections
  (the destructors of the record) infer the type, while the constructor
  gets checked:
  \begin{center}
    \mysmall
    \begin{tabular}{cc}
      \AxiomC{$\mychk{\mytmm}{\mytya}$}
      \AxiomC{$\mychk{\mytmn}{\myapp{\mytyb}{\mytmm}}$}
      \BinaryInfC{$\mychk{\mytyc{Prod}.\mydc{constr} \myappsp \mytmm \myappsp \mytmn}{\mytyc{Prod} \myappsp \mytya \myappsp \mytyb}$}
      \noLine
      \UnaryInfC{\phantom{$\myinf{\myfun{snd} \myappsp \mytmt}{\mytyb \myappsp (\myfst \myappsp \mytmt)}$}}
      \DisplayProof
      &
      \AxiomC{$\myinf{\mytmt}{\mytyc{Prod} \myappsp \mytya \myappsp \mytyb}$}
      \UnaryInfC{$\myinf{\myfun{fst} \myappsp \mytmt}{\mytya}$}
      \noLine
      \UnaryInfC{$\myinf{\myfun{snd} \myappsp \mytmt}{\mytyb \myappsp (\myfst \myappsp \mytmt)}$}
      \DisplayProof
    \end{tabular}
  \end{center}
  What we have is equivalent to ITT's dependent products.
\end{description}

\begin{figure}[p]
    \mydesc{syntax}{ }{
      \footnotesize
      $
      \begin{array}{l}
        \mynamesyn ::= \cdots \mysynsep \mytyc{D} \mysynsep \mytyc{D}.\mydc{c} \mysynsep \mytyc{D}.\myfun{f}
      \end{array}
      $
    }

    \mynegder

  \mydesc{syntax elaboration:}{\mydeclsyn \myelabf \mytmsyn ::= \cdots}{
    \footnotesize
      $
      \begin{array}{r@{\ }l}
         & \myadt{\mytyc{D}}{\mytele}{}{\cdots\ |\ \mydc{c}_n : \mytele_n } \\
        \myelabf &
        
        \begin{array}{r@{\ }c@{\ }l}
          \mytmsyn & ::= & \cdots \mysynsep \myapp{\mytyc{D}}{\mytmsyn^{\mytele}} \mysynsep \cdots \mysynsep
          \mytyc{D}.\mydc{c}_n \myappsp \mytmsyn^{\mytele_n} \mysynsep \mytyc{D}.\myfun{elim} \myappsp \mytmsyn \\
        \end{array}
      \end{array}
      $
  }

    \mynegder

  \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
        \footnotesize

      \AxiomC{$
        \begin{array}{c}
          \myinf{\mytele \myarr \mytyp}{\mytyp}\hspace{0.8cm}
          \mytyc{D} \not\in \myctx \\
          \myinff{\myctx;\ \mytyc{D} : \mytele \myarr \mytyp}{\mytele \mycc \mytele_i \myarr \myapp{\mytyc{D}}{\mytelee}}{\mytyp}\ \ \ (1 \leq i \leq n) \\
          \text{For each $(\myb{x} {:} \mytya)$ in each $\mytele_i$, if $\mytyc{D} \in \mytya$, then $\mytya = \myapp{\mytyc{D}}{\vec{\mytmt}}$.}
        \end{array}
          $}
      \UnaryInfC{$
        \begin{array}{r@{\ }c@{\ }l}
          \myctx & \myelabt & \myadt{\mytyc{D}}{\mytele}{}{ \cdots \ |\ \mydc{c}_n : \mytele_n } \\
          & & \vspace{-0.2cm} \\
          & \myelabf & \myctx;\ \mytyc{D} : \mytele \myarr \mytyp;\ \cdots;\ \mytyc{D}.\mydc{c}_n : \mytele \mycc \mytele_n \myarr \myapp{\mytyc{D}}{\mytelee}; \\
          &          &
          \begin{array}{@{}r@{\ }l l}
            \mytyc{D}.\myfun{elim} : & \mytele \myarr (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr & \textbf{target} \\
            & (\myb{P} {:} \myapp{\mytyc{D}}{\mytelee} \myarr \mytyp) \myarr & \textbf{motive} \\
            & \left.
              \begin{array}{@{}l}
                \myind{3} \vdots \\
                (\mytele_n \mycc \myhyps(\myb{P}, \mytele_n) \myarr \myapp{\myb{P}}{(\myapp{\mytyc{D}.\mydc{c}_n}{\mytelee_n})}) \myarr
              \end{array} \right \}
            & \textbf{methods}  \\
            & \myapp{\myb{P}}{\myb{x}} &
          \end{array}
        \end{array}
        $}
      \DisplayProof \\ \vspace{0.2cm}\ \\
      $
        \begin{array}{@{}l l@{\ } l@{} r c l}
          \textbf{where} & \myhyps(\myb{P}, & \myemptytele &) & \mymetagoes & \myemptytele \\
          & \myhyps(\myb{P}, & (\myb{r} {:} \myapp{\mytyc{D}}{\vec{\mytmt}}) \mycc \mytele &) & \mymetagoes & (\myb{r'} {:} \myapp{\myb{P}}{\myb{r}}) \mycc \myhyps(\myb{P}, \mytele) \\
          & \myhyps(\myb{P}, & (\myb{x} {:} \mytya) \mycc \mytele & ) & \mymetagoes & \myhyps(\myb{P}, \mytele)
        \end{array}
        $

  }

    \mynegder

  \mydesc{reduction elaboration:}{\mydeclsyn \myelabf \myctx \vdash \mytmsyn \myred \mytmsyn}{  
        \footnotesize
        $\myadt{\mytyc{D}}{\mytele}{}{ \cdots \ |\ \mydc{c}_n : \mytele_n } \ \ \myelabf$
      \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
      \AxiomC{$\mytyc{D}.\mydc{c}_i : \mytele;\mytele_i \myarr \myapp{\mytyc{D}}{\mytelee} \in \myctx$}
      \BinaryInfC{$
          \myctx \vdash \myapp{\myapp{\myapp{\mytyc{D}.\myfun{elim}}{(\myapp{\mytyc{D}.\mydc{c}_i}{\vec{\myse{t}}})}}{\myse{P}}}{\vec{\myse{m}}} \myred \myapp{\myapp{\myse{m}_i}{\vec{\mytmt}}}{\myrecs(\myse{P}, \vec{m}, \mytele_i)}
        $}
      \DisplayProof \\ \vspace{0.2cm}\ \\
      $
        \begin{array}{@{}l l@{\ } l@{} r c l}
          \textbf{where} & \myrecs(\myse{P}, \vec{m}, & \myemptytele &) & \mymetagoes & \myemptytele \\
                         & \myrecs(\myse{P}, \vec{m}, & (\myb{r} {:} \myapp{\mytyc{D}}{\vec{A}}); \mytele & ) & \mymetagoes &  (\mytyc{D}.\myfun{elim} \myappsp \myb{r} \myappsp \myse{P} \myappsp \vec{m}); \myrecs(\myse{P}, \vec{m}, \mytele) \\
                         & \myrecs(\myse{P}, \vec{m}, & (\myb{x} {:} \mytya); \mytele &) & \mymetagoes & \myrecs(\myse{P}, \vec{m}, \mytele)
        \end{array}
        $
  }

    \mynegder

    \mydesc{syntax elaboration:}{\myelab{\mydeclsyn}{\mytmsyn ::= \cdots}}{
          \footnotesize
    $
    \begin{array}{r@{\ }c@{\ }l}
      \myctx & \myelabt & \myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \\
             & \myelabf &

             \begin{array}{r@{\ }c@{\ }l}
               \mytmsyn & ::= & \cdots \mysynsep \myapp{\mytyc{D}}{\mytmsyn^{\mytele}} \mysynsep \mytyc{D}.\mydc{constr} \myappsp \mytmsyn^{n} \mysynsep \cdots  \mysynsep \mytyc{D}.\myfun{f}_n \myappsp \mytmsyn \\
             \end{array}
    \end{array}
    $
}

    \mynegder

\mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
      \footnotesize
    \AxiomC{$
      \begin{array}{c}
        \myinf{\mytele \myarr \mytyp}{\mytyp}\hspace{0.8cm}
        \mytyc{D} \not\in \myctx \\
        \myinff{\myctx; \mytele; (\myb{f}_j : \myse{F}_j)_{j=1}^{i - 1}}{F_i}{\mytyp} \myind{3} (1 \le i \le n)
      \end{array}
        $}
    \UnaryInfC{$
      \begin{array}{r@{\ }c@{\ }l}
        \myctx & \myelabt & \myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \\
        & & \vspace{-0.2cm} \\
        & \myelabf & \myctx;\ \mytyc{D} : \mytele \myarr \mytyp;\ \cdots;\ \mytyc{D}.\myfun{f}_n : \mytele \myarr (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr \mysub{\myse{F}_n}{\myb{f}_i}{\myapp{\myfun{f}_i}{\myb{x}}}_{i = 1}^{n-1}; \\
        & & \mytyc{D}.\mydc{constr} : \mytele \myarr \myse{F}_1 \myarr \cdots \myarr \myse{F}_n \myarr \myapp{\mytyc{D}}{\mytelee};
      \end{array}
      $}
    \DisplayProof
}

    \mynegder

  \mydesc{reduction elaboration:}{\mydeclsyn \myelabf \myctx \vdash \mytmsyn \myred \mytmsyn}{
        \footnotesize
          $\myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \ \ \myelabf$
          \AxiomC{$\mytyc{D} \in \myctx$}
          \UnaryInfC{$\myctx \vdash \myapp{\mytyc{D}.\myfun{f}_i}{(\mytyc{D}.\mydc{constr} \myappsp \vec{t})} \myred t_i$}
          \DisplayProof
  }

  \caption{Elaboration for data types and records.}
  \label{fig:elab}
\end{figure}

Following the intuition given by the examples, the mechanised
elaboration is presented in figure \ref{fig:elab}, which is essentially
a modification of figure 9 of \citep{McBride2004}\footnote{However, our
  datatypes do not have indices, we do bidirectional typechecking by
  treating constructors/destructors as syntactic constructs, and we have
  records.}.

In data types declarations we allow recursive occurrences as long as
they are \emph{strictly positive}, employing a syntactic check to make
sure that this is the case.  See \cite{Dybjer1991} for a more formal
treatment of inductive definitions in ITT.

For what concerns records, recursive occurrences are disallowed.  The
reason for this choice is answered by the reason for the choice of
having records at all: we need records to give the user types with
$\eta$-laws for equality, as we saw in Section \ref{sec:eta-expand}
and in the treatment of OTT in Section \ref{sec:ott}.  If we tried to
$\eta$-expand recursive data types, we would expand forever.

To implement bidirectional type checking for constructors and
destructors, we store their types in full in the context, and then
instantiate when due:

\mydesc{typing:}{\myctx \vdash \mytmsyn \Leftrightarrow \mytmsyn}{
    \AxiomC{$
      \begin{array}{c}
        \mytyc{D} : \mytele \myarr \mytyp \in \myctx \hspace{1cm}
        \mytyc{D}.\mydc{c} : \mytele \mycc \mytele' \myarr
        \myapp{\mytyc{D}}{\mytelee} \in \myctx \\
        \mytele'' = (\mytele;\mytele')\vec{A} \hspace{1cm}
        \mychkk{\myctx; \mytake_{i-1}(\mytele'')}{t_i}{\myix_i( \mytele'')}\ \ 
          (1 \le i \le \mytele'')
      \end{array}
      $}
    \UnaryInfC{$\mychk{\myapp{\mytyc{D}.\mydc{c}}{\vec{t}}}{\myapp{\mytyc{D}}{\vec{A}}}$}
    \DisplayProof

    \myderivspp

    \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
    \AxiomC{$\mytyc{D}.\myfun{f} : \mytele \mycc (\myb{x} {:}
      \myapp{\mytyc{D}}{\mytelee}) \myarr \myse{F}$}
    \AxiomC{$\myjud{\mytmt}{\myapp{\mytyc{D}}{\vec{A}}}$}
    \TrinaryInfC{$\myinf{\myapp{\mytyc{D}.\myfun{f}}{\mytmt}}{(\mytele
        \mycc (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr
        \myse{F})(\vec{A};\mytmt)}$}
    \DisplayProof
  }

\subsubsection{Why user defined types?  Why eliminators?}

The `hardest' design choice when designing $\mykant$\ was to decide
whether user defined types should be included.  In the end, we can
devise

% TODO reference levitated theories, indexed containers

foobar

\subsection{Cumulative hierarchy and typical ambiguity}
\label{sec:term-hierarchy}

Having a well founded type hierarchy is crucial if we want to retain
consistency, otherwise we can break our type systems by proving bottom,
as shown in Appendix \ref{sec:hurkens}.

However, hierarchy as presented in section \label{sec:itt} is a
considerable burden on the user, on various levels.  Consider for
example how we recovered disjunctions in Section \ref{sec:disju}: we
have a function that takes two $\mytyp_0$ and forms a new $\mytyp_0$.
What if we wanted to form a disjunction containing something a
$\mytyp_1$, or $\mytyp_{42}$?  Our definition would fail us, since
$\mytyp_1 : \mytyp_2$.

\begin{figure}[b!]

  % TODO finish
\mydesc{cumulativity:}{\myctx \vdash \mytmsyn \mycumul \mytmsyn}{
  \begin{tabular}{ccc}
    \AxiomC{$\myctx \vdash \mytya \mydefeq \mytyb$}
    \UnaryInfC{$\myctx \vdash \mytya \mycumul \mytyb$}
    \DisplayProof
    &
    \AxiomC{\phantom{$\myctx \vdash \mytya \mydefeq \mytyb$}}
    \UnaryInfC{$\myctx \vdash \mytyp_l \mycumul \mytyp_{l+1}$}
    \DisplayProof
    &
    \AxiomC{$\myctx \vdash \mytya \mycumul \mytyb$}
    \AxiomC{$\myctx \vdash \mytyb \mycumul \myse{C}$}
    \BinaryInfC{$\myctx \vdash \mytya \mycumul \myse{C}$}
    \DisplayProof
  \end{tabular}

  \myderivspp

  \begin{tabular}{ccc}
    \AxiomC{$\myjud{\mytmt}{\mytya}$}
    \AxiomC{$\myctx \vdash \mytya \mycumul \mytyb$}
    \BinaryInfC{$\myjud{\mytmt}{\mytyb}$}
    \DisplayProof
    &
    \AxiomC{$\myctx \vdash \mytya_1 \mydefeq \mytya_2$}
    \AxiomC{$\myctx; \myb{x} : \mytya_1 \vdash \mytyb_1 \mycumul \mytyb_2$}
    \BinaryInfC{$\myctx (\myb{x} {:} \mytya_1) \myarr \mytyb_1 \mycumul  (\myb{x} {:} \mytya_2) \myarr \mytyb_2$}
    \DisplayProof
  \end{tabular}
}
\caption{Cumulativity rules for base types in \mykant, plus a
  `conversion' rule for cumulative types.}
  \label{fig:cumulativity}
\end{figure}

One way to solve this issue is a \emph{cumulative} hierarchy, where
$\mytyp_{l_1} : \mytyp_{l_2}$ iff $l_1 < l_2$.  This way we retain
consistency, while allowing for `large' definitions that work on small
types too.  Figure \ref{fig:cumulativity} gives a formal definition of
cumulativity for types, abstractions, and data constructors.

For example we might define our disjunction to be
\[
  \myarg\myfun{$\vee$}\myarg : \mytyp_{100} \myarr \mytyp_{100} \myarr \mytyp_{100}
\]
And hope that $\mytyp_{100}$ will be large enough to fit all the types
that we want to use with our disjunction.  However, there are two
problems with this.  First, there is the obvious clumsyness of having to
manually specify the size of types.  More importantly, if we want to use
$\myfun{$\vee$}$ itself as an argument to other type-formers, we need to
make sure that those allow for types at least as large as
$\mytyp_{100}$.

A better option is to employ a mechanised version of what Russell called
\emph{typical ambiguity}: we let the user live under the illusion that
$\mytyp : \mytyp$, but check that the statements about types are
consistent behind the hood.  $\mykant$\ implements this following the
lines of \cite{Huet1988}.  See also \citep{Harper1991} for a published
reference, although describing a more complex system allowing for both
explicit and explicit hierarchy at the same time.

We define a partial ordering on the levels, with both weak ($\le$) and
strong ($<$) constraints---the laws governing them being the same as the
ones governing $<$ and $\le$ for the natural numbers.  Each occurrence
of $\mytyp$ is decorated with a unique reference, and we keep a set of
constraints and add new constraints as we type check, generating new
references when needed.

For example, when type checking the type $\mytyp\, r_1$, where $r_1$
denotes the unique reference assigned to that term, we will generate a
new fresh reference $\mytyp\, r_2$, and add the constraint $r_1 < r_2$
to the set.  When type checking $\myctx \vdash
\myfora{\myb{x}}{\mytya}{\mytyb}$, if $\myctx \vdash \mytya : \mytyp\,
r_1$ and $\myctx; \myb{x} : \mytyb \vdash \mytyb : \mytyp\,r_2$; we will
generate new reference $r$ and add $r_1 \le r$ and $r_2 \le r$ to the
set.

If at any point the constraint set becomes inconsistent, type checking
fails.  Moreover, when comparing two $\mytyp$ terms we equate their
respective references with two $\le$ constraints---the details are
explained in Section \ref{sec:hier-impl}.

Another more flexible but also more verbose alternative is the one
chosen by Agda, where levels can be quantified so that the relationship
between arguments and result in type formers can be explicitly
expressed:
\[
\myarg\myfun{$\vee$}\myarg : (l_1\, l_2 : \mytyc{Level}) \myarr \mytyp_{l_1} \myarr \mytyp_{l_2} \myarr \mytyp_{l_1 \mylub l_2}
\]
Inference algorithms to automatically derive this kind of relationship
are currently subject of research.  We chose less flexible but more
concise way, since it is easier to implement and better understood.

% \begin{figure}[t]
%   % TODO do this
%   \caption{Constraints generated by the typical ambiguity engine.  We
%     assume some global set of constraints with the ability of generating
%     fresh references.}
%   \label{fig:hierarchy}
% \end{figure}

\subsection{Observational equality, \mykant\ style}

There are two correlated differences between $\mykant$\ and the theory
used to present OTT.  The first is that in $\mykant$ we have a type
hierarchy, which lets us, for example, abstract over types.  The second
is that we let the user define inductive types.

Reconciling propositions for OTT and a hierarchy had already been
investigated by Conor McBride,\footnote{See
  \url{http://www.e-pig.org/epilogue/index.html?p=1098.html}.} and we
follow his broad design plan, although with some modifications.  Most of
the work, as an extension of elaboration, is to handle reduction rules
and coercions for data types---both type constructors and data
constructors.

\subsubsection{The \mykant\ prelude, and $\myprop$ositions}

Before defining $\myprop$, we define some basic types inside $\mykant$,
as the target for the $\myprop$ decoder:
\[
\begin{array}{l}
  \myadt{\mytyc{Empty}}{}{ }{ } \\
  \myfun{absurd} : (\myb{A} {:} \mytyp) \myarr \mytyc{Empty} \myarr \myb{A} \mapsto \\
  \myind{2} \myabs{\myb{A\ \myb{bot}}}{\mytyc{Empty}.\myfun{elim} \myappsp \myb{bot} \myappsp (\myabs{\_}{\myb{A}})} \\
  \ \\

  \myreco{\mytyc{Unit}}{}{}{ } \\ \ \\

  \myreco{\mytyc{Prod}}{\myappsp (\myb{A}\ \myb{B} {:} \mytyp)}{ }{\myfun{fst} : \myb{A}, \myfun{snd} : \myb{B} }
\end{array}
\]
When using $\mytyc{Prod}$, we shall use $\myprod$ to define `nested'
products, and $\myproj{n}$ to project elements from them, so that
\[
\begin{array}{@{}l}
\mytya \myprod \mytyb = \mytyc{Prod} \myappsp \mytya \myappsp (\mytyc{Prod} \myappsp \mytyb \myappsp \myunit) \\
\mytya \myprod \mytyb \myprod \myse{C} = \mytyc{Prod} \myappsp \mytya \myappsp (\mytyc{Prod} \myappsp \mytyb \myappsp (\mytyc{Prod} \myappsp \mytyc \myappsp \myunit)) \\
\myind{2} \vdots \\
\myproj{1} : \mytyc{Prod} \myappsp \mytya \myappsp \mytyb \myarr \mytya \\
\myproj{2} : \mytyc{Prod} \myappsp \mytya \myappsp (\mytyc{Prod} \myappsp \mytyb \myappsp \myse{C}) \myarr \mytyb \\
\myind{2} \vdots
\end{array}
\]
And so on, so that $\myproj{n}$ will work with all products with at
least than $n$ elements.  Then we can define propositions, and decoding:

\mydesc{syntax}{ }{
  $
  \begin{array}{r@{\ }c@{\ }l}
    \mytmsyn & ::= & \cdots \mysynsep \myprdec{\myprsyn} \\
    \myprsyn & ::= & \mybot \mysynsep \mytop \mysynsep \myprsyn \myand \myprsyn \mysynsep \myprfora{\myb{x}}{\mytmsyn}{\myprsyn}
  \end{array}
  $
}

\mydesc{proposition decoding:}{\myprdec{\mytmsyn} \myred \mytmsyn}{
  \begin{tabular}{cc}
    $
    \begin{array}{l@{\ }c@{\ }l}
      \myprdec{\mybot} & \myred & \myempty \\
      \myprdec{\mytop} & \myred & \myunit
    \end{array}
    $
    &
    $
    \begin{array}{r@{ }c@{ }l@{\ }c@{\ }l}
      \myprdec{&\myse{P} \myand \myse{Q} &} & \myred & \myprdec{\myse{P}} \myprod \myprdec{\myse{Q}} \\
      \myprdec{&\myprfora{\myb{x}}{\mytya}{\myse{P}} &} & \myred &
      \myfora{\myb{x}}{\mytya}{\myprdec{\myse{P}}}
    \end{array}
    $
  \end{tabular}
}

Adopting the same convention as with $\mytyp$-level products, we will
nest $\myand$ in the same way.

\subsubsection{Some OTT examples}

Before presenting the direction that $\mykant$\ takes, let's consider
some examples of use-defined data types, and the result we would expect,
given what we already know about OTT, assuming the same propositional
equalities.

\begin{description}

\item[Product types] Let's consider first the already mentioned
  dependent product, using the alternate name $\mysigma$\footnote{For
    extra confusion, `dependent products' are often called `dependent
    sums' in the literature, referring to the interpretation that
    identifies the first element as a `tag' deciding the type of the
    second element, which lets us recover sum types (disjuctions), as we
    saw in Section \ref{sec:user-type}.  Thus, $\mysigma$.} to
  avoid confusion with the $\mytyc{Prod}$ in the prelude:
  \[
  \begin{array}{@{}l}
    \myreco{\mysigma}{\myappsp (\myb{A} {:} \mytyp) \myappsp (\myb{B} {:} \myb{A} \myarr \mytyp)}{\\ \myind{2}}{\myfst : \myb{A}, \mysnd : \myapp{\myb{B}}{\myb{fst}}}
  \end{array}
  \]
  Let's start with type-level equality.  The result we want is
  \[
    \begin{array}{@{}l}
      \mysigma \myappsp \mytya_1 \myappsp \mytyb_1 \myeq \mysigma \myappsp \mytya_2 \myappsp \mytyb_2 \myred \\
      \myind{2} \mytya_1 \myeq \mytya_2 \myand \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{\myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2}} \myimpl \myapp{\mytyb_1}{\myb{x_1}} \myeq \myapp{\mytyb_2}{\myb{x_2}}}
    \end{array}
  \]
  The difference here is that in the original presentation of OTT
  the type binders are explicit, while here $\mytyb_1$ and $\mytyb_2$
  functions returning types.  We can do this thanks to the type
  hierarchy, and this hints at the fact that heterogeneous equality will
  have to allow $\mytyp$ `to the right of the colon', and in fact this
  provides the solution to simplify the equality above.

  If we take, just like we saw previously in OTT
  \[
    \begin{array}{@{}l}
      \myjm{\myse{f}_1}{\myfora{\mytya_1}{\myb{x_1}}{\mytyb_1}}{\myse{f}_2}{\myfora{\mytya_2}{\myb{x_2}}{\mytyb_2}} \myred \\
      \myind{2} \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{
           \myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2} \myimpl
           \myjm{\myapp{\myse{f}_1}{\myb{x_1}}}{\mytyb_1[\myb{x_1}]}{\myapp{\myse{f}_2}{\myb{x_2}}}{\mytyb_2[\myb{x_2}]}
         }}
    \end{array}
  \]
  Then we can simply take
  \[
    \begin{array}{@{}l}
      \mysigma \myappsp \mytya_1 \myappsp \mytyb_1 \myeq \mysigma \myappsp \mytya_2 \myappsp \mytyb_2 \myred \\ \myind{2} \mytya_1 \myeq \mytya_2 \myand \myjm{\mytyb_1}{\mytya_1 \myarr \mytyp}{\mytyb_2}{\mytya_2 \myarr \mytyp}
    \end{array}
  \]
  Which will reduce to precisely what we desire.  For what
  concerns coercions and quotation, things stay the same (apart from the
  fact that we apply to the second argument instead of substituting).
  We can recognise records such as $\mysigma$ as such and employ
  projections in value equality and coercions; as to not
  impede progress if not necessary.

\item[Lists] Now for finite lists, which will give us a taste for data
  constructors:
  \[
  \begin{array}{@{}l}
    \myadt{\mylist}{\myappsp (\myb{A} {:} \mytyp)}{ }{\mydc{nil} \mydcsep \mydc{cons} \myappsp \myb{A} \myappsp (\myapp{\mylist}{\myb{A}})}
  \end{array}
  \]
  Type equality is simple---we only need to compare the parameter:
  \[
    \mylist \myappsp \mytya_1 \myeq \mylist \myappsp \mytya_2 \myred \mytya_1 \myeq \mytya_2
    \]
    For coercions, we transport based on the constructor, recycling the
    proof for the inductive occurrence:
  \[
    \begin{array}{@{}l@{\ }c@{\ }l}
      \mycoe \myappsp (\mylist \myappsp \mytya_1) \myappsp (\mylist \myappsp \mytya_2) \myappsp \myse{Q} \myappsp \mydc{nil} & \myred & \mydc{nil} \\
      \mycoe \myappsp (\mylist \myappsp \mytya_1) \myappsp (\mylist \myappsp \mytya_2) \myappsp \myse{Q} \myappsp (\mydc{cons} \myappsp \mytmm \myappsp \mytmn) & \myred & \\
      \multicolumn{3}{l}{\myind{2} \mydc{cons} \myappsp (\mycoe \myappsp \mytya_1 \myappsp \mytya_2 \myappsp \myse{Q} \myappsp \mytmm) \myappsp (\mycoe \myappsp (\mylist \myappsp \mytya_1) \myappsp (\mylist \myappsp \mytya_2) \myappsp \myse{Q} \myappsp \mytmn)}
    \end{array}
  \]
  Value equality is unsurprising---we match the constructors, and
  return bottom for mismatches.  However, we also need to equate the
  parameter in $\mydc{nil}$:
  \[
    \begin{array}{r@{ }c@{\ }c@{\ }c@{}l@{\ }c@{\ }r@{}c@{\ }c@{\ }c@{}l@{\ }l}
      (& \mydc{nil} & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{nil} & : & \myapp{\mylist}{\mytya_2} &) \myred \mytya_1 \myeq \mytya_2 \\
      (& \mydc{cons} \myappsp \mytmm_1 \myappsp \mytmn_1 & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{cons} \myappsp \mytmm_2 \myappsp \mytmn_2 & : & \myapp{\mylist}{\mytya_2} &) \myred \\
      & \multicolumn{11}{@{}l}{ \myind{2}
        \myjm{\mytmm_1}{\mytya_1}{\mytmm_2}{\mytya_2} \myand \myjm{\mytmn_1}{\myapp{\mylist}{\mytya_1}}{\mytmn_2}{\myapp{\mylist}{\mytya_2}}
        } \\
      (& \mydc{nil} & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{cons} \myappsp \mytmm_2 \myappsp \mytmn_2 & : & \myapp{\mylist}{\mytya_2} &) \myred \mybot \\
      (& \mydc{cons} \myappsp \mytmm_1 \myappsp \mytmn_1 & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{nil} & : & \myapp{\mylist}{\mytya_2} &) \myred \mybot
    \end{array}
  \]
  % TODO quotation

\item[Evil type]
  Now for something useless but complicated.

\end{description}

\subsubsection{Only one equality}

Given the examples above, a more `flexible' heterogeneous emerged, since
of the fact that in $\mykant$ we re-gain the possibility of abstracting
and in general handling sets in a way that was not possible in the
original OTT presentation.  Moreover, we found that the rules for value
equality work very well if used with user defined type
abstractions---for example in the case of dependent products we recover
the original definition with explicit binders, in a very simple manner.

In fact, we can drop a separate notion of type-equality, which will
simply be served by $\myjm{\mytya}{\mytyp}{\mytyb}{\mytyp}$, from now on
abbreviated as $\mytya \myeq \mytyb$.  We shall still distinguish
equalities relating types for hierarchical purposes.  The full rules for
equality reductions, along with the syntax for propositions, are given
in figure \ref{fig:kant-eq-red}.  We exploit record to perform
$\eta$-expansion.  Moreover, given the nested $\myand$s, values of data
types with zero constructors (such as $\myempty$) and records with zero
destructors (such as $\myunit$) will be automatically always identified
as equal.

\begin{figure}[p]
\mydesc{syntax}{ }{
  \small
  $
  \begin{array}{r@{\ }c@{\ }l}
    \myprsyn & ::= & \cdots \mysynsep \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
  \end{array}
  $
}

    % \mytmsyn & ::= & \cdots \mysynsep \mycoee{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \mysynsep
    %                  \mycohh{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
    % \myprsyn & ::= & \cdots \mysynsep \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\

% \mynegder

% \mydesc{typing:}{\myctx \vdash \mytmsyn \Leftrightarrow \mytmsyn}{
%   \small
%   \begin{tabular}{cc}
%     \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
%     \AxiomC{$\myjud{\mytmt}{\mytya}$}
%     \BinaryInfC{$\myinf{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}$}
%     \DisplayProof
%     &
%     \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
%     \AxiomC{$\myjud{\mytmt}{\mytya}$}
%     \BinaryInfC{$\myinf{\mycohh{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\myprdec{\myjm{\mytmt}{\mytya}{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}}}$}
%     \DisplayProof
%   \end{tabular}
% }

\mynegder

\mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
  \small
    \begin{tabular}{cc}
      \AxiomC{\phantom{$\myjud{\myse{P}}{\myprop}$}}
      \UnaryInfC{$\myjud{\mytop}{\myprop}$}
      \noLine
      \UnaryInfC{$\myjud{\mybot}{\myprop}$}
      \DisplayProof
      &
      \AxiomC{$\myjud{\myse{P}}{\myprop}$}
      \AxiomC{$\myjud{\myse{Q}}{\myprop}$}
      \BinaryInfC{$\myjud{\myse{P} \myand \myse{Q}}{\myprop}$}
      \noLine
      \UnaryInfC{\phantom{$\myjud{\mybot}{\myprop}$}}
      \DisplayProof
    \end{tabular}

    \myderivspp

    \begin{tabular}{cc}
      \AxiomC{$
        \begin{array}{@{}c}
          \phantom{\myjud{\myse{A}}{\mytyp} \hspace{0.8cm} \myjud{\mytmm}{\myse{A}}} \\
          \myjud{\myse{A}}{\mytyp}\hspace{0.8cm}
          \myjudd{\myctx; \myb{x} : \mytya}{\myse{P}}{\myprop}
        \end{array}
        $}
      \UnaryInfC{$\myjud{\myprfora{\myb{x}}{\mytya}{\myse{P}}}{\myprop}$}
      \DisplayProof
      &
      \AxiomC{$
        \begin{array}{c}
          \myjud{\myse{A}}{\mytyp} \hspace{0.8cm} \myjud{\mytmm}{\myse{A}} \\
          \myjud{\myse{B}}{\mytyp} \hspace{0.8cm} \myjud{\mytmn}{\myse{B}}
        \end{array}
        $}
      \UnaryInfC{$\myjud{\myjm{\mytmm}{\myse{A}}{\mytmn}{\myse{B}}}{\myprop}$}
      \DisplayProof
    \end{tabular}
}

\mynegder
  % TODO equality for decodings
\mydesc{equality reduction:}{\myctx \vdash \myprsyn \myred \myprsyn}{
  \small
    \begin{tabular}{cc}
    \AxiomC{}
    \UnaryInfC{$\myctx \vdash \myjm{\mytyp}{\mytyp}{\mytyp}{\mytyp} \myred \mytop$}
    \DisplayProof
    &
    \AxiomC{}
    \UnaryInfC{$\myctx \vdash \myjm{\myprdec{\myse{P}}}{\mytyp}{\myprdec{\myse{Q}}}{\mytyp} \myred \mytop$}
    \DisplayProof
    \end{tabular}

  \myderivspp

  \AxiomC{}
  \UnaryInfC{$
    \begin{array}{@{}r@{\ }l}
    \myctx \vdash &
    \myjm{\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}}{\mytyp}{\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}}{\mytyp}  \myred \\
    & \myind{2} \mytya_2 \myeq \mytya_1 \myand \myprfora{\myb{x_2}}{\mytya_2}{\myprfora{\myb{x_1}}{\mytya_1}{
        \myjm{\myb{x_2}}{\mytya_2}{\myb{x_1}}{\mytya_1} \myimpl \mytyb_1[\myb{x_1}] \myeq \mytyb_2[\myb{x_2}]
      }}
    \end{array}
    $}
  \DisplayProof

  \myderivspp

  \AxiomC{}
  \UnaryInfC{$
    \begin{array}{@{}r@{\ }l}
      \myctx \vdash &
      \myjm{\myse{f}_1}{\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}}{\myse{f}_2}{\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}}  \myred \\
      & \myind{2} \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{
          \myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2} \myimpl
          \myjm{\myapp{\myse{f}_1}{\myb{x_1}}}{\mytyb_1[\myb{x_1}]}{\myapp{\myse{f}_2}{\myb{x_2}}}{\mytyb_2[\myb{x_2}]}
        }}
    \end{array}
    $}
  \DisplayProof
  

  \myderivspp

  \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
  \UnaryInfC{$
    \begin{array}{r@{\ }l}
      \myctx \vdash &
      \myjm{\mytyc{D} \myappsp \vec{A}}{\mytyp}{\mytyc{D} \myappsp \vec{B}}{\mytyp}  \myred \\
      & \myind{2} \mybigand_{i = 1}^n (\myjm{\mytya_n}{\myhead(\mytele(A_1 \cdots A_{i-1}))}{\mytyb_i}{\myhead(\mytele(B_1 \cdots B_{i-1}))})
    \end{array}
    $}
  \DisplayProof

  \myderivspp

  \AxiomC{$
    \begin{array}{@{}c}
      \mydataty(\mytyc{D}, \myctx)\hspace{0.8cm}
      \mytyc{D}.\mydc{c} : \mytele;\mytele' \myarr \mytyc{D} \myappsp \mytelee \in \myctx \hspace{0.8cm}
      \mytele_A = (\mytele;\mytele')\vec{A}\hspace{0.8cm}
      \mytele_B = (\mytele;\mytele')\vec{B}
    \end{array}
    $}
  \UnaryInfC{$
    \begin{array}{@{}l@{\ }l}
      \myctx \vdash & \myjm{\mytyc{D}.\mydc{c} \myappsp \vec{\myse{l}}}{\mytyc{D} \myappsp \vec{A}}{\mytyc{D}.\mydc{c} \myappsp \vec{\myse{r}}}{\mytyc{D} \myappsp \vec{B}} \myred \\
      & \myind{2} \mybigand_{i=1}^n(\myjm{\mytmm_i}{\myhead(\mytele_A (\mytya_i \cdots \mytya_{i-1}))}{\mytmn_i}{\myhead(\mytele_B (\mytyb_i \cdots \mytyb_{i-1}))})
    \end{array}
    $}
  \DisplayProof

  \myderivspp

  \AxiomC{$\mydataty(\mytyc{D}, \myctx)$}
  \UnaryInfC{$
      \myctx \vdash \myjm{\mytyc{D}.\mydc{c} \myappsp \vec{\myse{l}}}{\mytyc{D} \myappsp \vec{A}}{\mytyc{D}.\mydc{c'} \myappsp \vec{\myse{r}}}{\mytyc{D} \myappsp \vec{B}} \myred \mybot
    $}
  \DisplayProof

  \myderivspp

  \AxiomC{$
    \begin{array}{@{}c}
      \myisreco(\mytyc{D}, \myctx)\hspace{0.8cm}
      \mytyc{D}.\myfun{f}_i : \mytele; (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr \myse{F}_i  \in \myctx\\
    \end{array}
    $}
  \UnaryInfC{$
    \begin{array}{@{}l@{\ }l}
      \myctx \vdash & \myjm{\myse{l}}{\mytyc{D} \myappsp \vec{A}}{\myse{r}}{\mytyc{D} \myappsp \vec{B}} \myred \\ & \myind{2} \mybigand_{i=1}^n(\myjm{\mytyc{D}.\myfun{f}_1 \myappsp \myse{l}}{(\mytele; (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr \myse{F}_i)(\vec{\mytya};\myse{l})}{\mytyc{D}.\myfun{f}_i \myappsp \myse{r}}{(\mytele; (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr \myse{F}_i)(\vec{\mytyb};\myse{r})})
    \end{array}
    $}
  \DisplayProof
  
  \myderivspp
  \AxiomC{}
  \UnaryInfC{$\myjm{\mytmm}{\mytya}{\mytmn}{\mytyb}  \myred \mybot\ \text{if $\mytya$ and $\mytyb$ are canonical types.}$}
  \DisplayProof
}
\caption{Propositions and equality reduction in $\mykant$.  We assume
  the presence of $\mydataty$ and $\myisreco$ as operations on the
  context to recognise whether a user defined type is a data type or a
  record.}
  \label{fig:kant-eq-red}
\end{figure}

\subsubsection{Coercions}

% \begin{figure}[t]
%   \mydesc{reduction}{\mytmsyn \myred \mytmsyn}{

%   }
%   \caption{Coercions in \mykant.}
%   \label{fig:kant-coe}
% \end{figure}

% TODO finish

\subsubsection{$\myprop$ and the hierarchy}

Where is $\myprop$ placed in the type hierarchy?  The main indicator
is the decoding operator, since it converts into things that already
live in the hierarchy.  For example, if we
have
\[
  \myprdec{\mynat \myarr \mybool \myeq \mynat \myarr \mybool} \myred
  \mytop \myand ((\myb{x}\, \myb{y} : \mynat) \myarr \mytop \myarr \mytop)
\]
we will better make sure that the `to be decoded' is at the same
level as its reduction as to preserve subject reduction.  In the example
above, we'll have that proposition to be at least as large as the type
of $\mynat$, since the reduced proof will abstract over it.  Pretending
that we had explicit, non cumulative levels, it would be tempting to have
\begin{center}
\begin{tabular}{cc}
  \AxiomC{$\myjud{\myse{Q}}{\myprop_l}$}
  \UnaryInfC{$\myjud{\myprdec{\myse{Q}}}{\mytyp_l}$}
  \DisplayProof
&
  \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
  \AxiomC{$\myjud{\mytyb}{\mytyp_l}$}
  \BinaryInfC{$\myjud{\myjm{\mytya}{\mytyp_{l}}{\mytyb}{\mytyp_{l}}}{\myprop_l}$}
  \DisplayProof
\end{tabular}
\end{center}
$\mybot$ and $\mytop$ living at any level, $\myand$ and $\forall$
following rules similar to the ones for $\myprod$ and $\myarr$ in
Section \ref{sec:itt}. However, we need to be careful with value
equality since for example we have that
\[
  \myprdec{\myjm{\myse{f}_1}{\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}}{\myse{f}_2}{\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}}}
  \myred
  \myfora{\myb{x_1}}{\mytya_1}{\myfora{\myb{x_2}}{\mytya_2}{\cdots}}
\]
where the proposition decodes into something of type $\mytyp_l$, where
$\mytya : \mytyp_l$ and $\mytyb : \mytyp_l$.  We can resolve this
tension by making all equalities larger:
\begin{prooftree}
  \AxiomC{$\myjud{\mytmm}{\mytya}$}
  \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
  \AxiomC{$\myjud{\mytmn}{\mytyb}$}
  \AxiomC{$\myjud{\mytyb}{\mytyp_l}$}
  \QuaternaryInfC{$\myjud{\myjm{\mytmm}{\mytya}{\mytmm}{\mytya}}{\myprop_l}$}
\end{prooftree}
This is disappointing, since type equalities will be needlessly large:
$\myprdec{\myjm{\mytya}{\mytyp_l}{\mytyb}{\mytyp_l}} : \mytyp_{l + 1}$.

However, considering that our theory is cumulative, we can do better.
Assuming rules for $\myprop$ cumulativity similar to the ones for
$\mytyp$, we will have (with the conversion rule reproduced as a
reminder):
\begin{center}
  \begin{tabular}{cc}
    \AxiomC{$\myctx \vdash \mytya \mycumul \mytyb$}
    \AxiomC{$\myjud{\mytmt}{\mytya}$}
    \BinaryInfC{$\myjud{\mytmt}{\mytyb}$}
    \DisplayProof
    &
    \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
    \AxiomC{$\myjud{\mytyb}{\mytyp_l}$}
    \BinaryInfC{$\myjud{\myjm{\mytya}{\mytyp_{l}}{\mytyb}{\mytyp_{l}}}{\myprop_l}$}
    \DisplayProof
  \end{tabular}

  \myderivspp

  \AxiomC{$\myjud{\mytmm}{\mytya}$}
  \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
  \AxiomC{$\myjud{\mytmn}{\mytyb}$}
  \AxiomC{$\myjud{\mytyb}{\mytyp_l}$}
  \AxiomC{$\mytya$ and $\mytyb$ are not $\mytyp_{l'}$}
  \QuinaryInfC{$\myjud{\myjm{\mytmm}{\mytya}{\mytmm}{\mytya}}{\myprop_l}$}
  \DisplayProof
\end{center}

That is, we are small when we can (type equalities) and large otherwise.
This would not work in a non-cumulative theory because subject reduction
would not hold.  Consider for instance
\[
  \myjm{\mynat}{\myITE{\mytrue}{\mytyp_0}{\mytyp_0}}{\mybool}{\myITE{\mytrue}{\mytyp_0}{\mytyp_0}}
  : \myprop_1
\]
which reduces to
\[\myjm{\mynat}{\mytyp_0}{\mybool}{\mytyp_0} : \myprop_0 \]
We need $\myprop_0$ to be $\myprop_1$ too, which will be the case with
cumulativity.  This is not the most elegant of systems, but it buys us a
cheap type level equality without having to replicate functionality with
a dedicated construct.

\subsubsection{Quotation and definitional equality}
\label{sec:kant-irr}

Now we can give an account of definitional equality, by explaining how
to perform quotation (as defined in Section \ref{sec:eta-expand})
towards the goal described in Section \ref{sec:ott-quot}.

We want to:
\begin{itemize}
\item Perform $\eta$-expansion on functions and records.

\item As a consequence of the previous point, identify all records with
no projections as equal, since they will have only one element.

\item Identify all members of types with no elements as equal.

\item Identify all equivalent proofs as equal---with `equivalent proof'
we mean those proving the same propositions.

\item Advance coercions working across definitionally equal types.
\end{itemize}
Towards these goals and following the intuition between bidirectional
type checking we define two mutually recursive functions, one quoting
canonical terms against their types (since we need the type to typecheck
canonical terms), one quoting neutral terms while recovering their
types.

Our quotation will work on normalised terms, so that all defined values
will have been replaced.  Moreover, we match on datatype eliminators and
all their arguments, so that $\mynat.\myfun{elim} \myappsp \vec{\mytmt}$
will stand for $\mynat.\myfun{elim}$ applied to the scrutinised
$\mynat$, plus its three arguments.  This measure can be easily
implemented by checking the head of applications and `consuming' the
needed terms.

% TODO finish this
\begin{figure}[t]
  \mydesc{canonical quotation}{\myctx \vdash \mytmsyn \myquot \mytmsyn \mapsto \mytmsyn}{
                          
  }

  \mynegder

  \mydesc{neutral quotation}{\myctx \vdash \mynquot \mytmsyn  \mapsto \mytmsyn : \mytmsyn}{
                    
  }
  \caption{Quotation in \mykant.}
  \label{fig:kant-quot}
\end{figure}

% TODO finish

\subsubsection{Why $\myprop$?}

It is worth to ask if $\myprop$ is needed at all.  It is perfectly
possible to have the type checker identify propositional types
automatically, and in fact in some sense we already do during equality
reduction and quotation.  However, this has the considerable
disadvantage that we can never identify abstracted
variables\footnote{And in general neutral terms, although we currently
  don't have neutral propositions.} of type $\mytyp$ as $\myprop$, thus
forbidding the user to talk about $\myprop$ explicitly.

This is a considerable impediment, for example when implementing
\emph{quotient types}.  With quotients, we let the user specify an
equivalence class over a certain type, and then exploit this in various
way---crucially, we need to be sure that the equivalence given is
propositional, a fact which prevented the use of quotients in dependent
type theories \citep{Jacobs1994}.

% TODO finish

\section{\mykant : The practice}
\label{sec:kant-practice}

The codebase consists of around 2500 lines of Haskell, as reported by
the \texttt{cloc} utility.  The high level design is inspired by the
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 author learnt the hard way the implementations challenges for such a
project, and while there is a solid and working base to work on, the
implementation of observational equality is not currently complete.
However, given the detailed plan in the previous section, doing so
should not prove to be too much work.

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}[t]
{\small\begin{verbatim}B E R T U S
Version 0.0, made in London, year 2013.
>>> :h
<decl>     Declare value/data type/record
:t <term>  Typecheck
:e <term>  Normalise
:p <term>  Pretty print
:l <file>  Load file
:r <file>  Reload file (erases previous environment)
:i <name>  Info about an identifier
:q         Quit
>>> :l data/samples/good/common.ka 
OK
>>> :e plus three two
suc (suc (suc (suc (suc zero))))
>>> :t plus three two
Type: Nat\end{verbatim}
}

  \caption{A sample run of the \mykant\ 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 or
another REPL command, which then goes through various stages that can end up
in a context update, or in failures of various kind.  The process is described
diagrammatically in figure \ref{fig:kant-process}:

\begin{description}
\item[Parse] In this phase the text input gets converted to a sugared
  version of the core language.

\item[Desugar] The sugared declaration is converted to a core term.

\item[Reference] Occurrences of $\mytyp$ get decorated by a unique reference,
  which is necessary to implement the type hierarchy check.

\item[Elaborate] Converts the declaration to some context items, which
  might be a value declaration (type and body) or a data type
  declaration (constructors and destructors).  This phase works in
  tandem with \textbf{Type checking}, which in turns needs to
  \textbf{Evaluate} terms.

\item[Distill] and report the result.  `Distilling' refers to the process of
  converting a core term back to a sugared version that the user can
  visualise.  This can be necessary both to display errors including terms or
  to display result of evaluations or type checking that the user has
  requested.

\item[Pretty print] Format the terms in a nice way, and display the result to
  the user.

\end{description}

\begin{figure}
  \centering{\mysmall
    \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, left=of elaborate] (tycheck) {Typecheck};
        \node [block, left=of tycheck] (evaluate) {Evaluate};
        \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);
        \path [line] (tycheck) edge[bend right] (evaluate);
        \path [line] (evaluate) edge[bend right] (tycheck);
      \end{tikzpicture}
  }
  \caption{High level overview of the life of a \mykant\ prompt cycle.}
  \label{fig:kant-process}
\end{figure}

Here we will review only a sampling of the more interesting
implementation challenges present when implementing an interactive
theorem prover.

\subsection{Term and context representation}
\label{sec:term-repr}

\subsubsection{Naming and substituting}

Perhaps surprisingly, one of the most fundamental challenges in
implementing a theory of the kind presented is choosing a good data type
for terms, and specifically handling substitutions in a sane way.

There are two broad schools of thought when it comes to naming
variables, and thus substituting:
\begin{description}
\item[Nameful] Bound variables are represented by some enumerable data
  type, just as we have described up to now, starting from Section
  \ref{sec:untyped}.  The problem is that avoiding name capturing is a
  nightmare, both in the sense that it is not performant---given that we
  need to rename rename substitute each time we `enter' a binder---but
  most importantly given the fact that in even more slightly complicated
  systems it is very hard to get right, even for experts.

  One of the sore spots of explicit names is comparing terms up
  $\alpha$-renaming, which again generates a huge amounts of
  substitutions and requires special care.  We can represent the
  relationship between variables and their binders, by...

\item[Nameless] ...getting rid of names altogether, and representing
  bound variables with an index referring to the `binding' structure, a
  notion introduced by \cite{de1972lambda}.  Classically $0$ represents
  the variable bound by the innermost binding structure, $1$ the
  second-innermost, and so on.  For instance with simple abstractions we
  might have
  \[\mymacol{red}{\lambda}\, (\mymacol{blue}{\lambda}\, \mymacol{blue}{0}\, (\mymacol{AgdaInductiveConstructor}{\lambda\, 0}))\, (\mymacol{AgdaFunction}{\lambda}\, \mymacol{red}{1}\, \mymacol{AgdaFunction}{0}) : ((\mytya \myarr \mytya) \myarr \mytyb) \myarr \mytyb \]

  While this technique is obviously terrible in terms of human
  usability,\footnote{With some people going as far as defining it akin
  to an inverse Turing test.} it is much more convenient as an
  internal representation to deal with terms mechanically---at least in
  simple cases.  Moreover, $\alpha$ renaming ceases to be an issue, and
  term comparison is purely syntactical.

  Nonetheless, more complex, more complex constructs such as pattern
  matching put some strain on the indices and many systems end up using
  explicit names anyway (Agda, Coq, \dots).

\end{description}

In the past decade or so advancements in the Haskell's type system and
in general the spread new programming practices have enabled to make the
second option much more amenable.  \mykant\ thus takes the second path
through the use of Edward Kmett's excellent \texttt{bound}
library.\footnote{Available at
\url{http://hackage.haskell.org/package/bound}.}  We decribe its
advantages but also pitfalls in the previously relatively unknown
territory of dependent types---\texttt{bound} being created mostly to
handle more simply typed systems.

\texttt{bound} builds on two core ideas.  The first is the suggestion by
\cite{Bird1999} consists of parametrising the term type over the type of
the variables, and `nest' the type each time we enter a scope.  If we
wanted to define a term for the untyped $\lambda$-calculus, we might
have
\begin{Verbatim}
data Void

data Var v = Bound | Free v

data Tm v
    = V v               -- Bound variable
    | App (Tm v) (Tm v) -- Term application
    | Lam (Tm (Var v))  -- Abstraction
\end{Verbatim}
Closed terms would be of type \texttt{Tm Void}, so that there would be
no occurrences of \texttt{V}.  However, inside an abstraction, we can
have \texttt{V Bound}, representing the bound variable, and inside a
second abstraction we can have \texttt{V Bound} or \texttt{V (Free
Bound)}.  Thus the term $\myabs{\myb{x}}{\myabs{\myb{y}}{\myb{x}}}$ could be represented as
\begin{Verbatim}
Lam (Lam (Free Bound))
\end{Verbatim}
This allows us to reflect at the type level the `nestedness' of a type,
and since we usually work with functions polymorphic on the parameter
\texttt{v} it's very hard to make mistakes by putting terms of the wrong
nestedness where they don't belong.

Even more interestingly, the substitution operation is perfectly
captured by the \verb|>>=| (bind) operator of the \texttt{Monad}
typeclass:
\begin{Verbatim}
class Monad m where
  return :: m a
  (>>=)  :: m a -> (a -> m b) -> m b

instance Monad Tm where
  -- `return'ing turns a variable into a `Tm'
  return = V

  -- `t >>= f' takes a term `t' and a mapping from variables to terms
  -- `f' and applies `f' to all the variables in `t', replacing them
  -- with the mapped terms.
  V v     >>= f = f v
  App m n >>= f = App (m >>= f) (n >>= f)

  -- `Lam' is the tricky case: we modify the function to work with bound
  -- variables, so that if it encounters `Bound' it leaves it untouched
  -- (since the mapping referred to the outer scope); if it encounters a
  -- free variable it asks `f' for the term and then updates all the
  -- variables to make them refer to the outer scope they were meant to
  -- be in.
  Lam s   >>= f = Lam (s >>= bump)
    where bump Bound    = return Bound
          bump (Free v) = f v >>= V . Free
\end{Verbatim}
With this in mind, we can define functions which will not only work on
\verb|Tm|, but on any \verb|Monad|!
\begin{Verbatim}
-- Replaces free variable `v' with `m' in `n'.
subst :: (Eq v, Monad m) => v -> m v -> m v -> m v
subst v m n = n >>= \v' -> if v == v' then m else return v'

-- Replace the variable bound by `s' with term `t'.
inst :: Monad m => m v -> m (Var v) -> m v
inst t s = do v <- s
              case v of
                Bound   -> t
                Free v' -> return v'
\end{Verbatim}
The beauty of this technique is that in a few simple function we have
defined all the core operations in a general and `obviously correct'
way, with the extra confidence of having the type checker looking our
back.

Moreover, if we take the top level term type to be \verb|Tm String|, we
get for free a representation of terms with top-level, definitions;
where closed terms contain only \verb|String| references to said
definitions---see also \cite{McBride2004b}.

What are then the pitfalls of this seemingly invincible technique?  The
most obvious impediment is the need for polymorphic recursion.
Functions traversing terms parametrised by the variable type will have
types such as
\begin{Verbatim}
-- Infer the type of a term, or return an error.
infer :: Tm v -> Either Error (Tm v)
\end{Verbatim}
When traversing under a \verb|Scope| the parameter changes from \verb|v|
to \verb|Var v|, and thus if we do not specify the type for our function explicitly
inference will fail---type inference for polymorphic recursion being
undecidable \citep{henglein1993type}.  This causes some annoyance,
especially in the presence of many local definitions that we would like
to leave untyped.

But the real issue is the fact that giving a type parametrised over a
variable---say \verb|m v|---a \verb|Monad| instance means being able to
only substitute variables for values of type \verb|m v|.  This is a
considerable inconvenience.  Consider for instance the case of
telescopes, which are a central tool to deal with contexts and other
constructs:
\begin{Verbatim}
data Tele m v = End (m v) | Bind (m v) (Tele (Var v))
type TeleTm = Tele Tm
\end{Verbatim}
The problem here is that what we want to substitute for variables in
\verb|Tele m v| is \verb|m v| (probably \verb|Tm v|), not \verb|Tele m v| itself!  What we need is
\begin{Verbatim}
bindTele  :: Monad m => Tele m a -> (a -> m b) -> Tele m b
substTele :: (Eq v, Monad m) => v -> m v -> Tele m v -> Tele m v
instTele  :: Monad m => m v -> Tele m (Var v) -> Tele m v
\end{Verbatim}
Not what \verb|Monad| gives us.  Solving this issue in an elegant way
has been a major sink of time and source of headaches for the author,
who analysed some of the alternatives---most notably the work by
\cite{weirich2011binders}---but found it impossible to give up the
simplicity of the model above.

That said, our term type is still reasonably brief, as shown in full in
Figure \ref{fig:term}.  The fact that propositions cannot be factored
out in another data type is a consequence of the problems described
above.  However the real pain is during elaboration, where we are forced
to treat everything as a type while we would much rather have
telescopes.  Future work would include writing a library that marries a
nice interface similar to the one of \verb|bound| with a more flexible
interface.

\begin{figure}[t]
{\small\begin{verbatim}-- A top-level name.
type Id    = String
-- A data/type constructor name.
type ConId = String

-- A term, parametrised over the variable (`v') and over the reference
-- type used in the type hierarchy (`r').
data Tm r v
    = V v                        -- Variable.
    | Ty r                       -- Type, with a hierarchy reference.
    | Lam (TmScope r v)          -- Abstraction.
    | Arr (Tm r v) (TmScope r v) -- Dependent function.
    | App (Tm r v) (Tm r v)      -- Application.
    | Ann (Tm r v) (Tm r v)      -- Annotated term.
      -- Data constructor, the first ConId is the type constructor and
      -- the second is the data constructor.
    | Con ADTRec ConId ConId [Tm r v]
      -- Data destrutor, again first ConId being the type constructor
      -- and the second the name of the eliminator.
    | Destr ADTRec ConId Id (Tm r v)
      -- A type hole.
    | Hole HoleId [Tm r v]
      -- Decoding of propositions.
    | Dec (Tm r v)

      -- Propositions.
    | Prop r -- The type of proofs, with hierarchy reference.
    | Top
    | Bot
    | And (Tm r v) (Tm r v)
    | Forall (Tm r v) (TmScope r v)
      -- Heterogeneous equality.
    | Eq (Tm r v) (Tm r v) (Tm r v) (Tm r v)

-- Either a data type, or a record.
data ADTRec = ADT | Rec

-- Either a coercion, or coherence.
data Coeh = Coe | Coh\end{verbatim}
}
  \caption{Data type for terms in \mykant.}
  \label{fig:term}
\end{figure}

We also make use of a `forgetful' data type (as provided by
\verb|bound|) to store user-provided variables names along with the
`nameless' representation, so that the names will not be considered when
compared terms, but will be available when distilling so that we can
recover variable names that are as close as possible to what the user
originally used.

\subsubsection{Context}

% TODO finish

\subsection{Type hierarchy}
\label{sec:hier-impl}

As a breath of air amongst the type gas, we will explain how to
implement the typical ambiguity we have spoken about in
\ref{sec:term-hierarchy}.  As mentioned, we have to verify a the
consistency of a set of constraints each time we add a new one.  The
constraints range over some set of variables whose members we will
denote with $x, y, z, \dots$.  and are of two kinds:
\begin{center}
  \begin{tabular}{cc}
     $x \le y$ & $x < y$
  \end{tabular}
\end{center}

Predictably, $\le$ expresses a reflexive order, and $<$ expresses an
irreflexive order, both working with the same notion of equality, where
$x < y$ implies $x \le y$---they behave like $\le$ and $<$ do on natural
numbers (or in our case, levels in a type hierarchy).  We also need an
equality constraint ($x = y$), which can be reduced to two constraints
$x \le y$ and $y \le x$.

Given this specification, we have implemented a standalone Haskell
module---that we plan to release as a library---to efficiently store and
check the consistency of constraints.  Its interface is shown in Figure
\ref{fig:constraint}.  The problem unpredictably reduces to a graph
algorithm.  If we 

\begin{figure}[t]
{\small\begin{verbatim}module Data.Constraint where

-- | Data type holding the set of constraints, parametrised over the
--   type of the variables.
data Constrs a

-- | A representation of the constraints that we can add.
data Constr a = a :<=: a | a :<: a | a :==: a

-- | An empty set of constraints.
empty :: Ord a => Constrs a

-- | Adds one constraint to the set, returns the new set of constraints
--   if consistent.
addConstr :: Ord a => Constr a -> Constrs a -> Maybe (Constrs a)\end{verbatim}
}

  \caption{Interface for the module handling the constraints.}
  \label{fig:constraint}
\end{figure}


\subsection{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.

\section{Evaluation}

\section{Future work}

\subsection{Coinduction}

\subsection{Quotient types}

\subsection{Partiality}

\subsection{Pattern matching}

\subsection{Pattern unification}

% TODO coinduction (obscoin, gimenez, jacobs), pattern unification (miller,
% gundry), partiality monad (NAD)

\appendix

\section{Notation and syntax}

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

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

In the languages presented 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. \\
    $\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}

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}

I will often present `definitions' in the described calculi and in
$\mykant$\ itself, like so:
\[
\begin{array}{@{}l}
  \myfun{name} : \mytysyn \\
  \myfun{name} \myappsp \myb{arg_1} \myappsp \myb{arg_2} \myappsp \cdots \mapsto \mytmsyn
\end{array}
\]
To define operators, I use a mixfix notation similar
to Agda, where $\myarg$s denote arguments:
\[
\begin{array}{@{}l}
  \myarg \mathrel{\myfun{$\wedge$}} \myarg : \mybool \myarr \mybool \myarr \mybool \\
  \myb{b_1} \mathrel{\myfun{$\wedge$}} \myb{b_2} \mapsto \cdots
\end{array}
\]

In explicitly typed systems, I will also omit type annotations when they
are obvious, e.g. by not annotating the type of parameters of
abstractions or of dependent pairs.

I will also introduce multiple arguments in one go in arrow types:
\[
  (\myb{x}\, \myb{y} {:} \mytya) \myarr \cdots = (\myb{x} {:} \mytya) \myarr (\myb{y} {:} \mytya) \myarr \cdots
\]
and in abstractions:
\[
\myabs{\myb{x}\myappsp\myb{y}}{\cdots} = \myabs{\myb{x}}{\myabs{\myb{y}}{\cdots}}
\]

\section{Code}

\subsection{ITT renditions}
\label{app:itt-code}

\subsubsection{Agda}
\label{app:agda-itt}

Note that in what follows rules for `base' types are
universe-polymorphic, to reflect the exposition.  Derived definitions,
on the other hand, mostly work with \mytyc{Set}, reflecting the fact
that in the theory presented we don't have universe polymorphism.

\begin{code}
module ITT where
  open import Level

  data Empty : Set where

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

  ¬_ : ∀ {a} → (A : Set a) → Set a
  ¬ A = A → Empty

  record Unit : 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

  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} (x : Bool) {P : Bool → Set a} → P true → P false → P x
  if_then_else_ x {P} = if_/_then_else_ x P

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

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

module Examples-→ where
  open ITT

  data ℕ : Set where
    zero : ℕ
    suc : ℕ → ℕ

  -- These pragmas are needed so we can use number literals.
  {-# BUILTIN NATURAL ℕ #-}
  {-# BUILTIN ZERO zero #-}
  {-# BUILTIN SUC suc #-}

  data List (A : Set) : Set where
    [] : List A
    _∷_ : A → List A → List A

  length : ∀ {A} → List A → ℕ
  length [] = zero
  length (_ ∷ l) = suc (length l)

  _>_ : ℕ → ℕ → Set
  zero > _ = Empty
  suc _ > zero = Unit
  suc x > suc y = x > y

  head : ∀ {A} → (l : List A) → length l > 0 → A
  head [] p = absurd p
  head (x ∷ _) _ = x

module Examples-× where
  open ITT
  open Examples-→

  even : ℕ → Set
  even zero = Unit
  even (suc zero) = Empty
  even (suc (suc n)) = even n

  6-even : even 6
  6-even = tt

  5-not-even : ¬ (even 5)
  5-not-even = absurd
  
  there-is-an-even-number : ℕ × even
  there-is-an-even-number = 6 , 6-even

  _∨_ : (A B : Set) → Set
  A ∨ B = Bool × (λ b → if b then A else B)

  left : ∀ {A B} → A → A ∨ B
  left x = true , x

  right : ∀ {A B} → B → A ∨ B
  right x = false , x

  [_,_] : {A B C : Set} → (A → C) → (B → C) → A ∨ B → C
  [ f , g ] x =
    (if (fst x) / (λ b → if b then _ else _ → _) then f else g) (snd x)

module Examples-W where
  open ITT
  open Examples-×

  Tr : Bool → Set
  Tr b = if b then Unit else Empty

  ℕ : Set
  ℕ = W Bool Tr

  zero : ℕ
  zero = false ◁ absurd

  suc : ℕ → ℕ
  suc n = true ◁ (λ _ → n)

  plus : ℕ → ℕ → ℕ
  plus x y = rec
    (λ _ → ℕ)
    (λ b →
      if b / (λ b → (Tr b → ℕ) → (Tr b → ℕ) → ℕ)
      then (λ _ f → (suc (f tt))) else (λ _ _ → y))
    x

module Equality where
  open ITT
  
  data _≡_ {a} {A : Set a} : A → A → Set a where
    refl : ∀ x → x ≡ x

  ≡-elim : ∀ {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
  ≡-elim P p (refl x) = p

  subst : ∀ {A : Set} (P : A → Set) → ∀ {x y} → (x≡y : x ≡ y) → P x → P y
  subst P x≡y p = ≡-elim (λ _ y _ → P y) p x≡y

  sym : ∀ {A : Set} (x y : A) → x ≡ y → y ≡ x
  sym x y p = subst (λ y′ → y′ ≡ x) p (refl x)

  trans : ∀ {A : Set} (x y z : A) → x ≡ y → y ≡ z → x ≡ z
  trans x y z p q = subst (λ z′ → x ≡ z′) q p

  cong : ∀ {A B : Set} (x y : A) → x ≡ y → (f : A → B) → f x ≡ f y 
  cong x y p f = subst (λ z → f x ≡ f z) p (refl (f x))
\end{code}

\subsubsection{\mykant}

The following things are missing: $\mytyc{W}$-types, since our
positivity check is overly strict, and equality, since we haven't
implemented that yet.

{\small
\verbatiminput{itt.ka}
}

\subsection{\mykant\ examples}

{\small
\verbatiminput{examples.ka}
}

\subsection{\mykant's hierachy}
\label{sec:hurkens}

This rendition of the Hurken's paradox does not type check with the
hierachy enabled, type checks and loops without it.  Adapted from an
Agda version, available at
\url{http://code.haskell.org/Agda/test/succeed/Hurkens.agda}.

{\small
\verbatiminput{hurkens.ka}
}

\bibliographystyle{authordate1}
\bibliography{thesis}

\end{document}