From: Francesco Mazzoli Date: Tue, 18 Jun 2013 04:54:26 +0000 (+0100) Subject: the war is over johnny X-Git-Url: https://git.enpas.org/?p=bitonic-mengthesis.git;a=commitdiff_plain;h=7e1d2c79545c573617ccedf458ba11bda1cc3eb8 the war is over johnny --- diff --git a/thesis.lagda b/thesis.lagda index 55f12bf..77fdd95 100644 --- a/thesis.lagda +++ b/thesis.lagda @@ -2,34 +2,34 @@ %% THIS LATEX HURTS YOUR EYES. DO NOT READ. -% TODO side conditions - \documentclass[11pt, fleqn, twoside]{article} \usepackage{etex} \usepackage[usenames,dvipsnames]{xcolor} -% \usepackage[sc,slantedGreek]{mathpazo} -\usepackage[sc,osf,slantedGreek]{mathpazo} +\usepackage[sc,slantedGreek]{mathpazo} % \linespread{1.05} % \usepackage{times} -\oddsidemargin .50in -\evensidemargin -.25in -% \oddsidemargin 0in -% \evensidemargin 0in -\textheight 9.5in -\textwidth 6.2in -\topmargin -7mm -%% \parindent 10pt +% \oddsidemargin .50in +% \evensidemargin -.25in +% % \oddsidemargin 0in +% % \evensidemargin 0in +% \textheight 9.5in +% \textwidth 6.2in +% \topmargin -9mm +% %% \parindent 10pt -\headheight 0pt -\headsep 0pt +% \headheight 0pt +% \headsep 0pt -\usepackage{amsthm} +\usepackage[hmargin=2cm,vmargin=2.5cm]{geometry} +\geometry{textwidth=390pt} +\geometry{bindingoffset=1.5cm} -% \usepackage{microtype} +\raggedbottom +\usepackage{amsthm} %% Bibtex \usepackage{natbib} @@ -139,7 +139,7 @@ \parbox{\textwidth}{ {\mysmall \vspace{0.2cm} - \hfill \textup{\textbf{#1}} $#2$ + \hfill \textup{\phantom{ygp}\textbf{#1}} $#2$ \framebox[\textwidth]{ \parbox{\textwidth}{ \vspace{0.1cm} @@ -392,8 +392,8 @@ hypertexnames=true, pdfhighlight=/O, urlcolor=webbrown, linkcolor=black, citecol \renewcommand{\abstractname}{Acknowledgements} \begin{abstract} I would like to thank Steffen van Bakel, my supervisor, who was brave - enough to believe in my project and who provided much advice and - support. + enough to believe in my project and who provided support and + invaluable advice. I would also like to thank the Haskell and Agda community on \texttt{IRC}, which guided me through the strange world of types; and @@ -403,7 +403,7 @@ hypertexnames=true, pdfhighlight=/O, urlcolor=webbrown, linkcolor=black, citecol 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, + Finally, most of the work stems from the research of Conor McBride, who answered many of my doubts through these months. I also owe him the colours. \end{abstract} @@ -457,7 +457,7 @@ formulated in the 70s and then adjusted through a series of revisions, it has endured as the core of many practical systems widely in use today, and it is the most prominent instance of the proposition-as-types and proofs-as-programs paradigm. One of the most debated subjects in -this field has been regarding what notion of \emph{equality} should be +this field has been regarding what notion of equality should be exposed to the user. The tension when studying equality in type theory springs from the fact @@ -465,12 +465,11 @@ that there is a divide between what the user can prove equal \emph{inside} the theory---what is \emph{propositionally} equal---and what the theorem prover identifies as equal in its meta-theory---what is \emph{definitionally} equal. If we want our system to be well behaved -(mostly if we want type checking to be decidable) we must keep the two +(mostly if we want to keep type checking 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. +based on their syntactical structure, and not based on their behaviour. This thesis is concerned with exploring a new approach in this area, \emph{observational} equality. Promising to provide a more adequate @@ -563,14 +562,14 @@ adopting the proofs-as-programs mantra. The defining features of greater flexibility. We have two kinds of user defined types: inductive data types, formed by various data constructors whose type signatures can contain recursive occurrences of the type being - defined; and records, where we have just one data constructor and a - projection to extract each each field in said constructor. + defined; and records, where we have just one data constructor and + projections to extract each each field in said constructor. \item[Consistency] Our system is meant to be consistent with respects to the logic it embodies. For this reason, we restrict recursion to \emph{structural} recursion on the defined inductive types, through the use of operators (destructors) computing on each type. Following - the types-as-proofs interpretation, each destructor expresses an + the types-as-propositions interpretation, each destructor expresses an induction principle on the data type it operates on. To achieve the consistency of these operations we make sure that our recursive data types are \emph{strictly positive}. @@ -579,8 +578,8 @@ adopting the proofs-as-programs mantra. The defining features of \emph{bidirectional} type inference system in the style of \cite{Pierce2000}. This cuts down the type annotations by a considerable amount in an elegant way and at a very low cost. - Bidirectional type checking is usually employed in core calculi, in - \mykant\ we extend the concept to user defined data types. + Bidirectional type checking is usually employed in core calculi, but + in \mykant\ we extend the concept to user defined data types. \item[Type hierarchy] In set theory we have to take treat powerset-like objects with care, if we want to avoid paradoxes. However, the @@ -654,11 +653,11 @@ $\beta$-reduction and substitution for the $\lambda$-calculus. \myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{\myb{x}}{\mytmn}\text{ \textbf{where}} \\ \myind{2} \begin{array}{l@{\ }c@{\ }l} - \mysub{\myb{x}}{\myb{x}}{\mytmn} & = & \mytmn \\ - \mysub{\myb{y}}{\myb{x}}{\mytmn} & = & y\text{ \textbf{with} } \myb{x} \neq y \\ - \mysub{(\myapp{\mytmt}{\mytmm})}{\myb{x}}{\mytmn} & = & (\myapp{\mysub{\mytmt}{\myb{x}}{\mytmn}}{\mysub{\mytmm}{\myb{x}}{\mytmn}}) \\ - \mysub{(\myabs{\myb{x}}{\mytmm})}{\myb{x}}{\mytmn} & = & \myabs{\myb{x}}{\mytmm} \\ - \mysub{(\myabs{\myb{y}}{\mytmm})}{\myb{x}}{\mytmn} & = & \myabs{\myb{z}}{\mysub{\mysub{\mytmm}{\myb{y}}{\myb{z}}}{\myb{x}}{\mytmn}} \\ + \mysub{\myb{y}}{\myb{x}}{\mytmn} \mymetaguard \myb{x} = \myb{y} & \mymetagoes & \mytmn \\ + \mysub{\myb{y}}{\myb{x}}{\mytmn} & \mymetagoes & \myb{y} \\ + \mysub{(\myapp{\mytmt}{\mytmm})}{\myb{x}}{\mytmn} & \mymetagoes & (\myapp{\mysub{\mytmt}{\myb{x}}{\mytmn}}{\mysub{\mytmm}{\myb{x}}{\mytmn}}) \\ + \mysub{(\myabs{\myb{x}}{\mytmm})}{\myb{x}}{\mytmn} & \mymetagoes & \myabs{\myb{x}}{\mytmm} \\ + \mysub{(\myabs{\myb{y}}{\mytmm})}{\myb{x}}{\mytmn} & \mymetagoes & \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} @@ -673,7 +672,7 @@ 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}}$} + (\myapp{\omega}{\omega}) \myred (\myapp{\omega}{\omega}) \myred \cdots \text{, \textbf{where} $\omega = \myabs{x}{\myapp{x}{x}}$} \] \begin{mydef}[redex] A \emph{redex} is a term that can be reduced. @@ -701,8 +700,8 @@ systematically. Common evaluation strategies include \emph{call by 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 +is still not a $\lambda$. In both these strategies we never +reduce under an abstraction. For this reason a weaker form of normalisation is used, where all abstractions are said to be in \emph{weak head normal form} even if their body is not. @@ -946,9 +945,10 @@ and $\mysnd$ to $\wedge$ elimination. The trivial type $\myunit$ corresponds to the logical $\top$ (true), and dually $\myempty$ corresponds to the logical $\bot$ (false). $\myunit$ has one introduction rule ($\mytt$), and thus one inhabitant; and no -eliminators. $\myempty$ has no introduction rules, and thus no -inhabitants; and one eliminator ($\myabsurd{ }$), corresponding to the -logical \emph{ex falso quodlibet}. +eliminators---we cannot gain any information from a witness of the +single member of $\myunit$. $\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. @@ -1049,7 +1049,7 @@ inductive data. \subsection{Extending the STLC} \cite{Barendregt1991} succinctly expressed geometrically how we can add -expressivity to the STLC: +expressively to the STLC: $$ \xymatrix@!0@=1.5cm{ & \lambda\omega \ar@{-}[rr]\ar@{-}'[d][dd] @@ -1078,19 +1078,36 @@ Here $\lambda{\to}$, in the bottom left, is the STLC. From there can move along 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. + Haskell and SML are based on this discipline. In Haskell the above + example would be + \begin{Verbatim} +id :: a -> a +id x = x + \end{Verbatim} + Where \texttt{a} implicitly quantifies over a type, and will be + instantiated automatically thanks to the inference. \item[Types depending on types (towards $\lambda{\underline{\omega}}$)] We have type operators. For example we could define a function that given types $R$ and $\mytya$ forms the type that represents a value of type $\mytya$ in continuation passing style: - \[\displaystyle(\myabss{\myb{A} \myar \myb{R}}{\mytyp}{(\myb{A} + \[\displaystyle(\myabss{\myb{R} \myarr \myb{A}}{\mytyp}{(\myb{A} \myarr \myb{R}) \myarr \myb{R}}) : \mytyp \myarr \mytyp \myarr \mytyp \] + In Haskell we can define type operator of sorts, although we must + pair them with data constructors, to keep inference manageable: + \begin{Verbatim} +newtype Cont r a = Cont ((a -> r) -> r) + \end{Verbatim} + Where the `type' (kind in Haskell parlance) of \texttt{Cont} will be + \texttt{* -> * -> *}, with \texttt{*} signifying the type of types in + Haskell. \item[Types depending on terms (towards $\lambda{P}$)] Also known as `dependent types', give great expressive power. For example, we can have values of whose type depend on a boolean: \[\displaystyle(\myabss{\myb{x}}{\mybool}{\myite{\myb{x}}{\mynat}{\myrat}}) : \mybool - \myarr \mytyp\] + \myarr \mytyp\] We cannot give an Haskell example that expresses this + concept since Haskell does not support dependent types---it would be a + very different language if it did. \end{description} All the systems preserve the properties that make the STLC well behaved. The @@ -1127,10 +1144,10 @@ others. \label{sec:core-tt} The calculus I present follows the exposition in \cite{Thompson1991}, -and is quite close to the original formulation of -\citep{Martin-Lof1984}. Agda and \mykant\ renditions of the presented -theory and all the examples is reproduced in Appendix -\ref{app:itt-code}. +and is quite close to the original formulation of \cite{Martin-Lof1984}. +Agda and \mykant\ renditions of the presented theory and all the +examples (even the ones presented only as type signatures) are +reproduced in Appendix \ref{app:itt-code}. \begin{mydef}[Intuitionistic Type Theory (ITT)] The syntax and reduction rules are shown in Figure \ref{fig:core-tt-syn}. The typing rules are presented piece by piece in the following sections. @@ -1393,7 +1410,8 @@ correspondence with logic alive, dependent functions are much like universal quantifiers ($\forall$) in logic. For example, assuming that we have lists and natural numbers in our -language, using dependent functions we can write functions of types +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 \\ @@ -1412,7 +1430,7 @@ 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 +Finally, 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. @@ -1453,7 +1471,9 @@ The first element will be a number, and the second evidence that the number is even. This highlights the fact that we are working in a constructive logic: if we have an existence proof, we can always ask for a witness. This means, for instance, that $\neg \forall \neg$ is not -equivalent to $\exists$. +equivalent to $\exists$. Additionally, we need to specify the type of +the second element (ranging over the first element) explicitly when +using $\mypair{\myarg}{\myarg}$. Another perhaps more `dependent' application of products, paired with $\mybool$, is to offer choice between different types. For example we @@ -1503,11 +1523,11 @@ let us represent inductive data in a general way. We can form `nodes' of the shape \[\mytmt \mynode{\myb{x}}{\mytyb} \myse{f} : \myw{\myb{x}}{\mytya}{\mytyb}\] where $\mytmt$ is of type $\mytya$ and is the data present in the node, and $\myse{f}$ specifies a `child' of -the node for each member of $\mysub{\mytyb}{\myb{x}}{\mytmt}$.. The +the node for each member of $\mysub{\mytyb}{\myb{x}}{\mytmt}$. The $\myfun{rec}\ \myfun{with}$ acts as an induction principle on $\mytyc{W}$, given a predicate and a function dealing with the inductive -case---we will gain more intuition about inductive data in ITT in -Section \ref{sec:user-type}. +case---we will gain more intuition about inductive data in Section +\ref{sec:user-type}. For example, if we want to form natural numbers, we can take \[ @@ -1544,19 +1564,19 @@ And with a bit of effort, we can recover addition: \end{array} \] Note how we explicitly have to type the branches to make them match - with the definition of $\mynat$. This gives a taste of the - clumsiness of $\mytyc{W}$-types but not the whole story: well-orders - are inadequate not only because they are verbose, but also because the + with the definition of $\mynat$. This gives a taste of the clumsiness + of $\mytyc{W}$-types but not the whole story. Well-orders are + inadequate not only because they are verbose, but also because they face deeper problems due to the weakness of the notion of equality - present in most type theory (which we will present in the next - section) \citep{dybjer1997representing}. The `better' equality we - will present in Section \ref{sec:ott} helps but does not fully resolve + present in most type theories, which we will present in the next + section \citep{dybjer1997representing}. The `better' equality we will + present in Section \ref{sec:ott} helps but does not fully resolve these issues.\footnote{See \url{http://www.e-pig.org/epilogue/?p=324}, which concludes with `W-types are a powerful conceptual tool, but they’re no basis for an implementation of recursive data types in decidable type theories.'} For this reasons \mytyc{W}-types have remained nothing more than a reasoning tool, and practical systems - implement more expressive ways to represent data. + must implement more expressive ways to represent data. \section{The struggle for equality} \label{sec:equality} @@ -1594,11 +1614,11 @@ formalised in Agda in Appendix \ref{app:agda-itt}. } \end{minipage} \begin{minipage}{0.5\textwidth} -\mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{ +\mydesc{\phantom{y}reduction:}{\mytmsyn \myred \mytmsyn}{ $ \myjeq{\myse{P}}{(\myapp{\myrefl}{\mytmm})}{\mytmn} \myred \mytmn $ - \vspace{1.1cm} + \vspace{1.05cm} } \end{minipage} \mynegder @@ -1626,6 +1646,7 @@ formalised in Agda in Appendix \ref{app:agda-itt}. \DisplayProof \end{tabular} } +\ \\ To express equality between two terms inside ITT, the obvious way to do so is to have equality to be a type. Here we present what has survived @@ -1636,8 +1657,8 @@ Our type former is $\mypeq$, which given a type relates equal terms of that type. $\mypeq$ has one introduction rule, $\myrefl$, which introduces an equality relation between definitionally equal terms. -Finally, we have one eliminator for $\mypeq$ (also known as `\myfun{J} -axiom' in the literature), $\myjeqq$. +Finally, we have one eliminator for $\mypeq$ , $\myjeqq$ (also known as +`\myfun{J} axiom' in the literature). $\myjeq{\myse{P}}{\myse{q}}{\myse{p}}$ takes \begin{itemize} \item $\myse{P}$, a predicate working with two terms of a certain type (say @@ -1648,13 +1669,14 @@ $\myjeq{\myse{P}}{\myse{q}}{\myse{p}}$ takes twice, plus the trivial proof by reflexivity showing that $\myse{m}$ is equal to itself. \end{itemize} -Given these ingredients, $\myjeqq$ returns a member of $\myse{P}$ applied -to $\mytmm$, $\mytmn$, and $\myse{q}$. In other words $\myjeqq$ takes a -witness that $\myse{P}$ works with \emph{definitionally equal} terms, -and returns a witness of $\myse{P}$ working with \emph{propositionally - equal} terms. Invocations of $\myjeqq$ will vanish when the equality -proofs will reduce to invocations to reflexivity, at which point the -arguments must be definitionally equal, and thus the provided +Given these ingredients, $\myjeqq$ returns a member of $\myse{P}$ +applied to $\mytmm$, $\mytmn$, and $\myse{q}$. In other words $\myjeqq$ +takes a witness that $\myse{P}$ works with \emph{definitionally equal} +terms, and returns a witness of $\myse{P}$ working with +\emph{propositionally equal} terms. Given its reduction rules, +invocations of $\myjeqq$ will vanish when the equality proofs will +reduce to invocations to reflexivity, at which point the arguments must +be definitionally equal, and thus the provided $\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmm}}{(\myapp{\myrefl}{\mytmm})}$ can be returned. This means that $\myjeqq$ will not compute with hypothetical proofs, which makes sense given that they might be false. @@ -1669,8 +1691,9 @@ replaces equal for equal in predicates: \myjeq{(\myabs{\myb{x}\ \myb{y}\ \myb{q}}{\myapp{\myb{P}}{\myb{y}}})}{\myb{p}}{\myb{q}} \end{array} \] -Once we have $\myfun{subst}$, we can easily prove more familiar laws regarding -equality, such as symmetry, transitivity, congruence laws, etc. +Once we have $\myfun{subst}$, we can easily prove more familiar laws +regarding equality, such as symmetry, transitivity, congruence laws, +etc.\footnote{For definitions of these functions, refer to Appendix \ref{app:itt-code}.} \subsection{Common extensions} @@ -1681,7 +1704,7 @@ automatically extend propositional equality, given how $\myrefl$ works. \subsubsection{$\eta$-expansion} \label{sec:eta-expand} -A simple extension to our definitional equality is $\eta$-expansion. +A simple extension to our definitional equality is achieved by $\eta$-expansion. Given an abstract variable $\myb{f} : \mytya \myarr \mytyb$ the aim is to have that $\myb{f} \mydefeq \myabss{\myb{x}}{\mytya}{\myapp{\myb{f}}{\myb{x}}}$. We can achieve @@ -1693,7 +1716,7 @@ back into terms, which will `smooth out' differences like the one above \citep{Abel2007}. The same concept applies to $\myprod$, where we expand each inhabitant -by reconstructing it by getting its projections, so that $\myb{x} +reconstructing it by getting its projections, so that $\myb{x} \mydefeq \mypair{\myfst \myappsp \myb{x}}{\mysnd \myappsp \myb{x}}$. Similarly, all one inhabitants of $\myunit$ and all zero inhabitants of $\myempty$ can be considered equal. Quotation can be performed in a @@ -1753,7 +1776,7 @@ are by reflexivity. \cite{Hofmann1994} showed that $\myfun{K}$ is not derivable from $\myjeqq$, and \cite{McBride2004} showed that it is needed to implement -`dependent pattern matching', as first proposed by \cite{Coquand1992}. +`dependent pattern matching', as first proposed by \cite{Coquand1992}.\footnote{See Section \ref{sec:future-work} for more on dependent pattern matching.} Thus, $\myfun{K}$ is derivable in the systems that implement dependent pattern matching, such as Epigram and Agda; but for example not in Coq. @@ -1775,6 +1798,11 @@ Propositional equality as described is quite restricted when reasoning about equality beyond the term structure, which is what definitional equality gives us (extensions notwithstanding). +\begin{mydef}[Extensional equality] +Given two functions $\myse{f}$ and $\myse{g}$ of type $\mytya \myarr \mytyb$, they are are said to be \emph{extensionally equal} if +\[ (\myb{x} {:} \mytya) \myarr \mypeq \myappsp \mytyb \myappsp (\myse{f} \myappsp \myb{x}) \myappsp (\myse{g} \myappsp \myb{x}) \] +\end{mydef} + The problem is best exemplified by \emph{function extensionality}. In mathematics, we would expect to be able to treat functions that give equal output for equal input as equal. When reasoning in a mechanised @@ -1782,8 +1810,7 @@ framework we ought to be able to do the same: in the end, without considering the operational behaviour, all functions equal extensionally are going to be replaceable with one another. -However this is not the case, or in other words with the tools we have we have -no term of type +However this is not the case, or in other words with the tools we have there is no closed term of type \[ \myfun{ext} : \myfora{\myb{A}\ \myb{B}}{\mytyp}{\myfora{\myb{f}\ \myb{g}}{ \myb{A} \myarr \myb{B}}{ @@ -1802,18 +1829,18 @@ prove that \myfora{\myb{x}}{\mynat}{\mypeq \myappsp \mynat \myappsp (0 \mathrel{\myfun{$+$}} \myb{x}) \myappsp (\myb{x} \mathrel{\myfun{$+$}} 0)} \] By induction on $\mynat$ applied to $\myb{x}$. However, the two -functions are not definitionally equal, and thus we won't be able to get +functions are not definitionally equal, and thus we will not be able to get rid of the quantification. For the reasons given above, theories that offer a propositional equality similar to what we presented are called \emph{intensional}, as opposed to \emph{extensional}. Most systems widely used today (such as Agda, -Coq, and Epigram) are of this kind. +Coq, and Epigram) are of the former kind. This is quite an annoyance that often makes reasoning awkward or impossible to execute. For example, we might want to represent terms of some language in Agda and give their denotation by embedding them in -Agda---if we had $\lambda$-terms, functions will become Agda functions, +Agda---if we had $\lambda$-terms, functions will be Agda functions, application will be Agda's function application, and so on. Then we would like to perform optimisation passes on the terms, and verify that they are sound by proving that the denotation of the optimised version @@ -1874,7 +1901,6 @@ We can then derive \RightLabel{$\myrefl$} \UnaryInfC{$\myjud{\myapp{\myrefl}{\myb{f}}}{\mypeq \myappsp (\myb{A} \myarr \myb{B}) \myappsp \myb{f} \myappsp \myb{g}}$} \end{prooftree} - For this reason, theories employing equality reflection are often grouped under the name of \emph{Extensional Type Theory} (ETT). Now, the question is: do we need to give up well-behavedness of our theory to @@ -1972,7 +1998,7 @@ ad-hoc conditional for types, where the reduction rule is the obvious one. However, we have an addition: a universe of \emph{propositions}, -$\myprop$. $\myprop$ isolates a fragment of types at large, and +$\myprop$.\footnote{Note that we do not need syntax for the type of props, $\myprop$, since the user cannot abstract over them. In fact, we do not not need syntax for $\mytyp$ either, for the same reason.} $\myprop$ isolates a fragment of types at large, and indeed we can `inject' any $\myprop$ back in $\mytyp$ with $\myprdec{\myarg}$. \begin{mydef}[Proposition decoding]\ \end{mydef} \mydesc{proposition decoding:}{\myprdec{\mytmsyn} \myred \mytmsyn}{ @@ -1996,7 +2022,7 @@ indeed we can `inject' any $\myprop$ back in $\mytyp$ with $\myprdec{\myarg}$. Propositions are what we call the types of \emph{proofs}, or types whose inhabitants contain no `data', much like $\myunit$. The goal when isolating \mytyc{Prop} is twofold: erasing all top-level - propositions when compiling; and to identify all equivalent + propositions when compiling; and identifying all equivalent propositions as the same, as we will see later. Why did we choose what we have in $\myprop$? Given the above @@ -2008,12 +2034,12 @@ indeed we can `inject' any $\myprop$ back in $\mytyp$ with $\myprdec{\myarg}$. decoding will be a constant function for propositional content. The only threat is $\mybot$, by which we can fabricate anything we want: however if we are consistent there will be no closed term of type - $\mybot$ at, which is what we care about regarding proof erasure and + $\mybot$ at, which is enough regarding proof erasure and term equality. As an example of types that are \emph{not} propositional, consider $\mydc{Bool}$eans, which are the quintessential `relevant' data, since - they are often use to decide the execution path of a program through + they are often used to decide the execution path of a program through $\myfun{if}\myarg\myfun{then}\myarg\myfun{else}\myarg$ constructs. \subsection{Equality proofs} @@ -2135,16 +2161,20 @@ closed terms will reduce to a canonical term. The plan is to decompose type-level equalities between canonical types into decodable propositions containing equalities regarding the -subterms, and to use coerce recursively on the subterms using the -generated equalities. This interplay between the canonicity of equated -types, type equalities, and \myfun{coe} ensures that invocations of -$\myfun{coe}$ will vanish when we have evidence of the structural -equality of the types we are transporting terms across. If the type is -neutral, the equality will not reduce and thus $\myfun{coe}$ will not -reduce either. If we come across an equality between different -canonical types, then we reduce the equality to bottom, making sure that -no such proof can exist, and providing an `escape hatch' in -$\myfun{coe}$. +subterms. So if are equating two product types, the equality will +reduce to two subequalities regarding the first and second type. Then, +we can \myfun{coe}rce to transport values between equal types. +Following the subequalities, \myfun{coe} will procede recursively on the +subterms. + +This interplay between the canonicity of equated types, type +equalities, and \myfun{coe}, ensures that invocations of $\myfun{coe}$ +will vanish when we have evidence of the structural equality of the +types we are transporting terms across. If the type is neutral, the +equality will not reduce and thus $\myfun{coe}$ will not reduce either. +If we come across an equality between different canonical types, then we +reduce the equality to bottom, making sure that no such proof can exist, +and providing an `escape hatch' in $\myfun{coe}$. \begin{figure}[t] @@ -2310,8 +2340,11 @@ propositional data, such as $\myempty$ and $\myunit$, we automatically return the trivial type, since if a type has zero one members, all members will be equal. When matching on data-bearing types, such as $\mybool$, we check that such data matches, and return bottom otherwise. -When matching on records and functions, we rebuild the records and -expand the function to achieve $\eta$-expansion. +When matching on records and functions, we rebuild the records to +achieve $\eta$-expansion, and relate functions if they are extensionally +equal---exactly what we wanted. The case for \mytyc{W} is omitted but +unsurprising, it checks that equal data in the nodes will bring equal +children. \subsection{Proof irrelevance and stuck coercions} \label{sec:ott-quot} @@ -2357,6 +2390,13 @@ Section \ref{sec:contributions}, here we present them one by one. The exception is type holes, which we do not describe holes rigorously, but provide more information about them in Section \ref{sec:type-holes}. +Note that in this section we will present \mykant\ terms in a fancy +\LaTeX\ dress too keep up with the presentation, but every term, with its +syntax reduced to the concrete syntax, is a valid \mykant\ term accepted +by \mykant\ the software, and not only \mykant\ the theory. Appendix +\ref{app:kant-examples} displays most of the terms in this section in +their concrete syntax. + \subsection{Bidirectional type checking} We start by describing bidirectional type checking since it calls for @@ -2596,15 +2636,17 @@ although with some differences. \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$. + represented by $\myemptyctx$, and a new element is added with + $\myarg;\myarg$, 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. +We denote term vectors with the usual arrow notation, +e.g. $vec{\mytmt}$, $\myvec{\mytmt};\mytmm$, etc. We often 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 such +that $1 \le i \le n$. \begin{mydef}[Telescope] A \emph{telescope} is a series of typed bindings. The empty telescope @@ -2641,10 +2683,10 @@ We make use of various operations to manipulate telescopes: \myapp{\myfun{even}}{42})$. \end{itemize} -Additionally, when presenting syntax elaboration, I'll use $\mytmsyn^n$ -to indicate a term vector composed of $n$ elements, or -$\mytmsyn^{\mytele}$ for one composed by as many elements as the -telescope. +Additionally, when presenting syntax elaboration, We use $\mytmsyn^n$ to +indicate a term vector composed of $n$ elements. When clear from the +context, we use term vectors to signify their length, +e.g. $\mytmsyn^{\mytele}$, or $1 \le i \le \mytele$. \subsubsection{Declarations syntax} @@ -2669,14 +2711,17 @@ In \mykant\ we have four kind of declarations: \item[Defined value] A variable, together with a type and a body. \item[Abstract variable] An abstract variable, with a type but no body. \item[Inductive data] A \emph{data type}, with a \emph{type constructor} - and various \emph{data constructors}, quite similar to what we find in - Haskell. A primitive \emph{eliminator} (or \emph{destructor}, or - \emph{recursor}) will be used to compute with each data type. + (denoted in blue, capitalised, sans serif: $\mytyc{D}$) various + \emph{data constructors} (denoted in red, lowercase, sans serif: + $\mydc{c}$), quite similar to what we find in Haskell. A primitive + \emph{eliminator} (or \emph{destructor}, or \emph{recursor}; denoted + by green, lowercase, roman: \myfun{elim}) will be used to compute with + each data type. \item[Record] A \emph{record}, which like data types consists of a type constructor but only one data constructor. The user can also define various \emph{fields}, with no recursive occurrences of the type. The functions extracting the fields' values from an instance of a record - are called \emph{projections}. + are called \emph{projections} (denoted in the same way as destructors). \end{description} Elaborating defined variables consists of type checking the body against @@ -2755,11 +2800,11 @@ data Nat = Zero | Suc Nat Moreover, each data constructor is prefixed by the type constructor name, since we need to retrieve the type constructor of a data constructor when type checking. This measure aids in the presentation - of various features but it is not needed in the implementation, where + of the theory but it is not needed in the implementation, where we can have a dictionary to look up the type constructor corresponding to each data constructor. When using data constructors in examples I will omit the type constructor prefix for brevity, in this case - writing $\mydc{zero}$ instead of $\mynat.\mydc{suc}$ and $\mydc{suc}$ instead of + writing $\mydc{zero}$ instead of $\mynat.\mydc{zero}$ and $\mydc{suc}$ instead of $\mynat.\mydc{suc}$. Along with user defined constructors, $\mykant$\ automatically @@ -2827,9 +2872,10 @@ $\mynat$---the type system is far too weak. \end{array} \] The problem with this approach is that creating terms is incredibly - verbose and dull, since we would need to specify the type parameters - each time. For example if we wished to create a $\mytree \myappsp - \mynat$ with two nodes and three leaves, we would write + verbose and dull, since we would need to specify the type parameter of + $\mytyc{Tree}$ each time. For example if we wished to create a + $\mytree \myappsp \mynat$ with two nodes and three leaves, we would + write \[ \mydc{node} \myappsp \mynat \myappsp (\mydc{node} \myappsp \mynat \myappsp (\mydc{leaf} \myappsp \mynat) \myappsp (\myapp{\mydc{suc}}{\mydc{zero}}) \myappsp (\mydc{leaf} \myappsp \mynat)) \myappsp \mydc{zero} \myappsp (\mydc{leaf} \myappsp \mynat) \] @@ -2903,8 +2949,8 @@ $\mynat$---the type system is far too weak. new to the \{Haskell, SML, OCaml, functional\} programmer. However dependent types let us express much more than that. A useful example is the type of ordered lists. There are many ways to define such a - thing, but we will define our type to store the bounds of the list, - making sure that $\mydc{cons}$ing respects that. + thing, but we will define ours 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'. @@ -2948,12 +2994,13 @@ $\mynat$---the type system is far too weak. }) \end{array} \] - Finally, we can defined a type of ordered lists. The type is - parametrised over two values representing the lower and upper bounds - of the elements, as opposed to the type parameters that we are used - to. Then, an empty list will have to have evidence that the bounds - are ordered, and each time we add an element we require the list to - have a matching lower bound: + Finally, we can define a type of ordered lists. The type is + parametrised over two \emph{values} representing the lower and upper + bounds of the elements, as opposed to the \emph{type} parameters + that we are used to in Haskell or similar languages. An empty + list will have to have evidence that the bounds are ordered, and + each time we add an element we require the list to have a matching + lower bound: \[ \begin{array}{@{}l} \myadt{\mytyc{OList}}{\myappsp (\myb{low}\ \myb{upp} {:} \mytyc{Lift})}{\\ \myind{2}}{ @@ -3014,8 +3061,9 @@ $\mynat$---the type system is far too weak. \end{description} \begin{figure}[p] + \vspace{-.5cm} \mydesc{syntax}{ }{ - \footnotesize + \small $ \begin{array}{l} \mynamesyn ::= \cdots \mysynsep \mytyc{D} \mysynsep \mytyc{D}.\mydc{c} \mysynsep \mytyc{D}.\myfun{f} @@ -3026,7 +3074,7 @@ $\mynat$---the type system is far too weak. \mynegder \mydesc{syntax elaboration:}{\mydeclsyn \myelabf \mytmsyn ::= \cdots}{ - \footnotesize + \small $ \begin{array}{r@{\ }l} & \myadt{\mytyc{D}}{\mytele}{}{\cdots\ |\ \mydc{c}_n : \mytele_n } \\ @@ -3043,7 +3091,7 @@ $\mynat$---the type system is far too weak. \mynegder \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{ - \footnotesize + \small \AxiomC{$ \begin{array}{c} @@ -3086,7 +3134,7 @@ $\mynat$---the type system is far too weak. \mynegder \mydesc{reduction elaboration:}{\mydeclsyn \myelabf \myctx \vdash \mytmsyn \myred \mytmsyn}{ - \footnotesize + \small $\myadt{\mytyc{D}}{\mytele}{}{ \cdots \ |\ \mydc{c}_n : \mytele_n } \ \ \myelabf$ \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$} \AxiomC{$\mytyc{D}.\mydc{c}_i : \mytele;\mytele_i \myarr \myapp{\mytyc{D}}{\mytelee} \in \myctx$} @@ -3106,7 +3154,7 @@ $\mynat$---the type system is far too weak. \mynegder \mydesc{syntax elaboration:}{\myelab{\mydeclsyn}{\mytmsyn ::= \cdots}}{ - \footnotesize + \small $ \begin{array}{r@{\ }c@{\ }l} \myctx & \myelabt & \myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \\ @@ -3122,7 +3170,7 @@ $\mynat$---the type system is far too weak. \mynegder \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{ - \footnotesize + \small \AxiomC{$ \begin{array}{c} \myinf{\mytele \myarr \mytyp}{\mytyp}\hspace{0.8cm} @@ -3144,7 +3192,7 @@ $\mynat$---the type system is far too weak. \mynegder \mydesc{reduction elaboration:}{\mydeclsyn \myelabf \myctx \vdash \mytmsyn \myred \mytmsyn}{ - \footnotesize + \small $\myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \ \ \myelabf$ \AxiomC{$\mytyc{D} \in \myctx$} \UnaryInfC{$\myctx \vdash \myapp{\mytyc{D}.\myfun{f}_i}{(\mytyc{D}.\mydc{constr} \myappsp \vec{t})} \myred t_i$} @@ -3177,9 +3225,9 @@ achieve that we employing a syntactic check to make sure that this is the case---in fact the check is stricter than necessary for simplicity, given that we allow recursive occurrences only at the top level of data constructor arguments. For example a definition of the $\mytyc{W}$ type -is accepted in Agda but rejected in \mykant. - -Note that the +is accepted in Agda but rejected in \mykant. This is to make the +eliminator generation simpler, and in practice it is seldom an +impediment. Without these precautions, we can easily derive any type with no recursion: @@ -3205,8 +3253,8 @@ destructors, we store their types in full in the context, and then instantiate when due. \end{mydef} \mynegder -\mydesc{typing:}{\myctx \vdash \mytmsyn \Updownarrow \mytmsyn}{ - \AxiomC{$ +\mydesc{typing:}{\myctx + \vdash \mytmsyn \Updownarrow \mytmsyn}{ \AxiomC{$ \begin{array}{c} \mytyc{D} : \mytele \myarr \mytyp \in \myctx \hspace{1cm} \mytyc{D}.\mydc{c} : \mytele \mycc \mytele' \myarr @@ -3230,6 +3278,10 @@ instantiate when due. \myse{F})(\vec{A};\mytmt)}$} \DisplayProof } +Note that for 0-ary type constructors, like $\mynat$, we do not need to +check canonical terms: we can automatically infer that $\mydc{zero}$ and +$\mydc{suc}\myappsp n$ are of type $\mynat$. \mykant\ implements this measure, even +if it is not shown in the typing rule for simplicity. \subsubsection{Why user defined types? Why eliminators?} @@ -3260,7 +3312,7 @@ regarding the handling of data types: top of a larger set of combinators of those provided by \mykant. We can go ever further down this road and elaborate the declarations - for data types themselves to primitive types, so that our `core' + for data types themselves to a small set of primitives, so that our `core' language will be very small and manageable \citep{dagand2012elaborating, chapman2010gentle}. \end{description} @@ -3333,7 +3385,6 @@ types too. for user defined types, withe the type living in the least upper bound of the levels where the types contained data live. \end{mydef} - For example we might define our disjunction to be \[ \myarg\myfun{$\vee$}\myarg : \mytyp_{100} \myarr \mytyp_{100} \myarr \mytyp_{100} @@ -3364,15 +3415,16 @@ check, generating new references when needed. For example, when type checking the type $\mytyp\, r_1$, where $r_1$ denotes the unique reference assigned to that term, we will generate a -new fresh reference $\mytyp\, r_2$, and add the constraint $r_1 < r_2$ -to the set. When type checking $\myctx \vdash +new fresh reference and return the type $\mytyp\, r_2$, adding the +constraint $r_1 < r_2$ to the set. When type checking $\myctx \vdash \myfora{\myb{x}}{\mytya}{\mytyb}$, if $\myctx \vdash \mytya : \mytyp\, r_1$ and $\myctx; \myb{x} : \mytyb \vdash \mytyb : \mytyp\,r_2$; we will generate new reference $r$ and add $r_1 \le r$ and $r_2 \le r$ to the set. If at any point the constraint set becomes inconsistent, type checking -fails. Moreover, when comparing two $\mytyp$ terms we equate their +fails. Moreover, when comparing two $\mytyp$ terms---during the process +of deciding definitional equality for two terms---we equate their respective references with two $\le$ constraints. Implementation details are given in Section \ref{sec:hier-impl}. @@ -3384,7 +3436,7 @@ expressed: \myarg\myfun{$\vee$}\myarg : (l_1\, l_2 : \mytyc{Level}) \myarr \mytyp_{l_1} \myarr \mytyp_{l_2} \myarr \mytyp_{l_1 \mylub l_2} \] Inference algorithms to automatically derive this kind of relationship -are currently subject of research. We chose less flexible but more +are currently subject of research. We choose a less flexible but more concise way, since it is easier to implement and better understood. \subsection{Observational equality, \mykant\ style} @@ -3397,19 +3449,17 @@ is that we let the user define inductive types and records. Reconciling propositions for OTT and a hierarchy had already been investigated by Conor McBride,\footnote{See \url{http://www.e-pig.org/epilogue/index.html?p=1098.html}.} and we -follow his broad design plan, although with some innovation. Most of -the work, as an extension of elaboration, is to handle reduction rules -and coercions for data types---both type constructors and data -constructors. +follow some of his suggestions, with some innovation. Most of the dirty +work, as an extension of elaboration, is to handle reduction rules and +coercions for data types---both type constructors and data constructors. \subsubsection{The \mykant\ prelude, and $\myprop$ositions} Before defining $\myprop$, we define some basic types inside $\mykant$, as the target for the $\myprop$ decoder. - \begin{mydef}[\mykant' propositional prelude]\ \end{mydef} \[ -\begin{array}{l} +\begin{array}{@{}l} \myadt{\mytyc{Empty}}{}{ }{ } \\ \myfun{absurd} : (\myb{A} {:} \mytyp) \myarr \mytyc{Empty} \myarr \myb{A} \mapsto \\ \myind{2} \myabs{\myb{A\ \myb{bot}}}{\mytyc{Empty}.\myfun{elim} \myappsp \myb{bot} \myappsp (\myabs{\_}{\myb{A}})} \\ @@ -3514,7 +3564,7 @@ equalities. }} \end{array} \] - Then we can simply take + Then we can simply have \[ \begin{array}{@{}l} \mysigma \myappsp \mytya_1 \myappsp \mytyb_1 \myeq \mysigma \myappsp \mytya_2 \myappsp \mytyb_2 \myred \\ \myind{2} \mytya_1 \myeq \mytya_2 \myand \myjm{\mytyb_1}{\mytya_1 \myarr \mytyp}{\mytyb_2}{\mytya_2 \myarr \mytyp} @@ -3581,9 +3631,9 @@ 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 +rules for value equality work 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. +the original definition with explicit binders, in a natural manner. \begin{mydef}[Propositions, coercions, coherence, equalities and equality reduction for \mykant] See Figure \ref{fig:kant-eq-red}. @@ -3600,7 +3650,9 @@ still distinguish equalities relating types for hierarchical purposes. We exploit record to perform $\eta$-expansion. Moreover, given the nested $\myand$s, values of data types with zero constructors (such as $\myempty$) and records with zero destructors (such as -$\myunit$) will be automatically always identified as equal. +$\myunit$) will be automatically always identified as equal. As in the +original OTT, and for the same reasons, we can take $\myfun{coh}$ as +axiomatic. \begin{figure}[p] @@ -3887,7 +3939,7 @@ that already live in the hierarchy. For example, if we have \mytop \myand ((\myb{x}\, \myb{y} : \mynat) \myarr \mytop \myarr \mytop) \] we will better make sure that the `to be decoded' is at level compatible -(read: larger) with its reduction. In the example above, we'll have +(read: larger) with its reduction. In the example above, we will 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 @@ -3963,9 +4015,9 @@ would not hold. Consider for instance which reduces to \[\myjm{\mynat}{\mytyp_0}{\mybool}{\mytyp_0} : \myprop_0 \] We need members of $\myprop_0$ to be members of $\myprop_1$ too, which -will be the case with cumulativity. This is not the most elegant of -systems, but it buys us a cheap type level equality without having to -replicate functionality with a dedicated construct. +will be the case with cumulativity. This 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} @@ -3981,7 +4033,8 @@ We want to: \item As a consequence of the previous point, identify all records with no projections as equal, since they will have only one element. -\item Identify all members of types with no elements as equal. +\item Identify all members of types with no constructors (and thus no + elements) as equal. \item Identify all equivalent proofs as equal---with `equivalent proof' we mean those proving the same propositions. @@ -3992,20 +4045,27 @@ Towards these goals and following the intuition between bidirectional type checking we define two mutually recursive functions, one quoting canonical terms against their types (since we need the type to type check canonical terms), one quoting neutral terms while recovering their -types. The full procedure for quotation is shown in Figure -\ref{fig:kant-quot}. We $\boxed{\text{box}}$ the neutral proofs and +types. +\begin{mydef}[Quotation for \mykant] +The full procedure for quotation is shown in Figure +\ref{fig:kant-quot}. +\end{mydef} +We $\boxed{\text{box}}$ the neutral proofs and neutral members of empty types, following the notation in \cite{Altenkirch2007}, and we make use of $\mydefeq_{\mybox}$ which compares terms syntactically up to $\alpha$-renaming, but also up to equivalent proofs: we consider all boxed content as equal. Our quotation will work on normalised terms, so that all defined values -will have been replaced. Moreover, we match on data type eliminators and -all their arguments, so that $\mynat.\myfun{elim} \myappsp \mytmm +will have been replaced. Moreover, we match on data type eliminators +and all their arguments, so that $\mynat.\myfun{elim} \myappsp \mytmm \myappsp \myse{P} \myappsp \vec{\mytmn}$ will stand for $\mynat.\myfun{elim}$ applied to the scrutinised $\mynat$, the predicate, and the two cases. This measure can be easily implemented by checking the head of applications and `consuming' the needed terms. +Thus, we gain proof irrelevance, and not only for a more useful +definitional equality, but also for example to eliminate all +propositional content when compiling. \begin{figure}[t] \mydesc{canonical quotation:}{\mycanquot(\myctx, \mytmsyn : \mytmsyn) \mymetagoes \mytmsyn}{ @@ -4013,7 +4073,8 @@ checking the head of applications and `consuming' the needed terms. $ \begin{array}{@{}l@{}l} \mycanquot(\myctx,\ \mytmt : \mytyc{D} \myappsp \vec{A} &) \mymetaguard \mymeta{empty}(\myctx, \mytyc{D}) \mymetagoes \boxed{\mytmt} \\ - \mycanquot(\myctx,\ \mytmt : \mytyc{D} \myappsp \vec{A} &) \mymetaguard \mymeta{record}(\myctx, \mytyc{D}) \mymetagoes \mytyc{D}.\mydc{constr} \myappsp \cdots \myappsp \mycanquot(\myctx, \mytyc{D}.\myfun{f}_n : (\myctx(\mytyc{D}.\myfun{f}_n))(\vec{A};\mytmt)) \\ + \mycanquot(\myctx,\ \mytmt : \mytyc{D} \myappsp \vec{A} &) \mymetaguard \mymeta{record}(\myctx, \mytyc{D}) \mymetagoes + \mytyc{D}.\mydc{constr} \myappsp \cdots \myappsp \mycanquot(\myctx, \mytyc{D}.\myfun{f}_n : (\myctx(\mytyc{D}.\myfun{f}_n))(\vec{A};\mytmt)) \\ \mycanquot(\myctx,\ \mytyc{D}.\mydc{c} \myappsp \vec{t} : \mytyc{D} \myappsp \vec{A} &) \mymetagoes \cdots \\ \mycanquot(\myctx,\ \myse{f} : \myfora{\myb{x}}{\mytya}{\mytyb} &) \mymetagoes \myabs{\myb{x}}{\mycanquot(\myctx; \myb{x} : \mytya, \myapp{\myse{f}}{\myb{x}} : \mytyb)} \\ \mycanquot(\myctx,\ \myse{p} : \myprdec{\myse{P}} &) \mymetagoes \boxed{\myse{p}} @@ -4034,7 +4095,8 @@ checking the head of applications and `consuming' the needed terms. \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 \\ + \myneuquot(\myctx,\ \myprdec{\myjm{\mytmm}{\mytya}{\mytmn}{\mytyb}} &) \mymetagoes \\ + \multicolumn{2}{l}{\myind{2}\myprdec{\myjm{\mycanquot(\myctx, \mytmm : \mytya)}{\mytya'}{\mycanquot(\myctx, \mytmn : \mytyb)}{\mytyb'}} : \mytyp} \\ \multicolumn{2}{@{}l}{\myind{2}\text{\textbf{where}}\ \mytya' : \myarg = \myneuquot(\myctx, \mytya)} \\ \multicolumn{2}{@{}l}{\myind{2}\phantom{\text{\textbf{where}}}\ \mytyb' : \myarg = \myneuquot(\myctx, \mytyb)} \\ \myneuquot(\myctx,\ \mytyc{D}.\myfun{f} \myappsp \mytmt &) \mymetaguard \mymeta{record}(\myctx, \mytyc{D}) \mymetagoes \mytyc{D}.\myfun{f} \myappsp \mytmt' : (\myctx(\mytyc{D}.\myfun{f}))(\vec{A};\mytmt) \\ @@ -4066,7 +4128,7 @@ automatically, and in fact in some sense we already do during equality reduction and quotation. However, this has the considerable disadvantage that we can never identify abstracted variables\footnote{And in general neutral terms, although we currently - don't have neutral propositions apart from equalities on neutral + do not have neutral propositions apart from equalities on neutral terms.} of type $\mytyp$ as $\myprop$, thus forbidding the user to talk about $\myprop$ explicitly. @@ -4086,15 +4148,14 @@ The codebase consists of around 2500 lines of Haskell,\footnote{The full source code is available under the GPL3 license at \url{https://github.com/bitonic/kant}. `Kant' was a previous incarnation of the software, and the name remained.} as reported by -the \texttt{cloc} utility. The high level design is inspired by the -work on various incarnations of Epigram, and specifically by the first -version as described by \cite{McBride2004}. +the \texttt{cloc} utility. -The author learnt the hard way the implementation challenges for such a -project, and ran out of time while implementing observational equality. -While the constructs and typing rules are present, the machinery to make -it happen (equality reduction, coercions, quotation, etc.) is not -present yet. +We implement the type theory as described in Section +\ref{sec:kant-theory}. The author learnt the hard way the +implementation challenges for such a project, and ran out of time while +implementing observational equality. While the constructs and typing +rules are present, the machinery to make it happen (equality reduction, +coercions, quotation, etc.) is not present yet. This considered, everything else presented in Section \ref{sec:kant-theory} is implemented and working well---and in fact all @@ -4167,15 +4228,15 @@ Type: Nat 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 + process of converting a core term back to a sugared version that we + can show to the user. 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 +\item[Pretty print] Format the terms in a nice way, and display them to the user. \end{description} @@ -4400,10 +4461,10 @@ can be represented as -- Empty))'. Lam (Lam (V (Free Bound))) \end{Verbatim} -This allows us to reflect the of a type `nestedness' at the type level, +This allows us to reflect the `nestedness' of a type 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. +nestedness where they do not belong. Even more interestingly, the substitution operation is perfectly captured by the \verb|>>=| (bind) operator of the \texttt{Monad} @@ -4525,10 +4586,10 @@ way, by elaborating declarations in a series of \emph{rewriting rules}: \begin{Verbatim} type Rewr = forall v. - TmRef v -> -- Term to which the destructor is applied - [TmRef v] -> -- List of other arguments + Tm v -> -- Term to which the destructor is applied + [Tm v] -> -- List of other arguments -- The result of the rewriting, if the eliminator reduces. - Maybe [TmRef v] + Maybe [Tm v] \end{Verbatim} A rewriting rule is polymorphic in the variable type, guaranteeing that it just pattern matches on terms structure and rearranges them in some @@ -4544,7 +4605,16 @@ alternative that solves both of these is the already mentioned terms into Haskell values, and then reify back to terms to compare them---a useful tutorial on this technique is given by \cite{Loh2010}. -\subsubsection{Parametrised environment} +However, quotation has its disadvantages. The most obvious one is that +it is less simple: we need to set up some infrastructure to handle the +quotation and reification, while with substitution we have a uniform +representation through the process of type checking. The second is that +performance advantages can be rendered less effective by the continuous +quoting and reifying, although this can probably be mitigated with some +heuristics. + +\subsubsection{Parametrise everything!} +\label{sec:parame} Through the life of a REPL cycle we need to execute two broad `effectful' actions: @@ -4570,8 +4640,10 @@ data KError | IOError IOError | ... \end{Verbatim} -Without delving into the details of what a monad transformer is, this is -what \texttt{KMonadT} provides: +Without delving into the details of what a monad transformer +is,\footnote{See + \url{https://en.wikibooks.org/wiki/Haskell/Monad_transformers.}} this +is what \texttt{KMonadT} works with and provides: \begin{itemize} \item The \verb|v| parameter represents the parametrised variable for the term type that we spoke about at the beginning of this section. @@ -4585,7 +4657,7 @@ what \texttt{KMonadT} provides: environment at any time. \item The \verb|m| is the `inner' monad that we can `plug in' to be able - to do more effectful actions in \texttt{KMonatT}. For example if we + to perform more effectful actions in \texttt{KMonatT}. For example if we plug the \texttt{IO} monad in, we will be able to do input/output. \item The inner \verb|ErrorT| lets us throw errors at any time. The @@ -4628,7 +4700,7 @@ In the actual \mykant\ codebase, we have also abstracted the concept of structures and write generic operations on all context-like structures.\footnote{See the \texttt{Kant.Cursor} module for details.} -\subsection{Turning constraints into graphs} +\subsection{Turning a hierarchy into some graphs} \label{sec:hier-impl} In this section we will explain how to implement the typical ambiguity @@ -4750,9 +4822,12 @@ in \ref{fig:graph-one-after}. \label{fig:graph-one} \end{figure} -Each time we add a new constraint, we check if any strongly connected -component (SCC) arises, a SCC being a subset $V$ of vertices where for -each $(v_1,v_2) \in V \times V$ there is a path from $v_1$ to $v_2$. +\begin{mydef}[Strongly connected component] + A \emph{strongly connected component} in a graph with vertices $V$ is + a subset of $V$, say $V'$, such that for each $(v_1,v_2) \in V' \times + V$ there is a path from $v_1$ to $v_2$. +\end{mydef} + 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 @@ -4775,19 +4850,11 @@ Finally, we take a break from the types by giving a brief account of the design of our REPL, being a good example of modular design using various constructs dear to the Haskell programmer. -Across our codebase we make use of a \emph{monad transformers} named -\texttt{KMonadT}. Without delving into the details of \texttt{KMonadT} -or of monad transformers,\footnote{See - \url{https://en.wikibooks.org/wiki/Haskell/Monad_transformers.}} -computation done inside \texttt{KMonadT} can easily retrieve and modify -the environment and throw various kind of errors, be them parse error, -type errors, etc. Moreover, \texttt{KMonadT} being a monad -\emph{transformers}, we can `plug in' other monads to have access to -other facilities, such as input/output. - -That said, the REPL is represented as a function in \texttt{KMonadT} -consuming input and hopefully producing output. Then, frontends can -very easily written by marshalling data in and out of the REPL: +Keeping in mind the \texttt{KMonadT} monad described in Section +\ref{sec:parame}, the REPL is represented as a function in +\texttt{KMonadT} consuming input and hopefully producing output. Then, +frontends can very easily written by marshalling data in and out of the +REPL: \begin{Verbatim} data Input = ITyCheck String -- Type check a term @@ -4798,7 +4865,8 @@ data Input data Output = OTyCheck TmRefId [HoleCtx] -- Type checked term, with holes | OPretty TmRefId -- Term to pretty print, after evaluation - | OHoles [HoleCtx] -- Just holes, classically after loading a file + -- Just holes, classically after loading a file + | OHoles [HoleCtx] | ... -- KMonadT is parametrised over the type of the variables, which depends @@ -4807,6 +4875,7 @@ data Output type REPL m = KMonadT Id m repl :: ReadFile m => Input -> REPL m Output +repl = ... \end{Verbatim} The \texttt{ReadFile} monad embodies the only `extra' action that we need to have access too when running the REPL: reading files. We could @@ -4847,14 +4916,15 @@ instance ReadFile DirRead where Once this light-weight infrastructure is in place, adding a web interface was an easy exercise. We use Jasper Van der Jeugt's \texttt{websockets} library\footnote{Available at - \url{http://hackage.haskell.org/package/websockets}.} to create a proxy -that receives JSON messages with the user input, turns them into -\texttt{Input} messages for the REPL, and then sends back a JSON message -with the response. Moreover, each client is handled in a separate -threads, so crashes of the REPL in single threads will not bring the -whole application down. - -On the clients side, we had to write some JavaScript to accept input + \url{http://hackage.haskell.org/package/websockets}.} to create a +proxy that receives \texttt{JSON}\footnote{\texttt{JSON} is a popular data interchange + format, see \url{http://json.org} for more info.} messages with the +user input, turns them into \texttt{Input} messages for the REPL, and +then sends back a \texttt{JSON} message with the response. Moreover, each client +is handled in a separate threads, so crashes of the REPL for a certain +client will not bring the whole application down. + +On the frontend side, we had to write some JavaScript to accept input from a form, and to make the responses appear on the screen. The web prompt is publicly available at \url{http://bertus.mazzo.li}, a sample session is shown Figure \ref{fig:web-prompt-one}. @@ -4909,8 +4979,10 @@ Again, the best techniques to implement them in a dependently typed setting still have not crystallised and implementors reinvent many wheels each time a new system is built. The author is still conflicted on whether having user defined types at all it is the right decision: -while they are essential, in hindsight the idea of a bare but fully -implemented theory seems inviting. +while they are essential, the recent discovery of a paper by +\cite{dagand2012elaborating} describing a way to efficiently encode +user-defined data types to a set of core primitives---an option that +seems very attractive. In general, implementing dependently typed languages is still a poorly understood practice, and almost every stage requires experimentation on @@ -4939,10 +5011,10 @@ the type expected at that point. Furthermore, we can ask for the type of variables in context, to better understand our surroundings. In \mykant\ we use type holes by putting them where a term should go. -We need to specify a name and then we can put as many terms as we like -in the hole. \mykant\ will tell us which type it is expecting for the -term where the hole is, and the type of the terms that we have included. -For example if we had: +We need to specify a name for the hole and then we can put as many terms +as we like in it. \mykant\ will tell us which type it is expecting for +the term where the hole is, and the type for each term that we have +included. For example if we had: \begin{Verbatim} plus [m n : Nat] : Nat ⇒ ( {| h1 m n |} @@ -5077,7 +5149,7 @@ Unit >>> :e le (suc (suc zero)) (suc zero) Empty \end{Verbatim} -Another functionality of type holes is examining types of things in +The other 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}: @@ -5141,7 +5213,7 @@ more in general about the development process in \mykant. Most interactive theorem provers offer some kind of facility to... interactively develop proofs, usually much more powerful than the fairly bare tools present in \mykant. Agda in particular offers a -celebrated mode for the \texttt{Emacs} text editor. +celebrated interactive mode for the \texttt{Emacs} text editor. \section{Future work} \label{sec:future-work} @@ -5176,11 +5248,12 @@ system that we described---here we review the main ones. However as we extend the flexibility in our recursion elaborating definitions to eliminators becomes more and more laborious. For - example we might want mutually definitions and definitions that - terminate relying on the structure of two arguments instead of just - one. For this reason both Agda and Coq (Agda putting more effort) let - the user write recursive definitions freely, and then employ an - external syntactic check to ensure termination. + example we might want mutually recursive definitions and definitions + that terminate relying on the structure of two arguments instead of + just one. For this reason both Agda and Coq (Agda putting more + effort) let the user write recursive definitions freely, and then + employ an external syntactic one the recursive calls to ensure that + the definitions are terminating. Moreover, if we want to use dependently typed languages for programming purposes, we will probably want to sidestep the @@ -5202,8 +5275,8 @@ system that we described---here we review the main ones. way that Generalised Abstract Data Types \citep{GHC} are handled in Haskell. Interestingly the modified version of System F that lies at the core of recent versions of GHC features coercions reminiscent of - those found in OTT, motivated by the need to implement GADTs in an - elegant way \citep{Sulzmann2007}. + those found in OTT, motivated precisely by the need to implement GADTs + in an elegant way \citep{Sulzmann2007}. Another concept introduced by \cite{dybjer2000general} is induction-recursion, where we define a data type in tandem with a @@ -5242,7 +5315,7 @@ system that we described---here we review the main ones. is found in \emph{pattern unification}, which allows Hindley-Milner style inference for dependently typed languages. Unification for higher order terms is undecidable and unification problems do not - always have a most general unifier \cite{huet1973undecidability}. + always have a most general unifier \citep{huet1973undecidability}. However \cite{miller1992unification} identified a decidable fragment of higher order unification commonly known as pattern unification, which is employed in most theorem provers to drastically reduce the @@ -5291,10 +5364,10 @@ system that we described---here we review the main ones. language Charity, and coinduction has since been adopted in systems such as Coq \citep{Gimenez1996} and Agda. However these implementations are unsatisfactory, since Coq's break subject - reduction, and Agda does not allow types to depend on the unfolding of - codata to avoid this problem. \cite{mcbride2009let} has shown how - observational equality can help to resolve these issues, since we can - reason about the unfoldings in a better way, like we reason about + reduction; and Agda, to avoid this problem, does not allow types to + depend on the unfolding of codata. \cite{mcbride2009let} has shown + how observational equality can help to resolve these issues, since we + can reason about the unfoldings in a better way, like we reason about functions' extensional behaviour. \end{description} @@ -5316,8 +5389,8 @@ for example Typing derivations here. } -In the languages presented and Agda code samples I also highlight the syntax, -following a uniform colour and font convention: +In the languages presented and Agda code samples we also highlight the syntax, +following a uniform colour, capitalisation, and font style convention: \begin{center} \begin{tabular}{c | l} @@ -5330,15 +5403,15 @@ following a uniform colour and font convention: \end{tabular} \end{center} -When presenting grammars, I will use a word in $\mysynel{math}$ font +When presenting grammars, we 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}$ +nonterminals. Additionally, we 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 +When presenting type derivations, we often abbreviate and present multiple conclusions, each on a separate line: \begin{prooftree} \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$} @@ -5346,7 +5419,7 @@ conclusions, each on a separate line: \noLine \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mytyb}$} \end{prooftree} -I will often present `definitions' in the described calculi and in +We often present `definitions' in the described calculi and in $\mykant$\ itself, like so: \[ \begin{array}{@{}l} @@ -5354,7 +5427,7 @@ $\mykant$\ itself, like so: \myfun{name} \myappsp \myb{arg_1} \myappsp \myb{arg_2} \myappsp \cdots \mapsto \mytmsyn \end{array} \] -To define operators, I use a mixfix notation similar +To define operators, we use a mixfix notation similar to Agda, where $\myarg$s denote arguments: \[ \begin{array}{@{}l} @@ -5362,10 +5435,10 @@ to Agda, where $\myarg$s denote arguments: \myb{b_1} \mathrel{\myfun{$\wedge$}} \myb{b_2} \mapsto \cdots \end{array} \] -In explicitly typed systems, I will also omit type annotations when they +In explicitly typed systems, we omit type annotations when they are obvious, e.g. by not annotating the type of parameters of abstractions or of dependent pairs.\\ -I will introduce multiple arguments in one go in arrow types: +We 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 \] @@ -5373,13 +5446,13 @@ 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: +We also omit arrows to abbreviate types: \[ (\myb{x} {:} \mytya)(\myb{y} {:} \mytyb) \myarr \cdots = (\myb{x} {:} \mytya) \myarr (\myb{y} {:} \mytyb) \myarr \cdots \] -Meta operations names will be displayed in $\mymeta{smallcaps}$ and +Meta operations names are displayed in $\mymeta{smallcaps}$ and written in a pattern matching style, also making use of boolean guards. For example, a meta operation operating on a context and terms might look like this: @@ -5391,8 +5464,8 @@ look like this: \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 +From time to time we give examples in the Haskell programming +language as defined by \cite{Haskell2010}, which we typeset in \texttt{teletype} font. I assume that the reader is already familiar with Haskell, plenty of good introductions are available \citep{LYAH,ProgInHask}. @@ -5400,9 +5473,11 @@ with Haskell, plenty of good introductions are available 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: +\ref{sec:kant-practice} and in the appendices. All the \mykant\ code +shown is meant to be working and ready to be inputted in a \mykant\ +prompt or loaded from a file. 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: ⋆