%% 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}
\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}
\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
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}
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
\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
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}.
\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
\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}
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.
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.
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.
\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]
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
\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.
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 \\
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.
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
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
\[
\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}
}
\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
\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
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
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.
\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}
\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
\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
\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.
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
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}}{
\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
\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
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}{
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
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}
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]
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}
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
\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
\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}
\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
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
\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)
\]
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'.
})
\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}}{
\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}
\mynegder
\mydesc{syntax elaboration:}{\mydeclsyn \myelabf \mytmsyn ::= \cdots}{
- \footnotesize
+ \small
$
\begin{array}{r@{\ }l}
& \myadt{\mytyc{D}}{\mytele}{}{\cdots\ |\ \mydc{c}_n : \mytele_n } \\
\mynegder
\mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
- \footnotesize
+ \small
\AxiomC{$
\begin{array}{c}
\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$}
\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 } \\
\mynegder
\mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
- \footnotesize
+ \small
\AxiomC{$
\begin{array}{c}
\myinf{\mytele \myarr \mytyp}{\mytyp}\hspace{0.8cm}
\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$}
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:
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
\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?}
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}
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}
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}.
\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}
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}})} \\
}}
\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}
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}.
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]
\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
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}
\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.
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}{
$
\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}}
\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) \\
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.
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
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}
-- 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}
\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
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:
| 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.
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
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
\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
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
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
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
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}.
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
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 |}
>>> :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}:
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}
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
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
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
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}
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}
\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}$}
\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}
\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}
\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
\]
\[
\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:
\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}.
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: ⋆
projects / bitonic-mengthesis.git / commitdiff