-\documentclass[report]{article}
+%% 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}
-%% Narrow margins
-% \usepackage{fullpage}
+\usepackage[sc,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}
+
%% Bibtex
\usepackage{natbib}
%% Links
-\usepackage{hyperref}
+\usepackage[pdftex, pdfborderstyle={/S/U/W 0}]{hyperref}
%% Frames
\usepackage{framed}
%% 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}
\DeclareUnicodeCharacter{8799}{\ensuremath{\stackrel{?}{=}}}
\DeclareUnicodeCharacter{9655}{\ensuremath{\rhd}}
+\renewenvironment{code}%
+{\noindent\ignorespaces\advance\leftskip\mathindent\AgdaCodeStyle\pboxed\small}%
+{\endpboxed\par\noindent%
+\ignorespacesafterend\small}
+
%% -----------------------------------------------------------------------------
%% Commands
+\newcommand{\mysmall}{}
\newcommand{\mysyn}{\AgdaKeyword}
-\newcommand{\mytyc}{\AgdaDatatype}
-\newcommand{\mydc}{\AgdaInductiveConstructor}
-\newcommand{\myfld}{\AgdaField}
-\newcommand{\myfun}{\AgdaFunction}
-% TODO make this use AgdaBound
-\newcommand{\myb}[1]{\AgdaBound{#1}}
+\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}{\textsc{Kant}}
+\newcommand{\mykant}{\textmd{\textsc{Bertus}}}
\newcommand{\mysynel}[1]{#1}
\newcommand{\myse}{\mysynel}
\newcommand{\mytmsyn}{\mysynel{term}}
\newcommand{\mysp}{\ }
-% TODO \mathbin or \mathre here?
\newcommand{\myabs}[2]{\mydc{$\lambda$} #1 \mathrel{\mydc{$\mapsto$}} #2}
\newcommand{\myappsp}{\hspace{0.07cm}}
\newcommand{\myapp}[2]{#1 \myappsp #2}
\newcommand{\mysynsep}{\ \ |\ \ }
+\newcommand{\myITE}[3]{\myfun{If}\, #1\, \myfun{Then}\, #2\, \myfun{Else}\, #3}
+\newcommand{\mycumul}{\preceq}
\FrameSep0.2cm
\newcommand{\mydesc}[3]{
\noindent
\mbox{
\parbox{\textwidth}{
- {\small
- \vspace{0.3cm}
- \hfill \textbf{#1} $#2$
-
+ {\mysmall
+ \vspace{0.2cm}
+ \hfill \textup{\textbf{#1}} $#2$
\framebox[\textwidth]{
\parbox{\textwidth}{
\vspace{0.1cm}
- #3
- \vspace{0.1cm}
+ \centering{
+ #3
+ }
+ \vspace{0.2cm}
}
}
+ \vspace{0.2cm}
}
}
}
}
-% TODO is \mathbin the correct thing for arrow and times?
-
\newcommand{\mytmt}{\mysynel{t}}
\newcommand{\mytmm}{\mysynel{m}}
\newcommand{\mytmn}{\mysynel{n}}
\newcommand{\myred}{\leadsto}
-\newcommand{\mysub}[3]{#1[#2 / #3]}
+\newcommand{\mysub}[3]{#1[#3 / #2]}
\newcommand{\mytysyn}{\mysynel{type}}
\newcommand{\mybasetys}{K}
-% TODO change this name
\newcommand{\mybasety}[1]{B_{#1}}
\newcommand{\mytya}{\myse{A}}
\newcommand{\mytyb}{\myse{B}}
\newcommand{\myvalid}[1]{#1 \vdash \underline{\mathrm{valid}}}
\newcommand{\myjudd}[3]{#1 \vdash #2 : #3}
\newcommand{\myjud}[2]{\myjudd{\myctx}{#1}{#2}}
-% TODO \mathbin or \mathrel here?
\newcommand{\myabss}[3]{\mydc{$\lambda$} #1 {:} #2 \mathrel{\mydc{$\mapsto$}} #3}
\newcommand{\mytt}{\mydc{$\langle\rangle$}}
\newcommand{\myunit}{\mytyc{Unit}}
\newcommand{\myfst}{\myfld{fst}}
\newcommand{\mysnd}{\myfld{snd}}
\newcommand{\myconst}{\myse{c}}
-\newcommand{\myemptyctx}{\cdot}
+\newcommand{\myemptyctx}{\varepsilon}
\newcommand{\myhole}{\AgdaHole}
\newcommand{\myfix}[3]{\mysyn{fix} \myappsp #1 {:} #2 \mapsto #3}
\newcommand{\mysum}{\mathbin{\textcolor{AgdaDatatype}{+}}}
\newcommand{\mycase}[2]{\mathopen{\myfun{[}}#1\mathpunct{\myfun{,}} #2 \mathclose{\myfun{]}}}
\newcommand{\myabsurd}[1]{\myfun{absurd}_{#1}}
\newcommand{\myarg}{\_}
-\newcommand{\myderivsp}{\vspace{0.3cm}}
+\newcommand{\myderivsp}{}
+\newcommand{\myderivspp}{\vspace{0.3cm}}
\newcommand{\mytyp}{\mytyc{Type}}
\newcommand{\myneg}{\myfun{$\neg$}}
\newcommand{\myar}{\,}
\newcommand{\mycons}{\mathbin{\mydc{∷}}}
\newcommand{\myfoldr}{\myfun{foldr}}
\newcommand{\myw}[3]{\myapp{\myapp{\mytyc{W}}{(#1 {:} #2)}}{#3}}
-\newcommand{\mynode}[2]{\mathbin{\mydc{$\lhd$}_{#1.#2}}}
+\newcommand{\mynodee}{\mathbin{\mydc{$\lhd$}}}
+\newcommand{\mynode}[2]{\mynodee_{#1.#2}}
\newcommand{\myrec}[4]{\myfun{rec}\,#1 / {#2.#3}\,\myfun{with}\,#4}
\newcommand{\mylub}{\sqcup}
\newcommand{\mydefeq}{\cong}
\newcommand{\myrefl}{\mydc{refl}}
-\newcommand{\mypeq}[1]{\mathrel{\mytyc{=}_{#1}}}
-\newcommand{\myjeqq}{\myfun{=-elim}}
+\newcommand{\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]{\llbracket #1 \rrbracket}
-\newcommand{\myand}{\wedge}
-\newcommand{\myprfora}[3]{\forall #1 {:} #2. #3}
-\newcommand{\mybot}{\bot}
-\newcommand{\mytop}{\top}
+\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) = (#3 {:} #4)}
+\newcommand{\myjm}[4]{(#1 {:} #2) \mathrel{\mytyc{=}} (#3 {:} #4)}
+\newcommand{\myeq}{\mathrel{\mytyc{=}}}
\newcommand{\myprop}{\mytyc{Prop}}
\newcommand{\mytmup}{\mytmsyn\uparrow}
\newcommand{\mydefs}{\Delta}
\newcommand{\mynf}{\Downarrow}
-\newcommand{\myinff}[3]{#1 \vdash #2 \Rightarrow #3}
+\newcommand{\myinff}[3]{#1 \vdash #2 \Uparrow #3}
\newcommand{\myinf}[2]{\myinff{\myctx}{#1}{#2}}
-\newcommand{\mychkk}[3]{#1 \vdash #2 \Leftarrow #3}
+\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{postulate}\ #1 : #2}
-\newcommand{\myadt}[4]{\mysyn{data}\ #1 : #2 \myarr \mytyp\ \mysyn{where}\ #3\{ #4 \}}
-\newcommand{\myreco}[4]{\mysyn{record}\ #1 : #2 \myarr \mytyp\ \mysyn{where}\ #3\ \{ #4 \}}
-% TODO change vdash
+\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{\mymeta}{\textsc}
\newcommand{\myhyps}{\mymeta{hyps}}
\newcommand{\mycc}{;}
-\newcommand{\myemptytele}{\cdot}
+\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}
%% -----------------------------------------------------------------------------
\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}
-\iffalse
-\begin{code}
-module thesis where
-\end{code}
-\fi
+\begin{titlepage}
+\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}
+\end{titlepage}
-\maketitle
+\pagenumbering{gobble}
+
+\newpage{}
+\mbox{}
+\newpage{}
+
+\thispagestyle{empty}
\begin{abstract}
- The marriage between programming and logic has been a very fertile one. In
- particular, since the simply typed lambda calculus (STLC), a number of type
- systems have been devised with increasing expressive power.
-
- Section \ref{sec:types} will give a very brief overview of STLC, and then
- illustrate how it can be interpreted as a natural deduction system. Section
- \ref{sec:itt} will introduce Inutitionistic Type Theory (ITT), which expands
- on this concept, employing a more expressive logic. The exposition is quite
- dense since there is a lot of material to cover; for a more complete treatment
- of the material the reader can refer to \citep{Thompson1991, Pierce2002}.
- Section \ref{sec:equality} will explain why equality has always been a tricky
- business in these theories, and talk about the various attempts that have been
- made to make the situation better. One interesting development has recently
- emerged: Observational Type theory.
-
- Section \ref{sec:practical} will describe common extensions found in the
- systems currently in use. Finally, section \ref{sec:kant} will describe a
- system developed by the author that implements a core calculus based on the
- principles described.
+ The marriage between programming and logic has been a very 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, Inutitionistic Type Theory (ITT) has been a very
+ 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 will 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.
+ Nost 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
+\newpage{}
+\mbox{}
+\newpage{}
+
+\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}
+
+\newpage{}
+\mbox{}
+\newpage{}
+
+\thispagestyle{empty}
\tableofcontents
\clearpage
+\pagenumbering{arabic}
+
+\section{Introduction}
+
+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 it 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 a very active transfer of techniques and
+knowledge between logic and programming language theory, in both
+directions.
+
+Mathematics could provide programming with a huge 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
+wealth of approaches to effectively collaborate with computers, through
+the study of programming languages.
+
+We will 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
+probably the most prominent instance of the proposition-as-types and
+proofs-as-programs discipline. 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 in the field of equality 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
+(for example 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 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 mechanism that make it work.
+
+Section \ref{sec:kant-theory} will describe \mykant, a system we have
+developed incorporating OTT along constructs usually present in modern
+theorem provers. Along the way, we describe these additional features
+and their advantages. 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 Section \ref{sec:future-work}
+will give a roadmap to bring \mykant\ on par and beyond the
+competition.
+
+\subsection{Contribution}
+
+The goal 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}
+
\section{Simple and not-so-simple types}
\label{sec:types}
\subsection{The untyped $\lambda$-calculus}
-
-Along with Turing's machines, the earliest attempts to formalise computation
-lead to the $\lambda$-calculus \citep{Church1936}. This early programming
-language encodes computation with a minimal syntax and no `data' in the
-traditional sense, but just functions. Here we give a brief overview of the
-language, which will give the chance to introduce concepts central to the
-analysis of all the following calculi. The exposition follows the one found in
-chapter 5 of \cite{Queinnec2003}.
-
-The syntax of $\lambda$-terms consists of three things: variables, abstractions,
-and applications:
-
+\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}
$
}
-Parenthesis will be omitted in the usual way:
-$\myapp{\myapp{\mytmt}{\mytmm}}{\mytmn} =
-\myapp{(\myapp{\mytmt}{\mytmm})}{\mytmn}$.
+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:
+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{, where} \\
- \myind{1}
+ \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{, with } \myb{x} \neq y \\
+ \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{1} \text{with $\myb{x} \neq \myb{y}$ and $\myb{z}$ not free in $\myapp{\mytmm}{\mytmn}$}}
+ \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 required to avoid
-name capturing. We will use substitution in the future for other name-binding
-constructs assuming similar precautions.
+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 are of remarkable expressiveness, and in fact Turing
-complete. As a corollary, we must be able to devise a term that reduces forever
-(`loops' in imperative terms):
+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}}$}
\]
-
-A \emph{redex} is a term that can be reduced. In the untyped $\lambda$-calculus
-this will be the case for an application in which the first term is an
-abstraction, but in general we call aterm reducible if it appears to the left of
-a reduction rule. When a term contains no redexes it's said to be in
-\emph{normal form}. Given the observation above, not all terms reduce to a
-normal forms: we call the ones that do \emph{normalising}, and the ones that
-don't \emph{non-normalising}.
-
-The reduction rule presented is not syntax directed, but \emph{evaluation
- strategies} can be employed to reduce term systematically. Common evaluation
-strategies include \emph{call by value} (or \emph{strict}), where arguments of
-abstractions are reduced before being applied to the abstraction; and conversely
-\emph{call by name} (or \emph{lazy}), where we reduce only when we need to do so
-to proceed---in other words when we have an application where the function is
-still not a $\lambda$. In both these reduction strategies we never reduce under
-an abstraction: for this reason a weaker form of normalisation is used, where
-both abstractions and normal forms are said to be in \emph{weak head normal
- form}.
+\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 aterm 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 be have the \emph{normalisation property}, or
+ to be 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 both abstractions and normal forms are said
+to be in \emph{weak head normal form}.
\subsection{The simply typed $\lambda$-calculus}
A convenient way to `discipline' and reason about $\lambda$-terms is to assign
\emph{types} to them, and then check that the terms that we are forming make
-sense given our typing rules \citep{Curry1934}. The first most basic instance
-of this idea takes the name of \emph{simply typed $\lambda$ calculus}, whose
-rules are shown in figure \ref{fig:stlc}.
-
-Our types contain a set of \emph{type variables} $\Phi$, which might correspond
-to some `primitive' types; and $\myarr$, the type former for `arrow' types, the
-types of functions. The language is explicitly typed: when we bring a variable
-into scope with an abstraction, we explicitly declare its type. $\mytya$,
-$\mytyb$, $\mytycc$, will be used to refer to a generic type. Reduction is
-unchanged from the untyped $\lambda$-calculus.
+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}{ }{
}
\mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
- \centering{
\begin{tabular}{ccc}
\AxiomC{$\myctx(x) = A$}
\UnaryInfC{$\myjud{\myb{x}}{A}$}
\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.}
In the typing rules, a context $\myctx$ is used to store the types of bound
variables: $\myctx; \myb{x} : \mytya$ adds a variable to the context and
-$\myctx(x)$ returns the type of the rightmost occurrence of $x$.
+$\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{description}
-\item[Progress] A well-typed term is not stuck---it is either a variable, or its
- constructor does not appear on the left of the $\myred$ relation (currently
+\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 (currently
only $\lambda$), or it can take a step according to the evaluation rules.
-\item[Preservation] If a well-typed term takes a step of evaluation, then the
- resulting term is also well-typed, and preserves the previous type. Also
- known as \emph{subject reduction}.
-\end{description}
+\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 can't fill the blanks if we want to
+\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:
-\begin{equation*}
+\[
\myapp{(\myabss{\myb{x}}{\myhole{?}}{\myapp{\myb{x}}{\myb{x}}})}{(\myabss{\myb{x}}{\myhole{?}}{\myapp{\myb{x}}{\myb{x}}})}
-\end{equation*}
-
+\]
This makes the STLC Turing incomplete. We can recover the ability to loop by
adding a combinator that recurses:
-
+\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.4cm}
+ \vspace{0.5cm}
}
\end{minipage}
\begin{minipage}{0.5\textwidth}
\mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}} {
- \centering{
\AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytmt}{\mytya}$}
\UnaryInfC{$\myjud{\myfix{\myb{x}}{\mytya}{\mytmt}}{\mytya}$}
\DisplayProof
- }
}
\end{minipage}
-
+\mynegder
\mydesc{reduction:}{\myjud{\mytmsyn}{\mytmsyn}}{
- \centering{
$ \myfix{\myb{x}}{\mytya}{\mytmt} \myred \mysub{\mytmt}{\myb{x}}{(\myfix{\myb{x}}{\mytya}{\mytmt})}$
- }
}
This will deprive us of normalisation, which is a particularly bad thing if we
want to use the STLC as described in the next section.
+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 unique normal form for definitional equality
+to be decidable.
+
\subsection{The Curry-Howard correspondence}
-It turns out that the STLC can be seen a natural deduction system for
-intuitionistic propositional logic. Terms are proofs, and their types are the
-propositions they prove. This remarkable fact is known as the Curry-Howard
+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
\[
\myabss{\myb{f}}{(\mytya \myarr \mytyb)}{\myabss{\myb{g}}{(\mytyb \myarr \mytycc)}{\myabss{\myb{x}}{\mytya}{\myapp{\myb{g}}{(\myapp{\myb{f}}{\myb{x}})}}}}
\]
-That is, function composition. Going beyond arrow types, we can extend our bare
-lambda calculus with useful types to represent other logical constructs, as
-shown in figure \ref{fig:natded}.
+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{extendend simply typed $\lambda$-calculus}.
+\end{mydef}
\begin{figure}[t]
\mydesc{syntax}{ }{
}
\mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
- \centering{
\begin{tabular}{cc}
$
\begin{array}{l@{ }l@{\ }c@{\ }l}
\end{array}
$
\end{tabular}
- }
}
\mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
- \centering{
\begin{tabular}{cc}
\AxiomC{\phantom{$\myjud{\mytmt}{\myempty}$}}
\UnaryInfC{$\myjud{\mytt}{\myunit}$}
\UnaryInfC{$\myjud{\myapp{\myabsurd{\mytya}}{\mytmt}}{\mytya}$}
\DisplayProof
\end{tabular}
- }
- \myderivsp
- \centering{
+
+ \myderivspp
+
\begin{tabular}{cc}
\AxiomC{$\myjud{\mytmt}{\mytya}$}
\UnaryInfC{$\myjud{\myapp{\myleft{\mytyb}}{\mytmt}}{\mytya \mysum \mytyb}$}
\DisplayProof
\end{tabular}
- }
- \myderivsp
- \centering{
+
+ \myderivspp
+
\begin{tabular}{cc}
\AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$}
\AxiomC{$\myjud{\mytmn}{\mytya \myarr \mytycc}$}
\TrinaryInfC{$\myjud{\myapp{\mycase{\mytmm}{\mytmn}}{\mytmt}}{\mytycc}$}
\DisplayProof
\end{tabular}
- }
- \myderivsp
- \centering{
+
+ \myderivspp
+
\begin{tabular}{ccc}
\AxiomC{$\myjud{\mytmm}{\mytya}$}
\AxiomC{$\myjud{\mytmn}{\mytyb}$}
\UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mytyb}$}
\DisplayProof
\end{tabular}
- }
}
\caption{Rules for the extendend STLC. Only the new features are shown, all the
rules and syntax for the STLC apply here too.}
\label{fig:natded}
\end{figure}
-Tagged unions (or sums, or coproducts---$\mysum$ here, \texttt{Either} in
-Haskell) correspond to disjunctions, and dually tuples (or pairs, or
-products---$\myprod$ here, tuples in Haskell) correspond to conjunctions. This
-is apparent looking at the ways to construct and destruct the values inhabiting
-those types: for $\mysum$ $\myleft{ }$ and $\myright{ }$ correspond to $\vee$
-introduction, and $\mycase{\_}{\_}$ to $\vee$ elimination; for $\myprod$
-$\mypair{\_}{\_}$ corresponds to $\wedge$ introduction, $\myfst$ and $\mysnd$ to
-$\wedge$ elimination.
-
-The trivial type $\myunit$ corresponds to the logical $\top$, and dually
-$\myempty$ corresponds to the logical $\bot$. $\myunit$ has one introduction
-rule ($\mytt$), and thus one inhabitant; and no eliminators. $\myempty$ has no
-introduction rules, and thus no inhabitants; and one eliminator ($\myabsurd{
-}$), corresponding to the logical \emph{ex falso quodlibet}. Note that in the
-constructors for the sums and the destructor for $\myempty$ we need to include
-some type information to keep type checking decidable.
+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. $\myneg \mytya$ can be expressed as $\mytya
-\myarr \myempty$. However, there is an important omission: there is no term of
+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's no coincidence, since there
+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.
-Theories of this kind are called \emph{intuitionistic}, or \emph{constructive},
+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.}.
+the foundation of the STLC.\footnote{There is research to give computational
+ behaviour to classical logic, but I will not touch those subjects.}
As in logic, if we want to keep our system consistent, we must make sure that no
closed terms (in other words terms not under a $\lambda$) inhabit $\myempty$.
The variant of STLC presented here is indeed
consistent, a result that follows from the fact that it is
-normalising. % TODO explain
+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
-\]
+\[(\myfix{\myb{x}}{\mytya}{\myb{x}}) : \mytya\]
\subsection{Inductive data}
+\label{sec:ind-data}
To make the STLC more useful as a programming language or reasoning tool it is
common to include (or let the user define) inductive data types. These comprise
of a type former, various constructors, and an eliminator (or destructor) that
serves as primitive recursor.
-For example, we might add a $\mylist$ type constructor, along with an `empty
+\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$). See figure
+lists will be the usual folding operation ($\myfoldr$). Full rules in Figure
\ref{fig:list}.
-
+\end{mydef}
+\mynegder
\begin{figure}[h]
\mydesc{syntax}{ }{
$
$
}
\mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
- \centering{
$
\begin{array}{l@{\ }c@{\ }l}
\myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{\mynil{\mytya}} & \myred & \mytmt \\
\end{array}
$
}
-}
\mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
- \centering{
\begin{tabular}{cc}
\AxiomC{\phantom{$\myjud{\mytmm}{\mytya}$}}
\UnaryInfC{$\myjud{\mynil{\mytya}}{\myapp{\mylist}{\mytya}}$}
\BinaryInfC{$\myjud{\mytmm \mycons \mytmn}{\myapp{\mylist}{\mytya}}$}
\DisplayProof
\end{tabular}
- }
- \myderivsp
- \centering{
+ \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. %TODO does this make sense to have here?
+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}
The STLC can be made more expressive in various ways. \cite{Barendregt1991}
succinctly expressed geometrically how we can add expressivity:
-
$$
\xymatrix@!0@=1.5cm{
& \lambda\omega \ar@{-}[rr]\ar@{-}'[d][dd]
\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:
+ 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}
+ (\myabss{\myb{A}}{\mytyp}{\myabss{\myb{x}}{\myb{A}}{\myb{x}}}) : (\myb{A} {:} \mytyp) \myarr \myb{A} \myarr \myb{A}
\]
- The first and most famous instance of this idea has been System F. This form
- of polymorphism and has been wildly successful, also thanks to a well known
- inference algorithm for a restricted version of System F known as
- Hindley-Milner. Languages like Haskell and SML are based on this discipline.
+ 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\]
+ 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:
\subsection{A Bit of History}
-Logic frameworks and programming languages based on type theory have a long
-history. Per Martin-L\"{o}f described the first version of his theory in 1971,
-but then revised it since the original version was inconsistent due to its
-impredicativity\footnote{In the early version there was only one universe
- $\mytyp$ and $\mytyp : \mytyp$, see section \ref{sec:term-types} for an
- explanation on why this causes problems.}. For this reason he gave a revised
-and consistent definition later \citep{Martin-Lof1984}.
+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
include Agda \citep{Norell2007, Bove2009}, Coq \citep{Coq}, and Epigram
\citep{McBride2004, EpigramTut}.
-\subsection{A note on inference}
-
-% TODO do this, adding links to the sections about bidi type checking and
-% implicit universes.
-In the following text I will often omit explicit typing for abstractions or
-
-Moreover, I will use $\mytyp$ without bothering to specify a
-universe, with the silent assumption that the definition is consistent
-regarding to the hierarchy.
-
\subsection{A simple type theory}
\label{sec:core-tt}
-The calculus I present follows the exposition in \citep{Thompson1991}, and is
-quite close to the original formulation of predicative ITT as found in
-\citep{Martin-Lof1984}. The system's syntax and reduction rules are presented
-in their entirety in figure \ref{fig:core-tt-syn}. The typing rules are
-presented piece by piece. An Agda rendition of the presented theory is
-reproduced in appendix \ref{app:agda-code}.
+The calculus I present follows the exposition in \citep{Thompson1991},
+and is quite close to the original formulation of predicative ITT as
+found in \citep{Martin-Lof1984}.
+\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}
+Agda and \mykant\ renditions of the presented theory and all the
+examples is reproduced in Appendix \ref{app:itt-code}.
\begin{figure}[t]
\mydesc{syntax}{ }{
$
\begin{array}{r@{\ }c@{\ }l}
\mytmsyn & ::= & \myb{x} \mysynsep
- \mytyp_{l} \mysynsep
+ \mytyp_{level} \mysynsep
\myunit \mysynsep \mytt \mysynsep
\myempty \mysynsep \myapp{\myabsurd{\mytmsyn}}{\mytmsyn} \\
& | & \mybool \mysynsep \mytrue \mysynsep \myfalse \mysynsep
& | & \myw{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
\mytmsyn \mynode{\myb{x}}{\mytmsyn} \mytmsyn \\
& | & \myrec{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn} \\
- l & \in & \mathbb{N}
+ level & \in & \mathbb{N}
\end{array}
$
}
\mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
- \centering{
- \begin{tabular}{cc}
+ \begin{tabular}{ccc}
$
\begin{array}{l@{ }l@{\ }c@{\ }l}
\myitee{\mytrue &}{\myb{x}}{\myse{P}}{\mytmm}{\mytmn} & \myred & \mytmm \\
$
\myapp{(\myabss{\myb{x}}{\mytya}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{\myb{x}}{\mytmn}
$
- \myderivsp
- \end{tabular}
+ &
$
\begin{array}{l@{ }l@{\ }c@{\ }l}
\myapp{\myfst &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmm \\
\myapp{\mysnd &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmn
\end{array}
$
- \myderivsp
+ \end{tabular}
+
+ \myderivspp
$
\myrec{(\myse{s} \mynode{\myb{x}}{\myse{T}} \myse{f})}{\myb{y}}{\myse{P}}{\myse{p}} \myred
\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}
\label{sec:term-types}
\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
- \centering{
\begin{tabular}{cc}
\AxiomC{$\myjud{\mytmt}{\mytya}$}
\AxiomC{$\mytya \mydefeq \mytyb$}
\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
\[
\myabss{\myb{x}}{\mytya}{\myb{x}} \mydefeq \myabss{\myb{y}}{\mytya}{\myb{y}}
\]
-Types that are definitionally equal can be used interchangeably. Here the
-`conversion' rule is not syntax directed, however we will see how it is
-possible to employ $\myred$ to decide term equality in a systematic
-way. % TODO add section
-Another thing to notice is that considering the need to reduce terms to decide
-equality, it is essential for a dependently type system to be terminating and
-confluent for type checking to be decidable.
-
-Moreover, we specify a \emph{type hierarchy} to talk about `large' types:
-$\mytyp_0$ will be the type of types inhabited by data: $\mybool$, $\mynat$,
-$\mylist$, etc. $\mytyp_1$ will be the type of $\mytyp_0$, and so on---for
-example we have $\mytrue : \mybool : \mytyp_0 : \mytyp_1 : \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}. Moreover, various techniques
-can be employed to lift the burden of explicitly handling universes.
-% TODO add sectioon about universes
+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 it is essential for a dependently typed system to be
+terminating and confluent for type checking to be decidable, since every
+type needs to have a \emph{unique} normal form.
+
+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}}{
- \centering{
\begin{tabular}{cc}
\AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
\UnaryInfC{$\myvalid{\myemptyctx}$}
\UnaryInfC{$\myvalid{\myctx ; \myb{x} : \mytya}$}
\DisplayProof
\end{tabular}
- }
}
\end{minipage}
\begin{minipage}{0.5\textwidth}
\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
- \centering{
\AxiomC{$\myctx(x) = \mytya$}
\UnaryInfC{$\myjud{\myb{x}}{\mytya}$}
\DisplayProof
- }
}
\end{minipage}
\vspace{0.1cm}
\subsubsection{$\myunit$, $\myempty$}
\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
- \centering{
\begin{tabular}{ccc}
\AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
\UnaryInfC{$\myjud{\myunit}{\mytyp_0}$}
\UnaryInfC{\phantom{$\myjud{\myempty}{\mytyp_0}$}}
\DisplayProof
\end{tabular}
- }
}
Nothing surprising here: $\myunit$ and $\myempty$ are unchanged from the STLC,
\subsubsection{$\mybool$, and dependent $\myfun{if}$}
\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
- \centering{
\begin{tabular}{ccc}
\AxiomC{}
\UnaryInfC{$\myjud{\mybool}{\mytyp_0}$}
\UnaryInfC{$\myjud{\myfalse}{\mybool}$}
\DisplayProof
\end{tabular}
- \myderivsp
+ \myderivspp
\AxiomC{$\myjud{\mytmt}{\mybool}$}
\AxiomC{$\myjudd{\myctx : \mybool}{\mytya}{\mytyp_l}$}
\BinaryInfC{$\myjud{\mytmm}{\mysub{\mytya}{x}{\mytrue}}$ \hspace{0.7cm} $\myjud{\mytmn}{\mysub{\mytya}{x}{\myfalse}}$}
\UnaryInfC{$\myjud{\myitee{\mytmt}{\myb{x}}{\mytya}{\mytmm}{\mytmn}}{\mysub{\mytya}{\myb{x}}{\mytmt}}$}
\DisplayProof
-
- }
}
-With booleans we get the first taste of `dependent' in `dependent types'. While
-the two introduction rules ($\mytrue$ and $\myfalse$) are not surprising, the
-typing rules for $\myfun{if}$ are. In most strongly typed languages we expect
-the branches of an $\myfun{if}$ statements to be of the same type, to preserve
-subject reduction, since execution could take both paths. This is a pity, since
-the type system does not reflect the fact that in each branch we gain knowledge
-on the term we are branching on. Which means that programs along the lines of
-\begin{verbatim}
+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.
+\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
the updated knowledge on the value of $\myb{x}$.
\subsubsection{$\myarr$, or dependent function}
+\label{sec:depprod}
\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
- \centering{
\AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
\AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
\BinaryInfC{$\myjud{\myfora{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
\DisplayProof
- \myderivsp
+ \myderivspp
\begin{tabular}{cc}
\AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytmt}{\mytyb}$}
\BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mysub{\mytyb}{\myb{x}}{\mytmn}}$}
\DisplayProof
\end{tabular}
- }
}
Dependent functions are one of the two key features that perhaps most
characterise dependent types---the other being dependent products. With
-dependent functions, the result type can depend on the value of the argument.
-This feature, together with the fact that the result type might be a type
-itself, brings a lot of interesting possibilities. Keeping the correspondence
-with logic alive, dependent functions are much like universal quantifiers
-($\forall$) in logic.
-
-Again, we need to make sure that the type hierarchy is respected, which is the
-reason why a type formed by $\myarr$ will live in the least upper bound of the
-levels of argument and return type. This trend will continue with the other
-type-level binders, $\myprod$ and $\mytyc{W}$.
+dependent functions, the result type can depend on the value of the
+argument. This feature, together with the fact that the result type
+might be a type itself, brings a lot of interesting possibilities.
+Following this intuition, in the introduction rule, the return type is
+typechecked in a context with an abstracted variable of lhs' type, and
+in the elimination rule the actual argument is substituted in the return
+type. Keeping the correspondence with logic alive, dependent functions
+are much like universal quantifiers ($\forall$) in logic.
+
+For example, assuming that we have lists and natural numbers in our
+language, using dependent functions we 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}
+\]
-% TODO maybe examples?
+\myfun{length} is the usual polymorphic length
+function. $\myarg\myfun{$>$}\myarg$ is a function that takes two naturals
+and returns a type: if the lhs is greater then the rhs, $\myunit$ is
+returned, $\myempty$ otherwise. This way, we can express a
+`non-emptyness' condition in $\myfun{head}$, by including a proof that
+the length of the list argument is non-zero. This allows us to rule out
+the `empty list' case, so that we can safely return the first element.
+
+% TODO fix this
+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. If this was not the
+case, we would be able to form a `powerset' function along the lines of
+\[
+\begin{array}{@{}l}
+\myfun{P} : \mytyp_0 \myarr \mytyp_0 \\
+\myfun{P} \myappsp \myb{A} \mapsto \myb{A} \myarr \mytyp_0
+\end{array}
+\]
+Where the type of $\myb{A} \myarr \mytyp_0$ is in $\mytyp_0$ itself.
+Using this and similar devices we would be able to derive falsity
+\citep{Hurkens1995}. This trend will continue with the other type-level
+binders, $\myprod$ and $\mytyc{W}$.
\subsubsection{$\myprod$, or dependent product}
-
+\label{sec:disju}
\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
- \centering{
\AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
\AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
\BinaryInfC{$\myjud{\myexi{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
\DisplayProof
- \myderivsp
+ \myderivspp
\begin{tabular}{cc}
\AxiomC{$\myjud{\mytmm}{\mytya}$}
\UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mysub{\mytyb}{\myb{x}}{\myapp{\myfst}{\mytmt}}}$}
\DisplayProof
\end{tabular}
-
- }
}
+If dependent functions are a generalisation of $\myarr$ in the STLC,
+dependent products are a generalisation of $\myprod$ in the STLC. The
+improvement is that the second element's type can depend on the value of
+the first element. The corrispondence with logic is through the
+existential quantifier: $\exists x \in \mathbb{N}. even(x)$ can be
+expressed as $\myexi{\myb{x}}{\mynat}{\myapp{\myfun{even}}{\myb{x}}}$.
+The first element will be a number, and the second evidence that the
+number is even. This highlights the fact that we are working in a
+constructive logic: if we have an existence proof, we can always ask for
+a witness. This means, for instance, that $\neg \forall \neg$ is not
+equivalent to $\exists$.
+
+Another perhaps more `dependent' application of products, paired with
+$\mybool$, is to offer choice between different types. For example we
+can easily recover disjunctions:
+\[
+\begin{array}{l}
+ \myarg\myfun{$\vee$}\myarg : \mytyp_0 \myarr \mytyp_0 \myarr \mytyp_0 \\
+ \myb{A} \mathrel{\myfun{$\vee$}} \myb{B} \mapsto \myexi{\myb{x}}{\mybool}{\myite{\myb{x}}{\myb{A}}{\myb{B}}} \\ \ \\
+ \myfun{case} : (\myb{A}\ \myb{B}\ \myb{C} {:} \mytyp_0) \myarr (\myb{A} \myarr \myb{C}) \myarr (\myb{B} \myarr \myb{C}) \myarr \myb{A} \mathrel{\myfun{$\vee$}} \myb{B} \myarr \myb{C} \\
+ \myfun{case} \myappsp \myb{A} \myappsp \myb{B} \myappsp \myb{C} \myappsp \myb{f} \myappsp \myb{g} \myappsp \myb{x} \mapsto \\
+ \myind{2} \myapp{(\myitee{\myapp{\myfst}{\myb{x}}}{\myb{b}}{(\myite{\myb{b}}{\myb{A}}{\myb{B}})}{\myb{f}}{\myb{g}})}{(\myapp{\mysnd}{\myb{x}})}
+\end{array}
+\]
\subsubsection{$\mytyc{W}$, or well-order}
\label{sec:well-order}
\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
- \centering{
+ \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
- \myderivsp
+ &
\AxiomC{$\myjud{\mytmt}{\mytya}$}
\AxiomC{$\myjud{\mysynel{f}}{\mysub{\mytyb}{\myb{x}}{\mytmt} \myarr \myw{\myb{x}}{\mytya}{\mytyb}}$}
\BinaryInfC{$\myjud{\mytmt \mynode{\myb{x}}{\mytyb} \myse{f}}{\myw{\myb{x}}{\mytya}{\mytyb}}$}
\DisplayProof
+ \end{tabular}
- \myderivsp
+ \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}$}
}$}
\UnaryInfC{$\myjud{\myrec{\myse{u}}{\myb{w}}{\myse{P}}{\myse{p}}}{\mysub{\myse{P}}{\myb{w}}{\myse{u}}}$}
\DisplayProof
- }
}
+Finally, the well-order type, or in short $\mytyc{W}$-type, which will
+let us represent inductive data in a general (but clumsy) way. We can
+form `nodes' of the shape $\mytmt \mynode{\myb{x}}{\mytyb} \myse{f} :
+\myw{\myb{x}}{\mytya}{\mytyb}$ that contain data ($\mytmt$) of type and
+one `child' for each member of $\mysub{\mytyb}{\myb{x}}{\mytmt}$. The
+$\myfun{rec}\ \myfun{with}$ acts as an induction principle on
+$\mytyc{W}$, given a predicate 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 present deeper
+ problems because the notion of equality present in most type theory
+ (which we will present in the next section) is too weak
+ \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 datatypes 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}
-In the previous section we saw how a type checker (or a human) needs a notion of
-\emph{definitional equality}. Beyond this meta-theoretic notion, in this
-section we will explore the ways of expressing equality \emph{inside} the
-theory, as a reasoning tool available to the user. This area is the main
-concern of this thesis, and in general a very active research topic, since we do
-not have a fully satisfactory solution, yet.
+In the previous section we saw how a type checker (or a human) needs a
+notion of \emph{definitional equality}. Beyond this meta-theoretic
+notion, in this section we will explore the ways of expressing equality
+\emph{inside} the theory, as a reasoning tool available to the user.
+This area is the main concern of this thesis, and in general a very
+active research topic, since we do not have a fully satisfactory
+solution, yet. As in the previous section, everything presented is
+formalised in Agda in Appendix \ref{app:agda-itt}.
\subsection{Propositional equality}
+\begin{mydef}[Propositional equality] The syntax, reduction, and typing
+ rules for propositional equality and related constructs is defined as:
+\end{mydef}
+\mynegder
\noindent
\begin{minipage}{0.5\textwidth}
\mydesc{syntax}{ }{
$
\begin{array}{r@{\ }c@{\ }l}
\mytmsyn & ::= & \cdots \\
- & | & \mytmsyn \mypeq{\mytmsyn} \mytmsyn \mysynsep
+ & | & \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}{
- \centering{
$
\myjeq{\myse{P}}{(\myapp{\myrefl}{\mytmm})}{\mytmn} \myred \mytmn
$
- }
- \vspace{0.9cm}
+ \vspace{1.1cm}
}
\end{minipage}
-
+\mynegder
\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
- \centering{
\AxiomC{$\myjud{\mytya}{\mytyp_l}$}
\AxiomC{$\myjud{\mytmm}{\mytya}$}
\AxiomC{$\myjud{\mytmn}{\mytya}$}
- \TrinaryInfC{$\myjud{\mytmm \mypeq{\mytya} \mytmn}{\mytyp_l}$}
+ \TrinaryInfC{$\myjud{\mypeq \myappsp \mytya \myappsp \mytmm \myappsp \mytmn}{\mytyp_l}$}
\DisplayProof
- \myderivsp
+ \myderivspp
\begin{tabular}{cc}
- \AxiomC{\phantom{$\myctx P \mytyp_l$}}
- \noLine
- \UnaryInfC{$\myjud{\mytmt}{\mytya}$}
- \UnaryInfC{$\myjud{\myapp{\myrefl}{\mytmt}}{\mytmt \mypeq{\mytya} \mytmt}$}
+ \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{$\myjud{\myse{P}}{\myfora{\myb{x}\ \myb{y}}{\mytya}{\myfora{q}{\myb{x} \mypeq{\mytya} \myb{y}}{\mytyp_l}}}$}
- \noLine
- \UnaryInfC{$\myjud{\myse{q}}{\mytmm \mypeq{\mytya} \mytmn}\hspace{1.2cm}\myjud{\myse{p}}{\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmm}}{(\myapp{\myrefl}{\mytmm})}}$}
+ \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 the equality construction to be a type-former. Here we present what
-has survived as the dominating form of equality in systems based on ITT up to
-the present day.
+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 to the
+present day.
-Our type former is $\mypeq{\mytya}$, which given a type (in this case
-$\mytya$) relates equal terms of that type. $\mypeq{}$ has one introduction
+Our type former is $\mypeq$, which given a type (in this case
+$\mytya$) relates equal terms of that type. $\mypeq$ has one introduction
rule, $\myrefl$, which introduces an equality relation between definitionally
-equal terms---in the typing rule we display the term as `the same', meaning
-`the same up to $\mydefeq$'. % TODO maybe mention this earlier
+equal terms.
-Finally, we have one eliminator for $\mypeq{}$, $\myjeqq$. $\myjeq{\myse{P}}{\myse{q}}{\myse{p}}$ takes
+Finally, we have one eliminator for $\mypeq$, $\myjeqq$. $\myjeq{\myse{P}}{\myse{q}}{\myse{p}}$ takes
\begin{itemize}
\item $\myse{P}$, a predicate working with two terms of a certain type (say
- $\mytya$) and a proof of their equality
+ $\mytya$) and a proof of their equality;
\item $\myse{q}$, a proof that two terms in $\mytya$ (say $\myse{m}$ and
- $\myse{n}$) are equal
-\item and $\myse{p}$, an inhabitant of $\myse{P}$ applied to $\myse{m}$, plus
- the trivial proof by reflexivity showing that $\myse{m}$ is equal to itself
+ $\myse{n}$) are equal;
+\item and $\myse{p}$, an inhabitant of $\myse{P}$ applied to $\myse{m}$
+ twice, plus the trivial proof by reflexivity showing that $\myse{m}$
+ is equal to itself.
\end{itemize}
-Given these ingredients, $\myjeqq$ retuns a member of $\myse{P}$ applied to
-$\mytmm$, $\mytmn$, and $\myse{q}$. In other words $\myjeqq$ takes a
-witness that $\myse{P}$ works with \emph{definitionally equal} terms, and
-returns a witness of $\myse{P}$ working with \emph{propositionally equal}
-terms. Invokations of $\myjeqq$ will vanish when the equality proofs will
-reduce to invocations to reflexivity, at which point the arguments must be
-definitionally equal, and thus the provided
+Given these ingredients, $\myjeqq$ retuns a member of $\myse{P}$ applied
+to $\mytmm$, $\mytmn$, and $\myse{q}$. In other words $\myjeqq$ takes a
+witness that $\myse{P}$ works with \emph{definitionally equal} terms,
+and returns a witness of $\myse{P}$ working with \emph{propositionally
+ equal} terms. Invokations of $\myjeqq$ will vanish when the equality
+proofs will reduce to invocations to reflexivity, at which point the
+arguments must be definitionally equal, and thus the provided
$\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmm}}{(\myapp{\myrefl}{\mytmm})}$
-can be returned.
+can be returned. This means that $\myjeqq$ will not compute with
+hypotetical proofs, which makes sense given that they might be false.
-While the $\myjeqq$ rule is slightly convoluted, ve can derive many more
+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}
-(\myabs{\myb{A}\ \myb{P}\ \myb{x}\ \myb{y}\ \myb{q}\ \myb{p}}{
- \myjeq{(\myabs{\myb{x}\ \myb{y}\ \myb{q}}{\myapp{\myb{P}}{\myb{y}}})}{\myb{q}}{\myb{p}}}) : \\
-\myind{1} \myfora{\myb{A}}{\mytyp}{\myfora{\myb{P}}{\myb{A} \myarr \mytyp}{\myfora{\myb{x}\ \myb{y}}{\myb{A}}{\myb{x} \mypeq{\myb{A}} \myb{y} \myarr \myapp{\myb{P}}{\myb{x}} \myarr \myapp{\myb{P}}{\myb{y}}}}}
+\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}
\]
-This rule is often called $\myfun{subst}$---here we will invoke it without
-specifying the type ($\myb{A}$) and the sides of the equality
-($\myb{x},\myb{y}$).
-
Once we have $\myfun{subst}$, we can easily prove more familiar laws regarding
-equality, such as symmetry, transitivity, and a congruence law:
-
-% TODO finish this
+equality, such as symmetry, transitivity, congruence laws, etc.
\subsection{Common extensions}
-eta law
+Our definitional and propositional equalities can be enhanced in various
+ways. Obviously if we extend the definitional equality we are also
+automatically extend propositional equality, given how $\myrefl$ works.
+
+\subsubsection{$\eta$-expansion}
+\label{sec:eta-expand}
+
+A simple extension to our definitional equality is $\eta$-expansion.
+Given an abstract variable $\myb{f} : \mytya \myarr \mytyb$ the aim is
+to have that $\myb{f} \mydefeq
+\myabss{\myb{x}}{\mytya}{\myapp{\myb{f}}{\myb{x}}}$. We can achieve
+this by `expanding' terms based on their types, a process also known as
+\emph{quotation}---a term borrowed from the practice of
+\emph{normalisation by evaluation}, where we embed terms in some host
+language with an existing notion of computation, and then reify them
+back into terms, which will `smooth out' differences like the one above
+\citep{Abel2007}.
+
+The same concept applies to $\myprod$, where we expand each inhabitant
+by reconstructing it by getting its projections, so that $\myb{x}
+\mydefeq \mypair{\myfst \myappsp \myb{x}}{\mysnd \myappsp \myb{x}}$.
+Similarly, all one inhabitants of $\myunit$ and all zero inhabitants of
+$\myempty$ can be considered equal. Quotation can be performed in a
+type-directed way, as we will witness in Section \ref{sec:kant-irr}.
+
+\begin{mydef}[Congruence and $\eta$-laws]
+To justify quotation in our type system we will add a congruence law
+for abstractions and a similar law for products, plus the fact that all
+elements of $\myunit$ or $\myempty$ are equal.
+\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}
-congruence
+Another common but controversial addition to propositional equality is
+the $\myfun{K}$ axiom, which essentially states that all equality proofs
+are by reflexivity.
-UIP
+\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 the
+$\myjeqq$ axiom that we presented, and \cite{McBride2004} showed that it is
+needed to implement `dependent pattern matching', as first proposed by
+\cite{Coquand1992}. Thus, $\myfun{K}$ is derivable in the systems that
+implement dependent pattern matching, such as Epigram and Agda; but for
+example not in Coq.
+
+$\myfun{K}$ is controversial mainly because it is at odds with
+equalities that include computational behaviour, most notably
+Voevodsky's `Univalent Foundations', which includes a \emph{univalence}
+axiom that identifies isomorphisms between types with propositional
+equality. For example we would have two isomorphisms, and thus two
+equalities, between $\mybool$ and $\mybool$, corresponding to the two
+permutations---one is the identity, and one swaps the elements. Given
+this, $\myfun{K}$ and univalence are inconsistent, and thus a form of
+dependent pattern matching that does not imply $\myfun{K}$ is subject of
+research.\footnote{More information about univalence can be found at
+ \url{http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations.html}.}
\subsection{Limitations}
\epigraph{\emph{Half of my time spent doing research involves thinking up clever
schemes to avoid needing functional extensionality.}}{@larrytheliquid}
-However, propositional equality as described is quite restricted when
+Propositional equality as described is quite restricted when
reasoning about equality beyond the term structure, which is what definitional
-equality gives us (extension notwithstanding).
+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
\[
\myfun{ext} : \myfora{\myb{A}\ \myb{B}}{\mytyp}{\myfora{\myb{f}\ \myb{g}}{
\myb{A} \myarr \myb{B}}{
- (\myfora{\myb{x}}{\myb{A}}{\myapp{\myb{f}}{\myb{x}} \mypeq{\myb{B}} \myapp{\myb{g}}{\myb{x}}}) \myarr
- \myb{f} \mypeq{\myb{A} \myarr \myb{B}} \myb{g}
+ (\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 denotationally the same, and we can in fact prove that
+\[\myabs{\myb{x}}{0 \mathrel{\myfun{$+$}} \myb{x}}$ and $\myabs{\myb{x}}{\myb{x} \mathrel{\myfun{$+$}} 0}\]
+where $\myfun{$+$}$ is defined by recursion on the first argument,
+gradually destructing it to build up successors of the second argument.
+The two functions are clearly extensionally equal, and we can in fact
+prove that
\[
-\myfora{\myb{x}}{\mynat}{(0 \mathrel{\myfun{+}} \myb{x}) \mypeq{\mynat} (\myb{x} \mathrel{\myfun{+}} 0)}
+\myfora{\myb{x}}{\mynat}{\mypeq \myappsp \mynat \myappsp (0 \mathrel{\myfun{$+$}} \myb{x}) \myappsp (\myb{x} \mathrel{\myfun{$+$}} 0)}
\]
By analysis on the $\myb{x}$. However, the two functions are not
definitionally equal, and thus we won't be able to get rid of the
quantification.
-For the reasons above, theories that offer a propositional equality similar to
-what we presented are called \emph{intensional}, as opposed to
-\emph{extensional}. Most systems in wide use today (such as Agda, Coq and
-Epigram) are of this kind.
+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 to execute. It
also extends to other fields, for example proving bisimulation between
processes specified by coinduction, or in general proving equivalences based
-on the behaviour on a term.
+on the behaviour of a term.
\subsection{Equality reflection}
One way to `solve' this problem is by identifying propositional equality with
-definitional equality:
+definitional equality.
+\begin{mydef}[Equality reflection]\end{mydef}
\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
- \centering{
\AxiomC{$\myjud{\myse{q}}{\mytmm \mypeq{\mytya} \mytmn}$}
\UnaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\mytya}$}
\DisplayProof
- }
}
-This rule takes the name of \emph{equality reflection}, and is a very
-different rule from the ones we saw up to now: it links a typing judgement
-internal to the type theory to a meta-theoretic judgement that the type
-checker uses to work with terms. It is easy to see the dangerous consequences
-that this causes:
+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 syntax directed, and the type checker is presumably expected
- to come up with equality proofs when needed.
+\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.
- Consider for example
+ 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.
+
+ For example, assuming that we are in a context that contains
\[
- \myabss{\myb{q}}{\mytya \mypeq{\mytyp} (\mytya \myarr \mytya)}{\myhole{?}}
+ \myb{A} : \mytyp; \myb{q} : \mypeq \myappsp \mytyp
+ \myappsp (\mytya \myarr \mytya) \myappsp \mytya
\]
- Using the assumed proof in tandem with equality reflection we could easily
- write a classic Y combinator, sending the compiler into a loop.
+ we can write a looping term similar to the one we saw in Section
+ \ref{sec:untyped}:
+ % TODO dot this
\end{itemize}
Given these facts theories employing equality reflection, like NuPRL
\citep{NuPRL}, carry the derivations that gave rise to each typing judgement
-to keep the systems manageable. % TODO more info, problems with that.
+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}
- \AxiomC{$\myjudd{\myctx; \myb{x} : \myb{A}}{\myapp{\myb{q}}{\myb{x}}}{\myapp{\myb{f}}{\myb{x}} \mypeq{} \myapp{\myb{g}}{\myb{x}}}$}
+ \mysmall
+ \AxiomC{$\hspace{1.1cm}\myjudd{\myctx; \myb{x} : \myb{A}}{\myapp{\myb{q}}{\myb{x}}}{\myapp{\myb{f}}{\myb{x}} \mypeq{} \myapp{\myb{g}}{\myb{x}}}\hspace{1.1cm}$}
\RightLabel{equality reflection}
\UnaryInfC{$\myjudd{\myctx; \myb{x} : \myb{A}}{\myapp{\myb{f}}{\myb{x}} \mydefeq \myapp{\myb{g}}{\myb{x}}}{\myb{B}}$}
\RightLabel{congruence for $\lambda$s}
\UnaryInfC{$\myjud{(\myabs{\myb{x}}{\myapp{\myb{f}}{\myb{x}}}) \mydefeq (\myabs{\myb{x}}{\myapp{\myb{g}}{\myb{x}}})}{\myb{A} \myarr \myb{B}}$}
\RightLabel{$\eta$-law for $\lambda$}
- \UnaryInfC{$\myjud{\myb{f} \mydefeq \myb{g}}{\myb{A} \myarr \myb{B}}$}
+ \UnaryInfC{$\hspace{1.45cm}\myjud{\myb{f} \mydefeq \myb{g}}{\myb{A} \myarr \myb{B}}\hspace{1.45cm}$}
\RightLabel{$\myrefl$}
\UnaryInfC{$\myjud{\myapp{\myrefl}{\myb{f}}}{\myb{f} \mypeq{} \myb{g}}$}
\end{prooftree}
Now, the question is: do we need to give up well-behavedness of our theory to
gain extensionality?
-\subsection{Observational equality}
+\section{The observational approach}
\label{sec:ott}
-% TODO should we explain this in detail?
-A recent development by \citet{Altenkirch2007}, \emph{Observational Type
- Theory} (OTT), promises to keep the well behavedness of ITT while being able
-to gain many useful equality proofs\footnote{It is suspected that OTT gains
- \emph{all} the equality proofs of ETT, but no proof exists yet.}, including
-function extensionality. The main idea is to give the user the possibility to
-\emph{coerce} (or transport) values from a type $\mytya$ to a type $\mytyb$,
-if the type checker can prove structurally that $\mytya$ and $\mytya$ are
-equal; and providing a value-level equality based on similar principles. A
-brief overview is given below,
+% TODO add \begin{mydef}s
+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}{r@{\ }c@{\ }l}
- \mytmsyn & ::= & \cdots \\
- & | & \myprdec{\myprsyn} \mysynsep
- \mycoee{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \mysynsep
- \mycohh{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
- \myprsyn & ::= & \mybot \mysynsep \mytop \mysynsep \myprsyn \myand \myprsyn
- \mysynsep \myprfora{\myb{x}}{\mytmsyn}{\myprsyn} \\\
- & | & \mytmsyn = \mytmsyn \mysynsep
- \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn}
+ \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}}{
- \centering{
- }
+ \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}
}
-The original presentation of OTT employs the theory presented above. It is
-close to the one presented in section \ref{sec:itt}, with the additions
-presented above, and the change that only one the `first' universe, the type
-of small types ($\mytyp_0$), is present.
+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.
+
+\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}
+ $
+}
-The propositional universe is meant to be where equality proofs live in. The
-equality proofs are respectively between types ($\mytya = \mytyb$), and
-between values
+\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
-However, only one universe is present ($\mytyp_0$), and a \emph{propositional}
-universe is isolated, intended to be the universe where equality proofs live
-in. Propositions (as long as our system is consistent) are inhabited only by
-one element, and thus can all be treated as definitionally equal.
+ \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 repleaceable for one another with no additional
+changes. Note that this is not the same as saying that they are
+definitionally equal, since as we saw extensionally equal functions,
+while satisfying the above requirement, are not.
+
+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]
+ \emph{Canonical} types are those arising from the ground types
+ ($\myempty$, $\myunit$, $\mybool$) and the three type formers
+ ($\myarr$, $\myprod$, $\mytyc{W}$). \emph{Neutral} types are those
+ formed by $\myfun{If}\myarg\myfun{Then}\myarg\myfun{Else}\myarg$.
+ Correspondingly, canonical terms are those inhabiting data
+ constructors ($\mytt$, $\mytrue$, $\myfalse$,
+ $\myabss{\myb{x}}{\mytya}{\mytmt}$, ...); all the others being
+ neutral, including eliminators and abstracted variables.
+\end{mydef}
+
+In the current system (and hopefully in well-behaved systems), all
+closed terms reduce to a canonical term (as a consequence or
+normalisation), and all canonical types are inhabited by canonical
+terms (a property known as \emph{canonicity}).
+
+\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 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}$.
-% \section{Augmenting ITT}
-% \label{sec:practical}
+\begin{figure}[t]
-% \subsection{A more liberal hierarchy}
+\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}
-% \subsection{Type inference}
+\begin{mydef}[Type equalities reduction, and \myfun{coe}rcions] Figure
+ \ref{fig:eqred} illustrates the rules to reduce equalities and to
+ coerce terms.
+\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, things
+are similar but subtly different---the choices we make in the type
+equality are dictated by the desire of writing the $\myfun{coe}$ in a
+natural way.
+
+$\myprod$ is the easiest case: we decompose the proof into proofs that
+the first element's types are equal ($\mytya_1 \myeq \mytya_2$), and a
+proof that given equal values in the first element, the types of the
+second elements are equal too
+($\myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{\myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2}}
+ \myimpl \mytyb_1[\myb{x_1}] \myeq \mytyb_2[\myb{x_2}]}$).\footnote{We
+ are using $\myimpl$ to indicate a $\forall$ where we discard the first
+ value. We write $\mytyb_1[\myb{x_1}]$ to indicate that the
+ $\myb{x_1}$ in $\mytyb_1$ is re-bound to the $\myb{x_1}$ quantified by
+ the $\forall$, and similarly for $\myb{x_2}$ and $\mytyb_2$.} This
+also explains the need for heterogeneous equality, since in the second
+proof 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 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:
-% \subsubsection{Bidirectional type checking}
+\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
+ \AxiomC{$\myjud{\mytmt}{\mytya}$}
+ \UnaryInfC{$\myjud{\myapp{\myrefl}{\mytmt}}{\myprdec{\myjm{\mytmt}{\mytya}{\mytmt}{\mytya}}}$}
+ \DisplayProof
-% \subsubsection{Pattern unification}
+ \myderivspp
-% \subsection{Pattern matching and explicit fixpoints}
+ \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
+}
-% \subsection{Induction-recursion}
+$\myrefl$ is the equivalent of the reflexivity rule in propositional
+equality, and $\mytyc{R}$ asserts that if we have a we have a $\mytyp$
+abstracting over a value we can substitute equal for equal---this lets
+us recover $\myfun{subst}$. Note that while we need to provide ad-hoc
+rules in the restricted, non-hierarchical theory that we have, if our
+theory supports abstraction over $\mytyp$s we can easily add these
+axioms as abstracted variables.
-% \subsection{Coinduction}
+\subsubsection{Value-level equality}
-% \subsection{Dealing with partiality}
+\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}
+ $
+}
-% \subsection{Type holes}
+As with type-level equality, we want value-level equality to reduce
+based on the structure of the compared terms. When matching
+propositional data, such as $\myempty$ and $\myunit$, we automatically
+return the trivial type, since if a type has zero one members, all
+members will be equal. When matching on data-bearing types, such as
+$\mybool$, we check that such data matches, and return bottom otherwise.
+
+\subsection{Proof irrelevance and stuck coercions}
+\label{sec:ott-quot}
+
+The last effort is required to make sure that proofs (members of
+$\myprop$) are \emph{irrelevant}. Since they are devoid of
+computational content, we would like to identify all equivalent
+propositions as the same, in a similar way as we identified all
+$\myempty$ and all $\myunit$ as the same in section
+\ref{sec:eta-expand}.
+
+Thus we will have a quotation that will not only perform
+$\eta$-expansion, but will also identify and mark proofs that could not
+be decoded (that is, equalities on neutral types). Then, when
+comparing terms, marked proofs will be considered equal without
+analysing their contents, thus gaining irrelevance.
+
+Moreover we can safely advance `stuck' $\myfun{coe}$rcions between
+non-canonical but definitionally equal types. Consider for example
+\[
+\mycoee{(\myITE{\myb{b}}{\mynat}{\mybool})}{(\myITE{\myb{b}}{\mynat}{\mybool})}{\myb{x}}
+\]
+Where $\myb{b}$ and $\myb{x}$ are abstracted variables. This
+$\myfun{coe}$ will not advance, since the types are not canonical.
+However they are definitionally equal, and thus we can safely remove the
+coerce and return $\myb{x}$ as it is.
-\section{\mykant : the theory}
+\section{\mykant: the theory}
\label{sec:kant-theory}
\mykant\ is an interactive theorem prover developed as part of this thesis.
the basis for a more featureful system, while still presenting interesting
features and more importantly observational equality.
-The author learnt the hard way the implementations challenges for such a
-project, and while there is a solid and working base to work on, observational
-equality is not currently implemented. However, a detailed plan on how to add
-it this functionality is provided, and should not prove to be too much work.
+We will first present the features of the system, and then describe the
+implementation we have developed in Section \ref{sec:kant-practice}.
-The features currently implemented in \mykant\ are:
+The defining features of \mykant\ are:
\begin{description}
\item[Full dependent types] As we would expect, we have dependent a system
which is as expressive as the `best' corner in the lambda cube described in
- section \ref{sec:itt}.
+ Section \ref{sec:itt}.
\item[Implicit, cumulative universe hierarchy] The user does not need to
specify universe level explicitly, and universes are \emph{cumulative}.
with associated primitive recursion operators; or records, with associated
projections for each field.
-\item[Bidirectional type checking] While no `fancy' inference via unification
- is present, we take advantage of an type synthesis system in the style of
- \cite{Pierce2000}, extending the concept for user defined data types.
-
-\item[Type holes] When building up programs interactively, it is useful to
- leave parts unfinished while exploring the current context. This is what
- type holes are for.
-\end{description}
-
-The planned features are:
+\item[Bidirectional type checking] While no `fancy' inference via
+ unification is present, we take advantage of a type synthesis system
+ in the style of \cite{Pierce2000}, extending the concept for user
+ defined data types.
-\begin{description}
-\item[Observational equality] As described in section \ref{sec:ott} but
+\item[Observational equality] As described in Section \ref{sec:ott} but
extended to work with the type hierarchy and to admit equality between
arbitrary data types.
-\item[Coinductive data] ...
+\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. We do not describe holes rigorously, but
+ provide more information about them in Section \ref{sec:type-holes}.
+
\end{description}
-We will analyse the features one by one, along with motivations and tradeoffs
-for the design decisions made.
+We will analyse the features one by one, along with motivations and
+tradeoffs for the design decisions made.
\subsection{Bidirectional type checking}
-We start by describing bidirectional type checking since it calls for fairly
-different typing rules that what we have seen up to now. The idea is to have
-two kind of terms: terms for which a type can always be inferred, and terms
-that need to be checked against a type. A nice observation is that this
-duality runs through the semantics of the terms: data destructors (function
-application, record projections, primitive re cursors) \emph{infer} types,
-while data constructors (abstractions, record/data types data constructors)
-need to be checked. In the literature these terms are respectively known as
+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}.
-
-% TODO do this --- is it even necessary
-
-% \subsubsection{Declarations and contexts}
+bidirectional style. The presentation follows \cite{Loh2010}. The
+syntax for our bidirectional STLC is the same as the untyped
+$\lambda$-calculus, but with an extra construct to annotate terms
+explicitly---this will be necessary when having top-level canonical
+terms. The types are the same as those found in the normal STLC.
+
+\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 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}
-% A \mykant declaration can be one of 4 kinds:
+ \myderivspp
-% \begin{description}
-% \item[Value] A declared variable, together with a type and a body.
-% \item[Postulate] An abstract variable, with a type but no body.
-% \item[Inductive data] A datatype, with a type constructor and various data
-% constructors---somewhat similar to what we find in Haskell. A primitive
-% recursor (or `destructor') will be generated automatically.
-% \item[Record] A record, which consists of one data constructor and various
-% fields, with no recursive occurrences. We will explain the need for records
-% later.
-% \end{description}
+ \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}
+}
-% The syntax of
+For example, if we wanted to type function composition (in this case for
+naturals), we would have to annotate the term:
+\[
+ \myfun{comp} \mapsto (\myabs{\myb{f}\, \myb{g}\, \myb{x}}{\myb{f}\myappsp(\myb{g}\myappsp\myb{x})}) : (\mynat \myarr \mynat) \myarr (\mynat \myarr \mynat) \myarr \mynat \myarr \mynat
+\]
+But we would not have to annotate functions passed to it, since the type would be propagated to the arguments:
+\[
+ \myfun{comp}\myappsp (\myabs{\myb{x}}{\myb{x} \mathrel{\myfun{$+$}} 3}) \myappsp (\myabs{\myb{x}}{\myb{x} \mathrel{\myfun{$*$}} 4}) \myappsp 42
+\]
\subsection{Base terms and types}
-Let us begin by describing the primitives available without the user defining
-any data types, and without equality. The syntax given here is the one of the
-core (`desugared') terms, and 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.
-
+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
- \myabss{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
- (\myapp{\mytmsyn}{\mytmsyn}) \mysynsep
- (\myann{\mytmsyn}{\mytmsyn}) \\
+ & | & \myfora{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
+ \myabs{\myb{x}}{\mytmsyn} \mysynsep
+ (\myapp{\mytmsyn}{\mytmsyn}) \mysynsep
+ (\myann{\mytmsyn}{\mytmsyn}) \\
\mynamesyn & ::= & \myb{x} \mysynsep \myfun{f}
\end{array}
$
}
-The syntax for our calculus includes just two basic constructs: abstractions
-and $\mytyp$s. Everything else will be provided by user-definable constructs.
-Since we let the user define values, we will need a context capable of
-carrying the body of variables along with their type. We also want to make
-sure not to have duplicate top names, so we enforce that.
-
-% \mytyc{D} \mysynsep \mytyc{D}.\mydc{c}
-% \mysynsep \mytyc{D}.\myfun{f} \mysynsep
-
+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}}{
- \centering{
\begin{tabular}{ccc}
\AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
\UnaryInfC{$\myvalid{\myemptyctx}$}
\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 functional application ($\beta$-reduction), but also a rule to replace
-names with their bodies, if in the context ($\delta$-reduction), and one to
-discard type annotations. For this reason the new reduction rules are
-dependent on the context:
+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}{
- \centering{
\begin{tabular}{ccc}
\AxiomC{\phantom{$\myb{x} \mapsto \mytmt : \mytya \in \myctx$}}
\UnaryInfC{$\myctx \vdash \myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn}
\UnaryInfC{$\myctx \vdash \myann{\mytmm}{\mytya} \myred \mytmm$}
\DisplayProof
\end{tabular}
- }
}
-We want to define a \emph{weak head normal form} (WHNF) for our terms, to give
-a syntax directed presentation of type rules with no `conversion' rule. We
-will consider all \emph{canonical} forms (abstractions and data constructors)
-to be in weak head normal form... % TODO finish
-
-We can now give types to our terms. Using our definition of WHNF, I will use
-$\mytmm \mynf \mytmn$ to indicate that $\mytmm$'s normal form is $\mytmn$.
-This way, we can avoid the non syntax-directed conversion rule, giving a more
-algorithmic presentation of type checking.
+We can now give types to our terms. Although we include the usual
+conversion rule, we defer a detailed account of definitional equality to
+Section \ref{sec:kant-irr}.
-\mydesc{typing:}{\myctx \vdash \mytmsyn \Leftrightarrow \mytysyn}{
- \centering{
- \begin{tabular}{ccc}
- \AxiomC{$\myb{x} : A \in \myctx$ or $\myb{x} \mapsto \mytmt : A \in \myctx$}
- \UnaryInfC{$\myinf{\myb{x}}{A}$}
+\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}
- \myderivsp
- \AxiomC{$\myinf{\mytmm}{\mytya}$}
- \AxiomC{$\myctx \vdash \mytya \mynf \myfora{\myb{x}}{\mytyb}{\myse{C}}$}
- \AxiomC{$\mychk{\mytmn}{\mytyb}$}
- \TrinaryInfC{$\myinf{\myapp{\mytmm}{\mytmn}}{\mysub{\myse{C}}{\myb{x}}{\mytmn}}$}
- \DisplayProof
+ \myderivspp
- \myderivsp
+ \begin{tabular}{cc}
- \AxiomC{$\myctx \vdash \mytya \mynf \myfora{\myb{x}}{\mytyb}{\myse{C}}$}
- \AxiomC{$\mychkk{\myctx; \myb{x}: \mytyb}{\mytmt}{\myse{C}}$}
- \BinaryInfC{$\mychk{\myabs{\myb{x}}{\mytmt}}{\mytya}$}
+ \AxiomC{\phantom{$\mychkk{\myctx; \myb{x}: \mytya}{\mytmt}{\mytyb}$}}
+ \UnaryInfC{$\myinf{\mytyp}{\mytyp}$}
+ \DisplayProof
+ &
+ \AxiomC{$\myinf{\mytya}{\mytyp}$}
+ \AxiomC{$\myinff{\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 de Bruijn called \emph{telescopes}
+\citep{Bruijn91}, 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}}{\mytelesyn}{}{\mydc{c} : \mytelesyn\ |\ \cdots } \\
- & | & \myreco{\mytyc{D}}{\mytelesyn}{}{\myfun{f} : \mytmsyn,\ \cdots } \\
+ & | & \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)
+ \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 consists of one data constructor
+ and various \emph{fields}, with no recursive occurrences. The
+ functions extracting the fields' values from an instance of a record
+ are called \emph{projections}.
+\end{description}
-\subsubsection{Values and postulated variables}
+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}}{
- \centering{
\begin{tabular}{cc}
- \AxiomC{$\myjud{\mytmt}{\mytya}$}
+ \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{$\myjud{\mytya}{\mytyp}$}
+ \AxiomC{$\mychk{\mytya}{\mytyp}$}
\AxiomC{$\myfun{f} \not\in \myctx$}
\BinaryInfC{
$
\DisplayProof
\end{tabular}
}
-}
\subsubsection{User defined types}
+\label{sec:user-type}
-\mydesc{syntax}{ }{
- $
- \begin{array}{l}
- \mynamesyn ::= \cdots \mysynsep \mytyc{D} \mysynsep \mytyc{D}.\mydc{c} \mysynsep \mytyc{D}.\myfun{f}
+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 lookup 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{n_2}}{
+ \mytyc{Lift}.\myfun{elim} \myappsp \myb{l_2} \myappsp (\myabs{\myarg}{\mytyp}) \myappsp \myempty \myappsp (\myabs{\myb{n_2}}{\myfun{le} \myappsp \myb{n_1} \myappsp \myb{n_2}}) \myappsp \myunit
+ }) \\
+ \myind{2}\myind{2} (\myabs{\myb{n_1}\, \myb{n_2}}{
+ \mytyc{Lift}.\myfun{elim} \myappsp \myb{l_2} \myappsp (\myabs{\myarg}{\mytyp}) \myappsp \myempty \myappsp (\myabs{\myarg}{\myempty}) \myappsp \myunit
+ })
+ \end{array}
+ \]
+ Finally, we can defined a type of ordered lists. The type is
+ parametrised over two values representing the lower and upper bounds
+ of the elements, as opposed to the type parameters that we are used
+ to. Then, an empty list will have to have evidence that the bounds
+ are ordered, and each time we add an element we require the list to
+ have a matching lower bound:
+ \[
+ \begin{array}{@{}l}
+ \myadt{\mytyc{OList}}{\myappsp (\myb{low}\ \myb{upp} {:} \mytyc{Lift})}{\\ \myind{2}}{
+ \mydc{nil} \myappsp (\myfun{le'} \myappsp \myb{low} \myappsp \myb{upp}) \mydcsep \mydc{cons} \myappsp (\myb{n} {:} \mynat) \myappsp (\mytyc{OList} \myappsp (\myfun{lift} \myappsp \myb{n}) \myappsp \myb{upp}) \myappsp (\myfun{le'} \myappsp \myb{low} \myappsp (\myfun{lift} \myappsp \myb{n})
+ }
+ \end{array}
+ \]
+ 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
+ datatype with one constructor and `projections' to extract specific
+ fields of the said constructor.
+
+ For example, we can recover dependent products:
+ \[
+ \begin{array}{@{}l}
+ \myreco{\mytyc{Prod}}{\myappsp (\myb{A} {:} \mytyp) \myappsp (\myb{B} {:} \myb{A} \myarr \mytyp)}{\\ \myind{2}}{\myfst : \myb{A}, \mysnd : \myapp{\myb{B}}{\myb{fst}}}
+ \end{array}
+ \]
+ Here $\myfst$ and $\mysnd$ are the projections, with their respective
+ types. Note that each field can refer to the preceding fields---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}
+ $
+ }
-\subsubsection{Data types}
+ \mynegder
-\begin{figure}[t]
- \mydesc{syntax elaboration:}{\myelab{\mydeclsyn}{\mytmsyn ::= \cdots}}{
- \centering{
+ \mydesc{syntax elaboration:}{\mydeclsyn \myelabf \mytmsyn ::= \cdots}{
+ \footnotesize
$
- \begin{array}{r@{\ }c@{\ }l}
- \myctx & \myelabt & \myadt{\mytyc{D}}{\mytele}{}{\cdots\ |\ \mydc{c}_n : \myvec{(\myb{x} {:} \mytya)} \ |\ \cdots } \\
- & \myelabf &
+ \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}}{\myvec{\mytmsyn}} \mysynsep
- \mytyc{D}.\mydc{c}_n \myappsp \myvec{\mytmsyn} \mysynsep \cdots \mysynsep \mytyc{D}.\myfun{elim} \myappsp \mytmsyn \\
+ \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}}{
- \centering{
- \AxiomC{$\myinf{\mytele \myarr \mytyp}{\mytyp}$}
- \AxiomC{$\mytyc{D} \not\in \myctx$}
- \noLine
- \BinaryInfC{$\myinff{\myctx;\ \mytyc{D} : \mytele \myarr \mytyp}{\mytele \mycc \mytele_i \myarr \myapp{\mytyc{D}}{\mytelee}}{\mytyp}\ \ \ (1 \leq i \leq n)$}
- \noLine
- \UnaryInfC{For each $(\myb{x} {:} \mytya)$ in each $\mytele_i$, if $\mytyc{D} \in \mytya$, then $\mytya = \myapp{\mytyc{D}}{\vec{\mytmt}}$.}
+ \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}{}{ \mydc{c} : \mytele_1 \ |\ \cdots \ |\ \mydc{c}_n : \mytele_n } \\
+ \myctx & \myelabt & \myadt{\mytyc{D}}{\mytele}{}{ \cdots \ |\ \mydc{c}_n : \mytele_n } \\
& & \vspace{-0.2cm} \\
- & \myelabf & \myctx;\ \mytyc{D} : \mytele \mycc \mytyp;\ \mytyc{D}.\mydc{c}_1 : \mytele \mycc \mytele_1 \myarr \myapp{\mytyc{D}}{\mytelee};\ \cdots;\ \mytyc{D}.\mydc{c}_n : \mytele \mycc \mytele_n \myarr \myapp{\mytyc{D}}{\mytelee}; \\
+ & \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}
- (\mytele_1 \mycc \myhyps(\myb{P}, \mytele_1) \myarr \myapp{\myb{P}}{(\myapp{\mytyc{D}.\mydc{c}_1}{\mytelee_1})}) \myarr \\
\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} \\
- \\
- \multicolumn{3}{l}{
+ \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}
- }
- \end{array}
- $}
- \DisplayProof
- }
+ $
+
}
- \mydesc{reduction elaboration:}{\myctx \vdash \mytmsyn \myred \mytmsyn}{
- \centering{
+ \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{$
- \begin{array}{c}
- \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)} \\ \\
+ \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{t}}); \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{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}
\end{array}
- $}
- \DisplayProof
- }
+ $
}
- \caption{Elaborations for data types.}
- \label{fig:elab-adt}
-\end{figure}
-
-
-\subsubsection{Records}
+ \mynegder
-\begin{figure}[t]
-\mydesc{syntax elaboration:}{\myelab{\mydeclsyn}{\mytmsyn ::= \cdots}}{
- \centering{
+ \mydesc{syntax elaboration:}{\myelab{\mydeclsyn}{\mytmsyn ::= \cdots}}{
+ \footnotesize
$
\begin{array}{r@{\ }c@{\ }l}
- \myctx & \myelabt & \myadt{\mytyc{D}}{\mytele}{}{\cdots\ |\ \mydc{c}_n : \myvec{(\myb{x} {:} \mytya)} \ |\ \cdots } \\
+ \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}}{\myvec{\mytmsyn}} \mysynsep
- \mytyc{D}.\mydc{c}_n \myappsp \myvec{\mytmsyn} \mysynsep \cdots \mysynsep \mytyc{D}.\myfun{elim} \myappsp \mytmsyn \\
+ \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}}{
- \centering{
- \AxiomC{$\myinf{\mytele \myarr \mytyp}{\mytyp}$}
- \AxiomC{$\mytyc{D} \not\in \myctx$}
- \noLine
- \BinaryInfC{$\myinff{\myctx; \mytele; (\myb{f}_j : \myse{F}_j)_{j=1}^{i - 1}}{F_i}{\mytyp} \myind{3} (1 \le i \le n)$}
+ \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}{}{ \myfun{f}_1 : \myse{F}_1, \cdots, \myfun{f}_n : \myse{F}_n } \\
+ \myctx & \myelabt & \myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \\
& & \vspace{-0.2cm} \\
- & \myelabf & \myctx;\ \mytyc{D} : \mytele \myarr \mytyp;\\
- & & \mytyc{D}.\myfun{f}_1 : \mytele \myarr \myapp{\mytyc{D}}{\mytelee} \myarr \myse{F}_1;\ \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}; \\
+ & \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
- }
}
- \mydesc{reduction elaboration:}{\myctx \vdash \mytmsyn \myred \mytmsyn}{
- \centering{
- \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
- }
+ \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{Elaborations for records.}
- \label{fig:elab-adt}
+ \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.
+
+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?}
-\subsection{Type hierarchy}
+The hardest design choice when designing $\mykant$\ was to decide
+whether user defined types should be included, and how to handle them.
+In the end, as we saw, we can devise general structures like $\mytyc{W}$
+that can express all inductive structures. However, using those tools
+beyond very simple examples is near-impossible for a human user. 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 record, 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 maching, 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.
+\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}
-\subsection{Defined and postulated variables}
+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}.
-As mentioned, in \mykant\ we can defined top level variables, with or without
-a body. We call the variables
+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$.
-\subsection{Observational equality}
+\begin{figure}[b!]
-\section{\mykant : The practice}
-\label{sec:kant-practice}
+\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
-The codebase consists of around 2500 lines of Haskell, as reported by the
-\texttt{cloc} utility. The high level design is heavily inspired by Conor
-McBride's work on various incarnations of Epigram, and specifically by the
-first version as described \citep{McBride2004} and the codebase for the new
-version \footnote{Available intermittently as a \texttt{darcs} repository at
- \url{http://sneezy.cs.nott.ac.uk/darcs/Pig09}.}. In many ways \mykant\ is
-something in between the first and second version of Epigram.
+ \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}
-The interaction happens in a read-eval-print loop (REPL). The repl is a
-available both as a commandline application and in a web interface, which is
-available at \url{kant.mazzo.li} and presents itself as in figure
-\ref{fig:kant-web}.
+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{figure}
- \centering{
- \includegraphics[scale=1.0]{kant-web.png}
+\begin{mydef}[Cumulativity for \mykant' base types]
+ Figure \ref{fig:cumulativity} gives a formal definition of
+ 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, there is the obvious clumsyness of having to
+manually specify the size of types. More importantly, if we want to use
+$\myfun{$\vee$}$ itself as an argument to other type-formers, we need to
+make sure that those allow for types at least as large as
+$\mytyp_{100}$.
+
+A better option is to employ a mechanised version of what Russell called
+\emph{typical ambiguity}: we let the user live under the illusion that
+$\mytyp : \mytyp$, but check that the statements about types are
+consistent under the hood. $\mykant$\ implements this along the lines
+of \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, and we keep a set of
+constraints and add new constraints as we type check, generating new
+references when needed.
+
+For example, when type checking the type $\mytyp\, r_1$, where $r_1$
+denotes the unique reference assigned to that term, we will generate a
+new fresh reference $\mytyp\, r_2$, and add the constraint $r_1 < r_2$
+to the set. When type checking $\myctx \vdash
+\myfora{\myb{x}}{\mytya}{\mytyb}$, if $\myctx \vdash \mytya : \mytyp\,
+r_1$ and $\myctx; \myb{x} : \mytyb \vdash \mytyb : \mytyp\,r_2$; we will
+generate new reference $r$ and add $r_1 \le r$ and $r_2 \le r$ to the
+set.
+
+If at any point the constraint set becomes inconsistent, type checking
+fails. Moreover, when comparing two $\mytyp$ terms we equate their
+respective references with two $\le$ constraints. 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', and in fact this
+ provides the solution to simplify the equality above.
+
+ If we take, just like we saw previously in OTT
+ \[
+ \begin{array}{@{}l}
+ \myjm{\myse{f}_1}{\myfora{\mytya_1}{\myb{x_1}}{\mytyb_1}}{\myse{f}_2}{\myfora{\mytya_2}{\myb{x_2}}{\mytyb_2}} \myred \\
+ \myind{2} \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{
+ \myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2} \myimpl
+ \myjm{\myapp{\myse{f}_1}{\myb{x_1}}}{\mytyb_1[\myb{x_1}]}{\myapp{\myse{f}_2}{\myb{x_2}}}{\mytyb_2[\myb{x_2}]}
+ }}
+ \end{array}
+ \]
+ Then we can simply take
+ \[
+ \begin{array}{@{}l}
+ \mysigma \myappsp \mytya_1 \myappsp \mytyb_1 \myeq \mysigma \myappsp \mytya_2 \myappsp \mytyb_2 \myred \\ \myind{2} \mytya_1 \myeq \mytya_2 \myand \myjm{\mytyb_1}{\mytya_1 \myarr \mytyp}{\mytyb_2}{\mytya_2 \myarr \mytyp}
+ \end{array}
+ \]
+ Which will reduce to precisely what we desire. For what
+ concerns coercions and quotation, things stay the same (apart from the
+ fact that we apply to the second argument instead of substituting).
+ We can recognise records such as $\mysigma$ as such and employ
+ projections in value equality and coercions; as to not
+ impede progress if not necessary.
+
+\item[Lists] Now for finite lists, which will give us a taste for data
+ constructors:
+ \[
+ \begin{array}{@{}l}
+ \myadt{\mylist}{\myappsp (\myb{A} {:} \mytyp)}{ }{\mydc{nil} \mydcsep \mydc{cons} \myappsp \myb{A} \myappsp (\myapp{\mylist}{\myb{A}})}
+ \end{array}
+ \]
+ Type equality is simple---we only need to compare the parameter:
+ \[
+ \mylist \myappsp \mytya_1 \myeq \mylist \myappsp \mytya_2 \myred \mytya_1 \myeq \mytya_2
+ \]
+ For coercions, we transport based on the constructor, recycling the
+ proof for the inductive occurrence:
+ \[
+ \begin{array}{@{}l@{\ }c@{\ }l}
+ \mycoe \myappsp (\mylist \myappsp \mytya_1) \myappsp (\mylist \myappsp \mytya_2) \myappsp \myse{Q} \myappsp \mydc{nil} & \myred & \mydc{nil} \\
+ \mycoe \myappsp (\mylist \myappsp \mytya_1) \myappsp (\mylist \myappsp \mytya_2) \myappsp \myse{Q} \myappsp (\mydc{cons} \myappsp \mytmm \myappsp \mytmn) & \myred & \\
+ \multicolumn{3}{l}{\myind{2} \mydc{cons} \myappsp (\mycoe \myappsp \mytya_1 \myappsp \mytya_2 \myappsp \myse{Q} \myappsp \mytmm) \myappsp (\mycoe \myappsp (\mylist \myappsp \mytya_1) \myappsp (\mylist \myappsp \mytya_2) \myappsp \myse{Q} \myappsp \mytmn)}
+ \end{array}
+ \]
+ Value equality is unsurprising---we match the constructors, and
+ return bottom for mismatches. However, we also need to equate the
+ parameter in $\mydc{nil}$:
+ \[
+ \begin{array}{r@{ }c@{\ }c@{\ }c@{}l@{\ }c@{\ }r@{}c@{\ }c@{\ }c@{}l@{\ }l}
+ (& \mydc{nil} & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{nil} & : & \myapp{\mylist}{\mytya_2} &) \myred \mytya_1 \myeq \mytya_2 \\
+ (& \mydc{cons} \myappsp \mytmm_1 \myappsp \mytmn_1 & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{cons} \myappsp \mytmm_2 \myappsp \mytmn_2 & : & \myapp{\mylist}{\mytya_2} &) \myred \\
+ & \multicolumn{11}{@{}l}{ \myind{2}
+ \myjm{\mytmm_1}{\mytya_1}{\mytmm_2}{\mytya_2} \myand \myjm{\mytmn_1}{\myapp{\mylist}{\mytya_1}}{\mytmn_2}{\myapp{\mylist}{\mytya_2}}
+ } \\
+ (& \mydc{nil} & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{cons} \myappsp \mytmm_2 \myappsp \mytmn_2 & : & \myapp{\mylist}{\mytya_2} &) \myred \mybot \\
+ (& \mydc{cons} \myappsp \mytmm_1 \myappsp \mytmn_1 & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{nil} & : & \myapp{\mylist}{\mytya_2} &) \myred \mybot
+ \end{array}
+ \]
+
+\item[Evil type]
+ Now for something useless but complicated. % TODO finish
+
+\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.
+
+In fact, we can drop a separate notion of type-equality, which will
+simply be served by $\myjm{\mytya}{\mytyp}{\mytyb}{\mytyp}$, from now on
+abbreviated as $\mytya \myeq \mytyb$. We shall still distinguish
+equalities relating types for hierarchical purposes. The full rules for
+equality reductions, along with the syntax for propositions, are given
+in figure \ref{fig:kant-eq-red}. We exploit record to perform
+$\eta$-expansion. Moreover, given the nested $\myand$s, values of data
+types with zero constructors (such as $\myempty$) and records with zero
+destructors (such as $\myunit$) will be automatically always identified
+as equal.
+
+\begin{figure}[p]
+\mydesc{syntax}{ }{
+ \small
+ $
+ \begin{array}{r@{\ }c@{\ }l}
+ \myprsyn & ::= & \cdots \mysynsep \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
+ \end{array}
+ $
+}
+
+ % \mytmsyn & ::= & \cdots \mysynsep \mycoee{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \mysynsep
+ % \mycohh{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
+ % \myprsyn & ::= & \cdots \mysynsep \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
+
+% \mynegder
+
+% \mydesc{typing:}{\myctx \vdash \mytmsyn \Leftrightarrow \mytmsyn}{
+% \small
+% \begin{tabular}{cc}
+% \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
+% \AxiomC{$\myjud{\mytmt}{\mytya}$}
+% \BinaryInfC{$\myinf{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}$}
+% \DisplayProof
+% &
+% \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
+% \AxiomC{$\myjud{\mytmt}{\mytya}$}
+% \BinaryInfC{$\myinf{\mycohh{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\myprdec{\myjm{\mytmt}{\mytya}{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}}}$}
+% \DisplayProof
+% \end{tabular}
+% }
+
+\mynegder
+
+\mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
+ \small
+ \begin{tabular}{cc}
+ \AxiomC{\phantom{$\myjud{\myse{P}}{\myprop}$}}
+ \UnaryInfC{$\myjud{\mytop}{\myprop}$}
+ \noLine
+ \UnaryInfC{$\myjud{\mybot}{\myprop}$}
+ \DisplayProof
+ &
+ \AxiomC{$\myjud{\myse{P}}{\myprop}$}
+ \AxiomC{$\myjud{\myse{Q}}{\myprop}$}
+ \BinaryInfC{$\myjud{\myse{P} \myand \myse{Q}}{\myprop}$}
+ \noLine
+ \UnaryInfC{\phantom{$\myjud{\mybot}{\myprop}$}}
+ \DisplayProof
+ \end{tabular}
+
+ \myderivspp
+
+ \begin{tabular}{cc}
+ \AxiomC{$
+ \begin{array}{@{}c}
+ \phantom{\myjud{\myse{A}}{\mytyp} \hspace{0.8cm} \myjud{\mytmm}{\myse{A}}} \\
+ \myjud{\myse{A}}{\mytyp}\hspace{0.8cm}
+ \myjudd{\myctx; \myb{x} : \mytya}{\myse{P}}{\myprop}
+ \end{array}
+ $}
+ \UnaryInfC{$\myjud{\myprfora{\myb{x}}{\mytya}{\myse{P}}}{\myprop}$}
+ \DisplayProof
+ &
+ \AxiomC{$
+ \begin{array}{c}
+ \myjud{\myse{A}}{\mytyp} \hspace{0.8cm} \myjud{\mytmm}{\myse{A}} \\
+ \myjud{\myse{B}}{\mytyp} \hspace{0.8cm} \myjud{\mytmn}{\myse{B}}
+ \end{array}
+ $}
+ \UnaryInfC{$\myjud{\myjm{\mytmm}{\myse{A}}{\mytmn}{\myse{B}}}{\myprop}$}
+ \DisplayProof
+ \end{tabular}
+}
+
+\mynegder
+% TODO add syntax and types for coe and coh
+\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}
+\]
+
+
+% TODO finish
+
+\subsubsection{$\myprop$ and the hierarchy}
+
+We shall have, at earch 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 typecheck
+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 datatype 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}
+ $
}
- \caption{The \mykant\ web prompt.}
+
+ \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}
+
+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 \citep{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. Everything else presented is implemented and working
+reasonably well, and 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 commandline application and in
+a web interface, which is available at \url{bertus.mazzo.li}.
+
+A REPL cycle starts with the user inputing a \mykant\
+declaration or another REPL command, which then goes through various
+stages that can end up in a context update, or in failures of various
+kind. The process is described diagrammatically in figure
+\ref{fig:kant-process}.
+
+\begin{figure}[t]
+{\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}
-The interaction with the user takes place in a loop living in and updating a
-context \mykant\ declarations. The user inputs a new declaration that goes
-through various stages starts with the user inputing a \mykant\ declaration or
-another REPL command, which then goes through various stages that can end up
-in a context update, or in failures of various kind. The process is described
-diagrammatically in figure \ref{fig:kant-process}:
\begin{description}
+
\item[Parse] In this phase the text input gets converted to a sugared
- version of the core language.
+ 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] Convert the declaration to some context item, which might be
- a value declaration (type and body) or a data type declaration (constructors
- and destructors). This phase works in tandem with \textbf{Typechecking},
- which in turns needs to \textbf{Evaluate} terms.
-
-\item[Distill] and report the result. `Distilling' refers to the process of
- converting a core term back to a sugared version that the user can
- visualise. This can be necessary both to display errors including terms or
- to display result of evaluations or type checking that the user has
- requested.
+\item[Elaborate] Converts the declaration to some context items, which
+ might be a value declaration (type and body) or a data type
+ declaration (constructors and destructors). This phase works in
+ tandem with \textbf{Type checking}, which in turns needs to
+ \textbf{Evaluate} terms.
+
+\item[Distill] and report the result. `Distilling' refers to the
+ process of converting a core term back to a sugared version that the
+ user can visualise. This can be necessary both to display errors
+ including terms or to display result of evaluations or type checking
+ that the user has requested. 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}
-The details of each phase will be described in section % TODO insert section
-
\begin{figure}
- \centering{\small
+ \centering{\mysmall
\tikzstyle{block} = [rectangle, draw, text width=5em, text centered, rounded
corners, minimum height=2.5em, node distance=0.7cm]
\node [cloud] (user) {User};
\node [block, below left=1cm and 0.1cm of user] (parse) {Parse};
\node [block, below=of parse] (desugar) {Desugar};
- \node [block, below=of desugar] (reference) {Reference};
+ \node [block, below=of 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] (distill) {Distill};
- \node [block, right=of desugar] (update) {Update context};
+ \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) -- (reference);
+ \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] (error) edge[out=0,in=0] node [near start] {yes} (distill);
\path [line] (error) -- node [near start] {no} (update);
\path [line] (update) -- (distill);
- \path [line] (distill) -- (user);
+ \path [line] (pretty) -- (user);
+ \path [line] (distill) -- (pretty);
\path [line] (tycheck) edge[bend right] (evaluate);
\path [line] (evaluate) edge[bend right] (tycheck);
\end{tikzpicture}
\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 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 it
+is not very sophisticated, being specified in and processed by a parser
+generated with the \texttt{happy} parser generated for Haskell.
+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}
-\subsection{Type hierarchy}
+\subsubsection{Naming and substituting}
-\subsection{Elaboration}
+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 more slightly complicated
+ systems it is very hard to get right, even for experts.
+
+ One of the sore spots of explicit names is comparing terms up
+ $\alpha$-renaming, which again generates a huge amounts of
+ substitutions and requires special care. We can represent the
+ relationship between variables and their binders, by...
+
+\item[Nameless] ...getting rid of names altogether, and representing
+ bound variables with an index referring to the `binding' structure, a
+ notion introduced by \cite{de1972lambda}. Classically $0$ represents
+ the variable bound by the innermost binding structure, $1$ the
+ second-innermost, and so on. For instance with simple abstractions we
+ might have
+ \[
+ \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. Moreover, $\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 (Agda, Coq, \dots).
+
+\end{description}
+
+In the past decade or so advancements in the Haskell's type system and
+in general the spread new programming practices have enabled to make the
+second option much more amenable. \mykant\ thus takes the second path
+through the use of Edward Kmett's excellent \texttt{bound}
+library.\footnote{Available at
+\url{http://hackage.haskell.org/package/bound}.} We decribe its
+advantages but also pitfalls in the previously relatively unknown
+territory of dependent types---\texttt{bound} being created mostly to
+handle more simply typed systems.
+
+\texttt{bound} builds on the work of \cite{Bird1999}, who suggest 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}
+typeclass:
+\begin{Verbatim}
+class Monad m where
+ return :: m a
+ (>>=) :: m a -> (a -> m b) -> m b
+
+instance Monad Tm where
+ -- `return'ing turns a variable into a `Tm'
+ return = V
+
+ -- `t >>= f' takes a term `t' and a mapping from variables to terms
+ -- `f' and applies `f' to all the variables in `t', replacing them
+ -- with the mapped terms.
+ V v >>= f = f v
+ App m n >>= f = App (m >>= f) (n >>= f)
+
+ -- `Lam' is the tricky case: we modify the function to work with bound
+ -- variables, so that if it encounters `Bound' it leaves it untouched
+ -- (since the mapping 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 = do v <- s
+ case v of
+ Bound -> t
+ Free v' -> return v'
+\end{Verbatim}
+The beauty of this technique is that in a few simple function we have
+defined all the core operations in a general and `obviously correct'
+way, with the extra confidence of having the type checker looking our
+back. 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 for free a representation of terms with top-level, definitions;
+where closed terms contain only \verb|String| references to said
+definitions---see also \cite{McBride2004b}.
+
+What are then the pitfalls of this seemingly invincible technique? The
+most obvious impediment is the need for polymorphic recursion.
+Functions traversing terms parametrised by the variable type will have
+types such as
+\begin{Verbatim}
+-- Infer the type of a term, or return an error.
+infer :: Tm v -> Either Error (Tm v)
+\end{Verbatim}
+When traversing under a \verb|Scope| the parameter changes from \verb|v|
+to \verb|Var v|, and thus if we do not specify the type for our function explicitly
+inference will fail---type inference for polymorphic recursion being
+undecidable \citep{henglein1993type}. This causes some annoyance,
+especially in the presence of many local definitions that we would like
+to leave untyped.
+
+But the real issue is the fact that giving a type parametrised over a
+variable---say \verb|m v|---a \verb|Monad| instance means being able to
+only substitute variables for values of type \verb|m v|. This is a
+considerable inconvenience. Consider for instance the case of
+telescopes, which are a central tool to deal with contexts and other
+constructs. In Haskell we can give them a faithful representation
+with a data type along the lines of
+\begin{Verbatim}
+data Tele m v = End (m v) | Bind (m v) (Tele (Var v))
+type TeleTm = Tele Tm
+\end{Verbatim}
+The problem here is that what we want to substitute for variables in
+\verb|Tele m v| is \verb|m v| (probably \verb|Tm v|), not \verb|Tele m v| itself! What we need is
+\begin{Verbatim}
+bindTele :: Monad m => Tele m a -> (a -> m b) -> Tele m b
+substTele :: (Eq v, Monad m) => v -> m v -> Tele m v -> Tele m v
+instTele :: Monad m => m v -> Tele m (Var v) -> Tele m v
+\end{Verbatim}
+Not what \verb|Monad| gives us. Solving this issue in an elegant way
+has been a major sink of time and source of headaches for the author,
+who analysed some of the alternatives---most notably the work by
+\cite{weirich2011binders}---but found it impossible to give up the
+simplicity of the model above.
+
+That said, our term type is still reasonably brief, as shown in full in
+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 a
+nice interface similar to the one of \verb|bound| with a more flexible
+interface.
+
+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 wheak 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 being very simple, but has the disadvantage 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}.
+
+\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 standalone 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$ 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.
+
+\subsection{Tooling}
+
+\subsubsection{A type holes tutorial}
+\label{sec: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
+the word of mainstream programming. 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. Here we give a short tutorial in \mykant\ of this tool to
+give an idea of its usefulness.
+
+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}
+
+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
+particularly powerful mode for the \texttt{Emacs} text editor.
+
+\subsubsection{Web REPL}
\section{Evaluation}
+\label{sec:evaluation}
\section{Future work}
+\label{sec:future-work}
+
+As mentioned, the first move that the author plans to make is to work
+towards a simple but powerful term representation, and then adjust
+\mykant\ to this new 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, \mykant\ would still need many additions to compete
+as a reasonable alternative to the existing systems:
+
+\begin{description}
+\item[Pattern matching] Eliminators are very clumsy to use, and
+
+\item[More powerful data types] A popular improvement on basic data
+ types are inductive families \cite{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, where interestingly the modified version of System F that
+ lies at the core of recent versions of GHC features coercions similar
+ to those found in OTT \citep{Sulzmann2007}.
+
+ 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 constructors in \emph{other} arguments
+ \cite{McBride2004}.
+
+ Another popular extension 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.
+
+ It is also worth mentionning that in recent times there has been work
+ by \cite{dagand2012elaborating, chapman2010gentle} to show how to
+ define a set of primitives that data types can be elaborated into,
+ with the additional advantage of having the possibility of having a
+ very powerful notion of generic programming by writing functions
+ working on the `primitive' types as to be workable by all `compatible'
+ user-defined data 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[Type inference] While bidirectional type checking helps, for a
+ syts \cite{miller1992unification} \cite{gundrytutorial}
+ \cite{huet1973undecidability}.
+
+\item[Coinduction] \cite{cockett1992charity} \cite{mcbride2009let}.
+\end{description}
+
+% TODO coinduction (obscoin, gimenez, jacobs), pattern unification (miller,
+% gundry), partiality monad (NAD)
\appendix
for example
\mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
- \centering{Typing derivations here.}
+ Typing derivations here.
}
In the languages presented and Agda code samples I also highlight the syntax,
\end{tabular}
\end{center}
-Moreover, I will from time to time give examples in the Haskell programming
-language as defined in \citep{Haskell2010}, which I will typeset in
-\texttt{teletype} font. I assume that the reader is already familiar with
-Haskell, plenty of good introductions are available \citep{LYAH,ProgInHask}.
-
When presenting grammars, I will use a word in $\mysynel{math}$ font
-(e.g. $\mytmsyn$ or $\mytysyn$) to indicate indicate nonterminals. Additionally,
-I will use quite flexibly a $\mysynel{math}$ font to indicate a syntactic
-element. More specifically, terms are usually indicated by lowercase letters
-(often $\mytmt$, $\mytmm$, or $\mytmn$); and types by an uppercase letter (often
-$\mytya$, $\mytyb$, or $\mytycc$).
+(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}$}
\UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mytyb}$}
\end{prooftree}
-\section{Agda rendition of core ITT}
-\label{app:agda-code}
+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 ⊥ : Set where
+ data Empty : Set where
- absurd : ∀ {a} {A : Set a} → ⊥ → A
+ absurd : ∀ {a} {A : Set a} → Empty → A
absurd ()
- record ⊤ : Set where
+ ¬_ : ∀ {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
field
fst : A
snd : B fst
+ open _×_ public
data Bool : Set where
true false : Bool
- if_then_else_ : ∀ {a} {P : Bool → Set a} (x : Bool) → P true → P false → P x
- if true then x else _ = x
- if false then _ else x = x
+ 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
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
∀ {x y} → P x x (refl x) → (x≡y : x ≡ y) → P x y x≡y
≡-elim P p (refl x) = p
- subst : ∀ {a b} {A : Set a}
- (P : A → Set b) →
- ∀ {x y} → (x≡y : x ≡ y) → P x → P y
+ subst : ∀ {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}
-\nocite{*}
+\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}
+}
+
+
+
\bibliographystyle{authordate1}
\bibliography{thesis}
projects / bitonic-mengthesis.git / blobdiff