From fb4e0b4b2daac3838f6161836298cd4d1bf54766 Mon Sep 17 00:00:00 2001 From: Francesco Mazzoli Date: Fri, 14 Jun 2013 01:07:45 +0100 Subject: [PATCH] ... --- thesis.bib | 32 +- thesis.lagda | 949 ++++++++++++++++++++++++++++++++------------------- 2 files changed, 625 insertions(+), 356 deletions(-) diff --git a/thesis.bib b/thesis.bib index 5ca5dc0..e8a23d9 100644 --- a/thesis.bib +++ b/thesis.bib @@ -378,16 +378,12 @@ year = {2012} } @ARTICLE{Jacobs1994, - author = {Jacobs, Bart}, - title = {Quotients in simple type theory}, - journal = {available from the Hypatia Electronic Library: http://hypatia. dcs. - qmw. ac. uk}, - year = {1994}, - file = {:/home/bitonic/docs/papers/jacobs-quotients.pdf:PDF}, - publisher = {Citeseer} + author = {Jacobs, Bart}, + title = {Quotients in Simple Type Theory}, + journal = {Manuscript, Math. Inst}, + year = {1994} } - @inproceedings{Hofmann1994, title={The groupoid model refutes uniqueness of identity proofs}, author={Hofmann, Martin and Streicher, Thomas}, @@ -470,4 +466,24 @@ year = {2012} pages={333--345}, year={2011}, organization={ACM} +} + +@inproceedings{King1995, + title={Structuring depth-first search algorithms in Haskell}, + author={King, David J and Launchbury, John}, + booktitle={Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages}, + pages={344--354}, + year={1995}, + organization={ACM} +} + +@article{milner1978theory, + title={A theory of type polymorphism in programming}, + author={Milner, Robin}, + journal={Journal of computer and system sciences}, + volume={17}, + number={3}, + pages={348--375}, + year={1978}, + publisher={Elsevier} } \ No newline at end of file diff --git a/thesis.lagda b/thesis.lagda index cb80348..6ba5bf5 100644 --- a/thesis.lagda +++ b/thesis.lagda @@ -2,15 +2,17 @@ %% THIS LATEX HURTS YOUR EYES. DO NOT READ. -\documentclass[11pt, fleqn]{article} +% TODO side conditions + +\documentclass[11pt, fleqn, twoside]{article} \usepackage{etex} \usepackage[sc,slantedGreek]{mathpazo} % \linespread{1.05} % \usepackage{times} -\oddsidemargin 0in -\evensidemargin 0in +\oddsidemargin .50in +\evensidemargin -.25in \textheight 9.5in \textwidth 6.2in \topmargin -7mm @@ -19,15 +21,14 @@ \headheight 0pt \headsep 0pt +\usepackage{amsthm} -%% Narrow margins -% \usepackage{fullpage} %% Bibtex \usepackage{natbib} %% Links -\usepackage{hyperref} +\usepackage[pdftex, pdfborderstyle={/S/U/W 0}]{hyperref} %% Frames \usepackage{framed} @@ -93,14 +94,14 @@ \newcommand{\mysmall}{} \newcommand{\mysyn}{\AgdaKeyword} -\newcommand{\mytyc}{\AgdaDatatype} -\newcommand{\mydc}{\AgdaInductiveConstructor} -\newcommand{\myfld}{\AgdaField} -\newcommand{\myfun}{\AgdaFunction} +\newcommand{\mytyc}[1]{\textup{\AgdaDatatype{#1}}} +\newcommand{\mydc}[1]{\textup{\AgdaInductiveConstructor{#1}}} +\newcommand{\myfld}[1]{\textup{\AgdaField{#1}}} +\newcommand{\myfun}[1]{\textup{\AgdaFunction{#1}}} \newcommand{\myb}[1]{\AgdaBound{$#1$}} \newcommand{\myfield}{\AgdaField} \newcommand{\myind}{\AgdaIndent} -\newcommand{\mykant}{\textsc{Bertus}} +\newcommand{\mykant}{\textmd{\textsc{Bertus}}} \newcommand{\mysynel}[1]{#1} \newcommand{\myse}{\mysynel} \newcommand{\mytmsyn}{\mysynel{term}} @@ -119,7 +120,7 @@ \parbox{\textwidth}{ {\mysmall \vspace{0.2cm} - \hfill \textbf{#1} $#2$ + \hfill \textup{\textbf{#1}} $#2$ \framebox[\textwidth]{ \parbox{\textwidth}{ \vspace{0.1cm} @@ -195,7 +196,7 @@ \newcommand{\mylub}{\sqcup} \newcommand{\mydefeq}{\cong} \newcommand{\myrefl}{\mydc{refl}} -\newcommand{\mypeq}[1]{\mathrel{\mytyc{=}_{#1}}} +\newcommand{\mypeq}{\mytyc{=}} \newcommand{\myjeqq}{\myfun{$=$-elim}} \newcommand{\myjeq}[3]{\myapp{\myapp{\myapp{\myjeqq}{#1}}{#2}}{#3}} \newcommand{\mysubst}{\myfun{subst}} @@ -217,9 +218,9 @@ \newcommand{\mytmup}{\mytmsyn\uparrow} \newcommand{\mydefs}{\Delta} \newcommand{\mynf}{\Downarrow} -\newcommand{\myinff}[3]{#1 \vdash #2 \Rightarrow #3} +\newcommand{\myinff}[3]{#1 \vdash #2 \Uparrow #3} \newcommand{\myinf}[2]{\myinff{\myctx}{#1}{#2}} -\newcommand{\mychkk}[3]{#1 \vdash #2 \Leftarrow #3} +\newcommand{\mychkk}[3]{#1 \vdash #2 \Downarrow #3} \newcommand{\mychk}[2]{\mychkk{\myctx}{#1}{#2}} \newcommand{\myann}[2]{#1 : #2} \newcommand{\mydeclsyn}{\myse{decl}} @@ -258,11 +259,19 @@ \newcommand{\mynegder}{\vspace{-0.3cm}} \newcommand{\myquot}{\Uparrow} \newcommand{\mynquot}{\, \Downarrow} +\newcommand{\mycanquot}{\ensuremath{\textsc{quote}{\Uparrow}}} +\newcommand{\myneuquot}{\ensuremath{\textsc{quote}{\Downarrow}}} +\newcommand{\mymetaguard}{\ |\ } +\newcommand{\mybox}{\Box} \renewcommand{\[}{\begin{equation*}} \renewcommand{\]}{\end{equation*}} \newcommand{\mymacol}[2]{\text{\textcolor{#1}{$#2$}}} +\newtheorem*{mydef}{Definition} +\newtheoremstyle{named}{}{}{\itshape}{}{\bfseries}{}{.5em}{\textsc{#1}} +\theoremstyle{named} + %% ----------------------------------------------------------------------------- \title{\mykant: Implementing Observational Equality} @@ -277,11 +286,19 @@ \begin{document} -\begin{titlepage} - \centering +\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] - \maketitle - \thispagestyle{empty} +\textsc{\Large Final year project}\\[0.5cm] + +% Title +{ \huge \mykant: Implementing Observational Equality}\\[1.5cm] + +{\Large Francesco \textsc{Mazzoli} \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{}}}\\[0.8cm] \begin{minipage}{0.4\textwidth} \begin{flushleft} \large @@ -291,45 +308,54 @@ \end{minipage} \begin{minipage}{0.4\textwidth} \begin{flushright} \large - \emph{Co-marker:} \\ + \emph{Second marker:} \\ Dr. Philippa \textsc{Gardner} \end{flushright} \end{minipage} +\vfill + +% Bottom of the page +{\large \today} +\end{center} \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. + The marriage between programming and logic has been a very fertile + one. In particular, since the definition of the simply typed lambda + calculus, a number of type systems have been devised with increasing + expressive power. Among this systems, Inutitionistic Type Theory (ITT) has been a very popular framework for theorem provers and programming languages. - However, 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. + However, reasoning about equality has always been a tricky business in + ITT and related theories. In this thesis we will explain why this is + the case, and present Observational Type Theory (OTT), a solution to + some of the problems with equality. + + To bring OTT closer to the current practice of interactive theorem + provers, we describe \mykant, a system featuring OTT in a setting more + close to the one found in widely used provers such as Agda and Coq. + Nost notably, we feature used defined inductive and record types and a + cumulative, implicit type hierarchy. Having implemented part of + $\mykant$ as a Haskell program, we describe some of the implementation + issues faced. \end{abstract} \clearpage \renewcommand{\abstractname}{Acknowledgements} \begin{abstract} - I would like to thank Steffen van Backel, my supervisor, who was brave + I would like to thank Steffen van Bakel, my supervisor, who was brave enough to believe in my project and who provided much advice and support. I would also like to thank the Haskell and Agda community on \texttt{IRC}, which guided me through the strange world of types; and in particular Andrea Vezzosi and James Deikun, with whom I entertained - countless insightful discussions in the past year. Andrea suggested + countless insightful discussions over the past year. Andrea suggested Observational Type Theory as a topic of study: this thesis would not - exist without him. Before them, Tony Fields introduced me to Haskell, + exist without him. Before them, Tony Field introduced me to Haskell, unknowingly filling most of my free time from that time on. Finally, much of the work stems from the research of Conor McBride, @@ -343,6 +369,8 @@ \clearpage +\section{Introduction} + \section{Simple and not-so-simple types} \label{sec:types} @@ -357,9 +385,11 @@ language, which will give the chance to introduce concepts central to the analysis of all the following calculi. The exposition follows the one found in chapter 5 of \cite{Queinnec2003}. -The syntax of $\lambda$-terms consists of three things: variables, abstractions, -and applications: - +\begin{mydef}[$\lambda$-terms] + Syntax of the $\lambda$-calculus: variables, abstractions, and + applications. +\end{mydef} +\mynegder \mydesc{syntax}{ }{ $ \begin{array}{r@{\ }c@{\ }l} @@ -369,13 +399,16 @@ and applications: $ } -Parenthesis will be omitted in the usual way: -$\myapp{\myapp{\mytmt}{\mytmm}}{\mytmn} = -\myapp{(\myapp{\mytmt}{\mytmm})}{\mytmn}$. +Parenthesis will be omitted in the usual way, with application being +left associative. Abstractions roughly corresponds to functions, and their semantics is more -formally explained by the $\beta$-reduction rule: +formally explained by the $\beta$-reduction rule. +\begin{mydef}[$\beta$-reduction] +$\beta$-reduction and substitution for the $\lambda$-calculus. +\end{mydef} +\mynegder \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{ $ \begin{array}{l} @@ -397,38 +430,52 @@ The care required during substituting variables for terms is required to avoid name capturing. We will use substitution in the future for other name-binding constructs assuming similar precautions. -These few elements are of remarkable expressiveness, and in fact Turing -complete. As a corollary, we must be able to devise a term that reduces forever -(`loops' in imperative terms): +These few elements have a remarkable expressiveness, and are in fact +Turing complete. As a corollary, we must be able to devise a term that +reduces forever (`loops' in imperative terms): \[ (\myapp{\omega}{\omega}) \myred (\myapp{\omega}{\omega}) \myred \cdots \text{, with $\omega = \myabs{x}{\myapp{x}{x}}$} \] -A \emph{redex} is a term that can be reduced. In the untyped $\lambda$-calculus -this will be the case for an application in which the first term is an -abstraction, but in general we call aterm reducible if it appears to the left of -a reduction rule. When a term contains no redexes it's said to be in -\emph{normal form}. Given the observation above, not all terms reduce to a -normal forms: we call the ones that do \emph{normalising}, and the ones that -don't \emph{non-normalising}. - -The reduction rule presented is not syntax directed, but \emph{evaluation - strategies} can be employed to reduce term systematically. Common evaluation -strategies include \emph{call by value} (or \emph{strict}), where arguments of -abstractions are reduced before being applied to the abstraction; and conversely -\emph{call by name} (or \emph{lazy}), where we reduce only when we need to do so -to proceed---in other words when we have an application where the function is -still not a $\lambda$. In both these reduction strategies we never reduce under -an abstraction: for this reason a weaker form of normalisation is used, where -both abstractions and normal forms are said to be in \emph{weak head normal - form}. +\begin{mydef}[redex] + A \emph{redex} is a term that can be reduced. +\end{mydef} +In the untyped $\lambda$-calculus this will be the case for an +application in which the first term is an abstraction, but in general we +call aterm reducible if it appears to the left of a reduction rule. +\begin{mydef}[normal form] + A term that contains no redexes is said to be in \emph{normal form}. +\end{mydef} +\begin{mydef}[normalising terms and systems] + Terms that reduce in a finite number of reduction steps to a normal + form are \emph{normalising}. A system in which all terms are + normalising is said to be have the \emph{normalisation property}, or + to be normalising. +\end{mydef} +Given the reduction behaviour of $(\myapp{\omega}{\omega})$, it is clear +that the untyped $\lambda$-calculus does not have the normalisation +property. + +We have not presented reduction in an algorithmic way, but +\emph{evaluation strategies} can be employed to reduce term +systematically. Common evaluation strategies include \emph{call by + value} (or \emph{strict}), where arguments of abstractions are reduced +before being applied to the abstraction; and conversely \emph{call by + name} (or \emph{lazy}), where we reduce only when we need to do so to +proceed---in other words when we have an application where the function +is still not a $\lambda$. In both these reduction strategies we never +reduce under an abstraction: for this reason a weaker form of +normalisation is used, where both abstractions and normal forms are said +to be in \emph{weak head normal form}. \subsection{The simply typed $\lambda$-calculus} A convenient way to `discipline' and reason about $\lambda$-terms is to assign \emph{types} to them, and then check that the terms that we are forming make -sense given our typing rules \citep{Curry1934}. The first most basic instance -of this idea takes the name of \emph{simply typed $\lambda$ calculus}, whose -rules are shown in figure \ref{fig:stlc}. +sense given our typing rules \citep{Curry1934}.The first most basic instance +of this idea takes the name of \emph{simply typed $\lambda$-calculus} (STLC). +\begin{mydef}[Simply typed $\lambda$-calculus] + The syntax and typing rules for the STLC are given in Figure \ref{fig:stlc}. +\end{mydef} Our types contain a set of \emph{type variables} $\Phi$, which might correspond to some `primitive' types; and $\myarr$, the type former for @@ -473,22 +520,23 @@ $\lambda$-calculus. In the typing rules, a context $\myctx$ is used to store the types of bound variables: $\myctx; \myb{x} : \mytya$ adds a variable to the context and -$\myctx(x)$ returns the type of the rightmost occurrence of $x$. +$\myctx(x)$ extracts the type of the rightmost occurrence of $x$. This typing system takes the name of `simply typed lambda calculus' (STLC), and enjoys a number of properties. Two of them are expected in most type systems \citep{Pierce2002}: -\begin{description} -\item[Progress] A well-typed term is not stuck---it is either a variable, or its - constructor does not appear on the left of the $\myred$ relation (currently +\begin{mydef}[Progress] + A well-typed term is not stuck---it is either a variable, or it + does not appear on the left of the $\myred$ relation (currently only $\lambda$), or it can take a step according to the evaluation rules. -\item[Preservation] If a well-typed term takes a step of evaluation, then the - resulting term is also well-typed, and preserves the previous type. Also - known as \emph{subject reduction}. -\end{description} +\end{mydef} +\begin{mydef}[Subject reduction] + If a well-typed term takes a step of evaluation, then the + resulting term is also well-typed, and preserves the previous type. +\end{mydef} However, STLC buys us much more: every well-typed term is normalising -\citep{Tait1967}. It is easy to see that we can't fill the blanks if we want to +\citep{Tait1967}. It is easy to see that we cannot fill the blanks if we want to give types to the non-normalising term shown before: \[ \myapp{(\myabss{\myb{x}}{\myhole{?}}{\myapp{\myb{x}}{\myb{x}}})}{(\myabss{\myb{x}}{\myhole{?}}{\myapp{\myb{x}}{\myb{x}}})} @@ -496,12 +544,13 @@ give types to the non-normalising term shown before: This makes the STLC Turing incomplete. We can recover the ability to loop by adding a combinator that recurses: - +\begin{mydef}[Fixed-point combinator]\end{mydef} +\mynegder \noindent \begin{minipage}{0.5\textwidth} \mydesc{syntax}{ } { $ \mytmsyn ::= \cdots b \mysynsep \myfix{\myb{x}}{\mytysyn}{\mytmsyn} $ - \vspace{0.4cm} + \vspace{0.5cm} } \end{minipage} \begin{minipage}{0.5\textwidth} @@ -511,7 +560,7 @@ adding a combinator that recurses: \DisplayProof } \end{minipage} - +\mynegder \mydesc{reduction:}{\myjud{\mytmsyn}{\mytmsyn}}{ $ \myfix{\myb{x}}{\mytya}{\mytmt} \myred \mysub{\mytmt}{\myb{x}}{(\myfix{\myb{x}}{\mytya}{\mytmt})}$ } @@ -522,9 +571,9 @@ want to use the STLC as described in the next section. \subsection{The Curry-Howard correspondence} It turns out that the STLC can be seen a natural deduction system for -intuitionistic propositional logic. Terms are proofs, and their types are the -propositions they prove. This remarkable fact is known as the Curry-Howard -correspondence, or isomorphism. +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 @@ -533,9 +582,13 @@ correct type: \[ \myabss{\myb{f}}{(\mytya \myarr \mytyb)}{\myabss{\myb{g}}{(\mytyb \myarr \mytycc)}{\myabss{\myb{x}}{\mytya}{\myapp{\myb{g}}{(\myapp{\myb{f}}{\myb{x}})}}}} \] -That is, function composition. Going beyond arrow types, we can extend our bare -lambda calculus with useful types to represent other logical constructs, as -shown in figure \ref{fig:natded}. +Which is known to functional programmers as function composition. Going +beyond arrow types, we can extend our bare lambda calculus with useful +types to represent other logical constructs. +\begin{mydef}[The extended STLC] + Figure \ref{fig:natded} shows syntax, reduction, and typing rules for + the \emph{extendend simply typed $\lambda$-calculus}. +\end{mydef} \begin{figure}[t] \mydesc{syntax}{ }{ @@ -639,22 +692,26 @@ $\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}. +The trivial type $\myunit$ corresponds to the logical $\top$ (true), and +dually $\myempty$ corresponds to the logical $\bot$ (false). $\myunit$ +has one introduction rule ($\mytt$), and thus one inhabitant; and no +eliminators. $\myempty$ has no introduction rules, and thus no +inhabitants; and one eliminator ($\myabsurd{ }$), corresponding to the +logical \emph{ex falso quodlibet}. With these rules, our STLC now looks remarkably similar in power and use to the -natural deduction we already know. $\myneg \mytya$ can be expressed as $\mytya -\myarr \myempty$. However, there is an important omission: there is no term of +natural deduction we already know. +\begin{mydef}[Negation] + $\myneg \mytya$ can be expressed as $\mytya \myarr \myempty$. +\end{mydef} +However, there is an important omission: there is no term of the type $\mytya \mysum \myneg \mytya$ (excluded middle), or equivalently $\myneg \myneg \mytya \myarr \mytya$ (double negation), or indeed any term with a type equivalent to those. -This has a considerable effect on our logic and it's no coincidence, since there +This has a considerable effect on our logic and it is no coincidence, since there is no obvious computational behaviour for laws like the excluded middle. -Theories of this kind are called \emph{intuitionistic}, or \emph{constructive}, +Logics of this kind are called \emph{intuitionistic}, or \emph{constructive}, and all the systems analysed will have this characteristic since they build on the foundation of the STLC.\footnote{There is research to give computational behaviour to classical logic, but I will not touch those subjects.} @@ -677,11 +734,13 @@ common to include (or let the user define) inductive data types. These comprise of a type former, various constructors, and an eliminator (or destructor) that serves as primitive recursor. -For example, we might add a $\mylist$ type constructor, along with an `empty +\begin{mydef}[Finite lists for the STLC] +We add a $\mylist$ type constructor, along with an `empty list' ($\mynil{ }$) and `cons cell' ($\mycons$) constructor. The eliminator for -lists will be the usual folding operation ($\myfoldr$). See figure +lists will be the usual folding operation ($\myfoldr$). Full rules in Figure \ref{fig:list}. - +\end{mydef} +\mynegder \begin{figure}[h] \mydesc{syntax}{ }{ $ @@ -756,14 +815,15 @@ Here $\lambda{\to}$, in the bottom left, is the STLC. From there can move along \begin{description} \item[Terms depending on types (towards $\lambda{2}$)] We can quantify over types in our type signatures. For example, we can define a polymorphic - identity function: + identity function, where $\mytyp$ denotes the `type of types': \[\displaystyle - (\myabss{\myb{A}}{\mytyp}{\myabss{\myb{x}}{\myb{A}}{\myb{x}}}) : (\myb{A} : \mytyp) \myarr \myb{A} \myarr \myb{A} + (\myabss{\myb{A}}{\mytyp}{\myabss{\myb{x}}{\myb{A}}{\myb{x}}}) : (\myb{A} {:} \mytyp) \myarr \myb{A} \myarr \myb{A} \] - The first and most famous instance of this idea has been System F. This form - of polymorphism and has been wildly successful, also thanks to a well known - inference algorithm for a restricted version of System F known as - Hindley-Milner. Languages like Haskell and SML are based on this discipline. + The first and most famous instance of this idea has been System F. + This form of polymorphism and has been wildly successful, also thanks + to a well known inference algorithm for a restricted version of System + F known as Hindley-Milner \citep{milner1978theory}. Languages like + Haskell and SML are based on this discipline. \item[Types depending on types (towards $\lambda{\underline{\omega}}$)] We have type operators. For example we could define a function that given types $R$ and $\mytya$ forms the type that represents a value of type $\mytya$ in @@ -787,13 +847,14 @@ logic. \subsection{A Bit of History} -Logic frameworks and programming languages based on type theory have a long -history. Per Martin-L\"{o}f described the first version of his theory in 1971, -but then revised it since the original version was inconsistent due to its -impredicativity.\footnote{In the early version there was only one universe - $\mytyp$ and $\mytyp : \mytyp$, see Section \ref{sec:term-types} for an - explanation on why this causes problems.} For this reason he gave a revised -and consistent definition later \citep{Martin-Lof1984}. +Logic frameworks and programming languages based on type theory have a +long history. Per Martin-L\"{o}f described the first version of his +theory in 1971, but then revised it since the original version was +inconsistent due to its impredicativity.\footnote{In the early version + there was only one universe $\mytyp$ and $\mytyp : \mytyp$; see + Section \ref{sec:term-types} for an explanation on why this causes + problems.} For this reason he later gave a revised and consistent +definition \citep{Martin-Lof1984}. A related development is the polymorphic $\lambda$-calculus, and specifically the previously mentioned System F, which was developed independently by Girard @@ -811,11 +872,13 @@ include Agda \citep{Norell2007, Bove2009}, Coq \citep{Coq}, and Epigram 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}. +found in \citep{Martin-Lof1984}. +\begin{mydef}[Intuitionistic Type Theory (ITT)] +The syntax and reduction rules are shown in Figure \ref{fig:core-tt-syn}. +The typing rules are presented piece by piece in the following sections. +\end{mydef} +Agda and \mykant\ renditions of the presented theory and all the +examples is reproduced in Appendix \ref{app:itt-code}. \begin{figure}[t] \mydesc{syntax}{ }{ @@ -907,12 +970,13 @@ discipline we will find that \] 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. +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. 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. +decide equality it is essential for a dependently typed system to be +terminating and confluent for type checking to be decidable, since every +type needs to have a \emph{unique} normal form. Moreover, we specify a \emph{type hierarchy} to talk about `large' types: $\mytyp_0$ will be the type of types inhabited by data: @@ -1014,13 +1078,13 @@ sure that we are invoking $\myabsurd{}$ over a type. } 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 +types'. While the two introduction rules for $\mytrue$ and $\myfalse$ +are not surprising, the typing rules for $\myfun{if}$ are. In most +strongly typed languages we expect the branches of an $\myfun{if}$ +statements to be of the same type, to preserve subject reduction, since +execution could take both paths. This is a pity, since the type system +does not reflect the fact that in each branch we gain knowledge on the +term we are branching on. Which means that programs along the lines of \begin{Verbatim} if null xs then head xs else 0 \end{Verbatim} @@ -1066,8 +1130,7 @@ 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: +language, using dependent functions we are write functions of type: \[ \begin{array}{l} \myfun{length} : (\myb{A} {:} \mytyp_0) \myarr \myapp{\mylist}{\myb{A}} \myarr \mynat \\ @@ -1086,10 +1149,20 @@ returned, $\myempty$ otherwise. This way, we can express a 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}$. +Again, we need to make sure that the type hierarchy is respected, which +is the reason why a type formed by $\myarr$ will live in the least upper +bound of the levels of argument and return type. If this was not the +case, we would be able to form a `powerset' function along the lines of +\[ +\begin{array}{@{}l} +\myfun{P} : \mytyp_0 \myarr \mytyp_0 \\ +\myfun{P} \myappsp \myb{A} \mapsto \myb{A} \myarr \mytyp_0 +\end{array} +\] +Where the type of $\myb{A} \myarr \mytyp_0$ is in $\mytyp_0$ itself. +Using this and similar devices we would be able to derive falsity +\citep{Hurkens1995}. This trend will continue with the other type-level +binders, $\myprod$ and $\mytyc{W}$. \subsubsection{$\myprod$, or dependent product} \label{sec:disju} @@ -1232,17 +1305,21 @@ notion, in this section we will explore the ways of expressing equality 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}. +formalised in Agda in Appendix \ref{app:agda-itt}. \subsection{Propositional equality} +\begin{mydef}[Propositional equality] The syntax, reduction, and typing + rules for propositional equality and related constructs is defined as: +\end{mydef} +\mynegder \noindent \begin{minipage}{0.5\textwidth} \mydesc{syntax}{ }{ $ \begin{array}{r@{\ }c@{\ }l} \mytmsyn & ::= & \cdots \\ - & | & \mytmsyn \mypeq{\mytmsyn} \mytmsyn \mysynsep + & | & \mypeq \myappsp \mytmsyn \myappsp \mytmsyn \myappsp \mytmsyn \mysynsep \myapp{\myrefl}{\mytmsyn} \\ & | & \myjeq{\mytmsyn}{\mytmsyn}{\mytmsyn} \end{array} @@ -1262,20 +1339,20 @@ formalised in Agda in appendix \ref{app:agda-itt}. \AxiomC{$\myjud{\mytya}{\mytyp_l}$} \AxiomC{$\myjud{\mytmm}{\mytya}$} \AxiomC{$\myjud{\mytmn}{\mytya}$} - \TrinaryInfC{$\myjud{\mytmm \mypeq{\mytya} \mytmn}{\mytyp_l}$} + \TrinaryInfC{$\myjud{\mypeq \myappsp \mytya \myappsp \mytmm \myappsp \mytmn}{\mytyp_l}$} \DisplayProof \myderivspp \begin{tabular}{cc} \AxiomC{$\begin{array}{c}\ \\\myjud{\mytmm}{\mytya}\hspace{1.1cm}\mytmm \mydefeq \mytmn\end{array}$} - \UnaryInfC{$\myjud{\myapp{\myrefl}{\mytmm}}{\mytmm \mypeq{\mytya} \mytmn}$} + \UnaryInfC{$\myjud{\myapp{\myrefl}{\mytmm}}{\mypeq \myappsp \mytya \myappsp \mytmm \myappsp \mytmn}$} \DisplayProof & \AxiomC{$ \begin{array}{c} - \myjud{\myse{P}}{\myfora{\myb{x}\ \myb{y}}{\mytya}{\myfora{q}{\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})}} + \myjud{\myse{P}}{\myfora{\myb{x}\ \myb{y}}{\mytya}{\myfora{q}{\mypeq \myappsp \mytya \myappsp \myb{x} \myappsp \myb{y}}{\mytyp_l}}} \\ + \myjud{\myse{q}}{\mypeq \myappsp \mytya \myappsp \mytmm \myappsp \mytmn}\hspace{1.1cm}\myjud{\myse{p}}{\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmm}}{(\myapp{\myrefl}{\mytmm})}} \end{array} $} \UnaryInfC{$\myjud{\myjeq{\myse{P}}{\myse{q}}{\myse{p}}}{\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmn}}{q}}$} @@ -1283,17 +1360,17 @@ formalised in Agda in appendix \ref{app:agda-itt}. \end{tabular} } -To express equality between two terms inside ITT, the obvious way to do so is -to have the equality construction to be a type-former. Here we present what -has survived as the dominating form of equality in systems based on ITT up to -the present day. +To express equality between two terms inside ITT, the obvious way to do +so is to have equality to be a type. Here we present what has survived +as the dominating form of equality in systems based on ITT up to the +present day. -Our type former is $\mypeq{\mytya}$, which given a type (in this case -$\mytya$) relates equal terms of that type. $\mypeq{}$ has one introduction +Our type former is $\mypeq$, which given a type (in this case +$\mytya$) relates equal terms of that type. $\mypeq$ has one introduction rule, $\myrefl$, which introduces an equality relation between definitionally equal terms. -Finally, we have one eliminator for $\mypeq{}$, $\myjeqq$. $\myjeq{\myse{P}}{\myse{q}}{\myse{p}}$ takes +Finally, we have one eliminator for $\mypeq$, $\myjeqq$. $\myjeq{\myse{P}}{\myse{q}}{\myse{p}}$ takes \begin{itemize} \item $\myse{P}$, a predicate working with two terms of a certain type (say $\mytya$) and a proof of their equality @@ -1303,22 +1380,23 @@ Finally, we have one eliminator for $\mypeq{}$, $\myjeqq$. $\myjeq{\myse{P}}{\m twice, plus the trivial proof by reflexivity showing that $\myse{m}$ is equal to itself \end{itemize} -Given these ingredients, $\myjeqq$ retuns a member of $\myse{P}$ applied to -$\mytmm$, $\mytmn$, and $\myse{q}$. In other words $\myjeqq$ takes a -witness that $\myse{P}$ works with \emph{definitionally equal} terms, and -returns a witness of $\myse{P}$ working with \emph{propositionally equal} -terms. Invokations of $\myjeqq$ will vanish when the equality proofs will -reduce to invocations to reflexivity, at which point the arguments must be -definitionally equal, and thus the provided +Given these ingredients, $\myjeqq$ retuns a member of $\myse{P}$ applied +to $\mytmm$, $\mytmn$, and $\myse{q}$. In other words $\myjeqq$ takes a +witness that $\myse{P}$ works with \emph{definitionally equal} terms, +and returns a witness of $\myse{P}$ working with \emph{propositionally + equal} terms. Invokations of $\myjeqq$ will vanish when the equality +proofs will reduce to invocations to reflexivity, at which point the +arguments must be definitionally equal, and thus the provided $\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmm}}{(\myapp{\myrefl}{\mytmm})}$ -can be returned. +can be returned. This means that $\myjeqq$ will not compute with +hypotetical proofs, which makes sense given that they might be false. While the $\myjeqq$ rule is slightly convoluted, ve can derive many more `friendly' rules from it, for example a more obvious `substitution' rule, that replaces equal for equal in predicates: \[ \begin{array}{l} -\myfun{subst} : \myfora{\myb{A}}{\mytyp}{\myfora{\myb{P}}{\myb{A} \myarr \mytyp}{\myfora{\myb{x}\ \myb{y}}{\myb{A}}{\myb{x} \mypeq{\myb{A}} \myb{y} \myarr \myapp{\myb{P}}{\myb{x}} \myarr \myapp{\myb{P}}{\myb{y}}}}} \\ +\myfun{subst} : \myfora{\myb{A}}{\mytyp}{\myfora{\myb{P}}{\myb{A} \myarr \mytyp}{\myfora{\myb{x}\ \myb{y}}{\myb{A}}{\mypeq \myappsp \myb{A} \myappsp \myb{x} \myappsp \myb{y} \myarr \myapp{\myb{P}}{\myb{x}} \myarr \myapp{\myb{P}}{\myb{y}}}}} \\ \myfun{subst}\myappsp \myb{A}\myappsp\myb{P}\myappsp\myb{x}\myappsp\myb{y}\myappsp\myb{q}\myappsp\myb{p} \mapsto \myjeq{(\myabs{\myb{x}\ \myb{y}\ \myb{q}}{\myapp{\myb{P}}{\myb{y}}})}{\myb{p}}{\myb{q}} \end{array} @@ -1353,10 +1431,12 @@ Similarly, all one inhabitants of $\myunit$ and all zero inhabitants of $\myempty$ can be considered equal. Quotation can be performed in a type-directed way, as we will witness in Section \ref{sec:kant-irr}. -To justify this process in our type system we will add a congruence law +\begin{mydef}[Congruence and $\eta$-laws] +To justify quotation in our type system we will add a congruence law for abstractions and a similar law for products, plus the fact that all elements of $\myunit$ or $\myempty$ are equal. - +\end{mydef} +\mynegder \mydesc{definitional equality:}{\myjud{\mytmm \mydefeq \mytmn}{\mytmsyn}}{ \begin{tabular}{cc} \AxiomC{$\myjudd{\myctx; \myb{y} : \mytya}{\myapp{\myse{f}}{\myb{x}} \mydefeq \myapp{\myse{g}}{\myb{x}}}{\mysub{\mytyb}{\myb{x}}{\myb{y}}}$} @@ -1389,6 +1469,7 @@ Another common but controversial addition to propositional equality is the $\myfun{K}$ axiom, which essentially states that all equality proofs are by reflexivity. +\begin{mydef}[$\myfun{K}$ axiom]\end{mydef} \mydesc{typing:}{\myjud{\mytmm \mydefeq \mytmn}{\mytmsyn}}{ \AxiomC{$ \begin{array}{@{}c} @@ -1426,7 +1507,7 @@ research.\footnote{More information about univalence can be found at \epigraph{\emph{Half of my time spent doing research involves thinking up clever schemes to avoid needing functional extensionality.}}{@larrytheliquid} -However, propositional equality as described is quite restricted when +Propositional equality as described is quite restricted when reasoning about equality beyond the term structure, which is what definitional equality gives us (extension notwithstanding). @@ -1460,9 +1541,9 @@ 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 +For the reasons given above, theories that offer a propositional equality similar to what we presented are called \emph{intensional}, as opposed -to \emph{extensional}. Most systems in wide use today (such as Agda, +to \emph{extensional}. Most systems widely used today (such as Agda, Coq, and Epigram) are of this kind. This is quite an annoyance that often makes reasoning awkward to execute. It @@ -1473,26 +1554,36 @@ on the behaviour on a term. \subsection{Equality reflection} One way to `solve' this problem is by identifying propositional equality with -definitional equality: +definitional equality. +\begin{mydef}[Equality reflection]\end{mydef} \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{ \AxiomC{$\myjud{\myse{q}}{\mytmm \mypeq{\mytya} \mytmn}$} \UnaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\mytya}$} \DisplayProof } -This rule takes the name of \emph{equality reflection}, and is a very -different rule from the ones we saw up to now: it links a typing judgement -internal to the type theory to a meta-theoretic judgement that the type -checker uses to work with terms. It is easy to see the dangerous consequences -that this causes: +The \emph{equality reflection} rule is a very different rule from the +ones we saw up to now: it links a typing judgement internal to the type +theory to a meta-theoretic judgement that the type checker uses to work +with terms. It is easy to see the dangerous consequences that this +causes: \begin{itemize} -\item The rule is syntax directed, and the type checker is presumably expected - to come up with equality proofs when needed. +\item The rule is not syntax directed, and the type checker is + presumably expected to come up with equality proofs when needed. \item More worryingly, type checking becomes undecidable also because computing under false assumptions becomes unsafe, since we derive any equality proof and then use equality reflection and the conversion rule to have terms of any type. + + For example, assuming that we are in a context that contains + \[ + \myb{A} : \mytyp; \myb{q} : \mypeq \myappsp \mytyp + \myappsp (\mytya \myarr \mytya) \myappsp \mytya + \] + we can write a looping term similar to the one we saw in Section + \ref{sec:untyped}: + % TODO dot this \end{itemize} Given these facts theories employing equality reflection, like NuPRL @@ -1524,9 +1615,11 @@ gain extensionality? % TODO finish % TODO add `extentional axioms' (Hoffman), setoid models (Thorsten) -\section{Observational equality} +\section{The observational approach} \label{sec:ott} +% TODO add \begin{mydef}s + A recent development by \citet{Altenkirch2007}, \emph{Observational Type Theory} (OTT), promises to keep the well behavedness of ITT while being able to gain many useful equality proofs,\footnote{It is suspected @@ -1534,7 +1627,7 @@ being able to gain many useful equality proofs,\footnote{It is suspected 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 +structurally that $\mytya$ and $\mytyb$ are equal; and providing a value-level equality based on similar principles. Here we give an exposition which follows closely the original paper. @@ -1552,6 +1645,19 @@ exposition which follows closely the original paper. $ } +\mynegder + +\mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{ + $ + \begin{array}{l@{}l@{\ }c@{\ }l} + \myITE{\mytrue &}{\mytya}{\mytyb} & \myred & \mytya \\ + \myITE{\myfalse &}{\mytya}{\mytyb} & \myred & \mytyb + \end{array} + $ +} + +\mynegder + \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{ \begin{tabular}{cc} \AxiomC{$\myjud{\myse{P}}{\myprop}$} @@ -1566,6 +1672,8 @@ exposition which follows closely the original paper. \end{tabular} } +\mynegder + \mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{ \begin{tabular}{ccc} \AxiomC{\phantom{$\myjud{\myse{P}}{\myprop}$}} @@ -1626,14 +1734,15 @@ indeed we can `inject' any $\myprop$ back in $\mytyp$ with $\myprdec{\myarg}$: \ 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. + criteria, $\mytop$ obviously fits the bill, since it us 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 + 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} @@ -1938,9 +2047,6 @@ $\myfun{coe}$ will not advance, since the types are not canonical. However they are definitionally equal, and thus we can safely remove the coerce and return $\myb{x}$ as it is. -This process of identifying every proof as equivalent and removing -$\myfun{coe}$rcions is known as \emph{quotation}. - \section{\mykant : the theory} \label{sec:kant-theory} @@ -1975,6 +2081,13 @@ The defining features of \mykant\ are: \item[Observational equality] As described in Section \ref{sec:ott} but extended to work with the type hierarchy and to admit equality between arbitrary data types. + +\item[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}. + \end{description} We will analyse the features one by one, along with motivations and @@ -2014,31 +2127,31 @@ and so are annotate terms. The type of applications is inferred too, propagating types down the applied term. Abstractions are checked. Finally, we have a rule to check the type of an inferrable term. -\mydesc{typing:}{\myctx \vdash \mytmsyn \Leftrightarrow \mytmsyn}{ - \begin{tabular}{ccc} +\mydesc{typing:}{\myctx \vdash \mytmsyn \Updownarrow \mytmsyn}{ + \begin{tabular}{cc} \AxiomC{$\myctx(x) = A$} \UnaryInfC{$\myinf{\myb{x}}{A}$} \DisplayProof & \AxiomC{$\myjudd{\myctx;\myb{x} : A}{\mytmt}{\mytyb}$} - \UnaryInfC{$\mychk{\myabs{x}{\mytmt}}{\mytyb}$} - \DisplayProof - & - \AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$} - \AxiomC{$\myjud{\mytmn}{\mytya}$} - \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mytyb}$} + \UnaryInfC{$\mychk{\myabs{x}{\mytmt}}{(\myb{x} {:} \mytya) \myarr \mytyb}$} \DisplayProof \end{tabular} \myderivspp - \begin{tabular}{cc} + \begin{tabular}{ccc} + \AxiomC{$\myinf{\mytmm}{\mytya \myarr \mytyb}$} + \AxiomC{$\mychk{\mytmn}{\mytya}$} + \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mytyb}$} + \DisplayProof + & \AxiomC{$\mychk{\mytmt}{\mytya}$} \UnaryInfC{$\myinf{\myann{\mytmt}{\mytya}}{\mytya}$} \DisplayProof & \AxiomC{$\myinf{\mytmt}{\mytya}$} - \UnaryInfC{$\mychk{\mytmt}{\mytya}$} + \UnaryInfC{$\myinf{\mytmt}{\mytya}$} \DisplayProof \end{tabular} } @@ -2132,7 +2245,7 @@ We can now give types to our terms. Although we include the usual conversion rule, we defer a detailed account of definitional equality to Section \ref{sec:kant-irr}. -\mydesc{typing:}{\myctx \vdash \mytmsyn \Leftrightarrow \mytmsyn}{ +\mydesc{typing:}{\myctx \vdash \mytmsyn \Updownarrow \mytmsyn}{ \begin{tabular}{cccc} \AxiomC{$\myse{name} : A \in \myctx$} \UnaryInfC{$\myinf{\myse{name}}{A}$} @@ -2151,9 +2264,26 @@ Section \ref{sec:kant-irr}. \BinaryInfC{$\mychk{\mytmt}{\mytyb}$} \DisplayProof \end{tabular} + \myderivspp - \begin{tabular}{ccc} + \begin{tabular}{cc} + + \AxiomC{\phantom{$\mychkk{\myctx; \myb{x}: \mytya}{\mytmt}{\mytyb}$}} + \UnaryInfC{$\myinf{\mytyp}{\mytyp}$} + \DisplayProof + & + \AxiomC{$\myinf{\mytya}{\mytyp}$} + \AxiomC{$\myinff{\myctx; \myb{x} : \mytya}{\mytyb}{\mytyp}$} + \BinaryInfC{$\myinf{(\myb{x} {:} \mytya) \myarr \mytyb}{\mytyp}$} + \DisplayProof + + \end{tabular} + + + \myderivspp + + \begin{tabular}{cc} \AxiomC{$\myinf{\mytmm}{\myfora{\myb{x}}{\mytya}{\mytyb}}$} \AxiomC{$\mychk{\mytmn}{\mytya}$} \BinaryInfC{$\myinf{\myapp{\mytmm}{\mytmn}}{\mysub{\mytyb}{\myb{x}}{\mytmn}}$} @@ -2165,6 +2295,7 @@ Section \ref{sec:kant-irr}. \UnaryInfC{$\mychk{\myabs{\myb{x}}{\mytmt}}{\myfora{\myb{x}}{\mytyb}{\mytyb}}$} \DisplayProof \end{tabular} + } \subsection{Elaboration} @@ -2173,7 +2304,7 @@ 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}, +by McBride's and McKinna's early work on Epigram \citep{McBride2004}, although with some differences. \subsubsection{Term vectors, telescopes, and assorted notation} @@ -2185,14 +2316,14 @@ 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 what we do for contexts. 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 +\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. @@ -2249,15 +2380,15 @@ 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[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. \end{description} -Elaborating defined variables consists of type checking body against the -given type, and updating the context to contain the new binding. +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: @@ -2285,8 +2416,8 @@ checking the type, and updating the context with a new typed variable: \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. +Elaborating user defined types is the real effort. First, we will +explain what we can define, with some examples. \begin{description} \item[Natural numbers] To define natural numbers, we create a data type @@ -2323,7 +2454,7 @@ data Nat = Zero | Suc Nat \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 + for example using $\mytyc{\mynat}.\mydc{suc}$ on its own will give a syntax error. This is necessary so that we can easily infer the type of polymorphic data constructors, as we will see later. @@ -2333,7 +2464,9 @@ data Nat = Zero | Suc Nat 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. + will omit the type constructor prefix for brevity, in this case + writing $\mydc{zero}$ instead of $\mynat.\mydc{suc}$ and $\mydc{suc}$ instead of + $\mynat.\mydc{suc}$. Along with user defined constructors, $\mykant$\ automatically generates an \emph{eliminator}, or \emph{destructor}, to compute with @@ -2360,9 +2493,9 @@ data Nat = Zero | Suc Nat 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 + mean to compute. In this specific case $\mynat.\myfun{elim}$ + returns the base case if the provided number is $\mydc{zero}$, and + recursively applies the inductive step if the number is a $\mydc{suc}$cessor: \[ \begin{array}{@{}l@{}l} @@ -2376,7 +2509,9 @@ elim :: Nat -> a -> (Nat -> a -> a) -> a elim Zero pz ps = pz elim (Suc n) pz ps = ps n (elim n pz ps) \end{Verbatim} - Which buys us the computational behaviour, but not the reasoning power. +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. \item[Binary trees] Now for a polymorphic data type: binary trees, since lists are too similar to natural numbers to be interesting. @@ -2445,6 +2580,10 @@ elim (Suc n) pz ps = ps n (elim n pz ps) $} \end{prooftree} As expected, the eliminator embodies structural induction on trees. + We have a base case for $\myb{P} \myappsp \mydc{leaf}$, and an + inductive step that given two subtrees and the predicate applied to + them we need to return the predicate applied to the tree formed by a + node with the two subtrees as children. \item[Empty type] We have presented types that have at least one constructors, but nothing prevents us from defining types with @@ -2522,9 +2661,12 @@ elim (Suc n) pz ps = ps n (elim n pz ps) } \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: + Note that in the $\mydc{cons}$ constructor we quantify over the first + argument, which will determine the type of the following + arguments---again something we cannot do in systems like Haskell. If + we want we can then employ this structure to write and prove correct + various sorting algorithms.\footnote{See this presentation by Conor + McBride: \url{https://personal.cis.strath.ac.uk/conor.mcbride/Pivotal.pdf}, and this blog post by the author: \url{http://mazzo.li/posts/AgdaSort.html}.} @@ -2712,13 +2854,13 @@ elim (Suc n) pz ps = ps n (elim n pz ps) \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 +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 +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. @@ -2844,7 +2986,7 @@ $\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 +consistent under 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. @@ -2968,7 +3110,7 @@ nest $\myand$ in the same way. \subsubsection{Some OTT examples} -Before presenting the direction that $\mykant$\ takes, let's consider +Before presenting the direction that $\mykant$\ takes, let us 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. @@ -2996,7 +3138,7 @@ equalities. \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$ + the type binders are explicit, while here $\mytyb_1$ and $\mytyb_2$ are functions returning types. We can do this thanks to the type hierarchy, and this hints at the fact that heterogeneous equality will have to allow $\mytyp$ `to the right of the colon', and in fact this @@ -3162,7 +3304,7 @@ as equal. } \mynegder - % TODO equality for decodings + \mydesc{equality reduction:}{\myctx \vdash \myprsyn \myred \myprsyn}{ \small \begin{tabular}{cc} @@ -3284,10 +3426,10 @@ as equal. \subsubsection{$\myprop$ and the hierarchy} -Where is $\myprop$ placed in the type hierarchy? The main indicator -is the decoding operator, since it converts into things that already -live in the hierarchy. For example, if we -have +We shall have, at earch universe level, not only a $\mytyp_l$ but also a +$\myprop_l$. Where will propositions placed in the type hierarchy? The +main indicator is the decoding operator, since it converts into things +that already live in the hierarchy. For example, if we have \[ \myprdec{\mynat \myarr \mybool \myeq \mynat \myarr \mybool} \myred \mytop \myand ((\myb{x}\, \myb{y} : \mynat) \myarr \mytop \myarr \mytop) @@ -3318,8 +3460,8 @@ equality since for example we have that \myred \myfora{\myb{x_1}}{\mytya_1}{\myfora{\myb{x_2}}{\mytya_2}{\cdots}} \] -where the proposition decodes into something of type $\mytyp_l$, where -$\mytya : \mytyp_l$ and $\mytyb : \mytyp_l$. We can resolve this +where the proposition decodes into something of at least type $\mytyp_l$, where +$\mytya_l : \mytyp_l$ and $\mytyb_l : \mytyp_l$. We can resolve this tension by making all equalities larger: \begin{prooftree} \AxiomC{$\myjud{\mytmm}{\mytya}$} @@ -3410,14 +3552,45 @@ needed terms. % TODO finish this \begin{figure}[t] - \mydesc{canonical quotation}{\myctx \vdash \mytmsyn \myquot \mytmsyn \mapsto \mytmsyn}{ - + \mydesc{canonical quotation:}{\mycanquot(\myctx, \mytmsyn : \mytmsyn) \mymetagoes \mytmsyn}{ + \small + $ + \begin{array}{@{}l} + \mycanquot(\myctx, \mytmt : \mytyc{D} \myappsp \vec{A}) \mymetaguard \mymeta{empty}(\myctx, \mytyc{D}) \mymetagoes \boxed{\mytmt} \\ + \mycanquot(\myctx, \mytmt : \mytyc{D} \myappsp \vec{A}) \mymetaguard \mymeta{record}(\myctx, \mytyc{D}) \mymetagoes \\ \myind{2} \mytyc{D}.\mydc{constr} \myappsp \cdots \myappsp \mycanquot(\myctx, \mytyc{D}.\myfun{f}_n : (\myctx(\mytyc{D}.\myfun{f}_n))(\vec{A};\mytmt)) \\ + \mycanquot(\myctx, \mytyc{D}.\mydc{c} \myappsp \vec{t} : \mytyc{D} \myappsp \vec{A}) \mymetagoes \cdots \\ + \mycanquot(\myctx, \myse{f} : \myfora{\myb{x}}{\mytya}{\mytyb}) \mymetagoes \myabs{\myb{x}}{\mycanquot(\myctx; \myb{x} : \mytya, \myapp{\myse{f}}{\myb{x}} : \mytyb)} \\ + \mycanquot(\myctx, \myse{p} : \myprdec{\myse{P}}) \mymetagoes \boxed{\myse{p}} + \\ + \mycanquot(\myctx, \mytmt : \mytya) \mymetagoes \mytmt'\text{, where}\ \mytmt' : \myarg = \myneuquot(\myctx, \mytmt) + \end{array} + $ } \mynegder - \mydesc{neutral quotation}{\myctx \vdash \mynquot \mytmsyn \mapsto \mytmsyn : \mytmsyn}{ - + \mydesc{neutral quotation:}{\myneuquot(\myctx, \mytmsyn) \mymetagoes \mytmsyn : \mytmsyn}{ + \small + $ + \begin{array}{@{}l@{}l} + \myneuquot(\myctx,\ \myb{x} &) \mymetagoes \myb{x} : \myctx(\myb{x}) \\ + \myneuquot(\myctx,\ \mytyp &) \mymetagoes \mytyp : \mytyp \\ + \myneuquot(\myctx,\ \myfora{\myb{x}}{\mytya}{\mytyb} & ) \mymetagoes + \myfora{\myb{x}}{\myneuquot(\myctx, \mytya)}{\myneuquot(\myctx; \myb{x} : \mytya, \mytyb)} : \mytyp \\ + \myneuquot(\myctx,\ \mytyc{D} \myappsp \vec{A} &) \mymetagoes \mytyc{D} \myappsp \cdots \mycanquot(\myctx, \mymeta{head}((\myctx(\mytyc{D}))(\mytya_1 \cdots \mytya_{n-1}))) : \mytyp \\ + \myneuquot(\myctx,\ \myprdec{\myjm{\mytmm}{\mytya}{\mytmn}{\mytyb}} &) \mymetagoes \myprdec{\myjm{\mycanquot(\myctx, \mytmm : \mytya)}{\mytya'}{\mycanquot(\myctx, \mytmn : \mytyb)}{\mytyb'}} : \mytyp \\ + \multicolumn{2}{@{}l}{\myind{2}\text{where}\ \mytya' : \myarg = \myneuquot(\myctx, \mytya)\text{, and}\ \mytyb' : \myarg = \myneuquot(\myctx, \mytyb)} \\ + \myneuquot(\myctx,\ \mytyc{D}.\myfun{f} \myappsp \mytmt &) \mymetaguard \mymeta{record}(\myctx, \mytyc{D}) \mymetagoes \\ + \multicolumn{2}{@{}l}{\myind{2} \mytyc{D}.\myfun{f} \myappsp \mytmt' : (\myctx(\mytyc{D}.\myfun{f}))(\vec{A};\mytmt)\text{, where}\ \mytmt' : \mytyc{D} \myappsp \vec{A} = \myneuquot(\myctx, \mytmt)} \\ + \myneuquot(\myctx,\ \mytyc{D}.\myfun{elim} \myappsp \mytmt \myappsp \myse{P} &) \mymetaguard \mymeta{empty}(\myctx, \mytyc{D}) \mymetagoes \mytyc{D}.\myfun{elim} \myappsp \boxed{\mytmt} \myappsp \myneuquot(\myctx, \myse{P} \myappsp \mytmt) \\ + \myneuquot(\myctx,\ \mytyc{D}.\myfun{elim} \myappsp \mytmm \myappsp \myse{P} \myappsp \vec{\mytmn} &) \mymetagoes \cdots \\ + \myneuquot(\myctx,\ \myapp{\myse{f}}{\mytmt} &) \mymetagoes \\ + \multicolumn{2}{@{}l}{\myind{2} \myapp{\myse{f'}}{\mycanquot(\myctx, \mytmt : \mytya)} : \mysub{\mytyb}{\myb{x}}{\mytmt}\text{, where}\ \myse{f'} : \myfora{\myb{x}}{\mytya}{\mytyb} = \myneuquot(\myctx, \myse{f})} \\ + \myneuquot(\myctx,\ \mycoee{\mytya}{\mytyb}{\myse{Q}}{\mytmt} &) \mymetaguard \myneuquot(\myctx, \mytya) \mydefeq_{\mybox} \myneuquot(\myctx, \mytyb) \mymetagoes \myneuquot(\myctx, \mytmt) \\ +\myneuquot(\myctx,\ \mycoee{\mytya}{\mytyb}{\myse{Q}}{\mytmt} &) \mymetagoes + \mycoee{\myneuquot(\myctx, \mytya)}{\myneuquot(\myctx, \mytyb)}{\boxed{\myse{Q}}}{\myneuquot(\myctx, \mytmt)} + \end{array} + $ } \caption{Quotation in \mykant.} \label{fig:kant-quot} @@ -3457,7 +3630,7 @@ repository at \url{http://sneezy.cs.nott.ac.uk/darcs/Pig09}.} In many ways \mykant\ is something in between the first and second version of Epigram. -The author learnt the hard way the implementations challenges for such a +The author learnt the hard way the implementation challenges for such a project, and while there is a solid and working base to work on, the implementation of observational equality is not currently complete. However, given the detailed plan in the previous section, doing so @@ -3492,18 +3665,27 @@ Type: Nat\end{verbatim} \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}: +The interaction with the user takes place in a loop living in and +updating a context of \mykant\ declarations. A REPL cycle starts with +the user inputing a \mykant\ declaration or another REPL command, which +then goes through various stages that can end up in a context update, or +in failures of various kind. The process is described diagrammatically +in figure \ref{fig:kant-process}: \begin{description} + \item[Parse] In this phase the text input gets converted to a sugared - version of the core language. + version of the core language. For example, we accept multiple + arguments in arrow types and abstractions, and we represent variables + with names, while as we will see in Section \ref{sec:term-repr} the + final term types uses a \emph{nameless} representation. \item[Desugar] The sugared declaration is converted to a core term. + Most notably we go from names to nameless. + +\item[ConDestr] Short for `Constructors/Destructors', converts + applications of data destructors and constructors to a special form, + to perform bidirectional type checking. \item[Reference] Occurrences of $\mytyp$ get decorated by a unique reference, which is necessary to implement the type hierarchy check. @@ -3514,11 +3696,14 @@ diagrammatically in figure \ref{fig:kant-process}: tandem with \textbf{Type checking}, which in turns needs to \textbf{Evaluate} terms. -\item[Distill] and report the result. `Distilling' refers to the process of - converting a core term back to a sugared version that the user can - visualise. This can be necessary both to display errors including terms or - to display result of evaluations or type checking that the user has - requested. +\item[Distill] and report the result. `Distilling' refers to the + process of converting a core term back to a sugared version that the + user can visualise. This can be necessary both to display errors + including terms or to display result of evaluations or type checking + that the user has requested. Among the other things in this stage we + go from nameless back to names by recycling the names that the user + used originally, as to fabricate a term which is as close as possible + to what it originated from. \item[Pretty print] Format the terms in a nice way, and display the result to the user. @@ -3543,17 +3728,20 @@ diagrammatically in figure \ref{fig:kant-process}: \node [cloud] (user) {User}; \node [block, below left=1cm and 0.1cm of user] (parse) {Parse}; \node [block, below=of parse] (desugar) {Desugar}; - \node [block, below=of desugar] (reference) {Reference}; + \node [block, below=of desugar] (condestr) {ConDestr}; + \node [block, below=of condestr] (reference) {Reference}; \node [block, below=of reference] (elaborate) {Elaborate}; \node [block, left=of elaborate] (tycheck) {Typecheck}; \node [block, left=of tycheck] (evaluate) {Evaluate}; \node [decision, right=of elaborate] (error) {Error?}; - \node [block, right=of parse] (distill) {Distill}; - \node [block, right=of desugar] (update) {Update context}; + \node [block, right=of parse] (pretty) {Pretty print}; + \node [block, below=of pretty] (distill) {Distill}; + \node [block, below=of distill] (update) {Update context}; \path [line] (user) -- (parse); \path [line] (parse) -- (desugar); - \path [line] (desugar) -- (reference); + \path [line] (desugar) -- (condestr); + \path [line] (condestr) -- (reference); \path [line] (reference) -- (elaborate); \path [line] (elaborate) edge[bend right] (tycheck); \path [line] (tycheck) edge[bend right] (elaborate); @@ -3561,7 +3749,8 @@ diagrammatically in figure \ref{fig:kant-process}: \path [line] (error) edge[out=0,in=0] node [near start] {yes} (distill); \path [line] (error) -- node [near start] {no} (update); \path [line] (update) -- (distill); - \path [line] (distill) -- (user); + \path [line] (pretty) -- (user); + \path [line] (distill) -- (pretty); \path [line] (tycheck) edge[bend right] (evaluate); \path [line] (evaluate) edge[bend right] (tycheck); \end{tikzpicture} @@ -3579,7 +3768,7 @@ theorem prover. \subsubsection{Naming and substituting} -Perhaps surprisingly, one of the most fundamental challenges in +Perhaps surprisingly, one of the most difficult challenges in implementing a theory of the kind presented is choosing a good data type for terms, and specifically handling substitutions in a sane way. @@ -3605,7 +3794,12 @@ variables, and thus substituting: the variable bound by the innermost binding structure, $1$ the second-innermost, and so on. For instance with simple abstractions we might have - \[\mymacol{red}{\lambda}\, (\mymacol{blue}{\lambda}\, \mymacol{blue}{0}\, (\mymacol{AgdaInductiveConstructor}{\lambda\, 0}))\, (\mymacol{AgdaFunction}{\lambda}\, \mymacol{red}{1}\, \mymacol{AgdaFunction}{0}) : ((\mytya \myarr \mytya) \myarr \mytyb) \myarr \mytyb \] + \[ + \begin{array}{@{}l} + \mymacol{red}{\lambda}\, (\mymacol{blue}{\lambda}\, \mymacol{blue}{0}\, (\mymacol{AgdaInductiveConstructor}{\lambda\, 0}))\, (\mymacol{AgdaFunction}{\lambda}\, \mymacol{red}{1}\, \mymacol{AgdaFunction}{0}) : ((\mytya \myarr \mytya) \myarr \mytyb) \myarr \mytyb\text{, which corresponds to} \\ + \myabs{\myb{f}}{(\myabs{\myb{g}}{\myapp{\myb{g}}{(\myabs{\myb{x}}{\myb{x}})}}) \myappsp (\myabs{\myb{x}}{\myapp{\myb{f}}{\myb{x}}})} : ((\mytya \myarr \mytya) \myarr \mytyb) \myarr \mytyb + \end{array} + \] While this technique is obviously terrible in terms of human usability,\footnote{With some people going as far as defining it akin @@ -3614,9 +3808,9 @@ variables, and thus substituting: simple cases. Moreover, $\alpha$ renaming ceases to be an issue, and term comparison is purely syntactical. - Nonetheless, more complex, more complex constructs such as pattern - matching put some strain on the indices and many systems end up using - explicit names anyway (Agda, Coq, \dots). + Nonetheless, more complex, constructs such as pattern matching put + some strain on the indices and many systems end up using explicit + names anyway (Agda, Coq, \dots). \end{description} @@ -3630,13 +3824,13 @@ advantages but also pitfalls in the previously relatively unknown territory of dependent types---\texttt{bound} being created mostly to handle more simply typed systems. -\texttt{bound} builds on two core ideas. The first is the suggestion by -\cite{Bird1999} consists of parametrising the term type over the type of -the variables, and `nest' the type each time we enter a scope. If we -wanted to define a term for the untyped $\lambda$-calculus, we might -have +\texttt{bound} builds on the work of \cite{Bird1999}, who suggest to +parametrising the term type over the type of the variables, and `nest' +the type each time we enter a scope. If we wanted to define a term for +the untyped $\lambda$-calculus, we might have \begin{Verbatim} -data Void +-- A type with no members. +data Empty data Var v = Bound | Free v @@ -3645,15 +3839,21 @@ data Tm v | App (Tm v) (Tm v) -- Term application | Lam (Tm (Var v)) -- Abstraction \end{Verbatim} -Closed terms would be of type \texttt{Tm Void}, so that there would be +Closed terms would be of type \texttt{Tm Empty}, so that there would be no occurrences of \texttt{V}. However, inside an abstraction, we can have \texttt{V Bound}, representing the bound variable, and inside a second abstraction we can have \texttt{V Bound} or \texttt{V (Free -Bound)}. Thus the term $\myabs{\myb{x}}{\myabs{\myb{y}}{\myb{x}}}$ could be represented as +Bound)}. Thus the term +\[\myabs{\myb{x}}{\myabs{\myb{y}}{\myb{x}}}\] +can be represented as \begin{Verbatim} -Lam (Lam (Free Bound)) +-- The top level term is of type `Tm Empty'. +-- The inner term `Lam (Free Bound)' is of type `Tm (Var Empty)'. +-- The second inner term `V (Free Bound)' is of type `Tm (Var (Var +-- Empty))'. +Lam (Lam (V (Free Bound))) \end{Verbatim} -This allows us to reflect at the type level the `nestedness' of a type, +This allows us to reflect the of a type `nestedness' at the type level, and since we usually work with functions polymorphic on the parameter \texttt{v} it's very hard to make mistakes by putting terms of the wrong nestedness where they don't belong. @@ -3678,7 +3878,7 @@ instance Monad Tm where -- `Lam' is the tricky case: we modify the function to work with bound -- variables, so that if it encounters `Bound' it leaves it untouched - -- (since the mapping referred to the outer scope); if it encounters a + -- (since the mapping refers to the outer scope); if it encounters a -- free variable it asks `f' for the term and then updates all the -- variables to make them refer to the outer scope they were meant to -- be in. @@ -3703,7 +3903,9 @@ inst t s = do v <- s The beauty of this technique is that in a few simple function we have defined all the core operations in a general and `obviously correct' way, with the extra confidence of having the type checker looking our -back. +back. For what concerns term equality, we can just ask the Haskell +compiler to derive the instance for the \verb|Eq| type class and since +we are nameless that will be enough (modulo fancy quotation). Moreover, if we take the top level term type to be \verb|Tm String|, we get for free a representation of terms with top-level, definitions; @@ -3730,7 +3932,8 @@ variable---say \verb|m v|---a \verb|Monad| instance means being able to only substitute variables for values of type \verb|m v|. This is a considerable inconvenience. Consider for instance the case of telescopes, which are a central tool to deal with contexts and other -constructs: +constructs. In Haskell we can give them a faithful representation +with a data type along the lines of \begin{Verbatim} data Tele m v = End (m v) | Bind (m v) (Tele (Var v)) type TeleTm = Tele Tm @@ -3749,59 +3952,14 @@ who analysed some of the alternatives---most notably the work by simplicity of the model above. That said, our term type is still reasonably brief, as shown in full in -Figure \ref{fig:term}. The fact that propositions cannot be factored -out in another data type is a consequence of the problems described -above. However the real pain is during elaboration, where we are forced -to treat everything as a type while we would much rather have +Appendix \ref{app:termrep}. The fact that propositions cannot be +factored out in another data type is an instance of the problem +described above. However the real pain is during elaboration, where we +are forced to treat everything as a type while we would much rather have telescopes. Future work would include writing a library that marries a nice interface similar to the one of \verb|bound| with a more flexible interface. -\begin{figure}[t] -{\small\begin{verbatim}-- A top-level name. -type Id = String --- A data/type constructor name. -type ConId = String - --- A term, parametrised over the variable (`v') and over the reference --- type used in the type hierarchy (`r'). -data Tm r v - = V v -- Variable. - | Ty r -- Type, with a hierarchy reference. - | Lam (TmScope r v) -- Abstraction. - | Arr (Tm r v) (TmScope r v) -- Dependent function. - | App (Tm r v) (Tm r v) -- Application. - | Ann (Tm r v) (Tm r v) -- Annotated term. - -- Data constructor, the first ConId is the type constructor and - -- the second is the data constructor. - | Con ADTRec ConId ConId [Tm r v] - -- Data destrutor, again first ConId being the type constructor - -- and the second the name of the eliminator. - | Destr ADTRec ConId Id (Tm r v) - -- A type hole. - | Hole HoleId [Tm r v] - -- Decoding of propositions. - | Dec (Tm r v) - - -- Propositions. - | Prop r -- The type of proofs, with hierarchy reference. - | Top - | Bot - | And (Tm r v) (Tm r v) - | Forall (Tm r v) (TmScope r v) - -- Heterogeneous equality. - | Eq (Tm r v) (Tm r v) (Tm r v) (Tm r v) - --- Either a data type, or a record. -data ADTRec = ADT | Rec - --- Either a coercion, or coherence. -data Coeh = Coe | Coh\end{verbatim} -} - \caption{Data type for terms in \mykant.} - \label{fig:term} -\end{figure} - We also make use of a `forgetful' data type (as provided by \verb|bound|) to store user-provided variables names along with the `nameless' representation, so that the names will not be considered when @@ -3809,16 +3967,26 @@ compared terms, but will be available when distilling so that we can recover variable names that are as close as possible to what the user originally used. +\subsubsection{Evaluation} + +Another source of contention related to term representation is dealing +with evaluation. Here \mykant\ does not make bold moves, and simply +employs substitution. Before +Moreover, when elaborating user defined types, +all + \subsubsection{Context} +Given the parmetrised type, + % TODO finish -\subsection{Type hierarchy} +\subsection{Turning constraints into graphs} \label{sec:hier-impl} -As a breath of air amongst the type gas, we will explain how to +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}. As mentioned, we have to verify a the +\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: @@ -3836,39 +4004,48 @@ equality constraint ($x = y$), which can be reduced to two constraints $x \le y$ and $y \le x$. Given this specification, we have implemented a standalone Haskell -module---that we plan to release as a library---to efficiently store and -check the consistency of constraints. Its interface is shown in Figure -\ref{fig:constraint}. The problem unpredictably reduces to a graph -algorithm. If we +module---that we plan to release as a standalone library---to +efficiently store and check the consistency of constraints. The problem +predictably reduces to a graph algorithm, and for this reason we also +implement a library for labelled graphs, since the existing Haskell +graph libraries fell short in different areas.\footnote{We tried the +\texttt{Data.Graph} module in +\url{http://hackage.haskell.org/package/containers}, and the much more +featureful \texttt{fgl} library +\url{http://hackage.haskell.org/package/fgl}.}. The interfaces for +these modules are shown in Appendix \ref{app:constraint}. The graph +library is implemented as a modification of the code described by +\cite{King1995}. + +We represent the set by building a graph where vertices are variables, +and edges are constraints between them. The edges are labelled with the +constraint type ($<$ or $\le$). As we add constraints, $\le$ +constraints are replaced by $<$ constraints, so that if we started with +an empty set and added +\[ + x \le y,\ y < z,\ z \le k,\ k \le j,\ x < y,\ j \le y +\] +it would generate the graph shown in Figure \ref{fig:graph-one}. \begin{figure}[t] -{\small\begin{verbatim}module Data.Constraint where - --- | Data type holding the set of constraints, parametrised over the --- type of the variables. -data Constrs a - --- | A representation of the constraints that we can add. -data Constr a = a :<=: a | a :<: a | a :==: a --- | An empty set of constraints. -empty :: Ord a => Constrs a +\end{figure} --- | Adds one constraint to the set, returns the new set of constraints --- if consistent. -addConstr :: Ord a => Constr a -> Constrs a -> Maybe (Constrs a)\end{verbatim} -} +\subsection{Type holes} +\label{sec:type-holes} - \caption{Interface for the module handling the constraints.} - \label{fig:constraint} -\end{figure} +Type holes are, in the author's opinion, one of the `killer' features of +interactive theorem provers, and one that is begging to be exported to +the word of mainstream programming. The idea is that when we are +developing a proof or a program we can insert a hole to have the +software tell us the type expected at that point. Furthermore, we can +ask for the type of variables in context, to better understand our +sorroundings. +In \mykant\ -\subsection{Type holes} +\subsection{Web prompt} -When building up programs interactively, it is useful to leave parts -unfinished while exploring the current context. This is what type holes -are for. \section{Evaluation} @@ -3919,11 +4096,12 @@ language as defined in \citep{Haskell2010}, which I will typeset in Haskell, plenty of good introductions are available \citep{LYAH,ProgInHask}. When presenting grammars, I will use a word in $\mysynel{math}$ font -(e.g. $\mytmsyn$ or $\mytysyn$) to indicate indicate nonterminals. Additionally, -I will use quite flexibly a $\mysynel{math}$ font to indicate a syntactic -element. More specifically, terms are usually indicated by lowercase letters -(often $\mytmt$, $\mytmm$, or $\mytmn$); and types by an uppercase letter (often -$\mytya$, $\mytyb$, or $\mytycc$). +(e.g. $\mytmsyn$ or $\mytysyn$) to indicate indicate +nonterminals. Additionally, I will use quite flexibly a $\mysynel{math}$ +font to indicate a syntactic element in derivations or meta-operations. +More specifically, terms are usually indicated by lowercase letters +(often $\mytmt$, $\mytmm$, or $\mytmn$); and types by an uppercase +letter (often $\mytya$, $\mytyb$, or $\mytycc$). When presenting type derivations, I will often abbreviate and present multiple conclusions, each on a separate line: @@ -3955,7 +4133,7 @@ In explicitly typed systems, I will also omit type annotations when they are obvious, e.g. by not annotating the type of parameters of abstractions or of dependent pairs. -I will also introduce multiple arguments in one go in arrow types: +I will introduce multiple arguments in one go in arrow types: \[ (\myb{x}\, \myb{y} {:} \mytya) \myarr \cdots = (\myb{x} {:} \mytya) \myarr (\myb{y} {:} \mytya) \myarr \cdots \] @@ -3963,6 +4141,11 @@ and in abstractions: \[ \myabs{\myb{x}\myappsp\myb{y}}{\cdots} = \myabs{\myb{x}}{\myabs{\myb{y}}{\cdots}} \] +I will also omit arrows to abbreviate types: +\[ +(\myb{x} {:} \mytya)(\myb{y} {:} \mytyb) \myarr \cdots = +(\myb{x} {:} \mytya) \myarr (\myb{y} {:} \mytyb) \myarr \cdots +\] \section{Code} @@ -4146,7 +4329,7 @@ implemented that yet. \verbatiminput{examples.ka} } -\subsection{\mykant's hierachy} +\subsection{\mykant' hierachy} \label{sec:hurkens} This rendition of the Hurken's paradox does not type check with the @@ -4158,6 +4341,76 @@ Agda version, available at \verbatiminput{hurkens.ka} } +\subsection{Term representation} +\label{app:termrep} + +Data type for terms in \mykant. + +{\small\begin{verbatim}-- A top-level name. +type Id = String +-- A data/type constructor name. +type ConId = String + +-- A term, parametrised over the variable (`v') and over the reference +-- type used in the type hierarchy (`r'). +data Tm r v + = V v -- Variable. + | Ty r -- Type, with a hierarchy reference. + | Lam (TmScope r v) -- Abstraction. + | Arr (Tm r v) (TmScope r v) -- Dependent function. + | App (Tm r v) (Tm r v) -- Application. + | Ann (Tm r v) (Tm r v) -- Annotated term. + -- Data constructor, the first ConId is the type constructor and + -- the second is the data constructor. + | Con ADTRec ConId ConId [Tm r v] + -- Data destrutor, again first ConId being the type constructor + -- and the second the name of the eliminator. + | Destr ADTRec ConId Id (Tm r v) + -- A type hole. + | Hole HoleId [Tm r v] + -- Decoding of propositions. + | Dec (Tm r v) + + -- Propositions. + | Prop r -- The type of proofs, with hierarchy reference. + | Top + | Bot + | And (Tm r v) (Tm r v) + | Forall (Tm r v) (TmScope r v) + -- Heterogeneous equality. + | Eq (Tm r v) (Tm r v) (Tm r v) (Tm r v) + +-- Either a data type, or a record. +data ADTRec = ADT | Rec + +-- Either a coercion, or coherence. +data Coeh = Coe | Coh\end{verbatim} +} + +\subsection{Graph and constraints modules} +\label{app:constraint} + +The modules are respectively named \texttt{Data.LGraph} (short for +`labelled graph'), and \texttt{Data.Constraint}. The type class +constraints on the type parameters are not shown for clarity, unless +they are meaningful to the function. In practice we use the +\texttt{Hashable} type class on the vertex to implement the graph +efficiently with hash maps. + +\subsubsection{\texttt{Data.LGraph}} + +{\small +\verbatiminput{graph.hs} +} + +\subsubsection{\texttt{Data.Constraint}} + +{\small +\verbatiminput{constraint.hs} +} + + + \bibliographystyle{authordate1} \bibliography{thesis} -- 2.30.2