...

[bitonic-mengthesis.git] / thesis.lagda

%% I M P O R T A N T
%% THIS LATEX HURTS YOUR EYES.  DO NOT READ.


% TODO side conditions

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

\usepackage[usenames,dvipsnames]{xcolor}

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

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

\headheight 0pt
\headsep 0pt

\usepackage{amsthm}

% \usepackage{microtype}


%% Bibtex
\usepackage{natbib}

%% Links
\usepackage[pdftex, pdfborderstyle={/S/U/W 0}]{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}
\usetikzlibrary{intersections}
% \usepackage{tikz-cd}
% \usepackage{pgfplots}

\usepackage{titlesec}

% custom section
\titleformat{\section}
{\normalfont\huge\scshape}
{\thesection\hskip 9pt\textpipe\hskip 9pt}
{0pt}
{}

\newcommand{\sectionbreak}{\clearpage}



%% -----------------------------------------------------------------------------
%% 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}[1]{\textup{\AgdaDatatype{#1}}}
\newcommand{\mydc}[1]{\textup{\AgdaInductiveConstructor{#1}}}
\newcommand{\myfld}[1]{\textup{\AgdaField{#1}}}
\newcommand{\myfun}[1]{\textup{\AgdaFunction{#1}}}
\newcommand{\myb}[1]{\AgdaBound{$#1$}}
\newcommand{\myfield}{\AgdaField}
\newcommand{\myind}{\AgdaIndent}
\newcommand{\mykant}{\textmd{\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}

\newcommand{\mydesc}[3]{
  \noindent
  \mbox{
    \parbox{\textwidth}{
      {\mysmall
        \vspace{0.2cm}
        \hfill \textup{\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[#3 / #2]}
\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}{\mytyc{=}}
\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 \Uparrow #3}
\newcommand{\myinf}[2]{\myinff{\myctx}{#1}{#2}}
\newcommand{\mychkk}[3]{#1 \vdash #2 \Downarrow #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}
\newcommand{\mycanquot}{\ensuremath{\textsc{quote}{\Downarrow}}}
\newcommand{\myneuquot}{\ensuremath{\textsc{quote}{\Uparrow}}}
\newcommand{\mymetaguard}{\ |\ }
\newcommand{\mybox}{\Box}
\newcommand{\mytermi}[1]{\text{\texttt{#1}}}
\newcommand{\mysee}[1]{\langle\myse{#1}\rangle}

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

\newtheorem*{mydef}{Definition}
\newtheoremstyle{named}{}{}{\itshape}{}{\bfseries}{}{.5em}{\textsc{#1}}
\theoremstyle{named}

\pgfdeclarelayer{background}
\pgfdeclarelayer{foreground}
\pgfsetlayers{background,main,foreground}

\definecolor{webgreen}{rgb}{0,.5,0}
\definecolor{webbrown}{rgb}{.6,0,0}
\definecolor{webyellow}{rgb}{0.98,0.92,0.73}

\hypersetup{
colorlinks=true, linktocpage=true, pdfstartpage=3, pdfstartview=FitV,
breaklinks=true, pdfpagemode=UseNone, pageanchor=true, pdfpagemode=UseOutlines,
plainpages=false, bookmarksnumbered, bookmarksopen=true, bookmarksopenlevel=1,
hypertexnames=true, pdfhighlight=/O, urlcolor=webbrown, linkcolor=black, citecolor=webgreen}


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

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

\pagenumbering{gobble}

\begin{center}


% Upper part of the page. The '~' is needed because \\
% only works if a paragraph has started.
\includegraphics[width=0.4\textwidth]{brouwer-cropped.png}~\\[1cm]

\textsc{\Large Final year project}\\[0.5cm]

% Title
{ \huge \mykant: Implementing Observational Equality}\\[1.5cm]

{\Large Francesco \textsc{Mazzoli} \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{<fm2209@ic.ac.uk>}}}\\[0.8cm]

  \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{Second marker:} \\
    Dr. Philippa \textsc{Gardner}
  \end{flushright}
\end{minipage}
\vfill

% Bottom of the page
{\large \today}

\end{center}

\clearpage

\mbox{}
\clearpage

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

  Among this systems, Intuitionistic Type Theory (ITT) has been a
  popular framework for theorem provers and programming languages.
  However, reasoning about equality has always been a tricky business in
  ITT and related theories.  In this thesis we shall explain why this is
  the case, and present Observational Type Theory (OTT), a solution to
  some of the problems with equality.

  To bring OTT closer to the current practice of interactive theorem
  provers, we describe \mykant, a system featuring OTT in a setting more
  close to the one found in widely used provers such as Agda and Coq.
  Most notably, we feature used defined inductive and record types and a
  cumulative, implicit type hierarchy.  Having implemented part of
  $\mykant$ as a Haskell program, we describe some of the implementation
  issues faced.
\end{abstract}

\clearpage

\mbox{}
\clearpage

\renewcommand{\abstractname}{Acknowledgements}
\begin{abstract}
  I would like to thank Steffen van Bakel, 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 over the past year.  Andrea suggested
  Observational Type Theory as a topic of study: this thesis would not
  exist without him.  Before them, Tony Field 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
\mbox{}
\clearpage

\tableofcontents

\section{Introduction}

\pagenumbering{arabic}

Functional programming is in good shape.  In particular the `well-typed'
line of work originating from Milner's ML has been extremely fruitful,
in various directions.  Nowadays functional, well-typed programming
languages like Haskell or OCaml are slowly being absorbed by the
mainstream.  An important related development---and in fact the original
motivator for ML's existence---is the advancement of the practice of
\emph{interactive theorem provers}.


An interactive theorem prover, or proof assistant, is a tool that lets
the user develop formal proofs with the confidence of the machine
checking them for correctness.  While the effort towards a full
formalisation of mathematics has been ongoing for more than a century,
theorem provers have been the first class of software whose
implementation depends directly on these theories.

In a fortunate turn of events, it was discovered that well-typed
functional programming and proving theorems in an \emph{intuitionistic}
logic are the same activity.  Under this discipline, the types in our
programming language can be interpreted as proposition in our logic; and
the programs implementing the specification given by the types as their
proofs.  This fact stimulated an active transfer of techniques and
knowledge between logic and programming language theory, in both
directions.

Mathematics could provide programming with a wealth of abstractions and
constructs developed over centuries.  Moreover, identifying our types
with a logic lets us focus on foundational questions regarding
programming with a much more solid approach, given the years of rigorous
study of logic.  Programmers, on the other hand, had already developed a
number of approaches to effectively collaborate with computers, through
the study of programming languages.

In this space, we shall follow the discipline of Intuitionistic Type
Theory, or Martin-L\"{o}f Type Theory, after its inventor.  First
formulated in the 70s and then adjusted through a series of revisions,
it has endured as the core of many practical systems widely in use
today, and it is the most prominent instance of the proposition-as-types
and proofs-as-programs paradigm.  One of the most debated subjects in
this field has been regarding what notion of \emph{equality} should be
exposed to the user.

The tension when studying equality in type theory springs from the fact
that there is a divide between what the user can prove equal
\emph{inside} the theory---what is \emph{propositionally} equal---and
what the theorem prover identifies as equal in its meta-theory---what is
\emph{definitionally} equal.  If we want our system to be well behaved
(mostly if we want type checking to be decidable) we must keep the two
notions separate, with definitional equality inducing propositional
equality, but not the reverse.  However in this scenario propositional
equality is weaker than we would like: we can only prove terms equal
based on their syntactical structure, and not based on their observable
behaviour.

This thesis is concerned with exploring a new approach in this area,
\emph{observational} equality.  Promising to provide a more adequate
propositional equality while retaining well-behavedness, it still is a
relatively unexplored notion.  We set ourselves to change that by
studying it in a setting more akin to the one found in currently
available theorem provers.

\subsection{Structure}

Section \ref{sec:types} will give a brief overview of the
$\lambda$-calculus, both typed and untyped.  This will give us the
chance to introduce most of the concepts mentioned above rigorously, and
gain some intuition about them.  An excellent introduction to types in
general can be found in \cite{Pierce2002}, although not from the
perspective of theorem proving.

Section \ref{sec:itt} will describe a set of basic construct that form a
`baseline' Intuitionistic Type Theory.  The goal is to familiarise with
the main concept of ITT before attacking the problem of equality.  Given
the wealth of material covered the exposition is quite dense.  Good
introductions can be found in \cite{Thompson1991}, \cite{Nordstrom1990},
and \cite{Martin-Lof1984} himself.

Section \ref{sec:equality} will introduce propositional equality.  The
properties of propositional equality will be discussed along with its
limitations.  After reviewing some extensions to propositional equality,
we will explain why identifying definitional equality with propositional
equality causes problems.

Section \ref{sec:ott} will introduce observational equality, following
closely the original exposition by \cite{Altenkirch2007}.  The
presentation is free-standing but glosses over the meta-theoretic
properties of OTT, focusing on the mechanisms that make it work.

Section \ref{sec:kant-theory} is the central part of the thesis and will
describe \mykant, a system we have developed incorporating OTT along
constructs usually present in modern theorem provers.  Along the way, we
discuss these additional features and their trade-offs.  Section
\ref{sec:kant-practice} will describe an implementation implementing
part of \mykant.  A high level design of the software is given, along
with a few specific implementation issues.

Finally, Section \ref{sec:evaluation} will asses the decisions made in
designing and implementing \mykant and the results achieved; and Section
\ref{sec:future-work} will give a roadmap to bring \mykant\ on par and
beyond the competition.

\subsection{Contributions}
\label{sec:contributions}

The contribution of this thesis is threefold:

\begin{itemize}
\item Provide a description of observational equality `in context', to
  make the subject more accessible.  Considering the possibilities that
  OTT brings to the table, we think that introducing it to a wider
  audience can only be beneficial.

\item Fill in the gaps needed to make OTT work with user-defined
  inductive types and a type hierarchy.  We show how one notion of
  equality is enough, instead of separate notions of value- and
  type-equality as presented in the original paper.  We are able to keep
  the type equalities `small' while preserving subject reduction by
  exploiting the fact that we work within a cumulative theory.
  Incidentally, we also describe a generalised version of bidirectional
  type checking for user defined types.

\item Provide an implementation to probe the possibilities of OTT in a
  more realistic setting.  We have implemented an ITT with user defined
  types but due to the limited time constraints we were not able to
  complete the implementation of observational equality.  Nonetheless,
  we describe some interesting implementation issues faced by the type
  theory implementor.
\end{itemize}

The system developed as part of this thesis, \mykant, incorporates OTT
with features that are familiar to users of existing theorem provers
adopting the proofs-as-programs mantra.  The defining features of
\mykant\ are:

\begin{description}
\item[Full dependent types] In ITT, types are very `first class' notion
  and can be the result of computation---they can \emph{depend} on
  values, thus the name \emph{dependent types}.  \mykant\ espouses this
  notion to its full consequences.

\item[User defined data types and records] Instead of forcing the user
  to choose from a restricted toolbox, we let her define types for
  greater flexibility.  We have two kinds of user defined types:
  inductive data types, formed by various data constructors whose type
  signatures can contain recursive occurrences of the type being
  defined; and records, where we have just one data constructor and a
  projection to extract each each field in said constructor.

\item[Consistency] Our system is meant to be consistent with respects to
  the logic it embodies.  For this reason, we restrict recursion to
  \emph{structural} recursion on the defined inductive types, through
  the use of operators (destructors) computing on each type.  Following
  the types-as-proofs interpretation, each destructor expresses an
  induction principle on the data type it operates on.  To achieve the
  consistency of these operations we make sure that our recursive data
  types are \emph{strictly positive}.

\item[Bidirectional type checking] We take advantage of a
  \emph{bidirectional} type inference system in the style of
  \cite{Pierce2000}.  This cuts down the type annotations by a
  considerable amount in an elegant way and at a very low cost.
  Bidirectional type checking is usually employed in core calculi, in
  \mykant\ we extend the concept to user defined data types.

\item[Type hierarchy] In set theory we have to take treat powerset-like
  objects with care, if we want to avoid paradoxes.  However, the
  working mathematician is rarely concerned by this, and the consistency
  in this regard is implicitly assumed.  In the tradition of
  \cite{Russell1927}, in \mykant\ we employ a \emph{type hierarchy} to
  make sure that these size issues are taken care of; and we employ
  system so that the user will be free from thinking about the
  hierarchy, just like the mathematician is.

\item[Observational equality] The motivator of this thesis, \mykant\
  incorporates a notion of observational equality, modifying the
  original presentation by \cite{Altenkirch2007} to fit our more
  expressive system.  As mentioned, we reconcile OTT with user defined
  types and a type hierarchy. 

\item[Type holes] When building up programs interactively, it is useful
  to leave parts unfinished while exploring the current context.  This
  is what type holes are for.
\end{description}

\subsection{Notation and syntax}

Appendix \ref{app:notation} describes the notation and syntax used in
this thesis.

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

\epigraph{\emph{Well typed programs can't go wrong.}}{Robin Milner}

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

Along with Turing's machines, the earliest attempts to formalise
computation lead to the definition of 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}.

\begin{mydef}[$\lambda$-terms]
  Syntax of the $\lambda$-calculus: variables, abstractions, and
  applications.
\end{mydef}
\mynegder
\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, with application being
left associative.

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

\begin{mydef}[$\beta$-reduction]
$\beta$-reduction and substitution for the $\lambda$-calculus.
\end{mydef}
\mynegder
\mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
  $
  \begin{array}{l}
    \myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{\myb{x}}{\mytmn}\text{ \textbf{where}} \\
    \myind{2}
    \begin{array}{l@{\ }c@{\ }l}
      \mysub{\myb{x}}{\myb{x}}{\mytmn} & = & \mytmn \\
      \mysub{\myb{y}}{\myb{x}}{\mytmn} & = & y\text{ \textbf{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{\textbf{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 to avoid
name capturing.  We will use substitution in the future for other
name-binding constructs assuming similar precautions.

These few elements have a remarkable expressiveness, and are 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}}$}
\]
\begin{mydef}[redex]
  A \emph{redex} is a term that can be reduced.
\end{mydef}
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 a term reducible if it appears to the left of a reduction rule.
\begin{mydef}[normal form]
  A term that contains no redexes is said to be in \emph{normal form}.
\end{mydef}
\begin{mydef}[normalising terms and systems]
  Terms that reduce in a finite number of reduction steps to a normal
  form are \emph{normalising}.  A system in which all terms are
  normalising is said to have the \emph{normalisation property}, or
  to be \emph{normalising}.
\end{mydef}
Given the reduction behaviour of $(\myapp{\omega}{\omega})$, it is clear
that the untyped $\lambda$-calculus does not have the normalisation
property.

We have not presented reduction in an algorithmic way, 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 all abstractions are said to be in
\emph{weak head normal form} even if their body is not.

\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} (STLC).
\begin{mydef}[Simply typed $\lambda$-calculus]
  The syntax and typing rules for the STLC are given in Figure \ref{fig:stlc}.
\end{mydef}

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: $\myemptyctx$ is the empty context, and $\myctx;
\myb{x} : \mytya$ adds a variable to the context.  $\myctx(x)$ extracts
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{mydef}[Progress]
  A well-typed term is not stuck---it is either a variable, or it does
  not appear on the left of the $\myred$ relation , or it can take a
  step according to the evaluation rules.
\end{mydef}
\begin{mydef}[Subject reduction]
  If a well-typed term takes a step of evaluation, then the
  resulting term is also well-typed, and preserves the previous type.
\end{mydef}

However, STLC buys us much more: every well-typed term is normalising
\citep{Tait1967}.  It is easy to see that we cannot 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:
\begin{mydef}[Fixed-point combinator]\end{mydef}
\mynegder
\noindent
\begin{minipage}{0.5\textwidth}
\mydesc{syntax}{ } {
  $ \mytmsyn ::= \cdots b \mysynsep \myfix{\myb{x}}{\mytysyn}{\mytmsyn} $
  \vspace{0.5cm}
}
\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} 
\mynegder
\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.

Another important property of the STLC is the Church-Rosser property:
\begin{mydef}[Church-Rosser property]
  A system is said to have the \emph{Church-Rosser} property, or to be
  \emph{confluent}, if given any two reductions $\mytmm$ and $\mytmn$ of
  a given term $\mytmt$, there is exist a term to which both $\mytmm$
  and $\mytmn$ can be reduced.
\end{mydef}
Given that the STLC has the normalisation property and the Church-Rosser
property, each term has a \emph{unique} normal form.

\subsection{The Curry-Howard correspondence}

As hinted in the introduction, it turns out that the STLC can be seen a
natural deduction system for intuitionistic propositional logic.  Terms
correspond to proofs, and their types correspond to 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}})}}}}
\]
Which is known to functional programmers as function composition. Going
beyond arrow types, we can extend our bare lambda calculus with useful
types to represent other logical constructs.
\begin{mydef}[The extended STLC]
  Figure \ref{fig:natded} shows syntax, reduction, and typing rules for
  the \emph{extended simply typed $\lambda$-calculus}.
\end{mydef}

\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 extended 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$ (true), and
dually $\myempty$ corresponds to the logical $\bot$ (false).  $\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.
\begin{mydef}[Negation]
  $\myneg \mytya$ can be expressed as $\mytya \myarr \myempty$.
\end{mydef}
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 is no coincidence, since there
is no obvious computational behaviour for laws like the excluded middle.
Logics 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.

\begin{mydef}[Finite lists for the STLC]
We 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$).  Full rules in Figure
\ref{fig:list}.
\end{mydef}
\mynegder
\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}

\epigraph{\emph{Martin-L{\"o}f's type theory is a well established and
    convenient arena in which computational Christians are regularly
    fed to logical lions.}}{Conor McBride}

\subsection{Extending the STLC}

\cite{Barendregt1991} succinctly expressed geometrically how we can add
expressivity to the STLC:
$$
\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, where $\mytyp$ denotes the `type of types':
  \[\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 \citep{milner1978theory}.  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 later gave a revised and consistent
definition \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}, Coq \citep{Coq}, Epigram
\citep{McBride2004, EpigramTut}, Isabelle \citep{Paulson1990}, and many
others.

\subsection{A simple type theory}
\label{sec:core-tt}

The calculus I present follows the exposition in \cite{Thompson1991},
and is quite close to the original formulation of
\citep{Martin-Lof1984}.  Agda and \mykant\ renditions of the presented
theory and all the examples is reproduced in Appendix
\ref{app:itt-code}.
\begin{mydef}[Intuitionistic Type Theory (ITT)]
The syntax and reduction rules are shown in Figure \ref{fig:core-tt-syn}.
The typing rules are presented piece by piece in the following sections.
\end{mydef}

\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.
\begin{mydef}[Definitional equality]
  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)
\end{mydef}
For example under this discipline we will find that
\[
\begin{array}{@{}l}
  \myabss{\myb{x}}{\mytya}{\myb{x}} \mydefeq \myabss{\myb{y}}{\mytya}{\myb{y}} \\
  \myapp{(\myabss{\myb{f}}{\mytya \myarr \mytya}{\myb{f}})}{(\myabss{\myb{y}}{\mytya}{\myb{y}})} \mydefeq \myabss{\myb{quux}}{\mytya}{\myb{quux}}
\end{array}
\]
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, comparing
terms by reducing to their normal forms and then comparing them
syntactically; so that a separate conversion rule is not needed.
Another thing to notice is that, considering the need to reduce terms to
decide equality, for type checking to be decidable a dependently typed
must be terminating and confluent; since every type needs to have a
unique normal form for definitional equality 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 for $\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 type checked with
the updated knowledge of the value of $\myb{x}$.

\subsubsection{$\myarr$, or dependent function}
\label{sec:depprod}

 \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 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.  In the
introduction rule, the return type is type checked in a context with an
abstracted variable of domain's 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 can write functions of types
\[
\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-emptiness' 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.

\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 correspondence 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 way.  We can form `nodes'
of the shape \[\mytmt \mynode{\myb{x}}{\mytyb} \myse{f} :
\myw{\myb{x}}{\mytya}{\mytyb}\] where $\mytmt$ is of type $\mytya$ and
is the data present in the node, and $\myse{f}$ specifies a `child' of
the node 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 and 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}\, \myfun{then}\, \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{x}}{\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$.  This gives a taste of the
  clumsiness of $\mytyc{W}$-types but not the whole story: well-orders
  are inadequate not only because they are verbose, but also because the
  face deeper problems due to the weakness of the notion of equality
  present in most type theory (which we will present in the next
  section) \citep{dybjer1997representing}.  The `better' equality we
  will present in Section \ref{sec:ott} helps but does not fully resolve
  these issues.\footnote{See \url{http://www.e-pig.org/epilogue/?p=324},
    which concludes with `W-types are a powerful conceptual tool, but
    they’re no basis for an implementation of recursive data types in
    decidable type theories.'}  For this reasons \mytyc{W}-types have
  remained nothing more than a reasoning tool, and practical systems
  implement more expressive ways to represent data.

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

\epigraph{\emph{Half of my time spent doing research involves thinking up clever
  schemes to avoid needing functional extensionality.}}{@larrytheliquid}

In the previous section we learnt how a type checker for ITT 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}

\begin{mydef}[Propositional equality] The syntax, reduction, and typing
  rules for propositional equality and related constructs are defined
  as:
\end{mydef}
\mynegder
\noindent
\begin{minipage}{0.5\textwidth}
\mydesc{syntax}{ }{
  $
  \begin{array}{r@{\ }c@{\ }l}
    \mytmsyn & ::= & \cdots \\
             &  |  & \mypeq \myappsp \mytmsyn \myappsp \mytmsyn \myappsp \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{\mypeq \myappsp \mytya \myappsp  \mytmm \myappsp \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}}{\mypeq \myappsp \mytya \myappsp \mytmm \myappsp \mytmn}$}
      \DisplayProof
      &
      \AxiomC{$
        \begin{array}{c}
          \myjud{\myse{P}}{\myfora{\myb{x}\ \myb{y}}{\mytya}{\myfora{q}{\mypeq \myappsp \mytya \myappsp \myb{x} \myappsp \myb{y}}{\mytyp_l}}} \\
          \myjud{\myse{q}}{\mypeq \myappsp \mytya \myappsp \mytmm \myappsp \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 equality to be a type.  Here we present what has survived
as the dominating form of equality in systems based on ITT up since
\cite{Martin-Lof1984} up to the present day.

Our type former is $\mypeq$, which given a type 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$ (also known as `\myfun{J}
axiom' in the literature), $\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$ returns 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.  Invocations 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.  This means that $\myjeqq$ will not compute with
hypothetical proofs, which makes sense given that they might be false.

While the $\myjeqq$ rule is slightly convoluted, we 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}}{\mypeq \myappsp \myb{A} \myappsp \myb{x} \myappsp \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 depending on their types, a process 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}.

\begin{mydef}[Congruence and $\eta$-laws]
  To justify quotation in our type system we add a congruence law for
  abstractions and a similar law for products, plus the fact that all
  elements of $\myunit$ or $\myempty$ are equal.
\end{mydef}
\mynegder
\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.

\begin{mydef}[$\myfun{K}$ axiom]\end{mydef}
\mydesc{typing:}{\myjud{\mytmm \mydefeq \mytmn}{\mytmsyn}}{
  \AxiomC{$
    \begin{array}{@{}c}
      \myjud{\myse{P}}{\myfora{\myb{x}}{\mytya}{\mypeq \myappsp \mytya \myappsp \myb{x}\myappsp \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
$\myjeqq$, 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 \emph{Univalent Foundations}, which feature 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}

Propositional equality as described is quite restricted when
reasoning about equality beyond the term structure, which is what definitional
equality gives us (extensions 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 equal.  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}}{\mypeq \myappsp \myb{B} \myappsp (\myapp{\myb{f}}{\myb{x}}) \myappsp (\myapp{\myb{g}}{\myb{x}})}) \myarr
        \mypeq \myappsp (\myb{A} \myarr \myb{B}) \myappsp \myb{f} \myappsp \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}{\mypeq \myappsp \mynat \myappsp (0 \mathrel{\myfun{$+$}} \myb{x}) \myappsp (\myb{x} \mathrel{\myfun{$+$}} 0)}
\]
By induction on $\mynat$ applied to $\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 given above, theories that offer a propositional equality
similar to what we presented are called \emph{intensional}, as opposed
to \emph{extensional}.  Most systems widely used today (such as Agda,
Coq, and Epigram) are of this kind.

This is quite an annoyance that often makes reasoning awkward or
impossible to execute.  For example, we might want to represent terms of
some language in Agda and give their denotation by embedding them in
Agda---if we had $\lambda$-terms, functions will become Agda functions,
application will be Agda's function application, and so on.  Then we
would like to perform optimisation passes on the terms, and verify that
they are sound by proving that the denotation of the optimised version
is equal to the denotation of the starting term.

But if the embedding uses functions---and it probably will---we are
stuck with an equality that identifies as equal only syntactically equal
functions!  Since the point of optimising is about preserving the
denotational but changing the operational behaviour of terms, our
equality falls short of our needs.  Moreover, the problem extends to
other fields beyond functions, such as bisimulation between processes
specified by coinduction, or in general proving equivalences based on
the behaviour of a term.

\subsection{Equality reflection}

One way to `solve' this problem is by identifying propositional equality
with definitional equality.

\begin{mydef}[Equality reflection]\end{mydef}
\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
    \AxiomC{$\myjud{\myse{q}}{\mypeq \myappsp \mytya \myappsp \mytmm \myappsp \mytmn}$}
    \UnaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\mytya}$}
    \DisplayProof
}

The \emph{equality reflection} rule 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 not 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{$\myjudd{\myctx; \myb{x} : \myb{A}}{\myb{q}}{\mypeq \myappsp \myb{A} \myappsp (\myapp{\myb{f}}{\myb{x}}) \myappsp (\myapp{\myb{g}}{\myb{x}})}$}
  \RightLabel{equality reflection}
  \UnaryInfC{$\myjudd{\myctx; \myb{x} : \myb{A}}{\myapp{\myb{f}}{\myb{x}} \mydefeq \myapp{\myb{g}}{\myb{x}}}{\myb{B}}$}
  \RightLabel{congruence for $\lambda$s}
  \UnaryInfC{$\myjud{(\myabs{\myb{x}}{\myapp{\myb{f}}{\myb{x}}}) \mydefeq (\myabs{\myb{x}}{\myapp{\myb{g}}{\myb{x}}})}{\myb{A} \myarr \myb{B}}$}
  \RightLabel{$\eta$-law for $\lambda$}
  \UnaryInfC{$\myjud{\myb{f} \mydefeq \myb{g}}{\myb{A} \myarr \myb{B}}$}
  \RightLabel{$\myrefl$}
  \UnaryInfC{$\myjud{\myapp{\myrefl}{\myb{f}}}{\mypeq \myappsp (\myb{A} \myarr \myb{B}) \myappsp \myb{f} \myappsp \myb{g}}$}
\end{prooftree}

For this reason, theories employing equality reflection are often
grouped under the name of \emph{Extensional Type Theory} (ETT).  Now,
the question is: do we need to give up well-behavedness of our theory to
gain extensionality?

\section{The observational approach}
\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 $\mytyb$ 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}

\begin{mydef}[OTT's simple theory, with propositions]\ \end{mydef}
\mynegder
\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}
    $
}

\mynegder

\mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
  $
  \begin{array}{l@{}l@{\ }c@{\ }l}
    \myITE{\mytrue  &}{\mytya}{\mytyb} & \myred & \mytya \\
    \myITE{\myfalse &}{\mytya}{\mytyb} & \myred & \mytyb
  \end{array}
  $
}

\mynegder

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

\mynegder

\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}$.
\begin{mydef}[Proposition decoding]\ \end{mydef}
\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
  when isolating \mytyc{Prop} 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, since it has one element.
  A pair of propositions $\myse{P} \myand \myse{Q}$ still won't get us
  data, since if they both have one element the only possible pair is
  the one formed by said elements. Finally, if $\myse{P}$ is a
  proposition and we have $\myprfora{\myb{x}}{\mytya}{\myse{P}}$, the
  decoding will be a constant function for propositional content.  The
  only threat is $\mybot$, by which we can fabricate anything we want:
  however if we are consistent there will be no closed term of type
  $\mybot$ at, which is what we care about regarding proof erasure and
  term equality.

  As an example of types that are \emph{not} propositional, consider
  $\mydc{Bool}$eans, which are the quintessential `relevant' data, since
  they are often use to decide the execution path of a program through
  $\myfun{if}\myarg\myfun{then}\myarg\myfun{else}\myarg$ constructs.

\subsection{Equality proofs}

\begin{mydef}[Equality proofs and related operations]\ \end{mydef}
\mynegder
\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 that things judged to be equal are
still always replaceable 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.

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} terms and types.

\begin{mydef}[Canonical and neutral types and terms]
  In a type theory, \emph{neutral} terms are those formed by an
  abstracted variable or by an eliminator (including function
  application).  Everything else is \emph{canonical}.

  In the current system, data constructors ($\mytt$, $\mytrue$,
  $\myfalse$, $\myabss{\myb{x}}{\mytya}{\mytmt}$, ...) will be
  canonical, the rest neutral.  Correspondingly, 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$.
\end{mydef}
\begin{mydef}[Canonicity]
  If in a system all canonical types are inhabited by canonical terms
  the system is said to have the \emph{canonicity} property.
\end{mydef}
The current system, and well-behaved systems in general, has the
canonicity property.  Another consequence of normalisation is that all
closed terms will reduce to a canonical term.

\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 the canonicity of equated
types, 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 will not reduce and thus $\myfun{coe}$ will not
reduce either.  If we come across 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 \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 \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}

\begin{mydef}[Type equalities reduction, and \myfun{coe}rcions] Figure
  \ref{fig:eqred} illustrates the rules to reduce equalities and to
  coerce terms.  We use a $\mysyn{let}$ syntax for legibility.
\end{mydef}
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 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[\myb{x_1}] \myeq \mytyb_2[\myb{x_2}]}$).\footnote{We
  are using $\myimpl$ to indicate a $\forall$ where we discard the
  quantified 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 we need to equate terms of possibly different types.  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}
\label{sec:lazy}

It is important to notice that in the reduction rules for $\myfun{coe}$
are never obstructed by the structure of 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 top-level abstracted variables.

\subsubsection{Value-level equality}

\begin{mydef}[Value-level equality]\ \end{mydef}
\mynegder
\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.
When matching on records and functions, we rebuild the records and
expand the function to achieve $\eta$-expansion.

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

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

\epigraph{\emph{The construction itself is an art, its application to the world an evil parasite.}}{Luitzen Egbertus Jan `Bertus' Brouwer}

\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, along with motivations
and trade-offs for the design decisions made. Then we describe the
implementation we have developed in Section \ref{sec:kant-practice}.
For an overview of the features of \mykant, see
Section \ref{sec:contributions}, here we present them one by one.  The
exception is type holes, which we do not describe holes rigorously, but
provide more information about them in Section \ref{sec:type-holes}.

\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 is in correspondence with the notion of
canonical and neutral 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 dealing with top-level
canonical terms.  The types are the same as those found in the normal
STLC.

\begin{mydef}[Syntax for the annotated $\lambda$-calculus]\ \end{mydef}
\mynegder
\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 arrows signify the direction of the type
checking---inference pushes types up, checking propagates types
down.

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.

\begin{mydef}[Bidirectional type checking for the STLC]\ \end{mydef}
\mynegder
\mydesc{typing:}{\myctx \vdash \mytmsyn \Updownarrow \mytmsyn}{
  \begin{tabular}{cc}
    \AxiomC{$\myctx(x) = A$}
    \UnaryInfC{$\myinf{\myb{x}}{A}$}
    \DisplayProof
    &
    \AxiomC{$\myjudd{\myctx;\myb{x} : A}{\mytmt}{\mytyb}$}
    \UnaryInfC{$\mychk{\myabs{x}{\mytmt}}{(\myb{x} {:} \mytya) \myarr \mytyb}$}
    \DisplayProof
  \end{tabular}

  \myderivspp

  \begin{tabular}{ccc}
    \AxiomC{$\myinf{\mytmm}{\mytya \myarr \mytyb}$}
    \AxiomC{$\mychk{\mytmn}{\mytya}$}
    \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mytyb}$}
    \DisplayProof
    &
    \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:
\[
\begin{array}{@{}l}
  \myfun{comp} :  (\mynat \myarr \mynat) \myarr (\mynat \myarr \mynat) \myarr \mynat \myarr \mynat \\
  \myfun{comp} \mapsto (\myabs{\myb{f}\, \myb{g}\, \myb{x}}{\myb{f}\myappsp(\myb{g}\myappsp\myb{x})})
\end{array}
\]
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 : \mynat
\]

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

\begin{mydef}[Syntax for base types in \mykant]\ \end{mydef}
\mynegder
\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 user-defined.
Since we let the user define values too, we will need a context capable
of carrying the body of variables along with their type.

\begin{mydef}[Context validity]
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.
\end{mydef}
\mynegder
\mydesc{context validity:}{\myvalid{\myctx}}{
    \begin{tabular}{ccc}
      \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
      \UnaryInfC{$\myvalid{\myemptyctx}$}
      \DisplayProof
      &
      \AxiomC{$\mychk{\mytya}{\mytyp}$}
      \AxiomC{$\mynamesyn \not\in \myctx$}
      \BinaryInfC{$\myvalid{\myctx ; \mynamesyn : \mytya}$}
      \DisplayProof
      &
      \AxiomC{$\mychk{\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.

\begin{mydef}[Reduction rules for base types in \mykant]\ \end{mydef}
\mynegder
\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}.

\begin{mydef}[Bidirectional type checking for base types in \mykant]\ \end{mydef}
\mynegder
\mydesc{typing:}{\myctx \vdash \mytmsyn \Updownarrow \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}{cc}

      \AxiomC{\phantom{$\mychkk{\myctx; \myb{x}: \mytya}{\mytmt}{\mytyb}$}}
      \UnaryInfC{$\myinf{\mytyp}{\mytyp}$}
      \DisplayProof
      &
    \AxiomC{$\mychk{\mytya}{\mytyp}$}
    \AxiomC{$\mychkk{\myctx; \myb{x} : \mytya}{\mytyb}{\mytyp}$}
    \BinaryInfC{$\myinf{(\myb{x} {:} \mytya) \myarr \mytyb}{\mytyp}$}
    \DisplayProof

    \end{tabular}


    \myderivspp

    \begin{tabular}{cc}
      \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's and McKinna's early work on Epigram \citep{McBride2004},
although with some differences.

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

\begin{mydef}[Term vector]
  A \emph{term vector} is a series of terms.  The empty vector is
  represented by $\myemptyctx$, and a new element is added with a
  semicolon, similarly to contexts---$\vec{t};\mytmm$.
\end{mydef}

We use term vectors 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.

\begin{mydef}[Telescope]
  A \emph{telescope} is a series of typed bindings.  The empty telescope
  is represented by $\myemptyctx$, and a binding is added via
  $\myarg;\myarg$.
\end{mydef}

To present the elaboration and operations on user defined data types, we
frequently make use what \cite{Bruijn91} called \emph{telescopes}, a
construct that will prove useful when dealing with the types of type and
data constructors.  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$.  For example 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}

\begin{mydef}[Syntax of declarations in \mykant]\ \end{mydef}
\mynegder
\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 \emph{data type}, with a \emph{type constructor}
  and various \emph{data constructors}, quite similar to what we find in
  Haskell.  A primitive \emph{eliminator} (or \emph{destructor}, or
  \emph{recursor}) will be used to compute with each data type.
\item[Record] A \emph{record}, which like data types consists of a type
  constructor but only one data constructor.  The user can also define
  various \emph{fields}, with no recursive occurrences of the type.  The
  functions extracting the fields' values from an instance of a record
  are called \emph{projections}.
\end{description}

Elaborating defined variables consists of type checking the 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.

\begin{mydef}[Elaboration of defined and abstract variables]\ \end{mydef}
\mynegder
\mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
    \begin{tabular}{cc}
      \AxiomC{$\mychk{\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{$\mychk{\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, we will
explain what we can define, 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 give 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 look up the type constructor corresponding
  to each data constructor.  When using data constructors in examples I
  will omit the type constructor prefix for brevity, in this case
  writing $\mydc{zero}$ instead of $\mynat.\mydc{suc}$ and $\mydc{suc}$ instead of
  $\mynat.\mydc{suc}$.

  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 $\mynat.\myfun{elim}$
  returns the base case if the provided number is $\mydc{zero}$, and
  recursively applies 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,
since we cannot express the notion of a predicate depending on
$\mynat$---the type system is far too weak.

\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 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
  what we do to type abstractions:
  \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.
  We have a base case for $\myb{P} \myappsp \mydc{leaf}$, and an
  inductive step that given two subtrees and the predicate applied to
  them needs to return the predicate applied to the tree formed by a
  node with the two subtrees as children.

\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':
  \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}
  which lets us write the $\myfun{absurd}$ that we know and love:
  \[
  \begin{array}{l@{}}
    \myfun{absurd} : (\myb{A} {:} \mytyp) \myarr \myempty \myarr \myb{A} \\
    \myfun{absurd}\myappsp \myb{A} \myappsp \myb{x} \mapsto \myempty.\myfun{elim} \myappsp \myb{x} \myappsp (\myabs{\myarg}{\myb{A}})
  \end{array}
  \]

\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, but 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 ($\le$ everything but itself) and top
  ($\ge$ everything but itself) 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{l_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{l_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}
  \]
  Note that in the $\mydc{cons}$ constructor we quantify over the first
  argument, which will determine the type of the following
  arguments---again something we cannot do in systems like Haskell.  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
  data type 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---in
  this case we have the type of $\myfun{snd}$ depending on the value of
  $\myfun{fst}$.  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{$\hspace{0.2cm}\myinf{\mytmt}{\mytyc{Prod} \myappsp \mytya \myappsp \mytyb}\hspace{0.2cm}$}
      \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 defined here 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}

\begin{mydef}[Elaboration for user defined types]
  Following the intuition given by the examples, the full elaboration
  machinery is presented Figure \ref{fig:elab}.
\end{mydef}
Our elaboration is essentially a modification of Figure 9 of
\cite{McBride2004}. However, our data types are not inductive
families,\footnote{See Section \ref{sec:future-work} for a brief
  description of inductive families.} we do bidirectional type checking
by treating constructors/destructors as syntax, and we have records.

\begin{mydef}[Strict positivity]
  A inductive type declaration is \emph{strictly positive} if recursive
  occurrences of the type we are defining do not appear embedded
  anywhere in the domain part of any function in the types for the data
  constructors.
\end{mydef}
In data type declarations we allow recursive occurrences as long as they
are strictly positive, which ensures the consistency of the theory.  To
achieve that we employing a syntactic check to make sure that this is
the case---in fact the check is stricter than necessary for simplicity,
given that we allow recursive occurrences only at the top level of data
constructor arguments.  For example a definition of the $\mytyc{W}$ type
is accepted in Agda but rejected in \mykant.

Note that the 

Without these precautions, we can easily derive any type with no
recursion:
\begin{Verbatim}
data Fix a = Fix (Fix a -> a) -- Negative occurrence of `Fix a'
-- Term inhabiting any type `a'
boom :: a
boom = (\f -> f (Fix f)) (\x -> (\(Fix f) -> f) x x)
\end{Verbatim}
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.

\begin{mydef}[Bidirectional type checking for elaborated types]
To implement bidirectional type checking for constructors and
destructors, we store their types in full in the context, and then
instantiate when due.
\end{mydef}
\mynegder
\mydesc{typing:}{\myctx \vdash \mytmsyn \Updownarrow \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 in developing $\mykant$\ was to decide whether
user defined types should be included, and how to handle them.  As we
saw, while we can devise general structures like $\mytyc{W}$, they are
unsuitable both for for direct usage and `mechanical' usage.  Thus most
theorem provers in the wild provide some means for the user to define
structures tailored to specific uses.

Even if we take user defined types for granted, while there is not much
debate on how to handle records, there are two broad schools of thought
regarding the handling of data types:
\begin{description}
\item[Fixed points and pattern matching] The road chosen by Agda and Coq.
  Functions are written like in Haskell---matching on the input and with
  explicit recursion.  An external check on the recursive arguments
  ensures that they are decreasing, and thus that all functions
  terminate.  This approach is the best in terms of user usability, but
  it is tricky to implement correctly.

\item[Elaboration into eliminators] The road chose by \mykant, and
  pioneered by the Epigram line of work.  The advantage is that we can
  reduce every data type to simple definitions which guarantee
  termination and are simple to reduce and type.  It is however more
  cumbersome to use than pattern matching, although \cite{McBride2004}
  has shown how to implement an expressive pattern matching interface on
  top of a larger set of combinators of those provided by \mykant.

  We can go ever further down this road and elaborate the declarations
  for data types themselves to primitive types, so that our `core'
  language will be very small and manageable
  \citep{dagand2012elaborating, chapman2010gentle}.
\end{description}

We chose the safer and easier to implement path, given the time
constraints and the higher confidence of correctness.  See also Section
\ref{sec:future-work} for a brief overview of ways to extend or treat
user defined types.

\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{app:hurkens}.

However, hierarchy as presented in section \ref{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!]

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

\begin{mydef}[Cumulativity for \mykant' base types]
  Figure \ref{fig:cumulativity} gives a formal definition of
  \emph{cumulativity} for the base types.  Similar measures can be taken
  for user defined types, withe the type living in the least upper bound
  of the levels where the types contained data live.
\end{mydef}

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, clumsiness of having to manually specify the
size of types is still there.  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 under the hood.  $\mykant$\ implements this following the
plan given by \cite{Huet1988}.  See also \cite{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.  We keep a set of
constraints regarding the ordering of each occurrence of $\mytyp$, each
represented by its unique reference.  We 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.  Implementation
details are given 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.

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

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 innovation.  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{mydef}[\mykant' propositional prelude]\ \end{mydef}
\[
\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}
\]

\begin{mydef}[Propositions and decoding]\ \end{mydef}
\mynegder
\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}
  $
}
\mynegder
\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 & \mytyc{Prod} \myappsp \myprdec{\myse{P}} \myappsp \myprdec{\myse{Q}} \\
      \myprdec{&\myprfora{\myb{x}}{\mytya}{\myse{P}} &} & \myred &
      \myfora{\myb{x}}{\mytya}{\myprdec{\myse{P}}}
    \end{array}
    $
  \end{tabular}
}

We will overload the $\myand$ symbol to define `nested' products, and
$\myproj{n}$ to project elements from them, so that
\[
\begin{array}{@{}l}
\mytya \myand \mytyb = \mytya \myand (\mytyb \myand \mytop) \\
\mytya \myand \mytyb \myand \myse{C} = \mytya \myand (\mytyb \myand (\myse{C} \myand \mytop)) \\
\myind{2} \vdots \\
\myproj{1} : \myprdec{\mytya \myand \mytyb} \myarr \myprdec{\mytya} \\
\myproj{2} : \myprdec{\mytya \myand \mytyb \myand \myse{C}} \myarr \myprdec{\mytyb} \\
\myind{2} \vdots
\end{array}
\]
And so on, so that $\myproj{n}$ will work with all products with at
least than $n$ elements.  Logically a 0-ary $\myand$ will correspond to
$\mytop$.

\subsubsection{Some OTT examples}

Before presenting the direction that $\mykant$\ takes, let us consider
two 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 us 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:depprod}.  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}
  \]
  First 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$ are
  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'.  Indeed,
  heterogeneous equalities involving abstractions over types will
  provide 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, but with an
  heterogeneous equalities relating types instead of values:
  \[
  \begin{array}{@{}l}
    \mytya_1 \myeq \mytya_2 \myand \myjm{\mytyb_1}{\mytya_1 \myarr \mytyp}{\mytyb_2}{\mytya_2 \myarr \mytyp} \myred \\
    \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
        \myjm{\myapp{\mytyb_1}{\myb{x_1}}}{\mytyp}{\myapp{\mytyb_2}{\myb{x_2}}}{\mytyp}
      }}
  \end{array}
  \]
  If we pretend for the moment that those heterogeneous equalities were
  type equalities, things run smoothly. 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}
  \]
\end{description}

\subsubsection{Only one equality}

Given the examples above, a more `flexible' heterogeneous equality must
emerge, since of the fact that in $\mykant$ we re-gain the possibility
of abstracting and in general handling types 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.

\begin{mydef}[Propositions, coercions, coherence, equalities and
  equality reduction for \mykant] See Figure \ref{fig:kant-eq-red}.
\end{mydef}

\begin{mydef}[Type equality in \mykant]
  We define $\mytya \myeq \mytyb$ as an abbreviation for
  $\myjm{\mytya}{\mytyp}{\mytyb}{\mytyp}$.
\end{mydef}

In fact, we can drop a separate notion of type-equality, which will
simply be served by $\myjm{\mytya}{\mytyp}{\mytyb}{\mytyp}$.  We shall
still distinguish equalities relating types for hierarchical
purposes. 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}
    \mytmsyn & ::= & \cdots \mysynsep \mycoee{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \mysynsep
                     \mycohh{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
    \myprsyn & ::= & \cdots \mysynsep \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
  \end{array}
  $
}

\mynegder

\mydesc{typing:}{\myctx \vdash \mytmsyn \Leftrightarrow \mytmsyn}{
  \small
  \begin{tabular}{cc}
    \AxiomC{$\mychk{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
    \AxiomC{$\mychk{\mytmt}{\mytya}$}
    \BinaryInfC{$\myinf{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}$}
    \DisplayProof
    &
    \AxiomC{$\mychk{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
    \AxiomC{$\mychk{\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

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

For coercions the algorithm is messier and not reproduced here for lack
of a decent notation---the details are hairy but uninteresting.  To give
an idea of the possible complications, let us conceive a type that
showcases trouble not arising in the previous examples.
\[
\begin{array}{@{}l}
\myadt{\mytyc{Max}}{\myappsp (\myb{A} {:} \mynat \myarr \mytyp) \myappsp (\myb{B} {:} (\myb{x} {:} \mynat) \myarr \myb{A} \myappsp \myb{x} \myarr \mytyp) \myappsp (\myb{k} {:} \mynat)}{ \\ \myind{2}}{
  \mydc{max} \myappsp (\myb{A} \myappsp \myb{k}) \myappsp (\myb{x} {:} \mynat) \myappsp (\myb{a} {:} \myb{A} \myappsp \myb{x}) \myappsp (\myb{B} \myappsp \myb{x} \myappsp \myb{a})
}
\end{array}
\]
For type equalities we will have
\[
\begin{array}{@{}l@{\ }l}
  \myjm{\mytyc{Max} \myappsp \mytya_1 \myappsp \mytyb_1 \myappsp \myse{k}_1}{\mytyp}{\mytyc{Max} \myappsp \mytya_2 \myappsp \myappsp \mytyb_2 \myappsp \myse{k}_2}{\mytyp} & \myred \\[0.2cm]
  \begin{array}{@{}l}
    \myjm{\mytya_1}{\mynat \myarr \mytyp}{\mytya_2}{\mynat \myarr \mytyp} \myand \\
    \myjm{\mytyb_1}{(\myb{x} {:} \mynat) \myarr \mytya_1 \myappsp \myb{x} \myarr \mytyp}{\mytyb_2}{(\myb{x} {:} \mynat) \myarr \mytya_2 \myappsp \myb{x} \myarr \mytyp} \\
    \myjm{\myse{k}_1}{\mynat}{\myse{k}_2}{\mynat}
  \end{array} & \myred \\[0.7cm]
  \begin{array}{@{}l}
    (\mynat \myeq \mynat \myand  (\myprfora{\myb{x_1}\, \myb{x_2}}{\mynat}{\myjm{\myb{x_1}}{\mynat}{\myb{x_2}}{\mynat} \myimpl \myapp{\mytya_1}{\myb{x_1}} \myeq \myapp{\mytya_2}{\myb{x_2}}})) \myand \\
    (\mynat \myeq \mynat \myand \left(
    \begin{array}{@{}l}
      \myprfora{\myb{x_1}\, \myb{x_2}}{\mynat}{\myjm{\myb{x_1}}{\mynat}{\myb{x_2}}{\mynat} \myimpl  \\ \myjm{\mytyb_1 \myappsp \myb{x_1}}{\mytya_1 \myappsp \myb{x_1} \myarr \mytyp}{\mytyb_2 \myappsp \myb{x_2}}{\mytya_2 \myappsp \myb{x_2} \myarr \mytyp}}
    \end{array}
    \right)) \myand \\
    \myjm{\myse{k}_1}{\mynat}{\myse{k}_2}{\mynat}
  \end{array} & \myred \\[0.9cm]
  \begin{array}{@{}l}
    (\mytop \myand  (\myprfora{\myb{x_1}\, \myb{x_2}}{\mynat}{\myjm{\myb{x_1}}{\mynat}{\myb{x_2}}{\mynat} \myimpl \myapp{\mytya_1}{\myb{x_1}} \myeq \myapp{\mytya_2}{\myb{x_2}}})) \myand \\
    (\mytop \myand \left(
    \begin{array}{@{}l}
      \myprfora{\myb{x_1}\, \myb{x_2}}{\mynat}{\myjm{\myb{x_1}}{\mynat}{\myb{x_2}}{\mynat} \myimpl  \\
        \myprfora{\myb{y_1}}{\mytya_1 \myappsp \myb{x_1}}{\myprfora{\myb{y_2}}{\mytya_2 \myappsp \myb{x_2}}{\myjm{\myb{y_1}}{\mytya_1 \myappsp \myb{x_1}}{\myb{y_2}}{\mytya_2 \myappsp \myb{x_2}} \myimpl  \\
            \mytyb_1 \myappsp \myb{x_1} \myappsp \myb{y_1} \myeq \mytyb_2 \myappsp \myb{x_2} \myappsp \myb{y_2}}}}
    \end{array}
    \right)) \myand \\
    \myjm{\myse{k}_1}{\mynat}{\myse{k}_2}{\mynat}
  \end{array} & 
\end{array}
\]
The result, while looking complicated, is actually saying something
simple---given equal inputs, the parameters for $\mytyc{Max}$ will
return equal types.  Moreover, we have evidence that the two $\myb{k}$
parameters are equal.  When coercing, we need to mechanically generate
one proof of equality for each argument, and then coerce:
\[
\begin{array}{@{}l}
\mycoee{(\mytyc{Max} \myappsp \mytya_1 \myappsp \mytyb_1 \myappsp \myse{k}_1)}{(\mytyc{Max} \myappsp \mytya_2 \myappsp \mytyb_2 \myappsp \myse{k}_2)}{\myse{Q}}{(\mydc{max} \myappsp \myse{ak}_1 \myappsp \myse{n}_1 \myappsp \myse{a}_1 \myappsp \myse{b}_1)} \myred \\
\myind{2}
\begin{array}[t]{l@{\ }l@{\ }c@{\ }l}
  \mysyn{let} & \myb{Q_{Ak}} & \mapsto & \myhole{?} : \myprdec{\mytya_1 \myappsp \myse{k}_1 \myeq \mytya_2 \myappsp \myse{k}_2} \\
              & \myb{ak_2}    & \mapsto & \mycoee{(\mytya_1 \myappsp \myse{k}_1)}{(\mytya_2 \myappsp \myse{k}_2)}{\myb{Q_{Ak}}}{\myse{ak_1}} : \mytya_1 \myappsp \myse{k}_2 \\
              & \myb{Q_{\mathbb{N}}} & \mapsto & \myhole{?} : \myprdec{\mynat \myeq \mynat} \\
              & \myb{n_2} & \mapsto & \mycoee{\mynat}{\mynat}{\myb{Q_{\mathbb{N}}}}{\myse{n_1}} : \mynat \\
              & \myb{Q_A} & \mapsto & \myhole{?} : \myprdec{\mytya_1 \myappsp \myse{n_1} \myeq \mytya_2 \myappsp \myb{n_2}} \\
              & \myb{a_2} & \mapsto & \mycoee{(\mytya_1 \myappsp \myse{n_1})}{(\mytya_2 \myappsp \myb{n_2})}{\myb{Q_A}} :  \mytya_2 \myappsp \myb{n_2} \\
              & \myb{Q_B} & \mapsto & \myhole{?} : \myprdec{\mytyb_1 \myappsp \myse{n_1} \myappsp \myse{a}_1 \myeq \mytyb_1 \myappsp \myb{n_2} \myappsp \myb{a_2}} \\
              & \myb{b_2} & \mapsto & \mycoee{(\mytyb_1 \myappsp \myse{n_1} \myappsp \myse{a_1})}{(\mytyb_2 \myappsp \myb{n_2} \myappsp \myb{a_2})}{\myb{Q_B}} :  \mytyb_2 \myappsp \myb{n_2} \myappsp \myb{a_2} \\
  \mysyn{in} & \multicolumn{3}{@{}l}{\mydc{max} \myappsp \myb{ak_2} \myappsp \myb{n_2} \myappsp \myb{a_2} \myappsp \myb{b_2}}
\end{array}
\end{array}
\]
For equalities regarding types that are external to the data type we can
derive a proof by reflexivity by invoking $\mydc{refl}$ as defined in
Section \ref{sec:lazy}, and the instantiate arguments if we need too.
In this case, for $\mynat$, we do not have any arguments.  For
equalities concerning arguments of the type constructor or already
coerced arguments of the type constructor we have to refer to the right
proof and use $\mycoh$erence when due, which is where the technical
annoyance lies:
\[
\begin{array}{@{}l}
\mycoee{(\mytyc{Max} \myappsp \mytya_1 \myappsp \mytyb_1 \myappsp \myse{k}_1)}{(\mytyc{Max} \myappsp \mytya_2 \myappsp \mytyb_2 \myappsp \myse{k}_2)}{\myse{Q}}{(\mydc{max} \myappsp \myse{ak}_1 \myappsp \myse{n}_1 \myappsp \myse{a}_1 \myappsp \myse{b}_1)} \myred \\
\myind{2}
\begin{array}[t]{l@{\ }l@{\ }c@{\ }l}
  \mysyn{let} & \myb{Q_{Ak}} & \mapsto & (\myproj{2} \myappsp (\myproj{1} \myappsp \myse{Q})) \myappsp \myse{k_1} \myappsp \myse{k_2} \myappsp (\myproj{3} \myappsp \myse{Q}) : \myprdec{\mytya_1 \myappsp \myse{k}_1 \myeq \mytya_2 \myappsp \myse{k}_2} \\
              & \myb{ak_2}    & \mapsto & \mycoee{(\mytya_1 \myappsp \myse{k}_1)}{(\mytya_2 \myappsp \myse{k}_2)}{\myb{Q_{Ak}}}{\myse{ak_1}} : \mytya_1 \myappsp \myse{k}_2 \\
              & \myb{Q_{\mathbb{N}}} & \mapsto & \mydc{refl} \myappsp \mynat : \myprdec{\mynat \myeq \mynat} \\
              & \myb{n_2} & \mapsto & \mycoee{\mynat}{\mynat}{\myb{Q_{\mathbb{N}}}}{\myse{n_1}} : \mynat \\
              & \myb{Q_A} & \mapsto & (\myproj{2} \myappsp (\myproj{1} \myappsp \myse{Q})) \myappsp \myse{n_1} \myappsp \myb{n_2} \myappsp (\mycohh{\mynat}{\mynat}{\myb{Q_{\mathbb{N}}}}{\myse{n_1}}) : \myprdec{\mytya_1 \myappsp \myse{n_1} \myeq \mytya_2 \myappsp \myb{n_2}} \\
              & \myb{a_2} & \mapsto & \mycoee{(\mytya_1 \myappsp \myse{n_1})}{(\mytya_2 \myappsp \myb{n_2})}{\myb{Q_A}} :  \mytya_2 \myappsp \myb{n_2} \\
              & \myb{Q_B} & \mapsto & (\myproj{2} \myappsp (\myproj{2} \myappsp \myse{Q})) \myappsp \myse{n_1} \myappsp \myb{n_2} \myappsp \myb{Q_{\mathbb{N}}} \myappsp \myse{a_1} \myappsp \myb{a_2} \myappsp (\mycohh{(\mytya_1 \myappsp \myse{n_1})}{(\mytya_2 \myappsp \myse{n_2})}{\myb{Q_A}}{\myse{a_1}}) : \myprdec{\mytyb_1 \myappsp \myse{n_1} \myappsp \myse{a}_1 \myeq \mytyb_1 \myappsp \myb{n_2} \myappsp \myb{a_2}} \\
              & \myb{b_2} & \mapsto & \mycoee{(\mytyb_1 \myappsp \myse{n_1} \myappsp \myse{a_1})}{(\mytyb_2 \myappsp \myb{n_2} \myappsp \myb{a_2})}{\myb{Q_B}} :  \mytyb_2 \myappsp \myb{n_2} \myappsp \myb{a_2} \\
  \mysyn{in} & \multicolumn{3}{@{}l}{\mydc{max} \myappsp \myb{ak_2} \myappsp \myb{n_2} \myappsp \myb{a_2} \myappsp \myb{b_2}}
\end{array}
\end{array}
\]

\subsubsection{$\myprop$ and the hierarchy}

We shall have, at each universe level, not only a $\mytyp_l$ but also a
$\myprop_l$.  Where will propositions 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 level compatible
(read: larger) with its 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 at least type $\mytyp_l$, where
$\mytya_l : \mytyp_l$ and $\mytyb_l : \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 members of $\myprop_0$ to be members of $\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 type check
canonical terms), one quoting neutral terms while recovering their
types.  The full procedure for quotation is shown in Figure
\ref{fig:kant-quot}. We $\boxed{\text{box}}$ the neutral proofs and
neutral members of empty types, following the notation in
\cite{Altenkirch2007}, and we make use of $\mydefeq_{\mybox}$ which
compares terms syntactically up to $\alpha$-renaming, but also up to
equivalent proofs: we consider all boxed content as equal.

Our quotation will work on normalised terms, so that all defined values
will have been replaced.  Moreover, we match on data type eliminators and
all their arguments, so that $\mynat.\myfun{elim} \myappsp \mytmm
\myappsp \myse{P} \myappsp \vec{\mytmn}$ will stand for
$\mynat.\myfun{elim}$ applied to the scrutinised $\mynat$, the
predicate, and the two cases.  This measure can be easily implemented by
checking the head of applications and `consuming' the needed terms.

\begin{figure}[t]
  \mydesc{canonical quotation:}{\mycanquot(\myctx, \mytmsyn : \mytmsyn) \mymetagoes \mytmsyn}{
    \small
    $
    \begin{array}{@{}l@{}l}
      \mycanquot(\myctx,\ \mytmt : \mytyc{D} \myappsp \vec{A} &) \mymetaguard \mymeta{empty}(\myctx, \mytyc{D}) \mymetagoes \boxed{\mytmt} \\
      \mycanquot(\myctx,\ \mytmt : \mytyc{D} \myappsp \vec{A} &) \mymetaguard \mymeta{record}(\myctx, \mytyc{D}) \mymetagoes  \mytyc{D}.\mydc{constr} \myappsp \cdots \myappsp \mycanquot(\myctx, \mytyc{D}.\myfun{f}_n : (\myctx(\mytyc{D}.\myfun{f}_n))(\vec{A};\mytmt)) \\
      \mycanquot(\myctx,\ \mytyc{D}.\mydc{c} \myappsp \vec{t} : \mytyc{D} \myappsp \vec{A} &) \mymetagoes \cdots \\
      \mycanquot(\myctx,\ \myse{f} : \myfora{\myb{x}}{\mytya}{\mytyb} &) \mymetagoes \myabs{\myb{x}}{\mycanquot(\myctx; \myb{x} : \mytya, \myapp{\myse{f}}{\myb{x}} : \mytyb)} \\
      \mycanquot(\myctx,\ \myse{p} : \myprdec{\myse{P}} &) \mymetagoes \boxed{\myse{p}}
     \\
    \mycanquot(\myctx,\ \mytmt : \mytya &) \mymetagoes \mytmt'\ \text{\textbf{where}}\ \mytmt' : \myarg = \myneuquot(\myctx, \mytmt)
    \end{array}
    $
  }

  \mynegder

  \mydesc{neutral quotation:}{\myneuquot(\myctx, \mytmsyn) \mymetagoes \mytmsyn : \mytmsyn}{
    \small
    $
    \begin{array}{@{}l@{}l}
      \myneuquot(\myctx,\ \myb{x} &) \mymetagoes \myb{x} : \myctx(\myb{x}) \\
      \myneuquot(\myctx,\ \mytyp  &) \mymetagoes \mytyp : \mytyp \\
      \myneuquot(\myctx,\ \myfora{\myb{x}}{\mytya}{\mytyb} & ) \mymetagoes
       \myfora{\myb{x}}{\myneuquot(\myctx, \mytya)}{\myneuquot(\myctx; \myb{x} : \mytya, \mytyb)} : \mytyp \\
      \myneuquot(\myctx,\ \mytyc{D} \myappsp \vec{A} &) \mymetagoes \mytyc{D} \myappsp \cdots \mycanquot(\myctx, \mymeta{head}((\myctx(\mytyc{D}))(\mytya_1 \cdots \mytya_{n-1}))) : \mytyp \\
      \myneuquot(\myctx,\ \myprdec{\myjm{\mytmm}{\mytya}{\mytmn}{\mytyb}} &) \mymetagoes \myprdec{\myjm{\mycanquot(\myctx, \mytmm : \mytya)}{\mytya'}{\mycanquot(\myctx, \mytmn : \mytyb)}{\mytyb'}} : \mytyp \\
      \multicolumn{2}{@{}l}{\myind{2}\text{\textbf{where}}\ \mytya' : \myarg = \myneuquot(\myctx, \mytya)} \\
      \multicolumn{2}{@{}l}{\myind{2}\phantom{\text{\textbf{where}}}\ \mytyb' : \myarg = \myneuquot(\myctx, \mytyb)} \\
      \myneuquot(\myctx,\ \mytyc{D}.\myfun{f} \myappsp \mytmt &) \mymetaguard \mymeta{record}(\myctx, \mytyc{D}) \mymetagoes \mytyc{D}.\myfun{f} \myappsp \mytmt' : (\myctx(\mytyc{D}.\myfun{f}))(\vec{A};\mytmt) \\
      \multicolumn{2}{@{}l}{\myind{2}\text{\textbf{where}}\ \mytmt' : \mytyc{D} \myappsp \vec{A} = \myneuquot(\myctx, \mytmt)} \\
      \myneuquot(\myctx,\ \mytyc{D}.\myfun{elim} \myappsp \mytmt \myappsp \myse{P} &) \mymetaguard \mymeta{empty}(\myctx, \mytyc{D}) \mymetagoes \mytyc{D}.\myfun{elim} \myappsp \boxed{\mytmt} \myappsp \myneuquot(\myctx, \myse{P}) : \myse{P} \myappsp \mytmt \\
      \myneuquot(\myctx,\ \mytyc{D}.\myfun{elim} \myappsp \mytmm \myappsp \myse{P} \myappsp \vec{\mytmn} &) \mymetagoes \mytyc{D}.\myfun{elim} \myappsp \mytmm' \myappsp \myneuquot(\myctx, \myse{P}) \cdots : \myse{P} \myappsp \mytmm\\
      \multicolumn{2}{@{}l}{\myind{2}\text{\textbf{where}}\ \mytmm' : \mytyc{D} \myappsp \vec{A} = \myneuquot(\myctx, \mytmm)} \\
      \myneuquot(\myctx,\ \myapp{\myse{f}}{\mytmt} &) \mymetagoes \myapp{\myse{f'}}{\mycanquot(\myctx, \mytmt : \mytya)} : \mysub{\mytyb}{\myb{x}}{\mytmt} \\
      \multicolumn{2}{@{}l}{\myind{2}\text{\textbf{where}}\ \myse{f'} : \myfora{\myb{x}}{\mytya}{\mytyb} = \myneuquot(\myctx, \myse{f})} \\
       \myneuquot(\myctx,\ \mycoee{\mytya}{\mytyb}{\myse{Q}}{\mytmt} &) \mymetaguard \myneuquot(\myctx, \mytya) \mydefeq_{\mybox} \myneuquot(\myctx, \mytyb) \mymetagoes \myneuquot(\myctx, \mytmt) \\
\myneuquot(\myctx,\ \mycoee{\mytya}{\mytyb}{\myse{Q}}{\mytmt} &) \mymetagoes
       \mycoee{\myneuquot(\myctx, \mytya)}{\myneuquot(\myctx, \mytyb)}{\boxed{\myse{Q}}}{\myneuquot(\myctx, \mytmt)}
    \end{array}
    $
  }
  \caption{Quotation in \mykant.  Along the already used
    $\mymeta{record}$ meta-operation on the context we make use of
    $\mymeta{empty}$, which checks if a certain type constructor has
    zero data constructor.  The `data constructor' cases for non-record,
    non-empty, data types are omitted for brevity.}
  \label{fig:kant-quot}
\end{figure}

\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 apart from equalities on neutral
  terms.} 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}.

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

\epigraph{\emph{It's alive!}}{Henry Frankenstein}

The codebase consists of around 2500 lines of Haskell,\footnote{The full
  source code is available under the GPL3 license at
  \url{https://github.com/bitonic/kant}.  `Kant' was a previous
  incarnation of the software, and the name remained.} 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 by \cite{McBride2004}.

The author learnt the hard way the implementation challenges for such a
project, and ran out of time while implementing observational equality.
While the constructs and typing rules are present, the machinery to make
it happen (equality reduction, coercions, quotation, etc.) is not
present yet.

This considered, everything else presented in Section
\ref{sec:kant-theory} is implemented and working well---and in fact all
the examples presented in this thesis, apart from the ones that are
equality related, have been encoded in \mykant\ in the Appendix.
Moreover, given the detailed plan in the previous section, finishing off
should not prove too much work.

The interaction with the user takes place in a loop living in and
updating a context of \mykant\ declarations, which presents itself as in
Figure \ref{fig:kant-web}.  Files with lists of declarations can also be
loaded. The REPL is a available both as a command-line application and in
a web interface, which is available at \url{bertus.mazzo.li}.

A REPL cycle starts with the user inputting 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{figure}[b!]
{\small\begin{Verbatim}[frame=leftline,xleftmargin=3cm]
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}


\begin{description}

\item[Parse] In this phase the text input gets converted to a sugared
  version of the core language.  For example, we accept multiple
  arguments in arrow types and abstractions, and we represent variables
  with names, while as we will see in Section \ref{sec:term-repr} the
  final term types uses a \emph{nameless} representation.

\item[Desugar] The sugared declaration is converted to a core term.
  Most notably we go from names to nameless.

\item[ConDestr] Short for `Constructors/Destructors', converts
  applications of data destructors and constructors to a special form,
  to perform bidirectional type checking.

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

\item[Elaborate/Typecheck/Evaluate] \textbf{Elaboration} 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.  Among the other things in this stage we
  go from nameless back to names by recycling the names that the user
  used originally, as to fabricate a term which is as close as possible
  to what it originated from.

\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] (condestr) {ConDestr};
        \node [block, below=of condestr] (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] (pretty) {Pretty print};
        \node [block, below=of pretty] (distill) {Distill};
        \node [block, below=of distill] (update) {Update context};
        
        \path [line] (user) -- (parse);
        \path [line] (parse) -- (desugar);
        \path [line] (desugar) -- (condestr);
        \path [line] (condestr) -- (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] (pretty) -- (user);
        \path [line] (distill) -- (pretty);
        \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{Syntax}

The syntax of \mykant\ is presented in Figure \ref{fig:syntax}.
Examples showing the usage of most of the constructs---excluding the
OTT-related ones---are present in Appendices \ref{app:kant-itt},
\ref{app:kant-examples}, and \ref{app:hurkens}; plus a tutorial in
Section \ref{sec:type-holes}.  The syntax has grown organically with the
needs of the language, and thus is not very sophisticated.  The grammar
is specified in and processed by the \texttt{happy} parser generator for
Haskell.\footnote{Available at \url{http://www.haskell.org/happy}.}
Tokenisation is performed by a simple hand written lexer.

\begin{figure}[p]
  \centering
  $
  \begin{array}{@{\ \ }l@{\ }c@{\ }l}
    \multicolumn{3}{@{}l}{\text{A name, in regexp notation.}} \\
    \mysee{name}   & ::= & \texttt{[a-zA-Z] [a-zA-Z0-9'\_-]*} \\
    \multicolumn{3}{@{}l}{\text{A binder might or might not (\texttt{\_}) bind a name.}} \\
    \mysee{binder} & ::= & \mytermi{\_} \mysynsep \mysee{name} \\
    \multicolumn{3}{@{}l}{\text{A series of typed bindings.}} \\
    \mysee{telescope}\, \ \ \  & ::= & (\mytermi{[}\ \mysee{binder}\ \mytermi{:}\ \mysee{term}\ \mytermi{]}){*} \\
    \multicolumn{3}{@{}l}{\text{Terms, including propositions.}} \\
    \multicolumn{3}{@{}l}{
      \begin{array}{@{\ \ }l@{\ }c@{\ }l@{\ \ \ \ \ }l}
    \mysee{term} & ::= & \mysee{name} & \text{A variable.} \\
                 &  |  & \mytermi{*}  & \text{\mytyc{Type}.} \\
                 &  |  & \mytermi{\{|}\ \mysee{term}{*}\ \mytermi{|\}} & \text{Type holes.} \\
                 &  |  & \mytermi{Prop} & \text{\mytyc{Prop}.} \\
                 &  |  & \mytermi{Top} \mysynsep \mytermi{Bot} & \text{$\mytop$ and $\mybot$.} \\
                 &  |  & \mysee{term}\ \mytermi{/\textbackslash}\ \mysee{term} & \text{Conjuctions.} \\
                 &  |  & \mytermi{[|}\ \mysee{term}\ \mytermi{|]} & \text{Proposition decoding.} \\
                 &  |  & \mytermi{coe}\ \mysee{term}\ \mysee{term}\ \mysee{term}\ \mysee{term} & \text{Coercion.} \\
                 &  |  & \mytermi{coh}\ \mysee{term}\ \mysee{term}\ \mysee{term}\ \mysee{term} & \text{Coherence.} \\
                 &  | & \mytermi{(}\ \mysee{term}\ \mytermi{:}\ \mysee{term}\ \mytermi{)}\ \mytermi{=}\ \mytermi{(}\ \mysee{term}\ \mytermi{:}\ \mysee{term}\ \mytermi{)} & \text{Heterogeneous equality.} \\
                 &  |  & \mytermi{(}\ \mysee{compound}\ \mytermi{)} & \text{Parenthesised term.} \\
      \mysee{compound} & ::= & \mytermi{\textbackslash}\ \mysee{binder}{*}\ \mytermi{=>}\ \mysee{term} & \text{Untyped abstraction.} \\
                       &  |  & \mytermi{\textbackslash}\ \mysee{telescope}\ \mytermi{:}\ \mysee{term}\ \mytermi{=>}\ \mysee{term} & \text{Typed abstraction.} \\
                 &  | & \mytermi{forall}\ \mysee{telescope}\ \mysee{term} & \text{Universal quantification.} \\
                 &  | & \mysee{arr} \\
       \mysee{arr}    & ::= & \mysee{telescope}\ \mytermi{->}\ \mysee{arr} & \text{Dependent function.} \\
                      &  |  & \mysee{term}\ \mytermi{->}\ \mysee{arr} & \text{Non-dependent function.} \\
                      &  |  & \mysee{term}{+} & \text {Application.}
      \end{array}
    } \\
    \multicolumn{3}{@{}l}{\text{Typed names.}} \\
    \mysee{typed} & ::= & \mysee{name}\ \mytermi{:}\ \mysee{term} \\
    \multicolumn{3}{@{}l}{\text{Declarations.}} \\
    \mysee{decl}& ::= & \mysee{value} \mysynsep \mysee{abstract} \mysynsep \mysee{data} \mysynsep \mysee{record} \\
    \multicolumn{3}{@{}l}{\text{Defined values.  The telescope specifies named arguments.}} \\
    \mysee{value} & ::= & \mysee{name}\ \mysee{telescope}\ \mytermi{:}\ \mysee{term}\ \mytermi{=>}\ \mysee{term} \\
    \multicolumn{3}{@{}l}{\text{Abstracted variables.}} \\
    \mysee{abstract} & ::= & \mytermi{postulate}\ \mysee{typed} \\
    \multicolumn{3}{@{}l}{\text{Data types, and their constructors.}} \\
    \mysee{data} & ::= & \mytermi{data}\ \mysee{name}\ \mysee{telescope}\ \mytermi{->}\ \mytermi{*}\ \mytermi{=>}\ \mytermi{\{}\ \mysee{constrs}\ \mytermi{\}} \\
    \mysee{constrs} & ::= & \mysee{typed} \\
                   &  |  & \mysee{typed}\ \mytermi{|}\ \mysee{constrs} \\
    \multicolumn{3}{@{}l}{\text{Records, and their projections.  The $\mysee{name}$ before the projections is the constructor name.}} \\
    \mysee{record} & ::= & \mytermi{record}\ \mysee{name}\ \mysee{telescope}\ \mytermi{->}\ \mytermi{*}\ \mytermi{=>}\ \mysee{name}\ \mytermi{\{}\ \mysee{projs}\ \mytermi{\}} \\
    \mysee{projs} & ::= & \mysee{typed} \\
                   &  |  & \mysee{typed}\ \mytermi{,}\ \mysee{projs}
  \end{array}
  $

  \caption{\mykant' syntax.  The non-terminals are marked with
    $\langle\text{angle brackets}\rangle$ for greater clarity.  The
    syntax in the implementation is actually more liberal, for example
    giving the possibility of using arrow types directly in
    constructor/projection declarations.\\
    Additionally, we give the user the possibility of using Unicode
    characters instead of their ASCII counterparts, e.g. \texttt{→} in
    place of \texttt{->}, \texttt{λ} in place of
    \texttt{\textbackslash}, etc.}
  \label{fig:syntax}
\end{figure}

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

\subsubsection{Naming and substituting}

Perhaps surprisingly, one of the most difficult 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 slightly more complicated
  systems it is very hard to get right, even for experts.

  One of the sore spots of explicit names is comparing terms up to
  $\alpha$-renaming, which again generates a huge amounts of
  substitutions and requires special care.  

\item[Nameless] We can capture the relationship between variables and
  their binders, by getting rid of names altogether, and representing
  bound variables with an index referring to the `binding' structure, a
  notion introduced by \cite{de1972lambda}.  Usually $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
  \[
  \begin{array}{@{}l}
  \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\text{, which corresponds to} \\
  \myabs{\myb{f}}{(\myabs{\myb{g}}{\myapp{\myb{g}}{(\myabs{\myb{x}}{\myb{x}})}}) \myappsp (\myabs{\myb{x}}{\myapp{\myb{f}}{\myb{x}}})} : ((\mytya \myarr \mytya) \myarr \mytyb) \myarr \mytyb
  \end{array}
  \]

  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.  $\alpha$-renaming ceases to be an issue, and
  term comparison is purely syntactical.

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

\end{description}

In the past decade or so advancements in the Haskell's type system and
in general the spread new programming practices have made the nameless
option much more amenable.  \mykant\ thus takes the nameless path
through the use of Edward Kmett's excellent \texttt{bound}
library.\footnote{Available at
  \url{http://hackage.haskell.org/package/bound}.}  We describe the
advantages of \texttt{bound}'s approach, but also its 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 the work of \cite{Bird1999}, who suggested to
  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}
-- A type with no members.
data Empty

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 Empty}, 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}}}\]
can be represented as
\begin{Verbatim}
-- The top level term is of type `Tm Empty'.
-- The inner term `Lam (Free Bound)' is of type `Tm (Var Empty)'.
-- The second inner term `V (Free Bound)' is of type `Tm (Var (Var
-- Empty))'.
Lam (Lam (V (Free Bound)))
\end{Verbatim}
This allows us to reflect the of a type `nestedness' at the type level,
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}
type class:
\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 refers 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 = s >>= \v -> case v of
                           Bound   -> t
                           Free v' -> return v'
\end{Verbatim}
The beauty of this technique is that with a few simple functions 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.  For what concerns term equality, we can just ask the Haskell
compiler to derive the instance for the \verb|Eq| type class and since
we are nameless that will be enough (modulo fancy quotation).

Moreover, if we take the top level term type to be \verb|Tm String|, we
get 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.  In Haskell we can give them a faithful representation
with a data type along the lines of
\begin{Verbatim}
data Tele m v = Empty (m v) | Bind (m v) (Tele m (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
Appendix \ref{app:termrep}.  The fact that propositions cannot be
factored out in another data type is an instance of the problem
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
more flexibility with a nice interface similar to the one of
\verb|bound|.

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{Evaluation}

Another source of contention related to term representation is dealing
with evaluation.  Here \mykant\ does not make bold moves, and simply
employs substitution.  When type checking we match types by reducing
them to their weak head normal form, as to avoid unnecessary evaluation.

We treat data types eliminators and record projections in an uniform
way, by elaborating declarations in a series of \emph{rewriting rules}:
\begin{Verbatim}
type Rewr =
    forall v.
    TmRef v   -> -- Term to which the destructor is applied
    [TmRef v] -> -- List of other arguments
    -- The result of the rewriting, if the eliminator reduces.
    Maybe [TmRef v]
\end{Verbatim}
A rewriting rule is polymorphic in the variable type, guaranteeing that
it just pattern matches on terms structure and rearranges them in some
way, and making it possible to apply it at any level in the term.  When
reducing a series of applications we match the first term and check if
it is a destructor, and if that's the case we apply the reduction rule
and reduce further if it yields a new list of terms.

This has the advantage of simplicity, at the expense of being quite poor
in terms of performance and that we need to do quotation manually.  An
alternative that solves both of these is the already mentioned
\emph{normalization by evaluation}, where we would compute by turning
terms into Haskell values, and then reify back to terms to compare
them---a useful tutorial on this technique is given by \cite{Loh2010}.

\subsubsection{Parametrised environment}

Through the life of a REPL cycle we need to execute two broad
`effectful' actions:
\begin{itemize}
\item Retrieve, add, and modify elements to an environment.  The
  environment will contain not only types, but also the rewriting rules
  presented in the previous section, and a counter to generate fresh
  references for the type hierarchy.

\item Throw various kinds of errors when something goes wrong: parsing,
  type checking, input/output error when reading files, and more.
\end{itemize}
Haskell taught us the value of monads in programming languages, and in
\mykant\ we keep this lesson in mind.  All of the plumbing required to do
the two actions above is provided by a very general \emph{monad
  transformer} that we use through the codebase, \texttt{KMonadT}:
\begin{Verbatim}
newtype KMonad f v m a = KMonad (StateT (f v) (ErrorT KError m) a)

data KError
    = OutOfBounds Id
    | DuplicateName Id
    | IOError IOError
    | ...
\end{Verbatim}
Without delving into the details of what a monad transformer is, this is
what \texttt{KMonadT} provides:
\begin{itemize}
\item The \verb|v| parameter represents the parametrised variable for
  the term type that we spoke about at the beginning of this section.
  More on this later.

\item The \verb|f| parameter indicates what kind of environment we are
  holding.  Sometimes we want to traverse terms without carrying the
  entire environment, for various reasons---\texttt{KMonatT} lets us do
  that.  Note that \verb|f| is itself parametrised over \verb|v|.  The
  inner \verb|StateT| monad transformer lets us retrieve and modify this
  environment at any time.

\item The \verb|m| is the `inner' monad that we can `plug in' to be able
  to do more effectful actions in \texttt{KMonatT}.  For example if we
  plug the \texttt{IO} monad in, we will be able to do input/output.

\item The inner \verb|ErrorT| lets us throw errors at any time.  The
  error type is \verb|KError|, which describes all the possible errors
  that a \mykant\ process can throw.

\item Finally, the \verb|a| parameter represents the return type of the
  computation we are executing.
\end{itemize}

The clever trick in \texttt{KMonadT} is to have it to be parametrised
over the same type as the term type.  This way, we can easily carry the
environment while traversing under binders.  For example, if we only
needed to carry types of bound variables in the environment, we can
quickly set up the following infrastructure:
\begin{Verbatim}
data Tm v = ...

-- A context is a mapping from variables to types.
newtype Ctx v = Ctx (v -> Tm v)

-- A context monad holds a context.
type CtxMonad v m = KMonadT Ctx v m

-- Enter into a scope binding a type to the variable, execute a
-- computation there, and return exit the scope returning to the `current'
-- context.
nestM :: Monad m => Tm v -> CtxMonad (Var v) m a -> CtxMonad v m a
nestM = ...
\end{Verbatim}
Again, the types guard our back guaranteeing that we add a type when we
enter a scope, and we discharge it when we get out.  The author
originally started with a more traditional representation and often
forgot to add the right variable at the right moment.  Using this
practices it is very difficult to do so---we achieve correctness through
types.

In the actual \mykant\ codebase, we have also abstracted the concept of
`context' further, so that we can easily embed contexts into other
structures and write generic operations on all context-like
structures.\footnote{See the \texttt{Kant.Cursor} module for details.}

\subsection{Turning constraints into graphs}
\label{sec:hier-impl}

In this section we will explain how to implement the typical ambiguity
we have spoken about in \ref{sec:term-hierarchy} efficiently, a subject
which is often dismissed in the literature.  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 for 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.  The problem predictably reduces
to a graph algorithm, and for this reason we also implement a library
for labelled graphs, since the existing Haskell graph libraries fell
short in different areas.\footnote{We tried the \texttt{Data.Graph}
  module in \url{http://hackage.haskell.org/package/containers}, and the
  much more featureful \texttt{fgl} library
  \url{http://hackage.haskell.org/package/fgl}.}  The interfaces for
these modules are shown in Appendix \ref{app:constraint}.  The graph
library is implemented as a modification of the code described by
\cite{King1995}.

We represent the set by building a graph where vertices are variables,
and edges are constraints between them, labelled with the appropriate
constraint: $x < y$ gives rise to a $<$-labelled edge from $x$ to $y$,
and $x \le y$ to a $\le$-labelled edge from $x$ to $y$.  As we add
constraints, $\le$ constraints are replaced by $<$ constraints, so that
if we started with an empty set and added
\[
   x < y,\ y \le z,\ z \le k,\ k < j,\ j \le y\
\]
it would generate the graph shown in Figure \ref{fig:graph-one-before},
but adding $z < k$ would strengthen the edge from $z$ to $k$, as shown
in \ref{fig:graph-one-after}.

\begin{figure}[t]
  \centering
  \begin{subfigure}[b]{0.3\textwidth}
    \begin{tikzpicture}[node distance=1.5cm]
      % Place nodes
      \node (x) {$x$};
      \node [right of=x] (y) {$y$};
      \node [right of=y] (z) {$z$};
      \node [below of=z] (k) {$k$};
      \node [left  of=k] (j) {$j$};
      %% Lines
      \path[->]
      (x) edge node [above] {$<$}   (y)
      (y) edge node [above] {$\le$} (z)
      (z) edge node [right] {$\le$}   (k)
      (k) edge node [below] {$\le$} (j)
      (j) edge node [left ] {$\le$} (y);
    \end{tikzpicture}
    \caption{Before $z < k$.}
    \label{fig:graph-one-before}
  \end{subfigure}%
  ~
  \begin{subfigure}[b]{0.3\textwidth}
    \begin{tikzpicture}[node distance=1.5cm]
      % Place nodes
      \node (x) {$x$};
      \node [right of=x] (y) {$y$};
      \node [right of=y] (z) {$z$};
      \node [below of=z] (k) {$k$};
      \node [left  of=k] (j) {$j$};
      %% Lines
      \path[->]
      (x) edge node [above] {$<$}   (y)
      (y) edge node [above] {$\le$} (z)
      (z) edge node [right] {$<$}   (k)
      (k) edge node [below] {$\le$} (j)
      (j) edge node [left ] {$\le$} (y);
    \end{tikzpicture}
    \caption{After $z < k$.}
    \label{fig:graph-one-after}
  \end{subfigure}%
  ~
  \begin{subfigure}[b]{0.3\textwidth}
    \begin{tikzpicture}[remember picture, node distance=1.5cm]
      \begin{pgfonlayer}{foreground}
      % Place nodes
      \node (x) {$x$};
      \node [right of=x] (y) {$y$};
      \node [right of=y] (z) {$z$};
      \node [below of=z] (k) {$k$};
      \node [left  of=k] (j) {$j$};
      %% Lines
      \path[->]
      (x) edge node [above] {$<$}   (y)
      (y) edge node [above] {$\le$} (z)
      (z) edge node [right] {$<$}   (k)
      (k) edge node [below] {$\le$} (j)
      (j) edge node [left ] {$\le$} (y);
    \end{pgfonlayer}{foreground}
    \end{tikzpicture}
    \begin{tikzpicture}[remember picture, overlay]
      \begin{pgfonlayer}{background}
      \fill [red, opacity=0.3, rounded corners]
      (-2.7,2.6) rectangle (-0.2,0.05)
      (-4.1,2.4) rectangle (-3.3,1.6);
    \end{pgfonlayer}{background}
    \end{tikzpicture}
    \caption{SCCs.}
    \label{fig:graph-one-scc}
  \end{subfigure}%
  \caption{Strong constraints overrule weak constraints.}
  \label{fig:graph-one}
\end{figure}

Each time we add a new constraint, we check if any strongly connected
component (SCC) arises, a SCC being a subset $V$ of vertices where for
each $(v_1,v_2) \in V \times V$ there is a path from $v_1$ to $v_2$.
The SCCs in the graph for the constraints above is shown in Figure
\ref{fig:graph-one-scc}.  If we have a strongly connected component with
a $<$ edge---say $x < y$---in it, we have an inconsistency, since there
must also be a path from $y$ to $x$, and by transitivity it must either
be the case that $y \le x$ or $y < x$, which are both at odds with $x <
y$.

Moreover, if we have a SCC with no $<$ edges, it means that all members
of said SCC are equal, since for every $x \le y$ we have a path from $y$
to $x$, which again by transitivity means that $y \le x$.  Thus, we can
\emph{condense} the SCC to a single vertex, by choosing a variable among
the SCC as a representative for all the others.  This can be done
efficiently with disjoint set data structure, and is crucial to keep the
graph compact, given the very large number of constraints generated when
type checking.

\subsection{(Web) REPL}

Finally, we take a break from the types by giving a brief account of the
design of our REPL, being a good example of modular design using various
constructs dear to the Haskell programmer.

Across our codebase we make use of a \emph{monad transformers} named
\texttt{KMonadT}.  Without delving into the details of \texttt{KMonadT}
or of monad transformers,\footnote{See
  \url{https://en.wikibooks.org/wiki/Haskell/Monad_transformers.}}
computation done inside \texttt{KMonadT} can easily retrieve and modify
the environment and throw various kind of errors, be them parse error,
type errors, etc. Moreover, \texttt{KMonadT} being a monad
\emph{transformers}, we can `plug in' other monads to have access to
other facilities, such as input/output.

That said, the REPL is represented as a function in \texttt{KMonadT}
consuming input and hopefully producing output.  Then, frontends can
very easily written by marshalling data in and out of the REPL:
\begin{Verbatim}
data Input
    = ITyCheck String           -- Type check a term
    | IEval String              -- Evaluate a term
    | IDecl String              -- Declare something
    | ...

data Output
    = OTyCheck TmRefId [HoleCtx] -- Type checked term, with holes
    | OPretty TmRefId            -- Term to pretty print, after evaluation
    | OHoles [HoleCtx]           -- Just holes, classically after loading a file
    | ... 
    
-- KMonadT is parametrised over the type of the variables, which depends
-- on how deep in the term structure we are.  For the REPL, we only deal
-- with top-level terms, and thus only `Id' variables---top level names.
type REPL m = KMonadT Id m

repl :: ReadFile m => Input -> REPL m Output
\end{Verbatim}
The \texttt{ReadFile} monad embodies the only `extra' action that we
need to have access too when running the REPL: reading files.  We could
simply use the \texttt{IO} monad, but this will not serve us well when
implementing front end facing untrusted parties accessing the application
running on our servers.  In our case we expose the REPL as a web
application, and we want the user to be able to load only from a
pre-defined directory, not from the entire file system.

For this reason we specify \texttt{ReadFile} to have just one function:
\begin{Verbatim}
class Monad m => ReadFile m where
    readFile' :: FilePath -> m (Either IOError String)
\end{Verbatim}
While in the command-line application we will use the \texttt{IO} monad
and have \texttt{readFile'} to work in the `obvious' way---by reading
the file corresponding to the given file path---in the web prompt we
will have it to accept only a file name, not a path, and read it from a
pre-defined directory:
\begin{Verbatim}
-- The monad that will run the web REPL.  The `ReaderT' holds the
-- filepath to the directory where the files loadable by the user live.
-- The underlying `IO' monad will be used to actually read the files.
newtype DirRead a = DirRead (ReaderT FilePath IO a)

instance ReadFile DirRead where
    readFile' fp =
        do -- We get the base directory in the `ReaderT' with `ask'
           dir <- DirRead ask
           -- Is the filepath provided an unqualified file name?
           if snd (splitFileName fp) == fp
              -- If yes, go ahead and read the file, by lifting
              -- `readFile'' into the IO monad
              then DirRead (lift (readFile' (dir </> fp)))
              -- If not, return an error
              else return (Left (strMsg ("Invalid file name `" ++ fp ++ "'")))
\end{Verbatim}
Once this light-weight infrastructure is in place, adding a web
interface was an easy exercise.  We use Jasper Van der Jeugt's
\texttt{websockets} library\footnote{Available at
  \url{http://hackage.haskell.org/package/websockets}.} to create a proxy
that receives JSON messages with the user input, turns them into
\texttt{Input} messages for the REPL, and then sends back a JSON message
with the response.  Moreover, each client is handled in a separate
threads, so crashes of the REPL in single threads will not bring the
whole application down.

On the clients side, we had to write some JavaScript to accept input
from a form, and to make the responses appear on the screen.  The web
prompt is publicly available at \url{http://bertus.mazzo.li}, a sample
session is shown Figure \ref{fig:web-prompt-one}.

\begin{figure}[t]
  \includegraphics[width=\textwidth]{web-prompt.png}
  \caption{A sample run of the web prompt.}
  \label{fig:web-prompt-one}
\end{figure}



\section{Evaluation}
\label{sec:evaluation}

Going back to our goals in Section \ref{sec:contributions}, we feel that
this thesis fills a gap in the description of observational type theory.
In the design of \mykant\ we willingly patterned the core features
against the ones present in Agda, with the hope that future implementors
will be able to refer to this document without embarking on the same
adventure themselves.  We gave an original account of heterogeneous
equality by showing that in a cumulative hierarchy we can keep
equalities as small as we would be able too with a separate notion of
type equality.  As a side effect of developing \mykant, we also gave an
original account of bidirectional type checking for user defined types,
which get rid of many types while keeping the language very simple.

Through the design of the theory of \mykant\ we have followed an
approach where study and implementation were continuously interleaved,
as a `reality check' for the ideas that we wished to implement.  Given
the great effort necessary to build a theorem prover capable of
`real-world' proofs we have not attempted to compare \mykant's
capabilities to those of Agda and Coq, the theorem provers that the
author is most familiar with and in general two of the main players in
the field.  However we have ported a lot of simpler examples to check
that the key features are working, some of which have been used in the
previous sections and are reproduced in the appendices\footnote{The full
list is available in the repository:
\url{https://github.com/bitonic/kant/tree/master/data/samples/good}.}.
A full example of interaction with \mykant\ is given in Section
\ref{sec:type-holes}.

The main culprits for the delays in the implementation are two issues
that revealed themselves to be far less obvious than what the author
predicted.  The first, as we have already remarked in Section
\ref{sec:term-repr}, is to have an adequate term representation that
lets us express the right constructs in a safe way.  There is still no
widely accepted solution to this problem, which is approached in many
different ways both in the literature and in the programming
practice. The second aspect is the treatment of user defined data types.
Again, the best techniques to implement them in a dependently typed
setting still have not crystallised and implementors reinvent many
wheels each time a new system is built.  The author is still conflicted
on whether having user defined types at all it is the right decision:
while they are essential, in hindsight the idea of a bare but fully
implemented theory seems inviting.

In general, implementing dependently typed languages is still a poorly
understood practice, and almost every stage requires experimentation on
behalf of the author.  Another example is the treatment of the implicit
hierarchy, where no resources are present describing the problem from an
implementation perspective (we described our approach in Section
\ref{sec:hier-impl}).  Hopefully this state of things will change in the
near future, and recent publications are promising in this direction,
for example an unpublished paper by \cite{Brady2013} describing his
implementation of the Idris programming language.  Our ultimate goal is
to be a part of this collective effort.

\subsection{A type holes tutorial}
\label{sec:type-holes}

As a taster and showcase for the capabilities of \mykant, we present an
interactive session with the \mykant\ REPL.  While doing so, we present
a feature that we still have not covered: type holes.

Type holes are, in the author's opinion, one of the `killer' features of
interactive theorem provers, and one that is begging to be exported to
mainstream programming---although it is much more effective in a
well-typed, functional setting.  The idea is that when we are developing
a proof or a program we can insert a hole to have the software tell us
the type expected at that point.  Furthermore, we can ask for the type
of variables in context, to better understand our surroundings.

In \mykant\ we use type holes by putting them where a term should go.
We need to specify a name and then we can put as many terms as we like
in the hole.  \mykant\ will tell us which type it is expecting for the
term where the hole is, and the type of the terms that we have included.
For example if we had:
\begin{Verbatim}
plus [m n : Nat] : Nat ⇒ (
    {| h1 m n |}
)
\end{Verbatim}
And we loaded the file in \mykant, we would get:
\begin{Verbatim}[frame=leftline]
>>> :l plus.ka
Holes:
  h1 : Nat
    m : Nat
    n : Nat
\end{Verbatim}

Suppose we wanted to define the `less or equal' ordering on natural
numbers as described in Section \ref{sec:user-type}.  We will
incrementally build our functions in a file called \texttt{le.ka}.
First we define the necessary types, all of which we know well by now:
\begin{Verbatim}
data Nat : ⋆ ⇒ { zero : Nat | suc : Nat → Nat }

data Empty : ⋆ ⇒ { }
absurd [A : ⋆] [p : Empty] : A ⇒ (
    Empty-Elim p (λ _ ⇒ A)
)

record Unit : ⋆ ⇒ tt { }
\end{Verbatim}
Then fire up \mykant, and load the file:
\begin{Verbatim}[frame=leftline]
% ./bertus
B E R T U S
Version 0.0, made in London, year 2013.
>>> :l le.ka
OK
\end{Verbatim}
So far so good.  Our definition will be defined by recursion on a
natural number \texttt{n}, which will return a function that given
another number \texttt{m} will return the trivial type \texttt{Unit} if
$\texttt{n} \le \texttt{m}$, and the \texttt{Empty} type otherwise.
However we are still not sure on how to define it, so we invoke
$\texttt{Nat-Elim}$, the eliminator for natural numbers, and place holes
instead of arguments.  In the file we will write:
\begin{Verbatim}
le [n : Nat] : Nat → ⋆ ⇒ (
  Nat-Elim n (λ _ ⇒ Nat → ⋆)
    {|h1|}
    {|h2|}
)
\end{Verbatim}
And then we reload in \mykant:
\begin{Verbatim}[frame=leftline]
>>> :r le.ka
Holes:
  h1 : Nat → ⋆
  h2 : Nat → (Nat → ⋆) → Nat → ⋆
\end{Verbatim}
Which tells us what types we need to satisfy in each hole.  However, it
is not that clear what does what in each hole, and thus it is useful to
have a definition vacuous in its arguments just to clear things up.  We
will use \texttt{Le} aid in reading the goal, with \texttt{Le m n} as a
reminder that we to return the type corresponding to $\texttt{m} ≤
\texttt{n}$:
\begin{Verbatim}
Le [m n : Nat] : ⋆ ⇒ ⋆

le [n : Nat] : [m : Nat] → Le n m ⇒ (
  Nat-Elim n (λ n ⇒ [m : Nat] → Le n m)
    {|h1|}
    {|h2|}
)
\end{Verbatim}
\begin{Verbatim}[frame=leftline]
>>> :r le.ka
Holes:
  h1 : [m : Nat] → Le zero m
  h2 : [x : Nat] → ([m : Nat] → Le x m) → [m : Nat] → Le (suc x) m
\end{Verbatim}
This is much better!  \mykant, when printing terms, does not substitute
top-level names for their bodies, since usually the resulting term is
much clearer.  As a nice side-effect, we can use tricks like this to
find guidance.

In this case in the first case we need to return, given any number
\texttt{m}, $0 \le \texttt{m}$.  The trivial type will do, since every
number is less or equal than zero:
\begin{Verbatim}
le [n : Nat] : [m : Nat] → Le n m ⇒ (
  Nat-Elim n (λ n ⇒ [m : Nat] → Le n m)
    (λ _ ⇒ Unit)
    {|h2|}
)
\end{Verbatim}
\begin{Verbatim}[frame=leftline]
>>> :r le.ka
Holes:
  h2 : [x : Nat] → ([m : Nat] → Le x m) → [m : Nat] → Le (suc x) m
\end{Verbatim}
Now for the important case.  We are given our comparison function for a
number, and we need to produce the function for the successor.  Thus, we
need to re-apply the induction principle on the other number, \texttt{m}:
\begin{Verbatim}
le [n : Nat] : [m : Nat] → Le n m ⇒ (
  Nat-Elim n (λ n ⇒ [m : Nat] → Le n m)
    (λ _ ⇒ Unit)
    (λ n' f m ⇒ Nat-Elim m (λ m' ⇒ Le (suc n') m') {|h2|} {|h3|})
)
\end{Verbatim}
\begin{Verbatim}[frame=leftline]
>>> :r le.ka
Holes:
  h2 : ⋆
  h3 : [x : Nat] → Le (suc n') x → Le (suc n') (suc x)
\end{Verbatim}
In the first hole we know that the second number is zero, and thus we
can return empty.  In the second case, we can use the recursive argument
\texttt{f} on the two numbers:
\begin{Verbatim}
le [n : Nat] : [m : Nat] → Le n m ⇒ (
  Nat-Elim n (λ n ⇒ [m : Nat] → Le n m)
    (λ _ ⇒ Unit)
    (λ n' f m ⇒
       Nat-Elim m (λ m' ⇒ Le (suc n') m') Empty (λ f _ ⇒ f m'))
)
\end{Verbatim}
We can verify that our function works as expected:
\begin{Verbatim}[frame=leftline]
>>> :e le zero zero
Unit
>>> :e le zero (suc zero)
Unit
>>> :e le (suc (suc zero)) (suc zero)
Empty
\end{Verbatim}
Another functionality of type holes is examining types of things in
context.  Going back to the examples in Section \ref{sec:term-types}, we can
implement the safe \texttt{head} function with our newly defined
\texttt{le}:
\begin{Verbatim}
data List : [A : ⋆] → ⋆ ⇒
  { nil : List A | cons : A → List A → List A }

length [A : ⋆] [l : List A] : Nat ⇒ (
  List-Elim l (λ _ ⇒ Nat) zero (λ _ _ n ⇒ suc n)
)

gt [n m : Nat] : ⋆ ⇒ (le (suc m) n)

head [A : ⋆] [l : List A] : gt (length A l) zero → A ⇒ (
  List-Elim l (λ l ⇒ gt (length A l) zero → A)
    (λ p ⇒ {|h1 p|})
    {|h2|}
)
\end{Verbatim}
We define \texttt{List}s, a polymorphic \texttt{length} function, and
express $<$ (\texttt{gt}) in terms of $\le$.  Then, we set up the type
for our \texttt{head} function.  Given a list and a proof that its
length is greater than zero, we return the first element.  If we load
this in \mykant, we get:
\begin{Verbatim}[frame=leftline]
>>> :r le.ka
Holes:
  h1 : A
    p : Empty
  h2 : [x : A] [x1 : List A] →
       (gt (length A x1) zero → A) →
       gt (length A (cons x x1)) zero → A
\end{Verbatim}
In the first case (the one for \texttt{nil}), we have a proof of
\texttt{Empty}---surely we can use \texttt{absurd} to get rid of that
case.  In the second case we simply return the element in the
\texttt{cons}:
\begin{Verbatim}
head [A : ⋆] [l : List A] : gt (length A l) zero → A ⇒ (
  List-Elim l (λ l ⇒ gt (length A l) zero → A)
    (λ p ⇒ absurd A p)
    (λ x _ _ _ ⇒ x)
)
\end{Verbatim}
Now, if we tried to get the head of an empty list, we face a problem:
\begin{Verbatim}[frame=leftline]
>>> :t head Nat nil
Type: Empty → Nat
\end{Verbatim}
We would have to provide something of type \texttt{Empty}, which
hopefully should be impossible.  For non-empty lists, on the other hand,
things run smoothly:
\begin{Verbatim}[frame=leftline]
>>> :t head Nat (cons zero nil)
Type: Unit → Nat
>>> :e head Nat (cons zero nil) tt
zero
\end{Verbatim}
This should give a vague idea of why type holes are so useful and in
more in general about the development process in \mykant.  Most
interactive theorem provers offer some kind of facility
to... interactively develop proofs, usually much more powerful than the
fairly bare tools present in \mykant.  Agda in particular offers a
celebrated mode for the \texttt{Emacs} text editor.

\section{Future work}
\label{sec:future-work}

The first move that the author plans to make is to work towards a simple
but powerful term representation.  A good plan seems to be to associate
each type (terms, telescopes, etc.) with what we can substitute
variables with, so that the term type will be associated with itself,
while telescopes and propositions will be associated to terms.  This can
probably be accomplished elegantly with Haskell's \emph{type families}
\citep{chakravarty2005associated}.  After achieving a more solid
machinery for terms, implementing observational equality fully should
prove relatively easy.

Beyond this steps, we can go in many directions to improve the
system that we described---here we review the main ones.

\begin{description}
\item[Pattern matching and recursion] Eliminators are very clumsy,
  and using them can be especially frustrating if we are used to writing
  functions via explicit recursion.  \cite{Gimenez1995} showed how to
  reduce well-founded recursive definitions to primitive recursors.
  Intuitively, defining a function through an eliminators corresponds to
  pattern matching and recursively calling the function on the recursive
  occurrences of the type we matched against.

  Nested pattern matching can be justified by identifying a notion of
  `structurally smaller', and allowing recursive calls on all smaller
  arguments.  Epigram goes all the way and actually implements recursion
  exclusively by providing a convenient interface to the two constructs
  above \citep{EpigramTut, McBride2004}.

  However as we extend the flexibility in our recursion elaborating
  definitions to eliminators becomes more and more laborious.  For
  example we might want mutually definitions and definitions that
  terminate relying on the structure of two arguments instead of just
  one.  For this reason both Agda and Coq (Agda putting more effort) let
  the user write recursive definitions freely, and then employ an
  external syntactic check to ensure termination.

  Moreover, if we want to use dependently typed languages for
  programming purposes, we will probably want to sidestep the
  termination checker and write a possibly non-terminating function;
  maybe because proving termination is particularly difficult.  With
  explicit recursion this amounts to turning off a check, if we have
  only eliminators it is impossible.

\item[More powerful data types] A popular improvement on basic data
  types are inductive families \citep{Dybjer1991}, where the parameters
  for the type constructors can change based on the data constructors,
  which lets us express naturally types such as $\mytyc{Vec} : \mynat
  \myarr \mytyp$, which given a number returns the type of lists of that
  length, or $\mytyc{Fin} : \mynat \myarr \mytyp$, which given a number
  $n$ gives the type of numbers less than $n$.  This apparent omission
  was motivated by the fact that inductive families can be represented
  by adding equalities concerning the parameters of the type
  constructors as arguments to the data constructor, in much the same
  way that Generalised Abstract Data Types \citep{GHC} are handled in
  Haskell.  Interestingly the modified version of System F that lies at
  the core of recent versions of GHC features coercions reminiscent of
  those found in OTT, motivated by the need to implement GADTs in an
  elegant way \citep{Sulzmann2007}.

  Another concept introduced by \cite{dybjer2000general} is
  induction-recursion, where we define a data type in tandem with a
  function on that type.  This technique has proven extremely useful to
  define embeddings of other calculi in an host language, by defining
  the representation of the embedded language as a data type and at the
  same time a function decoding from the representation to a type in the
  host language.  The decoding function is then used to define the data
  type for the embedding itself, for example by reusing the host's
  language functions to describe functions in the embedded language,
  with decoded types as arguments.

  It is also worth mentioning that in recent times there has been work
  \citep{dagand2012elaborating, chapman2010gentle} to show how to define
  a set of primitives that data types can be elaborated into.  The big
  advantage of the approach proposed is enabling a very powerful notion
  of generic programming, by writing functions working on the
  `primitive' types as to be workable by all the other `compatible'
  elaborated user defined types.  This has been a considerable problem
  in the dependently type world, where we often define types which are
  more `strongly typed' version of similar structures,\footnote{For
    example the $\mytyc{OList}$ presented in Section \ref{sec:user-type}
    being a `more typed' version of an ordinary list.} and then find
  ourselves forced to redefine identical operations on both types.

\item[Pattern matching and inductive families] The notion of inductive
  family also yields a more interesting notion of pattern matching,
  since matching on an argument influences the value of the parameters
  of the type of said argument.  This means that pattern matching
  influences the context, which can be exploited to constraint the
  possible data constructors for \emph{other} arguments
  \citep{McBride2004}.

\item[Type inference] While bidirectional type checking helps at a very
  low cost of implementation and complexity, a much more powerful weapon
  is found in \emph{pattern unification}, which allows Hindley-Milner
  style inference for dependently typed languages.  Unification for
  higher order terms is undecidable and unification problems do not
  always have a most general unifier \cite{huet1973undecidability}.
  However \cite{miller1992unification} identified a decidable fragment
  of higher order unification commonly known as pattern unification,
  which is employed in most theorem provers to drastically reduce the
  number of type annotations.  \cite{gundrytutorial} provide a tutorial
  on this practice.

\item[Coinductive data types] When we specify inductive data types, we
  do it by specifying its \emph{constructors}---functions with the type
  we are defining as codomain.  Then, we are offered way of compute by
  recursively \emph{destructing} or \emph{eliminating} a member of the
  defined data type.

  Coinductive data types are the dual of this approach.  We specify ways
  to destruct data, and we are given a way to generate the defined type
  by repeatedly `unfolding' starting from some seed data.  For example,
  we could defined infinite streams by specifying a $\myfun{head}$ and
  $\myfun{tail}$ destructors---here using a syntax reminiscent of
  \mykant\ records:
  \[
  \begin{array}{@{}l}
    \mysyn{codata}\ \mytyc{Stream}\myappsp (\myb{A} {:} \mytyp)\ \mysyn{where} \\
    \myind{2} \{ \myfun{head} : \myb{A}, \myfun{tail} : \mytyc{Stream} \myappsp \myb{A}\}
  \end{array}
  \]
  which will hopefully give us something like
  \[
  \begin{array}{@{}l}
    \myfun{head} : (\myb{A}{:}\mytyp) \myarr \mytyc{Stream} \myappsp \myb{A} \myarr \myb{A} \\
    \myfun{tail} : (\myb{A}{:}\mytyp) \myarr \mytyc{Stream} \myappsp \myb{A} \myarr \mytyc{Stream} \myappsp \myb{A} \\
    \mytyc{Stream}.\mydc{unfold} : (\myb{A}\, \myb{B} {:} \mytyp) \myarr (\myb{A} \myarr \myb{B} \myprod \myb{A}) \myarr \myb{A} \myarr \mytyc{Stream} \myappsp \myb{B}
  \end{array}
  \]
  Where, in $\mydc{unfold}$, $\myb{B} \myprod \myb{A}$ represents the
  fields of $\mytyc{Stream}$ but with the recursive occurrence replaced
  by the `seed' type $\myb{A}$.

  Beyond simple infinite types like $\mytyc{Stream}$, coinduction is
  particularly useful to write non-terminating programs like servers or
  software interacting with a user, while guaranteeing their liveliness.
  Moreover it lets us model possibly non-terminating computations in an
  elegant way \citep{Capretta2005}, enabling for example the study of
  operational semantics for non-terminating languages
  \citep{Danielsson2012}.
 
  \cite{cockett1992charity} pioneered this approach in their programming
  language Charity, and coinduction has since been adopted in systems
  such as Coq \citep{Gimenez1996} and Agda.  However these
  implementations are unsatisfactory, since Coq's break subject
  reduction, and Agda does not allow types to depend on the unfolding of
  codata to avoid this problem.  \cite{mcbride2009let} has shown how
  observational equality can help to resolve these issues, since we can
  reason about the unfoldings in a better way, like we reason about
  functions' extensional behaviour.
\end{description}

The author looks forward to the study and possibly the implementation of
these ideas in the years to come.

\newpage{}

\appendix

\section{Notation and syntax}
\label{app:notation}

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

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 in derivations or meta-operations.
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 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}}
\]
I will also omit arrows to abbreviate types:
\[
(\myb{x} {:} \mytya)(\myb{y} {:} \mytyb) \myarr \cdots =
(\myb{x} {:} \mytya) \myarr (\myb{y} {:} \mytyb) \myarr \cdots
\]

Meta operations names will be displayed in $\mymeta{smallcaps}$ and
written in a pattern matching style, also making use of boolean guards.
For example, a meta operation operating on a context and terms might
look like this:
\[
\begin{array}{@{}l}
  \mymeta{quux}(\myctx, \myb{x}) \mymetaguard \myb{x} \in \myctx \mymetagoes \myctx(\myb{x}) \\
  \mymeta{quux}(\myctx, \myb{x}) \mymetagoes \mymeta{outofbounds} \\
  \myind{2} \vdots
\end{array}
\]

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

Examples of \mykant\ code will be typeset nicely with \LaTeX in Section
\ref{sec:kant-theory}, to adjust with the rest of the presentation; and
in \texttt{teletype} font in the rest of the document, including Section
\ref{sec:kant-practice} and in the appendices.  Snippets of sessions in
the \mykant\ prompt will be displayed with a left border, to distinguish
them from snippets of code:
\begin{Verbatim}[frame=leftline]
>>> :t ⋆
Type: ⋆
\end{Verbatim}

\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}
\label{app:kant-itt}

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}
\label{app:kant-examples}

{\small
\verbatiminput{examples.ka}
}

\subsection{\mykant' hierachy}
\label{app: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}
}

\subsection{Term representation}
\label{app:termrep}

Data type for terms in \mykant.

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

\subsection{Graph and constraints modules}
\label{app:constraint}

The modules are respectively named \texttt{Data.LGraph} (short for
`labelled graph'), and \texttt{Data.Constraint}.  The type class
constraints on the type parameters are not shown for clarity, unless
they are meaningful to the function.  In practice we use the
\texttt{Hashable} type class on the vertex to implement the graph
efficiently with hash maps.

\subsubsection{\texttt{Data.LGraph}}

{\small
\verbatiminput{graph.hs}
}

\subsubsection{\texttt{Data.Constraint}}

{\small
\verbatiminput{constraint.hs}
}

\newpage{}

\bibliographystyle{authordate1}
\bibliography{thesis}

\end{document}