% \linespread{1.05}
% \usepackage{times}
-\oddsidemargin .50in
-\evensidemargin -.25in
+% \oddsidemargin .50in
+% \evensidemargin -.25in
+\oddsidemargin 0in
+\evensidemargin 0in
\textheight 9.5in
\textwidth 6.2in
\topmargin -7mm
\newcommand{\mytmm}{\mysynel{m}}
\newcommand{\mytmn}{\mysynel{n}}
\newcommand{\myred}{\leadsto}
-\newcommand{\mysub}[3]{#1[#2 / #3]}
+\newcommand{\mysub}[3]{#1[#3 / #2]}
\newcommand{\mytysyn}{\mysynel{type}}
\newcommand{\mybasetys}{K}
\newcommand{\mybasety}[1]{B_{#1}}
\newcommand{\myprdec}[1]{\mathopen{\mytyc{$\llbracket$}} #1 \mathclose{\mytyc{$\rrbracket$}}}
\newcommand{\myand}{\mathrel{\mytyc{$\wedge$}}}
\newcommand{\mybigand}{\mathrel{\mytyc{$\bigwedge$}}}
-\newcommand{\myprfora}[3]{\forall #1 {:} #2. #3}
+\newcommand{\myprfora}[3]{\forall #1 {:} #2.\, #3}
\newcommand{\myimpl}{\mathrel{\mytyc{$\Rightarrow$}}}
\newcommand{\mybot}{\mytyc{$\bot$}}
\newcommand{\mytop}{\mytyc{$\top$}}
\begin{titlepage}
\begin{center}
+
% Upper part of the page. The '~' is needed because \\
% only works if a paragraph has started.
\includegraphics[width=0.4\textwidth]{brouwer-cropped.png}~\\[1cm]
\end{center}
\end{titlepage}
+\pagenumbering{gobble}
+
+\newpage{}
+\mbox{}
+\newpage{}
+
+\thispagestyle{empty}
+
\begin{abstract}
The marriage between programming and logic has been a very fertile
- one. In particular, since the definition of the simply typed lambda
- calculus, a number of type systems have been devised with increasing
- expressive power.
+ one. In particular, since the definition of the simply typed
+ $\lambda$-calculus, a number of type systems have been devised with
+ increasing expressive power.
Among this systems, Inutitionistic Type Theory (ITT) has been a very
popular framework for theorem provers and programming languages.
issues faced.
\end{abstract}
-\clearpage
+\newpage{}
+\mbox{}
+\newpage{}
\renewcommand{\abstractname}{Acknowledgements}
\begin{abstract}
the colours.
\end{abstract}
-\clearpage
+\newpage{}
+\mbox{}
+\newpage{}
+
+\thispagestyle{empty}
\tableofcontents
\clearpage
+\pagenumbering{arabic}
+
\section{Introduction}
+Functional programming is in good shape. In particular the `well-typed'
+line of work originating from Milner's ML has been extremely fruitful,
+in various directions. Nowadays functional, well-typed programming
+languages like Haskell or OCaml are slowly being absorbed by the
+mainstream. An important related development---and in fact the original
+motivator for ML's existence---is the advancement of the practice of
+\emph{interactive theorem provers}.
+
+
+An interactive theorem prover, or proof assistant, is a tool that lets
+the user develop formal proofs with the confidence of the machine
+checking it for correctness. While the effort towards a full
+formalisation of mathematics has been ongoing for more than a century,
+theorem provers have been the first class of software whose
+implementation depends directly on these theories.
+
+In a fortunate turn of events, it was discovered that well-typed
+functional programming and proving theorems in an \emph{intuitionistic}
+logic are the same activity. Under this discipline, the types in our
+programming language can be interpreted as proposition in our logic; and
+the programs implementing the specification given by the types as their
+proofs. This fact stimulated a very active transfer of techniques and
+knowledge between logic and programming language theory, in both
+directions.
+
+Mathematics could provide programming with a huge wealth of abstractions
+and constructs developed over centuries. Moreover, identifying our
+types with a logic lets us focus on foundational questions regarding
+programming with a much more solid approach, given the years of rigorous
+study of logic. Programmers, on the other hand, had already developed a
+wealth of approaches to effectively collaborate with computers, through
+the study of programming languages.
+
+We will follow the discipline of Intuitionistic Type Theory, or
+Martin-L\"{o}f Type Theory, after its inventor. First formulated in the
+70s and then adjusted through a series of revisions, it has endured as
+the core of many practical systems widely in use today, and it is
+probably the most prominent instance of the proposition-as-types and
+proofs-as-programs discipline. One of the most debated subjects in this
+field has been regarding what notion of \emph{equality} should be
+exposed to the user.
+
+The tension in the field of equality springs from the fact that there is
+a divide between what the user can prove equal \emph{inside} the
+theory---what is \emph{propositionally} equal--- and what the theorem
+prover identifies as equal in its meta-theory---what is
+\emph{definitionally} equal. If we want our system to be well behaved
+(for example if we want type checking to be decidable) we must keep the
+two notions separate, with definitional equality inducing propositional
+equality, but not the reverse. However in this scenario propositional
+equality is weaker than we would like: we can only prove terms equal
+based on their syntactical structure, and not based on their observable
+behaviour.
+
+This thesis is concerned with exploring a new approach in this area,
+\emph{observational} equality. Promising to provide a more adequate
+propositional equality while retaining well-behavedness, it still is a
+relatively unexplored notion. We set ourselves to change that by
+studying it in a setting more akin the one found in currently available
+theorem provers.
+
+\subsection{Structure}
+
+Section \ref{sec:types} will give a brief overview of the
+$\lambda$-calculus, both typed and untyped. This will give us the
+chance to introduce most of the concepts mentioned above rigorously, and
+gain some intuition about them. An excellent introduction to types in
+general can be found in \cite{Pierce2002}, although not from the
+perspective of theorem proving.
+
+Section \ref{sec:itt} will describe a set of basic construct that form a
+`baseline' Intuitionistic Type Theory. The goal is to familiarise with
+the main concept of ITT before attacking the problem of equality. Given
+the wealth of material covered the exposition is quite dense. Good
+introductions can be found in \cite{Thompson1991}, \cite{Nordstrom1990},
+and \cite{Martin-Lof1984} himself.
+
+Section \ref{sec:equality} will introduce propositional equality. The
+properties of propositional equality will be discussed along with its
+limitations. After reviewing some extensions to propositional equality,
+we will explain why identifying definitional equality with propositional
+equality causes problems.
+
+Section \ref{sec:ott} will introduce observational equality, following
+closely the original exposition by \cite{Altenkirch2007}. The
+presentation is free-standing but glosses over the meta-theoretic
+properties of OTT, focusing on the mechanism that make it work.
+
+Section \ref{sec:kant-theory} will describe \mykant, a system we have
+developed incorporating OTT along constructs usually present in modern
+theorem provers. Along the way, we describe these additional features
+and their advantages. Section \ref{sec:kant-practice} will describe an
+implementation implementing part of \mykant. A high level design of the
+software is given, along with a few specific implementation issues
+
+Finally, Section \ref{sec:evaluation} will asses the decisions made in
+designing and implementing \mykant, and Section \ref{sec:future-work}
+will give a roadmap to bring \mykant\ on par and beyond the
+competition.
+
+\subsection{Contribution}
+
+The goal of this thesis is threefold:
+\begin{itemize}
+\item Provide a description of observational equality `in context', to
+ make the subject more accessible. Considering the possibilities that
+ OTT brings to the table, we think that introducing it to a wider
+ audience can only be beneficial.
+
+\item Fill in the gaps needed to make OTT work with user-defined
+ inductive types and a type hierarchy. We show how one notion of
+ equality is enough, instead of separate notions of value- and
+ type-equality as presented in the original paper. We are able to keep
+ the type equalities `small' while preserving subject reduction by
+ exploiting the fact that we work within a cumulative theory.
+ Incidentally, we also describe a generalised version of bidirectional
+ type checking for user defined types.
+
+\item Provide an implementation to probe the possibilities of OTT in a
+ more realistic setting. We have implemented an ITT with user defined
+ types but due to the limited time constraints we were not able to
+ complete the implementation of observational equality. Nonetheless,
+ we describe some interesting implementation issues faced by the type
+ theory implementor.
+\end{itemize}
\section{Simple and not-so-simple types}
\label{sec:types}
with a minimal syntax and no `data' in the traditional sense, but just
functions. Here we give a brief overview of the language, which will
give the chance to introduce concepts central to the analysis of all the
-following calculi. The exposition follows the one found in chapter 5 of
+following calculi. The exposition follows the one found in Chapter 5 of
\cite{Queinnec2003}.
\begin{mydef}[$\lambda$-terms]
\mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
$
\begin{array}{l}
- \myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{\myb{x}}{\mytmn}\text{, where} \\
+ \myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{\myb{x}}{\mytmn}\text{ \textbf{where}} \\
\myind{2}
\begin{array}{l@{\ }c@{\ }l}
\mysub{\myb{x}}{\myb{x}}{\mytmn} & = & \mytmn \\
- \mysub{\myb{y}}{\myb{x}}{\mytmn} & = & y\text{, with } \myb{x} \neq y \\
+ \mysub{\myb{y}}{\myb{x}}{\mytmn} & = & y\text{ \textbf{with} } \myb{x} \neq y \\
\mysub{(\myapp{\mytmt}{\mytmm})}{\myb{x}}{\mytmn} & = & (\myapp{\mysub{\mytmt}{\myb{x}}{\mytmn}}{\mysub{\mytmm}{\myb{x}}{\mytmn}}) \\
\mysub{(\myabs{\myb{x}}{\mytmm})}{\myb{x}}{\mytmn} & = & \myabs{\myb{x}}{\mytmm} \\
- \mysub{(\myabs{\myb{y}}{\mytmm})}{\myb{x}}{\mytmn} & = & \myabs{\myb{z}}{\mysub{\mysub{\mytmm}{\myb{y}}{\myb{z}}}{\myb{x}}{\mytmn}}, \\
- \multicolumn{3}{l}{\myind{2} \text{with $\myb{x} \neq \myb{y}$ and $\myb{z}$ not free in $\myapp{\mytmm}{\mytmn}$}}
+ \mysub{(\myabs{\myb{y}}{\mytmm})}{\myb{x}}{\mytmn} & = & \myabs{\myb{z}}{\mysub{\mysub{\mytmm}{\myb{y}}{\myb{z}}}{\myb{x}}{\mytmn}} \\
+ \multicolumn{3}{l}{\myind{2} \text{\textbf{with} $\myb{x} \neq \myb{y}$ and $\myb{z}$ not free in $\myapp{\mytmm}{\mytmn}$}}
\end{array}
\end{array}
$
}
-The care required during substituting variables for terms is required to avoid
-name capturing. We will use substitution in the future for other name-binding
-constructs assuming similar precautions.
+The care required during substituting variables for terms is to avoid
+name capturing. We will use substitution in the future for other
+name-binding constructs assuming similar precautions.
These few elements have a remarkable expressiveness, and are in fact
Turing complete. As a corollary, we must be able to devise a term that
\[
\myapp{(\myabss{\myb{x}}{\myhole{?}}{\myapp{\myb{x}}{\myb{x}}})}{(\myabss{\myb{x}}{\myhole{?}}{\myapp{\myb{x}}{\myb{x}}})}
\]
-
This makes the STLC Turing incomplete. We can recover the ability to loop by
adding a combinator that recurses:
\begin{mydef}[Fixed-point combinator]\end{mydef}
This will deprive us of normalisation, which is a particularly bad thing if we
want to use the STLC as described in the next section.
+Another important property of the STLC is the Church-Rosser property:
+\begin{mydef}[Church-Rosser property]
+ A system is said to have the \emph{Church-Rosser} property, or to be
+ \emph{confluent}, if given any two reductions $\mytmm$ and $\mytmn$ of
+ a given term $\mytmt$, there is exist a term to which both $\mytmm$
+ and $\mytmn$ can be reduced.
+\end{mydef}
+Given that the STLC has the normalisation property and the Church-Rosser
+property, each term has a unique normal form for definitional equality
+to be decidable.
+
\subsection{The Curry-Howard correspondence}
-It turns out that the STLC can be seen a natural deduction system for
-intuitionistic propositional logic. Terms correspond to proofs, and
-their types correspond to the propositions they prove. This remarkable
-fact is known as the Curry-Howard correspondence, or isomorphism.
+As hinted in the introduction, it turns out that the STLC can be seen a
+natural deduction system for intuitionistic propositional logic. Terms
+correspond to proofs, and their types correspond to the propositions
+they prove. This remarkable fact is known as the Curry-Howard
+correspondence, or isomorphism.
The arrow ($\myarr$) type corresponds to implication. If we wish to prove that
that $(\mytya \myarr \mytyb) \myarr (\mytyb \myarr \mytycc) \myarr (\mytya
\]
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
-comparing terms by reducing to their normal forms and then comparing
-them syntactically; so that a separate conversion rule is not needed.
+employ $\myred$ to decide term equality in a systematic way, comparing
+terms by reducing to their normal forms and then comparing them
+syntactically; so that a separate conversion rule is not needed.
Another thing to notice is that considering the need to reduce terms to
decide equality it is essential for a dependently typed system to be
terminating and confluent for type checking to be decidable, since every
\begin{Verbatim}
if null xs then head xs else 0
\end{Verbatim}
-are a necessary, well typed, danger.
+are a necessary, well-typed, danger.
However, in a more expressive system, we can do better: the branches' type can
depend on the value of the scrutinised boolean. This is what the typing rule
the updated knowledge on the value of $\myb{x}$.
\subsubsection{$\myarr$, or dependent function}
-\label{rec:depprod}
+\label{sec:depprod}
\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
\AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
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 are write functions of type:
+language, using dependent functions we can write functions of types
\[
\begin{array}{l}
\myfun{length} : (\myb{A} {:} \mytyp_0) \myarr \myapp{\mylist}{\myb{A}} \myarr \mynat \\
the length of the list argument is non-zero. This allows us to rule out
the `empty list' case, so that we can safely return the first element.
+% TODO fix this
Again, we need to make sure that the type hierarchy is respected, which
is the reason why a type formed by $\myarr$ will live in the least upper
bound of the levels of argument and return type. If this was not the
\myw{\myb{x}}{\mytya}{\mytyb}$ that contain data ($\mytmt$) of type and
one `child' for each member of $\mysub{\mytyb}{\myb{x}}{\mytmt}$. The
$\myfun{rec}\ \myfun{with}$ acts as an induction principle on
-$\mytyc{W}$, given a predicate an a function dealing with the inductive
+$\mytyc{W}$, given a predicate and a function dealing with the inductive
case---we will gain more intuition about inductive data in ITT in
Section \ref{sec:user-type}.
\[
\begin{array}{@{}l}
\mytyc{Tr} : \mybool \myarr \mytyp_0 \\
- \mytyc{Tr} \myappsp \myb{b} \mapsto \myfun{if}\, \myb{b}\, \myunit\, \myfun{else}\, \myempty \\
+ \mytyc{Tr} \myappsp \myb{b} \mapsto \myfun{if}\, \myb{b}\, \myfun{then}\, \myunit\, \myfun{else}\, \myempty \\
\ \\
\mynat : \mytyp_0 \\
\mynat \mapsto \myw{\myb{b}}{\mybool}{(\mytyc{Tr}\myappsp\myb{b})}
\[
\begin{array}{@{}l}
\mydc{zero} : \mynat \\
- \mydc{zero} \mapsto \myfalse \mynodee (\myabs{\myb{z}}{\myabsurd{\mynat} \myappsp \myb{x}}) \\
+ \mydc{zero} \mapsto \myfalse \mynodee (\myabs{\myb{x}}{\myabsurd{\mynat} \myappsp \myb{x}}) \\
\ \\
\mydc{suc} : \mynat \myarr \mynat \\
\mydc{suc}\myappsp \myb{x} \mapsto \mytrue \mynodee (\myabs{\myarg}{\myb{x}})
\myind{2}\myind{2}\myfun{then}\,(\myabs{\myarg\, \myb{f}}{\mydc{suc}\myappsp (\myapp{\myb{f}}{\mytt})})\, \myfun{else}\, (\myabs{\myarg\, \myarg}{\myb{y}})}
\end{array}
\]
-Note how we explicitly have to type the branches to make them
-match with the definition of $\mynat$---which gives a taste of the
-`clumsiness' of $\mytyc{W}$-types, which while useful as a reasoning
-tool are useless to the user modelling data types.
+ Note how we explicitly have to type the branches to make them match
+ with the definition of $\mynat$. This gives a taste of the
+ `clumsiness' of $\mytyc{W}$-types but not the whole story: well-orders
+ are inadequate not only because they are verbose, but present deeper
+ problems because the notion of equality present in most type theory
+ (which we will present in the next section) is too weak
+ \citep{dybjer1997representing}. The `better' equality we will present
+ in Section \ref{sec:ott} helps but does not fully resolve these
+ issues.\footnote{See \url{http://www.e-pig.org/epilogue/?p=324}, which
+ concludes with `W-types are a powerful conceptual tool, but they’re
+ no basis for an implementation of recursive datatypes in decidable
+ type theories.'} For this reasons \mytyc{W}-types have remained
+ nothing more than a reasoning tool, and practical systems implement
+ more expressive ways to represent data.
\section{The struggle for equality}
\label{sec:equality}
Finally, we have one eliminator for $\mypeq$, $\myjeqq$. $\myjeq{\myse{P}}{\myse{q}}{\myse{p}}$ takes
\begin{itemize}
\item $\myse{P}$, a predicate working with two terms of a certain type (say
- $\mytya$) and a proof of their equality
+ $\mytya$) and a proof of their equality;
\item $\myse{q}$, a proof that two terms in $\mytya$ (say $\myse{m}$ and
- $\myse{n}$) are equal
+ $\myse{n}$) are equal;
\item and $\myse{p}$, an inhabitant of $\myse{P}$ applied to $\myse{m}$
twice, plus the trivial proof by reflexivity showing that $\myse{m}$
- is equal to itself
+ is equal to itself.
\end{itemize}
Given these ingredients, $\myjeqq$ retuns a member of $\myse{P}$ applied
to $\mytmm$, $\mytmn$, and $\myse{q}$. In other words $\myjeqq$ takes a
can be returned. This means that $\myjeqq$ will not compute with
hypotetical proofs, which makes sense given that they might be false.
-While the $\myjeqq$ rule is slightly convoluted, ve can derive many more
+While the $\myjeqq$ rule is slightly convoluted, we can derive many more
`friendly' rules from it, for example a more obvious `substitution' rule, that
replaces equal for equal in predicates:
\[
\mydesc{typing:}{\myjud{\mytmm \mydefeq \mytmn}{\mytmsyn}}{
\AxiomC{$
\begin{array}{@{}c}
- \myjud{\myse{P}}{\myfora{\myb{x}}{\mytya}{\myb{x} \mypeq{\mytya} \myb{x} \myarr \mytyp}} \\\
+ \myjud{\myse{P}}{\myfora{\myb{x}}{\mytya}{\mypeq \myappsp \mytya \myappsp \myb{x}\myappsp \myb{x} \myarr \mytyp}} \\\
\myjud{\mytmt}{\mytya} \hspace{1cm}
\myjud{\myse{p}}{\myse{P} \myappsp \mytmt \myappsp (\myrefl \myappsp \mytmt)} \hspace{1cm}
\myjud{\myse{q}}{\mytmt \mypeq{\mytya} \mytmt}
Propositional equality as described is quite restricted when
reasoning about equality beyond the term structure, which is what definitional
-equality gives us (extension notwithstanding).
+equality gives us (extensions notwithstanding).
The problem is best exemplified by \emph{function extensionality}. In
mathematics, we would expect to be able to treat functions that give equal
The two functions are clearly extensionally equal, and we can in fact
prove that
\[
-\myfora{\myb{x}}{\mynat}{(0 \mathrel{\myfun{$+$}} \myb{x}) \mypeq{\mynat} (\myb{x} \mathrel{\myfun{$+$}} 0)}
+\myfora{\myb{x}}{\mynat}{\mypeq \myappsp \mynat \myappsp (0 \mathrel{\myfun{$+$}} \myb{x}) \myappsp (\myb{x} \mathrel{\myfun{$+$}} 0)}
\]
By analysis on the $\myb{x}$. However, the two functions are not
definitionally equal, and thus we won't be able to get rid of the
This is quite an annoyance that often makes reasoning awkward to execute. It
also extends to other fields, for example proving bisimulation between
processes specified by coinduction, or in general proving equivalences based
-on the behaviour on a term.
+on the behaviour of a term.
\subsection{Equality reflection}
\subsection{A simpler theory, a propositional fragment}
+\begin{mydef}[OTT's simple theory, with propositions]\ \end{mydef}
+\mynegder
\mydesc{syntax}{ }{
$\mytyp_l$ is replaced by $\mytyp$. \\\ \\
$
\end{tabular}
}
-Our foundation will be a type theory like the one of section
+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
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}$: \\
+indeed we can `inject' any $\myprop$ back in $\mytyp$ with $\myprdec{\myarg}$.
+\begin{mydef}[Proposition decoding]\ \end{mydef}
\mydesc{proposition decoding:}{\myprdec{\mytmsyn} \myred \mytmsyn}{
\begin{tabular}{cc}
$
\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.
+ whose inhabitants contain no `data', much like $\myunit$. The goal
+ when isolating \mytyc{Prop} is twofold: erasing all top-level
+ propositions when compiling; and to identify all equivalent
+ propositions as the same, as we will see later.
Why did we choose what we have in $\myprop$? Given the above
- criteria, $\mytop$ obviously fits the bill, since it us one element.
+ criteria, $\mytop$ obviously fits the bill, since it has one element.
A pair of propositions $\myse{P} \myand \myse{Q}$ still won't get us
data, since if they both have one element the only possible pair is
the one formed by said elements. Finally, if $\myse{P}$ is a
proposition and we have $\myprfora{\myb{x}}{\mytya}{\myse{P}}$, the
- decoding will be a function which returns propositional content. The
+ decoding will be a constant function for propositional content. The
only threat is $\mybot$, by which we can fabricate anything we want:
- however if we are consistent there will be nothing of type $\mybot$ at
- the top level, which is what we care about regarding proof erasure.
+ however if we are consistent there will be no closed term of type
+ $\mybot$ at, which is what we care about regarding proof erasure and
+ term equality.
\subsection{Equality proofs}
+\begin{mydef}[Equality proofs and related operations]\ \end{mydef}
+\mynegder
\mydesc{syntax}{ }{
$
\begin{array}{r@{\ }c@{\ }l}
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.
+equality. In OTT we want to maintain that things judged to be equal are
+still always repleaceable for one another with no additional
+changes. Note that this is not the same as saying that they are
+definitionally equal, since as we saw extensionally equal functions,
+while satisfying the above requirement, are not.
Towards this goal we introduce two equality constructs in
$\myprop$---the fact that they are in $\myprop$ indicates that they
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.
+between \emph{canonical} and \emph{neutral} terms and types.
+
+\begin{mydef}[Canonical and neutral types and terms]
+ \emph{Canonical} types are those arising from the ground types
+ ($\myempty$, $\myunit$, $\mybool$) and the three type formers
+ ($\myarr$, $\myprod$, $\mytyc{W}$). \emph{Neutral} types are those
+ formed by $\myfun{If}\myarg\myfun{Then}\myarg\myfun{Else}\myarg$.
+ Correspondingly, canonical terms are those inhabiting data
+ constructors ($\mytt$, $\mytrue$, $\myfalse$,
+ $\myabss{\myb{x}}{\mytya}{\mytmt}$, ...); all the others being
+ neutral, including eliminators and abstracted variables.
+\end{mydef}
+
+In the current system (and hopefully in well-behaved systems), all
+closed terms reduce to a canonical term (as a consequence or
+normalisation), and all canonical types are inhabited by canonical
+terms (a property known as \emph{canonicity}).
\subsubsection{Type equality, and coercions}
The plan is to decompose type-level equalities between canonical types
into decodable propositions containing equalities regarding the
subterms, and to use coerce recursively on the subterms using the
-generated equalities. This interplay between 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}$.
+generated equalities. This interplay between the canonicity of equated
+types, type equalities, and \myfun{coe} ensures that invocations of
+$\myfun{coe}$ will vanish when we have evidence of the structural
+equality of the types we are transporting terms across. If the type is
+neutral, the equality will not reduce and thus $\myfun{coe}$ will not
+reduce either. If we come an equality between different canonical
+types, then we reduce the equality to bottom, making sure that no such
+proof can exist, and providing an `escape hatch' in $\myfun{coe}$.
\begin{figure}[t]
\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
+ \myind{2} \mytya_1 \myeq \mytya_2 \myand
\myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{\myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2}} \myimpl \mytyb_1[\myb{x_1}] \myeq \mytyb_2[\myb{x_2}]}
} \\
\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myfora{\myb{x_2}}{\mytya_2}{\mytyb_2} & \myred \cdots \\
\label{fig:eqred}
\end{figure}
-Figure \ref{fig:eqred} illustrates this idea in practice. For ground
-types, the proof is the trivial element, and \myfun{coe} is the
-identity. For $\myunit$, we can do better: we return its only member
-without matching on the term. For the three type binders, things are
-similar but subtly different---the choices we make in the type equality
-are dictated by the desire of writing the $\myfun{coe}$ in a natural
-way.
+\begin{mydef}[Type equalities reduction, and \myfun{coe}rcions] Figure
+ \ref{fig:eqred} illustrates the rules to reduce equalities and to
+ coerce terms.
+\end{mydef}
+For ground types, the proof is the trivial element, and \myfun{coe} is
+the identity. For $\myunit$, we can do better: we return its only
+member without matching on the term. For the three type binders, things
+are similar but subtly different---the choices we make in the type
+equality are dictated by the desire of writing the $\myfun{coe}$ in a
+natural way.
$\myprod$ is the easiest case: we decompose the proof into proofs that
the first element's types are equal ($\mytya_1 \myeq \mytya_2$), and a
proof that given equal values in the first element, the types of the
second elements are equal too
($\myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{\myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2}}
- \myimpl \mytyb_1 \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.
+ \myimpl \mytyb_1[\myb{x_1}] \myeq \mytyb_2[\myb{x_2}]}$).\footnote{We
+ are using $\myimpl$ to indicate a $\forall$ where we discard the first
+ value. We write $\mytyb_1[\myb{x_1}]$ to indicate that the
+ $\myb{x_1}$ in $\mytyb_1$ is re-bound to the $\myb{x_1}$ quantified by
+ the $\forall$, and similarly for $\myb{x_2}$ and $\mytyb_2$.} This
+also explains the need for heterogeneous equality, since in the second
+proof we need to equate terms of possibly different types. In the respective $\myfun{coe}$ case, since
+the types are canonical, we know at this point that the proof of
+equality is a pair of the shape described above. Thus, we can
+immediately coerce the first element of the pair using the first element
+of the proof, and then instantiate the second element with the two first
+elements and a proof by coherence of their equality, since we know that
+the types are equal.
The cases for the other binders are omitted for brevity, but they follow
the same principle with some twists to make $\myfun{coe}$ work with the
generated proofs; the reader can refer to the paper for details.
\subsubsection{$\myfun{coe}$, laziness, and $\myfun{coh}$erence}
+\label{sec:lazy}
It is important to notice that in the reduction rules for $\myfun{coe}$
are never obstructed by the proofs: with the exception of comparisons
\subsubsection{Value-level equality}
+\begin{mydef}[Value-level equality]\ \end{mydef}
+\mynegder
\mydesc{equality reduction:}{\myprsyn \myred \myprsyn}{
$
\begin{array}{r@{ }c@{\ }c@{\ }c@{}l@{\ }c@{\ }r@{}c@{\ }c@{\ }c@{}l@{\ }l}
However they are definitionally equal, and thus we can safely remove the
coerce and return $\myb{x}$ as it is.
-\section{\mykant : the theory}
+\section{\mykant: the theory}
\label{sec:kant-theory}
\mykant\ is an interactive theorem prover developed as part of this thesis.
\item[Type holes] When building up programs interactively, it is useful
to leave parts unfinished while exploring the current context. This
is what type holes are for. We do not describe holes rigorously, but
- provide more information about them from the implementation and usage
- perspective in Section \ref{sec:type-holes}.
+ provide more information about them in Section \ref{sec:type-holes}.
\end{description}
fairly different typing rules that what we have seen up to now. The
idea is to have two kinds of terms: terms for which a type can always be
inferred, and terms that need to be checked against a type. A nice
-observation is that this duality runs through the semantics of the
-terms: neutral terms (abstracted or defined variables, function
-application, record projections, primitive recursors, etc.) \emph{infer}
-types, canonical terms (abstractions, record/data types data
-constructors, etc.) need to be \emph{checked}.
+observation is that this duality is in correspondence with the notion of
+canonical and neutral terms: neutral terms
+(abstracted or defined variables, function application, record
+projections, primitive recursors, etc.) \emph{infer} types, canonical
+terms (abstractions, record/data types data constructors, etc.) need to
+be \emph{checked}.
To introduce the concept and notation, we will revisit the STLC in a
bidirectional style. The presentation follows \cite{Loh2010}. The
explicitly---this will be necessary when having top-level canonical
terms. The types are the same as those found in the normal STLC.
+\begin{mydef}[Syntax for the annotated $\lambda$-calculus]\ \end{mydef}
+\mynegder
\mydesc{syntax}{ }{
$
\begin{array}{r@{\ }c@{\ }l}
propagating types down the applied term. Abstractions are checked.
Finally, we have a rule to check the type of an inferrable term.
+\begin{mydef}[Bidirectional type checking for the STLC]\ \end{mydef}
+\mynegder
\mydesc{typing:}{\myctx \vdash \mytmsyn \Updownarrow \mytmsyn}{
\begin{tabular}{cc}
\AxiomC{$\myctx(x) = A$}
\DisplayProof
&
\AxiomC{$\myinf{\mytmt}{\mytya}$}
- \UnaryInfC{$\myinf{\mytmt}{\mytya}$}
+ \UnaryInfC{$\mychk{\mytmt}{\mytya}$}
\DisplayProof
\end{tabular}
}
rules too much, and just treat types as impredicative for the time
being.
+\begin{mydef}[Syntax for base types in \mykant]\ \end{mydef}
+\mynegder
\mydesc{syntax}{ }{
$
\begin{array}{r@{\ }c@{\ }l}
}
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.
+abstractions and $\mytyp$s. Everything else will be user-defined.
+Since we let the user define values too, we will need a context capable
+of carrying the body of variables along with their type.
+\begin{mydef}[Context validity]
Bound names and defined names are treated separately in the syntax, and
while both can be associated to a type in the context, only defined
-names can be associated with a body:
-
+names can be associated with a body.
+\end{mydef}
+\mynegder
\mydesc{context validity:}{\myvalid{\myctx}}{
\begin{tabular}{ccc}
\AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
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:
+opposed to what we have seen in the past.
+\begin{mydef}[Reduction rules for base types in \mykant]\ \end{mydef}
+\mynegder
\mydesc{reduction:}{\myctx \vdash \mytmsyn \myred \mytmsyn}{
\begin{tabular}{ccc}
\AxiomC{\phantom{$\myb{x} \mapsto \mytmt : \mytya \in \myctx$}}
conversion rule, we defer a detailed account of definitional equality to
Section \ref{sec:kant-irr}.
+\begin{mydef}[Bidirectional type checking for base types in \mykant]\ \end{mydef}
+\mynegder
\mydesc{typing:}{\myctx \vdash \mytmsyn \Updownarrow \mytmsyn}{
\begin{tabular}{cccc}
\AxiomC{$\myse{name} : A \in \myctx$}
\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 contexts.
+\begin{mydef}[Term vector]
+ A \emph{term vector} is a series of terms. The empty vector is
+ represented by $\myemptyctx$, and a new element is added with a
+ semicolon, similarly to contexts---$\vec{t};\mytmm$.
+\end{mydef}
+
+We use term vectors to refer to a series of term applied to another. For
+example $\mytyc{D} \myappsp \vec{A}$ is a shorthand for $\mytyc{D}
+\myappsp \mytya_1 \cdots \mytya_n$, for some $n$. $n$ is consistently
+used to refer to the length of such vectors, and $i$ to refer to an
+index in such vectors.
+
+\begin{mydef}[Telescope]
+ A \emph{telescope} is a series of typed bindings. The empty telescope
+ is represented by $\myemptyctx$, and a binding is added via
+ $\myarg;\myarg$.
+\end{mydef}
To present the elaboration and operations on user defined data types, we
frequently make use what de Bruijn called \emph{telescopes}
\citep{Bruijn91}, a construct that will prove useful when dealing with
-the types of type and data constructors. A telescope is a series of
-nested typed bindings, such as $(\myb{x} {:} \mynat); (\myb{p} {:}
-\myapp{\myfun{even}}{\myb{x}})$. Consistent 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
+the types of type and data constructors. We refer to telescopes with
+$\mytele$, $\mytele'$, $\mytele_i$, etc. If $\mytele$ refers to a
+telescope, $\mytelee$ refers to the term vector made up of all the
+variables bound by $\mytele$. $\mytele \myarr \mytya$ refers to the
+type made by turning the telescope into a series of $\myarr$. For
+example we have that
\[
(\myb{x} {:} \mynat); (\myb{p} : \myapp{\myfun{even}}{\myb{x}}) \myarr \mynat =
(\myb{x} {:} \mynat) \myarr (\myb{p} : \myapp{\myfun{even}}{\myb{x}}) \myarr \mynat
\subsubsection{Declarations syntax}
+\begin{mydef}[Syntax of declarations in \mykant]\ \end{mydef}
+\mynegder
\mydesc{syntax}{ }{
$
\begin{array}{r@{\ }c@{\ }l}
\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, quite 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.
+\item[Inductive data] A \emph{data type}, with a \emph{type constructor}
+ and various \emph{data constructors}, quite similar to what we find in
+ Haskell. A primitive \emph{eliminator} (or \emph{destructor}, or
+ \emph{recursor}) will be used to compute with each data type.
+\item[Record] A \emph{record}, which consists of one data constructor
+ and various \emph{fields}, with no recursive occurrences. The
+ functions extracting the fields' values from an instance of a record
+ are called \emph{projections}.
\end{description}
Elaborating defined variables consists of type checking the body against
the given type, and updating the context to contain the new binding.
Elaborating abstract variables and abstract variables consists of type
-checking the type, and updating the context with a new typed variable:
+checking the type, and updating the context with a new typed variable.
+\begin{mydef}[Elaboration of defined and abstract variables]\ \end{mydef}
+\mynegder
\mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
\begin{tabular}{cc}
\AxiomC{$\mychk{\mytmt}{\mytya}$}
elim (Suc n) pz ps = ps n (elim n pz ps)
\end{Verbatim}
Which buys us the computational behaviour, but not the reasoning power,
-since we cannot express the notion of a predicate depending on $\mynat$,
-since the type system is far too weak.
+since we cannot express the notion of a predicate depending on
+$\mynat$---the type system is far too weak.
\item[Binary trees] Now for a polymorphic data type: binary trees, since
lists are too similar to natural numbers to be interesting.
}
\end{array}
\]
- Now the purpose of constructors as syntax can be explained: what would
+ 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:
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
+ \mynat$ with two nodes and three leaves, we would write
\[
\mydc{node} \myappsp \mynat \myappsp (\mydc{node} \myappsp \mynat \myappsp (\mydc{leaf} \myappsp \mynat) \myappsp (\myapp{\mydc{suc}}{\mydc{zero}}) \myappsp (\mydc{leaf} \myappsp \mynat)) \myappsp \mydc{zero} \myappsp (\mydc{leaf} \myappsp \mynat)
\]
The redundancy of $\mynat$s is quite irritating. Instead, if we treat
constructors as syntactic elements, we can `extract' the type of the
parameter from the type that the term gets checked against, much like
- we get the type of abstraction arguments:
+ what we do to type abstractions:
\begin{center}
\mysmall
\begin{tabular}{cc}
As expected, the eliminator embodies structural induction on trees.
We have a base case for $\myb{P} \myappsp \mydc{leaf}$, and an
inductive step that given two subtrees and the predicate applied to
- them we need to return the predicate applied to the tree formed by a
+ them needs to return the predicate applied to the tree formed by a
node with the two subtrees as children.
\item[Empty type] We have presented types that have at least one
\[\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:
+ $\mykant$\ does not care, and generates an eliminator with no `cases':
\begin{prooftree}
\mysmall
\AxiomC{$\myinf{\mytmt}{\mytyc{Empty}}$}
\UnaryInfC{$\myinf{\myempty.\myfun{elim} \myappsp \mytmt}{(\myb{P} {:} \mytmt \myarr \mytyp) \myarr \myapp{\myb{P}}{\mytmt}}$}
\end{prooftree}
+ which lets us write the $\myfun{absurd}$ that we know and love:
+ \[
+ \begin{array}{l@{}}
+ \myfun{absurd} : (\myb{A} {:} \mytyp) \myarr \myempty \myarr \myb{A} \\
+ \myfun{absurd}\myappsp \myb{A} \myappsp \myb{x} \mapsto \myempty.\myfun{elim} \myappsp \myb{x} \myappsp (\myabs{\myarg}{\myb{A}})
+ \end{array}
+ \]
\item[Ordered lists] Up to this point, the examples shown are nothing
new to the \{Haskell, SML, OCaml, functional\} programmer. However
dependent types let us express much more than that. A useful example
is the type of ordered lists. There are many ways to define such a
- thing, we will define our type to store the bounds of the list, making
- sure that $\mydc{cons}$ing respects that.
+ thing, but we will define our type to store the bounds of the list,
+ making sure that $\mydc{cons}$ing respects that.
First, using $\myunit$ and $\myempty$, we define a type expressing the
ordering on natural numbers, $\myfun{le}$---`less or equal'.
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
+ `lifted' naturals with a bottom ($\le$ everything but itself) and top
+ ($\ge$ everything but itself) elements, along with an associated comparison
function:
\[
\begin{array}{@{}l}
\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.
+ types. Note that each field can refer to the preceding fields---in
+ this case we have the type of $\myfun{snd}$ depending on the value of
+ $\myfun{fst}$. A constructor will be automatically generated, under
+ the name of $\mytyc{Prod}.\mydc{constr}$. Dually to data types, we
+ will omit the type constructor prefix for record projections.
Following the bidirectionality of the system, we have that projections
(the destructors of the record) infer the type, while the constructor
\UnaryInfC{\phantom{$\myinf{\myfun{snd} \myappsp \mytmt}{\mytyb \myappsp (\myfst \myappsp \mytmt)}$}}
\DisplayProof
&
- \AxiomC{$\myinf{\mytmt}{\mytyc{Prod} \myappsp \mytya \myappsp \mytyb}$}
+ \AxiomC{$\hspace{0.2cm}\myinf{\mytmt}{\mytyc{Prod} \myappsp \mytya \myappsp \mytyb}\hspace{0.2cm}$}
\UnaryInfC{$\myinf{\myfun{fst} \myappsp \mytmt}{\mytya}$}
\noLine
\UnaryInfC{$\myinf{\myfun{snd} \myappsp \mytmt}{\mytyb \myappsp (\myfst \myappsp \mytmt)}$}
\DisplayProof
\end{tabular}
\end{center}
- What we have is equivalent to ITT's dependent products.
+ What we have defined here is equivalent to ITT's dependent products.
\end{description}
\begin{figure}[p]
\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 type 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.
+\begin{mydef}[Elaboration for user defined types]
+ Following the intuition given by the examples, the full elaboration
+ machinery is presented Figure \ref{fig:elab}.
+\end{mydef}
+Our elaboration is essentially a modification of Figure 9 of
+\cite{McBride2004}. However, our data types are not inductive
+families,\footnote{See Section \ref{sec:future-work} for a brief
+ description of inductive families.} we do bidirectional type checking
+by treating constructors/destructors as syntax, and we have records.
+
+\begin{mydef}[Strict positivity]
+ A inductive type declaration is \emph{strictly positive} if recursive
+ occurrences of the type we are defining do not appear embedded
+ anywhere in the domain part of any function in the types for the data
+ constructors.
+\end{mydef}
+In data type declarations we allow recursive occurrences as long as they
+are strictly positive, which ensures the consistency of the theory. To
+achieve that we employing a syntactic check to make sure that this is
+the case---in fact the check is stricter than necessary for simplicity,
+given that we allow recursive occurrences only at the top level of data
+constructor arguments.
+
+Without these precautions, we can easily derive any type with no
+recursion:
+\begin{Verbatim}
+data Fix a = Fix (Fix a -> a) -- Negative occurrence of `Fix a'
+-- Term inhabiting any type `a'
+boom :: a
+boom = (\f -> f (Fix f)) (\x -> (\(Fix f) -> f) x x)
+\end{Verbatim}
+See \cite{Dybjer1991} for a more formal treatment of inductive
+definitions in ITT.
For what concerns records, recursive occurrences are disallowed. The
reason for this choice is answered by the reason for the choice of
and in the treatment of OTT in Section \ref{sec:ott}. If we tried to
$\eta$-expand recursive data types, we would expand forever.
+\begin{mydef}[Bidirectional type checking for elaborated types]
To implement bidirectional type checking for constructors and
destructors, we store their types in full in the context, and then
-instantiate when due:
-
-\mydesc{typing:}{\myctx \vdash \mytmsyn \Leftrightarrow \mytmsyn}{
+instantiate when due.
+\end{mydef}
+\mynegder
+\mydesc{typing:}{\myctx \vdash \mytmsyn \Updownarrow \mytmsyn}{
\AxiomC{$
\begin{array}{c}
\mytyc{D} : \mytele \myarr \mytyp \in \myctx \hspace{1cm}
In the end, as we saw, we can devise general structures like $\mytyc{W}$
that can express all inductive structures. However, using those tools
beyond very simple examples is near-impossible for a human user. Thus
-all theorem provers in use provide some mean for the user to define
-structures tailored to specific uses.
+most theorem provers in the wild provide some means for the user to
+define structures tailored to specific uses.
-Even if we take user defined data types for granted, there are two broad
-schools of thought regarding how to manipulate them:
+Even if we take user defined types for granted, while there is not much
+debate on how to handle record, there are two broad schools of thought
+regarding the handling of data types:
\begin{description}
-\item[Fixed points and pattern matching] The road chose by Agda and Coq.
+\item[Fixed points and pattern matching] The road chosen by Agda and Coq.
Functions are written like in Haskell---matching on the input and with
explicit recursion. An external check on the recursive arguments
ensures that they are decreasing, and thus that all functions
reduce every data type to simple definitions which guarantee
termination and are simple to reduce and type. It is however more
cumbersome to use than pattern maching, although \cite{McBride2004}
- has shown how to implement a pattern matching interface on top of a
- larger set of combinators of those provided by \mykant.
+ has shown how to implement an expressive pattern matching interface on
+ top of a larger set of combinators of those provided by \mykant.
\end{description}
We chose the safer and easier to implement path, given the time
consistency, otherwise we can break our type systems by proving bottom,
as shown in Appendix \ref{app:hurkens}.
-However, hierarchy as presented in section \label{sec:itt} is a
+However, hierarchy as presented in section \ref{sec:itt} is a
considerable burden on the user, on various levels. Consider for
example how we recovered disjunctions in Section \ref{sec:disju}: we
have a function that takes two $\mytyp_0$ and forms a new $\mytyp_0$.
One way to solve this issue is a \emph{cumulative} hierarchy, where
$\mytyp_{l_1} : \mytyp_{l_2}$ iff $l_1 < l_2$. This way we retain
consistency, while allowing for `large' definitions that work on small
-types too. Figure \ref{fig:cumulativity} gives a formal definition of
-cumulativity for types, abstractions, and data constructors.
+types too.
+
+\begin{mydef}[Cumulativity for \mykant' base types]
+ Figure \ref{fig:cumulativity} gives a formal definition of
+ cumulativity for the base types. Similar measures can be taken for
+ user defined types, withe the type living in the least upper bound of
+ the levels where the types contained data live.
+\end{mydef}
For example we might define our disjunction to be
\[
A better option is to employ a mechanised version of what Russell called
\emph{typical ambiguity}: we let the user live under the illusion that
$\mytyp : \mytyp$, but check that the statements about types are
-consistent under the hood. $\mykant$\ implements this following the
-lines of \cite{Huet1988}. See also \citep{Harper1991} for a published
+consistent under the hood. $\mykant$\ implements this along the lines
+of \cite{Huet1988}. See also \cite{Harper1991} for a published
reference, although describing a more complex system allowing for both
explicit and explicit hierarchy at the same time.
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}.
+respective references with two $\le$ constraints. Implementation
+details are given in Section \ref{sec:hier-impl}.
Another more flexible but also more verbose alternative is the one
chosen by Agda, where levels can be quantified so that the relationship
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.
+is that we let the user define inductive types and records.
Reconciling propositions for OTT and a hierarchy had already been
investigated by Conor McBride,\footnote{See
\url{http://www.e-pig.org/epilogue/index.html?p=1098.html}.} and we
-follow his broad design plan, although with some modifications. Most of
+follow his broad design plan, although with some innovation. Most of
the work, as an extension of elaboration, is to handle reduction rules
and coercions for data types---both type constructors and data
constructors.
\subsubsection{The \mykant\ prelude, and $\myprop$ositions}
Before defining $\myprop$, we define some basic types inside $\mykant$,
-as the target for the $\myprop$ decoder:
+as the target for the $\myprop$ decoder.
+
+\begin{mydef}[\mykant' propositional prelude]\ \end{mydef}
\[
\begin{array}{l}
\myadt{\mytyc{Empty}}{}{ }{ } \\
\myreco{\mytyc{Prod}}{\myappsp (\myb{A}\ \myb{B} {:} \mytyp)}{ }{\myfun{fst} : \myb{A}, \myfun{snd} : \myb{B} }
\end{array}
\]
-When using $\mytyc{Prod}$, we shall use $\myprod$ to define `nested'
-products, and $\myproj{n}$ to project elements from them, so that
-\[
-\begin{array}{@{}l}
-\mytya \myprod \mytyb = \mytyc{Prod} \myappsp \mytya \myappsp (\mytyc{Prod} \myappsp \mytyb \myappsp \myunit) \\
-\mytya \myprod \mytyb \myprod \myse{C} = \mytyc{Prod} \myappsp \mytya \myappsp (\mytyc{Prod} \myappsp \mytyb \myappsp (\mytyc{Prod} \myappsp \mytyc \myappsp \myunit)) \\
-\myind{2} \vdots \\
-\myproj{1} : \mytyc{Prod} \myappsp \mytya \myappsp \mytyb \myarr \mytya \\
-\myproj{2} : \mytyc{Prod} \myappsp \mytya \myappsp (\mytyc{Prod} \myappsp \mytyb \myappsp \myse{C}) \myarr \mytyb \\
-\myind{2} \vdots
-\end{array}
-\]
-And so on, so that $\myproj{n}$ will work with all products with at
-least than $n$ elements. Then we can define propositions, and decoding:
+\begin{mydef}[Propositions and decoding]\ \end{mydef}
+\mynegder
\mydesc{syntax}{ }{
$
\begin{array}{r@{\ }c@{\ }l}
\end{array}
$
}
-
+\mynegder
\mydesc{proposition decoding:}{\myprdec{\mytmsyn} \myred \mytmsyn}{
\begin{tabular}{cc}
$
&
$
\begin{array}{r@{ }c@{ }l@{\ }c@{\ }l}
- \myprdec{&\myse{P} \myand \myse{Q} &} & \myred & \myprdec{\myse{P}} \myprod \myprdec{\myse{Q}} \\
+ \myprdec{&\myse{P} \myand \myse{Q} &} & \myred & \mytyc{Prod} \myappsp \myprdec{\myse{P}} \myappsp \myprdec{\myse{Q}} \\
\myprdec{&\myprfora{\myb{x}}{\mytya}{\myse{P}} &} & \myred &
\myfora{\myb{x}}{\mytya}{\myprdec{\myse{P}}}
\end{array}
\end{tabular}
}
-Adopting the same convention as with $\mytyp$-level products, we will
-nest $\myand$ in the same way.
+We will overload the $\myand$ symbol to define `nested' products, and
+$\myproj{n}$ to project elements from them, so that
+\[
+\begin{array}{@{}l}
+\mytya \myand \mytyb = \mytya \myand (\mytyb \myand \mytop) \\
+\mytya \myand \mytyb \myand \myse{C} = \mytya \myand (\mytyb \myand (\myse{C} \myand \mytop)) \\
+\myind{2} \vdots \\
+\myproj{1} : \myprdec{\mytya \myand \mytyb} \myarr \myprdec{\mytya} \\
+\myproj{2} : \myprdec{\mytya \myand \mytyb \myand \myse{C}} \myarr \myprdec{\mytyb} \\
+\myind{2} \vdots
+\end{array}
+\]
+And so on, so that $\myproj{n}$ will work with all products with at
+least than $n$ elements. Logically a 0-ary $\myand$ will correspond to
+$\mytop$.
\subsubsection{Some OTT examples}
Before presenting the direction that $\mykant$\ takes, let us consider
-some examples of use-defined data types, and the result we would expect,
+two examples of use-defined data types, and the result we would expect
given what we already know about OTT, assuming the same propositional
equalities.
\begin{description}
-\item[Product types] Let's consider first the already mentioned
+\item[Product types] Let us consider first the already mentioned
dependent product, using the alternate name $\mysigma$\footnote{For
extra confusion, `dependent products' are often called `dependent
sums' in the literature, referring to the interpretation that
\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
+ First type-level equality. The result we want is
\[
\begin{array}{@{}l}
\mysigma \myappsp \mytya_1 \myappsp \mytyb_1 \myeq \mysigma \myappsp \mytya_2 \myappsp \mytyb_2 \myred \\
(& \mydc{cons} \myappsp \mytmm_1 \myappsp \mytmn_1 & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{nil} & : & \myapp{\mylist}{\mytya_2} &) \myred \mybot
\end{array}
\]
- % TODO quotation
\item[Evil type]
- Now for something useless but complicated.
+ Now for something useless but complicated. % TODO finish
\end{description}
\subsubsection{Only one equality}
-Given the examples above, a more `flexible' heterogeneous emerged, since
-of the fact that in $\mykant$ we re-gain the possibility of abstracting
-and in general handling sets in a way that was not possible in the
-original OTT presentation. Moreover, we found that the rules for value
-equality work very well if used with user defined type
+Given the examples above, a more `flexible' heterogeneous equality must
+emerge, since of the fact that in $\mykant$ we re-gain the possibility
+of abstracting and in general handling types in a way that was not
+possible in the original OTT presentation. Moreover, we found that the
+rules for value equality work very well if used with user defined type
abstractions---for example in the case of dependent products we recover
the original definition with explicit binders, in a very simple manner.
}
\mynegder
-
+% TODO add syntax and types for coe and coh
\mydesc{equality reduction:}{\myctx \vdash \myprsyn \myred \myprsyn}{
\small
\begin{tabular}{cc}
\subsubsection{Coercions}
+For coercions the algorithm is messier and not reproduced here for lack
+of a decent notation---the details are hairy but uninteresting. To give
+an idea of the possible complications, let us conceive a type that
+showcases trouble not arising in the previous examples.
+\[
+\begin{array}{@{}l}
+\myadt{\mytyc{Max}}{\myappsp (\myb{A} {:} \mynat \myarr \mytyp) \myappsp (\myb{B} {:} (\myb{x} {:} \mynat) \myarr \myb{A} \myappsp \myb{x} \myarr \mytyp) \myappsp (\myb{k} {:} \mynat)}{ \\ \myind{2}}{
+ \mydc{max} \myappsp (\myb{A} \myappsp \myb{k}) \myappsp (\myb{x} {:} \mynat) \myappsp (\myb{a} {:} \myb{A} \myappsp \myb{x}) \myappsp (\myb{B} \myappsp \myb{x} \myappsp \myb{a})
+}
+\end{array}
+\]
+For type equalities we will have
+\[
+\begin{array}{@{}l@{\ }l}
+ \myjm{\mytyc{Max} \myappsp \mytya_1 \myappsp \mytyb_1 \myappsp \myse{k}_1}{\mytyp}{\mytyc{Max} \myappsp \mytya_2 \myappsp \myappsp \mytyb_2 \myappsp \myse{k}_2}{\mytyp} & \myred \\[0.2cm]
+ \begin{array}{@{}l}
+ \myjm{\mytya_1}{\mynat \myarr \mytyp}{\mytya_2}{\mynat \myarr \mytyp} \myand \\
+ \myjm{\mytyb_1}{(\myb{x} {:} \mynat) \myarr \mytya_1 \myappsp \myb{x} \myarr \mytyp}{\mytyb_2}{(\myb{x} {:} \mynat) \myarr \mytya_2 \myappsp \myb{x} \myarr \mytyp} \\
+ \myjm{\myse{k}_1}{\mynat}{\myse{k}_2}{\mynat}
+ \end{array} & \myred \\[0.7cm]
+ \begin{array}{@{}l}
+ (\mynat \myeq \mynat \myand (\myprfora{\myb{x_1}\, \myb{x_2}}{\mynat}{\myjm{\myb{x_1}}{\mynat}{\myb{x_2}}{\mynat} \myimpl \myapp{\mytya_1}{\myb{x_1}} \myeq \myapp{\mytya_2}{\myb{x_2}}})) \myand \\
+ (\mynat \myeq \mynat \myand \left(
+ \begin{array}{@{}l}
+ \myprfora{\myb{x_1}\, \myb{x_2}}{\mynat}{\myjm{\myb{x_1}}{\mynat}{\myb{x_2}}{\mynat} \myimpl \\ \myjm{\mytyb_1 \myappsp \myb{x_1}}{\mytya_1 \myappsp \myb{x_1} \myarr \mytyp}{\mytyb_2 \myappsp \myb{x_2}}{\mytya_2 \myappsp \myb{x_2} \myarr \mytyp}}
+ \end{array}
+ \right)) \myand \\
+ \myjm{\myse{k}_1}{\mynat}{\myse{k}_2}{\mynat}
+ \end{array} & \myred \\[0.9cm]
+ \begin{array}{@{}l}
+ (\mytop \myand (\myprfora{\myb{x_1}\, \myb{x_2}}{\mynat}{\myjm{\myb{x_1}}{\mynat}{\myb{x_2}}{\mynat} \myimpl \myapp{\mytya_1}{\myb{x_1}} \myeq \myapp{\mytya_2}{\myb{x_2}}})) \myand \\
+ (\mytop \myand \left(
+ \begin{array}{@{}l}
+ \myprfora{\myb{x_1}\, \myb{x_2}}{\mynat}{\myjm{\myb{x_1}}{\mynat}{\myb{x_2}}{\mynat} \myimpl \\
+ \myprfora{\myb{y_1}}{\mytya_1 \myappsp \myb{x_1}}{\myprfora{\myb{y_2}}{\mytya_2 \myappsp \myb{x_2}}{\myjm{\myb{y_1}}{\mytya_1 \myappsp \myb{x_1}}{\myb{y_2}}{\mytya_2 \myappsp \myb{x_2}} \myimpl \\
+ \mytyb_1 \myappsp \myb{x_1} \myappsp \myb{y_1} \myeq \mytyb_2 \myappsp \myb{x_2} \myappsp \myb{y_2}}}}
+ \end{array}
+ \right)) \myand \\
+ \myjm{\myse{k}_1}{\mynat}{\myse{k}_2}{\mynat}
+ \end{array} &
+\end{array}
+\]
+The result, while looking complicated, is actually saying something
+simple---given equal inputs, the parameters for $\mytyc{Max}$ will
+return equal types. Moreover, we have evidence that the two $\myb{k}$
+parameters are equal. When coercing, we need to mechanically generate
+one proof of equality for each argument, and then coerce:
+\[
+\begin{array}{@{}l}
+\mycoee{(\mytyc{Max} \myappsp \mytya_1 \myappsp \mytyb_1 \myappsp \myse{k}_1)}{(\mytyc{Max} \myappsp \mytya_2 \myappsp \mytyb_2 \myappsp \myse{k}_2)}{\myse{Q}}{(\mydc{max} \myappsp \myse{ak}_1 \myappsp \myse{n}_1 \myappsp \myse{a}_1 \myappsp \myse{b}_1)} \myred \\
+\myind{2}
+\begin{array}[t]{l@{\ }l@{\ }c@{\ }l}
+ \mysyn{let} & \myb{Q_{Ak}} & \mapsto & \myhole{?} : \myprdec{\mytya_1 \myappsp \myse{k}_1 \myeq \mytya_2 \myappsp \myse{k}_2} \\
+ & \myb{ak_2} & \mapsto & \mycoee{(\mytya_1 \myappsp \myse{k}_1)}{(\mytya_2 \myappsp \myse{k}_2)}{\myb{Q_{Ak}}}{\myse{ak_1}} : \mytya_1 \myappsp \myse{k}_2 \\
+ & \myb{Q_{\mathbb{N}}} & \mapsto & \myhole{?} : \myprdec{\mynat \myeq \mynat} \\
+ & \myb{n_2} & \mapsto & \mycoee{\mynat}{\mynat}{\myb{Q_{\mathbb{N}}}}{\myse{n_1}} : \mynat \\
+ & \myb{Q_A} & \mapsto & \myhole{?} : \myprdec{\mytya_1 \myappsp \myse{n_1} \myeq \mytya_2 \myappsp \myb{n_2}} \\
+ & \myb{a_2} & \mapsto & \mycoee{(\mytya_1 \myappsp \myse{n_1})}{(\mytya_2 \myappsp \myb{n_2})}{\myb{Q_A}} : \mytya_2 \myappsp \myb{n_2} \\
+ & \myb{Q_B} & \mapsto & \myhole{?} : \myprdec{\mytyb_1 \myappsp \myse{n_1} \myappsp \myse{a}_1 \myeq \mytyb_1 \myappsp \myb{n_2} \myappsp \myb{a_2}} \\
+ & \myb{b_2} & \mapsto & \mycoee{(\mytyb_1 \myappsp \myse{n_1} \myappsp \myse{a_1})}{(\mytyb_2 \myappsp \myb{n_2} \myappsp \myb{a_2})}{\myb{Q_B}} : \mytyb_2 \myappsp \myb{n_2} \myappsp \myb{a_2} \\
+ \mysyn{in} & \multicolumn{3}{@{}l}{\mydc{max} \myappsp \myb{ak_2} \myappsp \myb{n_2} \myappsp \myb{a_2} \myappsp \myb{b_2}}
+\end{array}
+\end{array}
+\]
+For equalities regarding types that are external to the data type we can
+derive a proof by reflexivity by invoking $\mydc{refl}$ as defined in
+Section \ref{sec:lazy}, and the instantiate arguments if we need too.
+In this case, for $\mynat$, we do not have any arguments. For
+equalities concerning arguments of the type constructor or already
+coerced arguments of the type constructor we have to refer to the right
+proof and use $\mycoh$erence when due, which is where the technical
+annoyance lies:
+\[
+\begin{array}{@{}l}
+\mycoee{(\mytyc{Max} \myappsp \mytya_1 \myappsp \mytyb_1 \myappsp \myse{k}_1)}{(\mytyc{Max} \myappsp \mytya_2 \myappsp \mytyb_2 \myappsp \myse{k}_2)}{\myse{Q}}{(\mydc{max} \myappsp \myse{ak}_1 \myappsp \myse{n}_1 \myappsp \myse{a}_1 \myappsp \myse{b}_1)} \myred \\
+\myind{2}
+\begin{array}[t]{l@{\ }l@{\ }c@{\ }l}
+ \mysyn{let} & \myb{Q_{Ak}} & \mapsto & (\myproj{2} \myappsp (\myproj{1} \myappsp \myse{Q})) \myappsp \myse{k_1} \myappsp \myse{k_2} \myappsp (\myproj{3} \myappsp \myse{Q}) : \myprdec{\mytya_1 \myappsp \myse{k}_1 \myeq \mytya_2 \myappsp \myse{k}_2} \\
+ & \myb{ak_2} & \mapsto & \mycoee{(\mytya_1 \myappsp \myse{k}_1)}{(\mytya_2 \myappsp \myse{k}_2)}{\myb{Q_{Ak}}}{\myse{ak_1}} : \mytya_1 \myappsp \myse{k}_2 \\
+ & \myb{Q_{\mathbb{N}}} & \mapsto & \mydc{refl} \myappsp \mynat : \myprdec{\mynat \myeq \mynat} \\
+ & \myb{n_2} & \mapsto & \mycoee{\mynat}{\mynat}{\myb{Q_{\mathbb{N}}}}{\myse{n_1}} : \mynat \\
+ & \myb{Q_A} & \mapsto & (\myproj{2} \myappsp (\myproj{1} \myappsp \myse{Q})) \myappsp \myse{n_1} \myappsp \myb{n_2} \myappsp (\mycohh{\mynat}{\mynat}{\myb{Q_{\mathbb{N}}}}{\myse{n_1}}) : \myprdec{\mytya_1 \myappsp \myse{n_1} \myeq \mytya_2 \myappsp \myb{n_2}} \\
+ & \myb{a_2} & \mapsto & \mycoee{(\mytya_1 \myappsp \myse{n_1})}{(\mytya_2 \myappsp \myb{n_2})}{\myb{Q_A}} : \mytya_2 \myappsp \myb{n_2} \\
+ & \myb{Q_B} & \mapsto & (\myproj{2} \myappsp (\myproj{2} \myappsp \myse{Q})) \myappsp \myse{n_1} \myappsp \myb{n_2} \myappsp \myb{Q_{\mathbb{N}}} \myappsp \myse{a_1} \myappsp \myb{a_2} \myappsp (\mycohh{(\mytya_1 \myappsp \myse{n_1})}{(\mytya_2 \myappsp \myse{n_2})}{\myb{Q_A}}{\myse{a_1}}) : \myprdec{\mytyb_1 \myappsp \myse{n_1} \myappsp \myse{a}_1 \myeq \mytyb_1 \myappsp \myb{n_2} \myappsp \myb{a_2}} \\
+ & \myb{b_2} & \mapsto & \mycoee{(\mytyb_1 \myappsp \myse{n_1} \myappsp \myse{a_1})}{(\mytyb_2 \myappsp \myb{n_2} \myappsp \myb{a_2})}{\myb{Q_B}} : \mytyb_2 \myappsp \myb{n_2} \myappsp \myb{a_2} \\
+ \mysyn{in} & \multicolumn{3}{@{}l}{\mydc{max} \myappsp \myb{ak_2} \myappsp \myb{n_2} \myappsp \myb{a_2} \myappsp \myb{b_2}}
+\end{array}
+\end{array}
+\]
+
+
% TODO finish
\subsubsection{$\myprop$ and the hierarchy}
\myprdec{\mynat \myarr \mybool \myeq \mynat \myarr \mybool} \myred
\mytop \myand ((\myb{x}\, \myb{y} : \mynat) \myarr \mytop \myarr \mytop)
\]
-we will better make sure that the `to be decoded' is at the same
-level as its reduction as to preserve subject reduction. In the example
-above, we'll have that proposition to be at least as large as the type
-of $\mynat$, since the reduced proof will abstract over it. Pretending
-that we had explicit, non cumulative levels, it would be tempting to have
+we will better make sure that the `to be decoded' is at level compatible
+(read: larger) with its reduction. In the example above, we'll have
+that proposition to be at least as large as the type of $\mynat$, since
+the reduced proof will abstract over it. Pretending that we had
+explicit, non cumulative levels, it would be tempting to have
\begin{center}
\begin{tabular}{cc}
\AxiomC{$\myjud{\myse{Q}}{\myprop_l}$}
\]
which reduces to
\[\myjm{\mynat}{\mytyp_0}{\mybool}{\mytyp_0} : \myprop_0 \]
-We need $\myprop_0$ to be $\myprop_1$ too, which will be the case with
-cumulativity. This is not the most elegant of systems, but it buys us a
-cheap type level equality without having to replicate functionality with
-a dedicated construct.
+We need members of $\myprop_0$ to be members of $\myprop_1$ too, which
+will be the case with cumulativity. This is not the most elegant of
+systems, but it buys us a cheap type level equality without having to
+replicate functionality with a dedicated construct.
\subsubsection{Quotation and definitional equality}
\label{sec:kant-irr}
reduction and quotation. However, this has the considerable
disadvantage that we can never identify abstracted
variables\footnote{And in general neutral terms, although we currently
- don't have neutral propositions.} of type $\mytyp$ as $\myprop$, thus
-forbidding the user to talk about $\myprop$ explicitly.
+ don't have neutral propositions apart from equalities on neutral
+ terms.} of type $\mytyp$ as $\myprop$, thus forbidding the user to
+talk about $\myprop$ explicitly.
This is a considerable impediment, for example when implementing
\emph{quotient types}. With quotients, we let the user specify an
propositional, a fact which prevented the use of quotients in dependent
type theories \citep{Jacobs1994}.
-\section{\mykant : The practice}
+\section{\mykant : the practice}
\label{sec:kant-practice}
-The codebase consists of around 2500 lines of Haskell, as reported by
+The codebase consists of around 2500 lines of Haskell,\footnote{The full
+ source code is available under the GPL3 license at
+ \url{https://github.com/bitonic/kant}. `Kant' was a previous
+ incarnation of the software, and the name remained.} as reported by
the \texttt{cloc} utility. The high level design is inspired by the
work on various incarnations of Epigram, and specifically by the first
-version as described \citep{McBride2004} 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.
+version as described \citep{McBride2004}.
The author learnt the hard way the implementation challenges for such a
project, and ran out of time while implementing observational equality.
\ref{fig:kant-process}.
\begin{figure}[t]
-{\small\begin{verbatim}B E R T U S
+{\small\begin{Verbatim}[frame=leftline,xleftmargin=3cm]
+B E R T U S
Version 0.0, made in London, year 2013.
>>> :h
<decl> Declare value/data type/record
>>> :e plus three two
suc (suc (suc (suc (suc zero))))
>>> :t plus three two
-Type: Nat\end{verbatim}
+Type: Nat
+\end{Verbatim}
}
\caption{A sample run of the \mykant\ prompt.}
The syntax of \mykant\ is presented in Figure \ref{fig:syntax}.
Examples showing the usage of most of the constructs are present in
Appendices \ref{app:kant-itt}, \ref{app:kant-examples}, and
-\ref{app:hurkens}.
+\ref{app:hurkens}; plus a tutorial in Section \ref{sec:type-holes}. The
+syntax has grown organically with the needs of the language, and thus it
+is not very sophisticated, being specified in and processed by a parser
+generated with the \texttt{happy} parser generated for Haskell.
+Tokenisation is performed by a simple hand written lexer.
\begin{figure}[p]
+ \centering
$
\begin{array}{@{\ \ }l@{\ }c@{\ }l}
\multicolumn{3}{@{}l}{\text{A name, in regexp notation.}} \\
$\langle\text{angle brackets}\rangle$ for greater clarity. The
syntax in the implementation is actually more liberal, for example
giving the possibility of using arrow types directly in
- constructor/projection declarations.}
+ constructor/projection declarations.\\
+ Additionally, we give the user the possibility of using Unicode
+ characters instead of their ASCII counterparts, e.g. \texttt{→} in
+ place of \texttt{->}, \texttt{λ} in place of
+ \texttt{\textbackslash}, etc.}
\label{fig:syntax}
\end{figure}
-\subsection{Term and context representation}
+\subsection{Term representation}
\label{sec:term-repr}
\subsubsection{Naming and substituting}
terms to compare them---a useful tutorial on this technique is given by
\cite{Loh2010}.
-\subsubsection{Context}
-
-Given our term type parametrised on the type of the variables,
-
-% TODO finish
-
\subsection{Turning constraints into graphs}
\label{sec:hier-impl}
-As an interlude from all the types, we will explain how to
-implement the typical ambiguity we have spoken about in
-\ref{sec:term-hierarchy} efficiently. As mentioned, we have to verify a the
-consistency of a set of constraints each time we add a new one. The
-constraints range over some set of variables whose members we will
-denote with $x, y, z, \dots$. and are of two kinds:
+In this section we will explain how to implement the typical ambiguity
+we have spoken about in \ref{sec:term-hierarchy} efficiently, a subject
+which is often dismissed in the literature. As mentioned, we have to
+verify a the consistency of a set of constraints each time we add a new
+one. The constraints range over some set of variables whose members we
+will denote with $x, y, z, \dots$. and are of two kinds:
\begin{center}
\begin{tabular}{cc}
$x \le y$ & $x < y$
constraints, $\le$ constraints are replaced by $<$ constraints, so that
if we started with an empty set and added
\[
- x < y,\ y \le z,\ z \le k,\ k < j,\ j \le y\, z < k
+ x < y,\ y \le z,\ z \le k,\ k < j,\ j \le y\
\]
-it would generate the graph shown in Figure \ref{fig:graph-one}.
+it would generate the graph shown in Figure \ref{fig:graph-one-before},
+but adding $z < k$ would strengthen the edge from $z$ to $k$, as shown
+in \ref{fig:graph-one-after}.
\begin{figure}[t]
\centering
\path[->]
(x) edge node [above] {$<$} (y)
(y) edge node [above] {$\le$} (z)
- (z) edge node [right] {$<$} (k)
+ (z) edge node [right] {$\le$} (k)
(k) edge node [below] {$\le$} (j)
(j) edge node [left ] {$\le$} (y);
\end{tikzpicture}
\end{tikzpicture}
\begin{tikzpicture}[remember picture, overlay]
\begin{pgfonlayer}{background}
- \fill [red, opacity=0.3]
- (-2.5,2.4) rectangle (-0.4,0.2)
- (-4,2.4) rectangle (-3.3,1.6);
+ \fill [red, opacity=0.3, rounded corners]
+ (-2.7,2.6) rectangle (-0.2,0.05)
+ (-4.1,2.4) rectangle (-3.3,1.6);
\end{pgfonlayer}{background}
\end{tikzpicture}
\caption{SCCs.}
\label{fig:graph-one}
\end{figure}
-\subsection{Type holes}
+Each time we add a new constraint, we check if any strongly connected
+component (SCC) arises, a SCC being a subset $V$ of vertices where for
+each $v_1,v_2 \in V$ there is a path from $v_1$ to $v_2$. The SCCs in
+the graph for the constraints above is shown in Figure
+\ref{fig:graph-one-scc}. If we have a strongly connected component with
+a $<$ edge---say $x < y$---in it, we have an inconsistency, since there
+must also be a path from $y$ to $x$, and by transitivity it must either
+be the case that $y \le x$ or $y < x$, which are both at odds with $x <
+y$.
+
+Moreover, if we have a SCC with no $<$ edges, it means that all members
+of said SCC are equal, since for every $x \le y$ we have a path from $y$
+to $x$, which again by transitivity means that $y \le x$. Thus, we can
+\emph{condense} the SCC to a single vertex, by choosing a variable among
+the SCC as a representative for all the others. This can be done
+efficiently with disjoint set data structure.
+
+\subsection{Tooling}
+
+\subsubsection{A type holes tutorial}
\label{sec:type-holes}
Type holes are, in the author's opinion, one of the `killer' features of
developing a proof or a program we can insert a hole to have the
software tell us the type expected at that point. Furthermore, we can
ask for the type of variables in context, to better understand our
-sorroundings.
+surroundings. Here we give a short tutorial in \mykant\ of this tool to
+give an idea of its usefulness.
+
+Suppose we wanted to define the `less or equal' ordering on natural
+numbers as described in Section \ref{sec:user-type}. We will
+incrementally build our functions in a file called \texttt{le.ka}.
+First we define the necessary types, all of which we know well by now:
+\begin{Verbatim}
+data Nat : ⋆ ⇒ { zero : Nat | suc : Nat → Nat }
+
+data Empty : ⋆ ⇒ { }
+absurd [A : ⋆] [p : Empty] : A ⇒ (
+ Empty-Elim p (λ _ ⇒ A)
+)
+
+record Unit : ⋆ ⇒ tt { }
+\end{Verbatim}
+Then fire up \mykant, and load the file:
+\begin{Verbatim}[frame=leftline]
+% ./bertus
+B E R T U S
+Version 0.0, made in London, year 2013.
+>>> :l le.ka
+OK
+\end{Verbatim}
+So far so good. Our definition will be defined by recursion on a
+natural number \texttt{n}, which will return a function that given
+another number \texttt{m} will return the trivial type \texttt{Unit} if
+$\texttt{n} \le \texttt{m}$, and the \texttt{Empty} type otherwise.
+However we are still not sure on how to define it, so we invoke
+$\texttt{Nat-Elim}$, the eliminator for natural numbers, and place holes
+instead of arguments. In the file we will write:
+\begin{Verbatim}
+le [n : Nat] : Nat → ⋆ ⇒ (
+ Nat-Elim n (λ _ ⇒ Nat → ⋆)
+ {|h1|}
+ {|h2|}
+)
+\end{Verbatim}
+And then we reload in \mykant:
+\begin{Verbatim}[frame=leftline]
+>>> :r le.ka
+Holes:
+ h1 : Nat → ⋆
+ h2 : Nat → (Nat → ⋆) → Nat → ⋆
+\end{Verbatim}
+Which tells us what types we need to satisfy in each hole. However, it
+is not that clear what does what in each hole, and thus it is useful to
+have a definition vacuous in its arguments just to clear things up. We
+will use \texttt{Le} aid in reading the goal, with \texttt{Le m n} as a
+reminder that we to return the type corresponding to $\texttt{m} ≤
+\texttt{n}$:
+\begin{Verbatim}
+Le [m n : Nat] : ⋆ ⇒ ⋆
-In \mykant\
+le [n : Nat] : [m : Nat] → Le n m ⇒ (
+ Nat-Elim n (λ n ⇒ [m : Nat] → Le n m)
+ {|h1|}
+ {|h2|}
+)
+\end{Verbatim}
+\begin{Verbatim}[frame=leftline]
+>>> :r le.ka
+Holes:
+ h1 : [m : Nat] → Le zero m
+ h2 : [x : Nat] → ([m : Nat] → Le x m) → [m : Nat] → Le (suc x) m
+\end{Verbatim}
+This is much better! \mykant, when printing terms, does not substitute
+top-level names for their bodies, since usually the resulting term is
+much clearer. As a nice side-effect, we can use tricks like this to
+find guidance.
+
+In this case in the first case we need to return, given any number
+\texttt{m}, $0 \le \texttt{m}$. The trivial type will do, since every
+number is less or equal than zero:
+\begin{Verbatim}
+le [n : Nat] : [m : Nat] → Le n m ⇒ (
+ Nat-Elim n (λ n ⇒ [m : Nat] → Le n m)
+ (λ _ ⇒ Unit)
+ {|h2|}
+)
+\end{Verbatim}
+\begin{Verbatim}[frame=leftline]
+>>> :r le.ka
+Holes:
+ h2 : [x : Nat] → ([m : Nat] → Le x m) → [m : Nat] → Le (suc x) m
+\end{Verbatim}
+Now for the important case. We are given our comparison function for a
+number, and we need to produce the function for the successor. Thus, we
+need to re-apply the induction principle on the other number, \texttt{m}:
+\begin{Verbatim}
+le [n : Nat] : [m : Nat] → Le n m ⇒ (
+ Nat-Elim n (λ n ⇒ [m : Nat] → Le n m)
+ (λ _ ⇒ Unit)
+ (λ n' f m ⇒ Nat-Elim m (λ m' ⇒ Le (suc n') m') {|h2|} {|h3|})
+)
+\end{Verbatim}
+\begin{Verbatim}[frame=leftline]
+>>> :r le.ka
+Holes:
+ h2 : ⋆
+ h3 : [x : Nat] → Le (suc n') x → Le (suc n') (suc x)
+\end{Verbatim}
+In the first hole we know that the second number is zero, and thus we
+can return empty. In the second case, we can use the recursive argument
+\texttt{f} on the two numbers:
+\begin{Verbatim}
+le [n : Nat] : [m : Nat] → Le n m ⇒ (
+ Nat-Elim n (λ n ⇒ [m : Nat] → Le n m)
+ (λ _ ⇒ Unit)
+ (λ n' f m ⇒
+ Nat-Elim m (λ m' ⇒ Le (suc n') m') Empty (λ f _ ⇒ f m'))
+)
+\end{Verbatim}
+We can verify that our function works as expected:
+\begin{Verbatim}[frame=leftline]
+>>> :e le zero zero
+Unit
+>>> :e le zero (suc zero)
+Unit
+>>> :e le (suc (suc zero)) (suc zero)
+Empty
+\end{Verbatim}
+Another functionality of type holes is examining types of things in
+context. Going back to the examples in Section \ref{sec:term-types}, we can
+implement the safe \texttt{head} function with our newly defined
+\texttt{le}:
+\begin{Verbatim}
+data List : [A : ⋆] → ⋆ ⇒
+ { nil : List A | cons : A → List A → List A }
-\subsection{Web REPL}
+length [A : ⋆] [l : List A] : Nat ⇒ (
+ List-Elim l (λ _ ⇒ Nat) zero (λ _ _ n ⇒ suc n)
+)
+gt [n m : Nat] : ⋆ ⇒ (le (suc m) n)
+
+head [A : ⋆] [l : List A] : gt (length A l) zero → A ⇒ (
+ List-Elim l (λ l ⇒ gt (length A l) zero → A)
+ (λ p ⇒ {|h1 p|})
+ {|h2|}
+)
+\end{Verbatim}
+We define \texttt{List}s, a polymorphic \texttt{length} function, and
+express $<$ (\texttt{gt}) in terms of $\le$. Then, we set up the type
+for our \texttt{head} function. Given a list and a proof that its
+length is greater than zero, we return the first element. If we load
+this in \mykant, we get:
+\begin{Verbatim}[frame=leftline]
+>>> :r le.ka
+Holes:
+ h1 : A
+ p : Empty
+ h2 : [x : A] [x1 : List A] →
+ (gt (length A x1) zero → A) →
+ gt (length A (cons x x1)) zero → A
+\end{Verbatim}
+In the first case (the one for \texttt{nil}), we have a proof of
+\texttt{Empty}---surely we can use \texttt{absurd} to get rid of that
+case. In the second case we simply return the element in the
+\texttt{cons}:
+\begin{Verbatim}
+head [A : ⋆] [l : List A] : gt (length A l) zero → A ⇒ (
+ List-Elim l (λ l ⇒ gt (length A l) zero → A)
+ (λ p ⇒ absurd A p)
+ (λ x _ _ _ ⇒ x)
+)
+\end{Verbatim}
+
+This should give a vague idea of why type holes are so useful and in
+more in general about the development process in \mykant. Most
+interactive theorem provers offer some kind of facility
+to... interactively develop proofs, usually much more powerful than the
+fairly bare tools present in \mykant. Agda in particular offers a
+particularly powerful mode for the \texttt{Emacs} text editor.
+
+\subsubsection{Web REPL}
\section{Evaluation}
+\label{sec:evaluation}
\section{Future work}
\label{sec:future-work}
\begin{description}
\item[Pattern matching] Eliminators are very clumsy to use, and
-\item[More powerful data types] Beyond normal inductive data types,
- \mykant\ does not in more sophisticated notions. A popular
- improvements on basic data types are inductive families, where the
- parameters for the type constructors change based on the data
- constructors, which lets us express naturally types such as
- $\mytyc{Vec} : \mynat \myarr \mytyp$, which given a number returns the
- type of lists of that length, or $\mytyc{Fin} : \mynat \myarr \mytyp$,
- which given a number $n$ gives the type of numbers less than $n$.
- This apparent omission was motivated by the fact that inductive
- families can be represented by adding equalities concerning the
- parameters of the type constructors as arguments to the data
- constructor, in much the same way that Generalised Abstract Data Types
- \citep{GHC} are handled in Haskell, where interestingly the modified
- version of System F that lies at the core of recent versions of GHC
- features coercions similar to those found in OTT \citep{Sulzmann2007}.
+\item[More powerful data types] A popular improvement on basic data
+ types are inductive families \cite{Dybjer1991}, where the parameters
+ for the type constructors can change based on the data constructors,
+ which lets us express naturally types such as $\mytyc{Vec} : \mynat
+ \myarr \mytyp$, which given a number returns the type of lists of that
+ length, or $\mytyc{Fin} : \mynat \myarr \mytyp$, which given a number
+ $n$ gives the type of numbers less than $n$. This apparent omission
+ was motivated by the fact that inductive families can be represented
+ by adding equalities concerning the parameters of the type
+ constructors as arguments to the data constructor, in much the same
+ way that Generalised Abstract Data Types \citep{GHC} are handled in
+ Haskell, where interestingly the modified version of System F that
+ lies at the core of recent versions of GHC features coercions similar
+ to those found in OTT \citep{Sulzmann2007}.
+
+ The notion of inductive family also yields a more interesting notion
+ of pattern matching, since matching on an argument influences the
+ value of the parameters of the type of said argument. This means that
+ pattern matching influences the context, which can be exploited to
+ constraint the possible constructors in \emph{other} arguments
+ \cite{McBride2004}.
Another popular extension introduced by \cite{dybjer2000general} is
induction-recursion, where we define a data type in tandem with a
\item[Coinduction] \cite{cockett1992charity} \cite{mcbride2009let}.
\end{description}
-
-
-\subsection{Coinduction}
-
-\subsection{Quotient types}
-
-\subsection{Partiality}
-
-\subsection{Pattern matching}
-
-\subsection{Pattern unification}
-
% TODO coinduction (obscoin, gimenez, jacobs), pattern unification (miller,
% gundry), partiality monad (NAD)
\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}$
\end{array}
\]
+I will from time to time give examples in the Haskell programming
+language as defined in \citep{Haskell2010}, which I will typeset in
+\texttt{teletype} font. I assume that the reader is already familiar
+with Haskell, plenty of good introductions are available
+\citep{LYAH,ProgInHask}.
+
+Examples of \mykant\ code will be typeset nicely with \LaTeX in Section
+\ref{sec:kant-theory}, to adjust with the rest of the presentation; and
+in \texttt{teletype} font in the rest of the document, including Section
+\ref{sec:kant-practice} and in the appendices. Snippets of sessions in
+the \mykant\ prompt will be displayed with a left border, to distinguish
+them from snippets of code:
+\begin{Verbatim}[frame=leftline]
+>>> :t ⋆
+Type: ⋆
+\end{Verbatim}
+
\section{Code}
\subsection{ITT renditions}
projects / bitonic-mengthesis.git / commitdiff