2 %% THIS LATEX HURTS YOUR EYES. DO NOT READ.
7 \documentclass[11pt, fleqn, twoside]{article}
10 \usepackage[usenames,dvipsnames]{xcolor}
12 % \usepackage[sc,slantedGreek]{mathpazo}
13 \usepackage[sc,osf,slantedGreek]{mathpazo}
18 \evensidemargin -.25in
31 % \usepackage{microtype}
38 \usepackage[pdftex, pdfborderstyle={/S/U/W 0}]{hyperref}
44 \usepackage[fleqn]{amsmath}
45 \usepackage{stmaryrd} %llbracket
48 \usepackage{bussproofs}
60 \usepackage{subcaption}
65 \RecustomVerbatimEnvironment
71 \usetikzlibrary{shapes,arrows,positioning}
72 \usetikzlibrary{intersections}
73 % \usepackage{tikz-cd}
74 % \usepackage{pgfplots}
79 \titleformat{\section}
80 {\normalfont\huge\scshape}
81 {\thesection\hskip 9pt\textpipe\hskip 9pt}
85 \newcommand{\sectionbreak}{\clearpage}
89 %% -----------------------------------------------------------------------------
91 \usepackage[english]{babel}
92 \usepackage[conor]{agda}
93 \renewcommand{\AgdaKeywordFontStyle}[1]{\ensuremath{\mathrm{\underline{#1}}}}
94 \renewcommand{\AgdaFunction}[1]{\textbf{\textcolor{AgdaFunction}{#1}}}
95 \renewcommand{\AgdaField}{\AgdaFunction}
96 % \definecolor{AgdaBound} {HTML}{000000}
97 \definecolor{AgdaHole} {HTML} {FFFF33}
99 \DeclareUnicodeCharacter{9665}{\ensuremath{\lhd}}
100 \DeclareUnicodeCharacter{964}{\ensuremath{\tau}}
101 \DeclareUnicodeCharacter{963}{\ensuremath{\sigma}}
102 \DeclareUnicodeCharacter{915}{\ensuremath{\Gamma}}
103 \DeclareUnicodeCharacter{8799}{\ensuremath{\stackrel{?}{=}}}
104 \DeclareUnicodeCharacter{9655}{\ensuremath{\rhd}}
106 \renewenvironment{code}%
107 {\noindent\ignorespaces\advance\leftskip\mathindent\AgdaCodeStyle\pboxed\small}%
108 {\endpboxed\par\noindent%
109 \ignorespacesafterend\small}
112 %% -----------------------------------------------------------------------------
115 \newcommand{\mysmall}{}
116 \newcommand{\mysyn}{\AgdaKeyword}
117 \newcommand{\mytyc}[1]{\textup{\AgdaDatatype{#1}}}
118 \newcommand{\mydc}[1]{\textup{\AgdaInductiveConstructor{#1}}}
119 \newcommand{\myfld}[1]{\textup{\AgdaField{#1}}}
120 \newcommand{\myfun}[1]{\textup{\AgdaFunction{#1}}}
121 \newcommand{\myb}[1]{\AgdaBound{$#1$}}
122 \newcommand{\myfield}{\AgdaField}
123 \newcommand{\myind}{\AgdaIndent}
124 \newcommand{\mykant}{\textmd{\textsc{Bertus}}}
125 \newcommand{\mysynel}[1]{#1}
126 \newcommand{\myse}{\mysynel}
127 \newcommand{\mytmsyn}{\mysynel{term}}
128 \newcommand{\mysp}{\ }
129 \newcommand{\myabs}[2]{\mydc{$\lambda$} #1 \mathrel{\mydc{$\mapsto$}} #2}
130 \newcommand{\myappsp}{\hspace{0.07cm}}
131 \newcommand{\myapp}[2]{#1 \myappsp #2}
132 \newcommand{\mysynsep}{\ \ |\ \ }
133 \newcommand{\myITE}[3]{\myfun{If}\, #1\, \myfun{Then}\, #2\, \myfun{Else}\, #3}
134 \newcommand{\mycumul}{\preceq}
136 \newcommand{\mydesc}[3]{
142 \hfill \textup{\textbf{#1}} $#2$
143 \framebox[\textwidth]{
158 \newcommand{\mytmt}{\mysynel{t}}
159 \newcommand{\mytmm}{\mysynel{m}}
160 \newcommand{\mytmn}{\mysynel{n}}
161 \newcommand{\myred}{\leadsto}
162 \newcommand{\mysub}[3]{#1[#3 / #2]}
163 \newcommand{\mytysyn}{\mysynel{type}}
164 \newcommand{\mybasetys}{K}
165 \newcommand{\mybasety}[1]{B_{#1}}
166 \newcommand{\mytya}{\myse{A}}
167 \newcommand{\mytyb}{\myse{B}}
168 \newcommand{\mytycc}{\myse{C}}
169 \newcommand{\myarr}{\mathrel{\textcolor{AgdaDatatype}{\to}}}
170 \newcommand{\myprod}{\mathrel{\textcolor{AgdaDatatype}{\times}}}
171 \newcommand{\myctx}{\Gamma}
172 \newcommand{\myvalid}[1]{#1 \vdash \underline{\mathrm{valid}}}
173 \newcommand{\myjudd}[3]{#1 \vdash #2 : #3}
174 \newcommand{\myjud}[2]{\myjudd{\myctx}{#1}{#2}}
175 \newcommand{\myabss}[3]{\mydc{$\lambda$} #1 {:} #2 \mathrel{\mydc{$\mapsto$}} #3}
176 \newcommand{\mytt}{\mydc{$\langle\rangle$}}
177 \newcommand{\myunit}{\mytyc{Unit}}
178 \newcommand{\mypair}[2]{\mathopen{\mydc{$\langle$}}#1\mathpunct{\mydc{,}} #2\mathclose{\mydc{$\rangle$}}}
179 \newcommand{\myfst}{\myfld{fst}}
180 \newcommand{\mysnd}{\myfld{snd}}
181 \newcommand{\myconst}{\myse{c}}
182 \newcommand{\myemptyctx}{\varepsilon}
183 \newcommand{\myhole}{\AgdaHole}
184 \newcommand{\myfix}[3]{\mysyn{fix} \myappsp #1 {:} #2 \mapsto #3}
185 \newcommand{\mysum}{\mathbin{\textcolor{AgdaDatatype}{+}}}
186 \newcommand{\myleft}[1]{\mydc{left}_{#1}}
187 \newcommand{\myright}[1]{\mydc{right}_{#1}}
188 \newcommand{\myempty}{\mytyc{Empty}}
189 \newcommand{\mycase}[2]{\mathopen{\myfun{[}}#1\mathpunct{\myfun{,}} #2 \mathclose{\myfun{]}}}
190 \newcommand{\myabsurd}[1]{\myfun{absurd}_{#1}}
191 \newcommand{\myarg}{\_}
192 \newcommand{\myderivsp}{}
193 \newcommand{\myderivspp}{\vspace{0.3cm}}
194 \newcommand{\mytyp}{\mytyc{Type}}
195 \newcommand{\myneg}{\myfun{$\neg$}}
196 \newcommand{\myar}{\,}
197 \newcommand{\mybool}{\mytyc{Bool}}
198 \newcommand{\mytrue}{\mydc{true}}
199 \newcommand{\myfalse}{\mydc{false}}
200 \newcommand{\myitee}[5]{\myfun{if}\,#1 / {#2.#3}\,\myfun{then}\,#4\,\myfun{else}\,#5}
201 \newcommand{\mynat}{\mytyc{$\mathbb{N}$}}
202 \newcommand{\myrat}{\mytyc{$\mathbb{R}$}}
203 \newcommand{\myite}[3]{\myfun{if}\,#1\,\myfun{then}\,#2\,\myfun{else}\,#3}
204 \newcommand{\myfora}[3]{(#1 {:} #2) \myarr #3}
205 \newcommand{\myexi}[3]{(#1 {:} #2) \myprod #3}
206 \newcommand{\mypairr}[4]{\mathopen{\mydc{$\langle$}}#1\mathpunct{\mydc{,}} #4\mathclose{\mydc{$\rangle$}}_{#2{.}#3}}
207 \newcommand{\mylist}{\mytyc{List}}
208 \newcommand{\mynil}[1]{\mydc{[]}_{#1}}
209 \newcommand{\mycons}{\mathbin{\mydc{∷}}}
210 \newcommand{\myfoldr}{\myfun{foldr}}
211 \newcommand{\myw}[3]{\myapp{\myapp{\mytyc{W}}{(#1 {:} #2)}}{#3}}
212 \newcommand{\mynodee}{\mathbin{\mydc{$\lhd$}}}
213 \newcommand{\mynode}[2]{\mynodee_{#1.#2}}
214 \newcommand{\myrec}[4]{\myfun{rec}\,#1 / {#2.#3}\,\myfun{with}\,#4}
215 \newcommand{\mylub}{\sqcup}
216 \newcommand{\mydefeq}{\cong}
217 \newcommand{\myrefl}{\mydc{refl}}
218 \newcommand{\mypeq}{\mytyc{=}}
219 \newcommand{\myjeqq}{\myfun{$=$-elim}}
220 \newcommand{\myjeq}[3]{\myapp{\myapp{\myapp{\myjeqq}{#1}}{#2}}{#3}}
221 \newcommand{\mysubst}{\myfun{subst}}
222 \newcommand{\myprsyn}{\myse{prop}}
223 \newcommand{\myprdec}[1]{\mathopen{\mytyc{$\llbracket$}} #1 \mathclose{\mytyc{$\rrbracket$}}}
224 \newcommand{\myand}{\mathrel{\mytyc{$\wedge$}}}
225 \newcommand{\mybigand}{\mathrel{\mytyc{$\bigwedge$}}}
226 \newcommand{\myprfora}[3]{\forall #1 {:} #2.\, #3}
227 \newcommand{\myimpl}{\mathrel{\mytyc{$\Rightarrow$}}}
228 \newcommand{\mybot}{\mytyc{$\bot$}}
229 \newcommand{\mytop}{\mytyc{$\top$}}
230 \newcommand{\mycoe}{\myfun{coe}}
231 \newcommand{\mycoee}[4]{\myapp{\myapp{\myapp{\myapp{\mycoe}{#1}}{#2}}{#3}}{#4}}
232 \newcommand{\mycoh}{\myfun{coh}}
233 \newcommand{\mycohh}[4]{\myapp{\myapp{\myapp{\myapp{\mycoh}{#1}}{#2}}{#3}}{#4}}
234 \newcommand{\myjm}[4]{(#1 {:} #2) \mathrel{\mytyc{=}} (#3 {:} #4)}
235 \newcommand{\myeq}{\mathrel{\mytyc{=}}}
236 \newcommand{\myprop}{\mytyc{Prop}}
237 \newcommand{\mytmup}{\mytmsyn\uparrow}
238 \newcommand{\mydefs}{\Delta}
239 \newcommand{\mynf}{\Downarrow}
240 \newcommand{\myinff}[3]{#1 \vdash #2 \Uparrow #3}
241 \newcommand{\myinf}[2]{\myinff{\myctx}{#1}{#2}}
242 \newcommand{\mychkk}[3]{#1 \vdash #2 \Downarrow #3}
243 \newcommand{\mychk}[2]{\mychkk{\myctx}{#1}{#2}}
244 \newcommand{\myann}[2]{#1 : #2}
245 \newcommand{\mydeclsyn}{\myse{decl}}
246 \newcommand{\myval}[3]{#1 : #2 \mapsto #3}
247 \newcommand{\mypost}[2]{\mysyn{abstract}\ #1 : #2}
248 \newcommand{\myadt}[4]{\mysyn{data}\ #1 #2\ \mysyn{where}\ #3\{ #4 \}}
249 \newcommand{\myreco}[4]{\mysyn{record}\ #1 #2\ \mysyn{where}\ \{ #4 \}}
250 \newcommand{\myelabt}{\vdash}
251 \newcommand{\myelabf}{\rhd}
252 \newcommand{\myelab}[2]{\myctx \myelabt #1 \myelabf #2}
253 \newcommand{\mytele}{\Delta}
254 \newcommand{\mytelee}{\delta}
255 \newcommand{\mydcctx}{\Gamma}
256 \newcommand{\mynamesyn}{\myse{name}}
257 \newcommand{\myvec}{\overrightarrow}
258 \newcommand{\mymeta}{\textsc}
259 \newcommand{\myhyps}{\mymeta{hyps}}
260 \newcommand{\mycc}{;}
261 \newcommand{\myemptytele}{\varepsilon}
262 \newcommand{\mymetagoes}{\Longrightarrow}
263 % \newcommand{\mytesctx}{\
264 \newcommand{\mytelesyn}{\myse{telescope}}
265 \newcommand{\myrecs}{\mymeta{recs}}
266 \newcommand{\myle}{\mathrel{\lcfun{$\le$}}}
267 \newcommand{\mylet}{\mysyn{let}}
268 \newcommand{\myhead}{\mymeta{head}}
269 \newcommand{\mytake}{\mymeta{take}}
270 \newcommand{\myix}{\mymeta{ix}}
271 \newcommand{\myapply}{\mymeta{apply}}
272 \newcommand{\mydataty}{\mymeta{datatype}}
273 \newcommand{\myisreco}{\mymeta{record}}
274 \newcommand{\mydcsep}{\ |\ }
275 \newcommand{\mytree}{\mytyc{Tree}}
276 \newcommand{\myproj}[1]{\myfun{$\pi_{#1}$}}
277 \newcommand{\mysigma}{\mytyc{$\Sigma$}}
278 \newcommand{\mynegder}{\vspace{-0.3cm}}
279 \newcommand{\myquot}{\Uparrow}
280 \newcommand{\mynquot}{\, \Downarrow}
281 \newcommand{\mycanquot}{\ensuremath{\textsc{quote}{\Downarrow}}}
282 \newcommand{\myneuquot}{\ensuremath{\textsc{quote}{\Uparrow}}}
283 \newcommand{\mymetaguard}{\ |\ }
284 \newcommand{\mybox}{\Box}
285 \newcommand{\mytermi}[1]{\text{\texttt{#1}}}
286 \newcommand{\mysee}[1]{\langle\myse{#1}\rangle}
288 \renewcommand{\[}{\begin{equation*}}
289 \renewcommand{\]}{\end{equation*}}
290 \newcommand{\mymacol}[2]{\text{\textcolor{#1}{$#2$}}}
292 \newtheorem*{mydef}{Definition}
293 \newtheoremstyle{named}{}{}{\itshape}{}{\bfseries}{}{.5em}{\textsc{#1}}
296 \pgfdeclarelayer{background}
297 \pgfdeclarelayer{foreground}
298 \pgfsetlayers{background,main,foreground}
300 \definecolor{webgreen}{rgb}{0,.5,0}
301 \definecolor{webbrown}{rgb}{.6,0,0}
302 \definecolor{webyellow}{rgb}{0.98,0.92,0.73}
305 colorlinks=true, linktocpage=true, pdfstartpage=3, pdfstartview=FitV,
306 breaklinks=true, pdfpagemode=UseNone, pageanchor=true, pdfpagemode=UseOutlines,
307 plainpages=false, bookmarksnumbered, bookmarksopen=true, bookmarksopenlevel=1,
308 hypertexnames=true, pdfhighlight=/O, urlcolor=webbrown, linkcolor=black, citecolor=webgreen}
311 %% -----------------------------------------------------------------------------
313 \title{\mykant: Implementing Observational Equality}
314 \author{Francesco Mazzoli \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{<fm2209@ic.ac.uk>}}}
325 \pagenumbering{gobble}
330 % Upper part of the page. The '~' is needed because \\
331 % only works if a paragraph has started.
332 \includegraphics[width=0.4\textwidth]{brouwer-cropped.png}~\\[1cm]
334 \textsc{\Large Final year project}\\[0.5cm]
337 { \huge \mykant: Implementing Observational Equality}\\[1.5cm]
339 {\Large Francesco \textsc{Mazzoli} \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{<fm2209@ic.ac.uk>}}}\\[0.8cm]
341 \begin{minipage}{0.4\textwidth}
342 \begin{flushleft} \large
344 Dr. Steffen \textsc{van Bakel}
347 \begin{minipage}{0.4\textwidth}
348 \begin{flushright} \large
349 \emph{Second marker:} \\
350 Dr. Philippa \textsc{Gardner}
366 The marriage between programming and logic has been a fertile one. In
367 particular, since the definition of the simply typed
368 $\lambda$-calculus, a number of type systems have been devised with
369 increasing expressive power.
371 Among this systems, Intuitionistic Type Theory (ITT) has been a
372 popular framework for theorem provers and programming languages.
373 However, reasoning about equality has always been a tricky business in
374 ITT and related theories. In this thesis we shall explain why this is
375 the case, and present Observational Type Theory (OTT), a solution to
376 some of the problems with equality.
378 To bring OTT closer to the current practice of interactive theorem
379 provers, we describe \mykant, a system featuring OTT in a setting more
380 close to the one found in widely used provers such as Agda and Coq.
381 Most notably, we feature used defined inductive and record types and a
382 cumulative, implicit type hierarchy. Having implemented part of
383 $\mykant$ as a Haskell program, we describe some of the implementation
392 \renewcommand{\abstractname}{Acknowledgements}
394 I would like to thank Steffen van Bakel, my supervisor, who was brave
395 enough to believe in my project and who provided much advice and
398 I would also like to thank the Haskell and Agda community on
399 \texttt{IRC}, which guided me through the strange world of types; and
400 in particular Andrea Vezzosi and James Deikun, with whom I entertained
401 countless insightful discussions over the past year. Andrea suggested
402 Observational Type Theory as a topic of study: this thesis would not
403 exist without him. Before them, Tony Field introduced me to Haskell,
404 unknowingly filling most of my free time from that time on.
406 Finally, much of the work stems from the research of Conor McBride,
407 who answered many of my doubts through these months. I also owe him
417 \section{Introduction}
419 \pagenumbering{arabic}
421 Functional programming is in good shape. In particular the `well-typed'
422 line of work originating from Milner's ML has been extremely fruitful,
423 in various directions. Nowadays functional, well-typed programming
424 languages like Haskell or OCaml are slowly being absorbed by the
425 mainstream. An important related development---and in fact the original
426 motivator for ML's existence---is the advancement of the practice of
427 \emph{interactive theorem provers}.
430 An interactive theorem prover, or proof assistant, is a tool that lets
431 the user develop formal proofs with the confidence of the machine
432 checking them for correctness. While the effort towards a full
433 formalisation of mathematics has been ongoing for more than a century,
434 theorem provers have been the first class of software whose
435 implementation depends directly on these theories.
437 In a fortunate turn of events, it was discovered that well-typed
438 functional programming and proving theorems in an \emph{intuitionistic}
439 logic are the same activity. Under this discipline, the types in our
440 programming language can be interpreted as proposition in our logic; and
441 the programs implementing the specification given by the types as their
442 proofs. This fact stimulated an active transfer of techniques and
443 knowledge between logic and programming language theory, in both
446 Mathematics could provide programming with a wealth of abstractions and
447 constructs developed over centuries. Moreover, identifying our types
448 with a logic lets us focus on foundational questions regarding
449 programming with a much more solid approach, given the years of rigorous
450 study of logic. Programmers, on the other hand, had already developed a
451 number of approaches to effectively collaborate with computers, through
452 the study of programming languages.
454 In this space, we shall follow the discipline of Intuitionistic Type
455 Theory, or Martin-L\"{o}f Type Theory, after its inventor. First
456 formulated in the 70s and then adjusted through a series of revisions,
457 it has endured as the core of many practical systems widely in use
458 today, and it is the most prominent instance of the proposition-as-types
459 and proofs-as-programs paradigm. One of the most debated subjects in
460 this field has been regarding what notion of \emph{equality} should be
463 The tension when studying equality in type theory springs from the fact
464 that there is a divide between what the user can prove equal
465 \emph{inside} the theory---what is \emph{propositionally} equal---and
466 what the theorem prover identifies as equal in its meta-theory---what is
467 \emph{definitionally} equal. If we want our system to be well behaved
468 (mostly if we want type checking to be decidable) we must keep the two
469 notions separate, with definitional equality inducing propositional
470 equality, but not the reverse. However in this scenario propositional
471 equality is weaker than we would like: we can only prove terms equal
472 based on their syntactical structure, and not based on their observable
475 This thesis is concerned with exploring a new approach in this area,
476 \emph{observational} equality. Promising to provide a more adequate
477 propositional equality while retaining well-behavedness, it still is a
478 relatively unexplored notion. We set ourselves to change that by
479 studying it in a setting more akin to the one found in currently
480 available theorem provers.
482 \subsection{Structure}
484 Section \ref{sec:types} will give a brief overview of the
485 $\lambda$-calculus, both typed and untyped. This will give us the
486 chance to introduce most of the concepts mentioned above rigorously, and
487 gain some intuition about them. An excellent introduction to types in
488 general can be found in \cite{Pierce2002}, although not from the
489 perspective of theorem proving.
491 Section \ref{sec:itt} will describe a set of basic construct that form a
492 `baseline' Intuitionistic Type Theory. The goal is to familiarise with
493 the main concept of ITT before attacking the problem of equality. Given
494 the wealth of material covered the exposition is quite dense. Good
495 introductions can be found in \cite{Thompson1991}, \cite{Nordstrom1990},
496 and \cite{Martin-Lof1984} himself.
498 Section \ref{sec:equality} will introduce propositional equality. The
499 properties of propositional equality will be discussed along with its
500 limitations. After reviewing some extensions to propositional equality,
501 we will explain why identifying definitional equality with propositional
502 equality causes problems.
504 Section \ref{sec:ott} will introduce observational equality, following
505 closely the original exposition by \cite{Altenkirch2007}. The
506 presentation is free-standing but glosses over the meta-theoretic
507 properties of OTT, focusing on the mechanisms that make it work.
509 Section \ref{sec:kant-theory} is the central part of the thesis and will
510 describe \mykant, a system we have developed incorporating OTT along
511 constructs usually present in modern theorem provers. Along the way, we
512 discuss these additional features and their trade-offs. Section
513 \ref{sec:kant-practice} will describe an implementation implementing
514 part of \mykant. A high level design of the software is given, along
515 with a few specific implementation issues.
517 Finally, Section \ref{sec:evaluation} will asses the decisions made in
518 designing and implementing \mykant and the results achieved; and Section
519 \ref{sec:future-work} will give a roadmap to bring \mykant\ on par and
520 beyond the competition.
522 \subsection{Contributions}
523 \label{sec:contributions}
525 The contribution of this thesis is threefold:
528 \item Provide a description of observational equality `in context', to
529 make the subject more accessible. Considering the possibilities that
530 OTT brings to the table, we think that introducing it to a wider
531 audience can only be beneficial.
533 \item Fill in the gaps needed to make OTT work with user-defined
534 inductive types and a type hierarchy. We show how one notion of
535 equality is enough, instead of separate notions of value- and
536 type-equality as presented in the original paper. We are able to keep
537 the type equalities `small' while preserving subject reduction by
538 exploiting the fact that we work within a cumulative theory.
539 Incidentally, we also describe a generalised version of bidirectional
540 type checking for user defined types.
542 \item Provide an implementation to probe the possibilities of OTT in a
543 more realistic setting. We have implemented an ITT with user defined
544 types but due to the limited time constraints we were not able to
545 complete the implementation of observational equality. Nonetheless,
546 we describe some interesting implementation issues faced by the type
550 The system developed as part of this thesis, \mykant, incorporates OTT
551 with features that are familiar to users of existing theorem provers
552 adopting the proofs-as-programs mantra. The defining features of
556 \item[Full dependent types] In ITT, types are very `first class' notion
557 and can be the result of computation---they can \emph{depend} on
558 values, thus the name \emph{dependent types}. \mykant\ espouses this
559 notion to its full consequences.
561 \item[User defined data types and records] Instead of forcing the user
562 to choose from a restricted toolbox, we let her define types for
563 greater flexibility. We have two kinds of user defined types:
564 inductive data types, formed by various data constructors whose type
565 signatures can contain recursive occurrences of the type being
566 defined; and records, where we have just one data constructor and a
567 projection to extract each each field in said constructor.
569 \item[Consistency] Our system is meant to be consistent with respects to
570 the logic it embodies. For this reason, we restrict recursion to
571 \emph{structural} recursion on the defined inductive types, through
572 the use of operators (destructors) computing on each type. Following
573 the types-as-proofs interpretation, each destructor expresses an
574 induction principle on the data type it operates on. To achieve the
575 consistency of these operations we make sure that our recursive data
576 types are \emph{strictly positive}.
578 \item[Bidirectional type checking] We take advantage of a
579 \emph{bidirectional} type inference system in the style of
580 \cite{Pierce2000}. This cuts down the type annotations by a
581 considerable amount in an elegant way and at a very low cost.
582 Bidirectional type checking is usually employed in core calculi, in
583 \mykant\ we extend the concept to user defined data types.
585 \item[Type hierarchy] In set theory we have to take treat powerset-like
586 objects with care, if we want to avoid paradoxes. However, the
587 working mathematician is rarely concerned by this, and the consistency
588 in this regard is implicitly assumed. In the tradition of
589 \cite{Russell1927}, in \mykant\ we employ a \emph{type hierarchy} to
590 make sure that these size issues are taken care of; and we employ
591 system so that the user will be free from thinking about the
592 hierarchy, just like the mathematician is.
594 \item[Observational equality] The motivator of this thesis, \mykant\
595 incorporates a notion of observational equality, modifying the
596 original presentation by \cite{Altenkirch2007} to fit our more
597 expressive system. As mentioned, we reconcile OTT with user defined
598 types and a type hierarchy.
600 \item[Type holes] When building up programs interactively, it is useful
601 to leave parts unfinished while exploring the current context. This
602 is what type holes are for.
605 \subsection{Notation and syntax}
607 Appendix \ref{app:notation} describes the notation and syntax used in
610 \section{Simple and not-so-simple types}
613 \epigraph{\emph{Well typed programs can't go wrong.}}{Robin Milner}
615 \subsection{The untyped $\lambda$-calculus}
618 Along with Turing's machines, the earliest attempts to formalise
619 computation lead to the definition of the $\lambda$-calculus
620 \citep{Church1936}. This early programming language encodes computation
621 with a minimal syntax and no `data' in the traditional sense, but just
622 functions. Here we give a brief overview of the language, which will
623 give the chance to introduce concepts central to the analysis of all the
624 following calculi. The exposition follows the one found in Chapter 5 of
627 \begin{mydef}[$\lambda$-terms]
628 Syntax of the $\lambda$-calculus: variables, abstractions, and
634 \begin{array}{r@{\ }c@{\ }l}
635 \mytmsyn & ::= & \myb{x} \mysynsep \myabs{\myb{x}}{\mytmsyn} \mysynsep (\myapp{\mytmsyn}{\mytmsyn}) \\
636 x & \in & \text{Some enumerable set of symbols}
641 Parenthesis will be omitted in the usual way, with application being
644 Abstractions roughly corresponds to functions, and their semantics is more
645 formally explained by the $\beta$-reduction rule.
647 \begin{mydef}[$\beta$-reduction]
648 $\beta$-reduction and substitution for the $\lambda$-calculus.
651 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
654 \myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{\myb{x}}{\mytmn}\text{ \textbf{where}} \\
656 \begin{array}{l@{\ }c@{\ }l}
657 \mysub{\myb{x}}{\myb{x}}{\mytmn} & = & \mytmn \\
658 \mysub{\myb{y}}{\myb{x}}{\mytmn} & = & y\text{ \textbf{with} } \myb{x} \neq y \\
659 \mysub{(\myapp{\mytmt}{\mytmm})}{\myb{x}}{\mytmn} & = & (\myapp{\mysub{\mytmt}{\myb{x}}{\mytmn}}{\mysub{\mytmm}{\myb{x}}{\mytmn}}) \\
660 \mysub{(\myabs{\myb{x}}{\mytmm})}{\myb{x}}{\mytmn} & = & \myabs{\myb{x}}{\mytmm} \\
661 \mysub{(\myabs{\myb{y}}{\mytmm})}{\myb{x}}{\mytmn} & = & \myabs{\myb{z}}{\mysub{\mysub{\mytmm}{\myb{y}}{\myb{z}}}{\myb{x}}{\mytmn}} \\
662 \multicolumn{3}{l}{\myind{2} \text{\textbf{with} $\myb{x} \neq \myb{y}$ and $\myb{z}$ not free in $\myapp{\mytmm}{\mytmn}$}}
668 The care required during substituting variables for terms is to avoid
669 name capturing. We will use substitution in the future for other
670 name-binding constructs assuming similar precautions.
672 These few elements have a remarkable expressiveness, and are in fact
673 Turing complete. As a corollary, we must be able to devise a term that
674 reduces forever (`loops' in imperative terms):
676 (\myapp{\omega}{\omega}) \myred (\myapp{\omega}{\omega}) \myred \cdots \text{, with $\omega = \myabs{x}{\myapp{x}{x}}$}
679 A \emph{redex} is a term that can be reduced.
681 In the untyped $\lambda$-calculus this will be the case for an
682 application in which the first term is an abstraction, but in general we
683 call a term reducible if it appears to the left of a reduction rule.
684 \begin{mydef}[normal form]
685 A term that contains no redexes is said to be in \emph{normal form}.
687 \begin{mydef}[normalising terms and systems]
688 Terms that reduce in a finite number of reduction steps to a normal
689 form are \emph{normalising}. A system in which all terms are
690 normalising is said to have the \emph{normalisation property}, or
691 to be \emph{normalising}.
693 Given the reduction behaviour of $(\myapp{\omega}{\omega})$, it is clear
694 that the untyped $\lambda$-calculus does not have the normalisation
697 We have not presented reduction in an algorithmic way, but
698 \emph{evaluation strategies} can be employed to reduce term
699 systematically. Common evaluation strategies include \emph{call by
700 value} (or \emph{strict}), where arguments of abstractions are reduced
701 before being applied to the abstraction; and conversely \emph{call by
702 name} (or \emph{lazy}), where we reduce only when we need to do so to
703 proceed---in other words when we have an application where the function
704 is still not a $\lambda$. In both these reduction strategies we never
705 reduce under an abstraction: for this reason a weaker form of
706 normalisation is used, where all abstractions are said to be in
707 \emph{weak head normal form} even if their body is not.
709 \subsection{The simply typed $\lambda$-calculus}
711 A convenient way to `discipline' and reason about $\lambda$-terms is to
712 assign \emph{types} to them, and then check that the terms that we are
713 forming make sense given our typing rules \citep{Curry1934}. The first
714 most basic instance of this idea takes the name of \emph{simply typed
715 $\lambda$-calculus} (STLC).
716 \begin{mydef}[Simply typed $\lambda$-calculus]
717 The syntax and typing rules for the STLC are given in Figure \ref{fig:stlc}.
720 Our types contain a set of \emph{type variables} $\Phi$, which might
721 correspond to some `primitive' types; and $\myarr$, the type former for
722 `arrow' types, the types of functions. The language is explicitly
723 typed: when we bring a variable into scope with an abstraction, we
724 declare its type. Reduction is unchanged from the untyped
730 \begin{array}{r@{\ }c@{\ }l}
731 \mytmsyn & ::= & \myb{x} \mysynsep \myabss{\myb{x}}{\mytysyn}{\mytmsyn} \mysynsep
732 (\myapp{\mytmsyn}{\mytmsyn}) \\
733 \mytysyn & ::= & \myse{\phi} \mysynsep \mytysyn \myarr \mytysyn \mysynsep \\
734 \myb{x} & \in & \text{Some enumerable set of symbols} \\
735 \myse{\phi} & \in & \Phi
740 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
742 \AxiomC{$\myctx(x) = A$}
743 \UnaryInfC{$\myjud{\myb{x}}{A}$}
746 \AxiomC{$\myjudd{\myctx;\myb{x} : A}{\mytmt}{\mytyb}$}
747 \UnaryInfC{$\myjud{\myabss{x}{A}{\mytmt}}{\mytyb}$}
750 \AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$}
751 \AxiomC{$\myjud{\mytmn}{\mytya}$}
752 \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mytyb}$}
756 \caption{Syntax and typing rules for the STLC. Reduction is unchanged from
757 the untyped $\lambda$-calculus.}
761 In the typing rules, a context $\myctx$ is used to store the types of
762 bound variables: $\myemptyctx$ is the empty context, and $\myctx;
763 \myb{x} : \mytya$ adds a variable to the context. $\myctx(x)$ extracts
764 the type of the rightmost occurrence of $x$.
766 This typing system takes the name of `simply typed lambda calculus' (STLC), and
767 enjoys a number of properties. Two of them are expected in most type systems
769 \begin{mydef}[Progress]
770 A well-typed term is not stuck---it is either a variable, or it does
771 not appear on the left of the $\myred$ relation , or it can take a
772 step according to the evaluation rules.
774 \begin{mydef}[Subject reduction]
775 If a well-typed term takes a step of evaluation, then the
776 resulting term is also well-typed, and preserves the previous type.
779 However, STLC buys us much more: every well-typed term is normalising
780 \citep{Tait1967}. It is easy to see that we cannot fill the blanks if we want to
781 give types to the non-normalising term shown before:
783 \myapp{(\myabss{\myb{x}}{\myhole{?}}{\myapp{\myb{x}}{\myb{x}}})}{(\myabss{\myb{x}}{\myhole{?}}{\myapp{\myb{x}}{\myb{x}}})}
785 This makes the STLC Turing incomplete. We can recover the ability to loop by
786 adding a combinator that recurses:
787 \begin{mydef}[Fixed-point combinator]\end{mydef}
790 \begin{minipage}{0.5\textwidth}
792 $ \mytmsyn ::= \cdots b \mysynsep \myfix{\myb{x}}{\mytysyn}{\mytmsyn} $
796 \begin{minipage}{0.5\textwidth}
797 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}} {
798 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytmt}{\mytya}$}
799 \UnaryInfC{$\myjud{\myfix{\myb{x}}{\mytya}{\mytmt}}{\mytya}$}
804 \mydesc{reduction:}{\myjud{\mytmsyn}{\mytmsyn}}{
805 $ \myfix{\myb{x}}{\mytya}{\mytmt} \myred \mysub{\mytmt}{\myb{x}}{(\myfix{\myb{x}}{\mytya}{\mytmt})}$
808 This will deprive us of normalisation, which is a particularly bad thing if we
809 want to use the STLC as described in the next section.
811 Another important property of the STLC is the Church-Rosser property:
812 \begin{mydef}[Church-Rosser property]
813 A system is said to have the \emph{Church-Rosser} property, or to be
814 \emph{confluent}, if given any two reductions $\mytmm$ and $\mytmn$ of
815 a given term $\mytmt$, there is exist a term to which both $\mytmm$
816 and $\mytmn$ can be reduced.
818 Given that the STLC has the normalisation property and the Church-Rosser
819 property, each term has a \emph{unique} normal form.
821 \subsection{The Curry-Howard correspondence}
823 As hinted in the introduction, it turns out that the STLC can be seen a
824 natural deduction system for intuitionistic propositional logic. Terms
825 correspond to proofs, and their types correspond to the propositions
826 they prove. This remarkable fact is known as the Curry-Howard
827 correspondence, or isomorphism.
829 The arrow ($\myarr$) type corresponds to implication. If we wish to prove that
830 that $(\mytya \myarr \mytyb) \myarr (\mytyb \myarr \mytycc) \myarr (\mytya
831 \myarr \mytycc)$, all we need to do is to devise a $\lambda$-term that has the
834 \myabss{\myb{f}}{(\mytya \myarr \mytyb)}{\myabss{\myb{g}}{(\mytyb \myarr \mytycc)}{\myabss{\myb{x}}{\mytya}{\myapp{\myb{g}}{(\myapp{\myb{f}}{\myb{x}})}}}}
836 Which is known to functional programmers as function composition. Going
837 beyond arrow types, we can extend our bare lambda calculus with useful
838 types to represent other logical constructs.
839 \begin{mydef}[The extended STLC]
840 Figure \ref{fig:natded} shows syntax, reduction, and typing rules for
841 the \emph{extended simply typed $\lambda$-calculus}.
847 \begin{array}{r@{\ }c@{\ }l}
848 \mytmsyn & ::= & \cdots \\
849 & | & \mytt \mysynsep \myapp{\myabsurd{\mytysyn}}{\mytmsyn} \\
850 & | & \myapp{\myleft{\mytysyn}}{\mytmsyn} \mysynsep
851 \myapp{\myright{\mytysyn}}{\mytmsyn} \mysynsep
852 \myapp{\mycase{\mytmsyn}{\mytmsyn}}{\mytmsyn} \\
853 & | & \mypair{\mytmsyn}{\mytmsyn} \mysynsep
854 \myapp{\myfst}{\mytmsyn} \mysynsep \myapp{\mysnd}{\mytmsyn} \\
855 \mytysyn & ::= & \cdots \mysynsep \myunit \mysynsep \myempty \mysynsep \mytmsyn \mysum \mytmsyn \mysynsep \mytysyn \myprod \mytysyn
860 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
863 \begin{array}{l@{ }l@{\ }c@{\ }l}
864 \myapp{\mycase{\mytmm}{\mytmn}}{(\myapp{\myleft{\mytya} &}{\mytmt})} & \myred &
865 \myapp{\mytmm}{\mytmt} \\
866 \myapp{\mycase{\mytmm}{\mytmn}}{(\myapp{\myright{\mytya} &}{\mytmt})} & \myred &
867 \myapp{\mytmn}{\mytmt}
872 \begin{array}{l@{ }l@{\ }c@{\ }l}
873 \myapp{\myfst &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmm \\
874 \myapp{\mysnd &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmn
880 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
882 \AxiomC{\phantom{$\myjud{\mytmt}{\myempty}$}}
883 \UnaryInfC{$\myjud{\mytt}{\myunit}$}
886 \AxiomC{$\myjud{\mytmt}{\myempty}$}
887 \UnaryInfC{$\myjud{\myapp{\myabsurd{\mytya}}{\mytmt}}{\mytya}$}
894 \AxiomC{$\myjud{\mytmt}{\mytya}$}
895 \UnaryInfC{$\myjud{\myapp{\myleft{\mytyb}}{\mytmt}}{\mytya \mysum \mytyb}$}
898 \AxiomC{$\myjud{\mytmt}{\mytyb}$}
899 \UnaryInfC{$\myjud{\myapp{\myright{\mytya}}{\mytmt}}{\mytya \mysum \mytyb}$}
907 \AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$}
908 \AxiomC{$\myjud{\mytmn}{\mytya \myarr \mytycc}$}
909 \AxiomC{$\myjud{\mytmt}{\mytya \mysum \mytyb}$}
910 \TrinaryInfC{$\myjud{\myapp{\mycase{\mytmm}{\mytmn}}{\mytmt}}{\mytycc}$}
917 \AxiomC{$\myjud{\mytmm}{\mytya}$}
918 \AxiomC{$\myjud{\mytmn}{\mytyb}$}
919 \BinaryInfC{$\myjud{\mypair{\mytmm}{\mytmn}}{\mytya \myprod \mytyb}$}
922 \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
923 \UnaryInfC{$\myjud{\myapp{\myfst}{\mytmt}}{\mytya}$}
926 \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
927 \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mytyb}$}
931 \caption{Rules for the extended STLC. Only the new features are shown, all the
932 rules and syntax for the STLC apply here too.}
936 Tagged unions (or sums, or coproducts---$\mysum$ here, \texttt{Either}
937 in Haskell) correspond to disjunctions, and dually tuples (or pairs, or
938 products---$\myprod$ here, tuples in Haskell) correspond to
939 conjunctions. This is apparent looking at the ways to construct and
940 destruct the values inhabiting those types: for $\mysum$ $\myleft{ }$
941 and $\myright{ }$ correspond to $\vee$ introduction, and
942 $\mycase{\myarg}{\myarg}$ to $\vee$ elimination; for $\myprod$
943 $\mypair{\myarg}{\myarg}$ corresponds to $\wedge$ introduction, $\myfst$
944 and $\mysnd$ to $\wedge$ elimination.
946 The trivial type $\myunit$ corresponds to the logical $\top$ (true), and
947 dually $\myempty$ corresponds to the logical $\bot$ (false). $\myunit$
948 has one introduction rule ($\mytt$), and thus one inhabitant; and no
949 eliminators. $\myempty$ has no introduction rules, and thus no
950 inhabitants; and one eliminator ($\myabsurd{ }$), corresponding to the
951 logical \emph{ex falso quodlibet}.
953 With these rules, our STLC now looks remarkably similar in power and use to the
954 natural deduction we already know.
955 \begin{mydef}[Negation]
956 $\myneg \mytya$ can be expressed as $\mytya \myarr \myempty$.
958 However, there is an important omission: there is no term of
959 the type $\mytya \mysum \myneg \mytya$ (excluded middle), or equivalently
960 $\myneg \myneg \mytya \myarr \mytya$ (double negation), or indeed any term with
961 a type equivalent to those.
963 This has a considerable effect on our logic and it is no coincidence, since there
964 is no obvious computational behaviour for laws like the excluded middle.
965 Logics of this kind are called \emph{intuitionistic}, or \emph{constructive},
966 and all the systems analysed will have this characteristic since they build on
967 the foundation of the STLC.\footnote{There is research to give computational
968 behaviour to classical logic, but I will not touch those subjects.}
970 As in logic, if we want to keep our system consistent, we must make sure that no
971 closed terms (in other words terms not under a $\lambda$) inhabit $\myempty$.
972 The variant of STLC presented here is indeed
973 consistent, a result that follows from the fact that it is
975 Going back to our $\mysyn{fix}$ combinator, it is easy to see how it ruins our
976 desire for consistency. The following term works for every type $\mytya$,
978 \[(\myfix{\myb{x}}{\mytya}{\myb{x}}) : \mytya\]
980 \subsection{Inductive data}
983 To make the STLC more useful as a programming language or reasoning tool it is
984 common to include (or let the user define) inductive data types. These comprise
985 of a type former, various constructors, and an eliminator (or destructor) that
986 serves as primitive recursor.
988 \begin{mydef}[Finite lists for the STLC]
989 We add a $\mylist$ type constructor, along with an `empty
990 list' ($\mynil{ }$) and `cons cell' ($\mycons$) constructor. The eliminator for
991 lists will be the usual folding operation ($\myfoldr$). Full rules in Figure
998 \begin{array}{r@{\ }c@{\ }l}
999 \mytmsyn & ::= & \cdots \mysynsep \mynil{\mytysyn} \mysynsep \mytmsyn \mycons \mytmsyn
1001 \myapp{\myapp{\myapp{\myfoldr}{\mytmsyn}}{\mytmsyn}}{\mytmsyn} \\
1002 \mytysyn & ::= & \cdots \mysynsep \myapp{\mylist}{\mytysyn}
1006 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
1008 \begin{array}{l@{\ }c@{\ }l}
1009 \myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{\mynil{\mytya}} & \myred & \mytmt \\
1011 \myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{(\mytmm \mycons \mytmn)} & \myred &
1012 \myapp{\myapp{\myse{f}}{\mytmm}}{(\myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{\mytmn})}
1016 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
1018 \AxiomC{\phantom{$\myjud{\mytmm}{\mytya}$}}
1019 \UnaryInfC{$\myjud{\mynil{\mytya}}{\myapp{\mylist}{\mytya}}$}
1022 \AxiomC{$\myjud{\mytmm}{\mytya}$}
1023 \AxiomC{$\myjud{\mytmn}{\myapp{\mylist}{\mytya}}$}
1024 \BinaryInfC{$\myjud{\mytmm \mycons \mytmn}{\myapp{\mylist}{\mytya}}$}
1029 \AxiomC{$\myjud{\mysynel{f}}{\mytya \myarr \mytyb \myarr \mytyb}$}
1030 \AxiomC{$\myjud{\mytmm}{\mytyb}$}
1031 \AxiomC{$\myjud{\mytmn}{\myapp{\mylist}{\mytya}}$}
1032 \TrinaryInfC{$\myjud{\myapp{\myapp{\myapp{\myfoldr}{\mysynel{f}}}{\mytmm}}{\mytmn}}{\mytyb}$}
1035 \caption{Rules for lists in the STLC.}
1039 In Section \ref{sec:well-order} we will see how to give a general account of
1042 \section{Intuitionistic Type Theory}
1045 \epigraph{\emph{Martin-L{\"o}f's type theory is a well established and
1046 convenient arena in which computational Christians are regularly
1047 fed to logical lions.}}{Conor McBride}
1049 \subsection{Extending the STLC}
1051 \cite{Barendregt1991} succinctly expressed geometrically how we can add
1052 expressivity to the STLC:
1054 \xymatrix@!0@=1.5cm{
1055 & \lambda\omega \ar@{-}[rr]\ar@{-}'[d][dd]
1056 & & \lambda C \ar@{-}[dd]
1058 \lambda2 \ar@{-}[ur]\ar@{-}[rr]\ar@{-}[dd]
1059 & & \lambda P2 \ar@{-}[ur]\ar@{-}[dd]
1061 & \lambda\underline\omega \ar@{-}'[r][rr]
1062 & & \lambda P\underline\omega
1064 \lambda{\to} \ar@{-}[rr]\ar@{-}[ur]
1065 & & \lambda P \ar@{-}[ur]
1068 Here $\lambda{\to}$, in the bottom left, is the STLC. From there can move along
1071 \item[Terms depending on types (towards $\lambda{2}$)] We can quantify over
1072 types in our type signatures. For example, we can define a polymorphic
1073 identity function, where $\mytyp$ denotes the `type of types':
1075 (\myabss{\myb{A}}{\mytyp}{\myabss{\myb{x}}{\myb{A}}{\myb{x}}}) : (\myb{A} {:} \mytyp) \myarr \myb{A} \myarr \myb{A}
1077 The first and most famous instance of this idea has been System F.
1078 This form of polymorphism and has been wildly successful, also thanks
1079 to a well known inference algorithm for a restricted version of System
1080 F known as Hindley-Milner \citep{milner1978theory}. Languages like
1081 Haskell and SML are based on this discipline.
1082 \item[Types depending on types (towards $\lambda{\underline{\omega}}$)] We have
1083 type operators. For example we could define a function that given types $R$
1084 and $\mytya$ forms the type that represents a value of type $\mytya$ in
1085 continuation passing style:
1086 \[\displaystyle(\myabss{\myb{A} \myar \myb{R}}{\mytyp}{(\myb{A}
1087 \myarr \myb{R}) \myarr \myb{R}}) : \mytyp \myarr \mytyp \myarr \mytyp
1089 \item[Types depending on terms (towards $\lambda{P}$)] Also known as `dependent
1090 types', give great expressive power. For example, we can have values of whose
1091 type depend on a boolean:
1092 \[\displaystyle(\myabss{\myb{x}}{\mybool}{\myite{\myb{x}}{\mynat}{\myrat}}) : \mybool
1096 All the systems preserve the properties that make the STLC well behaved. The
1097 system we are going to focus on, Intuitionistic Type Theory, has all of the
1098 above additions, and thus would sit where $\lambda{C}$ sits in the
1099 `$\lambda$-cube'. It will serve as the logical `core' of all the other
1100 extensions that we will present and ultimately our implementation of a similar
1103 \subsection{A Bit of History}
1105 Logic frameworks and programming languages based on type theory have a
1106 long history. Per Martin-L\"{o}f described the first version of his
1107 theory in 1971, but then revised it since the original version was
1108 inconsistent due to its impredicativity.\footnote{In the early version
1109 there was only one universe $\mytyp$ and $\mytyp : \mytyp$; see
1110 Section \ref{sec:term-types} for an explanation on why this causes
1111 problems.} For this reason he later gave a revised and consistent
1112 definition \citep{Martin-Lof1984}.
1114 A related development is the polymorphic $\lambda$-calculus, and specifically
1115 the previously mentioned System F, which was developed independently by Girard
1116 and Reynolds. An overview can be found in \citep{Reynolds1994}. The surprising
1117 fact is that while System F is impredicative it is still consistent and strongly
1118 normalising. \cite{Coquand1986} further extended this line of work with the
1119 Calculus of Constructions (CoC).
1121 Most widely used interactive theorem provers are based on ITT. Popular
1122 ones include Agda \citep{Norell2007}, Coq \citep{Coq}, Epigram
1123 \citep{McBride2004, EpigramTut}, Isabelle \citep{Paulson1990}, and many
1126 \subsection{A simple type theory}
1129 The calculus I present follows the exposition in \cite{Thompson1991},
1130 and is quite close to the original formulation of
1131 \citep{Martin-Lof1984}. Agda and \mykant\ renditions of the presented
1132 theory and all the examples is reproduced in Appendix
1134 \begin{mydef}[Intuitionistic Type Theory (ITT)]
1135 The syntax and reduction rules are shown in Figure \ref{fig:core-tt-syn}.
1136 The typing rules are presented piece by piece in the following sections.
1142 \begin{array}{r@{\ }c@{\ }l}
1143 \mytmsyn & ::= & \myb{x} \mysynsep
1144 \mytyp_{level} \mysynsep
1145 \myunit \mysynsep \mytt \mysynsep
1146 \myempty \mysynsep \myapp{\myabsurd{\mytmsyn}}{\mytmsyn} \\
1147 & | & \mybool \mysynsep \mytrue \mysynsep \myfalse \mysynsep
1148 \myitee{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
1149 & | & \myfora{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
1150 \myabss{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
1151 (\myapp{\mytmsyn}{\mytmsyn}) \\
1152 & | & \myexi{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
1153 \mypairr{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn} \\
1154 & | & \myapp{\myfst}{\mytmsyn} \mysynsep \myapp{\mysnd}{\mytmsyn} \\
1155 & | & \myw{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
1156 \mytmsyn \mynode{\myb{x}}{\mytmsyn} \mytmsyn \\
1157 & | & \myrec{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn} \\
1158 level & \in & \mathbb{N}
1163 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
1164 \begin{tabular}{ccc}
1166 \begin{array}{l@{ }l@{\ }c@{\ }l}
1167 \myitee{\mytrue &}{\myb{x}}{\myse{P}}{\mytmm}{\mytmn} & \myred & \mytmm \\
1168 \myitee{\myfalse &}{\myb{x}}{\myse{P}}{\mytmm}{\mytmn} & \myred & \mytmn \\
1173 \myapp{(\myabss{\myb{x}}{\mytya}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{\myb{x}}{\mytmn}
1177 \begin{array}{l@{ }l@{\ }c@{\ }l}
1178 \myapp{\myfst &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmm \\
1179 \myapp{\mysnd &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmn
1187 \myrec{(\myse{s} \mynode{\myb{x}}{\myse{T}} \myse{f})}{\myb{y}}{\myse{P}}{\myse{p}} \myred
1188 \myapp{\myapp{\myapp{\myse{p}}{\myse{s}}}{\myse{f}}}{(\myabss{\myb{t}}{\mysub{\myse{T}}{\myb{x}}{\myse{s}}}{
1189 \myrec{\myapp{\myse{f}}{\myb{t}}}{\myb{y}}{\myse{P}}{\mytmt}
1193 \caption{Syntax and reduction rules for our type theory.}
1194 \label{fig:core-tt-syn}
1197 \subsubsection{Types are terms, some terms are types}
1198 \label{sec:term-types}
1200 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1202 \AxiomC{$\myjud{\mytmt}{\mytya}$}
1203 \AxiomC{$\mytya \mydefeq \mytyb$}
1204 \BinaryInfC{$\myjud{\mytmt}{\mytyb}$}
1207 \AxiomC{\phantom{$\myjud{\mytmt}{\mytya}$}}
1208 \UnaryInfC{$\myjud{\mytyp_l}{\mytyp_{l + 1}}$}
1213 The first thing to notice is that a barrier between values and types that we had
1214 in the STLC is gone: values can appear in types, and the two are treated
1215 uniformly in the syntax.
1217 While the usefulness of doing this will become clear soon, a consequence is
1218 that since types can be the result of computation, deciding type equality is
1219 not immediate as in the STLC.
1220 \begin{mydef}[Definitional equality]
1221 We define \emph{definitional
1222 equality}, $\mydefeq$, as the congruence relation extending
1223 $\myred$. Moreover, when comparing types syntactically we do it up to
1224 renaming of bound names ($\alpha$-renaming)
1226 For example under this discipline we will find that
1229 \myabss{\myb{x}}{\mytya}{\myb{x}} \mydefeq \myabss{\myb{y}}{\mytya}{\myb{y}} \\
1230 \myapp{(\myabss{\myb{f}}{\mytya \myarr \mytya}{\myb{f}})}{(\myabss{\myb{y}}{\mytya}{\myb{y}})} \mydefeq \myabss{\myb{quux}}{\mytya}{\myb{quux}}
1233 Types that are definitionally equal can be used interchangeably. Here
1234 the `conversion' rule is not syntax directed, but it is possible to
1235 employ $\myred$ to decide term equality in a systematic way, comparing
1236 terms by reducing to their normal forms and then comparing them
1237 syntactically; so that a separate conversion rule is not needed.
1238 Another thing to notice is that, considering the need to reduce terms to
1239 decide equality, for type checking to be decidable a dependently typed
1240 must be terminating and confluent; since every type needs to have a
1241 unique normal form for definitional equality to be decidable.
1243 Moreover, we specify a \emph{type hierarchy} to talk about `large'
1244 types: $\mytyp_0$ will be the type of types inhabited by data:
1245 $\mybool$, $\mynat$, $\mylist$, etc. $\mytyp_1$ will be the type of
1246 $\mytyp_0$, and so on---for example we have $\mytrue : \mybool :
1247 \mytyp_0 : \mytyp_1 : \cdots$. Each type `level' is often called a
1248 universe in the literature. While it is possible to simplify things by
1249 having only one universe $\mytyp$ with $\mytyp : \mytyp$, this plan is
1250 inconsistent for much the same reason that impredicative na\"{\i}ve set
1251 theory is \citep{Hurkens1995}. However various techniques can be
1252 employed to lift the burden of explicitly handling universes, as we will
1253 see in Section \ref{sec:term-hierarchy}.
1255 \subsubsection{Contexts}
1257 \begin{minipage}{0.5\textwidth}
1258 \mydesc{context validity:}{\myvalid{\myctx}}{
1260 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
1261 \UnaryInfC{$\myvalid{\myemptyctx}$}
1264 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
1265 \UnaryInfC{$\myvalid{\myctx ; \myb{x} : \mytya}$}
1270 \begin{minipage}{0.5\textwidth}
1271 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1272 \AxiomC{$\myctx(x) = \mytya$}
1273 \UnaryInfC{$\myjud{\myb{x}}{\mytya}$}
1279 We need to refine the notion context to make sure that every variable appearing
1280 is typed correctly, or that in other words each type appearing in the context is
1281 indeed a type and not a value. In every other rule, if no premises are present,
1282 we assume the context in the conclusion to be valid.
1284 Then we can re-introduce the old rule to get the type of a variable for a
1287 \subsubsection{$\myunit$, $\myempty$}
1289 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1290 \begin{tabular}{ccc}
1291 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
1292 \UnaryInfC{$\myjud{\myunit}{\mytyp_0}$}
1294 \UnaryInfC{$\myjud{\myempty}{\mytyp_0}$}
1297 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
1298 \UnaryInfC{$\myjud{\mytt}{\myunit}$}
1300 \UnaryInfC{\phantom{$\myjud{\myempty}{\mytyp_0}$}}
1303 \AxiomC{$\myjud{\mytmt}{\myempty}$}
1304 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
1305 \BinaryInfC{$\myjud{\myapp{\myabsurd{\mytya}}{\mytmt}}{\mytya}$}
1307 \UnaryInfC{\phantom{$\myjud{\myempty}{\mytyp_0}$}}
1312 Nothing surprising here: $\myunit$ and $\myempty$ are unchanged from the STLC,
1313 with the added rules to type $\myunit$ and $\myempty$ themselves, and to make
1314 sure that we are invoking $\myabsurd{}$ over a type.
1316 \subsubsection{$\mybool$, and dependent $\myfun{if}$}
1318 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1319 \begin{tabular}{ccc}
1321 \UnaryInfC{$\myjud{\mybool}{\mytyp_0}$}
1325 \UnaryInfC{$\myjud{\mytrue}{\mybool}$}
1329 \UnaryInfC{$\myjud{\myfalse}{\mybool}$}
1334 \AxiomC{$\myjud{\mytmt}{\mybool}$}
1335 \AxiomC{$\myjudd{\myctx : \mybool}{\mytya}{\mytyp_l}$}
1337 \BinaryInfC{$\myjud{\mytmm}{\mysub{\mytya}{x}{\mytrue}}$ \hspace{0.7cm} $\myjud{\mytmn}{\mysub{\mytya}{x}{\myfalse}}$}
1338 \UnaryInfC{$\myjud{\myitee{\mytmt}{\myb{x}}{\mytya}{\mytmm}{\mytmn}}{\mysub{\mytya}{\myb{x}}{\mytmt}}$}
1342 With booleans we get the first taste of the `dependent' in `dependent
1343 types'. While the two introduction rules for $\mytrue$ and $\myfalse$
1344 are not surprising, the typing rules for $\myfun{if}$ are. In most
1345 strongly typed languages we expect the branches of an $\myfun{if}$
1346 statements to be of the same type, to preserve subject reduction, since
1347 execution could take both paths. This is a pity, since the type system
1348 does not reflect the fact that in each branch we gain knowledge on the
1349 term we are branching on. Which means that programs along the lines of
1351 if null xs then head xs else 0
1353 are a necessary, well-typed, danger.
1355 However, in a more expressive system, we can do better: the branches' type can
1356 depend on the value of the scrutinised boolean. This is what the typing rule
1357 expresses: the user provides a type $\mytya$ ranging over an $\myb{x}$
1358 representing the scrutinised boolean type, and the branches are type checked with
1359 the updated knowledge of the value of $\myb{x}$.
1361 \subsubsection{$\myarr$, or dependent function}
1364 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1365 \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
1366 \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
1367 \BinaryInfC{$\myjud{\myfora{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
1373 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytmt}{\mytyb}$}
1374 \UnaryInfC{$\myjud{\myabss{\myb{x}}{\mytya}{\mytmt}}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
1377 \AxiomC{$\myjud{\mytmm}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
1378 \AxiomC{$\myjud{\mytmn}{\mytya}$}
1379 \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mysub{\mytyb}{\myb{x}}{\mytmn}}$}
1384 Dependent functions are one of the two key features that characterise
1385 dependent types---the other being dependent products. With dependent
1386 functions, the result type can depend on the value of the argument.
1387 This feature, together with the fact that the result type might be a
1388 type itself, brings a lot of interesting possibilities. In the
1389 introduction rule, the return type is type checked in a context with an
1390 abstracted variable of domain's type; and in the elimination rule the
1391 actual argument is substituted in the return type. Keeping the
1392 correspondence with logic alive, dependent functions are much like
1393 universal quantifiers ($\forall$) in logic.
1395 For example, assuming that we have lists and natural numbers in our
1396 language, using dependent functions we can write functions of types
1399 \myfun{length} : (\myb{A} {:} \mytyp_0) \myarr \myapp{\mylist}{\myb{A}} \myarr \mynat \\
1400 \myarg \myfun{$>$} \myarg : \mynat \myarr \mynat \myarr \mytyp_0 \\
1401 \myfun{head} : (\myb{A} {:} \mytyp_0) \myarr (\myb{l} {:} \myapp{\mylist}{\myb{A}})
1402 \myarr \myapp{\myapp{\myfun{length}}{\myb{A}}}{\myb{l}} \mathrel{\myfun{$>$}} 0 \myarr
1407 \myfun{length} is the usual polymorphic length
1408 function. $\myarg\myfun{$>$}\myarg$ is a function that takes two naturals
1409 and returns a type: if the lhs is greater then the rhs, $\myunit$ is
1410 returned, $\myempty$ otherwise. This way, we can express a
1411 `non-emptiness' condition in $\myfun{head}$, by including a proof that
1412 the length of the list argument is non-zero. This allows us to rule out
1413 the `empty list' case, so that we can safely return the first element.
1415 Again, we need to make sure that the type hierarchy is respected, which
1416 is the reason why a type formed by $\myarr$ will live in the least upper
1417 bound of the levels of argument and return type.
1419 \subsubsection{$\myprod$, or dependent product}
1422 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1423 \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
1424 \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
1425 \BinaryInfC{$\myjud{\myexi{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
1431 \AxiomC{$\myjud{\mytmm}{\mytya}$}
1432 \AxiomC{$\myjud{\mytmn}{\mysub{\mytyb}{\myb{x}}{\mytmm}}$}
1433 \BinaryInfC{$\myjud{\mypairr{\mytmm}{\myb{x}}{\mytyb}{\mytmn}}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
1435 \UnaryInfC{\phantom{$--$}}
1438 \AxiomC{$\myjud{\mytmt}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
1439 \UnaryInfC{$\hspace{0.7cm}\myjud{\myapp{\myfst}{\mytmt}}{\mytya}\hspace{0.7cm}$}
1441 \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mysub{\mytyb}{\myb{x}}{\myapp{\myfst}{\mytmt}}}$}
1446 If dependent functions are a generalisation of $\myarr$ in the STLC,
1447 dependent products are a generalisation of $\myprod$ in the STLC. The
1448 improvement is that the second element's type can depend on the value of
1449 the first element. The correspondence with logic is through the
1450 existential quantifier: $\exists x \in \mathbb{N}. even(x)$ can be
1451 expressed as $\myexi{\myb{x}}{\mynat}{\myapp{\myfun{even}}{\myb{x}}}$.
1452 The first element will be a number, and the second evidence that the
1453 number is even. This highlights the fact that we are working in a
1454 constructive logic: if we have an existence proof, we can always ask for
1455 a witness. This means, for instance, that $\neg \forall \neg$ is not
1456 equivalent to $\exists$.
1458 Another perhaps more `dependent' application of products, paired with
1459 $\mybool$, is to offer choice between different types. For example we
1460 can easily recover disjunctions:
1463 \myarg\myfun{$\vee$}\myarg : \mytyp_0 \myarr \mytyp_0 \myarr \mytyp_0 \\
1464 \myb{A} \mathrel{\myfun{$\vee$}} \myb{B} \mapsto \myexi{\myb{x}}{\mybool}{\myite{\myb{x}}{\myb{A}}{\myb{B}}} \\ \ \\
1465 \myfun{case} : (\myb{A}\ \myb{B}\ \myb{C} {:} \mytyp_0) \myarr (\myb{A} \myarr \myb{C}) \myarr (\myb{B} \myarr \myb{C}) \myarr \myb{A} \mathrel{\myfun{$\vee$}} \myb{B} \myarr \myb{C} \\
1466 \myfun{case} \myappsp \myb{A} \myappsp \myb{B} \myappsp \myb{C} \myappsp \myb{f} \myappsp \myb{g} \myappsp \myb{x} \mapsto \\
1467 \myind{2} \myapp{(\myitee{\myapp{\myfst}{\myb{x}}}{\myb{b}}{(\myite{\myb{b}}{\myb{A}}{\myb{B}})}{\myb{f}}{\myb{g}})}{(\myapp{\mysnd}{\myb{x}})}
1471 \subsubsection{$\mytyc{W}$, or well-order}
1472 \label{sec:well-order}
1474 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1476 \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
1477 \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
1478 \BinaryInfC{$\myjud{\myw{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
1483 \AxiomC{$\myjud{\mytmt}{\mytya}$}
1484 \AxiomC{$\myjud{\mysynel{f}}{\mysub{\mytyb}{\myb{x}}{\mytmt} \myarr \myw{\myb{x}}{\mytya}{\mytyb}}$}
1485 \BinaryInfC{$\myjud{\mytmt \mynode{\myb{x}}{\mytyb} \myse{f}}{\myw{\myb{x}}{\mytya}{\mytyb}}$}
1491 \AxiomC{$\myjud{\myse{u}}{\myw{\myb{x}}{\myse{S}}{\myse{T}}}$}
1492 \AxiomC{$\myjudd{\myctx; \myb{w} : \myw{\myb{x}}{\myse{S}}{\myse{T}}}{\myse{P}}{\mytyp_l}$}
1494 \BinaryInfC{$\myjud{\myse{p}}{
1495 \myfora{\myb{s}}{\myse{S}}{\myfora{\myb{f}}{\mysub{\myse{T}}{\myb{x}}{\myse{s}} \myarr \myw{\myb{x}}{\myse{S}}{\myse{T}}}{(\myfora{\myb{t}}{\mysub{\myse{T}}{\myb{x}}{\myb{s}}}{\mysub{\myse{P}}{\myb{w}}{\myapp{\myb{f}}{\myb{t}}}}) \myarr \mysub{\myse{P}}{\myb{w}}{\myb{f}}}}
1497 \UnaryInfC{$\myjud{\myrec{\myse{u}}{\myb{w}}{\myse{P}}{\myse{p}}}{\mysub{\myse{P}}{\myb{w}}{\myse{u}}}$}
1501 Finally, the well-order type, or in short $\mytyc{W}$-type, which will
1502 let us represent inductive data in a general way. We can form `nodes'
1503 of the shape \[\mytmt \mynode{\myb{x}}{\mytyb} \myse{f} :
1504 \myw{\myb{x}}{\mytya}{\mytyb}\] where $\mytmt$ is of type $\mytya$ and
1505 is the data present in the node, and $\myse{f}$ specifies a `child' of
1506 the node for each member of $\mysub{\mytyb}{\myb{x}}{\mytmt}$.. The
1507 $\myfun{rec}\ \myfun{with}$ acts as an induction principle on
1508 $\mytyc{W}$, given a predicate and a function dealing with the inductive
1509 case---we will gain more intuition about inductive data in ITT in
1510 Section \ref{sec:user-type}.
1512 For example, if we want to form natural numbers, we can take
1515 \mytyc{Tr} : \mybool \myarr \mytyp_0 \\
1516 \mytyc{Tr} \myappsp \myb{b} \mapsto \myfun{if}\, \myb{b}\, \myfun{then}\, \myunit\, \myfun{else}\, \myempty \\
1518 \mynat : \mytyp_0 \\
1519 \mynat \mapsto \myw{\myb{b}}{\mybool}{(\mytyc{Tr}\myappsp\myb{b})}
1522 Each node will contain a boolean. If $\mytrue$, the number is non-zero,
1523 and we will have one child representing its predecessor, given that
1524 $\mytyc{Tr}$ will return $\myunit$. If $\myfalse$, the number is zero,
1525 and we will have no predecessors (children), given the $\myempty$:
1528 \mydc{zero} : \mynat \\
1529 \mydc{zero} \mapsto \myfalse \mynodee (\myabs{\myb{x}}{\myabsurd{\mynat} \myappsp \myb{x}}) \\
1531 \mydc{suc} : \mynat \myarr \mynat \\
1532 \mydc{suc}\myappsp \myb{x} \mapsto \mytrue \mynodee (\myabs{\myarg}{\myb{x}})
1535 And with a bit of effort, we can recover addition:
1538 \myfun{plus} : \mynat \myarr \mynat \myarr \mynat \\
1539 \myfun{plus} \myappsp \myb{x} \myappsp \myb{y} \mapsto \\
1540 \myind{2} \myfun{rec}\, \myb{x} / \myb{b}.\mynat \, \\
1541 \myind{2} \myfun{with}\, \myabs{\myb{b}}{\\
1542 \myind{2}\myind{2}\myfun{if}\, \myb{b} / \myb{b'}.((\mytyc{Tr} \myappsp \myb{b'} \myarr \mynat) \myarr (\mytyc{Tr} \myappsp \myb{b'} \myarr \mynat) \myarr \mynat) \\
1543 \myind{2}\myind{2}\myfun{then}\,(\myabs{\myarg\, \myb{f}}{\mydc{suc}\myappsp (\myapp{\myb{f}}{\mytt})})\, \myfun{else}\, (\myabs{\myarg\, \myarg}{\myb{y}})}
1546 Note how we explicitly have to type the branches to make them match
1547 with the definition of $\mynat$. This gives a taste of the
1548 clumsiness of $\mytyc{W}$-types but not the whole story: well-orders
1549 are inadequate not only because they are verbose, but also because the
1550 face deeper problems due to the weakness of the notion of equality
1551 present in most type theory (which we will present in the next
1552 section) \citep{dybjer1997representing}. The `better' equality we
1553 will present in Section \ref{sec:ott} helps but does not fully resolve
1554 these issues.\footnote{See \url{http://www.e-pig.org/epilogue/?p=324},
1555 which concludes with `W-types are a powerful conceptual tool, but
1556 they’re no basis for an implementation of recursive data types in
1557 decidable type theories.'} For this reasons \mytyc{W}-types have
1558 remained nothing more than a reasoning tool, and practical systems
1559 implement more expressive ways to represent data.
1561 \section{The struggle for equality}
1562 \label{sec:equality}
1564 \epigraph{\emph{Half of my time spent doing research involves thinking up clever
1565 schemes to avoid needing functional extensionality.}}{@larrytheliquid}
1567 In the previous section we learnt how a type checker for ITT needs
1568 a notion of \emph{definitional equality}. Beyond this meta-theoretic
1569 notion, in this section we will explore the ways of expressing equality
1570 \emph{inside} the theory, as a reasoning tool available to the user.
1571 This area is the main concern of this thesis, and in general a very
1572 active research topic, since we do not have a fully satisfactory
1573 solution, yet. As in the previous section, everything presented is
1574 formalised in Agda in Appendix \ref{app:agda-itt}.
1576 \subsection{Propositional equality}
1578 \begin{mydef}[Propositional equality] The syntax, reduction, and typing
1579 rules for propositional equality and related constructs are defined
1584 \begin{minipage}{0.5\textwidth}
1587 \begin{array}{r@{\ }c@{\ }l}
1588 \mytmsyn & ::= & \cdots \\
1589 & | & \mypeq \myappsp \mytmsyn \myappsp \mytmsyn \myappsp \mytmsyn \mysynsep
1590 \myapp{\myrefl}{\mytmsyn} \\
1591 & | & \myjeq{\mytmsyn}{\mytmsyn}{\mytmsyn}
1596 \begin{minipage}{0.5\textwidth}
1597 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
1599 \myjeq{\myse{P}}{(\myapp{\myrefl}{\mytmm})}{\mytmn} \myred \mytmn
1605 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1606 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
1607 \AxiomC{$\myjud{\mytmm}{\mytya}$}
1608 \AxiomC{$\myjud{\mytmn}{\mytya}$}
1609 \TrinaryInfC{$\myjud{\mypeq \myappsp \mytya \myappsp \mytmm \myappsp \mytmn}{\mytyp_l}$}
1615 \AxiomC{$\begin{array}{c}\ \\\myjud{\mytmm}{\mytya}\hspace{1.1cm}\mytmm \mydefeq \mytmn\end{array}$}
1616 \UnaryInfC{$\myjud{\myapp{\myrefl}{\mytmm}}{\mypeq \myappsp \mytya \myappsp \mytmm \myappsp \mytmn}$}
1621 \myjud{\myse{P}}{\myfora{\myb{x}\ \myb{y}}{\mytya}{\myfora{q}{\mypeq \myappsp \mytya \myappsp \myb{x} \myappsp \myb{y}}{\mytyp_l}}} \\
1622 \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})}}
1625 \UnaryInfC{$\myjud{\myjeq{\myse{P}}{\myse{q}}{\myse{p}}}{\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmn}}{q}}$}
1630 To express equality between two terms inside ITT, the obvious way to do
1631 so is to have equality to be a type. Here we present what has survived
1632 as the dominating form of equality in systems based on ITT up since
1633 \cite{Martin-Lof1984} up to the present day.
1635 Our type former is $\mypeq$, which given a type relates equal terms of
1636 that type. $\mypeq$ has one introduction rule, $\myrefl$, which
1637 introduces an equality relation between definitionally equal terms.
1639 Finally, we have one eliminator for $\mypeq$ (also known as `\myfun{J}
1640 axiom' in the literature), $\myjeqq$.
1641 $\myjeq{\myse{P}}{\myse{q}}{\myse{p}}$ takes
1643 \item $\myse{P}$, a predicate working with two terms of a certain type (say
1644 $\mytya$) and a proof of their equality;
1645 \item $\myse{q}$, a proof that two terms in $\mytya$ (say $\myse{m}$ and
1646 $\myse{n}$) are equal;
1647 \item and $\myse{p}$, an inhabitant of $\myse{P}$ applied to $\myse{m}$
1648 twice, plus the trivial proof by reflexivity showing that $\myse{m}$
1651 Given these ingredients, $\myjeqq$ returns a member of $\myse{P}$ applied
1652 to $\mytmm$, $\mytmn$, and $\myse{q}$. In other words $\myjeqq$ takes a
1653 witness that $\myse{P}$ works with \emph{definitionally equal} terms,
1654 and returns a witness of $\myse{P}$ working with \emph{propositionally
1655 equal} terms. Invocations of $\myjeqq$ will vanish when the equality
1656 proofs will reduce to invocations to reflexivity, at which point the
1657 arguments must be definitionally equal, and thus the provided
1658 $\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmm}}{(\myapp{\myrefl}{\mytmm})}$
1659 can be returned. This means that $\myjeqq$ will not compute with
1660 hypothetical proofs, which makes sense given that they might be false.
1662 While the $\myjeqq$ rule is slightly convoluted, we can derive many more
1663 `friendly' rules from it, for example a more obvious `substitution' rule, that
1664 replaces equal for equal in predicates:
1667 \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}}}}} \\
1668 \myfun{subst}\myappsp \myb{A}\myappsp\myb{P}\myappsp\myb{x}\myappsp\myb{y}\myappsp\myb{q}\myappsp\myb{p} \mapsto
1669 \myjeq{(\myabs{\myb{x}\ \myb{y}\ \myb{q}}{\myapp{\myb{P}}{\myb{y}}})}{\myb{p}}{\myb{q}}
1672 Once we have $\myfun{subst}$, we can easily prove more familiar laws regarding
1673 equality, such as symmetry, transitivity, congruence laws, etc.
1675 \subsection{Common extensions}
1677 Our definitional and propositional equalities can be enhanced in various
1678 ways. Obviously if we extend the definitional equality we are also
1679 automatically extend propositional equality, given how $\myrefl$ works.
1681 \subsubsection{$\eta$-expansion}
1682 \label{sec:eta-expand}
1684 A simple extension to our definitional equality is $\eta$-expansion.
1685 Given an abstract variable $\myb{f} : \mytya \myarr \mytyb$ the aim is
1686 to have that $\myb{f} \mydefeq
1687 \myabss{\myb{x}}{\mytya}{\myapp{\myb{f}}{\myb{x}}}$. We can achieve
1688 this by `expanding' terms depending on their types, a process known as
1689 \emph{quotation}---a term borrowed from the practice of
1690 \emph{normalisation by evaluation}, where we embed terms in some host
1691 language with an existing notion of computation, and then reify them
1692 back into terms, which will `smooth out' differences like the one above
1695 The same concept applies to $\myprod$, where we expand each inhabitant
1696 by reconstructing it by getting its projections, so that $\myb{x}
1697 \mydefeq \mypair{\myfst \myappsp \myb{x}}{\mysnd \myappsp \myb{x}}$.
1698 Similarly, all one inhabitants of $\myunit$ and all zero inhabitants of
1699 $\myempty$ can be considered equal. Quotation can be performed in a
1700 type-directed way, as we will witness in Section \ref{sec:kant-irr}.
1702 \begin{mydef}[Congruence and $\eta$-laws]
1703 To justify quotation in our type system we add a congruence law for
1704 abstractions and a similar law for products, plus the fact that all
1705 elements of $\myunit$ or $\myempty$ are equal.
1708 \mydesc{definitional equality:}{\myjud{\mytmm \mydefeq \mytmn}{\mytmsyn}}{
1710 \AxiomC{$\myjudd{\myctx; \myb{y} : \mytya}{\myapp{\myse{f}}{\myb{x}} \mydefeq \myapp{\myse{g}}{\myb{x}}}{\mysub{\mytyb}{\myb{x}}{\myb{y}}}$}
1711 \UnaryInfC{$\myjud{\myse{f} \mydefeq \myse{g}}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
1714 \AxiomC{$\myjud{\mypair{\myapp{\myfst}{\mytmm}}{\myapp{\mysnd}{\mytmm}} \mydefeq \mypair{\myapp{\myfst}{\mytmn}}{\myapp{\mysnd}{\mytmn}}}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
1715 \UnaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
1722 \AxiomC{$\myjud{\mytmm}{\myunit}$}
1723 \AxiomC{$\myjud{\mytmn}{\myunit}$}
1724 \BinaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\myunit}$}
1727 \AxiomC{$\myjud{\mytmm}{\myempty}$}
1728 \AxiomC{$\myjud{\mytmn}{\myempty}$}
1729 \BinaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\myempty}$}
1734 \subsubsection{Uniqueness of identity proofs}
1736 Another common but controversial addition to propositional equality is
1737 the $\myfun{K}$ axiom, which essentially states that all equality proofs
1740 \begin{mydef}[$\myfun{K}$ axiom]\end{mydef}
1741 \mydesc{typing:}{\myjud{\mytmm \mydefeq \mytmn}{\mytmsyn}}{
1744 \myjud{\myse{P}}{\myfora{\myb{x}}{\mytya}{\mypeq \myappsp \mytya \myappsp \myb{x}\myappsp \myb{x} \myarr \mytyp}} \\\
1745 \myjud{\mytmt}{\mytya} \hspace{1cm}
1746 \myjud{\myse{p}}{\myse{P} \myappsp \mytmt \myappsp (\myrefl \myappsp \mytmt)} \hspace{1cm}
1747 \myjud{\myse{q}}{\mytmt \mypeq{\mytya} \mytmt}
1750 \UnaryInfC{$\myjud{\myfun{K} \myappsp \myse{P} \myappsp \myse{t} \myappsp \myse{p} \myappsp \myse{q}}{\myse{P} \myappsp \mytmt \myappsp \myse{q}}$}
1754 \cite{Hofmann1994} showed that $\myfun{K}$ is not derivable from
1755 $\myjeqq$, and \cite{McBride2004} showed that it is needed to implement
1756 `dependent pattern matching', as first proposed by \cite{Coquand1992}.
1757 Thus, $\myfun{K}$ is derivable in the systems that implement dependent
1758 pattern matching, such as Epigram and Agda; but for example not in Coq.
1760 $\myfun{K}$ is controversial mainly because it is at odds with
1761 equalities that include computational behaviour, most notably
1762 Voevodsky's \emph{Univalent Foundations}, which feature a \emph{univalence}
1763 axiom that identifies isomorphisms between types with propositional
1764 equality. For example we would have two isomorphisms, and thus two
1765 equalities, between $\mybool$ and $\mybool$, corresponding to the two
1766 permutations---one is the identity, and one swaps the elements. Given
1767 this, $\myfun{K}$ and univalence are inconsistent, and thus a form of
1768 dependent pattern matching that does not imply $\myfun{K}$ is subject of
1769 research.\footnote{More information about univalence can be found at
1770 \url{http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations.html}.}
1772 \subsection{Limitations}
1774 Propositional equality as described is quite restricted when
1775 reasoning about equality beyond the term structure, which is what definitional
1776 equality gives us (extensions notwithstanding).
1778 The problem is best exemplified by \emph{function extensionality}. In
1779 mathematics, we would expect to be able to treat functions that give
1780 equal output for equal input as equal. When reasoning in a mechanised
1781 framework we ought to be able to do the same: in the end, without
1782 considering the operational behaviour, all functions equal extensionally
1783 are going to be replaceable with one another.
1785 However this is not the case, or in other words with the tools we have we have
1788 \myfun{ext} : \myfora{\myb{A}\ \myb{B}}{\mytyp}{\myfora{\myb{f}\ \myb{g}}{
1789 \myb{A} \myarr \myb{B}}{
1790 (\myfora{\myb{x}}{\myb{A}}{\mypeq \myappsp \myb{B} \myappsp (\myapp{\myb{f}}{\myb{x}}) \myappsp (\myapp{\myb{g}}{\myb{x}})}) \myarr
1791 \mypeq \myappsp (\myb{A} \myarr \myb{B}) \myappsp \myb{f} \myappsp \myb{g}
1795 To see why this is the case, consider the functions
1796 \[\myabs{\myb{x}}{0 \mathrel{\myfun{$+$}} \myb{x}}$ and $\myabs{\myb{x}}{\myb{x} \mathrel{\myfun{$+$}} 0}\]
1797 where $\myfun{$+$}$ is defined by recursion on the first argument,
1798 gradually destructing it to build up successors of the second argument.
1799 The two functions are clearly extensionally equal, and we can in fact
1802 \myfora{\myb{x}}{\mynat}{\mypeq \myappsp \mynat \myappsp (0 \mathrel{\myfun{$+$}} \myb{x}) \myappsp (\myb{x} \mathrel{\myfun{$+$}} 0)}
1804 By induction on $\mynat$ applied to $\myb{x}$. However, the two
1805 functions are not definitionally equal, and thus we won't be able to get
1806 rid of the quantification.
1808 For the reasons given above, theories that offer a propositional equality
1809 similar to what we presented are called \emph{intensional}, as opposed
1810 to \emph{extensional}. Most systems widely used today (such as Agda,
1811 Coq, and Epigram) are of this kind.
1813 This is quite an annoyance that often makes reasoning awkward or
1814 impossible to execute. For example, we might want to represent terms of
1815 some language in Agda and give their denotation by embedding them in
1816 Agda---if we had $\lambda$-terms, functions will become Agda functions,
1817 application will be Agda's function application, and so on. Then we
1818 would like to perform optimisation passes on the terms, and verify that
1819 they are sound by proving that the denotation of the optimised version
1820 is equal to the denotation of the starting term.
1822 But if the embedding uses functions---and it probably will---we are
1823 stuck with an equality that identifies as equal only syntactically equal
1824 functions! Since the point of optimising is about preserving the
1825 denotational but changing the operational behaviour of terms, our
1826 equality falls short of our needs. Moreover, the problem extends to
1827 other fields beyond functions, such as bisimulation between processes
1828 specified by coinduction, or in general proving equivalences based on
1829 the behaviour of a term.
1831 \subsection{Equality reflection}
1833 One way to `solve' this problem is by identifying propositional equality
1834 with definitional equality.
1836 \begin{mydef}[Equality reflection]\end{mydef}
1837 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1838 \AxiomC{$\myjud{\myse{q}}{\mypeq \myappsp \mytya \myappsp \mytmm \myappsp \mytmn}$}
1839 \UnaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\mytya}$}
1843 The \emph{equality reflection} rule is a very different rule from the
1844 ones we saw up to now: it links a typing judgement internal to the type
1845 theory to a meta-theoretic judgement that the type checker uses to work
1846 with terms. It is easy to see the dangerous consequences that this
1849 \item The rule is not syntax directed, and the type checker is
1850 presumably expected to come up with equality proofs when needed.
1851 \item More worryingly, type checking becomes undecidable also because
1852 computing under false assumptions becomes unsafe, since we derive any
1853 equality proof and then use equality reflection and the conversion
1854 rule to have terms of any type.
1857 Given these facts theories employing equality reflection, like NuPRL
1858 \citep{NuPRL}, carry the derivations that gave rise to each typing judgement
1859 to keep the systems manageable.
1861 For all its faults, equality reflection does allow us to prove extensionality,
1862 using the extensions we gave above. Assuming that $\myctx$ contains
1863 \[\myb{A}, \myb{B} : \mytyp; \myb{f}, \myb{g} : \myb{A} \myarr \myb{B}; \myb{q} : \myfora{\myb{x}}{\myb{A}}{\myapp{\myb{f}}{\myb{x}} \mypeq{} \myapp{\myb{g}}{\myb{x}}}\]
1867 \AxiomC{$\myjudd{\myctx; \myb{x} : \myb{A}}{\myb{q}}{\mypeq \myappsp \myb{A} \myappsp (\myapp{\myb{f}}{\myb{x}}) \myappsp (\myapp{\myb{g}}{\myb{x}})}$}
1868 \RightLabel{equality reflection}
1869 \UnaryInfC{$\myjudd{\myctx; \myb{x} : \myb{A}}{\myapp{\myb{f}}{\myb{x}} \mydefeq \myapp{\myb{g}}{\myb{x}}}{\myb{B}}$}
1870 \RightLabel{congruence for $\lambda$s}
1871 \UnaryInfC{$\myjud{(\myabs{\myb{x}}{\myapp{\myb{f}}{\myb{x}}}) \mydefeq (\myabs{\myb{x}}{\myapp{\myb{g}}{\myb{x}}})}{\myb{A} \myarr \myb{B}}$}
1872 \RightLabel{$\eta$-law for $\lambda$}
1873 \UnaryInfC{$\myjud{\myb{f} \mydefeq \myb{g}}{\myb{A} \myarr \myb{B}}$}
1874 \RightLabel{$\myrefl$}
1875 \UnaryInfC{$\myjud{\myapp{\myrefl}{\myb{f}}}{\mypeq \myappsp (\myb{A} \myarr \myb{B}) \myappsp \myb{f} \myappsp \myb{g}}$}
1878 For this reason, theories employing equality reflection are often
1879 grouped under the name of \emph{Extensional Type Theory} (ETT). Now,
1880 the question is: do we need to give up well-behavedness of our theory to
1881 gain extensionality?
1883 \section{The observational approach}
1886 A recent development by \citet{Altenkirch2007}, \emph{Observational Type
1887 Theory} (OTT), promises to keep the well behavedness of ITT while
1888 being able to gain many useful equality proofs,\footnote{It is suspected
1889 that OTT gains \emph{all} the equality proofs of ETT, but no proof
1890 exists yet.} including function extensionality. The main idea is to
1891 give the user the possibility to \emph{coerce} (or transport) values
1892 from a type $\mytya$ to a type $\mytyb$, if the type checker can prove
1893 structurally that $\mytya$ and $\mytyb$ are equal; and providing a
1894 value-level equality based on similar principles. Here we give an
1895 exposition which follows closely the original paper.
1897 \subsection{A simpler theory, a propositional fragment}
1899 \begin{mydef}[OTT's simple theory, with propositions]\ \end{mydef}
1902 $\mytyp_l$ is replaced by $\mytyp$. \\\ \\
1904 \begin{array}{r@{\ }c@{\ }l}
1905 \mytmsyn & ::= & \cdots \mysynsep \myprdec{\myprsyn} \mysynsep
1906 \myITE{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
1907 \myprsyn & ::= & \mybot \mysynsep \mytop \mysynsep \myprsyn \myand \myprsyn
1908 \mysynsep \myprfora{\myb{x}}{\mytmsyn}{\myprsyn}
1915 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
1917 \begin{array}{l@{}l@{\ }c@{\ }l}
1918 \myITE{\mytrue &}{\mytya}{\mytyb} & \myred & \mytya \\
1919 \myITE{\myfalse &}{\mytya}{\mytyb} & \myred & \mytyb
1926 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1928 \AxiomC{$\myjud{\myse{P}}{\myprop}$}
1929 \UnaryInfC{$\myjud{\myprdec{\myse{P}}}{\mytyp}$}
1932 \AxiomC{$\myjud{\mytmt}{\mybool}$}
1933 \AxiomC{$\myjud{\mytya}{\mytyp}$}
1934 \AxiomC{$\myjud{\mytyb}{\mytyp}$}
1935 \TrinaryInfC{$\myjud{\myITE{\mytmt}{\mytya}{\mytyb}}{\mytyp}$}
1942 \mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
1943 \begin{tabular}{ccc}
1944 \AxiomC{\phantom{$\myjud{\myse{P}}{\myprop}$}}
1945 \UnaryInfC{$\myjud{\mytop}{\myprop}$}
1947 \UnaryInfC{$\myjud{\mybot}{\myprop}$}
1950 \AxiomC{$\myjud{\myse{P}}{\myprop}$}
1951 \AxiomC{$\myjud{\myse{Q}}{\myprop}$}
1952 \BinaryInfC{$\myjud{\myse{P} \myand \myse{Q}}{\myprop}$}
1954 \UnaryInfC{\phantom{$\myjud{\mybot}{\myprop}$}}
1957 \AxiomC{$\myjud{\myse{A}}{\mytyp}$}
1958 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\myse{P}}{\myprop}$}
1959 \BinaryInfC{$\myjud{\myprfora{\myb{x}}{\mytya}{\myse{P}}}{\myprop}$}
1961 \UnaryInfC{\phantom{$\myjud{\mybot}{\myprop}$}}
1966 Our foundation will be a type theory like the one of Section
1967 \ref{sec:itt}, with only one level: $\mytyp_0$. In this context we will
1968 drop the $0$ and call $\mytyp_0$ $\mytyp$. Moreover, since the old
1969 $\myfun{if}\myarg\myfun{then}\myarg\myfun{else}$ was able to return
1970 types thanks to the hierarchy (which is gone), we need to reintroduce an
1971 ad-hoc conditional for types, where the reduction rule is the obvious
1974 However, we have an addition: a universe of \emph{propositions},
1975 $\myprop$. $\myprop$ isolates a fragment of types at large, and
1976 indeed we can `inject' any $\myprop$ back in $\mytyp$ with $\myprdec{\myarg}$.
1977 \begin{mydef}[Proposition decoding]\ \end{mydef}
1978 \mydesc{proposition decoding:}{\myprdec{\mytmsyn} \myred \mytmsyn}{
1981 \begin{array}{l@{\ }c@{\ }l}
1982 \myprdec{\mybot} & \myred & \myempty \\
1983 \myprdec{\mytop} & \myred & \myunit
1988 \begin{array}{r@{ }c@{ }l@{\ }c@{\ }l}
1989 \myprdec{&\myse{P} \myand \myse{Q} &} & \myred & \myprdec{\myse{P}} \myprod \myprdec{\myse{Q}} \\
1990 \myprdec{&\myprfora{\myb{x}}{\mytya}{\myse{P}} &} & \myred &
1991 \myfora{\myb{x}}{\mytya}{\myprdec{\myse{P}}}
1996 Propositions are what we call the types of \emph{proofs}, or types
1997 whose inhabitants contain no `data', much like $\myunit$. The goal
1998 when isolating \mytyc{Prop} is twofold: erasing all top-level
1999 propositions when compiling; and to identify all equivalent
2000 propositions as the same, as we will see later.
2002 Why did we choose what we have in $\myprop$? Given the above
2003 criteria, $\mytop$ obviously fits the bill, since it has one element.
2004 A pair of propositions $\myse{P} \myand \myse{Q}$ still won't get us
2005 data, since if they both have one element the only possible pair is
2006 the one formed by said elements. Finally, if $\myse{P}$ is a
2007 proposition and we have $\myprfora{\myb{x}}{\mytya}{\myse{P}}$, the
2008 decoding will be a constant function for propositional content. The
2009 only threat is $\mybot$, by which we can fabricate anything we want:
2010 however if we are consistent there will be no closed term of type
2011 $\mybot$ at, which is what we care about regarding proof erasure and
2014 As an example of types that are \emph{not} propositional, consider
2015 $\mydc{Bool}$eans, which are the quintessential `relevant' data, since
2016 they are often use to decide the execution path of a program through
2017 $\myfun{if}\myarg\myfun{then}\myarg\myfun{else}\myarg$ constructs.
2019 \subsection{Equality proofs}
2021 \begin{mydef}[Equality proofs and related operations]\ \end{mydef}
2025 \begin{array}{r@{\ }c@{\ }l}
2026 \mytmsyn & ::= & \cdots \mysynsep
2027 \mycoee{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \mysynsep
2028 \mycohh{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
2029 \myprsyn & ::= & \cdots \mysynsep \mytmsyn \myeq \mytmsyn \mysynsep
2030 \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn}
2035 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
2037 \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
2038 \AxiomC{$\myjud{\mytmt}{\mytya}$}
2039 \BinaryInfC{$\myjud{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}$}
2042 \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
2043 \AxiomC{$\myjud{\mytmt}{\mytya}$}
2044 \BinaryInfC{$\myjud{\mycohh{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\myprdec{\myjm{\mytmt}{\mytya}{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}}}$}
2050 \mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
2055 \myjud{\myse{A}}{\mytyp} \hspace{1cm} \myjud{\myse{B}}{\mytyp}
2058 \UnaryInfC{$\myjud{\mytya \myeq \mytyb}{\myprop}$}
2063 \myjud{\myse{A}}{\mytyp} \hspace{1cm} \myjud{\mytmm}{\myse{A}} \\
2064 \myjud{\myse{B}}{\mytyp} \hspace{1cm} \myjud{\mytmn}{\myse{B}}
2067 \UnaryInfC{$\myjud{\myjm{\mytmm}{\myse{A}}{\mytmn}{\myse{B}}}{\myprop}$}
2074 While isolating a propositional universe as presented can be a useful
2075 exercises on its own, what we are really after is a useful notion of
2076 equality. In OTT we want to maintain that things judged to be equal are
2077 still always replaceable for one another with no additional
2078 changes. Note that this is not the same as saying that they are
2079 definitionally equal, since as we saw extensionally equal functions,
2080 while satisfying the above requirement, are not.
2082 Towards this goal we introduce two equality constructs in
2083 $\myprop$---the fact that they are in $\myprop$ indicates that they
2084 indeed have no computational content. The first construct, $\myarg
2085 \myeq \myarg$, relates types, the second,
2086 $\myjm{\myarg}{\myarg}{\myarg}{\myarg}$, relates values. The
2087 value-level equality is different from our old propositional equality:
2088 instead of ranging over only one type, we might form equalities between
2089 values of different types---the usefulness of this construct will be
2090 clear soon. In the literature this equality is known as `heterogeneous'
2091 or `John Major', since
2094 John Major's `classless society' widened people's aspirations to
2095 equality, but also the gap between rich and poor. After all, aspiring
2096 to be equal to others than oneself is the politics of envy. In much
2097 the same way, forms equations between members of any type, but they
2098 cannot be treated as equals (ie substituted) unless they are of the
2099 same type. Just as before, each thing is only equal to
2100 itself. \citep{McBride1999}.
2103 Correspondingly, at the term level, $\myfun{coe}$ (`coerce') lets us
2104 transport values between equal types; and $\myfun{coh}$ (`coherence')
2105 guarantees that $\myfun{coe}$ respects the value-level equality, or in
2106 other words that it really has no computational component: if we
2107 transport $\mytmm : \mytya$ to $\mytmn : \mytyb$, $\mytmm$ and $\mytmn$
2108 will still be the same.
2110 Before introducing the core ideas that make OTT work, let us distinguish
2111 between \emph{canonical} and \emph{neutral} terms and types.
2113 \begin{mydef}[Canonical and neutral types and terms]
2114 In a type theory, \emph{neutral} terms are those formed by an
2115 abstracted variable or by an eliminator (including function
2116 application). Everything else is \emph{canonical}.
2118 In the current system, data constructors ($\mytt$, $\mytrue$,
2119 $\myfalse$, $\myabss{\myb{x}}{\mytya}{\mytmt}$, ...) will be
2120 canonical, the rest neutral. Correspondingly, canonical types are
2121 those arising from the ground types ($\myempty$, $\myunit$, $\mybool$)
2122 and the three type formers ($\myarr$, $\myprod$, $\mytyc{W}$).
2123 Neutral types are those formed by
2124 $\myfun{If}\myarg\myfun{Then}\myarg\myfun{Else}\myarg$.
2126 \begin{mydef}[Canonicity]
2127 If in a system all canonical types are inhabited by canonical terms
2128 the system is said to have the \emph{canonicity} property.
2130 The current system, and well-behaved systems in general, has the
2131 canonicity property. Another consequence of normalisation is that all
2132 closed terms will reduce to a canonical term.
2134 \subsubsection{Type equality, and coercions}
2136 The plan is to decompose type-level equalities between canonical types
2137 into decodable propositions containing equalities regarding the
2138 subterms, and to use coerce recursively on the subterms using the
2139 generated equalities. This interplay between the canonicity of equated
2140 types, type equalities, and \myfun{coe} ensures that invocations of
2141 $\myfun{coe}$ will vanish when we have evidence of the structural
2142 equality of the types we are transporting terms across. If the type is
2143 neutral, the equality will not reduce and thus $\myfun{coe}$ will not
2144 reduce either. If we come across an equality between different
2145 canonical types, then we reduce the equality to bottom, making sure that
2146 no such proof can exist, and providing an `escape hatch' in
2151 \mydesc{equality reduction:}{\myprsyn \myred \myprsyn}{
2153 \begin{array}{c@{\ }c@{\ }c@{\ }l}
2154 \myempty & \myeq & \myempty & \myred \mytop \\
2155 \myunit & \myeq & \myunit & \myred \mytop \\
2156 \mybool & \myeq & \mybool & \myred \mytop \\
2157 \myexi{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myexi{\myb{x_2}}{\mytya_2}{\mytya_2} & \myred \\
2159 \myind{2} \mytya_1 \myeq \mytya_2 \myand
2160 \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{\myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2}} \myimpl \mytyb_1[\myb{x_1}] \myeq \mytyb_2[\myb{x_2}]}
2162 \myfora{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myfora{\myb{x_2}}{\mytya_2}{\mytyb_2} & \myred \cdots \\
2163 \myw{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myw{\myb{x_2}}{\mytya_2}{\mytyb_2} & \myred \cdots \\
2164 \mytya & \myeq & \mytyb & \myred \mybot\ \text{if $\mytya$ and $\mytyb$ are canonical.}
2169 \mydesc{reduction}{\mytmsyn \myred \mytmsyn}{
2171 \begin{array}[t]{@{}l@{\ }l@{\ }l@{\ }l@{\ }l@{\ }c@{\ }l@{\ }}
2172 \mycoe & \myempty & \myempty & \myse{Q} & \myse{t} & \myred & \myse{t} \\
2173 \mycoe & \myunit & \myunit & \myse{Q} & \myse{t} & \myred & \mytt \\
2174 \mycoe & \mybool & \mybool & \myse{Q} & \mytrue & \myred & \mytrue \\
2175 \mycoe & \mybool & \mybool & \myse{Q} & \myfalse & \myred & \myfalse \\
2176 \mycoe & (\myexi{\myb{x_1}}{\mytya_1}{\mytyb_1}) &
2177 (\myexi{\myb{x_2}}{\mytya_2}{\mytyb_2}) & \myse{Q} &
2178 \mytmt_1 & \myred & \\
2180 \myind{2}\begin{array}[t]{l@{\ }l@{\ }c@{\ }l}
2181 \mysyn{let} & \myb{\mytmm_1} & \mapsto & \myapp{\myfst}{\mytmt_1} : \mytya_1 \\
2182 & \myb{\mytmn_1} & \mapsto & \myapp{\mysnd}{\mytmt_1} : \mysub{\mytyb_1}{\myb{x_1}}{\myb{\mytmm_1}} \\
2183 & \myb{Q_A} & \mapsto & \myapp{\myfst}{\myse{Q}} : \mytya_1 \myeq \mytya_2 \\
2184 & \myb{\mytmm_2} & \mapsto & \mycoee{\mytya_1}{\mytya_2}{\myb{Q_A}}{\myb{\mytmm_1}} : \mytya_2 \\
2185 & \myb{Q_B} & \mapsto & (\myapp{\mysnd}{\myse{Q}}) \myappsp \myb{\mytmm_1} \myappsp \myb{\mytmm_2} \myappsp (\mycohh{\mytya_1}{\mytya_2}{\myb{Q_A}}{\myb{\mytmm_1}}) : \myprdec{\mysub{\mytyb_1}{\myb{x_1}}{\myb{\mytmm_1}} \myeq \mysub{\mytyb_2}{\myb{x_2}}{\myb{\mytmm_2}}} \\
2186 & \myb{\mytmn_2} & \mapsto & \mycoee{\mysub{\mytyb_1}{\myb{x_1}}{\myb{\mytmm_1}}}{\mysub{\mytyb_2}{\myb{x_2}}{\myb{\mytmm_2}}}{\myb{Q_B}}{\myb{\mytmn_1}} : \mysub{\mytyb_2}{\myb{x_2}}{\myb{\mytmm_2}} \\
2187 \mysyn{in} & \multicolumn{3}{@{}l}{\mypair{\myb{\mytmm_2}}{\myb{\mytmn_2}}}
2190 \mycoe & (\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}) &
2191 (\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}) & \myse{Q} &
2195 \mycoe & (\myw{\myb{x_1}}{\mytya_1}{\mytyb_1}) &
2196 (\myw{\myb{x_2}}{\mytya_2}{\mytyb_2}) & \myse{Q} &
2200 \mycoe & \mytya & \mytyb & \myse{Q} & \mytmt & \myred & \myapp{\myabsurd{\mytyb}}{\myse{Q}}\ \text{if $\mytya$ and $\mytyb$ are canonical.}
2204 \caption{Reducing type equalities, and using them when
2205 $\myfun{coe}$rcing.}
2209 \begin{mydef}[Type equalities reduction, and \myfun{coe}rcions] Figure
2210 \ref{fig:eqred} illustrates the rules to reduce equalities and to
2211 coerce terms. We use a $\mysyn{let}$ syntax for legibility.
2213 For ground types, the proof is the trivial element, and \myfun{coe} is
2214 the identity. For $\myunit$, we can do better: we return its only
2215 member without matching on the term. For the three type binders the
2216 choices we make in the type equality are dictated by the desire of
2217 writing the $\myfun{coe}$ in a natural way.
2219 $\myprod$ is the easiest case: we decompose the proof into proofs that
2220 the first element's types are equal ($\mytya_1 \myeq \mytya_2$), and a
2221 proof that given equal values in the first element, the types of the
2222 second elements are equal too
2223 ($\myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{\myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2}}
2224 \myimpl \mytyb_1[\myb{x_1}] \myeq \mytyb_2[\myb{x_2}]}$).\footnote{We
2225 are using $\myimpl$ to indicate a $\forall$ where we discard the
2226 quantified value. We write $\mytyb_1[\myb{x_1}]$ to indicate that the
2227 $\myb{x_1}$ in $\mytyb_1$ is re-bound to the $\myb{x_1}$ quantified by
2228 the $\forall$, and similarly for $\myb{x_2}$ and $\mytyb_2$.} This
2229 also explains the need for heterogeneous equality, since in the second
2230 proof we need to equate terms of possibly different types. In the
2231 respective $\myfun{coe}$ case, since the types are canonical, we know at
2232 this point that the proof of equality is a pair of the shape described
2233 above. Thus, we can immediately coerce the first element of the pair
2234 using the first element of the proof, and then instantiate the second
2235 element with the two first elements and a proof by coherence of their
2236 equality, since we know that the types are equal.
2238 The cases for the other binders are omitted for brevity, but they follow
2239 the same principle with some twists to make $\myfun{coe}$ work with the
2240 generated proofs; the reader can refer to the paper for details.
2242 \subsubsection{$\myfun{coe}$, laziness, and $\myfun{coh}$erence}
2245 It is important to notice that in the reduction rules for $\myfun{coe}$
2246 are never obstructed by the structure of the proofs. With the exception
2247 of comparisons between different canonical types we never `pattern
2248 match' on the proof pairs, but always look at the projections. This
2249 means that, as long as we are consistent, and thus as long as we don't
2250 have $\mybot$-inducing proofs, we can add propositional axioms for
2251 equality and $\myfun{coe}$ will still compute. Thus, we can take
2252 $\myfun{coh}$ as axiomatic, and we can add back familiar useful equality
2255 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
2256 \AxiomC{$\myjud{\mytmt}{\mytya}$}
2257 \UnaryInfC{$\myjud{\myapp{\myrefl}{\mytmt}}{\myprdec{\myjm{\mytmt}{\mytya}{\mytmt}{\mytya}}}$}
2262 \AxiomC{$\myjud{\mytya}{\mytyp}$}
2263 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytyb}{\mytyp}$}
2264 \BinaryInfC{$\myjud{\mytyc{R} \myappsp (\myb{x} {:} \mytya) \myappsp \mytyb}{\myfora{\myb{y}\, \myb{z}}{\mytya}{\myprdec{\myjm{\myb{y}}{\mytya}{\myb{z}}{\mytya} \myimpl \mysub{\mytyb}{\myb{x}}{\myb{y}} \myeq \mysub{\mytyb}{\myb{x}}{\myb{z}}}}}$}
2268 $\myrefl$ is the equivalent of the reflexivity rule in propositional
2269 equality, and $\mytyc{R}$ asserts that if we have a we have a $\mytyp$
2270 abstracting over a value we can substitute equal for equal---this lets
2271 us recover $\myfun{subst}$. Note that while we need to provide ad-hoc
2272 rules in the restricted, non-hierarchical theory that we have, if our
2273 theory supports abstraction over $\mytyp$s we can easily add these
2274 axioms as top-level abstracted variables.
2276 \subsubsection{Value-level equality}
2278 \begin{mydef}[Value-level equality]\ \end{mydef}
2280 \mydesc{equality reduction:}{\myprsyn \myred \myprsyn}{
2282 \begin{array}{r@{ }c@{\ }c@{\ }c@{}l@{\ }c@{\ }r@{}c@{\ }c@{\ }c@{}l@{\ }l}
2283 (&\mytmt_1 & : & \myempty&) & \myeq & (&\mytmt_2 & : & \myempty &) & \myred \mytop \\
2284 (&\mytmt_1 & : & \myunit&) & \myeq & (&\mytmt_2 & : & \myunit&) & \myred \mytop \\
2285 (&\mytrue & : & \mybool&) & \myeq & (&\mytrue & : & \mybool&) & \myred \mytop \\
2286 (&\myfalse & : & \mybool&) & \myeq & (&\myfalse & : & \mybool&) & \myred \mytop \\
2287 (&\mytrue & : & \mybool&) & \myeq & (&\myfalse & : & \mybool&) & \myred \mybot \\
2288 (&\myfalse & : & \mybool&) & \myeq & (&\mytrue & : & \mybool&) & \myred \mybot \\
2289 (&\mytmt_1 & : & \myexi{\mytya_1}{\myb{x_1}}{\mytyb_1}&) & \myeq & (&\mytmt_2 & : & \myexi{\mytya_2}{\myb{x_2}}{\mytyb_2}&) & \myred \\
2290 & \multicolumn{11}{@{}l}{
2291 \myind{2} \myjm{\myapp{\myfst}{\mytmt_1}}{\mytya_1}{\myapp{\myfst}{\mytmt_2}}{\mytya_2} \myand
2292 \myjm{\myapp{\mysnd}{\mytmt_1}}{\mysub{\mytyb_1}{\myb{x_1}}{\myapp{\myfst}{\mytmt_1}}}{\myapp{\mysnd}{\mytmt_2}}{\mysub{\mytyb_2}{\myb{x_2}}{\myapp{\myfst}{\mytmt_2}}}
2294 (&\myse{f}_1 & : & \myfora{\mytya_1}{\myb{x_1}}{\mytyb_1}&) & \myeq & (&\myse{f}_2 & : & \myfora{\mytya_2}{\myb{x_2}}{\mytyb_2}&) & \myred \\
2295 & \multicolumn{11}{@{}l}{
2296 \myind{2} \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{
2297 \myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2} \myimpl
2298 \myjm{\myapp{\myse{f}_1}{\myb{x_1}}}{\mytyb_1[\myb{x_1}]}{\myapp{\myse{f}_2}{\myb{x_2}}}{\mytyb_2[\myb{x_2}]}
2301 (&\mytmt_1 \mynodee \myse{f}_1 & : & \myw{\mytya_1}{\myb{x_1}}{\mytyb_1}&) & \myeq & (&\mytmt_1 \mynodee \myse{f}_1 & : & \myw{\mytya_2}{\myb{x_2}}{\mytyb_2}&) & \myred \cdots \\
2302 (&\mytmt_1 & : & \mytya_1&) & \myeq & (&\mytmt_2 & : & \mytya_2 &) & \myred \mybot\ \text{if $\mytya_1$ and $\mytya_2$ are canonical.}
2307 As with type-level equality, we want value-level equality to reduce
2308 based on the structure of the compared terms. When matching
2309 propositional data, such as $\myempty$ and $\myunit$, we automatically
2310 return the trivial type, since if a type has zero one members, all
2311 members will be equal. When matching on data-bearing types, such as
2312 $\mybool$, we check that such data matches, and return bottom otherwise.
2313 When matching on records and functions, we rebuild the records and
2314 expand the function to achieve $\eta$-expansion.
2316 \subsection{Proof irrelevance and stuck coercions}
2317 \label{sec:ott-quot}
2319 The last effort is required to make sure that proofs (members of
2320 $\myprop$) are \emph{irrelevant}. Since they are devoid of
2321 computational content, we would like to identify all equivalent
2322 propositions as the same, in a similar way as we identified all
2323 $\myempty$ and all $\myunit$ as the same in section
2324 \ref{sec:eta-expand}.
2326 Thus we will have a quotation that will not only perform
2327 $\eta$-expansion, but will also identify and mark proofs that could not
2328 be decoded (that is, equalities on neutral types). Then, when
2329 comparing terms, marked proofs will be considered equal without
2330 analysing their contents, thus gaining irrelevance.
2332 Moreover we can safely advance `stuck' $\myfun{coe}$rcions between
2333 non-canonical but definitionally equal types. Consider for example
2335 \mycoee{(\myITE{\myb{b}}{\mynat}{\mybool})}{(\myITE{\myb{b}}{\mynat}{\mybool})}{\myb{x}}
2337 Where $\myb{b}$ and $\myb{x}$ are abstracted variables. This
2338 $\myfun{coe}$ will not advance, since the types are not canonical.
2339 However they are definitionally equal, and thus we can safely remove the
2340 coerce and return $\myb{x}$ as it is.
2342 \section{\mykant: the theory}
2343 \label{sec:kant-theory}
2345 \epigraph{\emph{The construction itself is an art, its application to the world an evil parasite.}}{Luitzen Egbertus Jan `Bertus' Brouwer}
2347 \mykant\ is an interactive theorem prover developed as part of this thesis.
2348 The plan is to present a core language which would be capable of serving as
2349 the basis for a more featureful system, while still presenting interesting
2350 features and more importantly observational equality.
2352 We will first present the features of the system, along with motivations
2353 and trade-offs for the design decisions made. Then we describe the
2354 implementation we have developed in Section \ref{sec:kant-practice}.
2355 For an overview of the features of \mykant, see
2356 Section \ref{sec:contributions}, here we present them one by one. The
2357 exception is type holes, which we do not describe holes rigorously, but
2358 provide more information about them in Section \ref{sec:type-holes}.
2360 \subsection{Bidirectional type checking}
2362 We start by describing bidirectional type checking since it calls for
2363 fairly different typing rules that what we have seen up to now. The
2364 idea is to have two kinds of terms: terms for which a type can always be
2365 inferred, and terms that need to be checked against a type. A nice
2366 observation is that this duality is in correspondence with the notion of
2367 canonical and neutral terms: neutral terms
2368 (abstracted or defined variables, function application, record
2369 projections, primitive recursors, etc.) \emph{infer} types, canonical
2370 terms (abstractions, record/data types data constructors, etc.) need to
2373 To introduce the concept and notation, we will revisit the STLC in a
2374 bidirectional style. The presentation follows \cite{Loh2010}. The
2375 syntax for our bidirectional STLC is the same as the untyped
2376 $\lambda$-calculus, but with an extra construct to annotate terms
2377 explicitly---this will be necessary when dealing with top-level
2378 canonical terms. The types are the same as those found in the normal
2381 \begin{mydef}[Syntax for the annotated $\lambda$-calculus]\ \end{mydef}
2385 \begin{array}{r@{\ }c@{\ }l}
2386 \mytmsyn & ::= & \myb{x} \mysynsep \myabs{\myb{x}}{\mytmsyn} \mysynsep (\myapp{\mytmsyn}{\mytmsyn}) \mysynsep (\mytmsyn : \mytysyn)
2391 We will have two kinds of typing judgements: \emph{inference} and
2392 \emph{checking}. $\myinf{\mytmt}{\mytya}$ indicates that $\mytmt$
2393 infers the type $\mytya$, while $\mychk{\mytmt}{\mytya}$ can be checked
2394 against type $\mytya$. The arrows signify the direction of the type
2395 checking---inference pushes types up, checking propagates types
2398 The type of variables in context is inferred, and so are annotate terms.
2399 The type of applications is inferred too, propagating types down the
2400 applied term. Abstractions are checked. Finally, we have a rule to
2401 check the type of an inferrable term.
2403 \begin{mydef}[Bidirectional type checking for the STLC]\ \end{mydef}
2405 \mydesc{typing:}{\myctx \vdash \mytmsyn \Updownarrow \mytmsyn}{
2407 \AxiomC{$\myctx(x) = A$}
2408 \UnaryInfC{$\myinf{\myb{x}}{A}$}
2411 \AxiomC{$\myjudd{\myctx;\myb{x} : A}{\mytmt}{\mytyb}$}
2412 \UnaryInfC{$\mychk{\myabs{x}{\mytmt}}{(\myb{x} {:} \mytya) \myarr \mytyb}$}
2418 \begin{tabular}{ccc}
2419 \AxiomC{$\myinf{\mytmm}{\mytya \myarr \mytyb}$}
2420 \AxiomC{$\mychk{\mytmn}{\mytya}$}
2421 \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mytyb}$}
2424 \AxiomC{$\mychk{\mytmt}{\mytya}$}
2425 \UnaryInfC{$\myinf{\myann{\mytmt}{\mytya}}{\mytya}$}
2428 \AxiomC{$\myinf{\mytmt}{\mytya}$}
2429 \UnaryInfC{$\mychk{\mytmt}{\mytya}$}
2434 For example, if we wanted to type function composition (in this case for
2435 naturals), we would have to annotate the term:
2438 \myfun{comp} : (\mynat \myarr \mynat) \myarr (\mynat \myarr \mynat) \myarr \mynat \myarr \mynat \\
2439 \myfun{comp} \mapsto (\myabs{\myb{f}\, \myb{g}\, \myb{x}}{\myb{f}\myappsp(\myb{g}\myappsp\myb{x})})
2442 But we would not have to annotate functions passed to it, since the type would be propagated to the arguments:
2444 \myfun{comp}\myappsp (\myabs{\myb{x}}{\myb{x} \mathrel{\myfun{$+$}} 3}) \myappsp (\myabs{\myb{x}}{\myb{x} \mathrel{\myfun{$*$}} 4}) \myappsp 42 : \mynat
2447 \subsection{Base terms and types}
2449 Let us begin by describing the primitives available without the user
2450 defining any data types, and without equality. The way we handle
2451 variables and substitution is left unspecified, and explained in section
2452 \ref{sec:term-repr}, along with other implementation issues. We are
2453 also going to give an account of the implicit type hierarchy separately
2454 in Section \ref{sec:term-hierarchy}, so as not to clutter derivation
2455 rules too much, and just treat types as impredicative for the time
2458 \begin{mydef}[Syntax for base types in \mykant]\ \end{mydef}
2462 \begin{array}{r@{\ }c@{\ }l}
2463 \mytmsyn & ::= & \mynamesyn \mysynsep \mytyp \\
2464 & | & \myfora{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
2465 \myabs{\myb{x}}{\mytmsyn} \mysynsep
2466 (\myapp{\mytmsyn}{\mytmsyn}) \mysynsep
2467 (\myann{\mytmsyn}{\mytmsyn}) \\
2468 \mynamesyn & ::= & \myb{x} \mysynsep \myfun{f}
2473 The syntax for our calculus includes just two basic constructs:
2474 abstractions and $\mytyp$s. Everything else will be user-defined.
2475 Since we let the user define values too, we will need a context capable
2476 of carrying the body of variables along with their type.
2478 \begin{mydef}[Context validity]
2479 Bound names and defined names are treated separately in the syntax, and
2480 while both can be associated to a type in the context, only defined
2481 names can be associated with a body.
2484 \mydesc{context validity:}{\myvalid{\myctx}}{
2485 \begin{tabular}{ccc}
2486 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
2487 \UnaryInfC{$\myvalid{\myemptyctx}$}
2490 \AxiomC{$\mychk{\mytya}{\mytyp}$}
2491 \AxiomC{$\mynamesyn \not\in \myctx$}
2492 \BinaryInfC{$\myvalid{\myctx ; \mynamesyn : \mytya}$}
2495 \AxiomC{$\mychk{\mytmt}{\mytya}$}
2496 \AxiomC{$\myfun{f} \not\in \myctx$}
2497 \BinaryInfC{$\myvalid{\myctx ; \myfun{f} \mapsto \mytmt : \mytya}$}
2502 Now we can present the reduction rules, which are unsurprising. We have
2503 the usual function application ($\beta$-reduction), but also a rule to
2504 replace names with their bodies ($\delta$-reduction), and one to discard
2505 type annotations. For this reason reduction is done in-context, as
2506 opposed to what we have seen in the past.
2508 \begin{mydef}[Reduction rules for base types in \mykant]\ \end{mydef}
2510 \mydesc{reduction:}{\myctx \vdash \mytmsyn \myred \mytmsyn}{
2511 \begin{tabular}{ccc}
2512 \AxiomC{\phantom{$\myb{x} \mapsto \mytmt : \mytya \in \myctx$}}
2513 \UnaryInfC{$\myctx \vdash \myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn}
2514 \myred \mysub{\mytmm}{\myb{x}}{\mytmn}$}
2517 \AxiomC{$\myfun{f} \mapsto \mytmt : \mytya \in \myctx$}
2518 \UnaryInfC{$\myctx \vdash \myfun{f} \myred \mytmt$}
2521 \AxiomC{\phantom{$\myb{x} \mapsto \mytmt : \mytya \in \myctx$}}
2522 \UnaryInfC{$\myctx \vdash \myann{\mytmm}{\mytya} \myred \mytmm$}
2527 We can now give types to our terms. Although we include the usual
2528 conversion rule, we defer a detailed account of definitional equality to
2529 Section \ref{sec:kant-irr}.
2531 \begin{mydef}[Bidirectional type checking for base types in \mykant]\ \end{mydef}
2533 \mydesc{typing:}{\myctx \vdash \mytmsyn \Updownarrow \mytmsyn}{
2534 \begin{tabular}{cccc}
2535 \AxiomC{$\myse{name} : A \in \myctx$}
2536 \UnaryInfC{$\myinf{\myse{name}}{A}$}
2539 \AxiomC{$\myfun{f} \mapsto \mytmt : A \in \myctx$}
2540 \UnaryInfC{$\myinf{\myfun{f}}{A}$}
2543 \AxiomC{$\mychk{\mytmt}{\mytya}$}
2544 \UnaryInfC{$\myinf{\myann{\mytmt}{\mytya}}{\mytya}$}
2547 \AxiomC{$\myinf{\mytmt}{\mytya}$}
2548 \AxiomC{$\myctx \vdash \mytya \mydefeq \mytyb$}
2549 \BinaryInfC{$\mychk{\mytmt}{\mytyb}$}
2557 \AxiomC{\phantom{$\mychkk{\myctx; \myb{x}: \mytya}{\mytmt}{\mytyb}$}}
2558 \UnaryInfC{$\myinf{\mytyp}{\mytyp}$}
2561 \AxiomC{$\mychk{\mytya}{\mytyp}$}
2562 \AxiomC{$\mychkk{\myctx; \myb{x} : \mytya}{\mytyb}{\mytyp}$}
2563 \BinaryInfC{$\myinf{(\myb{x} {:} \mytya) \myarr \mytyb}{\mytyp}$}
2572 \AxiomC{$\myinf{\mytmm}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
2573 \AxiomC{$\mychk{\mytmn}{\mytya}$}
2574 \BinaryInfC{$\myinf{\myapp{\mytmm}{\mytmn}}{\mysub{\mytyb}{\myb{x}}{\mytmn}}$}
2579 \AxiomC{$\mychkk{\myctx; \myb{x}: \mytya}{\mytmt}{\mytyb}$}
2580 \UnaryInfC{$\mychk{\myabs{\myb{x}}{\mytmt}}{\myfora{\myb{x}}{\mytyb}{\mytyb}}$}
2586 \subsection{Elaboration}
2588 As we mentioned, $\mykant$\ allows the user to define not only values
2589 but also custom data types and records. \emph{Elaboration} consists of
2590 turning these declarations into workable syntax, types, and reduction
2591 rules. The treatment of custom types in $\mykant$\ is heavily inspired
2592 by McBride's and McKinna's early work on Epigram \citep{McBride2004},
2593 although with some differences.
2595 \subsubsection{Term vectors, telescopes, and assorted notation}
2597 \begin{mydef}[Term vector]
2598 A \emph{term vector} is a series of terms. The empty vector is
2599 represented by $\myemptyctx$, and a new element is added with a
2600 semicolon, similarly to contexts---$\vec{t};\mytmm$.
2603 We use term vectors to refer to a series of term applied to another. For
2604 example $\mytyc{D} \myappsp \vec{A}$ is a shorthand for $\mytyc{D}
2605 \myappsp \mytya_1 \cdots \mytya_n$, for some $n$. $n$ is consistently
2606 used to refer to the length of such vectors, and $i$ to refer to an
2607 index in such vectors.
2609 \begin{mydef}[Telescope]
2610 A \emph{telescope} is a series of typed bindings. The empty telescope
2611 is represented by $\myemptyctx$, and a binding is added via
2615 To present the elaboration and operations on user defined data types, we
2616 frequently make use what \cite{Bruijn91} called \emph{telescopes}, a
2617 construct that will prove useful when dealing with the types of type and
2618 data constructors. We refer to telescopes with $\mytele$, $\mytele'$,
2619 $\mytele_i$, etc. If $\mytele$ refers to a telescope, $\mytelee$ refers
2620 to the term vector made up of all the variables bound by $\mytele$.
2621 $\mytele \myarr \mytya$ refers to the type made by turning the telescope
2622 into a series of $\myarr$. For example we have that
2624 (\myb{x} {:} \mynat); (\myb{p} : \myapp{\myfun{even}}{\myb{x}}) \myarr \mynat =
2625 (\myb{x} {:} \mynat) \myarr (\myb{p} : \myapp{\myfun{even}}{\myb{x}}) \myarr \mynat
2628 We make use of various operations to manipulate telescopes:
2630 \item $\myhead(\mytele)$ refers to the first type appearing in
2631 $\mytele$: $\myhead((\myb{x} {:} \mynat); (\myb{p} :
2632 \myapp{\myfun{even}}{\myb{x}})) = \mynat$. Similarly,
2633 $\myix_i(\mytele)$ refers to the $i^{th}$ type in a telescope
2635 \item $\mytake_i(\mytele)$ refers to the telescope created by taking the
2636 first $i$ elements of $\mytele$: $\mytake_1((\myb{x} {:} \mynat); (\myb{p} :
2637 \myapp{\myfun{even}}{\myb{x}})) = (\myb{x} {:} \mynat)$.
2638 \item $\mytele \vec{A}$ refers to the telescope made by `applying' the
2639 terms in $\vec{A}$ on $\mytele$: $((\myb{x} {:} \mynat); (\myb{p} :
2640 \myapp{\myfun{even}}{\myb{x}}))42 = (\myb{p} :
2641 \myapp{\myfun{even}}{42})$.
2644 Additionally, when presenting syntax elaboration, I'll use $\mytmsyn^n$
2645 to indicate a term vector composed of $n$ elements, or
2646 $\mytmsyn^{\mytele}$ for one composed by as many elements as the
2649 \subsubsection{Declarations syntax}
2651 \begin{mydef}[Syntax of declarations in \mykant]\ \end{mydef}
2655 \begin{array}{r@{\ }c@{\ }l}
2656 \mydeclsyn & ::= & \myval{\myb{x}}{\mytmsyn}{\mytmsyn} \\
2657 & | & \mypost{\myb{x}}{\mytmsyn} \\
2658 & | & \myadt{\mytyc{D}}{\myappsp \mytelesyn}{}{\mydc{c} : \mytelesyn\ |\ \cdots } \\
2659 & | & \myreco{\mytyc{D}}{\myappsp \mytelesyn}{}{\myfun{f} : \mytmsyn,\ \cdots } \\
2661 \mytelesyn & ::= & \myemptytele \mysynsep \mytelesyn \mycc (\myb{x} {:} \mytmsyn) \\
2662 \mynamesyn & ::= & \cdots \mysynsep \mytyc{D} \mysynsep \mytyc{D}.\mydc{c} \mysynsep \mytyc{D}.\myfun{f}
2666 In \mykant\ we have four kind of declarations:
2669 \item[Defined value] A variable, together with a type and a body.
2670 \item[Abstract variable] An abstract variable, with a type but no body.
2671 \item[Inductive data] A \emph{data type}, with a \emph{type constructor}
2672 and various \emph{data constructors}, quite similar to what we find in
2673 Haskell. A primitive \emph{eliminator} (or \emph{destructor}, or
2674 \emph{recursor}) will be used to compute with each data type.
2675 \item[Record] A \emph{record}, which like data types consists of a type
2676 constructor but only one data constructor. The user can also define
2677 various \emph{fields}, with no recursive occurrences of the type. The
2678 functions extracting the fields' values from an instance of a record
2679 are called \emph{projections}.
2682 Elaborating defined variables consists of type checking the body against
2683 the given type, and updating the context to contain the new binding.
2684 Elaborating abstract variables and abstract variables consists of type
2685 checking the type, and updating the context with a new typed variable.
2687 \begin{mydef}[Elaboration of defined and abstract variables]\ \end{mydef}
2689 \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
2691 \AxiomC{$\mychk{\mytmt}{\mytya}$}
2692 \AxiomC{$\myfun{f} \not\in \myctx$}
2694 $\myctx \myelabt \myval{\myfun{f}}{\mytya}{\mytmt} \ \ \myelabf\ \ \myctx; \myfun{f} \mapsto \mytmt : \mytya$
2698 \AxiomC{$\mychk{\mytya}{\mytyp}$}
2699 \AxiomC{$\myfun{f} \not\in \myctx$}
2702 \myctx \myelabt \mypost{\myfun{f}}{\mytya}
2703 \ \ \myelabf\ \ \myctx; \myfun{f} : \mytya
2710 \subsubsection{User defined types}
2711 \label{sec:user-type}
2713 Elaborating user defined types is the real effort. First, we will
2714 explain what we can define, with some examples.
2717 \item[Natural numbers] To define natural numbers, we create a data type
2718 with two constructors: one with zero arguments ($\mydc{zero}$) and one
2719 with one recursive argument ($\mydc{suc}$):
2722 \myadt{\mynat}{ }{ }{
2723 \mydc{zero} \mydcsep \mydc{suc} \myappsp \mynat
2727 This is very similar to what we would write in Haskell:
2729 data Nat = Zero | Suc Nat
2731 Once the data type is defined, $\mykant$\ will generate syntactic
2732 constructs for the type and data constructors, so that we will have
2735 \begin{tabular}{ccc}
2736 \AxiomC{\phantom{$\mychk{\mytmt}{\mynat}$}}
2737 \UnaryInfC{$\myinf{\mynat}{\mytyp}$}
2740 \AxiomC{\phantom{$\mychk{\mytmt}{\mynat}$}}
2741 \UnaryInfC{$\myinf{\mytyc{\mynat}.\mydc{zero}}{\mynat}$}
2744 \AxiomC{$\mychk{\mytmt}{\mynat}$}
2745 \UnaryInfC{$\myinf{\mytyc{\mynat}.\mydc{suc} \myappsp \mytmt}{\mynat}$}
2749 While in Haskell (or indeed in Agda or Coq) data constructors are
2750 treated the same way as functions, in $\mykant$\ they are syntax, so
2751 for example using $\mytyc{\mynat}.\mydc{suc}$ on its own will give a
2752 syntax error. This is necessary so that we can easily infer the type
2753 of polymorphic data constructors, as we will see later.
2755 Moreover, each data constructor is prefixed by the type constructor
2756 name, since we need to retrieve the type constructor of a data
2757 constructor when type checking. This measure aids in the presentation
2758 of various features but it is not needed in the implementation, where
2759 we can have a dictionary to look up the type constructor corresponding
2760 to each data constructor. When using data constructors in examples I
2761 will omit the type constructor prefix for brevity, in this case
2762 writing $\mydc{zero}$ instead of $\mynat.\mydc{suc}$ and $\mydc{suc}$ instead of
2763 $\mynat.\mydc{suc}$.
2765 Along with user defined constructors, $\mykant$\ automatically
2766 generates an \emph{eliminator}, or \emph{destructor}, to compute with
2767 natural numbers: If we have $\mytmt : \mynat$, we can destruct
2768 $\mytmt$ using the generated eliminator `$\mynat.\myfun{elim}$':
2771 \AxiomC{$\mychk{\mytmt}{\mynat}$}
2773 \myinf{\mytyc{\mynat}.\myfun{elim} \myappsp \mytmt}{
2775 \myfora{\myb{P}}{\mynat \myarr \mytyp}{ \\ \myapp{\myb{P}}{\mydc{zero}} \myarr (\myfora{\myb{x}}{\mynat}{\myapp{\myb{P}}{\myb{x}} \myarr \myapp{\myb{P}}{(\myapp{\mydc{suc}}{\myb{x}})}}) \myarr \\ \myapp{\myb{P}}{\mytmt}}
2779 $\mynat.\myfun{elim}$ corresponds to the induction principle for
2780 natural numbers: if we have a predicate on numbers ($\myb{P}$), and we
2781 know that predicate holds for the base case
2782 ($\myapp{\myb{P}}{\mydc{zero}}$) and for each inductive step
2783 ($\myfora{\myb{x}}{\mynat}{\myapp{\myb{P}}{\myb{x}} \myarr
2784 \myapp{\myb{P}}{(\myapp{\mydc{suc}}{\myb{x}})}}$), then $\myb{P}$
2785 holds for any number. As with the data constructors, we require the
2786 eliminator to be applied to the `destructed' element.
2788 While the induction principle is usually seen as a mean to prove
2789 properties about numbers, in the intuitionistic setting it is also a
2790 mean to compute. In this specific case $\mynat.\myfun{elim}$
2791 returns the base case if the provided number is $\mydc{zero}$, and
2792 recursively applies the inductive step if the number is a
2795 \begin{array}{@{}l@{}l}
2796 \mytyc{\mynat}.\myfun{elim} \myappsp \mydc{zero} & \myappsp \myse{P} \myappsp \myse{pz} \myappsp \myse{ps} \myred \myse{pz} \\
2797 \mytyc{\mynat}.\myfun{elim} \myappsp (\mydc{suc} \myappsp \mytmt) & \myappsp \myse{P} \myappsp \myse{pz} \myappsp \myse{ps} \myred \myse{ps} \myappsp \mytmt \myappsp (\mynat.\myfun{elim} \myappsp \mytmt \myappsp \myse{P} \myappsp \myse{pz} \myappsp \myse{ps})
2800 The Haskell equivalent would be
2802 elim :: Nat -> a -> (Nat -> a -> a) -> a
2803 elim Zero pz ps = pz
2804 elim (Suc n) pz ps = ps n (elim n pz ps)
2806 Which buys us the computational behaviour, but not the reasoning power,
2807 since we cannot express the notion of a predicate depending on
2808 $\mynat$---the type system is far too weak.
2810 \item[Binary trees] Now for a polymorphic data type: binary trees, since
2811 lists are too similar to natural numbers to be interesting.
2814 \myadt{\mytree}{\myappsp (\myb{A} {:} \mytyp)}{ }{
2815 \mydc{leaf} \mydcsep \mydc{node} \myappsp (\myapp{\mytree}{\myb{A}}) \myappsp \myb{A} \myappsp (\myapp{\mytree}{\myb{A}})
2819 Now the purpose of `constructors as syntax' can be explained: what would
2820 the type of $\mydc{leaf}$ be? If we were to treat it as a `normal'
2821 term, we would have to specify the type parameter of the tree each
2822 time the constructor is applied:
2824 \begin{array}{@{}l@{\ }l}
2825 \mydc{leaf} & : \myfora{\myb{A}}{\mytyp}{\myapp{\mytree}{\myb{A}}} \\
2826 \mydc{node} & : \myfora{\myb{A}}{\mytyp}{\myapp{\mytree}{\myb{A}} \myarr \myb{A} \myarr \myapp{\mytree}{\myb{A}} \myarr \myapp{\mytree}{\myb{A}}}
2829 The problem with this approach is that creating terms is incredibly
2830 verbose and dull, since we would need to specify the type parameters
2831 each time. For example if we wished to create a $\mytree \myappsp
2832 \mynat$ with two nodes and three leaves, we would write
2834 \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)
2836 The redundancy of $\mynat$s is quite irritating. Instead, if we treat
2837 constructors as syntactic elements, we can `extract' the type of the
2838 parameter from the type that the term gets checked against, much like
2839 what we do to type abstractions:
2843 \AxiomC{$\mychk{\mytya}{\mytyp}$}
2844 \UnaryInfC{$\mychk{\mydc{leaf}}{\myapp{\mytree}{\mytya}}$}
2847 \AxiomC{$\mychk{\mytmm}{\mytree \myappsp \mytya}$}
2848 \AxiomC{$\mychk{\mytmt}{\mytya}$}
2849 \AxiomC{$\mychk{\mytmm}{\mytree \myappsp \mytya}$}
2850 \TrinaryInfC{$\mychk{\mydc{node} \myappsp \mytmm \myappsp \mytmt \myappsp \mytmn}{\mytree \myappsp \mytya}$}
2854 Which enables us to write, much more concisely
2856 \mydc{node} \myappsp (\mydc{node} \myappsp \mydc{leaf} \myappsp (\myapp{\mydc{suc}}{\mydc{zero}}) \myappsp \mydc{leaf}) \myappsp \mydc{zero} \myappsp \mydc{leaf} : \myapp{\mytree}{\mynat}
2858 We gain an annotation, but we lose the myriad of types applied to the
2859 constructors. Conversely, with the eliminator for $\mytree$, we can
2860 infer the type of the arguments given the type of the destructed:
2863 \AxiomC{$\myinf{\mytmt}{\myapp{\mytree}{\mytya}}$}
2865 \myinf{\mytree.\myfun{elim} \myappsp \mytmt}{
2867 (\myb{P} {:} \myapp{\mytree}{\mytya} \myarr \mytyp) \myarr \\
2868 \myapp{\myb{P}}{\mydc{leaf}} \myarr \\
2869 ((\myb{l} {:} \myapp{\mytree}{\mytya}) (\myb{x} {:} \mytya) (\myb{r} {:} \myapp{\mytree}{\mytya}) \myarr \myapp{\myb{P}}{\myb{l}} \myarr
2870 \myapp{\myb{P}}{\myb{r}} \myarr \myb{P} \myappsp (\mydc{node} \myappsp \myb{l} \myappsp \myb{x} \myappsp \myb{r})) \myarr \\
2871 \myapp{\myb{P}}{\mytmt}
2876 As expected, the eliminator embodies structural induction on trees.
2877 We have a base case for $\myb{P} \myappsp \mydc{leaf}$, and an
2878 inductive step that given two subtrees and the predicate applied to
2879 them needs to return the predicate applied to the tree formed by a
2880 node with the two subtrees as children.
2882 \item[Empty type] We have presented types that have at least one
2883 constructors, but nothing prevents us from defining types with
2884 \emph{no} constructors:
2885 \[\myadt{\mytyc{Empty}}{ }{ }{ }\]
2886 What shall the `induction principle' on $\mytyc{Empty}$ be? Does it
2887 even make sense to talk about induction on $\mytyc{Empty}$?
2888 $\mykant$\ does not care, and generates an eliminator with no `cases':
2891 \AxiomC{$\myinf{\mytmt}{\mytyc{Empty}}$}
2892 \UnaryInfC{$\myinf{\myempty.\myfun{elim} \myappsp \mytmt}{(\myb{P} {:} \mytmt \myarr \mytyp) \myarr \myapp{\myb{P}}{\mytmt}}$}
2894 which lets us write the $\myfun{absurd}$ that we know and love:
2897 \myfun{absurd} : (\myb{A} {:} \mytyp) \myarr \myempty \myarr \myb{A} \\
2898 \myfun{absurd}\myappsp \myb{A} \myappsp \myb{x} \mapsto \myempty.\myfun{elim} \myappsp \myb{x} \myappsp (\myabs{\myarg}{\myb{A}})
2902 \item[Ordered lists] Up to this point, the examples shown are nothing
2903 new to the \{Haskell, SML, OCaml, functional\} programmer. However
2904 dependent types let us express much more than that. A useful example
2905 is the type of ordered lists. There are many ways to define such a
2906 thing, but we will define our type to store the bounds of the list,
2907 making sure that $\mydc{cons}$ing respects that.
2909 First, using $\myunit$ and $\myempty$, we define a type expressing the
2910 ordering on natural numbers, $\myfun{le}$---`less or equal'.
2911 $\myfun{le}\myappsp \mytmm \myappsp \mytmn$ will be inhabited only if
2912 $\mytmm \le \mytmn$:
2915 \myfun{le} : \mynat \myarr \mynat \myarr \mytyp \\
2916 \myfun{le} \myappsp \myb{n} \mapsto \\
2917 \myind{2} \mynat.\myfun{elim} \\
2918 \myind{2}\myind{2} \myb{n} \\
2919 \myind{2}\myind{2} (\myabs{\myarg}{\mynat \myarr \mytyp}) \\
2920 \myind{2}\myind{2} (\myabs{\myarg}{\myunit}) \\
2921 \myind{2}\myind{2} (\myabs{\myb{n}\, \myb{f}\, \myb{m}}{
2922 \mynat.\myfun{elim} \myappsp \myb{m} \myappsp (\myabs{\myarg}{\mytyp}) \myappsp \myempty \myappsp (\myabs{\myb{m'}\, \myarg}{\myapp{\myb{f}}{\myb{m'}}})
2926 We return $\myunit$ if the scrutinised is $\mydc{zero}$ (every
2927 number in less or equal than zero), $\myempty$ if the first number is
2928 a $\mydc{suc}$cessor and the second a $\mydc{zero}$, and we recurse if
2929 they are both successors. Since we want the list to have possibly
2930 `open' bounds, for example for empty lists, we create a type for
2931 `lifted' naturals with a bottom ($\le$ everything but itself) and top
2932 ($\ge$ everything but itself) elements, along with an associated comparison
2936 \myadt{\mytyc{Lift}}{ }{ }{\mydc{bot} \mydcsep \mydc{lift} \myappsp \mynat \mydcsep \mydc{top}}\\
2937 \myfun{le'} : \mytyc{Lift} \myarr \mytyc{Lift} \myarr \mytyp\\
2938 \myfun{le'} \myappsp \myb{l_1} \mapsto \\
2939 \myind{2} \mytyc{Lift}.\myfun{elim} \\
2940 \myind{2}\myind{2} \myb{l_1} \\
2941 \myind{2}\myind{2} (\myabs{\myarg}{\mytyc{Lift} \myarr \mytyp}) \\
2942 \myind{2}\myind{2} (\myabs{\myarg}{\myunit}) \\
2943 \myind{2}\myind{2} (\myabs{\myb{n_1}\, \myb{l_2}}{
2944 \mytyc{Lift}.\myfun{elim} \myappsp \myb{l_2} \myappsp (\myabs{\myarg}{\mytyp}) \myappsp \myempty \myappsp (\myabs{\myb{n_2}}{\myfun{le} \myappsp \myb{n_1} \myappsp \myb{n_2}}) \myappsp \myunit
2946 \myind{2}\myind{2} (\myabs{\myb{l_2}}{
2947 \mytyc{Lift}.\myfun{elim} \myappsp \myb{l_2} \myappsp (\myabs{\myarg}{\mytyp}) \myappsp \myempty \myappsp (\myabs{\myarg}{\myempty}) \myappsp \myunit
2951 Finally, we can defined a type of ordered lists. The type is
2952 parametrised over two values representing the lower and upper bounds
2953 of the elements, as opposed to the type parameters that we are used
2954 to. Then, an empty list will have to have evidence that the bounds
2955 are ordered, and each time we add an element we require the list to
2956 have a matching lower bound:
2959 \myadt{\mytyc{OList}}{\myappsp (\myb{low}\ \myb{upp} {:} \mytyc{Lift})}{\\ \myind{2}}{
2960 \mydc{nil} \myappsp (\myfun{le'} \myappsp \myb{low} \myappsp \myb{upp}) \mydcsep \mydc{cons} \myappsp (\myb{n} {:} \mynat) \myappsp (\mytyc{OList} \myappsp (\myfun{lift} \myappsp \myb{n}) \myappsp \myb{upp}) \myappsp (\myfun{le'} \myappsp \myb{low} \myappsp (\myfun{lift} \myappsp \myb{n})
2964 Note that in the $\mydc{cons}$ constructor we quantify over the first
2965 argument, which will determine the type of the following
2966 arguments---again something we cannot do in systems like Haskell. If
2967 we want we can then employ this structure to write and prove correct
2968 various sorting algorithms.\footnote{See this presentation by Conor
2970 \url{https://personal.cis.strath.ac.uk/conor.mcbride/Pivotal.pdf},
2971 and this blog post by the author:
2972 \url{http://mazzo.li/posts/AgdaSort.html}.}
2974 \item[Dependent products] Apart from $\mysyn{data}$, $\mykant$\ offers
2975 us another way to define types: $\mysyn{record}$. A record is a
2976 data type with one constructor and `projections' to extract specific
2977 fields of the said constructor.
2979 For example, we can recover dependent products:
2982 \myreco{\mytyc{Prod}}{\myappsp (\myb{A} {:} \mytyp) \myappsp (\myb{B} {:} \myb{A} \myarr \mytyp)}{\\ \myind{2}}{\myfst : \myb{A}, \mysnd : \myapp{\myb{B}}{\myb{fst}}}
2985 Here $\myfst$ and $\mysnd$ are the projections, with their respective
2986 types. Note that each field can refer to the preceding fields---in
2987 this case we have the type of $\myfun{snd}$ depending on the value of
2988 $\myfun{fst}$. A constructor will be automatically generated, under
2989 the name of $\mytyc{Prod}.\mydc{constr}$. Dually to data types, we
2990 will omit the type constructor prefix for record projections.
2992 Following the bidirectionality of the system, we have that projections
2993 (the destructors of the record) infer the type, while the constructor
2998 \AxiomC{$\mychk{\mytmm}{\mytya}$}
2999 \AxiomC{$\mychk{\mytmn}{\myapp{\mytyb}{\mytmm}}$}
3000 \BinaryInfC{$\mychk{\mytyc{Prod}.\mydc{constr} \myappsp \mytmm \myappsp \mytmn}{\mytyc{Prod} \myappsp \mytya \myappsp \mytyb}$}
3002 \UnaryInfC{\phantom{$\myinf{\myfun{snd} \myappsp \mytmt}{\mytyb \myappsp (\myfst \myappsp \mytmt)}$}}
3005 \AxiomC{$\hspace{0.2cm}\myinf{\mytmt}{\mytyc{Prod} \myappsp \mytya \myappsp \mytyb}\hspace{0.2cm}$}
3006 \UnaryInfC{$\myinf{\myfun{fst} \myappsp \mytmt}{\mytya}$}
3008 \UnaryInfC{$\myinf{\myfun{snd} \myappsp \mytmt}{\mytyb \myappsp (\myfst \myappsp \mytmt)}$}
3012 What we have defined here is equivalent to ITT's dependent products.
3021 \mynamesyn ::= \cdots \mysynsep \mytyc{D} \mysynsep \mytyc{D}.\mydc{c} \mysynsep \mytyc{D}.\myfun{f}
3028 \mydesc{syntax elaboration:}{\mydeclsyn \myelabf \mytmsyn ::= \cdots}{
3031 \begin{array}{r@{\ }l}
3032 & \myadt{\mytyc{D}}{\mytele}{}{\cdots\ |\ \mydc{c}_n : \mytele_n } \\
3035 \begin{array}{r@{\ }c@{\ }l}
3036 \mytmsyn & ::= & \cdots \mysynsep \myapp{\mytyc{D}}{\mytmsyn^{\mytele}} \mysynsep \cdots \mysynsep
3037 \mytyc{D}.\mydc{c}_n \myappsp \mytmsyn^{\mytele_n} \mysynsep \mytyc{D}.\myfun{elim} \myappsp \mytmsyn \\
3045 \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
3050 \myinf{\mytele \myarr \mytyp}{\mytyp}\hspace{0.8cm}
3051 \mytyc{D} \not\in \myctx \\
3052 \myinff{\myctx;\ \mytyc{D} : \mytele \myarr \mytyp}{\mytele \mycc \mytele_i \myarr \myapp{\mytyc{D}}{\mytelee}}{\mytyp}\ \ \ (1 \leq i \leq n) \\
3053 \text{For each $(\myb{x} {:} \mytya)$ in each $\mytele_i$, if $\mytyc{D} \in \mytya$, then $\mytya = \myapp{\mytyc{D}}{\vec{\mytmt}}$.}
3057 \begin{array}{r@{\ }c@{\ }l}
3058 \myctx & \myelabt & \myadt{\mytyc{D}}{\mytele}{}{ \cdots \ |\ \mydc{c}_n : \mytele_n } \\
3059 & & \vspace{-0.2cm} \\
3060 & \myelabf & \myctx;\ \mytyc{D} : \mytele \myarr \mytyp;\ \cdots;\ \mytyc{D}.\mydc{c}_n : \mytele \mycc \mytele_n \myarr \myapp{\mytyc{D}}{\mytelee}; \\
3062 \begin{array}{@{}r@{\ }l l}
3063 \mytyc{D}.\myfun{elim} : & \mytele \myarr (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr & \textbf{target} \\
3064 & (\myb{P} {:} \myapp{\mytyc{D}}{\mytelee} \myarr \mytyp) \myarr & \textbf{motive} \\
3068 (\mytele_n \mycc \myhyps(\myb{P}, \mytele_n) \myarr \myapp{\myb{P}}{(\myapp{\mytyc{D}.\mydc{c}_n}{\mytelee_n})}) \myarr
3069 \end{array} \right \}
3070 & \textbf{methods} \\
3071 & \myapp{\myb{P}}{\myb{x}} &
3075 \DisplayProof \\ \vspace{0.2cm}\ \\
3077 \begin{array}{@{}l l@{\ } l@{} r c l}
3078 \textbf{where} & \myhyps(\myb{P}, & \myemptytele &) & \mymetagoes & \myemptytele \\
3079 & \myhyps(\myb{P}, & (\myb{r} {:} \myapp{\mytyc{D}}{\vec{\mytmt}}) \mycc \mytele &) & \mymetagoes & (\myb{r'} {:} \myapp{\myb{P}}{\myb{r}}) \mycc \myhyps(\myb{P}, \mytele) \\
3080 & \myhyps(\myb{P}, & (\myb{x} {:} \mytya) \mycc \mytele & ) & \mymetagoes & \myhyps(\myb{P}, \mytele)
3088 \mydesc{reduction elaboration:}{\mydeclsyn \myelabf \myctx \vdash \mytmsyn \myred \mytmsyn}{
3090 $\myadt{\mytyc{D}}{\mytele}{}{ \cdots \ |\ \mydc{c}_n : \mytele_n } \ \ \myelabf$
3091 \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
3092 \AxiomC{$\mytyc{D}.\mydc{c}_i : \mytele;\mytele_i \myarr \myapp{\mytyc{D}}{\mytelee} \in \myctx$}
3094 \myctx \vdash \myapp{\myapp{\myapp{\mytyc{D}.\myfun{elim}}{(\myapp{\mytyc{D}.\mydc{c}_i}{\vec{\myse{t}}})}}{\myse{P}}}{\vec{\myse{m}}} \myred \myapp{\myapp{\myse{m}_i}{\vec{\mytmt}}}{\myrecs(\myse{P}, \vec{m}, \mytele_i)}
3096 \DisplayProof \\ \vspace{0.2cm}\ \\
3098 \begin{array}{@{}l l@{\ } l@{} r c l}
3099 \textbf{where} & \myrecs(\myse{P}, \vec{m}, & \myemptytele &) & \mymetagoes & \myemptytele \\
3100 & \myrecs(\myse{P}, \vec{m}, & (\myb{r} {:} \myapp{\mytyc{D}}{\vec{A}}); \mytele & ) & \mymetagoes & (\mytyc{D}.\myfun{elim} \myappsp \myb{r} \myappsp \myse{P} \myappsp \vec{m}); \myrecs(\myse{P}, \vec{m}, \mytele) \\
3101 & \myrecs(\myse{P}, \vec{m}, & (\myb{x} {:} \mytya); \mytele &) & \mymetagoes & \myrecs(\myse{P}, \vec{m}, \mytele)
3108 \mydesc{syntax elaboration:}{\myelab{\mydeclsyn}{\mytmsyn ::= \cdots}}{
3111 \begin{array}{r@{\ }c@{\ }l}
3112 \myctx & \myelabt & \myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \\
3115 \begin{array}{r@{\ }c@{\ }l}
3116 \mytmsyn & ::= & \cdots \mysynsep \myapp{\mytyc{D}}{\mytmsyn^{\mytele}} \mysynsep \mytyc{D}.\mydc{constr} \myappsp \mytmsyn^{n} \mysynsep \cdots \mysynsep \mytyc{D}.\myfun{f}_n \myappsp \mytmsyn \\
3124 \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
3128 \myinf{\mytele \myarr \mytyp}{\mytyp}\hspace{0.8cm}
3129 \mytyc{D} \not\in \myctx \\
3130 \myinff{\myctx; \mytele; (\myb{f}_j : \myse{F}_j)_{j=1}^{i - 1}}{F_i}{\mytyp} \myind{3} (1 \le i \le n)
3134 \begin{array}{r@{\ }c@{\ }l}
3135 \myctx & \myelabt & \myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \\
3136 & & \vspace{-0.2cm} \\
3137 & \myelabf & \myctx;\ \mytyc{D} : \mytele \myarr \mytyp;\ \cdots;\ \mytyc{D}.\myfun{f}_n : \mytele \myarr (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr \mysub{\myse{F}_n}{\myb{f}_i}{\myapp{\myfun{f}_i}{\myb{x}}}_{i = 1}^{n-1}; \\
3138 & & \mytyc{D}.\mydc{constr} : \mytele \myarr \myse{F}_1 \myarr \cdots \myarr \myse{F}_n \myarr \myapp{\mytyc{D}}{\mytelee};
3146 \mydesc{reduction elaboration:}{\mydeclsyn \myelabf \myctx \vdash \mytmsyn \myred \mytmsyn}{
3148 $\myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \ \ \myelabf$
3149 \AxiomC{$\mytyc{D} \in \myctx$}
3150 \UnaryInfC{$\myctx \vdash \myapp{\mytyc{D}.\myfun{f}_i}{(\mytyc{D}.\mydc{constr} \myappsp \vec{t})} \myred t_i$}
3154 \caption{Elaboration for data types and records.}
3158 \begin{mydef}[Elaboration for user defined types]
3159 Following the intuition given by the examples, the full elaboration
3160 machinery is presented Figure \ref{fig:elab}.
3162 Our elaboration is essentially a modification of Figure 9 of
3163 \cite{McBride2004}. However, our data types are not inductive
3164 families,\footnote{See Section \ref{sec:future-work} for a brief
3165 description of inductive families.} we do bidirectional type checking
3166 by treating constructors/destructors as syntax, and we have records.
3168 \begin{mydef}[Strict positivity]
3169 A inductive type declaration is \emph{strictly positive} if recursive
3170 occurrences of the type we are defining do not appear embedded
3171 anywhere in the domain part of any function in the types for the data
3174 In data type declarations we allow recursive occurrences as long as they
3175 are strictly positive, which ensures the consistency of the theory. To
3176 achieve that we employing a syntactic check to make sure that this is
3177 the case---in fact the check is stricter than necessary for simplicity,
3178 given that we allow recursive occurrences only at the top level of data
3179 constructor arguments. For example a definition of the $\mytyc{W}$ type
3180 is accepted in Agda but rejected in \mykant.
3184 Without these precautions, we can easily derive any type with no
3187 data Fix a = Fix (Fix a -> a) -- Negative occurrence of `Fix a'
3188 -- Term inhabiting any type `a'
3190 boom = (\f -> f (Fix f)) (\x -> (\(Fix f) -> f) x x)
3192 See \cite{Dybjer1991} for a more formal treatment of inductive
3195 For what concerns records, recursive occurrences are disallowed. The
3196 reason for this choice is answered by the reason for the choice of
3197 having records at all: we need records to give the user types with
3198 $\eta$-laws for equality, as we saw in Section \ref{sec:eta-expand}
3199 and in the treatment of OTT in Section \ref{sec:ott}. If we tried to
3200 $\eta$-expand recursive data types, we would expand forever.
3202 \begin{mydef}[Bidirectional type checking for elaborated types]
3203 To implement bidirectional type checking for constructors and
3204 destructors, we store their types in full in the context, and then
3205 instantiate when due.
3208 \mydesc{typing:}{\myctx \vdash \mytmsyn \Updownarrow \mytmsyn}{
3211 \mytyc{D} : \mytele \myarr \mytyp \in \myctx \hspace{1cm}
3212 \mytyc{D}.\mydc{c} : \mytele \mycc \mytele' \myarr
3213 \myapp{\mytyc{D}}{\mytelee} \in \myctx \\
3214 \mytele'' = (\mytele;\mytele')\vec{A} \hspace{1cm}
3215 \mychkk{\myctx; \mytake_{i-1}(\mytele'')}{t_i}{\myix_i( \mytele'')}\ \
3216 (1 \le i \le \mytele'')
3219 \UnaryInfC{$\mychk{\myapp{\mytyc{D}.\mydc{c}}{\vec{t}}}{\myapp{\mytyc{D}}{\vec{A}}}$}
3224 \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
3225 \AxiomC{$\mytyc{D}.\myfun{f} : \mytele \mycc (\myb{x} {:}
3226 \myapp{\mytyc{D}}{\mytelee}) \myarr \myse{F}$}
3227 \AxiomC{$\myjud{\mytmt}{\myapp{\mytyc{D}}{\vec{A}}}$}
3228 \TrinaryInfC{$\myinf{\myapp{\mytyc{D}.\myfun{f}}{\mytmt}}{(\mytele
3229 \mycc (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr
3230 \myse{F})(\vec{A};\mytmt)}$}
3234 \subsubsection{Why user defined types? Why eliminators?}
3236 The hardest design choice in developing $\mykant$\ was to decide whether
3237 user defined types should be included, and how to handle them. As we
3238 saw, while we can devise general structures like $\mytyc{W}$, they are
3239 unsuitable both for for direct usage and `mechanical' usage. Thus most
3240 theorem provers in the wild provide some means for the user to define
3241 structures tailored to specific uses.
3243 Even if we take user defined types for granted, while there is not much
3244 debate on how to handle records, there are two broad schools of thought
3245 regarding the handling of data types:
3247 \item[Fixed points and pattern matching] The road chosen by Agda and Coq.
3248 Functions are written like in Haskell---matching on the input and with
3249 explicit recursion. An external check on the recursive arguments
3250 ensures that they are decreasing, and thus that all functions
3251 terminate. This approach is the best in terms of user usability, but
3252 it is tricky to implement correctly.
3254 \item[Elaboration into eliminators] The road chose by \mykant, and
3255 pioneered by the Epigram line of work. The advantage is that we can
3256 reduce every data type to simple definitions which guarantee
3257 termination and are simple to reduce and type. It is however more
3258 cumbersome to use than pattern matching, although \cite{McBride2004}
3259 has shown how to implement an expressive pattern matching interface on
3260 top of a larger set of combinators of those provided by \mykant.
3262 We can go ever further down this road and elaborate the declarations
3263 for data types themselves to primitive types, so that our `core'
3264 language will be very small and manageable
3265 \citep{dagand2012elaborating, chapman2010gentle}.
3268 We chose the safer and easier to implement path, given the time
3269 constraints and the higher confidence of correctness. See also Section
3270 \ref{sec:future-work} for a brief overview of ways to extend or treat
3273 \subsection{Cumulative hierarchy and typical ambiguity}
3274 \label{sec:term-hierarchy}
3276 Having a well founded type hierarchy is crucial if we want to retain
3277 consistency, otherwise we can break our type systems by proving bottom,
3278 as shown in Appendix \ref{app:hurkens}.
3280 However, hierarchy as presented in section \ref{sec:itt} is a
3281 considerable burden on the user, on various levels. Consider for
3282 example how we recovered disjunctions in Section \ref{sec:disju}: we
3283 have a function that takes two $\mytyp_0$ and forms a new $\mytyp_0$.
3284 What if we wanted to form a disjunction containing something a
3285 $\mytyp_1$, or $\mytyp_{42}$? Our definition would fail us, since
3286 $\mytyp_1 : \mytyp_2$.
3290 \mydesc{cumulativity:}{\myctx \vdash \mytmsyn \mycumul \mytmsyn}{
3291 \begin{tabular}{ccc}
3292 \AxiomC{$\myctx \vdash \mytya \mydefeq \mytyb$}
3293 \UnaryInfC{$\myctx \vdash \mytya \mycumul \mytyb$}
3296 \AxiomC{\phantom{$\myctx \vdash \mytya \mydefeq \mytyb$}}
3297 \UnaryInfC{$\myctx \vdash \mytyp_l \mycumul \mytyp_{l+1}$}
3300 \AxiomC{$\myctx \vdash \mytya \mycumul \mytyb$}
3301 \AxiomC{$\myctx \vdash \mytyb \mycumul \myse{C}$}
3302 \BinaryInfC{$\myctx \vdash \mytya \mycumul \myse{C}$}
3308 \begin{tabular}{ccc}
3309 \AxiomC{$\myjud{\mytmt}{\mytya}$}
3310 \AxiomC{$\myctx \vdash \mytya \mycumul \mytyb$}
3311 \BinaryInfC{$\myjud{\mytmt}{\mytyb}$}
3314 \AxiomC{$\myctx \vdash \mytya_1 \mydefeq \mytya_2$}
3315 \AxiomC{$\myctx; \myb{x} : \mytya_1 \vdash \mytyb_1 \mycumul \mytyb_2$}
3316 \BinaryInfC{$\myctx (\myb{x} {:} \mytya_1) \myarr \mytyb_1 \mycumul (\myb{x} {:} \mytya_2) \myarr \mytyb_2$}
3320 \caption{Cumulativity rules for base types in \mykant, plus a
3321 `conversion' rule for cumulative types.}
3322 \label{fig:cumulativity}
3325 One way to solve this issue is a \emph{cumulative} hierarchy, where
3326 $\mytyp_{l_1} : \mytyp_{l_2}$ iff $l_1 < l_2$. This way we retain
3327 consistency, while allowing for `large' definitions that work on small
3330 \begin{mydef}[Cumulativity for \mykant' base types]
3331 Figure \ref{fig:cumulativity} gives a formal definition of
3332 \emph{cumulativity} for the base types. Similar measures can be taken
3333 for user defined types, withe the type living in the least upper bound
3334 of the levels where the types contained data live.
3337 For example we might define our disjunction to be
3339 \myarg\myfun{$\vee$}\myarg : \mytyp_{100} \myarr \mytyp_{100} \myarr \mytyp_{100}
3341 And hope that $\mytyp_{100}$ will be large enough to fit all the types
3342 that we want to use with our disjunction. However, there are two
3343 problems with this. First, clumsiness of having to manually specify the
3344 size of types is still there. More importantly, if we want to use
3345 $\myfun{$\vee$}$ itself as an argument to other type-formers, we need to
3346 make sure that those allow for types at least as large as
3349 A better option is to employ a mechanised version of what Russell called
3350 \emph{typical ambiguity}: we let the user live under the illusion that
3351 $\mytyp : \mytyp$, but check that the statements about types are
3352 consistent under the hood. $\mykant$\ implements this following the
3353 plan given by \cite{Huet1988}. See also \cite{Harper1991} for a
3354 published reference, although describing a more complex system allowing
3355 for both explicit and explicit hierarchy at the same time.
3357 We define a partial ordering on the levels, with both weak ($\le$) and
3358 strong ($<$) constraints, the laws governing them being the same as the
3359 ones governing $<$ and $\le$ for the natural numbers. Each occurrence
3360 of $\mytyp$ is decorated with a unique reference. We keep a set of
3361 constraints regarding the ordering of each occurrence of $\mytyp$, each
3362 represented by its unique reference. We add new constraints as we type
3363 check, generating new references when needed.
3365 For example, when type checking the type $\mytyp\, r_1$, where $r_1$
3366 denotes the unique reference assigned to that term, we will generate a
3367 new fresh reference $\mytyp\, r_2$, and add the constraint $r_1 < r_2$
3368 to the set. When type checking $\myctx \vdash
3369 \myfora{\myb{x}}{\mytya}{\mytyb}$, if $\myctx \vdash \mytya : \mytyp\,
3370 r_1$ and $\myctx; \myb{x} : \mytyb \vdash \mytyb : \mytyp\,r_2$; we will
3371 generate new reference $r$ and add $r_1 \le r$ and $r_2 \le r$ to the
3374 If at any point the constraint set becomes inconsistent, type checking
3375 fails. Moreover, when comparing two $\mytyp$ terms we equate their
3376 respective references with two $\le$ constraints. Implementation
3377 details are given in Section \ref{sec:hier-impl}.
3379 Another more flexible but also more verbose alternative is the one
3380 chosen by Agda, where levels can be quantified so that the relationship
3381 between arguments and result in type formers can be explicitly
3384 \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}
3386 Inference algorithms to automatically derive this kind of relationship
3387 are currently subject of research. We chose less flexible but more
3388 concise way, since it is easier to implement and better understood.
3390 \subsection{Observational equality, \mykant\ style}
3392 There are two correlated differences between $\mykant$\ and the theory
3393 used to present OTT. The first is that in $\mykant$ we have a type
3394 hierarchy, which lets us, for example, abstract over types. The second
3395 is that we let the user define inductive types and records.
3397 Reconciling propositions for OTT and a hierarchy had already been
3398 investigated by Conor McBride,\footnote{See
3399 \url{http://www.e-pig.org/epilogue/index.html?p=1098.html}.} and we
3400 follow his broad design plan, although with some innovation. Most of
3401 the work, as an extension of elaboration, is to handle reduction rules
3402 and coercions for data types---both type constructors and data
3405 \subsubsection{The \mykant\ prelude, and $\myprop$ositions}
3407 Before defining $\myprop$, we define some basic types inside $\mykant$,
3408 as the target for the $\myprop$ decoder.
3410 \begin{mydef}[\mykant' propositional prelude]\ \end{mydef}
3413 \myadt{\mytyc{Empty}}{}{ }{ } \\
3414 \myfun{absurd} : (\myb{A} {:} \mytyp) \myarr \mytyc{Empty} \myarr \myb{A} \mapsto \\
3415 \myind{2} \myabs{\myb{A\ \myb{bot}}}{\mytyc{Empty}.\myfun{elim} \myappsp \myb{bot} \myappsp (\myabs{\_}{\myb{A}})} \\
3418 \myreco{\mytyc{Unit}}{}{}{ } \\ \ \\
3420 \myreco{\mytyc{Prod}}{\myappsp (\myb{A}\ \myb{B} {:} \mytyp)}{ }{\myfun{fst} : \myb{A}, \myfun{snd} : \myb{B} }
3424 \begin{mydef}[Propositions and decoding]\ \end{mydef}
3428 \begin{array}{r@{\ }c@{\ }l}
3429 \mytmsyn & ::= & \cdots \mysynsep \myprdec{\myprsyn} \\
3430 \myprsyn & ::= & \mybot \mysynsep \mytop \mysynsep \myprsyn \myand \myprsyn \mysynsep \myprfora{\myb{x}}{\mytmsyn}{\myprsyn}
3435 \mydesc{proposition decoding:}{\myprdec{\mytmsyn} \myred \mytmsyn}{
3438 \begin{array}{l@{\ }c@{\ }l}
3439 \myprdec{\mybot} & \myred & \myempty \\
3440 \myprdec{\mytop} & \myred & \myunit
3445 \begin{array}{r@{ }c@{ }l@{\ }c@{\ }l}
3446 \myprdec{&\myse{P} \myand \myse{Q} &} & \myred & \mytyc{Prod} \myappsp \myprdec{\myse{P}} \myappsp \myprdec{\myse{Q}} \\
3447 \myprdec{&\myprfora{\myb{x}}{\mytya}{\myse{P}} &} & \myred &
3448 \myfora{\myb{x}}{\mytya}{\myprdec{\myse{P}}}
3454 We will overload the $\myand$ symbol to define `nested' products, and
3455 $\myproj{n}$ to project elements from them, so that
3458 \mytya \myand \mytyb = \mytya \myand (\mytyb \myand \mytop) \\
3459 \mytya \myand \mytyb \myand \myse{C} = \mytya \myand (\mytyb \myand (\myse{C} \myand \mytop)) \\
3461 \myproj{1} : \myprdec{\mytya \myand \mytyb} \myarr \myprdec{\mytya} \\
3462 \myproj{2} : \myprdec{\mytya \myand \mytyb \myand \myse{C}} \myarr \myprdec{\mytyb} \\
3466 And so on, so that $\myproj{n}$ will work with all products with at
3467 least than $n$ elements. Logically a 0-ary $\myand$ will correspond to
3470 \subsubsection{Some OTT examples}
3472 Before presenting the direction that $\mykant$\ takes, let us consider
3473 two examples of use-defined data types, and the result we would expect
3474 given what we already know about OTT, assuming the same propositional
3479 \item[Product types] Let us consider first the already mentioned
3480 dependent product, using the alternate name $\mysigma$\footnote{For
3481 extra confusion, `dependent products' are often called `dependent
3482 sums' in the literature, referring to the interpretation that
3483 identifies the first element as a `tag' deciding the type of the
3484 second element, which lets us recover sum types (disjuctions), as we
3485 saw in Section \ref{sec:depprod}. Thus, $\mysigma$.} to
3486 avoid confusion with the $\mytyc{Prod}$ in the prelude:
3489 \myreco{\mysigma}{\myappsp (\myb{A} {:} \mytyp) \myappsp (\myb{B} {:} \myb{A} \myarr \mytyp)}{\\ \myind{2}}{\myfst : \myb{A}, \mysnd : \myapp{\myb{B}}{\myb{fst}}}
3492 First type-level equality. The result we want is
3495 \mysigma \myappsp \mytya_1 \myappsp \mytyb_1 \myeq \mysigma \myappsp \mytya_2 \myappsp \mytyb_2 \myred \\
3496 \myind{2} \mytya_1 \myeq \mytya_2 \myand \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{\myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2}} \myimpl \myapp{\mytyb_1}{\myb{x_1}} \myeq \myapp{\mytyb_2}{\myb{x_2}}}
3499 The difference here is that in the original presentation of OTT the
3500 type binders are explicit, while here $\mytyb_1$ and $\mytyb_2$ are
3501 functions returning types. We can do this thanks to the type
3502 hierarchy, and this hints at the fact that heterogeneous equality will
3503 have to allow $\mytyp$ `to the right of the colon'. Indeed,
3504 heterogeneous equalities involving abstractions over types will
3505 provide the solution to simplify the equality above.
3507 If we take, just like we saw previously in OTT
3510 \myjm{\myse{f}_1}{\myfora{\mytya_1}{\myb{x_1}}{\mytyb_1}}{\myse{f}_2}{\myfora{\mytya_2}{\myb{x_2}}{\mytyb_2}} \myred \\
3511 \myind{2} \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{
3512 \myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2} \myimpl
3513 \myjm{\myapp{\myse{f}_1}{\myb{x_1}}}{\mytyb_1[\myb{x_1}]}{\myapp{\myse{f}_2}{\myb{x_2}}}{\mytyb_2[\myb{x_2}]}
3517 Then we can simply take
3520 \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}
3523 Which will reduce to precisely what we desire, but with an
3524 heterogeneous equalities relating types instead of values:
3527 \mytya_1 \myeq \mytya_2 \myand \myjm{\mytyb_1}{\mytya_1 \myarr \mytyp}{\mytyb_2}{\mytya_2 \myarr \mytyp} \myred \\
3528 \mytya_1 \myeq \mytya_2 \myand
3529 \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{
3530 \myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2} \myimpl
3531 \myjm{\myapp{\mytyb_1}{\myb{x_1}}}{\mytyp}{\myapp{\mytyb_2}{\myb{x_2}}}{\mytyp}
3535 If we pretend for the moment that those heterogeneous equalities were
3536 type equalities, things run smoothly. For what concerns coercions and
3537 quotation, things stay the same (apart from the fact that we apply to
3538 the second argument instead of substituting). We can recognise
3539 records such as $\mysigma$ as such and employ projections in value
3540 equality and coercions; as to not impede progress if not necessary.
3542 \item[Lists] Now for finite lists, which will give us a taste for data
3546 \myadt{\mylist}{\myappsp (\myb{A} {:} \mytyp)}{ }{\mydc{nil} \mydcsep \mydc{cons} \myappsp \myb{A} \myappsp (\myapp{\mylist}{\myb{A}})}
3549 Type equality is simple---we only need to compare the parameter:
3551 \mylist \myappsp \mytya_1 \myeq \mylist \myappsp \mytya_2 \myred \mytya_1 \myeq \mytya_2
3553 For coercions, we transport based on the constructor, recycling the
3554 proof for the inductive occurrence:
3556 \begin{array}{@{}l@{\ }c@{\ }l}
3557 \mycoe \myappsp (\mylist \myappsp \mytya_1) \myappsp (\mylist \myappsp \mytya_2) \myappsp \myse{Q} \myappsp \mydc{nil} & \myred & \mydc{nil} \\
3558 \mycoe \myappsp (\mylist \myappsp \mytya_1) \myappsp (\mylist \myappsp \mytya_2) \myappsp \myse{Q} \myappsp (\mydc{cons} \myappsp \mytmm \myappsp \mytmn) & \myred & \\
3559 \multicolumn{3}{l}{\myind{2} \mydc{cons} \myappsp (\mycoe \myappsp \mytya_1 \myappsp \mytya_2 \myappsp \myse{Q} \myappsp \mytmm) \myappsp (\mycoe \myappsp (\mylist \myappsp \mytya_1) \myappsp (\mylist \myappsp \mytya_2) \myappsp \myse{Q} \myappsp \mytmn)}
3562 Value equality is unsurprising---we match the constructors, and
3563 return bottom for mismatches. However, we also need to equate the
3564 parameter in $\mydc{nil}$:
3566 \begin{array}{r@{ }c@{\ }c@{\ }c@{}l@{\ }c@{\ }r@{}c@{\ }c@{\ }c@{}l@{\ }l}
3567 (& \mydc{nil} & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{nil} & : & \myapp{\mylist}{\mytya_2} &) \myred \mytya_1 \myeq \mytya_2 \\
3568 (& \mydc{cons} \myappsp \mytmm_1 \myappsp \mytmn_1 & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{cons} \myappsp \mytmm_2 \myappsp \mytmn_2 & : & \myapp{\mylist}{\mytya_2} &) \myred \\
3569 & \multicolumn{11}{@{}l}{ \myind{2}
3570 \myjm{\mytmm_1}{\mytya_1}{\mytmm_2}{\mytya_2} \myand \myjm{\mytmn_1}{\myapp{\mylist}{\mytya_1}}{\mytmn_2}{\myapp{\mylist}{\mytya_2}}
3572 (& \mydc{nil} & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{cons} \myappsp \mytmm_2 \myappsp \mytmn_2 & : & \myapp{\mylist}{\mytya_2} &) \myred \mybot \\
3573 (& \mydc{cons} \myappsp \mytmm_1 \myappsp \mytmn_1 & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{nil} & : & \myapp{\mylist}{\mytya_2} &) \myred \mybot
3578 \subsubsection{Only one equality}
3580 Given the examples above, a more `flexible' heterogeneous equality must
3581 emerge, since of the fact that in $\mykant$ we re-gain the possibility
3582 of abstracting and in general handling types in a way that was not
3583 possible in the original OTT presentation. Moreover, we found that the
3584 rules for value equality work very well if used with user defined type
3585 abstractions---for example in the case of dependent products we recover
3586 the original definition with explicit binders, in a very simple manner.
3588 \begin{mydef}[Propositions, coercions, coherence, equalities and
3589 equality reduction for \mykant] See Figure \ref{fig:kant-eq-red}.
3592 \begin{mydef}[Type equality in \mykant]
3593 We define $\mytya \myeq \mytyb$ as an abbreviation for
3594 $\myjm{\mytya}{\mytyp}{\mytyb}{\mytyp}$.
3597 In fact, we can drop a separate notion of type-equality, which will
3598 simply be served by $\myjm{\mytya}{\mytyp}{\mytyb}{\mytyp}$. We shall
3599 still distinguish equalities relating types for hierarchical
3600 purposes. We exploit record to perform $\eta$-expansion. Moreover,
3601 given the nested $\myand$s, values of data types with zero constructors
3602 (such as $\myempty$) and records with zero destructors (such as
3603 $\myunit$) will be automatically always identified as equal.
3610 \begin{array}{r@{\ }c@{\ }l}
3611 \mytmsyn & ::= & \cdots \mysynsep \mycoee{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \mysynsep
3612 \mycohh{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
3613 \myprsyn & ::= & \cdots \mysynsep \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
3620 \mydesc{typing:}{\myctx \vdash \mytmsyn \Leftrightarrow \mytmsyn}{
3623 \AxiomC{$\mychk{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
3624 \AxiomC{$\mychk{\mytmt}{\mytya}$}
3625 \BinaryInfC{$\myinf{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}$}
3628 \AxiomC{$\mychk{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
3629 \AxiomC{$\mychk{\mytmt}{\mytya}$}
3630 \BinaryInfC{$\myinf{\mycohh{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\myprdec{\myjm{\mytmt}{\mytya}{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}}}$}
3637 \mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
3640 \AxiomC{\phantom{$\myjud{\myse{P}}{\myprop}$}}
3641 \UnaryInfC{$\myjud{\mytop}{\myprop}$}
3643 \UnaryInfC{$\myjud{\mybot}{\myprop}$}
3646 \AxiomC{$\myjud{\myse{P}}{\myprop}$}
3647 \AxiomC{$\myjud{\myse{Q}}{\myprop}$}
3648 \BinaryInfC{$\myjud{\myse{P} \myand \myse{Q}}{\myprop}$}
3650 \UnaryInfC{\phantom{$\myjud{\mybot}{\myprop}$}}
3659 \phantom{\myjud{\myse{A}}{\mytyp} \hspace{0.8cm} \myjud{\mytmm}{\myse{A}}} \\
3660 \myjud{\myse{A}}{\mytyp}\hspace{0.8cm}
3661 \myjudd{\myctx; \myb{x} : \mytya}{\myse{P}}{\myprop}
3664 \UnaryInfC{$\myjud{\myprfora{\myb{x}}{\mytya}{\myse{P}}}{\myprop}$}
3669 \myjud{\myse{A}}{\mytyp} \hspace{0.8cm} \myjud{\mytmm}{\myse{A}} \\
3670 \myjud{\myse{B}}{\mytyp} \hspace{0.8cm} \myjud{\mytmn}{\myse{B}}
3673 \UnaryInfC{$\myjud{\myjm{\mytmm}{\myse{A}}{\mytmn}{\myse{B}}}{\myprop}$}
3680 \mydesc{equality reduction:}{\myctx \vdash \myprsyn \myred \myprsyn}{
3684 \UnaryInfC{$\myctx \vdash \myjm{\mytyp}{\mytyp}{\mytyp}{\mytyp} \myred \mytop$}
3688 \UnaryInfC{$\myctx \vdash \myjm{\myprdec{\myse{P}}}{\mytyp}{\myprdec{\myse{Q}}}{\mytyp} \myred \mytop$}
3696 \begin{array}{@{}r@{\ }l}
3698 \myjm{\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}}{\mytyp}{\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}}{\mytyp} \myred \\
3699 & \myind{2} \mytya_2 \myeq \mytya_1 \myand \myprfora{\myb{x_2}}{\mytya_2}{\myprfora{\myb{x_1}}{\mytya_1}{
3700 \myjm{\myb{x_2}}{\mytya_2}{\myb{x_1}}{\mytya_1} \myimpl \mytyb_1[\myb{x_1}] \myeq \mytyb_2[\myb{x_2}]
3710 \begin{array}{@{}r@{\ }l}
3712 \myjm{\myse{f}_1}{\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}}{\myse{f}_2}{\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}} \myred \\
3713 & \myind{2} \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{
3714 \myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2} \myimpl
3715 \myjm{\myapp{\myse{f}_1}{\myb{x_1}}}{\mytyb_1[\myb{x_1}]}{\myapp{\myse{f}_2}{\myb{x_2}}}{\mytyb_2[\myb{x_2}]}
3724 \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
3726 \begin{array}{r@{\ }l}
3728 \myjm{\mytyc{D} \myappsp \vec{A}}{\mytyp}{\mytyc{D} \myappsp \vec{B}}{\mytyp} \myred \\
3729 & \myind{2} \mybigand_{i = 1}^n (\myjm{\mytya_n}{\myhead(\mytele(A_1 \cdots A_{i-1}))}{\mytyb_i}{\myhead(\mytele(B_1 \cdots B_{i-1}))})
3738 \mydataty(\mytyc{D}, \myctx)\hspace{0.8cm}
3739 \mytyc{D}.\mydc{c} : \mytele;\mytele' \myarr \mytyc{D} \myappsp \mytelee \in \myctx \hspace{0.8cm}
3740 \mytele_A = (\mytele;\mytele')\vec{A}\hspace{0.8cm}
3741 \mytele_B = (\mytele;\mytele')\vec{B}
3745 \begin{array}{@{}l@{\ }l}
3746 \myctx \vdash & \myjm{\mytyc{D}.\mydc{c} \myappsp \vec{\myse{l}}}{\mytyc{D} \myappsp \vec{A}}{\mytyc{D}.\mydc{c} \myappsp \vec{\myse{r}}}{\mytyc{D} \myappsp \vec{B}} \myred \\
3747 & \myind{2} \mybigand_{i=1}^n(\myjm{\mytmm_i}{\myhead(\mytele_A (\mytya_i \cdots \mytya_{i-1}))}{\mytmn_i}{\myhead(\mytele_B (\mytyb_i \cdots \mytyb_{i-1}))})
3754 \AxiomC{$\mydataty(\mytyc{D}, \myctx)$}
3756 \myctx \vdash \myjm{\mytyc{D}.\mydc{c} \myappsp \vec{\myse{l}}}{\mytyc{D} \myappsp \vec{A}}{\mytyc{D}.\mydc{c'} \myappsp \vec{\myse{r}}}{\mytyc{D} \myappsp \vec{B}} \myred \mybot
3764 \myisreco(\mytyc{D}, \myctx)\hspace{0.8cm}
3765 \mytyc{D}.\myfun{f}_i : \mytele; (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr \myse{F}_i \in \myctx\\
3769 \begin{array}{@{}l@{\ }l}
3770 \myctx \vdash & \myjm{\myse{l}}{\mytyc{D} \myappsp \vec{A}}{\myse{r}}{\mytyc{D} \myappsp \vec{B}} \myred \\ & \myind{2} \mybigand_{i=1}^n(\myjm{\mytyc{D}.\myfun{f}_1 \myappsp \myse{l}}{(\mytele; (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr \myse{F}_i)(\vec{\mytya};\myse{l})}{\mytyc{D}.\myfun{f}_i \myappsp \myse{r}}{(\mytele; (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr \myse{F}_i)(\vec{\mytyb};\myse{r})})
3777 \UnaryInfC{$\myjm{\mytmm}{\mytya}{\mytmn}{\mytyb} \myred \mybot\ \text{if $\mytya$ and $\mytyb$ are canonical types.}$}
3780 \caption{Propositions and equality reduction in $\mykant$. We assume
3781 the presence of $\mydataty$ and $\myisreco$ as operations on the
3782 context to recognise whether a user defined type is a data type or a
3784 \label{fig:kant-eq-red}
3787 \subsubsection{Coercions}
3789 For coercions the algorithm is messier and not reproduced here for lack
3790 of a decent notation---the details are hairy but uninteresting. To give
3791 an idea of the possible complications, let us conceive a type that
3792 showcases trouble not arising in the previous examples.
3795 \myadt{\mytyc{Max}}{\myappsp (\myb{A} {:} \mynat \myarr \mytyp) \myappsp (\myb{B} {:} (\myb{x} {:} \mynat) \myarr \myb{A} \myappsp \myb{x} \myarr \mytyp) \myappsp (\myb{k} {:} \mynat)}{ \\ \myind{2}}{
3796 \mydc{max} \myappsp (\myb{A} \myappsp \myb{k}) \myappsp (\myb{x} {:} \mynat) \myappsp (\myb{a} {:} \myb{A} \myappsp \myb{x}) \myappsp (\myb{B} \myappsp \myb{x} \myappsp \myb{a})
3800 For type equalities we will have
3802 \begin{array}{@{}l@{\ }l}
3803 \myjm{\mytyc{Max} \myappsp \mytya_1 \myappsp \mytyb_1 \myappsp \myse{k}_1}{\mytyp}{\mytyc{Max} \myappsp \mytya_2 \myappsp \myappsp \mytyb_2 \myappsp \myse{k}_2}{\mytyp} & \myred \\[0.2cm]
3805 \myjm{\mytya_1}{\mynat \myarr \mytyp}{\mytya_2}{\mynat \myarr \mytyp} \myand \\
3806 \myjm{\mytyb_1}{(\myb{x} {:} \mynat) \myarr \mytya_1 \myappsp \myb{x} \myarr \mytyp}{\mytyb_2}{(\myb{x} {:} \mynat) \myarr \mytya_2 \myappsp \myb{x} \myarr \mytyp} \\
3807 \myjm{\myse{k}_1}{\mynat}{\myse{k}_2}{\mynat}
3808 \end{array} & \myred \\[0.7cm]
3810 (\mynat \myeq \mynat \myand (\myprfora{\myb{x_1}\, \myb{x_2}}{\mynat}{\myjm{\myb{x_1}}{\mynat}{\myb{x_2}}{\mynat} \myimpl \myapp{\mytya_1}{\myb{x_1}} \myeq \myapp{\mytya_2}{\myb{x_2}}})) \myand \\
3811 (\mynat \myeq \mynat \myand \left(
3813 \myprfora{\myb{x_1}\, \myb{x_2}}{\mynat}{\myjm{\myb{x_1}}{\mynat}{\myb{x_2}}{\mynat} \myimpl \\ \myjm{\mytyb_1 \myappsp \myb{x_1}}{\mytya_1 \myappsp \myb{x_1} \myarr \mytyp}{\mytyb_2 \myappsp \myb{x_2}}{\mytya_2 \myappsp \myb{x_2} \myarr \mytyp}}
3816 \myjm{\myse{k}_1}{\mynat}{\myse{k}_2}{\mynat}
3817 \end{array} & \myred \\[0.9cm]
3819 (\mytop \myand (\myprfora{\myb{x_1}\, \myb{x_2}}{\mynat}{\myjm{\myb{x_1}}{\mynat}{\myb{x_2}}{\mynat} \myimpl \myapp{\mytya_1}{\myb{x_1}} \myeq \myapp{\mytya_2}{\myb{x_2}}})) \myand \\
3820 (\mytop \myand \left(
3822 \myprfora{\myb{x_1}\, \myb{x_2}}{\mynat}{\myjm{\myb{x_1}}{\mynat}{\myb{x_2}}{\mynat} \myimpl \\
3823 \myprfora{\myb{y_1}}{\mytya_1 \myappsp \myb{x_1}}{\myprfora{\myb{y_2}}{\mytya_2 \myappsp \myb{x_2}}{\myjm{\myb{y_1}}{\mytya_1 \myappsp \myb{x_1}}{\myb{y_2}}{\mytya_2 \myappsp \myb{x_2}} \myimpl \\
3824 \mytyb_1 \myappsp \myb{x_1} \myappsp \myb{y_1} \myeq \mytyb_2 \myappsp \myb{x_2} \myappsp \myb{y_2}}}}
3827 \myjm{\myse{k}_1}{\mynat}{\myse{k}_2}{\mynat}
3831 The result, while looking complicated, is actually saying something
3832 simple---given equal inputs, the parameters for $\mytyc{Max}$ will
3833 return equal types. Moreover, we have evidence that the two $\myb{k}$
3834 parameters are equal. When coercing, we need to mechanically generate
3835 one proof of equality for each argument, and then coerce:
3838 \mycoee{(\mytyc{Max} \myappsp \mytya_1 \myappsp \mytyb_1 \myappsp \myse{k}_1)}{(\mytyc{Max} \myappsp \mytya_2 \myappsp \mytyb_2 \myappsp \myse{k}_2)}{\myse{Q}}{(\mydc{max} \myappsp \myse{ak}_1 \myappsp \myse{n}_1 \myappsp \myse{a}_1 \myappsp \myse{b}_1)} \myred \\
3840 \begin{array}[t]{l@{\ }l@{\ }c@{\ }l}
3841 \mysyn{let} & \myb{Q_{Ak}} & \mapsto & \myhole{?} : \myprdec{\mytya_1 \myappsp \myse{k}_1 \myeq \mytya_2 \myappsp \myse{k}_2} \\
3842 & \myb{ak_2} & \mapsto & \mycoee{(\mytya_1 \myappsp \myse{k}_1)}{(\mytya_2 \myappsp \myse{k}_2)}{\myb{Q_{Ak}}}{\myse{ak_1}} : \mytya_1 \myappsp \myse{k}_2 \\
3843 & \myb{Q_{\mathbb{N}}} & \mapsto & \myhole{?} : \myprdec{\mynat \myeq \mynat} \\
3844 & \myb{n_2} & \mapsto & \mycoee{\mynat}{\mynat}{\myb{Q_{\mathbb{N}}}}{\myse{n_1}} : \mynat \\
3845 & \myb{Q_A} & \mapsto & \myhole{?} : \myprdec{\mytya_1 \myappsp \myse{n_1} \myeq \mytya_2 \myappsp \myb{n_2}} \\
3846 & \myb{a_2} & \mapsto & \mycoee{(\mytya_1 \myappsp \myse{n_1})}{(\mytya_2 \myappsp \myb{n_2})}{\myb{Q_A}} : \mytya_2 \myappsp \myb{n_2} \\
3847 & \myb{Q_B} & \mapsto & \myhole{?} : \myprdec{\mytyb_1 \myappsp \myse{n_1} \myappsp \myse{a}_1 \myeq \mytyb_1 \myappsp \myb{n_2} \myappsp \myb{a_2}} \\
3848 & \myb{b_2} & \mapsto & \mycoee{(\mytyb_1 \myappsp \myse{n_1} \myappsp \myse{a_1})}{(\mytyb_2 \myappsp \myb{n_2} \myappsp \myb{a_2})}{\myb{Q_B}} : \mytyb_2 \myappsp \myb{n_2} \myappsp \myb{a_2} \\
3849 \mysyn{in} & \multicolumn{3}{@{}l}{\mydc{max} \myappsp \myb{ak_2} \myappsp \myb{n_2} \myappsp \myb{a_2} \myappsp \myb{b_2}}
3853 For equalities regarding types that are external to the data type we can
3854 derive a proof by reflexivity by invoking $\mydc{refl}$ as defined in
3855 Section \ref{sec:lazy}, and the instantiate arguments if we need too.
3856 In this case, for $\mynat$, we do not have any arguments. For
3857 equalities concerning arguments of the type constructor or already
3858 coerced arguments of the type constructor we have to refer to the right
3859 proof and use $\mycoh$erence when due, which is where the technical
3863 \mycoee{(\mytyc{Max} \myappsp \mytya_1 \myappsp \mytyb_1 \myappsp \myse{k}_1)}{(\mytyc{Max} \myappsp \mytya_2 \myappsp \mytyb_2 \myappsp \myse{k}_2)}{\myse{Q}}{(\mydc{max} \myappsp \myse{ak}_1 \myappsp \myse{n}_1 \myappsp \myse{a}_1 \myappsp \myse{b}_1)} \myred \\
3865 \begin{array}[t]{l@{\ }l@{\ }c@{\ }l}
3866 \mysyn{let} & \myb{Q_{Ak}} & \mapsto & (\myproj{2} \myappsp (\myproj{1} \myappsp \myse{Q})) \myappsp \myse{k_1} \myappsp \myse{k_2} \myappsp (\myproj{3} \myappsp \myse{Q}) : \myprdec{\mytya_1 \myappsp \myse{k}_1 \myeq \mytya_2 \myappsp \myse{k}_2} \\
3867 & \myb{ak_2} & \mapsto & \mycoee{(\mytya_1 \myappsp \myse{k}_1)}{(\mytya_2 \myappsp \myse{k}_2)}{\myb{Q_{Ak}}}{\myse{ak_1}} : \mytya_1 \myappsp \myse{k}_2 \\
3868 & \myb{Q_{\mathbb{N}}} & \mapsto & \mydc{refl} \myappsp \mynat : \myprdec{\mynat \myeq \mynat} \\
3869 & \myb{n_2} & \mapsto & \mycoee{\mynat}{\mynat}{\myb{Q_{\mathbb{N}}}}{\myse{n_1}} : \mynat \\
3870 & \myb{Q_A} & \mapsto & (\myproj{2} \myappsp (\myproj{1} \myappsp \myse{Q})) \myappsp \myse{n_1} \myappsp \myb{n_2} \myappsp (\mycohh{\mynat}{\mynat}{\myb{Q_{\mathbb{N}}}}{\myse{n_1}}) : \myprdec{\mytya_1 \myappsp \myse{n_1} \myeq \mytya_2 \myappsp \myb{n_2}} \\
3871 & \myb{a_2} & \mapsto & \mycoee{(\mytya_1 \myappsp \myse{n_1})}{(\mytya_2 \myappsp \myb{n_2})}{\myb{Q_A}} : \mytya_2 \myappsp \myb{n_2} \\
3872 & \myb{Q_B} & \mapsto & (\myproj{2} \myappsp (\myproj{2} \myappsp \myse{Q})) \myappsp \myse{n_1} \myappsp \myb{n_2} \myappsp \myb{Q_{\mathbb{N}}} \myappsp \myse{a_1} \myappsp \myb{a_2} \myappsp (\mycohh{(\mytya_1 \myappsp \myse{n_1})}{(\mytya_2 \myappsp \myse{n_2})}{\myb{Q_A}}{\myse{a_1}}) : \myprdec{\mytyb_1 \myappsp \myse{n_1} \myappsp \myse{a}_1 \myeq \mytyb_1 \myappsp \myb{n_2} \myappsp \myb{a_2}} \\
3873 & \myb{b_2} & \mapsto & \mycoee{(\mytyb_1 \myappsp \myse{n_1} \myappsp \myse{a_1})}{(\mytyb_2 \myappsp \myb{n_2} \myappsp \myb{a_2})}{\myb{Q_B}} : \mytyb_2 \myappsp \myb{n_2} \myappsp \myb{a_2} \\
3874 \mysyn{in} & \multicolumn{3}{@{}l}{\mydc{max} \myappsp \myb{ak_2} \myappsp \myb{n_2} \myappsp \myb{a_2} \myappsp \myb{b_2}}
3879 \subsubsection{$\myprop$ and the hierarchy}
3881 We shall have, at each universe level, not only a $\mytyp_l$ but also a
3882 $\myprop_l$. Where will propositions placed in the type hierarchy? The
3883 main indicator is the decoding operator, since it converts into things
3884 that already live in the hierarchy. For example, if we have
3886 \myprdec{\mynat \myarr \mybool \myeq \mynat \myarr \mybool} \myred
3887 \mytop \myand ((\myb{x}\, \myb{y} : \mynat) \myarr \mytop \myarr \mytop)
3889 we will better make sure that the `to be decoded' is at level compatible
3890 (read: larger) with its reduction. In the example above, we'll have
3891 that proposition to be at least as large as the type of $\mynat$, since
3892 the reduced proof will abstract over it. Pretending that we had
3893 explicit, non cumulative levels, it would be tempting to have
3896 \AxiomC{$\myjud{\myse{Q}}{\myprop_l}$}
3897 \UnaryInfC{$\myjud{\myprdec{\myse{Q}}}{\mytyp_l}$}
3900 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
3901 \AxiomC{$\myjud{\mytyb}{\mytyp_l}$}
3902 \BinaryInfC{$\myjud{\myjm{\mytya}{\mytyp_{l}}{\mytyb}{\mytyp_{l}}}{\myprop_l}$}
3906 $\mybot$ and $\mytop$ living at any level, $\myand$ and $\forall$
3907 following rules similar to the ones for $\myprod$ and $\myarr$ in
3908 Section \ref{sec:itt}. However, we need to be careful with value
3909 equality since for example we have that
3911 \myprdec{\myjm{\myse{f}_1}{\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}}{\myse{f}_2}{\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}}}
3913 \myfora{\myb{x_1}}{\mytya_1}{\myfora{\myb{x_2}}{\mytya_2}{\cdots}}
3915 where the proposition decodes into something of at least type $\mytyp_l$, where
3916 $\mytya_l : \mytyp_l$ and $\mytyb_l : \mytyp_l$. We can resolve this
3917 tension by making all equalities larger:
3919 \AxiomC{$\myjud{\mytmm}{\mytya}$}
3920 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
3921 \AxiomC{$\myjud{\mytmn}{\mytyb}$}
3922 \AxiomC{$\myjud{\mytyb}{\mytyp_l}$}
3923 \QuaternaryInfC{$\myjud{\myjm{\mytmm}{\mytya}{\mytmm}{\mytya}}{\myprop_l}$}
3925 This is disappointing, since type equalities will be needlessly large:
3926 $\myprdec{\myjm{\mytya}{\mytyp_l}{\mytyb}{\mytyp_l}} : \mytyp_{l + 1}$.
3928 However, considering that our theory is cumulative, we can do better.
3929 Assuming rules for $\myprop$ cumulativity similar to the ones for
3930 $\mytyp$, we will have (with the conversion rule reproduced as a
3934 \AxiomC{$\myctx \vdash \mytya \mycumul \mytyb$}
3935 \AxiomC{$\myjud{\mytmt}{\mytya}$}
3936 \BinaryInfC{$\myjud{\mytmt}{\mytyb}$}
3939 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
3940 \AxiomC{$\myjud{\mytyb}{\mytyp_l}$}
3941 \BinaryInfC{$\myjud{\myjm{\mytya}{\mytyp_{l}}{\mytyb}{\mytyp_{l}}}{\myprop_l}$}
3947 \AxiomC{$\myjud{\mytmm}{\mytya}$}
3948 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
3949 \AxiomC{$\myjud{\mytmn}{\mytyb}$}
3950 \AxiomC{$\myjud{\mytyb}{\mytyp_l}$}
3951 \AxiomC{$\mytya$ and $\mytyb$ are not $\mytyp_{l'}$}
3952 \QuinaryInfC{$\myjud{\myjm{\mytmm}{\mytya}{\mytmm}{\mytya}}{\myprop_l}$}
3956 That is, we are small when we can (type equalities) and large otherwise.
3957 This would not work in a non-cumulative theory because subject reduction
3958 would not hold. Consider for instance
3960 \myjm{\mynat}{\myITE{\mytrue}{\mytyp_0}{\mytyp_0}}{\mybool}{\myITE{\mytrue}{\mytyp_0}{\mytyp_0}}
3964 \[\myjm{\mynat}{\mytyp_0}{\mybool}{\mytyp_0} : \myprop_0 \]
3965 We need members of $\myprop_0$ to be members of $\myprop_1$ too, which
3966 will be the case with cumulativity. This is not the most elegant of
3967 systems, but it buys us a cheap type level equality without having to
3968 replicate functionality with a dedicated construct.
3970 \subsubsection{Quotation and definitional equality}
3971 \label{sec:kant-irr}
3973 Now we can give an account of definitional equality, by explaining how
3974 to perform quotation (as defined in Section \ref{sec:eta-expand})
3975 towards the goal described in Section \ref{sec:ott-quot}.
3979 \item Perform $\eta$-expansion on functions and records.
3981 \item As a consequence of the previous point, identify all records with
3982 no projections as equal, since they will have only one element.
3984 \item Identify all members of types with no elements as equal.
3986 \item Identify all equivalent proofs as equal---with `equivalent proof'
3987 we mean those proving the same propositions.
3989 \item Advance coercions working across definitionally equal types.
3991 Towards these goals and following the intuition between bidirectional
3992 type checking we define two mutually recursive functions, one quoting
3993 canonical terms against their types (since we need the type to type check
3994 canonical terms), one quoting neutral terms while recovering their
3995 types. The full procedure for quotation is shown in Figure
3996 \ref{fig:kant-quot}. We $\boxed{\text{box}}$ the neutral proofs and
3997 neutral members of empty types, following the notation in
3998 \cite{Altenkirch2007}, and we make use of $\mydefeq_{\mybox}$ which
3999 compares terms syntactically up to $\alpha$-renaming, but also up to
4000 equivalent proofs: we consider all boxed content as equal.
4002 Our quotation will work on normalised terms, so that all defined values
4003 will have been replaced. Moreover, we match on data type eliminators and
4004 all their arguments, so that $\mynat.\myfun{elim} \myappsp \mytmm
4005 \myappsp \myse{P} \myappsp \vec{\mytmn}$ will stand for
4006 $\mynat.\myfun{elim}$ applied to the scrutinised $\mynat$, the
4007 predicate, and the two cases. This measure can be easily implemented by
4008 checking the head of applications and `consuming' the needed terms.
4011 \mydesc{canonical quotation:}{\mycanquot(\myctx, \mytmsyn : \mytmsyn) \mymetagoes \mytmsyn}{
4014 \begin{array}{@{}l@{}l}
4015 \mycanquot(\myctx,\ \mytmt : \mytyc{D} \myappsp \vec{A} &) \mymetaguard \mymeta{empty}(\myctx, \mytyc{D}) \mymetagoes \boxed{\mytmt} \\
4016 \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)) \\
4017 \mycanquot(\myctx,\ \mytyc{D}.\mydc{c} \myappsp \vec{t} : \mytyc{D} \myappsp \vec{A} &) \mymetagoes \cdots \\
4018 \mycanquot(\myctx,\ \myse{f} : \myfora{\myb{x}}{\mytya}{\mytyb} &) \mymetagoes \myabs{\myb{x}}{\mycanquot(\myctx; \myb{x} : \mytya, \myapp{\myse{f}}{\myb{x}} : \mytyb)} \\
4019 \mycanquot(\myctx,\ \myse{p} : \myprdec{\myse{P}} &) \mymetagoes \boxed{\myse{p}}
4021 \mycanquot(\myctx,\ \mytmt : \mytya &) \mymetagoes \mytmt'\ \text{\textbf{where}}\ \mytmt' : \myarg = \myneuquot(\myctx, \mytmt)
4028 \mydesc{neutral quotation:}{\myneuquot(\myctx, \mytmsyn) \mymetagoes \mytmsyn : \mytmsyn}{
4031 \begin{array}{@{}l@{}l}
4032 \myneuquot(\myctx,\ \myb{x} &) \mymetagoes \myb{x} : \myctx(\myb{x}) \\
4033 \myneuquot(\myctx,\ \mytyp &) \mymetagoes \mytyp : \mytyp \\
4034 \myneuquot(\myctx,\ \myfora{\myb{x}}{\mytya}{\mytyb} & ) \mymetagoes
4035 \myfora{\myb{x}}{\myneuquot(\myctx, \mytya)}{\myneuquot(\myctx; \myb{x} : \mytya, \mytyb)} : \mytyp \\
4036 \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 \\
4037 \myneuquot(\myctx,\ \myprdec{\myjm{\mytmm}{\mytya}{\mytmn}{\mytyb}} &) \mymetagoes \myprdec{\myjm{\mycanquot(\myctx, \mytmm : \mytya)}{\mytya'}{\mycanquot(\myctx, \mytmn : \mytyb)}{\mytyb'}} : \mytyp \\
4038 \multicolumn{2}{@{}l}{\myind{2}\text{\textbf{where}}\ \mytya' : \myarg = \myneuquot(\myctx, \mytya)} \\
4039 \multicolumn{2}{@{}l}{\myind{2}\phantom{\text{\textbf{where}}}\ \mytyb' : \myarg = \myneuquot(\myctx, \mytyb)} \\
4040 \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) \\
4041 \multicolumn{2}{@{}l}{\myind{2}\text{\textbf{where}}\ \mytmt' : \mytyc{D} \myappsp \vec{A} = \myneuquot(\myctx, \mytmt)} \\
4042 \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}) : \myse{P} \myappsp \mytmt \\
4043 \myneuquot(\myctx,\ \mytyc{D}.\myfun{elim} \myappsp \mytmm \myappsp \myse{P} \myappsp \vec{\mytmn} &) \mymetagoes \mytyc{D}.\myfun{elim} \myappsp \mytmm' \myappsp \myneuquot(\myctx, \myse{P}) \cdots : \myse{P} \myappsp \mytmm\\
4044 \multicolumn{2}{@{}l}{\myind{2}\text{\textbf{where}}\ \mytmm' : \mytyc{D} \myappsp \vec{A} = \myneuquot(\myctx, \mytmm)} \\
4045 \myneuquot(\myctx,\ \myapp{\myse{f}}{\mytmt} &) \mymetagoes \myapp{\myse{f'}}{\mycanquot(\myctx, \mytmt : \mytya)} : \mysub{\mytyb}{\myb{x}}{\mytmt} \\
4046 \multicolumn{2}{@{}l}{\myind{2}\text{\textbf{where}}\ \myse{f'} : \myfora{\myb{x}}{\mytya}{\mytyb} = \myneuquot(\myctx, \myse{f})} \\
4047 \myneuquot(\myctx,\ \mycoee{\mytya}{\mytyb}{\myse{Q}}{\mytmt} &) \mymetaguard \myneuquot(\myctx, \mytya) \mydefeq_{\mybox} \myneuquot(\myctx, \mytyb) \mymetagoes \myneuquot(\myctx, \mytmt) \\
4048 \myneuquot(\myctx,\ \mycoee{\mytya}{\mytyb}{\myse{Q}}{\mytmt} &) \mymetagoes
4049 \mycoee{\myneuquot(\myctx, \mytya)}{\myneuquot(\myctx, \mytyb)}{\boxed{\myse{Q}}}{\myneuquot(\myctx, \mytmt)}
4053 \caption{Quotation in \mykant. Along the already used
4054 $\mymeta{record}$ meta-operation on the context we make use of
4055 $\mymeta{empty}$, which checks if a certain type constructor has
4056 zero data constructor. The `data constructor' cases for non-record,
4057 non-empty, data types are omitted for brevity.}
4058 \label{fig:kant-quot}
4061 \subsubsection{Why $\myprop$?}
4063 It is worth to ask if $\myprop$ is needed at all. It is perfectly
4064 possible to have the type checker identify propositional types
4065 automatically, and in fact in some sense we already do during equality
4066 reduction and quotation. However, this has the considerable
4067 disadvantage that we can never identify abstracted
4068 variables\footnote{And in general neutral terms, although we currently
4069 don't have neutral propositions apart from equalities on neutral
4070 terms.} of type $\mytyp$ as $\myprop$, thus forbidding the user to
4071 talk about $\myprop$ explicitly.
4073 This is a considerable impediment, for example when implementing
4074 \emph{quotient types}. With quotients, we let the user specify an
4075 equivalence class over a certain type, and then exploit this in various
4076 way---crucially, we need to be sure that the equivalence given is
4077 propositional, a fact which prevented the use of quotients in dependent
4078 type theories \citep{Jacobs1994}.
4080 \section{\mykant : the practice}
4081 \label{sec:kant-practice}
4083 \epigraph{\emph{It's alive!}}{Henry Frankenstein}
4085 The codebase consists of around 2500 lines of Haskell,\footnote{The full
4086 source code is available under the GPL3 license at
4087 \url{https://github.com/bitonic/kant}. `Kant' was a previous
4088 incarnation of the software, and the name remained.} as reported by
4089 the \texttt{cloc} utility. The high level design is inspired by the
4090 work on various incarnations of Epigram, and specifically by the first
4091 version as described by \cite{McBride2004}.
4093 The author learnt the hard way the implementation challenges for such a
4094 project, and ran out of time while implementing observational equality.
4095 While the constructs and typing rules are present, the machinery to make
4096 it happen (equality reduction, coercions, quotation, etc.) is not
4099 This considered, everything else presented in Section
4100 \ref{sec:kant-theory} is implemented and working well---and in fact all
4101 the examples presented in this thesis, apart from the ones that are
4102 equality related, have been encoded in \mykant\ in the Appendix.
4103 Moreover, given the detailed plan in the previous section, finishing off
4104 should not prove too much work.
4106 The interaction with the user takes place in a loop living in and
4107 updating a context of \mykant\ declarations, which presents itself as in
4108 Figure \ref{fig:kant-web}. Files with lists of declarations can also be
4109 loaded. The REPL is a available both as a command-line application and in
4110 a web interface, which is available at \url{bertus.mazzo.li}.
4112 A REPL cycle starts with the user inputting a \mykant\
4113 declaration or another REPL command, which then goes through various
4114 stages that can end up in a context update, or in failures of various
4115 kind. The process is described diagrammatically in figure
4116 \ref{fig:kant-process}.
4119 {\small\begin{Verbatim}[frame=leftline,xleftmargin=3cm]
4121 Version 0.0, made in London, year 2013.
4123 <decl> Declare value/data type/record
4126 :p <term> Pretty print
4128 :r <file> Reload file (erases previous environment)
4129 :i <name> Info about an identifier
4131 >>> :l data/samples/good/common.ka
4133 >>> :e plus three two
4134 suc (suc (suc (suc (suc zero))))
4135 >>> :t plus three two
4140 \caption{A sample run of the \mykant\ prompt.}
4141 \label{fig:kant-web}
4147 \item[Parse] In this phase the text input gets converted to a sugared
4148 version of the core language. For example, we accept multiple
4149 arguments in arrow types and abstractions, and we represent variables
4150 with names, while as we will see in Section \ref{sec:term-repr} the
4151 final term types uses a \emph{nameless} representation.
4153 \item[Desugar] The sugared declaration is converted to a core term.
4154 Most notably we go from names to nameless.
4156 \item[ConDestr] Short for `Constructors/Destructors', converts
4157 applications of data destructors and constructors to a special form,
4158 to perform bidirectional type checking.
4160 \item[Reference] Occurrences of $\mytyp$ get decorated by a unique reference,
4161 which is necessary to implement the type hierarchy check.
4163 \item[Elaborate/Typecheck/Evaluate] \textbf{Elaboration} converts the
4164 declaration to some context items, which might be a value declaration
4165 (type and body) or a data type declaration (constructors and
4166 destructors). This phase works in tandem with \textbf{Type checking},
4167 which in turns needs to \textbf{Evaluate} terms.
4169 \item[Distill] and report the result. `Distilling' refers to the
4170 process of converting a core term back to a sugared version that the
4171 user can visualise. This can be necessary both to display errors
4172 including terms or to display result of evaluations or type checking
4173 that the user has requested. Among the other things in this stage we
4174 go from nameless back to names by recycling the names that the user
4175 used originally, as to fabricate a term which is as close as possible
4176 to what it originated from.
4178 \item[Pretty print] Format the terms in a nice way, and display the result to
4185 \tikzstyle{block} = [rectangle, draw, text width=5em, text centered, rounded
4186 corners, minimum height=2.5em, node distance=0.7cm]
4188 \tikzstyle{decision} = [diamond, draw, text width=4.5em, text badly
4189 centered, inner sep=0pt, node distance=0.7cm]
4191 \tikzstyle{line} = [draw, -latex']
4193 \tikzstyle{cloud} = [draw, ellipse, minimum height=2em, text width=5em, text
4194 centered, node distance=1.5cm]
4197 \begin{tikzpicture}[auto]
4198 \node [cloud] (user) {User};
4199 \node [block, below left=1cm and 0.1cm of user] (parse) {Parse};
4200 \node [block, below=of parse] (desugar) {Desugar};
4201 \node [block, below=of desugar] (condestr) {ConDestr};
4202 \node [block, below=of condestr] (reference) {Reference};
4203 \node [block, below=of reference] (elaborate) {Elaborate};
4204 \node [block, left=of elaborate] (tycheck) {Typecheck};
4205 \node [block, left=of tycheck] (evaluate) {Evaluate};
4206 \node [decision, right=of elaborate] (error) {Error?};
4207 \node [block, right=of parse] (pretty) {Pretty print};
4208 \node [block, below=of pretty] (distill) {Distill};
4209 \node [block, below=of distill] (update) {Update context};
4211 \path [line] (user) -- (parse);
4212 \path [line] (parse) -- (desugar);
4213 \path [line] (desugar) -- (condestr);
4214 \path [line] (condestr) -- (reference);
4215 \path [line] (reference) -- (elaborate);
4216 \path [line] (elaborate) edge[bend right] (tycheck);
4217 \path [line] (tycheck) edge[bend right] (elaborate);
4218 \path [line] (elaborate) -- (error);
4219 \path [line] (error) edge[out=0,in=0] node [near start] {yes} (distill);
4220 \path [line] (error) -- node [near start] {no} (update);
4221 \path [line] (update) -- (distill);
4222 \path [line] (pretty) -- (user);
4223 \path [line] (distill) -- (pretty);
4224 \path [line] (tycheck) edge[bend right] (evaluate);
4225 \path [line] (evaluate) edge[bend right] (tycheck);
4228 \caption{High level overview of the life of a \mykant\ prompt cycle.}
4229 \label{fig:kant-process}
4232 Here we will review only a sampling of the more interesting
4233 implementation challenges present when implementing an interactive
4238 The syntax of \mykant\ is presented in Figure \ref{fig:syntax}.
4239 Examples showing the usage of most of the constructs---excluding the
4240 OTT-related ones---are present in Appendices \ref{app:kant-itt},
4241 \ref{app:kant-examples}, and \ref{app:hurkens}; plus a tutorial in
4242 Section \ref{sec:type-holes}. The syntax has grown organically with the
4243 needs of the language, and thus is not very sophisticated. The grammar
4244 is specified in and processed by the \texttt{happy} parser generator for
4245 Haskell.\footnote{Available at \url{http://www.haskell.org/happy}.}
4246 Tokenisation is performed by a simple hand written lexer.
4251 \begin{array}{@{\ \ }l@{\ }c@{\ }l}
4252 \multicolumn{3}{@{}l}{\text{A name, in regexp notation.}} \\
4253 \mysee{name} & ::= & \texttt{[a-zA-Z] [a-zA-Z0-9'\_-]*} \\
4254 \multicolumn{3}{@{}l}{\text{A binder might or might not (\texttt{\_}) bind a name.}} \\
4255 \mysee{binder} & ::= & \mytermi{\_} \mysynsep \mysee{name} \\
4256 \multicolumn{3}{@{}l}{\text{A series of typed bindings.}} \\
4257 \mysee{telescope}\, \ \ \ & ::= & (\mytermi{[}\ \mysee{binder}\ \mytermi{:}\ \mysee{term}\ \mytermi{]}){*} \\
4258 \multicolumn{3}{@{}l}{\text{Terms, including propositions.}} \\
4259 \multicolumn{3}{@{}l}{
4260 \begin{array}{@{\ \ }l@{\ }c@{\ }l@{\ \ \ \ \ }l}
4261 \mysee{term} & ::= & \mysee{name} & \text{A variable.} \\
4262 & | & \mytermi{*} & \text{\mytyc{Type}.} \\
4263 & | & \mytermi{\{|}\ \mysee{term}{*}\ \mytermi{|\}} & \text{Type holes.} \\
4264 & | & \mytermi{Prop} & \text{\mytyc{Prop}.} \\
4265 & | & \mytermi{Top} \mysynsep \mytermi{Bot} & \text{$\mytop$ and $\mybot$.} \\
4266 & | & \mysee{term}\ \mytermi{/\textbackslash}\ \mysee{term} & \text{Conjuctions.} \\
4267 & | & \mytermi{[|}\ \mysee{term}\ \mytermi{|]} & \text{Proposition decoding.} \\
4268 & | & \mytermi{coe}\ \mysee{term}\ \mysee{term}\ \mysee{term}\ \mysee{term} & \text{Coercion.} \\
4269 & | & \mytermi{coh}\ \mysee{term}\ \mysee{term}\ \mysee{term}\ \mysee{term} & \text{Coherence.} \\
4270 & | & \mytermi{(}\ \mysee{term}\ \mytermi{:}\ \mysee{term}\ \mytermi{)}\ \mytermi{=}\ \mytermi{(}\ \mysee{term}\ \mytermi{:}\ \mysee{term}\ \mytermi{)} & \text{Heterogeneous equality.} \\
4271 & | & \mytermi{(}\ \mysee{compound}\ \mytermi{)} & \text{Parenthesised term.} \\
4272 \mysee{compound} & ::= & \mytermi{\textbackslash}\ \mysee{binder}{*}\ \mytermi{=>}\ \mysee{term} & \text{Untyped abstraction.} \\
4273 & | & \mytermi{\textbackslash}\ \mysee{telescope}\ \mytermi{:}\ \mysee{term}\ \mytermi{=>}\ \mysee{term} & \text{Typed abstraction.} \\
4274 & | & \mytermi{forall}\ \mysee{telescope}\ \mysee{term} & \text{Universal quantification.} \\
4275 & | & \mysee{arr} \\
4276 \mysee{arr} & ::= & \mysee{telescope}\ \mytermi{->}\ \mysee{arr} & \text{Dependent function.} \\
4277 & | & \mysee{term}\ \mytermi{->}\ \mysee{arr} & \text{Non-dependent function.} \\
4278 & | & \mysee{term}{+} & \text {Application.}
4281 \multicolumn{3}{@{}l}{\text{Typed names.}} \\
4282 \mysee{typed} & ::= & \mysee{name}\ \mytermi{:}\ \mysee{term} \\
4283 \multicolumn{3}{@{}l}{\text{Declarations.}} \\
4284 \mysee{decl}& ::= & \mysee{value} \mysynsep \mysee{abstract} \mysynsep \mysee{data} \mysynsep \mysee{record} \\
4285 \multicolumn{3}{@{}l}{\text{Defined values. The telescope specifies named arguments.}} \\
4286 \mysee{value} & ::= & \mysee{name}\ \mysee{telescope}\ \mytermi{:}\ \mysee{term}\ \mytermi{=>}\ \mysee{term} \\
4287 \multicolumn{3}{@{}l}{\text{Abstracted variables.}} \\
4288 \mysee{abstract} & ::= & \mytermi{postulate}\ \mysee{typed} \\
4289 \multicolumn{3}{@{}l}{\text{Data types, and their constructors.}} \\
4290 \mysee{data} & ::= & \mytermi{data}\ \mysee{name}\ \mysee{telescope}\ \mytermi{->}\ \mytermi{*}\ \mytermi{=>}\ \mytermi{\{}\ \mysee{constrs}\ \mytermi{\}} \\
4291 \mysee{constrs} & ::= & \mysee{typed} \\
4292 & | & \mysee{typed}\ \mytermi{|}\ \mysee{constrs} \\
4293 \multicolumn{3}{@{}l}{\text{Records, and their projections. The $\mysee{name}$ before the projections is the constructor name.}} \\
4294 \mysee{record} & ::= & \mytermi{record}\ \mysee{name}\ \mysee{telescope}\ \mytermi{->}\ \mytermi{*}\ \mytermi{=>}\ \mysee{name}\ \mytermi{\{}\ \mysee{projs}\ \mytermi{\}} \\
4295 \mysee{projs} & ::= & \mysee{typed} \\
4296 & | & \mysee{typed}\ \mytermi{,}\ \mysee{projs}
4300 \caption{\mykant' syntax. The non-terminals are marked with
4301 $\langle\text{angle brackets}\rangle$ for greater clarity. The
4302 syntax in the implementation is actually more liberal, for example
4303 giving the possibility of using arrow types directly in
4304 constructor/projection declarations.\\
4305 Additionally, we give the user the possibility of using Unicode
4306 characters instead of their ASCII counterparts, e.g. \texttt{→} in
4307 place of \texttt{->}, \texttt{λ} in place of
4308 \texttt{\textbackslash}, etc.}
4312 \subsection{Term representation}
4313 \label{sec:term-repr}
4315 \subsubsection{Naming and substituting}
4317 Perhaps surprisingly, one of the most difficult challenges in
4318 implementing a theory of the kind presented is choosing a good data type
4319 for terms, and specifically handling substitutions in a sane way.
4321 There are two broad schools of thought when it comes to naming
4322 variables, and thus substituting:
4324 \item[Nameful] Bound variables are represented by some enumerable data
4325 type, just as we have described up to now, starting from Section
4326 \ref{sec:untyped}. The problem is that avoiding name capturing is a
4327 nightmare, both in the sense that it is not performant---given that we
4328 need to rename rename substitute each time we `enter' a binder---but
4329 most importantly given the fact that in even slightly more complicated
4330 systems it is very hard to get right, even for experts.
4332 One of the sore spots of explicit names is comparing terms up to
4333 $\alpha$-renaming, which again generates a huge amounts of
4334 substitutions and requires special care.
4336 \item[Nameless] We can capture the relationship between variables and
4337 their binders, by getting rid of names altogether, and representing
4338 bound variables with an index referring to the `binding' structure, a
4339 notion introduced by \cite{de1972lambda}. Usually $0$ represents the
4340 variable bound by the innermost binding structure, $1$ the
4341 second-innermost, and so on. For instance with simple abstractions we
4345 \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} \\
4346 \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
4350 While this technique is obviously terrible in terms of human
4351 usability,\footnote{With some people going as far as defining it akin
4352 to an inverse Turing test.} it is much more convenient as an
4353 internal representation to deal with terms mechanically---at least in
4354 simple cases. $\alpha$-renaming ceases to be an issue, and
4355 term comparison is purely syntactical.
4357 Nonetheless, more complex constructs such as pattern matching put
4358 some strain on the indices and many systems end up using explicit
4363 In the past decade or so advancements in the Haskell's type system and
4364 in general the spread new programming practices have made the nameless
4365 option much more amenable. \mykant\ thus takes the nameless path
4366 through the use of Edward Kmett's excellent \texttt{bound}
4367 library.\footnote{Available at
4368 \url{http://hackage.haskell.org/package/bound}.} We describe the
4369 advantages of \texttt{bound}'s approach, but also its pitfalls in the
4370 previously relatively unknown territory of dependent
4371 types---\texttt{bound} being created mostly to handle more simply typed
4374 \texttt{bound} builds on the work of \cite{Bird1999}, who suggested to
4375 parametrising the term type over the type of the variables, and `nest'
4376 the type each time we enter a scope. If we wanted to define a term
4377 for the untyped $\lambda$-calculus, we might have
4379 -- A type with no members.
4382 data Var v = Bound | Free v
4385 = V v -- Bound variable
4386 | App (Tm v) (Tm v) -- Term application
4387 | Lam (Tm (Var v)) -- Abstraction
4389 Closed terms would be of type \texttt{Tm Empty}, so that there would be
4390 no occurrences of \texttt{V}. However, inside an abstraction, we can
4391 have \texttt{V Bound}, representing the bound variable, and inside a
4392 second abstraction we can have \texttt{V Bound} or \texttt{V (Free
4393 Bound)}. Thus the term
4394 \[\myabs{\myb{x}}{\myabs{\myb{y}}{\myb{x}}}\]
4395 can be represented as
4397 -- The top level term is of type `Tm Empty'.
4398 -- The inner term `Lam (Free Bound)' is of type `Tm (Var Empty)'.
4399 -- The second inner term `V (Free Bound)' is of type `Tm (Var (Var
4401 Lam (Lam (V (Free Bound)))
4403 This allows us to reflect the of a type `nestedness' at the type level,
4404 and since we usually work with functions polymorphic on the parameter
4405 \texttt{v} it's very hard to make mistakes by putting terms of the wrong
4406 nestedness where they don't belong.
4408 Even more interestingly, the substitution operation is perfectly
4409 captured by the \verb|>>=| (bind) operator of the \texttt{Monad}
4414 (>>=) :: m a -> (a -> m b) -> m b
4416 instance Monad Tm where
4417 -- `return'ing turns a variable into a `Tm'
4420 -- `t >>= f' takes a term `t' and a mapping from variables to terms
4421 -- `f' and applies `f' to all the variables in `t', replacing them
4422 -- with the mapped terms.
4424 App m n >>= f = App (m >>= f) (n >>= f)
4426 -- `Lam' is the tricky case: we modify the function to work with bound
4427 -- variables, so that if it encounters `Bound' it leaves it untouched
4428 -- (since the mapping refers to the outer scope); if it encounters a
4429 -- free variable it asks `f' for the term and then updates all the
4430 -- variables to make them refer to the outer scope they were meant to
4432 Lam s >>= f = Lam (s >>= bump)
4433 where bump Bound = return Bound
4434 bump (Free v) = f v >>= V . Free
4436 With this in mind, we can define functions which will not only work on
4437 \verb|Tm|, but on any \verb|Monad|!
4439 -- Replaces free variable `v' with `m' in `n'.
4440 subst :: (Eq v, Monad m) => v -> m v -> m v -> m v
4441 subst v m n = n >>= \v' -> if v == v' then m else return v'
4443 -- Replace the variable bound by `s' with term `t'.
4444 inst :: Monad m => m v -> m (Var v) -> m v
4445 inst t s = s >>= \v -> case v of
4447 Free v' -> return v'
4449 The beauty of this technique is that with a few simple functions we have
4450 defined all the core operations in a general and `obviously correct'
4451 way, with the extra confidence of having the type checker looking our
4452 back. For what concerns term equality, we can just ask the Haskell
4453 compiler to derive the instance for the \verb|Eq| type class and since
4454 we are nameless that will be enough (modulo fancy quotation).
4456 Moreover, if we take the top level term type to be \verb|Tm String|, we
4457 get a representation of terms with top-level definitions; where closed
4458 terms contain only \verb|String| references to said definitions---see
4459 also \cite{McBride2004b}.
4461 What are then the pitfalls of this seemingly invincible technique? The
4462 most obvious impediment is the need for polymorphic recursion.
4463 Functions traversing terms parametrised by the variable type will have
4466 -- Infer the type of a term, or return an error.
4467 infer :: Tm v -> Either Error (Tm v)
4469 When traversing under a \verb|Scope| the parameter changes from \verb|v|
4470 to \verb|Var v|, and thus if we do not specify the type for our function explicitly
4471 inference will fail---type inference for polymorphic recursion being
4472 undecidable \citep{henglein1993type}. This causes some annoyance,
4473 especially in the presence of many local definitions that we would like
4476 But the real issue is the fact that giving a type parametrised over a
4477 variable---say \verb|m v|---a \verb|Monad| instance means being able to
4478 only substitute variables for values of type \verb|m v|. This is a
4479 considerable inconvenience. Consider for instance the case of
4480 telescopes, which are a central tool to deal with contexts and other
4481 constructs. In Haskell we can give them a faithful representation
4482 with a data type along the lines of
4484 data Tele m v = Empty (m v) | Bind (m v) (Tele m (Var v))
4485 type TeleTm = Tele Tm
4487 The problem here is that what we want to substitute for variables in
4488 \verb|Tele m v| is \verb|m v| (probably \verb|Tm v|), not \verb|Tele m v| itself! What we need is
4490 bindTele :: Monad m => Tele m a -> (a -> m b) -> Tele m b
4491 substTele :: (Eq v, Monad m) => v -> m v -> Tele m v -> Tele m v
4492 instTele :: Monad m => m v -> Tele m (Var v) -> Tele m v
4494 Not what \verb|Monad| gives us. Solving this issue in an elegant way
4495 has been a major sink of time and source of headaches for the author,
4496 who analysed some of the alternatives---most notably the work by
4497 \cite{weirich2011binders}---but found it impossible to give up the
4498 simplicity of the model above.
4500 That said, our term type is still reasonably brief, as shown in full in
4501 Appendix \ref{app:termrep}. The fact that propositions cannot be
4502 factored out in another data type is an instance of the problem
4503 described above. However the real pain is during elaboration, where we
4504 are forced to treat everything as a type while we would much rather have
4505 telescopes. Future work would include writing a library that marries
4506 more flexibility with a nice interface similar to the one of
4509 We also make use of a `forgetful' data type (as provided by
4510 \verb|bound|) to store user-provided variables names along with the
4511 `nameless' representation, so that the names will not be considered when
4512 compared terms, but will be available when distilling so that we can
4513 recover variable names that are as close as possible to what the user
4516 \subsubsection{Evaluation}
4518 Another source of contention related to term representation is dealing
4519 with evaluation. Here \mykant\ does not make bold moves, and simply
4520 employs substitution. When type checking we match types by reducing
4521 them to their weak head normal form, as to avoid unnecessary evaluation.
4523 We treat data types eliminators and record projections in an uniform
4524 way, by elaborating declarations in a series of \emph{rewriting rules}:
4528 TmRef v -> -- Term to which the destructor is applied
4529 [TmRef v] -> -- List of other arguments
4530 -- The result of the rewriting, if the eliminator reduces.
4533 A rewriting rule is polymorphic in the variable type, guaranteeing that
4534 it just pattern matches on terms structure and rearranges them in some
4535 way, and making it possible to apply it at any level in the term. When
4536 reducing a series of applications we match the first term and check if
4537 it is a destructor, and if that's the case we apply the reduction rule
4538 and reduce further if it yields a new list of terms.
4540 This has the advantage of simplicity, at the expense of being quite poor
4541 in terms of performance and that we need to do quotation manually. An
4542 alternative that solves both of these is the already mentioned
4543 \emph{normalization by evaluation}, where we would compute by turning
4544 terms into Haskell values, and then reify back to terms to compare
4545 them---a useful tutorial on this technique is given by \cite{Loh2010}.
4547 \subsubsection{Parametrised environment}
4549 Through the life of a REPL cycle we need to execute two broad
4550 `effectful' actions:
4552 \item Retrieve, add, and modify elements to an environment. The
4553 environment will contain not only types, but also the rewriting rules
4554 presented in the previous section, and a counter to generate fresh
4555 references for the type hierarchy.
4557 \item Throw various kinds of errors when something goes wrong: parsing,
4558 type checking, input/output error when reading files, and more.
4560 Haskell taught us the value of monads in programming languages, and in
4561 \mykant\ we keep this lesson in mind. All of the plumbing required to do
4562 the two actions above is provided by a very general \emph{monad
4563 transformer} that we use through the codebase, \texttt{KMonadT}:
4565 newtype KMonad f v m a = KMonad (StateT (f v) (ErrorT KError m) a)
4573 Without delving into the details of what a monad transformer is, this is
4574 what \texttt{KMonadT} provides:
4576 \item The \verb|v| parameter represents the parametrised variable for
4577 the term type that we spoke about at the beginning of this section.
4580 \item The \verb|f| parameter indicates what kind of environment we are
4581 holding. Sometimes we want to traverse terms without carrying the
4582 entire environment, for various reasons---\texttt{KMonatT} lets us do
4583 that. Note that \verb|f| is itself parametrised over \verb|v|. The
4584 inner \verb|StateT| monad transformer lets us retrieve and modify this
4585 environment at any time.
4587 \item The \verb|m| is the `inner' monad that we can `plug in' to be able
4588 to do more effectful actions in \texttt{KMonatT}. For example if we
4589 plug the \texttt{IO} monad in, we will be able to do input/output.
4591 \item The inner \verb|ErrorT| lets us throw errors at any time. The
4592 error type is \verb|KError|, which describes all the possible errors
4593 that a \mykant\ process can throw.
4595 \item Finally, the \verb|a| parameter represents the return type of the
4596 computation we are executing.
4599 The clever trick in \texttt{KMonadT} is to have it to be parametrised
4600 over the same type as the term type. This way, we can easily carry the
4601 environment while traversing under binders. For example, if we only
4602 needed to carry types of bound variables in the environment, we can
4603 quickly set up the following infrastructure:
4607 -- A context is a mapping from variables to types.
4608 newtype Ctx v = Ctx (v -> Tm v)
4610 -- A context monad holds a context.
4611 type CtxMonad v m = KMonadT Ctx v m
4613 -- Enter into a scope binding a type to the variable, execute a
4614 -- computation there, and return exit the scope returning to the `current'
4616 nestM :: Monad m => Tm v -> CtxMonad (Var v) m a -> CtxMonad v m a
4619 Again, the types guard our back guaranteeing that we add a type when we
4620 enter a scope, and we discharge it when we get out. The author
4621 originally started with a more traditional representation and often
4622 forgot to add the right variable at the right moment. Using this
4623 practices it is very difficult to do so---we achieve correctness through
4626 In the actual \mykant\ codebase, we have also abstracted the concept of
4627 `context' further, so that we can easily embed contexts into other
4628 structures and write generic operations on all context-like
4629 structures.\footnote{See the \texttt{Kant.Cursor} module for details.}
4631 \subsection{Turning constraints into graphs}
4632 \label{sec:hier-impl}
4634 In this section we will explain how to implement the typical ambiguity
4635 we have spoken about in \ref{sec:term-hierarchy} efficiently, a subject
4636 which is often dismissed in the literature. As mentioned, we have to
4637 verify a the consistency of a set of constraints each time we add a new
4638 one. The constraints range over some set of variables whose members we
4639 will denote with $x, y, z, \dots$. and are of two kinds:
4646 Predictably, $\le$ expresses a reflexive order, and $<$ expresses an
4647 irreflexive order, both working with the same notion of equality, where
4648 $x < y$ implies $x \le y$---they behave like $\le$ and $<$ do for natural
4649 numbers (or in our case, levels in a type hierarchy). We also need an
4650 equality constraint ($x = y$), which can be reduced to two constraints
4651 $x \le y$ and $y \le x$.
4653 Given this specification, we have implemented a standalone Haskell
4654 module---that we plan to release as a library---to efficiently store and
4655 check the consistency of constraints. The problem predictably reduces
4656 to a graph algorithm, and for this reason we also implement a library
4657 for labelled graphs, since the existing Haskell graph libraries fell
4658 short in different areas.\footnote{We tried the \texttt{Data.Graph}
4659 module in \url{http://hackage.haskell.org/package/containers}, and the
4660 much more featureful \texttt{fgl} library
4661 \url{http://hackage.haskell.org/package/fgl}.} The interfaces for
4662 these modules are shown in Appendix \ref{app:constraint}. The graph
4663 library is implemented as a modification of the code described by
4666 We represent the set by building a graph where vertices are variables,
4667 and edges are constraints between them, labelled with the appropriate
4668 constraint: $x < y$ gives rise to a $<$-labelled edge from $x$ to $y$,
4669 and $x \le y$ to a $\le$-labelled edge from $x$ to $y$. As we add
4670 constraints, $\le$ constraints are replaced by $<$ constraints, so that
4671 if we started with an empty set and added
4673 x < y,\ y \le z,\ z \le k,\ k < j,\ j \le y\
4675 it would generate the graph shown in Figure \ref{fig:graph-one-before},
4676 but adding $z < k$ would strengthen the edge from $z$ to $k$, as shown
4677 in \ref{fig:graph-one-after}.
4681 \begin{subfigure}[b]{0.3\textwidth}
4682 \begin{tikzpicture}[node distance=1.5cm]
4685 \node [right of=x] (y) {$y$};
4686 \node [right of=y] (z) {$z$};
4687 \node [below of=z] (k) {$k$};
4688 \node [left of=k] (j) {$j$};
4691 (x) edge node [above] {$<$} (y)
4692 (y) edge node [above] {$\le$} (z)
4693 (z) edge node [right] {$\le$} (k)
4694 (k) edge node [below] {$\le$} (j)
4695 (j) edge node [left ] {$\le$} (y);
4697 \caption{Before $z < k$.}
4698 \label{fig:graph-one-before}
4701 \begin{subfigure}[b]{0.3\textwidth}
4702 \begin{tikzpicture}[node distance=1.5cm]
4705 \node [right of=x] (y) {$y$};
4706 \node [right of=y] (z) {$z$};
4707 \node [below of=z] (k) {$k$};
4708 \node [left of=k] (j) {$j$};
4711 (x) edge node [above] {$<$} (y)
4712 (y) edge node [above] {$\le$} (z)
4713 (z) edge node [right] {$<$} (k)
4714 (k) edge node [below] {$\le$} (j)
4715 (j) edge node [left ] {$\le$} (y);
4717 \caption{After $z < k$.}
4718 \label{fig:graph-one-after}
4721 \begin{subfigure}[b]{0.3\textwidth}
4722 \begin{tikzpicture}[remember picture, node distance=1.5cm]
4723 \begin{pgfonlayer}{foreground}
4726 \node [right of=x] (y) {$y$};
4727 \node [right of=y] (z) {$z$};
4728 \node [below of=z] (k) {$k$};
4729 \node [left of=k] (j) {$j$};
4732 (x) edge node [above] {$<$} (y)
4733 (y) edge node [above] {$\le$} (z)
4734 (z) edge node [right] {$<$} (k)
4735 (k) edge node [below] {$\le$} (j)
4736 (j) edge node [left ] {$\le$} (y);
4737 \end{pgfonlayer}{foreground}
4739 \begin{tikzpicture}[remember picture, overlay]
4740 \begin{pgfonlayer}{background}
4741 \fill [red, opacity=0.3, rounded corners]
4742 (-2.7,2.6) rectangle (-0.2,0.05)
4743 (-4.1,2.4) rectangle (-3.3,1.6);
4744 \end{pgfonlayer}{background}
4747 \label{fig:graph-one-scc}
4749 \caption{Strong constraints overrule weak constraints.}
4750 \label{fig:graph-one}
4753 Each time we add a new constraint, we check if any strongly connected
4754 component (SCC) arises, a SCC being a subset $V$ of vertices where for
4755 each $(v_1,v_2) \in V \times V$ there is a path from $v_1$ to $v_2$.
4756 The SCCs in the graph for the constraints above is shown in Figure
4757 \ref{fig:graph-one-scc}. If we have a strongly connected component with
4758 a $<$ edge---say $x < y$---in it, we have an inconsistency, since there
4759 must also be a path from $y$ to $x$, and by transitivity it must either
4760 be the case that $y \le x$ or $y < x$, which are both at odds with $x <
4763 Moreover, if we have a SCC with no $<$ edges, it means that all members
4764 of said SCC are equal, since for every $x \le y$ we have a path from $y$
4765 to $x$, which again by transitivity means that $y \le x$. Thus, we can
4766 \emph{condense} the SCC to a single vertex, by choosing a variable among
4767 the SCC as a representative for all the others. This can be done
4768 efficiently with disjoint set data structure, and is crucial to keep the
4769 graph compact, given the very large number of constraints generated when
4772 \subsection{(Web) REPL}
4774 Finally, we take a break from the types by giving a brief account of the
4775 design of our REPL, being a good example of modular design using various
4776 constructs dear to the Haskell programmer.
4778 Across our codebase we make use of a \emph{monad transformers} named
4779 \texttt{KMonadT}. Without delving into the details of \texttt{KMonadT}
4780 or of monad transformers,\footnote{See
4781 \url{https://en.wikibooks.org/wiki/Haskell/Monad_transformers.}}
4782 computation done inside \texttt{KMonadT} can easily retrieve and modify
4783 the environment and throw various kind of errors, be them parse error,
4784 type errors, etc. Moreover, \texttt{KMonadT} being a monad
4785 \emph{transformers}, we can `plug in' other monads to have access to
4786 other facilities, such as input/output.
4788 That said, the REPL is represented as a function in \texttt{KMonadT}
4789 consuming input and hopefully producing output. Then, frontends can
4790 very easily written by marshalling data in and out of the REPL:
4793 = ITyCheck String -- Type check a term
4794 | IEval String -- Evaluate a term
4795 | IDecl String -- Declare something
4799 = OTyCheck TmRefId [HoleCtx] -- Type checked term, with holes
4800 | OPretty TmRefId -- Term to pretty print, after evaluation
4801 | OHoles [HoleCtx] -- Just holes, classically after loading a file
4804 -- KMonadT is parametrised over the type of the variables, which depends
4805 -- on how deep in the term structure we are. For the REPL, we only deal
4806 -- with top-level terms, and thus only `Id' variables---top level names.
4807 type REPL m = KMonadT Id m
4809 repl :: ReadFile m => Input -> REPL m Output
4811 The \texttt{ReadFile} monad embodies the only `extra' action that we
4812 need to have access too when running the REPL: reading files. We could
4813 simply use the \texttt{IO} monad, but this will not serve us well when
4814 implementing front end facing untrusted parties accessing the application
4815 running on our servers. In our case we expose the REPL as a web
4816 application, and we want the user to be able to load only from a
4817 pre-defined directory, not from the entire file system.
4819 For this reason we specify \texttt{ReadFile} to have just one function:
4821 class Monad m => ReadFile m where
4822 readFile' :: FilePath -> m (Either IOError String)
4824 While in the command-line application we will use the \texttt{IO} monad
4825 and have \texttt{readFile'} to work in the `obvious' way---by reading
4826 the file corresponding to the given file path---in the web prompt we
4827 will have it to accept only a file name, not a path, and read it from a
4828 pre-defined directory:
4830 -- The monad that will run the web REPL. The `ReaderT' holds the
4831 -- filepath to the directory where the files loadable by the user live.
4832 -- The underlying `IO' monad will be used to actually read the files.
4833 newtype DirRead a = DirRead (ReaderT FilePath IO a)
4835 instance ReadFile DirRead where
4837 do -- We get the base directory in the `ReaderT' with `ask'
4839 -- Is the filepath provided an unqualified file name?
4840 if snd (splitFileName fp) == fp
4841 -- If yes, go ahead and read the file, by lifting
4842 -- `readFile'' into the IO monad
4843 then DirRead (lift (readFile' (dir </> fp)))
4844 -- If not, return an error
4845 else return (Left (strMsg ("Invalid file name `" ++ fp ++ "'")))
4847 Once this light-weight infrastructure is in place, adding a web
4848 interface was an easy exercise. We use Jasper Van der Jeugt's
4849 \texttt{websockets} library\footnote{Available at
4850 \url{http://hackage.haskell.org/package/websockets}.} to create a proxy
4851 that receives JSON messages with the user input, turns them into
4852 \texttt{Input} messages for the REPL, and then sends back a JSON message
4853 with the response. Moreover, each client is handled in a separate
4854 threads, so crashes of the REPL in single threads will not bring the
4855 whole application down.
4857 On the clients side, we had to write some JavaScript to accept input
4858 from a form, and to make the responses appear on the screen. The web
4859 prompt is publicly available at \url{http://bertus.mazzo.li}, a sample
4860 session is shown Figure \ref{fig:web-prompt-one}.
4863 \includegraphics[width=\textwidth]{web-prompt.png}
4864 \caption{A sample run of the web prompt.}
4865 \label{fig:web-prompt-one}
4870 \section{Evaluation}
4871 \label{sec:evaluation}
4873 Going back to our goals in Section \ref{sec:contributions}, we feel that
4874 this thesis fills a gap in the description of observational type theory.
4875 In the design of \mykant\ we willingly patterned the core features
4876 against the ones present in Agda, with the hope that future implementors
4877 will be able to refer to this document without embarking on the same
4878 adventure themselves. We gave an original account of heterogeneous
4879 equality by showing that in a cumulative hierarchy we can keep
4880 equalities as small as we would be able too with a separate notion of
4881 type equality. As a side effect of developing \mykant, we also gave an
4882 original account of bidirectional type checking for user defined types,
4883 which get rid of many types while keeping the language very simple.
4885 Through the design of the theory of \mykant\ we have followed an
4886 approach where study and implementation were continuously interleaved,
4887 as a `reality check' for the ideas that we wished to implement. Given
4888 the great effort necessary to build a theorem prover capable of
4889 `real-world' proofs we have not attempted to compare \mykant's
4890 capabilities to those of Agda and Coq, the theorem provers that the
4891 author is most familiar with and in general two of the main players in
4892 the field. However we have ported a lot of simpler examples to check
4893 that the key features are working, some of which have been used in the
4894 previous sections and are reproduced in the appendices\footnote{The full
4895 list is available in the repository:
4896 \url{https://github.com/bitonic/kant/tree/master/data/samples/good}.}.
4897 A full example of interaction with \mykant\ is given in Section
4898 \ref{sec:type-holes}.
4900 The main culprits for the delays in the implementation are two issues
4901 that revealed themselves to be far less obvious than what the author
4902 predicted. The first, as we have already remarked in Section
4903 \ref{sec:term-repr}, is to have an adequate term representation that
4904 lets us express the right constructs in a safe way. There is still no
4905 widely accepted solution to this problem, which is approached in many
4906 different ways both in the literature and in the programming
4907 practice. The second aspect is the treatment of user defined data types.
4908 Again, the best techniques to implement them in a dependently typed
4909 setting still have not crystallised and implementors reinvent many
4910 wheels each time a new system is built. The author is still conflicted
4911 on whether having user defined types at all it is the right decision:
4912 while they are essential, in hindsight the idea of a bare but fully
4913 implemented theory seems inviting.
4915 In general, implementing dependently typed languages is still a poorly
4916 understood practice, and almost every stage requires experimentation on
4917 behalf of the author. Another example is the treatment of the implicit
4918 hierarchy, where no resources are present describing the problem from an
4919 implementation perspective (we described our approach in Section
4920 \ref{sec:hier-impl}). Hopefully this state of things will change in the
4921 near future, and recent publications are promising in this direction,
4922 for example an unpublished paper by \cite{Brady2013} describing his
4923 implementation of the Idris programming language. Our ultimate goal is
4924 to be a part of this collective effort.
4926 \subsection{A type holes tutorial}
4927 \label{sec:type-holes}
4929 As a taster and showcase for the capabilities of \mykant, we present an
4930 interactive session with the \mykant\ REPL. While doing so, we present
4931 a feature that we still have not covered: type holes.
4933 Type holes are, in the author's opinion, one of the `killer' features of
4934 interactive theorem provers, and one that is begging to be exported to
4935 mainstream programming---although it is much more effective in a
4936 well-typed, functional setting. The idea is that when we are developing
4937 a proof or a program we can insert a hole to have the software tell us
4938 the type expected at that point. Furthermore, we can ask for the type
4939 of variables in context, to better understand our surroundings.
4941 In \mykant\ we use type holes by putting them where a term should go.
4942 We need to specify a name and then we can put as many terms as we like
4943 in the hole. \mykant\ will tell us which type it is expecting for the
4944 term where the hole is, and the type of the terms that we have included.
4945 For example if we had:
4947 plus [m n : Nat] : Nat ⇒ (
4951 And we loaded the file in \mykant, we would get:
4952 \begin{Verbatim}[frame=leftline]
4960 Suppose we wanted to define the `less or equal' ordering on natural
4961 numbers as described in Section \ref{sec:user-type}. We will
4962 incrementally build our functions in a file called \texttt{le.ka}.
4963 First we define the necessary types, all of which we know well by now:
4965 data Nat : ⋆ ⇒ { zero : Nat | suc : Nat → Nat }
4967 data Empty : ⋆ ⇒ { }
4968 absurd [A : ⋆] [p : Empty] : A ⇒ (
4969 Empty-Elim p (λ _ ⇒ A)
4972 record Unit : ⋆ ⇒ tt { }
4974 Then fire up \mykant, and load the file:
4975 \begin{Verbatim}[frame=leftline]
4978 Version 0.0, made in London, year 2013.
4982 So far so good. Our definition will be defined by recursion on a
4983 natural number \texttt{n}, which will return a function that given
4984 another number \texttt{m} will return the trivial type \texttt{Unit} if
4985 $\texttt{n} \le \texttt{m}$, and the \texttt{Empty} type otherwise.
4986 However we are still not sure on how to define it, so we invoke
4987 $\texttt{Nat-Elim}$, the eliminator for natural numbers, and place holes
4988 instead of arguments. In the file we will write:
4990 le [n : Nat] : Nat → ⋆ ⇒ (
4991 Nat-Elim n (λ _ ⇒ Nat → ⋆)
4996 And then we reload in \mykant:
4997 \begin{Verbatim}[frame=leftline]
5001 h2 : Nat → (Nat → ⋆) → Nat → ⋆
5003 Which tells us what types we need to satisfy in each hole. However, it
5004 is not that clear what does what in each hole, and thus it is useful to
5005 have a definition vacuous in its arguments just to clear things up. We
5006 will use \texttt{Le} aid in reading the goal, with \texttt{Le m n} as a
5007 reminder that we to return the type corresponding to $\texttt{m} ≤
5010 Le [m n : Nat] : ⋆ ⇒ ⋆
5012 le [n : Nat] : [m : Nat] → Le n m ⇒ (
5013 Nat-Elim n (λ n ⇒ [m : Nat] → Le n m)
5018 \begin{Verbatim}[frame=leftline]
5021 h1 : [m : Nat] → Le zero m
5022 h2 : [x : Nat] → ([m : Nat] → Le x m) → [m : Nat] → Le (suc x) m
5024 This is much better! \mykant, when printing terms, does not substitute
5025 top-level names for their bodies, since usually the resulting term is
5026 much clearer. As a nice side-effect, we can use tricks like this to
5029 In this case in the first case we need to return, given any number
5030 \texttt{m}, $0 \le \texttt{m}$. The trivial type will do, since every
5031 number is less or equal than zero:
5033 le [n : Nat] : [m : Nat] → Le n m ⇒ (
5034 Nat-Elim n (λ n ⇒ [m : Nat] → Le n m)
5039 \begin{Verbatim}[frame=leftline]
5042 h2 : [x : Nat] → ([m : Nat] → Le x m) → [m : Nat] → Le (suc x) m
5044 Now for the important case. We are given our comparison function for a
5045 number, and we need to produce the function for the successor. Thus, we
5046 need to re-apply the induction principle on the other number, \texttt{m}:
5048 le [n : Nat] : [m : Nat] → Le n m ⇒ (
5049 Nat-Elim n (λ n ⇒ [m : Nat] → Le n m)
5051 (λ n' f m ⇒ Nat-Elim m (λ m' ⇒ Le (suc n') m') {|h2|} {|h3|})
5054 \begin{Verbatim}[frame=leftline]
5058 h3 : [x : Nat] → Le (suc n') x → Le (suc n') (suc x)
5060 In the first hole we know that the second number is zero, and thus we
5061 can return empty. In the second case, we can use the recursive argument
5062 \texttt{f} on the two numbers:
5064 le [n : Nat] : [m : Nat] → Le n m ⇒ (
5065 Nat-Elim n (λ n ⇒ [m : Nat] → Le n m)
5068 Nat-Elim m (λ m' ⇒ Le (suc n') m') Empty (λ f _ ⇒ f m'))
5071 We can verify that our function works as expected:
5072 \begin{Verbatim}[frame=leftline]
5075 >>> :e le zero (suc zero)
5077 >>> :e le (suc (suc zero)) (suc zero)
5080 Another functionality of type holes is examining types of things in
5081 context. Going back to the examples in Section \ref{sec:term-types}, we can
5082 implement the safe \texttt{head} function with our newly defined
5085 data List : [A : ⋆] → ⋆ ⇒
5086 { nil : List A | cons : A → List A → List A }
5088 length [A : ⋆] [l : List A] : Nat ⇒ (
5089 List-Elim l (λ _ ⇒ Nat) zero (λ _ _ n ⇒ suc n)
5092 gt [n m : Nat] : ⋆ ⇒ (le (suc m) n)
5094 head [A : ⋆] [l : List A] : gt (length A l) zero → A ⇒ (
5095 List-Elim l (λ l ⇒ gt (length A l) zero → A)
5100 We define \texttt{List}s, a polymorphic \texttt{length} function, and
5101 express $<$ (\texttt{gt}) in terms of $\le$. Then, we set up the type
5102 for our \texttt{head} function. Given a list and a proof that its
5103 length is greater than zero, we return the first element. If we load
5104 this in \mykant, we get:
5105 \begin{Verbatim}[frame=leftline]
5110 h2 : [x : A] [x1 : List A] →
5111 (gt (length A x1) zero → A) →
5112 gt (length A (cons x x1)) zero → A
5114 In the first case (the one for \texttt{nil}), we have a proof of
5115 \texttt{Empty}---surely we can use \texttt{absurd} to get rid of that
5116 case. In the second case we simply return the element in the
5119 head [A : ⋆] [l : List A] : gt (length A l) zero → A ⇒ (
5120 List-Elim l (λ l ⇒ gt (length A l) zero → A)
5125 Now, if we tried to get the head of an empty list, we face a problem:
5126 \begin{Verbatim}[frame=leftline]
5130 We would have to provide something of type \texttt{Empty}, which
5131 hopefully should be impossible. For non-empty lists, on the other hand,
5132 things run smoothly:
5133 \begin{Verbatim}[frame=leftline]
5134 >>> :t head Nat (cons zero nil)
5136 >>> :e head Nat (cons zero nil) tt
5139 This should give a vague idea of why type holes are so useful and in
5140 more in general about the development process in \mykant. Most
5141 interactive theorem provers offer some kind of facility
5142 to... interactively develop proofs, usually much more powerful than the
5143 fairly bare tools present in \mykant. Agda in particular offers a
5144 celebrated mode for the \texttt{Emacs} text editor.
5146 \section{Future work}
5147 \label{sec:future-work}
5149 The first move that the author plans to make is to work towards a simple
5150 but powerful term representation. A good plan seems to be to associate
5151 each type (terms, telescopes, etc.) with what we can substitute
5152 variables with, so that the term type will be associated with itself,
5153 while telescopes and propositions will be associated to terms. This can
5154 probably be accomplished elegantly with Haskell's \emph{type families}
5155 \citep{chakravarty2005associated}. After achieving a more solid
5156 machinery for terms, implementing observational equality fully should
5157 prove relatively easy.
5159 Beyond this steps, we can go in many directions to improve the
5160 system that we described---here we review the main ones.
5163 \item[Pattern matching and recursion] Eliminators are very clumsy,
5164 and using them can be especially frustrating if we are used to writing
5165 functions via explicit recursion. \cite{Gimenez1995} showed how to
5166 reduce well-founded recursive definitions to primitive recursors.
5167 Intuitively, defining a function through an eliminators corresponds to
5168 pattern matching and recursively calling the function on the recursive
5169 occurrences of the type we matched against.
5171 Nested pattern matching can be justified by identifying a notion of
5172 `structurally smaller', and allowing recursive calls on all smaller
5173 arguments. Epigram goes all the way and actually implements recursion
5174 exclusively by providing a convenient interface to the two constructs
5175 above \citep{EpigramTut, McBride2004}.
5177 However as we extend the flexibility in our recursion elaborating
5178 definitions to eliminators becomes more and more laborious. For
5179 example we might want mutually definitions and definitions that
5180 terminate relying on the structure of two arguments instead of just
5181 one. For this reason both Agda and Coq (Agda putting more effort) let
5182 the user write recursive definitions freely, and then employ an
5183 external syntactic check to ensure termination.
5185 Moreover, if we want to use dependently typed languages for
5186 programming purposes, we will probably want to sidestep the
5187 termination checker and write a possibly non-terminating function;
5188 maybe because proving termination is particularly difficult. With
5189 explicit recursion this amounts to turning off a check, if we have
5190 only eliminators it is impossible.
5192 \item[More powerful data types] A popular improvement on basic data
5193 types are inductive families \citep{Dybjer1991}, where the parameters
5194 for the type constructors can change based on the data constructors,
5195 which lets us express naturally types such as $\mytyc{Vec} : \mynat
5196 \myarr \mytyp$, which given a number returns the type of lists of that
5197 length, or $\mytyc{Fin} : \mynat \myarr \mytyp$, which given a number
5198 $n$ gives the type of numbers less than $n$. This apparent omission
5199 was motivated by the fact that inductive families can be represented
5200 by adding equalities concerning the parameters of the type
5201 constructors as arguments to the data constructor, in much the same
5202 way that Generalised Abstract Data Types \citep{GHC} are handled in
5203 Haskell. Interestingly the modified version of System F that lies at
5204 the core of recent versions of GHC features coercions reminiscent of
5205 those found in OTT, motivated by the need to implement GADTs in an
5206 elegant way \citep{Sulzmann2007}.
5208 Another concept introduced by \cite{dybjer2000general} is
5209 induction-recursion, where we define a data type in tandem with a
5210 function on that type. This technique has proven extremely useful to
5211 define embeddings of other calculi in an host language, by defining
5212 the representation of the embedded language as a data type and at the
5213 same time a function decoding from the representation to a type in the
5214 host language. The decoding function is then used to define the data
5215 type for the embedding itself, for example by reusing the host's
5216 language functions to describe functions in the embedded language,
5217 with decoded types as arguments.
5219 It is also worth mentioning that in recent times there has been work
5220 \citep{dagand2012elaborating, chapman2010gentle} to show how to define
5221 a set of primitives that data types can be elaborated into. The big
5222 advantage of the approach proposed is enabling a very powerful notion
5223 of generic programming, by writing functions working on the
5224 `primitive' types as to be workable by all the other `compatible'
5225 elaborated user defined types. This has been a considerable problem
5226 in the dependently type world, where we often define types which are
5227 more `strongly typed' version of similar structures,\footnote{For
5228 example the $\mytyc{OList}$ presented in Section \ref{sec:user-type}
5229 being a `more typed' version of an ordinary list.} and then find
5230 ourselves forced to redefine identical operations on both types.
5232 \item[Pattern matching and inductive families] The notion of inductive
5233 family also yields a more interesting notion of pattern matching,
5234 since matching on an argument influences the value of the parameters
5235 of the type of said argument. This means that pattern matching
5236 influences the context, which can be exploited to constraint the
5237 possible data constructors for \emph{other} arguments
5238 \citep{McBride2004}.
5240 \item[Type inference] While bidirectional type checking helps at a very
5241 low cost of implementation and complexity, a much more powerful weapon
5242 is found in \emph{pattern unification}, which allows Hindley-Milner
5243 style inference for dependently typed languages. Unification for
5244 higher order terms is undecidable and unification problems do not
5245 always have a most general unifier \cite{huet1973undecidability}.
5246 However \cite{miller1992unification} identified a decidable fragment
5247 of higher order unification commonly known as pattern unification,
5248 which is employed in most theorem provers to drastically reduce the
5249 number of type annotations. \cite{gundrytutorial} provide a tutorial
5252 \item[Coinductive data types] When we specify inductive data types, we
5253 do it by specifying its \emph{constructors}---functions with the type
5254 we are defining as codomain. Then, we are offered way of compute by
5255 recursively \emph{destructing} or \emph{eliminating} a member of the
5258 Coinductive data types are the dual of this approach. We specify ways
5259 to destruct data, and we are given a way to generate the defined type
5260 by repeatedly `unfolding' starting from some seed data. For example,
5261 we could defined infinite streams by specifying a $\myfun{head}$ and
5262 $\myfun{tail}$ destructors---here using a syntax reminiscent of
5266 \mysyn{codata}\ \mytyc{Stream}\myappsp (\myb{A} {:} \mytyp)\ \mysyn{where} \\
5267 \myind{2} \{ \myfun{head} : \myb{A}, \myfun{tail} : \mytyc{Stream} \myappsp \myb{A}\}
5270 which will hopefully give us something like
5273 \myfun{head} : (\myb{A}{:}\mytyp) \myarr \mytyc{Stream} \myappsp \myb{A} \myarr \myb{A} \\
5274 \myfun{tail} : (\myb{A}{:}\mytyp) \myarr \mytyc{Stream} \myappsp \myb{A} \myarr \mytyc{Stream} \myappsp \myb{A} \\
5275 \mytyc{Stream}.\mydc{unfold} : (\myb{A}\, \myb{B} {:} \mytyp) \myarr (\myb{A} \myarr \myb{B} \myprod \myb{A}) \myarr \myb{A} \myarr \mytyc{Stream} \myappsp \myb{B}
5278 Where, in $\mydc{unfold}$, $\myb{B} \myprod \myb{A}$ represents the
5279 fields of $\mytyc{Stream}$ but with the recursive occurrence replaced
5280 by the `seed' type $\myb{A}$.
5282 Beyond simple infinite types like $\mytyc{Stream}$, coinduction is
5283 particularly useful to write non-terminating programs like servers or
5284 software interacting with a user, while guaranteeing their liveliness.
5285 Moreover it lets us model possibly non-terminating computations in an
5286 elegant way \citep{Capretta2005}, enabling for example the study of
5287 operational semantics for non-terminating languages
5288 \citep{Danielsson2012}.
5290 \cite{cockett1992charity} pioneered this approach in their programming
5291 language Charity, and coinduction has since been adopted in systems
5292 such as Coq \citep{Gimenez1996} and Agda. However these
5293 implementations are unsatisfactory, since Coq's break subject
5294 reduction, and Agda does not allow types to depend on the unfolding of
5295 codata to avoid this problem. \cite{mcbride2009let} has shown how
5296 observational equality can help to resolve these issues, since we can
5297 reason about the unfoldings in a better way, like we reason about
5298 functions' extensional behaviour.
5301 The author looks forward to the study and possibly the implementation of
5302 these ideas in the years to come.
5308 \section{Notation and syntax}
5309 \label{app:notation}
5311 Syntax, derivation rules, and reduction rules, are enclosed in frames describing
5312 the type of relation being established and the syntactic elements appearing,
5315 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
5316 Typing derivations here.
5319 In the languages presented and Agda code samples I also highlight the syntax,
5320 following a uniform colour and font convention:
5323 \begin{tabular}{c | l}
5324 $\mytyc{Sans}$ & Type constructors. \\
5325 $\mydc{sans}$ & Data constructors. \\
5326 % $\myfld{sans}$ & Field accessors (e.g. \myfld{fst} and \myfld{snd} for products). \\
5327 $\mysyn{roman}$ & Keywords of the language. \\
5328 $\myfun{roman}$ & Defined values and destructors. \\
5329 $\myb{math}$ & Bound variables.
5333 When presenting grammars, I will use a word in $\mysynel{math}$ font
5334 (e.g. $\mytmsyn$ or $\mytysyn$) to indicate indicate
5335 nonterminals. Additionally, I will use quite flexibly a $\mysynel{math}$
5336 font to indicate a syntactic element in derivations or meta-operations.
5337 More specifically, terms are usually indicated by lowercase letters
5338 (often $\mytmt$, $\mytmm$, or $\mytmn$); and types by an uppercase
5339 letter (often $\mytya$, $\mytyb$, or $\mytycc$).
5341 When presenting type derivations, I will often abbreviate and present multiple
5342 conclusions, each on a separate line:
5344 \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
5345 \UnaryInfC{$\myjud{\myapp{\myfst}{\mytmt}}{\mytya}$}
5347 \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mytyb}$}
5349 I will often present `definitions' in the described calculi and in
5350 $\mykant$\ itself, like so:
5353 \myfun{name} : \mytysyn \\
5354 \myfun{name} \myappsp \myb{arg_1} \myappsp \myb{arg_2} \myappsp \cdots \mapsto \mytmsyn
5357 To define operators, I use a mixfix notation similar
5358 to Agda, where $\myarg$s denote arguments:
5361 \myarg \mathrel{\myfun{$\wedge$}} \myarg : \mybool \myarr \mybool \myarr \mybool \\
5362 \myb{b_1} \mathrel{\myfun{$\wedge$}} \myb{b_2} \mapsto \cdots
5365 In explicitly typed systems, I will also omit type annotations when they
5366 are obvious, e.g. by not annotating the type of parameters of
5367 abstractions or of dependent pairs.\\
5368 I will introduce multiple arguments in one go in arrow types:
5370 (\myb{x}\, \myb{y} {:} \mytya) \myarr \cdots = (\myb{x} {:} \mytya) \myarr (\myb{y} {:} \mytya) \myarr \cdots
5372 and in abstractions:
5374 \myabs{\myb{x}\myappsp\myb{y}}{\cdots} = \myabs{\myb{x}}{\myabs{\myb{y}}{\cdots}}
5376 I will also omit arrows to abbreviate types:
5378 (\myb{x} {:} \mytya)(\myb{y} {:} \mytyb) \myarr \cdots =
5379 (\myb{x} {:} \mytya) \myarr (\myb{y} {:} \mytyb) \myarr \cdots
5382 Meta operations names will be displayed in $\mymeta{smallcaps}$ and
5383 written in a pattern matching style, also making use of boolean guards.
5384 For example, a meta operation operating on a context and terms might
5388 \mymeta{quux}(\myctx, \myb{x}) \mymetaguard \myb{x} \in \myctx \mymetagoes \myctx(\myb{x}) \\
5389 \mymeta{quux}(\myctx, \myb{x}) \mymetagoes \mymeta{outofbounds} \\
5394 I will from time to time give examples in the Haskell programming
5395 language as defined in \citep{Haskell2010}, which I will typeset in
5396 \texttt{teletype} font. I assume that the reader is already familiar
5397 with Haskell, plenty of good introductions are available
5398 \citep{LYAH,ProgInHask}.
5400 Examples of \mykant\ code will be typeset nicely with \LaTeX in Section
5401 \ref{sec:kant-theory}, to adjust with the rest of the presentation; and
5402 in \texttt{teletype} font in the rest of the document, including Section
5403 \ref{sec:kant-practice} and in the appendices. Snippets of sessions in
5404 the \mykant\ prompt will be displayed with a left border, to distinguish
5405 them from snippets of code:
5406 \begin{Verbatim}[frame=leftline]
5413 \subsection{ITT renditions}
5414 \label{app:itt-code}
5416 \subsubsection{Agda}
5417 \label{app:agda-itt}
5419 Note that in what follows rules for `base' types are
5420 universe-polymorphic, to reflect the exposition. Derived definitions,
5421 on the other hand, mostly work with \mytyc{Set}, reflecting the fact
5422 that in the theory presented we don't have universe polymorphism.
5428 data Empty : Set where
5430 absurd : ∀ {a} {A : Set a} → Empty → A
5433 ¬_ : ∀ {a} → (A : Set a) → Set a
5436 record Unit : Set where
5439 record _×_ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
5446 data Bool : Set where
5449 if_/_then_else_ : ∀ {a} (x : Bool) (P : Bool → Set a) → P true → P false → P x
5450 if true / _ then x else _ = x
5451 if false / _ then _ else x = x
5453 if_then_else_ : ∀ {a} (x : Bool) {P : Bool → Set a} → P true → P false → P x
5454 if_then_else_ x {P} = if_/_then_else_ x P
5456 data W {s p} (S : Set s) (P : S → Set p) : Set (s ⊔ p) where
5457 _◁_ : (s : S) → (P s → W S P) → W S P
5459 rec : ∀ {a b} {S : Set a} {P : S → Set b}
5460 (C : W S P → Set) → -- some conclusion we hope holds
5461 ((s : S) → -- given a shape...
5462 (f : P s → W S P) → -- ...and a bunch of kids...
5463 ((p : P s) → C (f p)) → -- ...and C for each kid in the bunch...
5464 C (s ◁ f)) → -- ...does C hold for the node?
5465 (x : W S P) → -- If so, ...
5466 C x -- ...C always holds.
5467 rec C c (s ◁ f) = c s f (λ p → rec C c (f p))
5469 module Examples-→ where
5476 -- These pragmas are needed so we can use number literals.
5477 {-# BUILTIN NATURAL ℕ #-}
5478 {-# BUILTIN ZERO zero #-}
5479 {-# BUILTIN SUC suc #-}
5481 data List (A : Set) : Set where
5483 _∷_ : A → List A → List A
5485 length : ∀ {A} → List A → ℕ
5487 length (_ ∷ l) = suc (length l)
5492 suc x > suc y = x > y
5494 head : ∀ {A} → (l : List A) → length l > 0 → A
5495 head [] p = absurd p
5498 module Examples-× where
5504 even (suc zero) = Empty
5505 even (suc (suc n)) = even n
5510 5-not-even : ¬ (even 5)
5513 there-is-an-even-number : ℕ × even
5514 there-is-an-even-number = 6 , 6-even
5516 _∨_ : (A B : Set) → Set
5517 A ∨ B = Bool × (λ b → if b then A else B)
5519 left : ∀ {A B} → A → A ∨ B
5522 right : ∀ {A B} → B → A ∨ B
5525 [_,_] : {A B C : Set} → (A → C) → (B → C) → A ∨ B → C
5527 (if (fst x) / (λ b → if b then _ else _ → _) then f else g) (snd x)
5529 module Examples-W where
5534 Tr b = if b then Unit else Empty
5540 zero = false ◁ absurd
5543 suc n = true ◁ (λ _ → n)
5549 if b / (λ b → (Tr b → ℕ) → (Tr b → ℕ) → ℕ)
5550 then (λ _ f → (suc (f tt))) else (λ _ _ → y))
5553 module Equality where
5556 data _≡_ {a} {A : Set a} : A → A → Set a where
5559 ≡-elim : ∀ {a b} {A : Set a}
5560 (P : (x y : A) → x ≡ y → Set b) →
5561 ∀ {x y} → P x x (refl x) → (x≡y : x ≡ y) → P x y x≡y
5562 ≡-elim P p (refl x) = p
5564 subst : ∀ {A : Set} (P : A → Set) → ∀ {x y} → (x≡y : x ≡ y) → P x → P y
5565 subst P x≡y p = ≡-elim (λ _ y _ → P y) p x≡y
5567 sym : ∀ {A : Set} (x y : A) → x ≡ y → y ≡ x
5568 sym x y p = subst (λ y′ → y′ ≡ x) p (refl x)
5570 trans : ∀ {A : Set} (x y z : A) → x ≡ y → y ≡ z → x ≡ z
5571 trans x y z p q = subst (λ z′ → x ≡ z′) q p
5573 cong : ∀ {A B : Set} (x y : A) → x ≡ y → (f : A → B) → f x ≡ f y
5574 cong x y p f = subst (λ z → f x ≡ f z) p (refl (f x))
5577 \subsubsection{\mykant}
5578 \label{app:kant-itt}
5580 The following things are missing: $\mytyc{W}$-types, since our
5581 positivity check is overly strict, and equality, since we haven't
5582 implemented that yet.
5585 \verbatiminput{itt.ka}
5588 \subsection{\mykant\ examples}
5589 \label{app:kant-examples}
5592 \verbatiminput{examples.ka}
5595 \subsection{\mykant' hierachy}
5598 This rendition of the Hurken's paradox does not type check with the
5599 hierachy enabled, type checks and loops without it. Adapted from an
5600 Agda version, available at
5601 \url{http://code.haskell.org/Agda/test/succeed/Hurkens.agda}.
5604 \verbatiminput{hurkens.ka}
5607 \subsection{Term representation}
5610 Data type for terms in \mykant.
5612 {\small\begin{verbatim}-- A top-level name.
5614 -- A data/type constructor name.
5617 -- A term, parametrised over the variable (`v') and over the reference
5618 -- type used in the type hierarchy (`r').
5621 | Ty r -- Type, with a hierarchy reference.
5622 | Lam (TmScope r v) -- Abstraction.
5623 | Arr (Tm r v) (TmScope r v) -- Dependent function.
5624 | App (Tm r v) (Tm r v) -- Application.
5625 | Ann (Tm r v) (Tm r v) -- Annotated term.
5626 -- Data constructor, the first ConId is the type constructor and
5627 -- the second is the data constructor.
5628 | Con ADTRec ConId ConId [Tm r v]
5629 -- Data destrutor, again first ConId being the type constructor
5630 -- and the second the name of the eliminator.
5631 | Destr ADTRec ConId Id (Tm r v)
5633 | Hole HoleId [Tm r v]
5634 -- Decoding of propositions.
5638 | Prop r -- The type of proofs, with hierarchy reference.
5641 | And (Tm r v) (Tm r v)
5642 | Forall (Tm r v) (TmScope r v)
5643 -- Heterogeneous equality.
5644 | Eq (Tm r v) (Tm r v) (Tm r v) (Tm r v)
5646 -- Either a data type, or a record.
5647 data ADTRec = ADT | Rec
5649 -- Either a coercion, or coherence.
5650 data Coeh = Coe | Coh\end{verbatim}
5653 \subsection{Graph and constraints modules}
5654 \label{app:constraint}
5656 The modules are respectively named \texttt{Data.LGraph} (short for
5657 `labelled graph'), and \texttt{Data.Constraint}. The type class
5658 constraints on the type parameters are not shown for clarity, unless
5659 they are meaningful to the function. In practice we use the
5660 \texttt{Hashable} type class on the vertex to implement the graph
5661 efficiently with hash maps.
5663 \subsubsection{\texttt{Data.LGraph}}
5666 \verbatiminput{graph.hs}
5669 \subsubsection{\texttt{Data.Constraint}}
5672 \verbatiminput{constraint.hs}
5677 \bibliographystyle{authordate1}
5678 \bibliography{thesis}