%% THIS LATEX HURTS YOUR EYES. DO NOT READ.
-\documentclass[11pt, fleqn]{article}
+% TODO side conditions
+
+\documentclass[11pt, fleqn, twoside]{article}
\usepackage{etex}
\usepackage[sc,slantedGreek]{mathpazo}
% \linespread{1.05}
% \usepackage{times}
-\oddsidemargin 0in
-\evensidemargin 0in
+\oddsidemargin .50in
+\evensidemargin -.25in
\textheight 9.5in
\textwidth 6.2in
\topmargin -7mm
\headheight 0pt
\headsep 0pt
+\usepackage{amsthm}
-%% Narrow margins
-% \usepackage{fullpage}
%% Bibtex
\usepackage{natbib}
%% Links
-\usepackage{hyperref}
+\usepackage[pdftex, pdfborderstyle={/S/U/W 0}]{hyperref}
%% Frames
\usepackage{framed}
\newcommand{\mysmall}{}
\newcommand{\mysyn}{\AgdaKeyword}
-\newcommand{\mytyc}{\AgdaDatatype}
-\newcommand{\mydc}{\AgdaInductiveConstructor}
-\newcommand{\myfld}{\AgdaField}
-\newcommand{\myfun}{\AgdaFunction}
+\newcommand{\mytyc}[1]{\textup{\AgdaDatatype{#1}}}
+\newcommand{\mydc}[1]{\textup{\AgdaInductiveConstructor{#1}}}
+\newcommand{\myfld}[1]{\textup{\AgdaField{#1}}}
+\newcommand{\myfun}[1]{\textup{\AgdaFunction{#1}}}
\newcommand{\myb}[1]{\AgdaBound{$#1$}}
\newcommand{\myfield}{\AgdaField}
\newcommand{\myind}{\AgdaIndent}
-\newcommand{\mykant}{\textsc{Bertus}}
+\newcommand{\mykant}{\textmd{\textsc{Bertus}}}
\newcommand{\mysynel}[1]{#1}
\newcommand{\myse}{\mysynel}
\newcommand{\mytmsyn}{\mysynel{term}}
\parbox{\textwidth}{
{\mysmall
\vspace{0.2cm}
- \hfill \textbf{#1} $#2$
+ \hfill \textup{\textbf{#1}} $#2$
\framebox[\textwidth]{
\parbox{\textwidth}{
\vspace{0.1cm}
\newcommand{\mylub}{\sqcup}
\newcommand{\mydefeq}{\cong}
\newcommand{\myrefl}{\mydc{refl}}
-\newcommand{\mypeq}[1]{\mathrel{\mytyc{=}_{#1}}}
+\newcommand{\mypeq}{\mytyc{=}}
\newcommand{\myjeqq}{\myfun{$=$-elim}}
\newcommand{\myjeq}[3]{\myapp{\myapp{\myapp{\myjeqq}{#1}}{#2}}{#3}}
\newcommand{\mysubst}{\myfun{subst}}
\newcommand{\mytmup}{\mytmsyn\uparrow}
\newcommand{\mydefs}{\Delta}
\newcommand{\mynf}{\Downarrow}
-\newcommand{\myinff}[3]{#1 \vdash #2 \Rightarrow #3}
+\newcommand{\myinff}[3]{#1 \vdash #2 \Uparrow #3}
\newcommand{\myinf}[2]{\myinff{\myctx}{#1}{#2}}
-\newcommand{\mychkk}[3]{#1 \vdash #2 \Leftarrow #3}
+\newcommand{\mychkk}[3]{#1 \vdash #2 \Downarrow #3}
\newcommand{\mychk}[2]{\mychkk{\myctx}{#1}{#2}}
\newcommand{\myann}[2]{#1 : #2}
\newcommand{\mydeclsyn}{\myse{decl}}
\newcommand{\mynegder}{\vspace{-0.3cm}}
\newcommand{\myquot}{\Uparrow}
\newcommand{\mynquot}{\, \Downarrow}
+\newcommand{\mycanquot}{\ensuremath{\textsc{quote}{\Uparrow}}}
+\newcommand{\myneuquot}{\ensuremath{\textsc{quote}{\Downarrow}}}
+\newcommand{\mymetaguard}{\ |\ }
+\newcommand{\mybox}{\Box}
\renewcommand{\[}{\begin{equation*}}
\renewcommand{\]}{\end{equation*}}
\newcommand{\mymacol}[2]{\text{\textcolor{#1}{$#2$}}}
+\newtheorem*{mydef}{Definition}
+\newtheoremstyle{named}{}{}{\itshape}{}{\bfseries}{}{.5em}{\textsc{#1}}
+\theoremstyle{named}
+
%% -----------------------------------------------------------------------------
\title{\mykant: Implementing Observational Equality}
\begin{document}
-\begin{titlepage}
- \centering
+\begin{titlepage}
+\begin{center}
+
+% Upper part of the page. The '~' is needed because \\
+% only works if a paragraph has started.
+\includegraphics[width=0.4\textwidth]{brouwer-cropped.png}~\\[1cm]
- \maketitle
- \thispagestyle{empty}
+\textsc{\Large Final year project}\\[0.5cm]
+
+% Title
+{ \huge \mykant: Implementing Observational Equality}\\[1.5cm]
+
+{\Large Francesco \textsc{Mazzoli} \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{<fm2209@ic.ac.uk>}}}\\[0.8cm]
\begin{minipage}{0.4\textwidth}
\begin{flushleft} \large
\end{minipage}
\begin{minipage}{0.4\textwidth}
\begin{flushright} \large
- \emph{Co-marker:} \\
+ \emph{Second marker:} \\
Dr. Philippa \textsc{Gardner}
\end{flushright}
\end{minipage}
+\vfill
+
+% Bottom of the page
+{\large \today}
+\end{center}
\end{titlepage}
\begin{abstract}
- The marriage between programming and logic has been a very fertile one. In
- particular, since the simply typed lambda calculus (STLC), a number of type
- systems have been devised with increasing expressive power.
+ The marriage between programming and logic has been a very fertile
+ one. In particular, since the definition of the simply typed lambda
+ calculus, a number of type systems have been devised with increasing
+ expressive power.
Among this systems, Inutitionistic Type Theory (ITT) has been a very
popular framework for theorem provers and programming languages.
- However, equality has always been a tricky business in ITT and related
- theories.
-
- In these thesis we will explain why this is the case, and present
- Observational Type Theory (OTT), a solution to some of the problems
- with equality. We then describe $\mykant$, a theorem prover featuring
- OTT in a setting more close to the one found in current systems.
- Having implemented part of $\mykant$ as a Haskell program, we describe
- some of the implementation issues faced.
+ However, reasoning about equality has always been a tricky business in
+ ITT and related theories. In this thesis we will explain why this is
+ the case, and present Observational Type Theory (OTT), a solution to
+ some of the problems with equality.
+
+ To bring OTT closer to the current practice of interactive theorem
+ provers, we describe \mykant, a system featuring OTT in a setting more
+ close to the one found in widely used provers such as Agda and Coq.
+ Nost notably, we feature used defined inductive and record types and a
+ cumulative, implicit type hierarchy. Having implemented part of
+ $\mykant$ as a Haskell program, we describe some of the implementation
+ issues faced.
\end{abstract}
\clearpage
\renewcommand{\abstractname}{Acknowledgements}
\begin{abstract}
- I would like to thank Steffen van Backel, my supervisor, who was brave
+ I would like to thank Steffen van Bakel, my supervisor, who was brave
enough to believe in my project and who provided much advice and
support.
I would also like to thank the Haskell and Agda community on
\texttt{IRC}, which guided me through the strange world of types; and
in particular Andrea Vezzosi and James Deikun, with whom I entertained
- countless insightful discussions in the past year. Andrea suggested
+ countless insightful discussions over the past year. Andrea suggested
Observational Type Theory as a topic of study: this thesis would not
- exist without him. Before them, Tony Fields introduced me to Haskell,
+ exist without him. Before them, Tony Field introduced me to Haskell,
unknowingly filling most of my free time from that time on.
Finally, much of the work stems from the research of Conor McBride,
\clearpage
+\section{Introduction}
+
\section{Simple and not-so-simple types}
\label{sec:types}
analysis of all the following calculi. The exposition follows the one found in
chapter 5 of \cite{Queinnec2003}.
-The syntax of $\lambda$-terms consists of three things: variables, abstractions,
-and applications:
-
+\begin{mydef}[$\lambda$-terms]
+ Syntax of the $\lambda$-calculus: variables, abstractions, and
+ applications.
+\end{mydef}
+\mynegder
\mydesc{syntax}{ }{
$
\begin{array}{r@{\ }c@{\ }l}
$
}
-Parenthesis will be omitted in the usual way:
-$\myapp{\myapp{\mytmt}{\mytmm}}{\mytmn} =
-\myapp{(\myapp{\mytmt}{\mytmm})}{\mytmn}$.
+Parenthesis will be omitted in the usual way, with application being
+left associative.
Abstractions roughly corresponds to functions, and their semantics is more
-formally explained by the $\beta$-reduction rule:
+formally explained by the $\beta$-reduction rule.
+\begin{mydef}[$\beta$-reduction]
+$\beta$-reduction and substitution for the $\lambda$-calculus.
+\end{mydef}
+\mynegder
\mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
$
\begin{array}{l}
name capturing. We will use substitution in the future for other name-binding
constructs assuming similar precautions.
-These few elements are of remarkable expressiveness, and in fact Turing
-complete. As a corollary, we must be able to devise a term that reduces forever
-(`loops' in imperative terms):
+These few elements have a remarkable expressiveness, and are in fact
+Turing complete. As a corollary, we must be able to devise a term that
+reduces forever (`loops' in imperative terms):
\[
(\myapp{\omega}{\omega}) \myred (\myapp{\omega}{\omega}) \myred \cdots \text{, with $\omega = \myabs{x}{\myapp{x}{x}}$}
\]
-A \emph{redex} is a term that can be reduced. In the untyped $\lambda$-calculus
-this will be the case for an application in which the first term is an
-abstraction, but in general we call aterm reducible if it appears to the left of
-a reduction rule. When a term contains no redexes it's said to be in
-\emph{normal form}. Given the observation above, not all terms reduce to a
-normal forms: we call the ones that do \emph{normalising}, and the ones that
-don't \emph{non-normalising}.
-
-The reduction rule presented is not syntax directed, but \emph{evaluation
- strategies} can be employed to reduce term systematically. Common evaluation
-strategies include \emph{call by value} (or \emph{strict}), where arguments of
-abstractions are reduced before being applied to the abstraction; and conversely
-\emph{call by name} (or \emph{lazy}), where we reduce only when we need to do so
-to proceed---in other words when we have an application where the function is
-still not a $\lambda$. In both these reduction strategies we never reduce under
-an abstraction: for this reason a weaker form of normalisation is used, where
-both abstractions and normal forms are said to be in \emph{weak head normal
- form}.
+\begin{mydef}[redex]
+ A \emph{redex} is a term that can be reduced.
+\end{mydef}
+In the untyped $\lambda$-calculus this will be the case for an
+application in which the first term is an abstraction, but in general we
+call aterm reducible if it appears to the left of a reduction rule.
+\begin{mydef}[normal form]
+ A term that contains no redexes is said to be in \emph{normal form}.
+\end{mydef}
+\begin{mydef}[normalising terms and systems]
+ Terms that reduce in a finite number of reduction steps to a normal
+ form are \emph{normalising}. A system in which all terms are
+ normalising is said to be have the \emph{normalisation property}, or
+ to be normalising.
+\end{mydef}
+Given the reduction behaviour of $(\myapp{\omega}{\omega})$, it is clear
+that the untyped $\lambda$-calculus does not have the normalisation
+property.
+
+We have not presented reduction in an algorithmic way, but
+\emph{evaluation strategies} can be employed to reduce term
+systematically. Common evaluation strategies include \emph{call by
+ value} (or \emph{strict}), where arguments of abstractions are reduced
+before being applied to the abstraction; and conversely \emph{call by
+ name} (or \emph{lazy}), where we reduce only when we need to do so to
+proceed---in other words when we have an application where the function
+is still not a $\lambda$. In both these reduction strategies we never
+reduce under an abstraction: for this reason a weaker form of
+normalisation is used, where both abstractions and normal forms are said
+to be in \emph{weak head normal form}.
\subsection{The simply typed $\lambda$-calculus}
A convenient way to `discipline' and reason about $\lambda$-terms is to assign
\emph{types} to them, and then check that the terms that we are forming make
-sense given our typing rules \citep{Curry1934}. The first most basic instance
-of this idea takes the name of \emph{simply typed $\lambda$ calculus}, whose
-rules are shown in figure \ref{fig:stlc}.
+sense given our typing rules \citep{Curry1934}.The first most basic instance
+of this idea takes the name of \emph{simply typed $\lambda$-calculus} (STLC).
+\begin{mydef}[Simply typed $\lambda$-calculus]
+ The syntax and typing rules for the STLC are given in Figure \ref{fig:stlc}.
+\end{mydef}
Our types contain a set of \emph{type variables} $\Phi$, which might
correspond to some `primitive' types; and $\myarr$, the type former for
In the typing rules, a context $\myctx$ is used to store the types of bound
variables: $\myctx; \myb{x} : \mytya$ adds a variable to the context and
-$\myctx(x)$ returns the type of the rightmost occurrence of $x$.
+$\myctx(x)$ extracts the type of the rightmost occurrence of $x$.
This typing system takes the name of `simply typed lambda calculus' (STLC), and
enjoys a number of properties. Two of them are expected in most type systems
\citep{Pierce2002}:
-\begin{description}
-\item[Progress] A well-typed term is not stuck---it is either a variable, or its
- constructor does not appear on the left of the $\myred$ relation (currently
+\begin{mydef}[Progress]
+ A well-typed term is not stuck---it is either a variable, or it
+ does not appear on the left of the $\myred$ relation (currently
only $\lambda$), or it can take a step according to the evaluation rules.
-\item[Preservation] If a well-typed term takes a step of evaluation, then the
- resulting term is also well-typed, and preserves the previous type. Also
- known as \emph{subject reduction}.
-\end{description}
+\end{mydef}
+\begin{mydef}[Subject reduction]
+ If a well-typed term takes a step of evaluation, then the
+ resulting term is also well-typed, and preserves the previous type.
+\end{mydef}
However, STLC buys us much more: every well-typed term is normalising
-\citep{Tait1967}. It is easy to see that we can't fill the blanks if we want to
+\citep{Tait1967}. It is easy to see that we cannot fill the blanks if we want to
give types to the non-normalising term shown before:
\[
\myapp{(\myabss{\myb{x}}{\myhole{?}}{\myapp{\myb{x}}{\myb{x}}})}{(\myabss{\myb{x}}{\myhole{?}}{\myapp{\myb{x}}{\myb{x}}})}
This makes the STLC Turing incomplete. We can recover the ability to loop by
adding a combinator that recurses:
-
+\begin{mydef}[Fixed-point combinator]\end{mydef}
+\mynegder
\noindent
\begin{minipage}{0.5\textwidth}
\mydesc{syntax}{ } {
$ \mytmsyn ::= \cdots b \mysynsep \myfix{\myb{x}}{\mytysyn}{\mytmsyn} $
- \vspace{0.4cm}
+ \vspace{0.5cm}
}
\end{minipage}
\begin{minipage}{0.5\textwidth}
\DisplayProof
}
\end{minipage}
-
+\mynegder
\mydesc{reduction:}{\myjud{\mytmsyn}{\mytmsyn}}{
$ \myfix{\myb{x}}{\mytya}{\mytmt} \myred \mysub{\mytmt}{\myb{x}}{(\myfix{\myb{x}}{\mytya}{\mytmt})}$
}
\subsection{The Curry-Howard correspondence}
It turns out that the STLC can be seen a natural deduction system for
-intuitionistic propositional logic. Terms are proofs, and their types are the
-propositions they prove. This remarkable fact is known as the Curry-Howard
-correspondence, or isomorphism.
+intuitionistic propositional logic. Terms correspond to proofs, and
+their types correspond to the propositions they prove. This remarkable
+fact is known as the Curry-Howard correspondence, or isomorphism.
The arrow ($\myarr$) type corresponds to implication. If we wish to prove that
that $(\mytya \myarr \mytyb) \myarr (\mytyb \myarr \mytycc) \myarr (\mytya
\[
\myabss{\myb{f}}{(\mytya \myarr \mytyb)}{\myabss{\myb{g}}{(\mytyb \myarr \mytycc)}{\myabss{\myb{x}}{\mytya}{\myapp{\myb{g}}{(\myapp{\myb{f}}{\myb{x}})}}}}
\]
-That is, function composition. Going beyond arrow types, we can extend our bare
-lambda calculus with useful types to represent other logical constructs, as
-shown in figure \ref{fig:natded}.
+Which is known to functional programmers as function composition. Going
+beyond arrow types, we can extend our bare lambda calculus with useful
+types to represent other logical constructs.
+\begin{mydef}[The extended STLC]
+ Figure \ref{fig:natded} shows syntax, reduction, and typing rules for
+ the \emph{extendend simply typed $\lambda$-calculus}.
+\end{mydef}
\begin{figure}[t]
\mydesc{syntax}{ }{
$\mypair{\myarg}{\myarg}$ corresponds to $\wedge$ introduction, $\myfst$
and $\mysnd$ to $\wedge$ elimination.
-The trivial type $\myunit$ corresponds to the logical $\top$, and dually
-$\myempty$ corresponds to the logical $\bot$. $\myunit$ has one introduction
-rule ($\mytt$), and thus one inhabitant; and no eliminators. $\myempty$ has no
-introduction rules, and thus no inhabitants; and one eliminator ($\myabsurd{
-}$), corresponding to the logical \emph{ex falso quodlibet}.
+The trivial type $\myunit$ corresponds to the logical $\top$ (true), and
+dually $\myempty$ corresponds to the logical $\bot$ (false). $\myunit$
+has one introduction rule ($\mytt$), and thus one inhabitant; and no
+eliminators. $\myempty$ has no introduction rules, and thus no
+inhabitants; and one eliminator ($\myabsurd{ }$), corresponding to the
+logical \emph{ex falso quodlibet}.
With these rules, our STLC now looks remarkably similar in power and use to the
-natural deduction we already know. $\myneg \mytya$ can be expressed as $\mytya
-\myarr \myempty$. However, there is an important omission: there is no term of
+natural deduction we already know.
+\begin{mydef}[Negation]
+ $\myneg \mytya$ can be expressed as $\mytya \myarr \myempty$.
+\end{mydef}
+However, there is an important omission: there is no term of
the type $\mytya \mysum \myneg \mytya$ (excluded middle), or equivalently
$\myneg \myneg \mytya \myarr \mytya$ (double negation), or indeed any term with
a type equivalent to those.
-This has a considerable effect on our logic and it's no coincidence, since there
+This has a considerable effect on our logic and it is no coincidence, since there
is no obvious computational behaviour for laws like the excluded middle.
-Theories of this kind are called \emph{intuitionistic}, or \emph{constructive},
+Logics of this kind are called \emph{intuitionistic}, or \emph{constructive},
and all the systems analysed will have this characteristic since they build on
the foundation of the STLC.\footnote{There is research to give computational
behaviour to classical logic, but I will not touch those subjects.}
of a type former, various constructors, and an eliminator (or destructor) that
serves as primitive recursor.
-For example, we might add a $\mylist$ type constructor, along with an `empty
+\begin{mydef}[Finite lists for the STLC]
+We add a $\mylist$ type constructor, along with an `empty
list' ($\mynil{ }$) and `cons cell' ($\mycons$) constructor. The eliminator for
-lists will be the usual folding operation ($\myfoldr$). See figure
+lists will be the usual folding operation ($\myfoldr$). Full rules in Figure
\ref{fig:list}.
-
+\end{mydef}
+\mynegder
\begin{figure}[h]
\mydesc{syntax}{ }{
$
\begin{description}
\item[Terms depending on types (towards $\lambda{2}$)] We can quantify over
types in our type signatures. For example, we can define a polymorphic
- identity function:
+ identity function, where $\mytyp$ denotes the `type of types':
\[\displaystyle
- (\myabss{\myb{A}}{\mytyp}{\myabss{\myb{x}}{\myb{A}}{\myb{x}}}) : (\myb{A} : \mytyp) \myarr \myb{A} \myarr \myb{A}
+ (\myabss{\myb{A}}{\mytyp}{\myabss{\myb{x}}{\myb{A}}{\myb{x}}}) : (\myb{A} {:} \mytyp) \myarr \myb{A} \myarr \myb{A}
\]
- The first and most famous instance of this idea has been System F. This form
- of polymorphism and has been wildly successful, also thanks to a well known
- inference algorithm for a restricted version of System F known as
- Hindley-Milner. Languages like Haskell and SML are based on this discipline.
+ The first and most famous instance of this idea has been System F.
+ This form of polymorphism and has been wildly successful, also thanks
+ to a well known inference algorithm for a restricted version of System
+ F known as Hindley-Milner \citep{milner1978theory}. Languages like
+ Haskell and SML are based on this discipline.
\item[Types depending on types (towards $\lambda{\underline{\omega}}$)] We have
type operators. For example we could define a function that given types $R$
and $\mytya$ forms the type that represents a value of type $\mytya$ in
\subsection{A Bit of History}
-Logic frameworks and programming languages based on type theory have a long
-history. Per Martin-L\"{o}f described the first version of his theory in 1971,
-but then revised it since the original version was inconsistent due to its
-impredicativity.\footnote{In the early version there was only one universe
- $\mytyp$ and $\mytyp : \mytyp$, see Section \ref{sec:term-types} for an
- explanation on why this causes problems.} For this reason he gave a revised
-and consistent definition later \citep{Martin-Lof1984}.
+Logic frameworks and programming languages based on type theory have a
+long history. Per Martin-L\"{o}f described the first version of his
+theory in 1971, but then revised it since the original version was
+inconsistent due to its impredicativity.\footnote{In the early version
+ there was only one universe $\mytyp$ and $\mytyp : \mytyp$; see
+ Section \ref{sec:term-types} for an explanation on why this causes
+ problems.} For this reason he later gave a revised and consistent
+definition \citep{Martin-Lof1984}.
A related development is the polymorphic $\lambda$-calculus, and specifically
the previously mentioned System F, which was developed independently by Girard
The calculus I present follows the exposition in \citep{Thompson1991},
and is quite close to the original formulation of predicative ITT as
-found in \citep{Martin-Lof1984}. The system's syntax and reduction
-rules are presented in their entirety in figure \ref{fig:core-tt-syn}.
-The typing rules are presented piece by piece. Agda and \mykant\
-renditions of the presented theory and all the examples is reproduced in
-appendix \ref{app:itt-code}.
+found in \citep{Martin-Lof1984}.
+\begin{mydef}[Intuitionistic Type Theory (ITT)]
+The syntax and reduction rules are shown in Figure \ref{fig:core-tt-syn}.
+The typing rules are presented piece by piece in the following sections.
+\end{mydef}
+Agda and \mykant\ renditions of the presented theory and all the
+examples is reproduced in Appendix \ref{app:itt-code}.
\begin{figure}[t]
\mydesc{syntax}{ }{
\]
Types that are definitionally equal can be used interchangeably. Here
the `conversion' rule is not syntax directed, but it is possible to
-employ $\myred$ to decide term equality in a systematic way, by always
-reducing terms to their normal forms before comparing them, so that a
-separate conversion rule is not needed.
+employ $\myred$ to decide term equality in a systematic way, by
+comparing terms by reducing to their normal forms and then comparing
+them syntactically; so that a separate conversion rule is not needed.
Another thing to notice is that considering the need to reduce terms to
-decide equality, it is essential for a dependently type system to be
-terminating and confluent for type checking to be decidable.
+decide equality it is essential for a dependently typed system to be
+terminating and confluent for type checking to be decidable, since every
+type needs to have a \emph{unique} normal form.
Moreover, we specify a \emph{type hierarchy} to talk about `large'
types: $\mytyp_0$ will be the type of types inhabited by data:
}
With booleans we get the first taste of the `dependent' in `dependent
-types'. While the two introduction rules ($\mytrue$ and $\myfalse$) are
-not surprising, the typing rules for $\myfun{if}$ are. In most strongly
-typed languages we expect the branches of an $\myfun{if}$ statements to
-be of the same type, to preserve subject reduction, since execution
-could take both paths. This is a pity, since the type system does not
-reflect the fact that in each branch we gain knowledge on the term we
-are branching on. Which means that programs along the lines of
+types'. While the two introduction rules for $\mytrue$ and $\myfalse$
+are not surprising, the typing rules for $\myfun{if}$ are. In most
+strongly typed languages we expect the branches of an $\myfun{if}$
+statements to be of the same type, to preserve subject reduction, since
+execution could take both paths. This is a pity, since the type system
+does not reflect the fact that in each branch we gain knowledge on the
+term we are branching on. Which means that programs along the lines of
\begin{Verbatim}
if null xs then head xs else 0
\end{Verbatim}
are much like universal quantifiers ($\forall$) in logic.
For example, assuming that we have lists and natural numbers in our
-language, using dependent functions we would be able to
-write:
+language, using dependent functions we are write functions of type:
\[
\begin{array}{l}
\myfun{length} : (\myb{A} {:} \mytyp_0) \myarr \myapp{\mylist}{\myb{A}} \myarr \mynat \\
the length of the list argument is non-zero. This allows us to rule out
the `empty list' case, so that we can safely return the first element.
-Again, we need to make sure that the type hierarchy is respected, which is the
-reason why a type formed by $\myarr$ will live in the least upper bound of the
-levels of argument and return type. This trend will continue with the other
-type-level binders, $\myprod$ and $\mytyc{W}$.
+Again, we need to make sure that the type hierarchy is respected, which
+is the reason why a type formed by $\myarr$ will live in the least upper
+bound of the levels of argument and return type. If this was not the
+case, we would be able to form a `powerset' function along the lines of
+\[
+\begin{array}{@{}l}
+\myfun{P} : \mytyp_0 \myarr \mytyp_0 \\
+\myfun{P} \myappsp \myb{A} \mapsto \myb{A} \myarr \mytyp_0
+\end{array}
+\]
+Where the type of $\myb{A} \myarr \mytyp_0$ is in $\mytyp_0$ itself.
+Using this and similar devices we would be able to derive falsity
+\citep{Hurkens1995}. This trend will continue with the other type-level
+binders, $\myprod$ and $\mytyc{W}$.
\subsubsection{$\myprod$, or dependent product}
\label{sec:disju}
This area is the main concern of this thesis, and in general a very
active research topic, since we do not have a fully satisfactory
solution, yet. As in the previous section, everything presented is
-formalised in Agda in appendix \ref{app:agda-itt}.
+formalised in Agda in Appendix \ref{app:agda-itt}.
\subsection{Propositional equality}
+\begin{mydef}[Propositional equality] The syntax, reduction, and typing
+ rules for propositional equality and related constructs is defined as:
+\end{mydef}
+\mynegder
\noindent
\begin{minipage}{0.5\textwidth}
\mydesc{syntax}{ }{
$
\begin{array}{r@{\ }c@{\ }l}
\mytmsyn & ::= & \cdots \\
- & | & \mytmsyn \mypeq{\mytmsyn} \mytmsyn \mysynsep
+ & | & \mypeq \myappsp \mytmsyn \myappsp \mytmsyn \myappsp \mytmsyn \mysynsep
\myapp{\myrefl}{\mytmsyn} \\
& | & \myjeq{\mytmsyn}{\mytmsyn}{\mytmsyn}
\end{array}
\AxiomC{$\myjud{\mytya}{\mytyp_l}$}
\AxiomC{$\myjud{\mytmm}{\mytya}$}
\AxiomC{$\myjud{\mytmn}{\mytya}$}
- \TrinaryInfC{$\myjud{\mytmm \mypeq{\mytya} \mytmn}{\mytyp_l}$}
+ \TrinaryInfC{$\myjud{\mypeq \myappsp \mytya \myappsp \mytmm \myappsp \mytmn}{\mytyp_l}$}
\DisplayProof
\myderivspp
\begin{tabular}{cc}
\AxiomC{$\begin{array}{c}\ \\\myjud{\mytmm}{\mytya}\hspace{1.1cm}\mytmm \mydefeq \mytmn\end{array}$}
- \UnaryInfC{$\myjud{\myapp{\myrefl}{\mytmm}}{\mytmm \mypeq{\mytya} \mytmn}$}
+ \UnaryInfC{$\myjud{\myapp{\myrefl}{\mytmm}}{\mypeq \myappsp \mytya \myappsp \mytmm \myappsp \mytmn}$}
\DisplayProof
&
\AxiomC{$
\begin{array}{c}
- \myjud{\myse{P}}{\myfora{\myb{x}\ \myb{y}}{\mytya}{\myfora{q}{\myb{x} \mypeq{\mytya} \myb{y}}{\mytyp_l}}} \\
- \myjud{\myse{q}}{\mytmm \mypeq{\mytya} \mytmn}\hspace{1.1cm}\myjud{\myse{p}}{\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmm}}{(\myapp{\myrefl}{\mytmm})}}
+ \myjud{\myse{P}}{\myfora{\myb{x}\ \myb{y}}{\mytya}{\myfora{q}{\mypeq \myappsp \mytya \myappsp \myb{x} \myappsp \myb{y}}{\mytyp_l}}} \\
+ \myjud{\myse{q}}{\mypeq \myappsp \mytya \myappsp \mytmm \myappsp \mytmn}\hspace{1.1cm}\myjud{\myse{p}}{\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmm}}{(\myapp{\myrefl}{\mytmm})}}
\end{array}
$}
\UnaryInfC{$\myjud{\myjeq{\myse{P}}{\myse{q}}{\myse{p}}}{\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmn}}{q}}$}
\end{tabular}
}
-To express equality between two terms inside ITT, the obvious way to do so is
-to have the equality construction to be a type-former. Here we present what
-has survived as the dominating form of equality in systems based on ITT up to
-the present day.
+To express equality between two terms inside ITT, the obvious way to do
+so is to have equality to be a type. Here we present what has survived
+as the dominating form of equality in systems based on ITT up to the
+present day.
-Our type former is $\mypeq{\mytya}$, which given a type (in this case
-$\mytya$) relates equal terms of that type. $\mypeq{}$ has one introduction
+Our type former is $\mypeq$, which given a type (in this case
+$\mytya$) relates equal terms of that type. $\mypeq$ has one introduction
rule, $\myrefl$, which introduces an equality relation between definitionally
equal terms.
-Finally, we have one eliminator for $\mypeq{}$, $\myjeqq$. $\myjeq{\myse{P}}{\myse{q}}{\myse{p}}$ takes
+Finally, we have one eliminator for $\mypeq$, $\myjeqq$. $\myjeq{\myse{P}}{\myse{q}}{\myse{p}}$ takes
\begin{itemize}
\item $\myse{P}$, a predicate working with two terms of a certain type (say
$\mytya$) and a proof of their equality
twice, plus the trivial proof by reflexivity showing that $\myse{m}$
is equal to itself
\end{itemize}
-Given these ingredients, $\myjeqq$ retuns a member of $\myse{P}$ applied to
-$\mytmm$, $\mytmn$, and $\myse{q}$. In other words $\myjeqq$ takes a
-witness that $\myse{P}$ works with \emph{definitionally equal} terms, and
-returns a witness of $\myse{P}$ working with \emph{propositionally equal}
-terms. Invokations of $\myjeqq$ will vanish when the equality proofs will
-reduce to invocations to reflexivity, at which point the arguments must be
-definitionally equal, and thus the provided
+Given these ingredients, $\myjeqq$ retuns a member of $\myse{P}$ applied
+to $\mytmm$, $\mytmn$, and $\myse{q}$. In other words $\myjeqq$ takes a
+witness that $\myse{P}$ works with \emph{definitionally equal} terms,
+and returns a witness of $\myse{P}$ working with \emph{propositionally
+ equal} terms. Invokations of $\myjeqq$ will vanish when the equality
+proofs will reduce to invocations to reflexivity, at which point the
+arguments must be definitionally equal, and thus the provided
$\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmm}}{(\myapp{\myrefl}{\mytmm})}$
-can be returned.
+can be returned. This means that $\myjeqq$ will not compute with
+hypotetical proofs, which makes sense given that they might be false.
While the $\myjeqq$ rule is slightly convoluted, ve can derive many more
`friendly' rules from it, for example a more obvious `substitution' rule, that
replaces equal for equal in predicates:
\[
\begin{array}{l}
-\myfun{subst} : \myfora{\myb{A}}{\mytyp}{\myfora{\myb{P}}{\myb{A} \myarr \mytyp}{\myfora{\myb{x}\ \myb{y}}{\myb{A}}{\myb{x} \mypeq{\myb{A}} \myb{y} \myarr \myapp{\myb{P}}{\myb{x}} \myarr \myapp{\myb{P}}{\myb{y}}}}} \\
+\myfun{subst} : \myfora{\myb{A}}{\mytyp}{\myfora{\myb{P}}{\myb{A} \myarr \mytyp}{\myfora{\myb{x}\ \myb{y}}{\myb{A}}{\mypeq \myappsp \myb{A} \myappsp \myb{x} \myappsp \myb{y} \myarr \myapp{\myb{P}}{\myb{x}} \myarr \myapp{\myb{P}}{\myb{y}}}}} \\
\myfun{subst}\myappsp \myb{A}\myappsp\myb{P}\myappsp\myb{x}\myappsp\myb{y}\myappsp\myb{q}\myappsp\myb{p} \mapsto
\myjeq{(\myabs{\myb{x}\ \myb{y}\ \myb{q}}{\myapp{\myb{P}}{\myb{y}}})}{\myb{p}}{\myb{q}}
\end{array}
$\myempty$ can be considered equal. Quotation can be performed in a
type-directed way, as we will witness in Section \ref{sec:kant-irr}.
-To justify this process in our type system we will add a congruence law
+\begin{mydef}[Congruence and $\eta$-laws]
+To justify quotation in our type system we will add a congruence law
for abstractions and a similar law for products, plus the fact that all
elements of $\myunit$ or $\myempty$ are equal.
-
+\end{mydef}
+\mynegder
\mydesc{definitional equality:}{\myjud{\mytmm \mydefeq \mytmn}{\mytmsyn}}{
\begin{tabular}{cc}
\AxiomC{$\myjudd{\myctx; \myb{y} : \mytya}{\myapp{\myse{f}}{\myb{x}} \mydefeq \myapp{\myse{g}}{\myb{x}}}{\mysub{\mytyb}{\myb{x}}{\myb{y}}}$}
the $\myfun{K}$ axiom, which essentially states that all equality proofs
are by reflexivity.
+\begin{mydef}[$\myfun{K}$ axiom]\end{mydef}
\mydesc{typing:}{\myjud{\mytmm \mydefeq \mytmn}{\mytmsyn}}{
\AxiomC{$
\begin{array}{@{}c}
\epigraph{\emph{Half of my time spent doing research involves thinking up clever
schemes to avoid needing functional extensionality.}}{@larrytheliquid}
-However, propositional equality as described is quite restricted when
+Propositional equality as described is quite restricted when
reasoning about equality beyond the term structure, which is what definitional
equality gives us (extension notwithstanding).
definitionally equal, and thus we won't be able to get rid of the
quantification.
-For the reasons above, theories that offer a propositional equality
+For the reasons given above, theories that offer a propositional equality
similar to what we presented are called \emph{intensional}, as opposed
-to \emph{extensional}. Most systems in wide use today (such as Agda,
+to \emph{extensional}. Most systems widely used today (such as Agda,
Coq, and Epigram) are of this kind.
This is quite an annoyance that often makes reasoning awkward to execute. It
\subsection{Equality reflection}
One way to `solve' this problem is by identifying propositional equality with
-definitional equality:
+definitional equality.
+\begin{mydef}[Equality reflection]\end{mydef}
\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
\AxiomC{$\myjud{\myse{q}}{\mytmm \mypeq{\mytya} \mytmn}$}
\UnaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\mytya}$}
\DisplayProof
}
-This rule takes the name of \emph{equality reflection}, and is a very
-different rule from the ones we saw up to now: it links a typing judgement
-internal to the type theory to a meta-theoretic judgement that the type
-checker uses to work with terms. It is easy to see the dangerous consequences
-that this causes:
+The \emph{equality reflection} rule is a very different rule from the
+ones we saw up to now: it links a typing judgement internal to the type
+theory to a meta-theoretic judgement that the type checker uses to work
+with terms. It is easy to see the dangerous consequences that this
+causes:
\begin{itemize}
-\item The rule is syntax directed, and the type checker is presumably expected
- to come up with equality proofs when needed.
+\item The rule is not syntax directed, and the type checker is
+ presumably expected to come up with equality proofs when needed.
\item More worryingly, type checking becomes undecidable also because
computing under false assumptions becomes unsafe, since we derive any
equality proof and then use equality reflection and the conversion
rule to have terms of any type.
+
+ For example, assuming that we are in a context that contains
+ \[
+ \myb{A} : \mytyp; \myb{q} : \mypeq \myappsp \mytyp
+ \myappsp (\mytya \myarr \mytya) \myappsp \mytya
+ \]
+ we can write a looping term similar to the one we saw in Section
+ \ref{sec:untyped}:
+ % TODO dot this
\end{itemize}
Given these facts theories employing equality reflection, like NuPRL
% TODO finish
% TODO add `extentional axioms' (Hoffman), setoid models (Thorsten)
-\section{Observational equality}
+\section{The observational approach}
\label{sec:ott}
+% TODO add \begin{mydef}s
+
A recent development by \citet{Altenkirch2007}, \emph{Observational Type
Theory} (OTT), promises to keep the well behavedness of ITT while
being able to gain many useful equality proofs,\footnote{It is suspected
exists yet.} including function extensionality. The main idea is to
give the user the possibility to \emph{coerce} (or transport) values
from a type $\mytya$ to a type $\mytyb$, if the type checker can prove
-structurally that $\mytya$ and $\mytya$ are equal; and providing a
+structurally that $\mytya$ and $\mytyb$ are equal; and providing a
value-level equality based on similar principles. Here we give an
exposition which follows closely the original paper.
$
}
+\mynegder
+
+\mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
+ $
+ \begin{array}{l@{}l@{\ }c@{\ }l}
+ \myITE{\mytrue &}{\mytya}{\mytyb} & \myred & \mytya \\
+ \myITE{\myfalse &}{\mytya}{\mytyb} & \myred & \mytyb
+ \end{array}
+ $
+}
+
+\mynegder
+
\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
\begin{tabular}{cc}
\AxiomC{$\myjud{\myse{P}}{\myprop}$}
\end{tabular}
}
+\mynegder
+
\mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
\begin{tabular}{ccc}
\AxiomC{\phantom{$\myjud{\myse{P}}{\myprop}$}}
we will see later.
Why did we choose what we have in $\myprop$? Given the above
- criteria, $\mytop$ obviously fits the bill. A pair of propositions
- $\myse{P} \myand \myse{Q}$ still won't get us data. Finally, if
- $\myse{P}$ is a proposition and we have
- $\myprfora{\myb{x}}{\mytya}{\myse{P}}$ , the decoding will be a
- function which returns propositional content. The only threat is
- $\mybot$, by which we can fabricate anything we want: however if we
- are consistent there will be nothing of type $\mybot$ at the top
- level, which is what we care about regarding proof erasure.
+ criteria, $\mytop$ obviously fits the bill, since it us one element.
+ A pair of propositions $\myse{P} \myand \myse{Q}$ still won't get us
+ data, since if they both have one element the only possible pair is
+ the one formed by said elements. Finally, if $\myse{P}$ is a
+ proposition and we have $\myprfora{\myb{x}}{\mytya}{\myse{P}}$, the
+ decoding will be a function which returns propositional content. The
+ only threat is $\mybot$, by which we can fabricate anything we want:
+ however if we are consistent there will be nothing of type $\mybot$ at
+ the top level, which is what we care about regarding proof erasure.
\subsection{Equality proofs}
However they are definitionally equal, and thus we can safely remove the
coerce and return $\myb{x}$ as it is.
-This process of identifying every proof as equivalent and removing
-$\myfun{coe}$rcions is known as \emph{quotation}.
-
\section{\mykant : the theory}
\label{sec:kant-theory}
\item[Observational equality] As described in Section \ref{sec:ott} but
extended to work with the type hierarchy and to admit equality between
arbitrary data types.
+
+\item[Type holes] When building up programs interactively, it is useful
+ to leave parts unfinished while exploring the current context. This
+ is what type holes are for. We do not describe holes rigorously, but
+ provide more information about them from the implementation and usage
+ perspective in Section \ref{sec:type-holes}.
+
\end{description}
We will analyse the features one by one, along with motivations and
propagating types down the applied term. Abstractions are checked.
Finally, we have a rule to check the type of an inferrable term.
-\mydesc{typing:}{\myctx \vdash \mytmsyn \Leftrightarrow \mytmsyn}{
- \begin{tabular}{ccc}
+\mydesc{typing:}{\myctx \vdash \mytmsyn \Updownarrow \mytmsyn}{
+ \begin{tabular}{cc}
\AxiomC{$\myctx(x) = A$}
\UnaryInfC{$\myinf{\myb{x}}{A}$}
\DisplayProof
&
\AxiomC{$\myjudd{\myctx;\myb{x} : A}{\mytmt}{\mytyb}$}
- \UnaryInfC{$\mychk{\myabs{x}{\mytmt}}{\mytyb}$}
- \DisplayProof
- &
- \AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$}
- \AxiomC{$\myjud{\mytmn}{\mytya}$}
- \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mytyb}$}
+ \UnaryInfC{$\mychk{\myabs{x}{\mytmt}}{(\myb{x} {:} \mytya) \myarr \mytyb}$}
\DisplayProof
\end{tabular}
\myderivspp
- \begin{tabular}{cc}
+ \begin{tabular}{ccc}
+ \AxiomC{$\myinf{\mytmm}{\mytya \myarr \mytyb}$}
+ \AxiomC{$\mychk{\mytmn}{\mytya}$}
+ \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mytyb}$}
+ \DisplayProof
+ &
\AxiomC{$\mychk{\mytmt}{\mytya}$}
\UnaryInfC{$\myinf{\myann{\mytmt}{\mytya}}{\mytya}$}
\DisplayProof
&
\AxiomC{$\myinf{\mytmt}{\mytya}$}
- \UnaryInfC{$\mychk{\mytmt}{\mytya}$}
+ \UnaryInfC{$\myinf{\mytmt}{\mytya}$}
\DisplayProof
\end{tabular}
}
conversion rule, we defer a detailed account of definitional equality to
Section \ref{sec:kant-irr}.
-\mydesc{typing:}{\myctx \vdash \mytmsyn \Leftrightarrow \mytmsyn}{
+\mydesc{typing:}{\myctx \vdash \mytmsyn \Updownarrow \mytmsyn}{
\begin{tabular}{cccc}
\AxiomC{$\myse{name} : A \in \myctx$}
\UnaryInfC{$\myinf{\myse{name}}{A}$}
\BinaryInfC{$\mychk{\mytmt}{\mytyb}$}
\DisplayProof
\end{tabular}
+
\myderivspp
- \begin{tabular}{ccc}
+ \begin{tabular}{cc}
+
+ \AxiomC{\phantom{$\mychkk{\myctx; \myb{x}: \mytya}{\mytmt}{\mytyb}$}}
+ \UnaryInfC{$\myinf{\mytyp}{\mytyp}$}
+ \DisplayProof
+ &
+ \AxiomC{$\myinf{\mytya}{\mytyp}$}
+ \AxiomC{$\myinff{\myctx; \myb{x} : \mytya}{\mytyb}{\mytyp}$}
+ \BinaryInfC{$\myinf{(\myb{x} {:} \mytya) \myarr \mytyb}{\mytyp}$}
+ \DisplayProof
+
+ \end{tabular}
+
+
+ \myderivspp
+
+ \begin{tabular}{cc}
\AxiomC{$\myinf{\mytmm}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
\AxiomC{$\mychk{\mytmn}{\mytya}$}
\BinaryInfC{$\myinf{\myapp{\mytmm}{\mytmn}}{\mysub{\mytyb}{\myb{x}}{\mytmn}}$}
\UnaryInfC{$\mychk{\myabs{\myb{x}}{\mytmt}}{\myfora{\myb{x}}{\mytyb}{\mytyb}}$}
\DisplayProof
\end{tabular}
+
}
\subsection{Elaboration}
but also custom data types and records. \emph{Elaboration} consists of
turning these declarations into workable syntax, types, and reduction
rules. The treatment of custom types in $\mykant$\ is heavily inspired
-by McBride and McKinna early work on Epigram \citep{McBride2004},
+by McBride's and McKinna's early work on Epigram \citep{McBride2004},
although with some differences.
\subsubsection{Term vectors, telescopes, and assorted notation}
refer to an index in such vectors. We also often need to `build up'
terms vectors, in which case we use $\myemptyctx$ for an empty vector
and add elements to an existing vector with $\myarg ; \myarg$, similarly
-to what we do for context.
+to what we do for contexts.
To present the elaboration and operations on user defined data types, we
frequently make use what de Bruijn called \emph{telescopes}
\citep{Bruijn91}, a construct that will prove useful when dealing with
the types of type and data constructors. A telescope is a series of
nested typed bindings, such as $(\myb{x} {:} \mynat); (\myb{p} {:}
-\myapp{\myfun{even}}{\myb{x}})$. Consistently with the notation for
+\myapp{\myfun{even}}{\myb{x}})$. Consistent with the notation for
contexts and term vectors, we use $\myemptyctx$ to denote an empty
telescope and $\myarg ; \myarg$ to add a new binding to an existing
telescope.
\begin{description}
\item[Defined value] A variable, together with a type and a body.
\item[Abstract variable] An abstract variable, with a type but no body.
-\item[Inductive data] A datatype, with a type constructor and various data
- constructors---somewhat similar to what we find in Haskell. A primitive
- recursor (or `destructor') will be generated automatically.
+\item[Inductive data] A datatype, with a type constructor and various
+ data constructors, quite similar to what we find in Haskell. A
+ primitive recursor (or `destructor') will be generated automatically.
\item[Record] A record, which consists of one data constructor and various
fields, with no recursive occurrences.
\end{description}
-Elaborating defined variables consists of type checking body against the
-given type, and updating the context to contain the new binding.
+Elaborating defined variables consists of type checking the body against
+the given type, and updating the context to contain the new binding.
Elaborating abstract variables and abstract variables consists of type
checking the type, and updating the context with a new typed variable:
\subsubsection{User defined types}
\label{sec:user-type}
-Elaborating user defined types is the real effort. First, let's explain
-what we can defined, with some examples.
+Elaborating user defined types is the real effort. First, we will
+explain what we can define, with some examples.
\begin{description}
\item[Natural numbers] To define natural numbers, we create a data type
\end{center}
While in Haskell (or indeed in Agda or Coq) data constructors are
treated the same way as functions, in $\mykant$\ they are syntax, so
- for example using $\mytyc{\mynat}.\mydc{suc}$ on its own will be a
+ for example using $\mytyc{\mynat}.\mydc{suc}$ on its own will give a
syntax error. This is necessary so that we can easily infer the type
of polymorphic data constructors, as we will see later.
of various features but it is not needed in the implementation, where
we can have a dictionary to lookup the type constructor corresponding
to each data constructor. When using data constructors in examples I
- will omit the type constructor prefix for brevity.
+ will omit the type constructor prefix for brevity, in this case
+ writing $\mydc{zero}$ instead of $\mynat.\mydc{suc}$ and $\mydc{suc}$ instead of
+ $\mynat.\mydc{suc}$.
Along with user defined constructors, $\mykant$\ automatically
generates an \emph{eliminator}, or \emph{destructor}, to compute with
While the induction principle is usually seen as a mean to prove
properties about numbers, in the intuitionistic setting it is also a
- mean to compute. In this specific case we will $\mynat.\myfun{elim}$
- will return the base case if the provided number is $\mydc{zero}$, and
- recursively apply the inductive step if the number is a
+ mean to compute. In this specific case $\mynat.\myfun{elim}$
+ returns the base case if the provided number is $\mydc{zero}$, and
+ recursively applies the inductive step if the number is a
$\mydc{suc}$cessor:
\[
\begin{array}{@{}l@{}l}
elim Zero pz ps = pz
elim (Suc n) pz ps = ps n (elim n pz ps)
\end{Verbatim}
- Which buys us the computational behaviour, but not the reasoning power.
+Which buys us the computational behaviour, but not the reasoning power,
+since we cannot express the notion of a predicate depending on $\mynat$,
+since the type system is far too weak.
\item[Binary trees] Now for a polymorphic data type: binary trees, since
lists are too similar to natural numbers to be interesting.
$}
\end{prooftree}
As expected, the eliminator embodies structural induction on trees.
+ We have a base case for $\myb{P} \myappsp \mydc{leaf}$, and an
+ inductive step that given two subtrees and the predicate applied to
+ them we need to return the predicate applied to the tree formed by a
+ node with the two subtrees as children.
\item[Empty type] We have presented types that have at least one
constructors, but nothing prevents us from defining types with
}
\end{array}
\]
- If we want we can then employ this structure to write and prove
- correct various sorting algorithms.\footnote{See this presentation by
- Conor McBride:
+ Note that in the $\mydc{cons}$ constructor we quantify over the first
+ argument, which will determine the type of the following
+ arguments---again something we cannot do in systems like Haskell. If
+ we want we can then employ this structure to write and prove correct
+ various sorting algorithms.\footnote{See this presentation by Conor
+ McBride:
\url{https://personal.cis.strath.ac.uk/conor.mcbride/Pivotal.pdf},
and this blog post by the author:
\url{http://mazzo.li/posts/AgdaSort.html}.}
\end{figure}
Following the intuition given by the examples, the mechanised
-elaboration is presented in figure \ref{fig:elab}, which is essentially
-a modification of figure 9 of \citep{McBride2004}\footnote{However, our
+elaboration is presented in Figure \ref{fig:elab}, which is essentially
+a modification of Figure 9 of \citep{McBride2004}\footnote{However, our
datatypes do not have indices, we do bidirectional typechecking by
treating constructors/destructors as syntactic constructs, and we have
records.}.
-In data types declarations we allow recursive occurrences as long as
+In data type declarations we allow recursive occurrences as long as
they are \emph{strictly positive}, employing a syntactic check to make
sure that this is the case. See \cite{Dybjer1991} for a more formal
treatment of inductive definitions in ITT.
A better option is to employ a mechanised version of what Russell called
\emph{typical ambiguity}: we let the user live under the illusion that
$\mytyp : \mytyp$, but check that the statements about types are
-consistent behind the hood. $\mykant$\ implements this following the
+consistent under the hood. $\mykant$\ implements this following the
lines of \cite{Huet1988}. See also \citep{Harper1991} for a published
reference, although describing a more complex system allowing for both
explicit and explicit hierarchy at the same time.
\subsubsection{Some OTT examples}
-Before presenting the direction that $\mykant$\ takes, let's consider
+Before presenting the direction that $\mykant$\ takes, let us consider
some examples of use-defined data types, and the result we would expect,
given what we already know about OTT, assuming the same propositional
equalities.
\end{array}
\]
The difference here is that in the original presentation of OTT
- the type binders are explicit, while here $\mytyb_1$ and $\mytyb_2$
+ the type binders are explicit, while here $\mytyb_1$ and $\mytyb_2$ are
functions returning types. We can do this thanks to the type
hierarchy, and this hints at the fact that heterogeneous equality will
have to allow $\mytyp$ `to the right of the colon', and in fact this
}
\mynegder
- % TODO equality for decodings
+
\mydesc{equality reduction:}{\myctx \vdash \myprsyn \myred \myprsyn}{
\small
\begin{tabular}{cc}
\subsubsection{$\myprop$ and the hierarchy}
-Where is $\myprop$ placed in the type hierarchy? The main indicator
-is the decoding operator, since it converts into things that already
-live in the hierarchy. For example, if we
-have
+We shall have, at earch universe level, not only a $\mytyp_l$ but also a
+$\myprop_l$. Where will propositions placed in the type hierarchy? The
+main indicator is the decoding operator, since it converts into things
+that already live in the hierarchy. For example, if we have
\[
\myprdec{\mynat \myarr \mybool \myeq \mynat \myarr \mybool} \myred
\mytop \myand ((\myb{x}\, \myb{y} : \mynat) \myarr \mytop \myarr \mytop)
\myred
\myfora{\myb{x_1}}{\mytya_1}{\myfora{\myb{x_2}}{\mytya_2}{\cdots}}
\]
-where the proposition decodes into something of type $\mytyp_l$, where
-$\mytya : \mytyp_l$ and $\mytyb : \mytyp_l$. We can resolve this
+where the proposition decodes into something of at least type $\mytyp_l$, where
+$\mytya_l : \mytyp_l$ and $\mytyb_l : \mytyp_l$. We can resolve this
tension by making all equalities larger:
\begin{prooftree}
\AxiomC{$\myjud{\mytmm}{\mytya}$}
% TODO finish this
\begin{figure}[t]
- \mydesc{canonical quotation}{\myctx \vdash \mytmsyn \myquot \mytmsyn \mapsto \mytmsyn}{
-
+ \mydesc{canonical quotation:}{\mycanquot(\myctx, \mytmsyn : \mytmsyn) \mymetagoes \mytmsyn}{
+ \small
+ $
+ \begin{array}{@{}l}
+ \mycanquot(\myctx, \mytmt : \mytyc{D} \myappsp \vec{A}) \mymetaguard \mymeta{empty}(\myctx, \mytyc{D}) \mymetagoes \boxed{\mytmt} \\
+ \mycanquot(\myctx, \mytmt : \mytyc{D} \myappsp \vec{A}) \mymetaguard \mymeta{record}(\myctx, \mytyc{D}) \mymetagoes \\ \myind{2} \mytyc{D}.\mydc{constr} \myappsp \cdots \myappsp \mycanquot(\myctx, \mytyc{D}.\myfun{f}_n : (\myctx(\mytyc{D}.\myfun{f}_n))(\vec{A};\mytmt)) \\
+ \mycanquot(\myctx, \mytyc{D}.\mydc{c} \myappsp \vec{t} : \mytyc{D} \myappsp \vec{A}) \mymetagoes \cdots \\
+ \mycanquot(\myctx, \myse{f} : \myfora{\myb{x}}{\mytya}{\mytyb}) \mymetagoes \myabs{\myb{x}}{\mycanquot(\myctx; \myb{x} : \mytya, \myapp{\myse{f}}{\myb{x}} : \mytyb)} \\
+ \mycanquot(\myctx, \myse{p} : \myprdec{\myse{P}}) \mymetagoes \boxed{\myse{p}}
+ \\
+ \mycanquot(\myctx, \mytmt : \mytya) \mymetagoes \mytmt'\text{, where}\ \mytmt' : \myarg = \myneuquot(\myctx, \mytmt)
+ \end{array}
+ $
}
\mynegder
- \mydesc{neutral quotation}{\myctx \vdash \mynquot \mytmsyn \mapsto \mytmsyn : \mytmsyn}{
-
+ \mydesc{neutral quotation:}{\myneuquot(\myctx, \mytmsyn) \mymetagoes \mytmsyn : \mytmsyn}{
+ \small
+ $
+ \begin{array}{@{}l@{}l}
+ \myneuquot(\myctx,\ \myb{x} &) \mymetagoes \myb{x} : \myctx(\myb{x}) \\
+ \myneuquot(\myctx,\ \mytyp &) \mymetagoes \mytyp : \mytyp \\
+ \myneuquot(\myctx,\ \myfora{\myb{x}}{\mytya}{\mytyb} & ) \mymetagoes
+ \myfora{\myb{x}}{\myneuquot(\myctx, \mytya)}{\myneuquot(\myctx; \myb{x} : \mytya, \mytyb)} : \mytyp \\
+ \myneuquot(\myctx,\ \mytyc{D} \myappsp \vec{A} &) \mymetagoes \mytyc{D} \myappsp \cdots \mycanquot(\myctx, \mymeta{head}((\myctx(\mytyc{D}))(\mytya_1 \cdots \mytya_{n-1}))) : \mytyp \\
+ \myneuquot(\myctx,\ \myprdec{\myjm{\mytmm}{\mytya}{\mytmn}{\mytyb}} &) \mymetagoes \myprdec{\myjm{\mycanquot(\myctx, \mytmm : \mytya)}{\mytya'}{\mycanquot(\myctx, \mytmn : \mytyb)}{\mytyb'}} : \mytyp \\
+ \multicolumn{2}{@{}l}{\myind{2}\text{where}\ \mytya' : \myarg = \myneuquot(\myctx, \mytya)\text{, and}\ \mytyb' : \myarg = \myneuquot(\myctx, \mytyb)} \\
+ \myneuquot(\myctx,\ \mytyc{D}.\myfun{f} \myappsp \mytmt &) \mymetaguard \mymeta{record}(\myctx, \mytyc{D}) \mymetagoes \\
+ \multicolumn{2}{@{}l}{\myind{2} \mytyc{D}.\myfun{f} \myappsp \mytmt' : (\myctx(\mytyc{D}.\myfun{f}))(\vec{A};\mytmt)\text{, where}\ \mytmt' : \mytyc{D} \myappsp \vec{A} = \myneuquot(\myctx, \mytmt)} \\
+ \myneuquot(\myctx,\ \mytyc{D}.\myfun{elim} \myappsp \mytmt \myappsp \myse{P} &) \mymetaguard \mymeta{empty}(\myctx, \mytyc{D}) \mymetagoes \mytyc{D}.\myfun{elim} \myappsp \boxed{\mytmt} \myappsp \myneuquot(\myctx, \myse{P} \myappsp \mytmt) \\
+ \myneuquot(\myctx,\ \mytyc{D}.\myfun{elim} \myappsp \mytmm \myappsp \myse{P} \myappsp \vec{\mytmn} &) \mymetagoes \cdots \\
+ \myneuquot(\myctx,\ \myapp{\myse{f}}{\mytmt} &) \mymetagoes \\
+ \multicolumn{2}{@{}l}{\myind{2} \myapp{\myse{f'}}{\mycanquot(\myctx, \mytmt : \mytya)} : \mysub{\mytyb}{\myb{x}}{\mytmt}\text{, where}\ \myse{f'} : \myfora{\myb{x}}{\mytya}{\mytyb} = \myneuquot(\myctx, \myse{f})} \\
+ \myneuquot(\myctx,\ \mycoee{\mytya}{\mytyb}{\myse{Q}}{\mytmt} &) \mymetaguard \myneuquot(\myctx, \mytya) \mydefeq_{\mybox} \myneuquot(\myctx, \mytyb) \mymetagoes \myneuquot(\myctx, \mytmt) \\
+\myneuquot(\myctx,\ \mycoee{\mytya}{\mytyb}{\myse{Q}}{\mytmt} &) \mymetagoes
+ \mycoee{\myneuquot(\myctx, \mytya)}{\myneuquot(\myctx, \mytyb)}{\boxed{\myse{Q}}}{\myneuquot(\myctx, \mytmt)}
+ \end{array}
+ $
}
\caption{Quotation in \mykant.}
\label{fig:kant-quot}
ways \mykant\ is something in between the first and second version of
Epigram.
-The author learnt the hard way the implementations challenges for such a
+The author learnt the hard way the implementation challenges for such a
project, and while there is a solid and working base to work on, the
implementation of observational equality is not currently complete.
However, given the detailed plan in the previous section, doing so
\label{fig:kant-web}
\end{figure}
-The interaction with the user takes place in a loop living in and updating a
-context \mykant\ declarations. The user inputs a new declaration that goes
-through various stages starts with the user inputing a \mykant\ declaration or
-another REPL command, which then goes through various stages that can end up
-in a context update, or in failures of various kind. The process is described
-diagrammatically in figure \ref{fig:kant-process}:
+The interaction with the user takes place in a loop living in and
+updating a context of \mykant\ declarations. A REPL cycle starts with
+the user inputing a \mykant\ declaration or another REPL command, which
+then goes through various stages that can end up in a context update, or
+in failures of various kind. The process is described diagrammatically
+in figure \ref{fig:kant-process}:
\begin{description}
+
\item[Parse] In this phase the text input gets converted to a sugared
- version of the core language.
+ version of the core language. For example, we accept multiple
+ arguments in arrow types and abstractions, and we represent variables
+ with names, while as we will see in Section \ref{sec:term-repr} the
+ final term types uses a \emph{nameless} representation.
\item[Desugar] The sugared declaration is converted to a core term.
+ Most notably we go from names to nameless.
+
+\item[ConDestr] Short for `Constructors/Destructors', converts
+ applications of data destructors and constructors to a special form,
+ to perform bidirectional type checking.
\item[Reference] Occurrences of $\mytyp$ get decorated by a unique reference,
which is necessary to implement the type hierarchy check.
tandem with \textbf{Type checking}, which in turns needs to
\textbf{Evaluate} terms.
-\item[Distill] and report the result. `Distilling' refers to the process of
- converting a core term back to a sugared version that the user can
- visualise. This can be necessary both to display errors including terms or
- to display result of evaluations or type checking that the user has
- requested.
+\item[Distill] and report the result. `Distilling' refers to the
+ process of converting a core term back to a sugared version that the
+ user can visualise. This can be necessary both to display errors
+ including terms or to display result of evaluations or type checking
+ that the user has requested. Among the other things in this stage we
+ go from nameless back to names by recycling the names that the user
+ used originally, as to fabricate a term which is as close as possible
+ to what it originated from.
\item[Pretty print] Format the terms in a nice way, and display the result to
the user.
\node [cloud] (user) {User};
\node [block, below left=1cm and 0.1cm of user] (parse) {Parse};
\node [block, below=of parse] (desugar) {Desugar};
- \node [block, below=of desugar] (reference) {Reference};
+ \node [block, below=of desugar] (condestr) {ConDestr};
+ \node [block, below=of condestr] (reference) {Reference};
\node [block, below=of reference] (elaborate) {Elaborate};
\node [block, left=of elaborate] (tycheck) {Typecheck};
\node [block, left=of tycheck] (evaluate) {Evaluate};
\node [decision, right=of elaborate] (error) {Error?};
- \node [block, right=of parse] (distill) {Distill};
- \node [block, right=of desugar] (update) {Update context};
+ \node [block, right=of parse] (pretty) {Pretty print};
+ \node [block, below=of pretty] (distill) {Distill};
+ \node [block, below=of distill] (update) {Update context};
\path [line] (user) -- (parse);
\path [line] (parse) -- (desugar);
- \path [line] (desugar) -- (reference);
+ \path [line] (desugar) -- (condestr);
+ \path [line] (condestr) -- (reference);
\path [line] (reference) -- (elaborate);
\path [line] (elaborate) edge[bend right] (tycheck);
\path [line] (tycheck) edge[bend right] (elaborate);
\path [line] (error) edge[out=0,in=0] node [near start] {yes} (distill);
\path [line] (error) -- node [near start] {no} (update);
\path [line] (update) -- (distill);
- \path [line] (distill) -- (user);
+ \path [line] (pretty) -- (user);
+ \path [line] (distill) -- (pretty);
\path [line] (tycheck) edge[bend right] (evaluate);
\path [line] (evaluate) edge[bend right] (tycheck);
\end{tikzpicture}
\subsubsection{Naming and substituting}
-Perhaps surprisingly, one of the most fundamental challenges in
+Perhaps surprisingly, one of the most difficult challenges in
implementing a theory of the kind presented is choosing a good data type
for terms, and specifically handling substitutions in a sane way.
the variable bound by the innermost binding structure, $1$ the
second-innermost, and so on. For instance with simple abstractions we
might have
- \[\mymacol{red}{\lambda}\, (\mymacol{blue}{\lambda}\, \mymacol{blue}{0}\, (\mymacol{AgdaInductiveConstructor}{\lambda\, 0}))\, (\mymacol{AgdaFunction}{\lambda}\, \mymacol{red}{1}\, \mymacol{AgdaFunction}{0}) : ((\mytya \myarr \mytya) \myarr \mytyb) \myarr \mytyb \]
+ \[
+ \begin{array}{@{}l}
+ \mymacol{red}{\lambda}\, (\mymacol{blue}{\lambda}\, \mymacol{blue}{0}\, (\mymacol{AgdaInductiveConstructor}{\lambda\, 0}))\, (\mymacol{AgdaFunction}{\lambda}\, \mymacol{red}{1}\, \mymacol{AgdaFunction}{0}) : ((\mytya \myarr \mytya) \myarr \mytyb) \myarr \mytyb\text{, which corresponds to} \\
+ \myabs{\myb{f}}{(\myabs{\myb{g}}{\myapp{\myb{g}}{(\myabs{\myb{x}}{\myb{x}})}}) \myappsp (\myabs{\myb{x}}{\myapp{\myb{f}}{\myb{x}}})} : ((\mytya \myarr \mytya) \myarr \mytyb) \myarr \mytyb
+ \end{array}
+ \]
While this technique is obviously terrible in terms of human
usability,\footnote{With some people going as far as defining it akin
simple cases. Moreover, $\alpha$ renaming ceases to be an issue, and
term comparison is purely syntactical.
- Nonetheless, more complex, more complex constructs such as pattern
- matching put some strain on the indices and many systems end up using
- explicit names anyway (Agda, Coq, \dots).
+ Nonetheless, more complex, constructs such as pattern matching put
+ some strain on the indices and many systems end up using explicit
+ names anyway (Agda, Coq, \dots).
\end{description}
territory of dependent types---\texttt{bound} being created mostly to
handle more simply typed systems.
-\texttt{bound} builds on two core ideas. The first is the suggestion by
-\cite{Bird1999} consists of parametrising the term type over the type of
-the variables, and `nest' the type each time we enter a scope. If we
-wanted to define a term for the untyped $\lambda$-calculus, we might
-have
+\texttt{bound} builds on the work of \cite{Bird1999}, who suggest to
+parametrising the term type over the type of the variables, and `nest'
+the type each time we enter a scope. If we wanted to define a term for
+the untyped $\lambda$-calculus, we might have
\begin{Verbatim}
-data Void
+-- A type with no members.
+data Empty
data Var v = Bound | Free v
| App (Tm v) (Tm v) -- Term application
| Lam (Tm (Var v)) -- Abstraction
\end{Verbatim}
-Closed terms would be of type \texttt{Tm Void}, so that there would be
+Closed terms would be of type \texttt{Tm Empty}, so that there would be
no occurrences of \texttt{V}. However, inside an abstraction, we can
have \texttt{V Bound}, representing the bound variable, and inside a
second abstraction we can have \texttt{V Bound} or \texttt{V (Free
-Bound)}. Thus the term $\myabs{\myb{x}}{\myabs{\myb{y}}{\myb{x}}}$ could be represented as
+Bound)}. Thus the term
+\[\myabs{\myb{x}}{\myabs{\myb{y}}{\myb{x}}}\]
+can be represented as
\begin{Verbatim}
-Lam (Lam (Free Bound))
+-- The top level term is of type `Tm Empty'.
+-- The inner term `Lam (Free Bound)' is of type `Tm (Var Empty)'.
+-- The second inner term `V (Free Bound)' is of type `Tm (Var (Var
+-- Empty))'.
+Lam (Lam (V (Free Bound)))
\end{Verbatim}
-This allows us to reflect at the type level the `nestedness' of a type,
+This allows us to reflect the of a type `nestedness' at the type level,
and since we usually work with functions polymorphic on the parameter
\texttt{v} it's very hard to make mistakes by putting terms of the wrong
nestedness where they don't belong.
-- `Lam' is the tricky case: we modify the function to work with bound
-- variables, so that if it encounters `Bound' it leaves it untouched
- -- (since the mapping referred to the outer scope); if it encounters a
+ -- (since the mapping refers to the outer scope); if it encounters a
-- free variable it asks `f' for the term and then updates all the
-- variables to make them refer to the outer scope they were meant to
-- be in.
The beauty of this technique is that in a few simple function we have
defined all the core operations in a general and `obviously correct'
way, with the extra confidence of having the type checker looking our
-back.
+back. For what concerns term equality, we can just ask the Haskell
+compiler to derive the instance for the \verb|Eq| type class and since
+we are nameless that will be enough (modulo fancy quotation).
Moreover, if we take the top level term type to be \verb|Tm String|, we
get for free a representation of terms with top-level, definitions;
only substitute variables for values of type \verb|m v|. This is a
considerable inconvenience. Consider for instance the case of
telescopes, which are a central tool to deal with contexts and other
-constructs:
+constructs. In Haskell we can give them a faithful representation
+with a data type along the lines of
\begin{Verbatim}
data Tele m v = End (m v) | Bind (m v) (Tele (Var v))
type TeleTm = Tele Tm
simplicity of the model above.
That said, our term type is still reasonably brief, as shown in full in
-Figure \ref{fig:term}. The fact that propositions cannot be factored
-out in another data type is a consequence of the problems described
-above. However the real pain is during elaboration, where we are forced
-to treat everything as a type while we would much rather have
+Appendix \ref{app:termrep}. The fact that propositions cannot be
+factored out in another data type is an instance of the problem
+described above. However the real pain is during elaboration, where we
+are forced to treat everything as a type while we would much rather have
telescopes. Future work would include writing a library that marries a
nice interface similar to the one of \verb|bound| with a more flexible
interface.
-\begin{figure}[t]
-{\small\begin{verbatim}-- A top-level name.
-type Id = String
--- A data/type constructor name.
-type ConId = String
-
--- A term, parametrised over the variable (`v') and over the reference
--- type used in the type hierarchy (`r').
-data Tm r v
- = V v -- Variable.
- | Ty r -- Type, with a hierarchy reference.
- | Lam (TmScope r v) -- Abstraction.
- | Arr (Tm r v) (TmScope r v) -- Dependent function.
- | App (Tm r v) (Tm r v) -- Application.
- | Ann (Tm r v) (Tm r v) -- Annotated term.
- -- Data constructor, the first ConId is the type constructor and
- -- the second is the data constructor.
- | Con ADTRec ConId ConId [Tm r v]
- -- Data destrutor, again first ConId being the type constructor
- -- and the second the name of the eliminator.
- | Destr ADTRec ConId Id (Tm r v)
- -- A type hole.
- | Hole HoleId [Tm r v]
- -- Decoding of propositions.
- | Dec (Tm r v)
-
- -- Propositions.
- | Prop r -- The type of proofs, with hierarchy reference.
- | Top
- | Bot
- | And (Tm r v) (Tm r v)
- | Forall (Tm r v) (TmScope r v)
- -- Heterogeneous equality.
- | Eq (Tm r v) (Tm r v) (Tm r v) (Tm r v)
-
--- Either a data type, or a record.
-data ADTRec = ADT | Rec
-
--- Either a coercion, or coherence.
-data Coeh = Coe | Coh\end{verbatim}
-}
- \caption{Data type for terms in \mykant.}
- \label{fig:term}
-\end{figure}
-
We also make use of a `forgetful' data type (as provided by
\verb|bound|) to store user-provided variables names along with the
`nameless' representation, so that the names will not be considered when
recover variable names that are as close as possible to what the user
originally used.
+\subsubsection{Evaluation}
+
+Another source of contention related to term representation is dealing
+with evaluation. Here \mykant\ does not make bold moves, and simply
+employs substitution. Before
+Moreover, when elaborating user defined types,
+all
+
\subsubsection{Context}
+Given the parmetrised type,
+
% TODO finish
-\subsection{Type hierarchy}
+\subsection{Turning constraints into graphs}
\label{sec:hier-impl}
-As a breath of air amongst the type gas, we will explain how to
+As an interlude from all the types, we will explain how to
implement the typical ambiguity we have spoken about in
-\ref{sec:term-hierarchy}. As mentioned, we have to verify a the
+\ref{sec:term-hierarchy} efficiently. As mentioned, we have to verify a the
consistency of a set of constraints each time we add a new one. The
constraints range over some set of variables whose members we will
denote with $x, y, z, \dots$. and are of two kinds:
$x \le y$ and $y \le x$.
Given this specification, we have implemented a standalone Haskell
-module---that we plan to release as a library---to efficiently store and
-check the consistency of constraints. Its interface is shown in Figure
-\ref{fig:constraint}. The problem unpredictably reduces to a graph
-algorithm. If we
+module---that we plan to release as a standalone library---to
+efficiently store and check the consistency of constraints. The problem
+predictably reduces to a graph algorithm, and for this reason we also
+implement a library for labelled graphs, since the existing Haskell
+graph libraries fell short in different areas.\footnote{We tried the
+\texttt{Data.Graph} module in
+\url{http://hackage.haskell.org/package/containers}, and the much more
+featureful \texttt{fgl} library
+\url{http://hackage.haskell.org/package/fgl}.}. The interfaces for
+these modules are shown in Appendix \ref{app:constraint}. The graph
+library is implemented as a modification of the code described by
+\cite{King1995}.
+
+We represent the set by building a graph where vertices are variables,
+and edges are constraints between them. The edges are labelled with the
+constraint type ($<$ or $\le$). As we add constraints, $\le$
+constraints are replaced by $<$ constraints, so that if we started with
+an empty set and added
+\[
+ x \le y,\ y < z,\ z \le k,\ k \le j,\ x < y,\ j \le y
+\]
+it would generate the graph shown in Figure \ref{fig:graph-one}.
\begin{figure}[t]
-{\small\begin{verbatim}module Data.Constraint where
-
--- | Data type holding the set of constraints, parametrised over the
--- type of the variables.
-data Constrs a
-
--- | A representation of the constraints that we can add.
-data Constr a = a :<=: a | a :<: a | a :==: a
--- | An empty set of constraints.
-empty :: Ord a => Constrs a
+\end{figure}
--- | Adds one constraint to the set, returns the new set of constraints
--- if consistent.
-addConstr :: Ord a => Constr a -> Constrs a -> Maybe (Constrs a)\end{verbatim}
-}
+\subsection{Type holes}
+\label{sec:type-holes}
- \caption{Interface for the module handling the constraints.}
- \label{fig:constraint}
-\end{figure}
+Type holes are, in the author's opinion, one of the `killer' features of
+interactive theorem provers, and one that is begging to be exported to
+the word of mainstream programming. The idea is that when we are
+developing a proof or a program we can insert a hole to have the
+software tell us the type expected at that point. Furthermore, we can
+ask for the type of variables in context, to better understand our
+sorroundings.
+In \mykant\
-\subsection{Type holes}
+\subsection{Web prompt}
-When building up programs interactively, it is useful to leave parts
-unfinished while exploring the current context. This is what type holes
-are for.
\section{Evaluation}
Haskell, plenty of good introductions are available \citep{LYAH,ProgInHask}.
When presenting grammars, I will use a word in $\mysynel{math}$ font
-(e.g. $\mytmsyn$ or $\mytysyn$) to indicate indicate nonterminals. Additionally,
-I will use quite flexibly a $\mysynel{math}$ font to indicate a syntactic
-element. More specifically, terms are usually indicated by lowercase letters
-(often $\mytmt$, $\mytmm$, or $\mytmn$); and types by an uppercase letter (often
-$\mytya$, $\mytyb$, or $\mytycc$).
+(e.g. $\mytmsyn$ or $\mytysyn$) to indicate indicate
+nonterminals. Additionally, I will use quite flexibly a $\mysynel{math}$
+font to indicate a syntactic element in derivations or meta-operations.
+More specifically, terms are usually indicated by lowercase letters
+(often $\mytmt$, $\mytmm$, or $\mytmn$); and types by an uppercase
+letter (often $\mytya$, $\mytyb$, or $\mytycc$).
When presenting type derivations, I will often abbreviate and present multiple
conclusions, each on a separate line:
are obvious, e.g. by not annotating the type of parameters of
abstractions or of dependent pairs.
-I will also introduce multiple arguments in one go in arrow types:
+I will introduce multiple arguments in one go in arrow types:
\[
(\myb{x}\, \myb{y} {:} \mytya) \myarr \cdots = (\myb{x} {:} \mytya) \myarr (\myb{y} {:} \mytya) \myarr \cdots
\]
\[
\myabs{\myb{x}\myappsp\myb{y}}{\cdots} = \myabs{\myb{x}}{\myabs{\myb{y}}{\cdots}}
\]
+I will also omit arrows to abbreviate types:
+\[
+(\myb{x} {:} \mytya)(\myb{y} {:} \mytyb) \myarr \cdots =
+(\myb{x} {:} \mytya) \myarr (\myb{y} {:} \mytyb) \myarr \cdots
+\]
\section{Code}
\verbatiminput{examples.ka}
}
-\subsection{\mykant's hierachy}
+\subsection{\mykant' hierachy}
\label{sec:hurkens}
This rendition of the Hurken's paradox does not type check with the
\verbatiminput{hurkens.ka}
}
+\subsection{Term representation}
+\label{app:termrep}
+
+Data type for terms in \mykant.
+
+{\small\begin{verbatim}-- A top-level name.
+type Id = String
+-- A data/type constructor name.
+type ConId = String
+
+-- A term, parametrised over the variable (`v') and over the reference
+-- type used in the type hierarchy (`r').
+data Tm r v
+ = V v -- Variable.
+ | Ty r -- Type, with a hierarchy reference.
+ | Lam (TmScope r v) -- Abstraction.
+ | Arr (Tm r v) (TmScope r v) -- Dependent function.
+ | App (Tm r v) (Tm r v) -- Application.
+ | Ann (Tm r v) (Tm r v) -- Annotated term.
+ -- Data constructor, the first ConId is the type constructor and
+ -- the second is the data constructor.
+ | Con ADTRec ConId ConId [Tm r v]
+ -- Data destrutor, again first ConId being the type constructor
+ -- and the second the name of the eliminator.
+ | Destr ADTRec ConId Id (Tm r v)
+ -- A type hole.
+ | Hole HoleId [Tm r v]
+ -- Decoding of propositions.
+ | Dec (Tm r v)
+
+ -- Propositions.
+ | Prop r -- The type of proofs, with hierarchy reference.
+ | Top
+ | Bot
+ | And (Tm r v) (Tm r v)
+ | Forall (Tm r v) (TmScope r v)
+ -- Heterogeneous equality.
+ | Eq (Tm r v) (Tm r v) (Tm r v) (Tm r v)
+
+-- Either a data type, or a record.
+data ADTRec = ADT | Rec
+
+-- Either a coercion, or coherence.
+data Coeh = Coe | Coh\end{verbatim}
+}
+
+\subsection{Graph and constraints modules}
+\label{app:constraint}
+
+The modules are respectively named \texttt{Data.LGraph} (short for
+`labelled graph'), and \texttt{Data.Constraint}. The type class
+constraints on the type parameters are not shown for clarity, unless
+they are meaningful to the function. In practice we use the
+\texttt{Hashable} type class on the vertex to implement the graph
+efficiently with hash maps.
+
+\subsubsection{\texttt{Data.LGraph}}
+
+{\small
+\verbatiminput{graph.hs}
+}
+
+\subsubsection{\texttt{Data.Constraint}}
+
+{\small
+\verbatiminput{constraint.hs}
+}
+
+
+
\bibliographystyle{authordate1}
\bibliography{thesis}
projects / bitonic-mengthesis.git / commitdiff