-\documentclass[report]{article}
+\documentclass[report, 11pt]{article}
+\usepackage{etex}
+
+\usepackage[sc,slantedGreek]{mathpazo}
+\linespread{1.05}
+% \usepackage{times}
+
+\oddsidemargin 0in
+\evensidemargin 0in
+\textheight 9.5in
+\textwidth 6.2in
+\topmargin -7mm
+\parindent 10pt
+
%% Narrow margins
% \usepackage{fullpage}
%% Images
\usepackage{graphicx}
+%% Subfigure
+\usepackage{subcaption}
+
+\usepackage{verbatim}
+
%% diagrams
\usepackage{tikz}
\usetikzlibrary{shapes,arrows,positioning}
\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{\mydc}{\AgdaInductiveConstructor}
\newcommand{\myfld}{\AgdaField}
\newcommand{\myfun}{\AgdaFunction}
-% TODO make this use AgdaBound
-\newcommand{\myb}[1]{\AgdaBound{#1}}
+\newcommand{\myb}[1]{\AgdaBound{$#1$}}
\newcommand{\myfield}{\AgdaField}
\newcommand{\myind}{\AgdaIndent}
\newcommand{\mykant}{\textsc{Kant}}
\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}
\FrameSep0.2cm
\newcommand{\mydesc}[3]{
\mbox{
\parbox{\textwidth}{
{\small
- \vspace{0.3cm}
+ \vspace{0.2cm}
\hfill \textbf{#1} $#2$
-
\framebox[\textwidth]{
\parbox{\textwidth}{
\vspace{0.1cm}
- #3
- \vspace{0.1cm}
+ \centering{
+ #3
+ }
+ \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{\mysub}[3]{#1[#2 / #3]}
\newcommand{\mytysyn}{\mysynel{type}}
\newcommand{\mybasetys}{K}
-% TODO change this name
\newcommand{\mybasety}[1]{B_{#1}}
\newcommand{\mytya}{\myse{A}}
\newcommand{\mytyb}{\myse{B}}
\newcommand{\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{\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{\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{\myprdec}[1]{\mathopen{\mytyc{$\llbracket$}} #1 \mathopen{\mytyc{$\rrbracket$}}}
+\newcommand{\myand}{\mathrel{\mytyc{$\wedge$}}}
+\newcommand{\mybigand}{\mathrel{\mytyc{$\bigwedge$}}}
\newcommand{\myprfora}[3]{\forall #1 {:} #2. #3}
-\newcommand{\mybot}{\bot}
-\newcommand{\mytop}{\top}
+\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{\myinf}[2]{\myinff{\myctx}{#1}{#2}}
+\newcommand{\mychkk}[3]{#1 \vdash #2 \Leftarrow #3}
+\newcommand{\mychk}[2]{\mychkk{\myctx}{#1}{#2}}
+\newcommand{\myann}[2]{#1 : #2}
+\newcommand{\mydeclsyn}{\myse{decl}}
+\newcommand{\myval}[3]{#1 : #2 \mapsto #3}
+\newcommand{\mypost}[2]{\mysyn{abstract}\ #1 : #2}
+\newcommand{\myadt}[4]{\mysyn{data}\ #1 #2\ \mysyn{where}\ #3\{ #4 \}}
+\newcommand{\myreco}[4]{\mysyn{record}\ #1 #2\ \mysyn{where}\ \{ #4 \}}
+\newcommand{\myelabt}{\vdash}
+\newcommand{\myelabf}{\rhd}
+\newcommand{\myelab}[2]{\myctx \myelabt #1 \myelabf #2}
+\newcommand{\mytele}{\Delta}
+\newcommand{\mytelee}{\delta}
+\newcommand{\mydcctx}{\Gamma}
+\newcommand{\mynamesyn}{\myse{name}}
+\newcommand{\myvec}{\overrightarrow}
+\newcommand{\mymeta}{\textsc}
+\newcommand{\myhyps}{\mymeta{hyps}}
+\newcommand{\mycc}{;}
+\newcommand{\myemptytele}{\cdot}
+\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$}}
+
%% -----------------------------------------------------------------------------
\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}
+ \centering
+
+ \maketitle
+ \thispagestyle{empty}
+
+ \begin{minipage}{0.4\textwidth}
+ \begin{flushleft} \large
+ \emph{Supervisor:}\\
+ Dr. Steffen \textsc{van Backel}
+ \end{flushleft}
+\end{minipage}
+\begin{minipage}{0.4\textwidth}
+ \begin{flushright} \large
+ \emph{Co-marker:} \\
+ Dr. Philippa \textsc{Gardner}
+ \end{flushright}
+\end{minipage}
-\maketitle
+\end{titlepage}
\begin{abstract}
The marriage between programming and logic has been a very fertile one. In
particular, since the simply typed lambda calculus (STLC), a number of type
systems have been devised with increasing expressive power.
- 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.
+ Among this systems, Inutitionistic Type Theory (ITT) has been a very
+ popular framework for theorem provers and programming languages.
+ However, equality has always been a tricky business in ITT and related
+ theories.
+
+ In these thesis we will explain why this is the case, and present
+ Observational Type Theory (OTT), a solution to some of the problems
+ with equality. We then describe $\mykant$, a theorem prover featuring
+ OTT in a setting more close to the one found in current systems.
+ Having implemented part of $\mykant$ as a Haskell program, we describe
+ some of the implementation issues faced.
+\end{abstract}
+
+\clearpage
+
+\renewcommand{\abstractname}{Acknowledgements}
+\begin{abstract}
+ I would like to thank Steffen van Backel, my supervisor, who was brave
+ enough to believe in my project and who provided much advice and
+ support.
+
+ I would also like to thank the Haskell and Agda community on
+ \texttt{IRC}, which guided me through the strange world of types; and
+ in particular Andrea Vezzosi and James Deikun, with whom I entertained
+ countless insightful discussions in the past year. Andrea suggested
+ Observational Type Theory as a topic of study: this thesis would not
+ exist without him. Before them, Tony Fields introduced me to Haskell,
+ unknowingly filling most of my free time from that time on.
+
+ Finally, much of the work stems from the research of Conor McBride,
+ who answered many of my doubts through these months. I also owe him
+ the colours.
\end{abstract}
\clearpage
$
\begin{array}{l}
\myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{\myb{x}}{\mytmn}\text{, where} \\
- \myind{1}
+ \myind{2}
\begin{array}{l@{\ }c@{\ }l}
\mysub{\myb{x}}{\myb{x}}{\mytmn} & = & \mytmn \\
\mysub{\myb{y}}{\myb{x}}{\mytmn} & = & y\text{, with } \myb{x} \neq y \\
\mysub{(\myapp{\mytmt}{\mytmm})}{\myb{x}}{\mytmn} & = & (\myapp{\mysub{\mytmt}{\myb{x}}{\mytmn}}{\mysub{\mytmm}{\myb{x}}{\mytmn}}) \\
\mysub{(\myabs{\myb{x}}{\mytmm})}{\myb{x}}{\mytmn} & = & \myabs{\myb{x}}{\mytmm} \\
\mysub{(\myabs{\myb{y}}{\mytmm})}{\myb{x}}{\mytmn} & = & \myabs{\myb{z}}{\mysub{\mysub{\mytmm}{\myb{y}}{\myb{z}}}{\myb{x}}{\mytmn}}, \\
- \multicolumn{3}{l}{\myind{1} \text{with $\myb{x} \neq \myb{y}$ and $\myb{z}$ not free in $\myapp{\mytmm}{\mytmn}$}}
+ \multicolumn{3}{l}{\myind{2} \text{with $\myb{x} \neq \myb{y}$ and $\myb{z}$ not free in $\myapp{\mytmm}{\mytmn}$}}
\end{array}
\end{array}
$
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):
+{\small
\[
- (\myapp{\omega}{\omega}) \myred (\myapp{\omega}{\omega}) \myred \dots\text{, with $\omega = \myabs{x}{\myapp{x}{x}}$}
+ (\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
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.
+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.}
\noindent
\begin{minipage}{0.5\textwidth}
\mydesc{syntax}{ } {
- $ \mytmsyn ::= \dotsb \mysynsep \myfix{\myb{x}}{\mytysyn}{\mytmsyn} $
+ $ \mytmsyn ::= \cdots b \mysynsep \myfix{\myb{x}}{\mytysyn}{\mytmsyn} $
\vspace{0.4cm}
}
\end{minipage}
\begin{minipage}{0.5\textwidth}
\mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}} {
- \centering{
\AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytmt}{\mytya}$}
\UnaryInfC{$\myjud{\myfix{\myb{x}}{\mytya}{\mytmt}}{\mytya}$}
\DisplayProof
- }
}
\end{minipage}
\mydesc{reduction:}{\myjud{\mytmsyn}{\mytmsyn}}{
- \centering{
$ \myfix{\myb{x}}{\mytya}{\mytmt} \myred \mysub{\mytmt}{\myb{x}}{(\myfix{\myb{x}}{\mytya}{\mytmt})}$
- }
}
This will deprive us of normalisation, which is a particularly bad thing if we
that $(\mytya \myarr \mytyb) \myarr (\mytyb \myarr \mytycc) \myarr (\mytya
\myarr \mytycc)$, all we need to do is to devise a $\lambda$-term that has the
correct type:
-\[
+{\small\[
\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}.
\mydesc{syntax}{ }{
$
\begin{array}{r@{\ }c@{\ }l}
- \mytmsyn & ::= & \dots \\
+ \mytmsyn & ::= & \cdots \\
& | & \mytt \mysynsep \myapp{\myabsurd{\mytysyn}}{\mytmsyn} \\
& | & \myapp{\myleft{\mytysyn}}{\mytmsyn} \mysynsep
\myapp{\myright{\mytysyn}}{\mytmsyn} \mysynsep
\myapp{\mycase{\mytmsyn}{\mytmsyn}}{\mytmsyn} \\
& | & \mypair{\mytmsyn}{\mytmsyn} \mysynsep
\myapp{\myfst}{\mytmsyn} \mysynsep \myapp{\mysnd}{\mytmsyn} \\
- \mytysyn & ::= & \dots \mysynsep \myunit \mysynsep \myempty \mysynsep \mytmsyn \mysum \mytmsyn \mysynsep \mytysyn \myprod \mytysyn
+ \mytysyn & ::= & \cdots \mysynsep \myunit \mysynsep \myempty \mysynsep \mytmsyn \mysum \mytmsyn \mysynsep \mytysyn \myprod \mytysyn
\end{array}
$
}
\mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
- \centering{
\begin{tabular}{cc}
$
\begin{array}{l@{ }l@{\ }c@{\ }l}
\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{
+
\begin{tabular}{cc}
\AxiomC{$\myjud{\mytmt}{\mytya}$}
\UnaryInfC{$\myjud{\myapp{\myleft{\mytyb}}{\mytmt}}{\mytya \mysum \mytyb}$}
\DisplayProof
\end{tabular}
- }
+
\myderivsp
- \centering{
+
\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{
+
\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.
+Tagged unions (or sums, or coproducts---$\mysum$ here, \texttt{Either}
+in Haskell) correspond to disjunctions, and dually tuples (or pairs, or
+products---$\myprod$ here, tuples in Haskell) correspond to
+conjunctions. This is apparent looking at the ways to construct and
+destruct the values inhabiting those types: for $\mysum$ $\myleft{ }$
+and $\myright{ }$ correspond to $\vee$ introduction, and
+$\mycase{\myarg}{\myarg}$ to $\vee$ elimination; for $\myprod$
+$\mypair{\myarg}{\myarg}$ corresponds to $\wedge$ introduction, $\myfst$
+and $\mysnd$ to $\wedge$ elimination.
The trivial type $\myunit$ corresponds to the logical $\top$, and dually
$\myempty$ corresponds to the logical $\bot$. $\myunit$ has one introduction
rule ($\mytt$), and thus one inhabitant; and no eliminators. $\myempty$ has no
introduction rules, and thus no inhabitants; and one eliminator ($\myabsurd{
-}$), corresponding to the logical \emph{ex falso quodlibet}. 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.
+}$), 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
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:
-\[
+{\small\[
(\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
\mydesc{syntax}{ }{
$
\begin{array}{r@{\ }c@{\ }l}
- \mytmsyn & ::= & \dots \mysynsep \mynil{\mytysyn} \mysynsep \mytmsyn \mycons \mytmsyn
+ \mytmsyn & ::= & \cdots \mysynsep \mynil{\mytysyn} \mysynsep \mytmsyn \mycons \mytmsyn
\mysynsep
\myapp{\myapp{\myapp{\myfoldr}{\mytmsyn}}{\mytmsyn}}{\mytmsyn} \\
- \mytysyn & ::= & \dots \mysynsep \myapp{\mylist}{\mytysyn}
+ \mytysyn & ::= & \cdots \mysynsep \myapp{\mylist}{\mytysyn}
\end{array}
$
}
\mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
- \centering{
$
\begin{array}{l@{\ }c@{\ }l}
\myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{\mynil{\mytya}} & \myred & \mytmt \\
\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{
+
\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}
\item[Terms depending on types (towards $\lambda{2}$)] We can quantify over
types in our type signatures. For example, we can define a polymorphic
identity function:
- \[\displaystyle
+ {\small\[\displaystyle
(\myabss{\myb{A}}{\mytyp}{\myabss{\myb{x}}{\myb{A}}{\myb{x}}}) : (\myb{A} : \mytyp) \myarr \myb{A} \myarr \myb{A}
- \]
+ \]}
The first and most famous instance of this idea has been System F. This form
of polymorphism and has been wildly successful, also thanks to a well known
inference algorithm for a restricted version of System F known as
\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: {\small\[\displaystyle(\myabss{\myb{A} \myar \myb{R}}{\mytyp}{(\myb{A}
+ \myarr \myb{R}) \myarr \myb{R}}) : \mytyp \myarr \mytyp \myarr \mytyp\]}
\item[Types depending on terms (towards $\lambda{P}$)] Also known as `dependent
types', give great expressive power. For example, we can have values of whose
type depend on a boolean:
- \[\displaystyle(\myabss{\myb{x}}{\mybool}{\myite{\myb{x}}{\mynat}{\myrat}}) : \mybool
- \myarr \mytyp\]
+ {\small\[\displaystyle(\myabss{\myb{x}}{\mybool}{\myite{\myb{x}}{\mynat}{\myrat}}) : \mybool
+ \myarr \mytyp\]}
\end{description}
All the systems preserve the properties that make the STLC well behaved. The
\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}. The system's syntax and reduction
+rules are presented in their entirety in figure \ref{fig:core-tt-syn}.
+The typing rules are presented piece by piece. Agda and \mykant\
+renditions of the presented theory and all the examples is reproduced in
+appendix \ref{app:itt-code}.
\begin{figure}[t]
\mydesc{syntax}{ }{
& | & \mybool \mysynsep \mytrue \mysynsep \myfalse \mysynsep
\myitee{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
& | & \myfora{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
- \myabss{\myb{x}}{\mytmsyn}{\mytmsyn} \\
+ \myabss{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
+ (\myapp{\mytmsyn}{\mytmsyn}) \\
& | & \myexi{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
\mypairr{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn} \\
& | & \myapp{\myfst}{\mytmsyn} \mysynsep \myapp{\mysnd}{\mytmsyn} \\
}
\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}
$
+ \end{tabular}
+
\myderivsp
$
\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
$\myred$---moreover, when comparing types syntactically we do it up to
renaming of bound names ($\alpha$-renaming). For example under this
discipline we will find that
-\[
+{\small\[
\myabss{\myb{x}}{\mytya}{\myb{x}} \mydefeq \myabss{\myb{y}}{\mytya}{\myb{y}}
-\]
-Types that are definitionally equal can be used interchangeably. Here the
-`conversion' rule is not syntax directed, however we will see how it is
-possible to employ $\myred$ to decide term equality in a systematic
-way. % TODO add section
-Another thing to notice is that considering the need to reduce terms to decide
-equality, it is essential for a dependently type system to be terminating and
-confluent for type checking to be decidable.
-
-Moreover, we specify a \emph{type hierarchy} to talk about `large' types:
-$\mytyp_0$ will be the type of types inhabited by data: $\mybool$, $\mynat$,
-$\mylist$, etc. $\mytyp_1$ will be the type of $\mytyp_0$, and so on---for
-example we have $\mytrue : \mybool : \mytyp_0 : \mytyp_1 : \dots$. Each type
-`level' is often called a universe in the literature. While it is possible,
-to simplify things by having only one universe $\mytyp$ with $\mytyp :
-\mytyp$, this plan is inconsistent for much the same reason that impredicative
-na\"{\i}ve set theory is \citep{Hurkens1995}. Moreover, various techniques
-can be employed to lift the burden of explicitly handling universes.
-% TODO add sectioon about universes
+\]}
+Types that are definitionally equal can be used interchangeably. Here
+the `conversion' rule is not syntax directed, but it is possible to
+employ $\myred$ to decide term equality in a systematic way, by always
+reducing terms to their normal forms before comparing them, so that a
+separate conversion rule is not needed. % 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}. 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}$}
\BinaryInfC{$\myjud{\mytmm}{\mysub{\mytya}{x}{\mytrue}}$ \hspace{0.7cm} $\myjud{\mytmn}{\mysub{\mytya}{x}{\myfalse}}$}
\UnaryInfC{$\myjud{\myitee{\mytmt}{\myb{x}}{\mytya}{\mytmm}{\mytmn}}{\mysub{\mytya}{\myb{x}}{\mytmt}}$}
\DisplayProof
-
- }
}
-With booleans we get the first taste of `dependent' in `dependent types'. While
-the two introduction rules ($\mytrue$ and $\myfalse$) are not surprising, the
-typing rules for $\myfun{if}$ are. In most strongly typed languages we expect
-the branches of an $\myfun{if}$ statements to be of the same type, to preserve
-subject reduction, since execution could take both paths. This is a pity, since
-the type system does not reflect the fact that in each branch we gain knowledge
-on the term we are branching on. Which means that programs along the lines of
-\begin{verbatim}
-if null xs then head xs else 0
-\end{verbatim}
+With booleans we get the first taste of the `dependent' in `dependent
+types'. While the two introduction rules ($\mytrue$ and $\myfalse$) are
+not surprising, the typing rules for $\myfun{if}$ are. In most strongly
+typed languages we expect the branches of an $\myfun{if}$ statements to
+be of the same type, to preserve subject reduction, since execution
+could take both paths. This is a pity, since the type system does not
+reflect the fact that in each branch we gain knowledge on the term we
+are branching on. Which means that programs along the lines of
+{\small\[\text{\texttt{if null xs then head xs else 0}}\]}
are a necessary, well typed, danger.
However, in a more expressive system, we can do better: the branches' type can
\subsubsection{$\myarr$, or dependent function}
\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
- \centering{
\AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
\AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
\BinaryInfC{$\myjud{\myfora{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
\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.
+dependent functions, the result type can depend on the value of the
+argument. This feature, together with the fact that the result type
+might be a type itself, brings a lot of interesting possibilities.
+Following this intuition, in the introduction rule, the return type is
+typechecked in a context with an abstracted variable of lhs' type, and
+in the elimination rule the actual argument is substituted in the return
+type. Keeping the correspondence with logic alive, dependent functions
+are much like universal quantifiers ($\forall$) in logic.
+
+For example, assuming that we have lists and natural numbers in our
+language, using dependent functions we would be able to
+write:
+{\small\[
+\begin{array}{l}
+\myfun{length} : (\myb{A} {:} \mytyp_0) \myarr \myapp{\mylist}{\myb{A}} \myarr \mynat \\
+\myarg \myfun{$>$} \myarg : \mynat \myarr \mynat \myarr \mytyp_0 \\
+\myfun{head} : (\myb{A} {:} \mytyp_0) \myarr (\myb{l} {:} \myapp{\mylist}{\myb{A}})
+ \myarr \myapp{\myapp{\myfun{length}}{\myb{A}}}{\myb{l}} \mathrel{\myfun{>}} 0 \myarr
+ \myb{A}
+\end{array}
+\]}
+
+\myfun{length} is the usual polymorphic length function. $\myfun{>}$ is
+a function that takes two naturals and returns a type: if the lhs is
+greater then the rhs, $\myunit$ is returned, $\myempty$ otherwise. This
+way, we can express a `non-emptyness' condition in $\myfun{head}$, by
+including a proof that the length of the list argument is non-zero.
+This allows us to rule out the `empty list' case, so that we can safely
+return the first element.
Again, we need to make sure that the type hierarchy is respected, which is the
reason why a type formed by $\myarr$ will live in the least upper bound of the
levels of argument and return type. This trend will continue with the other
type-level binders, $\myprod$ and $\mytyc{W}$.
-% TODO maybe examples?
-
\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}}$}
\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:
+{\small\[
+\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{b}}}{\myb{x}}{(\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{
\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}}$}
}$}
\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. The core
+idea is to
+
+% TODO finish
+
+
\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}
\mydesc{syntax}{ }{
$
\begin{array}{r@{\ }c@{\ }l}
- \mytmsyn & ::= & \dots \\
+ \mytmsyn & ::= & \cdots \\
& | & \mytmsyn \mypeq{\mytmsyn} \mytmsyn \mysynsep
\myapp{\myrefl}{\mytmsyn} \\
& | & \myjeq{\mytmsyn}{\mytmsyn}{\mytmsyn}
\end{minipage}
\begin{minipage}{0.5\textwidth}
\mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
- \centering{
$
\myjeq{\myse{P}}{(\myapp{\myrefl}{\mytmm})}{\mytmn} \myred \mytmn
$
- }
\vspace{0.9cm}
}
\end{minipage}
\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
- \centering{
\AxiomC{$\myjud{\mytya}{\mytyp_l}$}
\AxiomC{$\myjud{\mytmm}{\mytya}$}
\AxiomC{$\myjud{\mytmn}{\mytya}$}
\myderivsp
\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}}{\mytmm \mypeq{\mytya} \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}{\myb{x} \mypeq{\mytya} \myb{y}}{\mytyp_l}}} \\
+ \myjud{\myse{q}}{\mytmm \mypeq{\mytya} \mytmn}\hspace{1.1cm}\myjud{\myse{p}}{\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmm}}{(\myapp{\myrefl}{\mytmm})}}
+ \end{array}
+ $}
\UnaryInfC{$\myjud{\myjeq{\myse{P}}{\myse{q}}{\myse{p}}}{\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmn}}{q}}$}
\DisplayProof
\end{tabular}
- }
}
To express equality between two terms inside ITT, the obvious way to do so is
Our type former is $\mypeq{\mytya}$, which given a type (in this case
$\mytya$) relates equal terms of that type. $\mypeq{}$ has one introduction
rule, $\myrefl$, which introduces an equality relation between definitionally
-equal terms---in the typing rule we display the term as `the same', meaning
-`the same up to $\mydefeq$'. % TODO maybe mention this earlier
+equal terms.
Finally, we have one eliminator for $\mypeq{}$, $\myjeqq$. $\myjeq{\myse{P}}{\myse{q}}{\myse{p}}$ takes
\begin{itemize}
While the $\myjeqq$ rule is slightly convoluted, ve can derive many more
`friendly' rules from it, for example a more obvious `substitution' rule, that
replaces equal for equal in predicates:
-\[
+{\small\[
\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}}{\myb{x} \mypeq{\myb{A}} \myb{y} \myarr \myapp{\myb{P}}{\myb{x}} \myarr \myapp{\myb{P}}{\myb{y}}}}} \\
+\myfun{subst}\myappsp \myb{A}\myappsp\myb{P}\myappsp\myb{x}\myappsp\myb{y}\myappsp\myb{q}\myappsp\myb{p} \mapsto
+ \myjeq{(\myabs{\myb{x}\ \myb{y}\ \myb{q}}{\myapp{\myb{P}}{\myb{y}}})}{\myb{p}}{\myb{q}}
\end{array}
-\]
-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:
+equality, such as symmetry, transitivity, and a congruence law.
% TODO finish this
\subsection{Common extensions}
-eta law
+Our definitional equality can be made larger in various ways, here we
+review some common extensions.
+
+\subsubsection{Congruence laws and $\eta$-expansion}
+
+A simple type-directed check that we can do on functions and records is
+$\eta$-expansion. We can then have
+
+\mydesc{definitional equality:}{\myjud{\mytmm \mydefeq \mytmn}{\mytmsyn}}{
+ \begin{tabular}{cc}
+ \AxiomC{$\myjud{f \mydefeq (\myabss{\myb{x}}{\mytya}{\myapp{\myse{g}}{\myb{x}}})}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
+ \UnaryInfC{$\myjud{\myse{f} \mydefeq \myse{g}}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
+ \DisplayProof
+ &
+ \AxiomC{$\myjud{\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}
+
+ \myderivsp
+
+ \AxiomC{$\myjud{\mytmm}{\myunit}$}
+ \AxiomC{$\myjud{\mytmn}{\myunit}$}
+ \BinaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\myunit}$}
+ \DisplayProof
+}
+
+% TODO finish
+
+\subsubsection{Uniqueness of identity proofs}
-congruence
+% TODO finish
+% TODO reference the fact that J does not imply J
+% TODO mention univalence
-UIP
+
+\mydesc{definitional equality:}{\myjud{\mytmm \mydefeq \mytmn}{\mytmsyn}}{
+ \AxiomC{$
+ \begin{array}{@{}c}
+ \myjud{\myse{P}}{\myfora{\myb{x}}{\mytya}{\myb{x} \mypeq{\mytya} \myb{x} \myarr \mytyp}} \\\
+ \myjud{\myse{p}}{\myfora{\myb{x}}{\mytya}{\myse{P} \myappsp \myb{x} \myappsp \myb{x} \myappsp (\myrefl \myapp \myb{x})}} \hspace{1cm}
+ \myjud{\mytmt}{\mytya} \hspace{1cm}
+ \myjud{\myse{q}}{\mytmt \mypeq{\mytya} \mytmt}
+ \end{array}
+ $}
+ \UnaryInfC{$\myjud{\myfun{K} \myappsp \myse{P} \myappsp \myse{p} \myappsp \myse{t} \myappsp \myse{q}}{\myse{P} \myappsp \mytmt \myappsp \myse{q}}$}
+ \DisplayProof
+}
\subsection{Limitations}
However this is not the case, or in other words with the tools we have we have
no term of type
-\[
+{\small\[
\myfun{ext} : \myfora{\myb{A}\ \myb{B}}{\mytyp}{\myfora{\myb{f}\ \myb{g}}{
\myb{A} \myarr \myb{B}}{
(\myfora{\myb{x}}{\myb{A}}{\myapp{\myb{f}}{\myb{x}} \mypeq{\myb{B}} \myapp{\myb{g}}{\myb{x}}}) \myarr
\myb{f} \mypeq{\myb{A} \myarr \myb{B}} \myb{g}
}
}
-\]
+\]}
To see why this is the case, consider the functions
-\[\myabs{\myb{x}}{0 \mathrel{\myfun{+}} \myb{x}}$ and $\myabs{\myb{x}}{\myb{x} \mathrel{\myfun{+}} 0}\]
-where $\myfun{+}$ is defined by recursion on the first argument, gradually
-destructing it to build up successors of the second argument. The two
-functions are clearly denotationally the same, and we can in fact prove that
-\[
+{\small\[\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
+{\small\[
\myfora{\myb{x}}{\mynat}{(0 \mathrel{\myfun{+}} \myb{x}) \mypeq{\mynat} (\myb{x} \mathrel{\myfun{+}} 0)}
-\]
+\]}
By analysis on the $\myb{x}$. However, the two functions are not
definitionally equal, and thus we won't be able to get rid of the
quantification.
-For the reasons above, theories that offer a propositional equality similar to
-what we presented are called \emph{intensional}, as opposed to
-\emph{extensional}. Most systems in wide use today (such as Agda, Coq and
-Epigram) are of this kind.
+For the reasons above, theories that offer a propositional equality
+similar to what we presented are called \emph{intensional}, as opposed
+to \emph{extensional}. Most systems in wide use today (such as Agda,
+Coq, and Epigram) are of this kind.
This is quite an annoyance that often makes reasoning awkward to execute. It
also extends to other fields, for example proving bisimulation between
definitional equality:
\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
- \centering{
\AxiomC{$\myjud{\myse{q}}{\mytmm \mypeq{\mytya} \mytmn}$}
\UnaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\mytya}$}
\DisplayProof
- }
}
This rule takes the name of \emph{equality reflection}, and is a very
\item The rule is syntax directed, and the type checker is presumably expected
to come up with equality proofs when needed.
\item More worryingly, type checking becomes undecidable also because
- computing under false assumptions becomes unsafe.
- Consider for example
- \[
- \myabss{\myb{q}}{\mytya \mypeq{\mytyp} (\mytya \myarr \mytya)}{\myhole{?}}
- \]
- Using the assumed proof in tandem with equality reflection we could easily
- write a classic Y combinator, sending the compiler into a loop.
+ computing under false assumptions becomes unsafe, since we can use
+ equality reflection and the conversion rule to have terms of any
+ type.
+ Consider for example {\small\[ \myabss{\myb{q}}{\mytya
+ \mypeq{\mytyp} (\mytya \myarr \mytya)}{\myhole{?}}
+ \]}
+Using the assumed proof in tandem with equality reflection we
+could easily write a classic Y combinator, sending the compiler into a
+loop. In general, we using the conversion rule
+% TODO check that this makes sense
\end{itemize}
Given these facts theories employing equality reflection, like NuPRL
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}}}\]
+{\small\[\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}}}$}
+ \small
+ \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}
-\ref{sec:ott}
+\subsection{Some alternatives}
+
+% TODO finish
+% TODO add `extentional axioms' (Hoffman), setoid models (Thorsten)
+
+\section{Observational equality}
+\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,
+ Theory} (OTT), promises to keep the well behavedness of ITT while
+being able to gain many useful equality proofs\footnote{It is suspected
+ that OTT gains \emph{all} the equality proofs of ETT, but no proof
+ exists yet.}, including function extensionality. The main idea is to
+give the user the possibility to \emph{coerce} (or transport) values
+from a type $\mytya$ to a type $\mytyb$, if the type checker can prove
+structurally that $\mytya$ and $\mytya$ are equal; and providing a
+value-level equality based on similar principles. Here we give an
+exposition which follows closely the original paper.
+
+\subsection{A simpler theory, a propositional fragment}
+
+\mydesc{syntax}{ }{
+ $\mytyp_l$ is replaced by $\mytyp$. \\\ \\
+ $
+ \begin{array}{r@{\ }c@{\ }l}
+ \mytmsyn & ::= & \cdots \mysynsep \myprdec{\myprsyn} \mysynsep
+ \myITE{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
+ \myprsyn & ::= & \mybot \mysynsep \mytop \mysynsep \myprsyn \myand \myprsyn
+ \mysynsep \myprfora{\myb{x}}{\mytmsyn}{\myprsyn}
+ \end{array}
+ $
+}
+
+\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
+ \begin{tabular}{cc}
+ \AxiomC{$\myjud{\myse{P}}{\myprop}$}
+ \UnaryInfC{$\myjud{\myprdec{\myse{P}}}{\mytyp}$}
+ \DisplayProof
+ &
+ \AxiomC{$\myjud{\mytmt}{\mybool}$}
+ \AxiomC{$\myjud{\mytya}{\mytyp}$}
+ \AxiomC{$\myjud{\mytyb}{\mytyp}$}
+ \TrinaryInfC{$\myjud{\myITE{\mytmt}{\mytya}{\mytyb}}{\mytyp}$}
+ \DisplayProof
+ \end{tabular}
+}
+
+\mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
+ \begin{tabular}{ccc}
+ \AxiomC{\phantom{$\myjud{\myse{P}}{\myprop}$}}
+ \UnaryInfC{$\myjud{\mytop}{\myprop}$}
+ \noLine
+ \UnaryInfC{$\myjud{\mybot}{\myprop}$}
+ \DisplayProof
+ &
+ \AxiomC{$\myjud{\myse{P}}{\myprop}$}
+ \AxiomC{$\myjud{\myse{Q}}{\myprop}$}
+ \BinaryInfC{$\myjud{\myse{P} \myand \myse{Q}}{\myprop}$}
+ \noLine
+ \UnaryInfC{\phantom{$\myjud{\mybot}{\myprop}$}}
+ \DisplayProof
+ &
+ \AxiomC{$\myjud{\myse{A}}{\mytyp}$}
+ \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\myse{P}}{\myprop}$}
+ \BinaryInfC{$\myjud{\myprfora{\myb{x}}{\mytya}{\myse{P}}}{\myprop}$}
+ \noLine
+ \UnaryInfC{\phantom{$\myjud{\mybot}{\myprop}$}}
+ \DisplayProof
+ \end{tabular}
+}
+
+Our foundation will be a type theory like the one of section
+\ref{sec:itt}, with only one level: $\mytyp_0$. In this context we will
+drop the $0$ and call $\mytyp_0$ $\mytyp$. Moreover, since the old
+$\myfun{if}\myarg\myfun{then}\myarg\myfun{else}$ was able to return
+types thanks to the hierarchy (which is gone), we need to reintroduce an
+ad-hoc conditional for types, where the reduction rule is the obvious
+one.
+
+However, we have an addition: a universe of \emph{propositions},
+$\myprop$. $\myprop$ isolates a fragment of types at large, and
+indeed we can `inject' any $\myprop$ back in $\mytyp$ with $\myprdec{\myarg}$: \\
+\mydesc{proposition decoding:}{\myprdec{\mytmsyn} \myred \mytmsyn}{
+ \begin{tabular}{cc}
+ $
+ \begin{array}{l@{\ }c@{\ }l}
+ \myprdec{\mybot} & \myred & \myempty \\
+ \myprdec{\mytop} & \myred & \myunit
+ \end{array}
+ $
+ &
+ $
+ \begin{array}{r@{ }c@{ }l@{\ }c@{\ }l}
+ \myprdec{&\myse{P} \myand \myse{Q} &} & \myred & \myprdec{\myse{P}} \myprod \myprdec{\myse{Q}} \\
+ \myprdec{&\myprfora{\myb{x}}{\mytya}{\myse{P}} &} & \myred &
+ \myfora{\myb{x}}{\mytya}{\myprdec{\myse{P}}}
+ \end{array}
+ $
+ \end{tabular}
+ } \\
+ Propositions are what we call the types of \emph{proofs}, or types
+ whose inhabitants contain no `data', much like $\myunit$. The goal of
+ doing this is twofold: erasing all top-level propositions when
+ compiling; and to identify all equivalent propositions as the same, as
+ we will see later.
+
+ Why did we choose what we have in $\myprop$? Given the above
+ criteria, $\mytop$ obviously fits the bill. A pair of propositions
+ $\myse{P} \myand \myse{Q}$ still won't get us data. Finally, if
+ $\myse{P}$ is a proposition and we have
+ $\myprfora{\myb{x}}{\mytya}{\myse{P}}$ , the decoding will be a
+ function which returns propositional content. The only threat is
+ $\mybot$, by which we can fabricate anything we want: however if we
+ are consistent there will be nothing of type $\mybot$ at the top
+ level, which is what we care about regarding proof erasure.
+
+\subsection{Equality proofs}
\mydesc{syntax}{ }{
+ $
+ \begin{array}{r@{\ }c@{\ }l}
+ \mytmsyn & ::= & \cdots \mysynsep
+ \mycoee{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \mysynsep
+ \mycohh{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
+ \myprsyn & ::= & \cdots \mysynsep \mytmsyn \myeq \mytmsyn \mysynsep
+ \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn}
+ \end{array}
+ $
+}
+
+\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
+ \begin{tabular}{cc}
+ \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
+ \AxiomC{$\myjud{\mytmt}{\mytya}$}
+ \BinaryInfC{$\myjud{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}$}
+ \DisplayProof
+ &
+ \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
+ \AxiomC{$\myjud{\mytmt}{\mytya}$}
+ \BinaryInfC{$\myjud{\mycohh{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\myprdec{\myjm{\mytmt}{\mytya}{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}}}$}
+ \DisplayProof
+
+ \end{tabular}
+}
+
+\mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
+ \begin{tabular}{cc}
+ \AxiomC{$
+ \begin{array}{l}
+ \ \\
+ \myjud{\myse{A}}{\mytyp} \hspace{1cm} \myjud{\myse{B}}{\mytyp}
+ \end{array}
+ $}
+ \UnaryInfC{$\myjud{\mytya \myeq \mytyb}{\myprop}$}
+ \DisplayProof
+ &
+ \AxiomC{$
+ \begin{array}{c}
+ \myjud{\myse{A}}{\mytyp} \hspace{1cm} \myjud{\mytmm}{\myse{A}} \\
+ \myjud{\myse{B}}{\mytyp} \hspace{1cm} \myjud{\mytmn}{\myse{B}}
+ \end{array}
+ $}
+ \UnaryInfC{$\myjud{\myjm{\mytmm}{\myse{A}}{\mytmn}{\myse{B}}}{\myprop}$}
+ \DisplayProof
+
+ \end{tabular}
+}
+
+
+While isolating a propositional universe as presented can be a useful
+exercises on its own, what we are really after is a useful notion of
+equality. In OTT we want to maintain the notion that things judged to
+be equal are still always repleaceable for one another with no
+additional changes. Note that this is not the same as saying that they
+are definitionally equal, since as we saw extensionally equal functions,
+while satisfying the above requirement, are not definitionally equal.
+
+Towards this goal we introduce two equality constructs in
+$\myprop$---the fact that they are in $\myprop$ indicates that they
+indeed have no computational content. The first construct, $\myarg
+\myeq \myarg$, relates types, the second,
+$\myjm{\myarg}{\myarg}{\myarg}{\myarg}$, relates values. The
+value-level equality is different from our old propositional equality:
+instead of ranging over only one type, we might form equalities between
+values of different types---the usefulness of this construct will be
+clear soon. In the literature this equality is known as `heterogeneous'
+or `John Major', since
+
+\begin{quote}
+ John Major's `classless society' widened people's aspirations to
+ equality, but also the gap between rich and poor. After all, aspiring
+ to be equal to others than oneself is the politics of envy. In much
+ the same way, forms equations between members of any type, but they
+ cannot be treated as equals (ie substituted) unless they are of the
+ same type. Just as before, each thing is only equal to
+ itself. \citep{McBride1999}.
+\end{quote}
+
+Correspondingly, at the term level, $\myfun{coe}$ (`coerce') lets us
+transport values between equal types; and $\myfun{coh}$ (`coherence')
+guarantees that $\myfun{coe}$ respects the value-level equality, or in
+other words that it really has no computational component: if we
+transport $\mytmm : \mytya$ to $\mytmn : \mytyb$, $\mytmm$ and $\mytmn$
+will still be the same.
+
+Before introducing the core ideas that make OTT work, let us distinguish
+between \emph{canonical} and \emph{neutral} types. Canonical types are
+those arising from the ground types ($\myempty$, $\myunit$, $\mybool$)
+and the three type formers ($\myarr$, $\myprod$, $\mytyc{W}$). Neutral
+types are those formed by
+$\myfun{If}\myarg\myfun{Then}\myarg\myfun{Else}\myarg$.
+Correspondingly, canonical terms are those inhabiting canonical types
+($\mytt$, $\mytrue$, $\myfalse$, $\myabss{\myb{x}}{\mytya}{\mytmt}$,
+...), and neutral terms those formed by eliminators\footnote{Using the
+ terminology from section \ref{sec:types}, we'd say that canonical
+ terms are in \emph{weak head normal form}.}. In the current system
+(and hopefully in well-behaved systems), all closed terms reduce to a
+canonical term, and all canonical types are inhabited by canonical
+terms.
+
+\subsubsection{Type equality, and coercions}
+
+The plan is to decompose type-level equalities between canonical types
+into decodable propositions containing equalities regarding the
+subterms, and to use coerce recursively on the subterms using the
+generated equalities. This interplay between type equalities and
+\myfun{coe} ensures that invocations of $\myfun{coe}$ will vanish when
+we have evidence of the structural equality of the types we are
+transporting terms across. If the type is neutral, the equality won't
+reduce and thus $\myfun{coe}$ won't reduce either. If we come an
+equality between different canonical types, then we reduce the equality
+to bottom, making sure that no such proof can exist, and providing an
+`escape hatch' in $\myfun{coe}$.
+
+\begin{figure}[t]
+
+\mydesc{equality reduction:}{\myprsyn \myred \myprsyn}{
+ $
+ \begin{array}{c@{\ }c@{\ }c@{\ }l}
+ \myempty & \myeq & \myempty & \myred \mytop \\
+ \myunit & \myeq & \myunit & \myred \mytop \\
+ \mybool & \myeq & \mybool & \myred \mytop \\
+ \myexi{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myexi{\myb{x_2}}{\mytya_2}{\mytya_2} & \myred \\
+ \multicolumn{4}{l}{
+ \myind{2} \mytya_1 \myeq \mytyb_1 \myand
+ \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{\myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2}} \myimpl \mytyb_1[\myb{x_1}] \myeq \mytyb_2[\myb{x_2}]}
+ } \\
+ \myfora{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myfora{\myb{x_2}}{\mytya_2}{\mytyb_2} & \myred \cdots \\
+ \myw{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myw{\myb{x_2}}{\mytya_2}{\mytyb_2} & \myred \cdots \\
+ \mytya & \myeq & \mytyb & \myred \mybot\ \text{if $\mytya$ and $\mytyb$ are canonical.}
+ \end{array}
+ $
+}
+\myderivsp
+\mydesc{reduction}{\mytmsyn \myred \mytmsyn}{
$
- \begin{array}{r@{\ }c@{\ }l}
- \mytmsyn & ::= & \dots \\
- & | & \myprdec{\myprsyn} \mysynsep
- \mycoee{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \mysynsep
- \mycohh{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
- \myprsyn & ::= & \mybot \mysynsep \mytop \mysynsep \myprsyn \myand \myprsyn
- \mysynsep \myprfora{\myb{x}}{\mytmsyn}{\myprsyn} \\\
- & | & \mytmsyn = \mytmsyn \mysynsep
- \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn}
+ \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} & \mytt & \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 & \\
+ \multicolumn{7}{l}{
+ \myind{2}\myapp{\myabsurd{\mytyb}}{\myse{Q}}\ \text{if $\mytya$ and $\mytyb$ are canonical.}
+ }
\end{array}
$
}
-\mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
- \centering{
- }
-}
+\caption{Reducing type equalities, and using them when
+ $\myfun{coe}$rcing.}
+\label{fig:eqred}
+\end{figure}
-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.
+Figure \ref{fig:eqred} illustrates this idea in practice. For ground
+types, the proof is the trivial element, and \myfun{coe} is the
+identity. For the three type binders, things are similar but subtly
+different---the choices we make in the type equality are dictated by
+the desire of writing the $\myfun{coe}$ in a natural way.
+
+$\myprod$ is the easiest case: we decompose the proof into proofs that
+the first element's types are equal ($\mytya_1 \myeq \mytya_2$), and a
+proof that given equal values in the first element, the types of the
+second elements are equal too
+($\myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{\myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2}}
+ \myimpl \mytyb_1 \myeq \mytyb_2}$)\footnote{We are using $\myimpl$ to
+ indicate a $\forall$ where we discard the first value. We write
+ $\mytyb_1[\myb{x_1}]$ to indicate that the $\myb{x_1}$ in $\mytyb_1$
+ is re-bound to the $\myb{x_1}$ quantified by the $\forall$, and
+ similarly for $\myb{x_2}$ and $\mytyb_2$.}. This also explains the
+need for heterogeneous equality, since in the second proof it would be
+awkward to express the fact that $\myb{A_1}$ is the same as $\myb{A_2}$.
+In the respective $\myfun{coe}$ case, since the types are canonical, we
+know at this point that the proof of equality is a pair of the shape
+described above. Thus, we can immediately coerce the first element of
+the pair using the first element of the proof, and then instantiate the
+second element with the two first elements and a proof by coherence of
+their equality, since we know that the types are equal. The cases for
+the other binders are omitted for brevity, but they follow the same
+principle.
+
+\subsubsection{$\myfun{coe}$, laziness, and $\myfun{coh}$erence}
+
+It is important to notice that in the reduction rules for $\myfun{coe}$
+are never obstructed by the proofs: with the exception of comparisons
+between different canonical types we never pattern match on the 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:
-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{\mytmt}{\mytya}$}
+ \UnaryInfC{$\myjud{\myapp{\myrefl}{\mytmt}}{\myprdec{\myjm{\myb{x}}{\myb{\mytya}}{\myb{x}}{\myb{\mytya}}}}$}
+ \DisplayProof
+ &
+ \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
+ \end{tabular}
+}
+$\myrefl$ is the equivalent of the reflexivity rule in propositional
+equality, and $\mytyc{R}$ asserts that if we have a we have a $\mytyp$
+abstracting over a value we can substitute equal for equal---this lets
+us recover $\myfun{subst}$. Note that while we need to provide ad-hoc
+rules in the restricted, non-hierarchical theory that we have, if our
+theory supports abstraction over $\mytyp$s we can easily add these
+axioms as abstracted variables.
+\subsubsection{Value-level equality}
-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.
+\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 & : & \myempty&) & \myeq & (&\mytmt_2 & : & \myempty&) & \myred \mytop \\
+ (&\mytrue & : & \mybool&) & \myeq & (&\mytrue & : & \mybool&) & \myred \mytop \\
+ (&\myfalse & : & \mybool&) & \myeq & (&\myfalse & : & \mybool&) & \myred \mytop \\
+ (&\mytmt_1 & : & \mybool&) & \myeq & (&\mytmt_1 & : & \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 \\
+ & \multicolumn{11}{@{}l}{
+ \myind{2} \mybot\ \text{if $\mytya_1$ and $\mytya_2$ are canonical.}
+ }
+ \end{array}
+ $
+}
+As with type-level equality, we want value-level equality to reduce
+based on the structure of the compared terms.
+\subsection{Proof irrelevance}
-\section{Augmenting ITT}
-\label{sec:practical}
+% \section{Augmenting ITT}
+% \label{sec:practical}
-\subsection{A more liberal hierarchy}
+% \subsection{A more liberal hierarchy}
-\subsection{Type inference}
+% \subsection{Type inference}
-\subsubsection{Bidirectional type checking}
+% \subsubsection{Bidirectional type checking}
-\subsubsection{Pattern unification}
+% \subsubsection{Pattern unification}
-\subsection{Pattern matching and explicit fixpoints}
+% \subsection{Pattern matching and explicit fixpoints}
-\subsection{Induction-recursion}
+% \subsection{Induction-recursion}
-\subsection{Coinduction}
+% \subsection{Coinduction}
-\subsection{Dealing with partiality}
+% \subsection{Dealing with partiality}
-\subsection{Type holes}
+% \subsection{Type holes}
-\section{\mykant}
-\label{sec:kant}
+\section{\mykant : the theory}
+\label{sec:kant-theory}
-\mykant is an interactive theorem prover developed as part of this thesis.
+\mykant\ is an interactive theorem prover developed as part of this thesis.
The plan is to present a core language which would be capable of serving as
the basis for a more featureful system, while still presenting interesting
features and more importantly observational equality.
equality is not currently implemented. However, a detailed plan on how to add
it this functionality is provided, and should not prove to be too much work.
-\subsection{High level overview}
-
-\subsubsection{Features}
-
-The features currently implemented in \mykant are:
+The features currently implemented in \mykant\ are:
\begin{description}
\item[Full dependent types] As we would expect, we have dependent a system
The planned features are:
\begin{description}
-\item[Observational equality] As described in section \label{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.
We will analyse the features one by one, along with motivations and tradeoffs
for the design decisions made.
-\subsubsection{Implementation}
-
-The codebase consists of around 2500 lines of Haskell, as reported by the
-\texttt{cloc} utility. The high level design is heavily inspired by Conor
-McBride's work on various incarnations of Epigram, and specifically by the
-first version as described \citep{McBride2004} and the codebase for the new
-version \footnote{Available intermittently as a \texttt{darcs} repository at
- \url{http://sneezy.cs.nott.ac.uk/darcs/Pig09}.}. In many ways \mykant is
-something in between the first and second version of Epigram.
-
-The interaction happens in a read-eval-print loop (REPL). The repl is a
-available both as a commandline application and in a web interface, which is
-available at \url{kant.mazzo.li} and presents itself as in figure
-\ref{fig:kant-web}.
-
-\begin{figure}
- \centering{
- \includegraphics[scale=1.0]{kant-web.png}
- }
- \caption{The \mykant web prompt.}
- \label{fig:kant-web}
-\end{figure}
-
-The interaction with the user takes place in a loop living in and updating a
-context \mykant declarations. The user inputs a new declaration that goes
-through various stages starts with the user inputing a \mykant declaration,
-which then goes through various stages that can end up in a context update, or
-in failures of various kind. The process is described in figure
-\ref{fig:kant-process}. The workings of each phase will be illustrated in the
-next sections.
-
-\begin{figure}
- {\small
- \tikzstyle{block} = [rectangle, draw, text width=5em, text centered, rounded
- corners, minimum height=2.5em, node distance=0.7cm]
-
- \tikzstyle{decision} = [diamond, draw, text width=4.5em, text badly
- centered, inner sep=0pt, node distance=0.7cm]
-
- \tikzstyle{line} = [draw, -latex']
-
- \tikzstyle{cloud} = [draw, ellipse, minimum height=2em, text width=5em, text
- centered, node distance=1.5cm]
-
-
- \begin{tikzpicture}[auto]
- \node [cloud] (user) {User};
- \node [block, below left=1cm and 0.1cm of user] (parse) {Parse};
- \node [block, below=of parse] (desugar) {Desugar};
- \node [block, below=of desugar] (reference) {Reference};
- \node [block, below=of reference] (elaborate) {Elaborate};
- \node [block, below=of elaborate] (tycheck) {Typecheck};
- \node [decision, right=of elaborate] (error) {Error?};
- \node [block, right=of parse] (distill) {Distill};
- \node [block, right=of desugar] (update) {Update context};
-
- \path [line] (user) -- (parse);
- \path [line] (parse) -- (desugar);
- \path [line] (desugar) -- (reference);
- \path [line] (reference) -- (elaborate);
- \path [line] (elaborate) edge[bend right] (tycheck);
- \path [line] (tycheck) edge[bend right] (elaborate);
- \path [line] (elaborate) -- (error);
- \path [line] (error) edge[out=0,in=0] node [near start] {yes} (distill);
- \path [line] (error) -- node [near start] {no} (update);
- \path [line] (update) -- (distill);
- \path [line] (distill) -- (user);
-
-
- \end{tikzpicture}
- }
- \caption{High level overview of the life of a \mykant prompt cycle.}
- \label{fig:kant-process}
-\end{figure}
-
\subsection{Bidirectional type checking}
We start by describing bidirectional type checking since it calls for fairly
two kind of terms: terms for which a type can always be inferred, and terms
that need to be checked against a type. A nice observation is that this
duality runs through the semantics of the terms: data destructors (function
-application, record projections, primitive recursors) \emph{infer} types,
+application, record projections, primitive re cursors) \emph{infer} types,
while data constructors (abstractions, record/data types data constructors)
-need to be checked.
+need to be checked. In the literature these terms are respectively known as
To introduce the concept and notation, we will revisit the STLC in a
-bidirectional style.
-
-\appendix
+bidirectional style. The presentation follows \cite{Loh2010}.
-\section{Notation and syntax}
+% TODO do this --- is it even necessary
-Syntax, derivation rules, and reduction rules, are enclosed in frames describing
-the type of relation being established and the syntactic elements appearing,
-for example
+% The syntax of
-\mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
- \centering{Typing derivations here.}
-}
+\subsection{Base terms and types}
-In the languages presented and Agda code samples I also highlight the syntax,
-following a uniform color and font convention:
+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{center}
- \begin{tabular}{c | l}
- $\mytyc{Sans}$ & Type constructors. \\
- $\mydc{sans}$ & Data constructors. \\
- % $\myfld{sans}$ & Field accessors (e.g. \myfld{fst} and \myfld{snd} for products). \\
- $\mysyn{roman}$ & Keywords of the language. \\
- $\myfun{roman}$ & Defined values and destructors. \\
- $\myb{math}$ & Bound variables.
- \end{tabular}
-\end{center}
+\mydesc{syntax}{ }{
+ $
+ \begin{array}{r@{\ }c@{\ }l}
+ \mytmsyn & ::= & \mynamesyn \mysynsep \mytyp \\
+ & | & \myfora{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
+ \myabs{\myb{x}}{\mytmsyn} \mysynsep
+ (\myapp{\mytmsyn}{\mytmsyn}) \mysynsep
+ (\myann{\mytmsyn}{\mytmsyn}) \\
+ \mynamesyn & ::= & \myb{x} \mysynsep \myfun{f}
+ \end{array}
+ $
+}
-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}.
+The syntax for our calculus includes just two basic constructs:
+abstractions and $\mytyp$s. Everything else will be provided by
+user-definable constructs. Since we let the user define values, we will
+need a context capable of carrying the body of variables along with
+their type. Bound names and defined names are treated separately in the
+syntax, and while both can be associated to a type in the context, only
+defined names can be associated with a body:
-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
+\mydesc{context validity:}{\myvalid{\myctx}}{
+ \begin{tabular}{ccc}
+ \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
+ \UnaryInfC{$\myvalid{\myemptyctx}$}
+ \DisplayProof
+ &
+ \AxiomC{$\myjud{\mytya}{\mytyp}$}
+ \AxiomC{$\mynamesyn \not\in \myctx$}
+ \BinaryInfC{$\myvalid{\myctx ; \mynamesyn : \mytya}$}
+ \DisplayProof
+ &
+ \AxiomC{$\myjud{\mytmt}{\mytya}$}
+ \AxiomC{$\myfun{f} \not\in \myctx$}
+ \BinaryInfC{$\myvalid{\myctx ; \myfun{f} \mapsto \mytmt : \mytya}$}
+ \DisplayProof
+ \end{tabular}
+}
+
+Now we can present the reduction rules, which are unsurprising. We have
+the usual function application ($\beta$-reduction), but also a rule to
+replace names with their bodies ($\delta$-reduction), and one to discard
+type annotations. For this reason reduction is done in-context, as
+opposed to what we have seen in the past:
+
+\mydesc{reduction:}{\myctx \vdash \mytmsyn \myred \mytmsyn}{
+ \begin{tabular}{ccc}
+ \AxiomC{\phantom{$\myb{x} \mapsto \mytmt : \mytya \in \myctx$}}
+ \UnaryInfC{$\myctx \vdash \myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn}
+ \myred \mysub{\mytmm}{\myb{x}}{\mytmn}$}
+ \DisplayProof
+ &
+ \AxiomC{$\myfun{f} \mapsto \mytmt : \mytya \in \myctx$}
+ \UnaryInfC{$\myctx \vdash \myfun{f} \myred \mytmt$}
+ \DisplayProof
+ &
+ \AxiomC{\phantom{$\myb{x} \mapsto \mytmt : \mytya \in \myctx$}}
+ \UnaryInfC{$\myctx \vdash \myann{\mytmm}{\mytya} \myred \mytmm$}
+ \DisplayProof
+ \end{tabular}
+}
+
+We can now give types to our terms. The type of names, both defined and
+abstract, is inferred. 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. We
+defer the question of term equality (which is needed for type checking)
+to section \label{sec:kant-irr}.
+
+\mydesc{typing:}{\myctx \vdash \mytmsyn \Leftrightarrow \mytmsyn}{
+ \begin{tabular}{ccc}
+ \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{$\myinf{\mytmt}{\mytya}$}
+ \UnaryInfC{$\mychk{\myann{\mytmt}{\mytya}}{\mytya}$}
+ \DisplayProof
+ \end{tabular}
+ \myderivsp
+
+ \begin{tabular}{ccc}
+ \AxiomC{$\myinf{\mytmm}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
+ \AxiomC{$\mychk{\mytmn}{\mytya}$}
+ \BinaryInfC{$\myinf{\myapp{\mytmm}{\mytmn}}{\mysub{\mytyb}{\myb{x}}{\mytmn}}$}
+ \DisplayProof
+
+ &
+
+ \AxiomC{$\mychkk{\myctx; \myb{x}: \mytya}{\mytmt}{\mytyb}$}
+ \UnaryInfC{$\mychk{\myabs{\myb{x}}{\mytmt}}{\myfora{\myb{x}}{\mytyb}{\mytyb}}$}
+ \DisplayProof
+ \end{tabular}
+}
+
+\subsection{Elaboration}
+
+As we mentioned, $\mykant$\ allows the user to define not only values
+but also custom data types and records. \emph{Elaboration} consists of
+turning these declarations into workable syntax, types, and reduction
+rules. The treatment of custom types in $\mykant$\ is heavily inspired
+by McBride and McKinna early work on Epigram \citep{McBride2004},
+although with some differences.
+
+\subsubsection{Term vectors, telescopes, and assorted notation}
+
+We use a vector notation to refer to a series of term applied to
+another, for example $\mytyc{D} \myappsp \vec{A}$ is a shorthand for
+$\mytyc{D} \myappsp \mytya_1 \cdots \mytya_n$, for some $n$. $n$ is
+consistently used to refer to the length of such vectors, and $i$ to
+refer to an index in such vectors. We also often need to `build up'
+terms vectors, in which case we use $\myemptyctx$ for an empty vector
+and add elements to an existing vector with $\myarg ; \myarg$, similarly
+to what we do for context.
+
+To present the elaboration and operations on user defined data types, we
+frequently make use what de Bruijn called \emph{telescopes}
+\citep{Bruijn91}, a construct that will prove useful when dealing with
+the types of type and data constructors. A telescope is a series of
+nested typed bindings, such as $(\myb{x} {:} \mynat); (\myb{p} {:}
+\myapp{\myfun{even}}{\myb{x}})$. Consistently with the notation for
+contexts and term vectors, we use $\myemptyctx$ to denote an empty
+telescope and $\myarg ; \myarg$ to add a new binding to an existing
+telescope.
+
+We refer to telescopes with $\mytele$, $\mytele'$, $\mytele_i$, etc. If
+$\mytele$ refers to a telescope, $\mytelee$ refers to the term vector
+made up of all the variables bound by $\mytele$. $\mytele \myarr
+\mytya$ refers to the type made by turning the telescope into a series
+of $\myarr$. Returning to the examples above, we have that
+{\small\[
+ (\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}
+
+\subsubsection{Declarations syntax}
+
+\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 } \\
+
+ \mytelesyn & ::= & \myemptytele \mysynsep \mytelesyn \mycc (\myb{x} {:} \mytmsyn) \\
+ \mynamesyn & ::= & \cdots \mysynsep \mytyc{D} \mysynsep \mytyc{D}.\mydc{c} \mysynsep \mytyc{D}.\myfun{f}
+ \end{array}
+ $
+}
+
+In \mykant\ we have four kind of declarations:
+
+\begin{description}
+\item[Defined value] A variable, together with a type and a body.
+\item[Abstract variable] An abstract variable, with a type but no body.
+\item[Inductive data] A datatype, with a type constructor and various data
+ constructors---somewhat similar to what we find in Haskell. A primitive
+ recursor (or `destructor') will be generated automatically.
+\item[Record] A record, which consists of one data constructor and various
+ fields, with no recursive occurrences.
+\end{description}
+
+Elaborating defined variables consists of type checking body against the
+given type, and updating the context to contain the new binding.
+Elaborating abstract variables and abstract variables consists of type
+checking the type, and updating the context with a new typed variable:
+
+\mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
+ \begin{tabular}{cc}
+ \AxiomC{$\myjud{\mytmt}{\mytya}$}
+ \AxiomC{$\myfun{f} \not\in \myctx$}
+ \BinaryInfC{
+ $\myctx \myelabt \myval{\myfun{f}}{\mytya}{\mytmt} \ \ \myelabf\ \ \myctx; \myfun{f} \mapsto \mytmt : \mytya$
+ }
+ \DisplayProof
+ &
+ \AxiomC{$\myjud{\mytya}{\mytyp}$}
+ \AxiomC{$\myfun{f} \not\in \myctx$}
+ \BinaryInfC{
+ $
+ \myctx \myelabt \mypost{\myfun{f}}{\mytya}
+ \ \ \myelabf\ \ \myctx; \myfun{f} : \mytya
+ $
+ }
+ \DisplayProof
+ \end{tabular}
+}
+
+\subsubsection{User defined types}
+\label{sec:user-type}
+
+Elaborating user defined types is the real effort. First, let's explain
+what we can defined, with some examples.
+
+\begin{description}
+\item[Natural numbers] To define natural numbers, we create a data type
+ with two constructors: one with zero arguments ($\mydc{zero}$) and one
+ with one recursive argument ($\mydc{suc}$):
+ {\small\[
+ \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:
+ {\small\[\text{\texttt{data Nat = Zero | Suc Nat}}\]}
+ Once the data type is defined, $\mykant$\ will generate syntactic
+ constructs for the type and data constructors, so that we will have
+ \begin{center}
+ \small
+ \begin{tabular}{ccc}
+ \AxiomC{\phantom{$\mychk{\mytmt}{\mynat}$}}
+ \UnaryInfC{$\myinf{\mynat}{\mytyp}$}
+ \DisplayProof
+ &
+ \AxiomC{\phantom{$\mychk{\mytmt}{\mynat}$}}
+ \UnaryInfC{$\myinf{\mytyc{\mynat}.\mydc{zero}}{\mynat}$}
+ \DisplayProof
+ &
+ \AxiomC{$\mychk{\mytmt}{\mynat}$}
+ \UnaryInfC{$\myinf{\mytyc{\mynat}.\mydc{suc} \myappsp \mytmt}{\mynat}$}
+ \DisplayProof
+ \end{tabular}
+ \end{center}
+ While in Haskell (or indeed in Agda or Coq) data constructors are
+ treated the same way as functions, in $\mykant$\ they are syntax, so
+ for example using $\mytyc{\mynat}.\mydc{suc}$ on its own will be a
+ syntax error. This is necessary so that we can easily infer the type
+ of polymorphic data constructors, as we will see later.
+
+ Moreover, each data constructor is prefixed by the type constructor
+ name, since we need to retrieve the type constructor of a data
+ constructor when type checking. This measure aids in the presentation
+ of various features but it is not needed in the implementation, where
+ we can have a dictionary to lookup the type constructor corresponding
+ to each data constructor. When using data constructors in examples I
+ will omit the type constructor prefix for brevity.
+
+ Along with user defined constructors, $\mykant$\ automatically
+ generates an \emph{eliminator}, or \emph{destructor}, to compute with
+ natural numbers: If we have $\mytmt : \mynat$, we can destruct
+ $\mytmt$ using the generated eliminator `$\mynat.\myfun{elim}$':
+ \begin{prooftree}
+ \small
+ \AxiomC{$\mychk{\mytmt}{\mynat}$}
+ \UnaryInfC{$
+ \myinf{\mytyc{\mynat}.\myfun{elim} \myappsp \mytmt}{
+ \begin{array}{@{}l}
+ \myfora{\myb{P}}{\mynat \myarr \mytyp}{ \\ \myapp{\myb{P}}{\mydc{zero}} \myarr (\myfora{\myb{x}}{\mynat}{\myapp{\myb{P}}{\myb{x}} \myarr \myapp{\myb{P}}{(\myapp{\mydc{suc}}{\myb{x}})}}) \myarr \\ \myapp{\myb{P}}{\mytmt}}
+ \end{array}
+ }$}
+ \end{prooftree}
+ $\mynat.\myfun{elim}$ corresponds to the induction principle for
+ natural numbers: if we have a predicate on numbers ($\myb{P}$), and we
+ know that predicate holds for the base case
+ ($\myapp{\myb{P}}{\mydc{zero}}$) and for each inductive step
+ ($\myfora{\myb{x}}{\mynat}{\myapp{\myb{P}}{\myb{x}} \myarr
+ \myapp{\myb{P}}{(\myapp{\mydc{suc}}{\myb{x}})}}$), then $\myb{P}$
+ holds for any number. As with the data constructors, we require the
+ eliminator to be applied to the `destructed' element.
+
+ While the induction principle is usually seen as a mean to prove
+ properties about numbers, in the intuitionistic setting it is also a
+ mean to compute. In this specific case we will $\mynat.\myfun{elim}$
+ will return the base case if the provided number is $\mydc{zero}$, and
+ recursively apply the inductive step if the number is a
+ $\mydc{suc}$cessor:
+ {\small\[
+ \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
+ {\small\[
+ \begin{array}{@{}l}
+ \text{\texttt{elim :: Nat -> a -> (Nat -> a -> a) -> a}}\\
+ \text{\texttt{elim Zero pz ps = pz}}\\
+ \text{\texttt{elim (Suc n) pz ps = ps n (elim n pz ps)}}
+ \end{array}
+ \]}
+ Which buys us the computational behaviour, but not the reasoning power.
+ % TODO maybe more examples, e.g. Haskell eliminator and fibonacci
+
+\item[Binary trees] Now for a polymorphic data type: binary trees, since
+ lists are too similar to natural numbers to be interesting.
+ {\small\[
+ \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:
+ {\small\[
+ \begin{array}{@{}l@{\ }l}
+ \mydc{leaf} & : \myfora{\myb{A}}{\mytyp}{\myapp{\mytree}{\myb{A}}} \\
+ \mydc{node} & : \myfora{\myb{A}}{\mytyp}{\myapp{\mytree}{\myb{A}} \myarr \myb{A} \myarr \myapp{\mytree}{\myb{A}} \myarr \myapp{\mytree}{\myb{A}}}
+ \end{array}
+ \]}
+ The problem with this approach is that creating terms is incredibly
+ verbose and dull, since we would need to specify the type parameters
+ each time. For example if we wished to create a $\mytree \myappsp
+ \mynat$ with two nodes and three leaves, we would have to write
+ {\small\[
+ \mydc{node} \myappsp \mynat \myappsp (\mydc{node} \myappsp \mynat \myappsp (\mydc{leaf} \myappsp \mynat) \myappsp (\myapp{\mydc{suc}}{\mydc{zero}}) \myappsp (\mydc{leaf} \myappsp \mynat)) \myappsp \mydc{zero} \myappsp (\mydc{leaf} \myappsp \mynat)
+ \]}
+ The redundancy of $\mynat$s is quite irritating. Instead, if we treat
+ constructors as syntactic elements, we can `extract' the type of the
+ parameter from the type that the term gets checked against, much like
+ we get the type of abstraction arguments:
+ \begin{center}
+ \small
+ \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
+ {\small\[
+ \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}
+ \footnotesize
+ \AxiomC{$\myinf{\mytmt}{\myapp{\mytree}{\mytya}}$}
+ \UnaryInfC{$
+ \myinf{\mytree.\myfun{elim} \myappsp \mytmt}{
+ \begin{array}{@{}l}
+ (\myb{P} {:} \myapp{\mytree}{\mytya} \myarr \mytyp) \myarr \\
+ \myapp{\myb{P}}{\mydc{leaf}} \myarr \\
+ ((\myb{l} {:} \myapp{\mytree}{\mytya}) (\myb{x} {:} \mytya) (\myb{r} {:} \myapp{\mytree}{\mytya}) \myarr \myapp{\myb{P}}{\myb{l}} \myarr
+ \myapp{\myb{P}}{\myb{r}} \myarr \myb{P} \myappsp (\mydc{node} \myappsp \myb{l} \myappsp \myb{x} \myappsp \myb{r})) \myarr \\
+ \myapp{\myb{P}}{\mytmt}
+ \end{array}
+ }
+ $}
+ \end{prooftree}
+ As expected, the eliminator embodies structural induction on trees.
+
+\item[Empty type] We have presented types that have at least one
+ constructors, but nothing prevents us from defining types with
+ \emph{no} constructors:
+ {\small\[
+ \myadt{\mytyc{Empty}}{ }{ }{ }
+ \]}
+ What shall the `induction principle' on $\mytyc{Empty}$ be? Does it
+ even make sense to talk about induction on $\mytyc{Empty}$?
+ $\mykant$\ does not care, and generates an eliminator with no `cases',
+ and thus corresponding to the $\myfun{absurd}$ that we know and love:
+ \begin{prooftree}
+ \small
+ \AxiomC{$\myinf{\mytmt}{\mytyc{Empty}}$}
+ \UnaryInfC{$\myinf{\myempty.\myfun{elim} \myappsp \mytmt}{(\myb{P} {:} \mytmt \myarr \mytyp) \myarr \myapp{\myb{P}}{\mytmt}}$}
+ \end{prooftree}
+
+\item[Ordered lists] Up to this point, the examples shown are nothing
+ new to the \{Haskell, SML, OCaml, functional\} programmer. However
+ dependent types let us express much more than that. A useful example
+ is the type of ordered lists. There are many ways to define such a
+ thing, we will define our type to store the bounds of the list, making
+ sure that $\mydc{cons}$ing respects that.
+
+ First, using $\myunit$ and $\myempty$, we define a type expressing the
+ ordering on natural numbers, $\myfun{le}$---`less or equal'.
+ $\myfun{le}\myappsp \mytmm \myappsp \mytmn$ will be inhabited only if
+ $\mytmm \le \mytmn$:
+ {\small\[
+ \begin{array}{@{}l}
+ \myfun{le} : \mynat \myarr \mynat \myarr \mytyp \mapsto \\
+ \myind{2} \myabs{\myb{n}}{\\
+ \myind{2}\myind{2} \mynat.\myfun{elim} \\
+ \myind{2}\myind{2}\myind{2} \myb{n} \\
+ \myind{2}\myind{2}\myind{2} (\myabs{\myarg}{\mynat \myarr \mytyp}) \\
+ \myind{2}\myind{2}\myind{2} (\myabs{\myarg}{\myunit}) \\
+ \myind{2}\myind{2}\myind{2} (\myabs{\myb{n}\, \myb{f}\, \myb{m}}{
+ \mynat.\myfun{elim} \myappsp \myb{m} \myappsp (\myabs{\myarg}{\mytyp}) \myappsp \myempty \myappsp (\myabs{\myb{m'}\, \myarg}{\myapp{\myb{f}}{\myb{m'}}})
+ })
+ }
+ \end{array}
+ \]} We return $\myunit$ if the scrutinised is $\mydc{zero}$ (every
+ number in less or equal than zero), $\myempty$ if the first number is
+ a $\mydc{suc}$cessor and the second a $\mydc{zero}$, and we recurse if
+ they are both successors. Since we want the list to have possibly
+ `open' bounds, for example for empty lists, we create a type for
+ `lifted' naturals with a bottom (less than everything) and top
+ (greater than everything) elements, along with an associated comparison
+ function:
+ {\small\[
+ \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 \mapsto \cdots \\
+ \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:
+ {\small\[
+ \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 (\myfun{le'} \myappsp \myb{low} \myappsp (\myfun{lift} \myappsp \myb{n})
+ }
+ \end{array}
+ \]} If we want we can then employ this structure to write and prove
+ correct various sorting algorithms\footnote{See this presentation by
+ Conor McBride:
+ \url{https://personal.cis.strath.ac.uk/conor.mcbride/Pivotal.pdf},
+ and this blog post by the author:
+ \url{http://mazzo.li/posts/AgdaSort.html}.}.
+
+ % TODO
+
+\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:
+ {\small\[
+ \begin{array}{@{}l}
+ \myreco{\mytyc{Prod}}{\myappsp (\myb{A} {:} \mytyp) \myappsp (\myb{B} {:} \myb{A} \myarr \mytyp)}{\\ \myind{2}}{\myfst : \myb{A}, \mysnd : \myapp{\myb{B}}{\myb{fst}}}
+ \end{array}
+ \]}
+ Here $\myfst$ and $\mysnd$ are the projections, with their respective
+ types. Note that each field can refer to the preceding fields. A
+ constructor will be automatically generated, under the name of
+ $\mytyc{Prod}.\mydc{constr}$. Dually to data types, we will omit the
+ type constructor prefix for record projections.
+
+ Following the bidirectionality of the system, we have that projections
+ (the destructors of the record) infer the type, while the constructor
+ gets checked:
+ \begin{center}
+ \small
+ \begin{tabular}{cc}
+ \AxiomC{$\mychk{\mytmm}{\mytya}$}
+ \AxiomC{$\mychk{\mytmn}{\myapp{\mytyb}{\mytmm}}$}
+ \BinaryInfC{$\mychk{\mytyc{Prod}.\mydc{constr} \myappsp \mytmm \myappsp \mytmn}{\mytyc{Prod} \myappsp \mytya \myappsp \mytyb}$}
+ \noLine
+ \UnaryInfC{\phantom{$\myinf{\myfun{snd} \myappsp \mytmt}{\mytyb \myappsp (\myfst \myappsp \mytmt)}$}}
+ \DisplayProof
+ &
+ \AxiomC{$\myinf{\mytmt}{\mytyc{Prod} \myappsp \mytya \myappsp \mytyb}$}
+ \UnaryInfC{$\myinf{\myfun{fst} \myappsp \mytmt}{\mytya}$}
+ \noLine
+ \UnaryInfC{$\myinf{\myfun{snd} \myappsp \mytmt}{\mytyb \myappsp (\myfst \myappsp \mytmt)}$}
+ \DisplayProof
+ \end{tabular}
+ \end{center}
+ What we have is equivalent to ITT's dependent products.
+\end{description}
+
+\begin{figure}[p]
+ \begin{subfigure}[b]{\textwidth}
+ \vspace{-1cm}
+ \mydesc{syntax}{ }{
+ \footnotesize
+ $
+ \begin{array}{l}
+ \mynamesyn ::= \cdots \mysynsep \mytyc{D} \mysynsep \mytyc{D}.\mydc{c} \mysynsep \mytyc{D}.\myfun{f}
+ \end{array}
+ $
+ }
+
+ \mydesc{syntax elaboration:}{\mydeclsyn \myelabf \mytmsyn ::= \cdots}{
+ \footnotesize
+ $
+ \begin{array}{r@{\ }l}
+ & \myadt{\mytyc{D}}{\mytele}{}{\cdots\ |\ \mydc{c}_n : \mytele_n } \\
+ \myelabf &
+
+ \begin{array}{r@{\ }c@{\ }l}
+ \mytmsyn & ::= & \cdots \mysynsep \myapp{\mytyc{D}}{\mytmsyn^{\mytele}} \mysynsep \cdots \mysynsep
+ \mytyc{D}.\mydc{c}_n \myappsp \mytmsyn^{\mytele_n} \mysynsep \mytyc{D}.\myfun{elim} \myappsp \mytmsyn \\
+ \end{array}
+ \end{array}
+ $
+ }
+
+ \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
+ \footnotesize
+
+ \AxiomC{$
+ \begin{array}{c}
+ \myinf{\mytele \myarr \mytyp}{\mytyp}\hspace{0.8cm}
+ \mytyc{D} \not\in \myctx \\
+ \myinff{\myctx;\ \mytyc{D} : \mytele \myarr \mytyp}{\mytele \mycc \mytele_i \myarr \myapp{\mytyc{D}}{\mytelee}}{\mytyp}\ \ \ (1 \leq i \leq n) \\
+ \text{For each $(\myb{x} {:} \mytya)$ in each $\mytele_i$, if $\mytyc{D} \in \mytya$, then $\mytya = \myapp{\mytyc{D}}{\vec{\mytmt}}$.}
+ \end{array}
+ $}
+ \UnaryInfC{$
+ \begin{array}{r@{\ }c@{\ }l}
+ \myctx & \myelabt & \myadt{\mytyc{D}}{\mytele}{}{ \cdots \ |\ \mydc{c}_n : \mytele_n } \\
+ & & \vspace{-0.2cm} \\
+ & \myelabf & \myctx;\ \mytyc{D} : \mytele \myarr \mytyp;\ \cdots;\ \mytyc{D}.\mydc{c}_n : \mytele \mycc \mytele_n \myarr \myapp{\mytyc{D}}{\mytelee}; \\
+ & &
+ \begin{array}{@{}r@{\ }l l}
+ \mytyc{D}.\myfun{elim} : & \mytele \myarr (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr & \textbf{target} \\
+ & (\myb{P} {:} \myapp{\mytyc{D}}{\mytelee} \myarr \mytyp) \myarr & \textbf{motive} \\
+ & \left.
+ \begin{array}{@{}l}
+ \myind{3} \vdots \\
+ (\mytele_n \mycc \myhyps(\myb{P}, \mytele_n) \myarr \myapp{\myb{P}}{(\myapp{\mytyc{D}.\mydc{c}_n}{\mytelee_n})}) \myarr
+ \end{array} \right \}
+ & \textbf{methods} \\
+ & \myapp{\myb{P}}{\myb{x}} &
+ \end{array}
+ \end{array}
+ $}
+ \DisplayProof \\ \vspace{0.2cm}\ \\
+ $
+ \begin{array}{@{}l l@{\ } l@{} r c l}
+ \textbf{where} & \myhyps(\myb{P}, & \myemptytele &) & \mymetagoes & \myemptytele \\
+ & \myhyps(\myb{P}, & (\myb{r} {:} \myapp{\mytyc{D}}{\vec{\mytmt}}) \mycc \mytele &) & \mymetagoes & (\myb{r'} {:} \myapp{\myb{P}}{\myb{r}}) \mycc \myhyps(\myb{P}, \mytele) \\
+ & \myhyps(\myb{P}, & (\myb{x} {:} \mytya) \mycc \mytele & ) & \mymetagoes & \myhyps(\myb{P}, \mytele)
+ \end{array}
+ $
+
+ }
+
+ \mydesc{reduction elaboration:}{\mydeclsyn \myelabf \myctx \vdash \mytmsyn \myred \mytmsyn}{
+ \footnotesize
+ $\myadt{\mytyc{D}}{\mytele}{}{ \cdots \ |\ \mydc{c}_n : \mytele_n } \ \ \myelabf$
+ \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
+ \AxiomC{$\mytyc{D}.\mydc{c}_i : \mytele;\mytele_i \myarr \myapp{\mytyc{D}}{\mytelee} \in \myctx$}
+ \BinaryInfC{$
+ \myctx \vdash \myapp{\myapp{\myapp{\mytyc{D}.\myfun{elim}}{(\myapp{\mytyc{D}.\mydc{c}_i}{\vec{\myse{t}}})}}{\myse{P}}}{\vec{\myse{m}}} \myred \myapp{\myapp{\myse{m}_i}{\vec{\mytmt}}}{\myrecs(\myse{P}, \vec{m}, \mytele_i)}
+ $}
+ \DisplayProof \\ \vspace{0.2cm}\ \\
+ $
+ \begin{array}{@{}l l@{\ } l@{} r c l}
+ \textbf{where} & \myrecs(\myse{P}, \vec{m}, & \myemptytele &) & \mymetagoes & \myemptytele \\
+ & \myrecs(\myse{P}, \vec{m}, & (\myb{r} {:} \myapp{\mytyc{D}}{\vec{A}}); \mytele & ) & \mymetagoes & (\mytyc{D}.\myfun{elim} \myappsp \myb{r} \myappsp \myse{P} \myappsp \vec{m}); \myrecs(\myse{P}, \vec{m}, \mytele) \\
+ & \myrecs(\myse{P}, \vec{m}, & (\myb{x} {:} \mytya); \mytele &) & \mymetagoes & \myrecs(\myse{P}, \vec{m}, \mytele)
+ \end{array}
+ $
+ }
+ \end{subfigure}
+
+ \begin{subfigure}[b]{\textwidth}
+ \mydesc{syntax elaboration:}{\myelab{\mydeclsyn}{\mytmsyn ::= \cdots}}{
+ \footnotesize
+ $
+ \begin{array}{r@{\ }c@{\ }l}
+ \myctx & \myelabt & \myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \\
+ & \myelabf &
+
+ \begin{array}{r@{\ }c@{\ }l}
+ \mytmsyn & ::= & \cdots \mysynsep \myapp{\mytyc{D}}{\mytmsyn^{\mytele}} \mysynsep \mytyc{D}.\mydc{constr} \myappsp \mytmsyn^{n} \mysynsep \cdots \mysynsep \mytyc{D}.\myfun{f}_n \myappsp \mytmsyn \\
+ \end{array}
+ \end{array}
+ $
+}
+
+
+\mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
+ \footnotesize
+ \AxiomC{$
+ \begin{array}{c}
+ \myinf{\mytele \myarr \mytyp}{\mytyp}\hspace{0.8cm}
+ \mytyc{D} \not\in \myctx \\
+ \myinff{\myctx; \mytele; (\myb{f}_j : \myse{F}_j)_{j=1}^{i - 1}}{F_i}{\mytyp} \myind{3} (1 \le i \le n)
+ \end{array}
+ $}
+ \UnaryInfC{$
+ \begin{array}{r@{\ }c@{\ }l}
+ \myctx & \myelabt & \myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \\
+ & & \vspace{-0.2cm} \\
+ & \myelabf & \myctx;\ \mytyc{D} : \mytele \myarr \mytyp;\ \cdots;\ \mytyc{D}.\myfun{f}_n : \mytele \myarr (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr \mysub{\myse{F}_n}{\myb{f}_i}{\myapp{\myfun{f}_i}{\myb{x}}}_{i = 1}^{n-1}; \\
+ & & \mytyc{D}.\mydc{constr} : \mytele \myarr \myse{F}_1 \myarr \cdots \myarr \myse{F}_n \myarr \myapp{\mytyc{D}}{\mytelee};
+ \end{array}
+ $}
+ \DisplayProof
+}
+
+ \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
+ }
+
+ \end{subfigure}
+ \caption{Elaboration for data types and records.}
+ \label{fig:elab}
+\end{figure}
+
+Following the intuition given by the examples, the mechanised
+elaboration is presented in figure \ref{fig:elab}, which is essentially
+a modification of figure 9 of \citep{McBride2004}\footnote{However, our
+ datatypes do not have indices, we do bidirectional typechecking by
+ treating constructors/destructors as syntactic constructs, and we have
+ records.}.
+
+In data types declarations we allow recursive occurrences as long as
+they are \emph{strictly positive}, employing a syntactic check to make
+sure that this is the case. See \cite{Dybjer1991} for a more formal
+treatment of inductive definitions in ITT.
+
+For what concerns records, recursive occurrences are disallowed. The
+reason for this choice is answered by the reason for the choice of
+having records at all: we need records to give the user types with
+$\eta$-laws for equality, as we saw in section % TODO add section
+and in the treatment of OTT in section \ref{sec:ott}. If we tried to
+$\eta$-expand recursive data types, we would expand forever.
+
+To implement bidirectional type checking for constructors and
+destructors, we store their types in full in the context, and then
+instantiate when due:
+
+\mydesc{typing:}{ }{
+ \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
+
+ \myderivsp
+
+ \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?}
+
+% TODO reference levitated theories, indexed containers
+
+foobar
+
+\subsection{Cumulative hierarchy and typical ambiguity}
+\label{sec:term-hierarchy}
+
+A type hierarchy as presented in section \label{sec:itt} is a
+considerable burden on the user, on various levels. Consider for
+example how we recovered disjunctions in section \ref{sec:disju}: we
+have a function that takes two $\mytyp_0$ and forms a new $\mytyp_0$.
+What if we wanted to form a disjunction containing two $\mytyp_0$, or
+$\mytyp_{42}$? Our definition would fail us, since $\mytyp_0 :
+\mytyp_1$.
+
+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. For example we might define our disjunction to be
+{\small\[
+ \myarg\myfun{$\vee$}\myarg : \mytyp_{100} \myarr \mytyp_{100} \myarr \mytyp_{100}
+\]}
+And hope that $\mytyp_{100}$ will be large enough to fit all the types
+that we want to use with our disjunction. However, there are two
+problems with this. First, there is the obvious clumsyness of having to
+manually specify the size of types. More importantly, if we want to use
+$\myfun{$\vee$}$ itself as an argument to other type-formers, we need to
+make sure that those allow for types at least as large as
+$\mytyp_{100}$.
+
+A better option is to employ a mechanised version of what Russell called
+\emph{typical ambiguity}: we let the user live under the illusion that
+$\mytyp : \mytyp$, but check that the statements about types are
+consistent behind the hood. $\mykant$\ implements this following the
+lines of \cite{Huet1988}. See also \citep{Harper1991} for a published
+reference, although describing a more complex system allowing for both
+explicit and explicit hierarchy at the same time.
+
+We define a partial ordering on the levels, with both weak ($\le$) and
+strong ($<$) constraints---the laws governing them being the same as the
+ones governing $<$ and $\le$ for the natural numbers. Each occurrence
+of $\mytyp$ is decorated with a unique reference, and we keep a set of
+constraints and add new constraints as we type check, generating new
+references when needed.
+
+For example, when type checking the type $\mytyp\, r_1$, where $r_1$
+denotes the unique reference assigned to that term, we will generate a
+new fresh reference $\mytyp\, r_2$, and add the constraint $r_1 < r_2$
+to the set. When type checking $\myctx \vdash
+\myfora{\myb{x}}{\mytya}{\mytyb}$, if $\myctx \vdash \mytya : \mytyp\,
+r_1$ and $\myctx; \myb{x} : \mytyb \vdash \mytyb : \mytyp\,r_2$; we will
+generate new reference $r$ and add $r_1 \le r$ and $r_2 \le r$ to the
+set.
+
+If at any point the constraint set becomes inconsistent, type checking
+fails. Moreover, when comparing two $\mytyp$ terms we equate their
+respective references with two $\le$ constraints---the details are
+explained in section \ref{sec:hier-impl}.
+
+Another more flexible but also more verbose alternative is the one
+chosen by Agda, where levels can be quantified so that the relationship
+between arguments and result in type formers can be explicitly
+expressed:
+{\small\[
+\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.
+
+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 footsteps. Most of the work, as an extension of elaboration,
+is to generate reduction rules and coercions.
+
+\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{framed}
+\small
+$
+\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}
+$
+\end{framed}
+When using $\mytyc{Prod}$, we shall use $\myprod$ to define `nested'
+products, and $\myproj{n}$ to project elements from them, so that
+{\small
+\[
+\begin{array}{@{}l}
+\mytya \myprod \mytyb = \mytyc{Prod} \myappsp \mytya \myappsp (\mytyc{Prod} \myappsp \mytyb \myappsp \myunit) \\
+\mytya \myprod \mytyb \myprod \myse{C} = \mytyc{Prod} \myappsp \mytya \myappsp (\mytyc{Prod} \myappsp \mytyb \myappsp (\mytyc{Prod} \myappsp \mytyc \myappsp \myunit)) \\
+\myind{2} \vdots \\
+\myproj{1} : \mytyc{Prod} \myappsp \mytya \myappsp \mytyb \myarr \mytya \\
+\myproj{2} : \mytyc{Prod} \myappsp \mytya \myappsp (\mytyc{Prod} \myappsp \mytyb \myappsp \myse{C}) \myarr \mytyb \\
+\myind{2} \vdots
+\end{array}
+\]
+}
+And so on, so that $\myproj{n}$ will work with all products with at
+least than $n$ elements. Then we can define propositions, and decoding:
+
+\mydesc{syntax}{ }{
+ $
+ \begin{array}{r@{\ }c@{\ }l}
+ \mytmsyn & ::= & \cdots \mysynsep \myprdec{\myprsyn} \\
+ \myprsyn & ::= & \mybot \mysynsep \mytop \mysynsep \myprsyn \myand \myprsyn \mysynsep \myprfora{\myb{x}}{\mytmsyn}{\myprsyn}
+ \end{array}
+ $
+}
+
+\mydesc{proposition decoding:}{\myprdec{\mytmsyn} \myred \mytmsyn}{
+ \begin{tabular}{cc}
+ $
+ \begin{array}{l@{\ }c@{\ }l}
+ \myprdec{\mybot} & \myred & \myempty \\
+ \myprdec{\mytop} & \myred & \myunit
+ \end{array}
+ $
+ &
+ $
+ \begin{array}{r@{ }c@{ }l@{\ }c@{\ }l}
+ \myprdec{&\myse{P} \myand \myse{Q} &} & \myred & \myprdec{\myse{P}} \myprod \myprdec{\myse{Q}} \\
+ \myprdec{&\myprfora{\myb{x}}{\mytya}{\myse{P}} &} & \myred &
+ \myfora{\myb{x}}{\mytya}{\myprdec{\myse{P}}}
+ \end{array}
+ $
+ \end{tabular}
+}
+
+\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 that is what The author initially planned to
+identify the propositional fragment internally \cite{Jacobs1994}.
+
+% TODO finish
+
+\subsubsection{OTT constructs}
+
+Before presenting the direction that $\mykant$\ takes, let's consider
+some examples of use-defined data types, and the result we would expect,
+given what we already know about OTT, assuming the same propositional
+equalities.
+
+\begin{description}
+
+\item[Product types] Let's consider first the already mentioned
+ dependent product, using the alternate name $\mysigma$\footnote{For
+ extra confusion, `dependent products' are often called `dependent
+ sums' in the literature, referring to the interpretation that
+ identifies the first element as a `tag' deciding the type of the
+ second element, which lets us recover sum types (disjuctions), as we
+ saw in section \ref{sec:user-type}. Thus, $\mysigma$.} to
+ avoid confusion with the $\mytyc{Prod}$ in the prelude: {\small\[
+ \begin{array}{@{}l}
+ \myreco{\mysigma}{\myappsp (\myb{A} {:} \mytyp) \myappsp (\myb{B} {:} \myb{A} \myarr \mytyp)}{\\ \myind{2}}{\myfst : \myb{A}, \mysnd : \myapp{\myb{B}}{\myb{fst}}}
+ \end{array}
+ \]} Let's start with type-level equality. The result we want is
+ {\small\[
+ \begin{array}{@{}l}
+ \mysigma \myappsp \mytya_1 \myappsp \mytyb_1 \myeq \mysigma \myappsp \mytya_2 \myappsp \mytyb_2 \myred \\
+ \myind{2} \mytya_1 \myeq \mytya_2 \myand \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{\myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2}} \myimpl \myapp{\mytyb_1}{\myb{x_1}} \myeq \myapp{\mytyb_2}{\myb{x_2}}}
+ \end{array}
+ \]} The difference here is that in the original presentation of OTT
+ the type binders are explicit, while here $\mytyb_1$ and $\mytyb_2$
+ functions returning types. We can do this thanks to the type
+ hierarchy, and this hints at the fact that heterogeneous equality will
+ have to allow $\mytyp$ `to the right of the colon', and in fact this
+ provides the solution to simplify the equality above.
+
+ If we take, just like we saw previously in OTT
+ {\small\[
+ \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
+ {\small\[
+ \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, coercions, and quotation; as to not
+ impede progress if not necessary.
+
+\item[Lists] Now for finite lists, which will give us a taste for data
+ constructors:
+ {\small\[
+ \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:
+ {\small\[
+ \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: {\small\[
+ \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}$: {\small\[
+ \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}
+ \]}
+ Finally, quotation
+ % TODO quotation
+
+
+
+
+\end{description}
+
+
+\mydesc{syntax}{ }{
+ $
+ \begin{array}{r@{\ }c@{\ }l}
+ \mytmsyn & ::= & \cdots \mysynsep \mycoee{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \mysynsep
+ \mycohh{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
+ \myprsyn & ::= & \cdots \mysynsep \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
+ \end{array}
+ $
+}
+
+\begin{figure}[p]
+\mydesc{typing:}{\myctx \vdash \myprsyn \myred \myprsyn}{
+ \footnotesize
+ \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}}{
+ \footnotesize
+ \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}
+
+ \myderivsp
+
+ \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}
+}
+ % TODO equality for decodings
+\mydesc{equality reduction:}{\myctx \vdash \myprsyn \myred \myprsyn}{
+ \footnotesize
+ \AxiomC{}
+ \UnaryInfC{$\myctx \vdash \myjm{\mytyp}{\mytyp}{\mytyp}{\mytyp} \myred \mytop$}
+ \DisplayProof
+
+ \myderivsp
+
+ \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 \myeq \mytyb_2
+ }}
+ \end{array}
+ $}
+ \DisplayProof
+
+ \myderivsp
+
+ \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
+
+
+ \myderivsp
+
+ \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
+
+ \myderivsp
+
+ \AxiomC{$
+ \begin{array}{@{}c}
+ \mydataty(\mytyc{D}, \myctx)\hspace{0.8cm}
+ \mytyc{D}.\mydc{c} : \mytele;\mytele' \myarr \mytyc{D} \myappsp \mytelee \in \myctx \\
+ \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
+
+ \myderivsp
+
+ \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
+
+ \myderivsp
+
+ \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
+
+ \myderivsp
+ \AxiomC{}
+ \UnaryInfC{$\myjm{\mytmm}{\mytya}{\mytmn}{\mytyb} \myred \mybot\ \text{if $\mytya$ and $\mytyb$ are canonical types.}$}
+ \DisplayProof
+}
+ \caption{Equality reduction for $\mykant$.}
+ \label{fig:kant-eq-red}
+\end{figure}
+
+\subsubsection{$\myprop$ and the hierarchy}
+
+Where is $\myprop$ placed in the $\mytyp$ hierarchy? At each universe
+level, we will have that
+
+\subsubsection{Quotation and irrelevance}
+\ref{sec:kant-irr}
+
+foo
+
+\section{\mykant : The practice}
+\label{sec:kant-practice}
+
+The codebase consists of around 2500 lines of Haskell, as reported by
+the \texttt{cloc} utility. The high level design is inspired by Conor
+McBride's work on various incarnations of Epigram, and specifically by
+the first version as described \citep{McBride2004} and the codebase for
+the new version \footnote{Available intermittently as a \texttt{darcs}
+ repository at \url{http://sneezy.cs.nott.ac.uk/darcs/Pig09}.}. In
+many ways \mykant\ is something in between the first and second version
+of Epigram.
+
+The interaction happens in a read-eval-print loop (REPL). The REPL is a
+available both as a commandline application and in a web interface,
+which is available at \url{kant.mazzo.li} and presents itself as in
+figure \ref{fig:kant-web}.
+
+\begin{figure}
+ \centering{
+ \includegraphics[scale=1.0]{kant-web.png}
+ }
+ \caption{The \mykant\ web prompt.}
+ \label{fig:kant-web}
+\end{figure}
+
+The interaction with the user takes place in a loop living in and updating a
+context \mykant\ declarations. The user inputs a new declaration that goes
+through various stages starts with the user inputing a \mykant\ declaration or
+another REPL command, which then goes through various stages that can end up
+in a context update, or in failures of various kind. The process is described
+diagrammatically in figure \ref{fig:kant-process}:
+
+\begin{description}
+\item[Parse] In this phase the text input gets converted to a sugared
+ version of the core language.
+
+\item[Desugar] The sugared declaration is converted to a core term.
+
+\item[Reference] Occurrences of $\mytyp$ get decorated by a unique reference,
+ which is necessary to implement the type hierarchy check.
+
+\item[Elaborate] 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[Pretty print] Format the terms in a nice way, and display the result to
+ the user.
+
+\end{description}
+
+\begin{figure}
+ \centering{\small
+ \tikzstyle{block} = [rectangle, draw, text width=5em, text centered, rounded
+ corners, minimum height=2.5em, node distance=0.7cm]
+
+ \tikzstyle{decision} = [diamond, draw, text width=4.5em, text badly
+ centered, inner sep=0pt, node distance=0.7cm]
+
+ \tikzstyle{line} = [draw, -latex']
+
+ \tikzstyle{cloud} = [draw, ellipse, minimum height=2em, text width=5em, text
+ centered, node distance=1.5cm]
+
+
+ \begin{tikzpicture}[auto]
+ \node [cloud] (user) {User};
+ \node [block, below left=1cm and 0.1cm of user] (parse) {Parse};
+ \node [block, below=of parse] (desugar) {Desugar};
+ \node [block, below=of desugar] (reference) {Reference};
+ \node [block, below=of reference] (elaborate) {Elaborate};
+ \node [block, left=of elaborate] (tycheck) {Typecheck};
+ \node [block, left=of tycheck] (evaluate) {Evaluate};
+ \node [decision, right=of elaborate] (error) {Error?};
+ \node [block, right=of parse] (distill) {Distill};
+ \node [block, right=of desugar] (update) {Update context};
+
+ \path [line] (user) -- (parse);
+ \path [line] (parse) -- (desugar);
+ \path [line] (desugar) -- (reference);
+ \path [line] (reference) -- (elaborate);
+ \path [line] (elaborate) edge[bend right] (tycheck);
+ \path [line] (tycheck) edge[bend right] (elaborate);
+ \path [line] (elaborate) -- (error);
+ \path [line] (error) edge[out=0,in=0] node [near start] {yes} (distill);
+ \path [line] (error) -- node [near start] {no} (update);
+ \path [line] (update) -- (distill);
+ \path [line] (distill) -- (user);
+ \path [line] (tycheck) edge[bend right] (evaluate);
+ \path [line] (evaluate) edge[bend right] (tycheck);
+ \end{tikzpicture}
+ }
+ \caption{High level overview of the life of a \mykant\ prompt cycle.}
+ \label{fig:kant-process}
+\end{figure}
+
+\subsection{Parsing and \texttt{Sugar}}
+
+\subsection{Term representation and context}
+\label{sec:term-repr}
+
+\subsection{Type checking}
+
+\subsection{Type hierarchy}
+\label{sec:hier-impl}
+
+\subsection{Elaboration}
+
+\section{Evaluation}
+
+\section{Future work}
+
+\subsection{Coinduction}
+
+\subsection{Quotient types}
+
+\subsection{Partiality}
+
+\subsection{Pattern matching}
+
+\subsection{Pattern unification}
+
+% TODO coinduction (obscoin, gimenez), pattern unification (miller,
+% gundry), partiality monad (NAD)
+
+\appendix
+
+\section{Notation and syntax}
+
+Syntax, derivation rules, and reduction rules, are enclosed in frames describing
+the type of relation being established and the syntactic elements appearing,
+for example
+
+\mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
+ Typing derivations here.
+}
+
+In the languages presented and Agda code samples I also highlight the syntax,
+following a uniform color and font convention:
+
+\begin{center}
+ \begin{tabular}{c | l}
+ $\mytyc{Sans}$ & Type constructors. \\
+ $\mydc{sans}$ & Data constructors. \\
+ % $\myfld{sans}$ & Field accessors (e.g. \myfld{fst} and \myfld{snd} for products). \\
+ $\mysyn{roman}$ & Keywords of the language. \\
+ $\myfun{roman}$ & Defined values and destructors. \\
+ $\myb{math}$ & Bound variables.
+ \end{tabular}
+\end{center}
+
+Moreover, I will from time to time give examples in the Haskell programming
+language as defined in \citep{Haskell2010}, which I will typeset in
+\texttt{teletype} font. I assume that the reader is already familiar with
+Haskell, plenty of good introductions are available \citep{LYAH,ProgInHask}.
+
+When presenting grammars, I will use a word in $\mysynel{math}$ font
+(e.g. $\mytmsyn$ or $\mytysyn$) to indicate indicate nonterminals. Additionally,
+I will use quite flexibly a $\mysynel{math}$ font to indicate a syntactic
element. More specifically, terms are usually indicated by lowercase letters
(often $\mytmt$, $\mytmm$, or $\mytmn$); and types by an uppercase letter (often
$\mytya$, $\mytyb$, or $\mytycc$).
When presenting type derivations, I will often abbreviate and present multiple
conclusions, each on a separate line:
-
\begin{prooftree}
\AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
\UnaryInfC{$\myjud{\myapp{\myfst}{\mytmt}}{\mytya}$}
\UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mytyb}$}
\end{prooftree}
-\section{Agda rendition of core ITT}
-\label{app:agda-code}
+I will often present `definition' in the described calculi and in
+$\mykant$\ itself, like so:
+{\small\[
+\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, for example
+{\small\[
+\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}
+\]}
+
+\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
+
+ List : (A : Set) → Set
+ List A = W (A ∨ Unit) (λ s → Tr (fst s))
+
+ [] : ∀ {A} → List A
+ [] = (false , tt) ◁ absurd
+
+ _∷_ : ∀ {A} → A → List A → List A
+ x ∷ l = (true , x) ◁ (λ _ → l)
+
+ _++_ : ∀ {A} → List A → List A → List A
+ l₁ ++ l₂ = rec
+ (λ _ → List _ → List _)
+ (λ s f c l → {!!})
+ l₁ l₂
+
+module Equality where
+ open ITT
+
data _≡_ {a} {A : Set a} : A → A → Set a where
refl : ∀ x → x ≡ x
- J : ∀ {a b} {A : Set a}
+ ≡-elim : ∀ {a b} {A : Set a}
(P : (x y : A) → x ≡ y → Set b) →
∀ {x y} → P x x (refl x) → (x≡y : x ≡ y) → P x y x≡y
- J P p (refl x) = p
+ ≡-elim P p (refl x) = p
+
+ subst : ∀ {A : Set} (P : A → Set) → ∀ {x y} → (x≡y : x ≡ y) → P x → P y
+ subst P x≡y p = ≡-elim (λ _ y _ → P y) p x≡y
+
+ sym : ∀ {A : Set} (x y : A) → x ≡ y → y ≡ x
+ sym x y p = subst (λ y′ → y′ ≡ x) p (refl x)
+
+ trans : ∀ {A : Set} (x y z : A) → x ≡ y → y ≡ z → x ≡ z
+ trans x y z p q = subst (λ z′ → x ≡ z′) q p
- subst : ∀ {a b} {A : Set a}
- (P : A → Set b) →
- ∀ {x y} → (x≡y : x ≡ y) → P x → P y
- subst P q p = J (λ _ y _ → P y) p q
+ 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}
+
+The following things are missing: $\mytyc{W}$-types, since our
+positivity check is overly strict, and equality, since we haven't
+implemented that yet.
+
+{\small
+\verbatiminput{itt.ka}
+}
+
+\subsection{\mykant\ examples}
+
+{\small
+\verbatiminput{examples.ka}
+}
+
+\subsection{\mykant's hierachy}
+
+This rendition of the Hurken's paradox does not type check with the
+hierachy enabled, type checks and loops without it. Adapted from an
+Agda version, available at
+\url{http://code.haskell.org/Agda/test/succeed/Hurkens.agda}.
+
+{\small
+\verbatiminput{hurkens.ka}
+}
+
\bibliographystyle{authordate1}
\bibliography{thesis}
projects / bitonic-mengthesis.git / blobdiff