2 %% THIS LATEX HURTS YOUR EYES. DO NOT READ.
5 \documentclass[11pt, fleqn, twoside, a4paper]{article}
8 \usepackage[usenames,dvipsnames]{xcolor}
10 \usepackage[sc,slantedGreek]{mathpazo}
14 % \oddsidemargin .50in
15 % \evensidemargin -.25in
16 % % \oddsidemargin 0in
17 % % \evensidemargin 0in
26 \usepackage[hmargin=2cm,vmargin=2.5cm,a4paper]{geometry}
27 \geometry{textwidth=390pt}
28 \geometry{bindingoffset=1.5cm}
38 \usepackage[pdftex, pdfborderstyle={/S/U/W 0}]{hyperref}
44 \usepackage[fleqn]{amsmath}
45 \usepackage{stmaryrd} %llbracket
48 \usepackage{bussproofs}
60 \usepackage{subcaption}
65 \usepackage[nottoc]{tocbibind}
67 \RecustomVerbatimEnvironment
73 \usetikzlibrary{shapes,arrows,positioning}
74 \usetikzlibrary{intersections}
75 % \usepackage{tikz-cd}
76 % \usepackage{pgfplots}
81 \titleformat{\section}
82 {\normalfont\huge\scshape}
83 {\thesection\hskip 9pt\textpipe\hskip 9pt}
87 \newcommand{\sectionbreak}{\clearpage}
91 %% -----------------------------------------------------------------------------
93 \usepackage[english]{babel}
94 \usepackage[conor]{agda}
95 \renewcommand{\AgdaKeywordFontStyle}[1]{\ensuremath{\mathrm{\underline{#1}}}}
96 \renewcommand{\AgdaFunction}[1]{\textbf{\textcolor{AgdaFunction}{#1}}}
97 \renewcommand{\AgdaField}{\AgdaFunction}
98 % \definecolor{AgdaBound} {HTML}{000000}
99 \definecolor{AgdaHole} {HTML} {FFFF33}
101 \DeclareUnicodeCharacter{9665}{\ensuremath{\lhd}}
102 \DeclareUnicodeCharacter{964}{\ensuremath{\tau}}
103 \DeclareUnicodeCharacter{963}{\ensuremath{\sigma}}
104 \DeclareUnicodeCharacter{915}{\ensuremath{\Gamma}}
105 \DeclareUnicodeCharacter{8799}{\ensuremath{\stackrel{?}{=}}}
106 \DeclareUnicodeCharacter{9655}{\ensuremath{\rhd}}
108 \renewenvironment{code}%
109 {\noindent\ignorespaces\advance\leftskip\mathindent\AgdaCodeStyle\pboxed\small}%
110 {\endpboxed\par\noindent%
111 \ignorespacesafterend\small}
114 %% -----------------------------------------------------------------------------
117 \newcommand{\mysmall}{}
118 \newcommand{\mysyn}{\AgdaKeyword}
119 \newcommand{\mytyc}[1]{\textup{\AgdaDatatype{#1}}}
120 \newcommand{\mydc}[1]{\textup{\AgdaInductiveConstructor{#1}}}
121 \newcommand{\myfld}[1]{\textup{\AgdaField{#1}}}
122 \newcommand{\myfun}[1]{\textup{\AgdaFunction{#1}}}
123 \newcommand{\myb}[1]{\AgdaBound{$#1$}}
124 \newcommand{\myfield}{\AgdaField}
125 \newcommand{\myind}{\AgdaIndent}
126 \newcommand{\mykant}{\textmd{\textsc{Bertus}}}
127 \newcommand{\mysynel}[1]{#1}
128 \newcommand{\myse}{\mysynel}
129 \newcommand{\mytmsyn}{\mysynel{term}}
130 \newcommand{\mysp}{\ }
131 \newcommand{\myabs}[2]{\mydc{$\lambda$} #1 \mathrel{\mydc{$\mapsto$}} #2}
132 \newcommand{\myappsp}{\hspace{0.07cm}}
133 \newcommand{\myapp}[2]{#1 \myappsp #2}
134 \newcommand{\mysynsep}{\ \ |\ \ }
135 \newcommand{\myITE}[3]{\myfun{If}\, #1\, \myfun{Then}\, #2\, \myfun{Else}\, #3}
136 \newcommand{\mycumul}{\preceq}
138 \newcommand{\mydesc}[3]{
144 \hfill \textup{\phantom{ygp}\textbf{#1}} $#2$
145 \framebox[\textwidth]{
160 \newcommand{\mytmt}{\mysynel{t}}
161 \newcommand{\mytmm}{\mysynel{m}}
162 \newcommand{\mytmn}{\mysynel{n}}
163 \newcommand{\myred}{\leadsto}
164 \newcommand{\mysub}[3]{#1[#3 / #2]}
165 \newcommand{\mytysyn}{\mysynel{type}}
166 \newcommand{\mybasetys}{K}
167 \newcommand{\mybasety}[1]{B_{#1}}
168 \newcommand{\mytya}{\myse{A}}
169 \newcommand{\mytyb}{\myse{B}}
170 \newcommand{\mytycc}{\myse{C}}
171 \newcommand{\myarr}{\mathrel{\textcolor{AgdaDatatype}{\to}}}
172 \newcommand{\myprod}{\mathrel{\textcolor{AgdaDatatype}{\times}}}
173 \newcommand{\myctx}{\Gamma}
174 \newcommand{\myvalid}[1]{#1 \vdash \underline{\mathrm{valid}}}
175 \newcommand{\myjudd}[3]{#1 \vdash #2 : #3}
176 \newcommand{\myjud}[2]{\myjudd{\myctx}{#1}{#2}}
177 \newcommand{\myabss}[3]{\mydc{$\lambda$} #1 {:} #2 \mathrel{\mydc{$\mapsto$}} #3}
178 \newcommand{\mytt}{\mydc{$\langle\rangle$}}
179 \newcommand{\myunit}{\mytyc{Unit}}
180 \newcommand{\mypair}[2]{\mathopen{\mydc{$\langle$}}#1\mathpunct{\mydc{,}} #2\mathclose{\mydc{$\rangle$}}}
181 \newcommand{\myfst}{\myfld{fst}}
182 \newcommand{\mysnd}{\myfld{snd}}
183 \newcommand{\myconst}{\myse{c}}
184 \newcommand{\myemptyctx}{\varepsilon}
185 \newcommand{\myhole}{\AgdaHole}
186 \newcommand{\myfix}[3]{\mysyn{fix} \myappsp #1 {:} #2 \mapsto #3}
187 \newcommand{\mysum}{\mathbin{\textcolor{AgdaDatatype}{+}}}
188 \newcommand{\myleft}[1]{\mydc{left}_{#1}}
189 \newcommand{\myright}[1]{\mydc{right}_{#1}}
190 \newcommand{\myempty}{\mytyc{Empty}}
191 \newcommand{\mycase}[2]{\mathopen{\myfun{[}}#1\mathpunct{\myfun{,}} #2 \mathclose{\myfun{]}}}
192 \newcommand{\myabsurd}[1]{\myfun{absurd}_{#1}}
193 \newcommand{\myarg}{\_}
194 \newcommand{\myderivsp}{}
195 \newcommand{\myderivspp}{\vspace{0.3cm}}
196 \newcommand{\mytyp}{\mytyc{Type}}
197 \newcommand{\myneg}{\myfun{$\neg$}}
198 \newcommand{\myar}{\,}
199 \newcommand{\mybool}{\mytyc{Bool}}
200 \newcommand{\mytrue}{\mydc{true}}
201 \newcommand{\myfalse}{\mydc{false}}
202 \newcommand{\myitee}[5]{\myfun{if}\,#1 / {#2.#3}\,\myfun{then}\,#4\,\myfun{else}\,#5}
203 \newcommand{\mynat}{\mytyc{$\mathbb{N}$}}
204 \newcommand{\myrat}{\mytyc{$\mathbb{R}$}}
205 \newcommand{\myite}[3]{\myfun{if}\,#1\,\myfun{then}\,#2\,\myfun{else}\,#3}
206 \newcommand{\myfora}[3]{(#1 {:} #2) \myarr #3}
207 \newcommand{\myexi}[3]{(#1 {:} #2) \myprod #3}
208 \newcommand{\mypairr}[4]{\mathopen{\mydc{$\langle$}}#1\mathpunct{\mydc{,}} #4\mathclose{\mydc{$\rangle$}}_{#2{.}#3}}
209 \newcommand{\mylist}{\mytyc{List}}
210 \newcommand{\mynil}[1]{\mydc{[]}_{#1}}
211 \newcommand{\mycons}{\mathbin{\mydc{∷}}}
212 \newcommand{\myfoldr}{\myfun{foldr}}
213 \newcommand{\myw}[3]{\myapp{\myapp{\mytyc{W}}{(#1 {:} #2)}}{#3}}
214 \newcommand{\mynodee}{\mathbin{\mydc{$\lhd$}}}
215 \newcommand{\mynode}[2]{\mynodee_{#1.#2}}
216 \newcommand{\myrec}[4]{\myfun{rec}\,#1 / {#2.#3}\,\myfun{with}\,#4}
217 \newcommand{\mylub}{\sqcup}
218 \newcommand{\mydefeq}{\cong}
219 \newcommand{\myrefl}{\mydc{refl}}
220 \newcommand{\mypeq}{\mytyc{=}}
221 \newcommand{\myjeqq}{\myfun{$=$-elim}}
222 \newcommand{\myjeq}[3]{\myapp{\myapp{\myapp{\myjeqq}{#1}}{#2}}{#3}}
223 \newcommand{\mysubst}{\myfun{subst}}
224 \newcommand{\myprsyn}{\myse{prop}}
225 \newcommand{\myprdec}[1]{\mathopen{\mytyc{$\llbracket$}} #1 \mathclose{\mytyc{$\rrbracket$}}}
226 \newcommand{\myand}{\mathrel{\mytyc{$\wedge$}}}
227 \newcommand{\mybigand}{\mathrel{\mytyc{$\bigwedge$}}}
228 \newcommand{\myprfora}[3]{\forall #1 {:} #2.\, #3}
229 \newcommand{\myimpl}{\mathrel{\mytyc{$\Rightarrow$}}}
230 \newcommand{\mybot}{\mytyc{$\bot$}}
231 \newcommand{\mytop}{\mytyc{$\top$}}
232 \newcommand{\mycoe}{\myfun{coe}}
233 \newcommand{\mycoee}[4]{\myapp{\myapp{\myapp{\myapp{\mycoe}{#1}}{#2}}{#3}}{#4}}
234 \newcommand{\mycoh}{\myfun{coh}}
235 \newcommand{\mycohh}[4]{\myapp{\myapp{\myapp{\myapp{\mycoh}{#1}}{#2}}{#3}}{#4}}
236 \newcommand{\myjm}[4]{(#1 {:} #2) \mathrel{\mytyc{=}} (#3 {:} #4)}
237 \newcommand{\myeq}{\mathrel{\mytyc{=}}}
238 \newcommand{\myprop}{\mytyc{Prop}}
239 \newcommand{\mytmup}{\mytmsyn\uparrow}
240 \newcommand{\mydefs}{\Delta}
241 \newcommand{\mynf}{\Downarrow}
242 \newcommand{\myinff}[3]{#1 \vdash #2 \Uparrow #3}
243 \newcommand{\myinf}[2]{\myinff{\myctx}{#1}{#2}}
244 \newcommand{\mychkk}[3]{#1 \vdash #2 \Downarrow #3}
245 \newcommand{\mychk}[2]{\mychkk{\myctx}{#1}{#2}}
246 \newcommand{\myann}[2]{#1 : #2}
247 \newcommand{\mydeclsyn}{\myse{decl}}
248 \newcommand{\myval}[3]{#1 : #2 \mapsto #3}
249 \newcommand{\mypost}[2]{\mysyn{abstract}\ #1 : #2}
250 \newcommand{\myadt}[4]{\mysyn{data}\ #1 #2\ \mysyn{where}\ #3\{ #4 \}}
251 \newcommand{\myreco}[4]{\mysyn{record}\ #1 #2\ \mysyn{where}\ \{ #4 \}}
252 \newcommand{\myelabt}{\vdash}
253 \newcommand{\myelabf}{\rhd}
254 \newcommand{\myelab}[2]{\myctx \myelabt #1 \myelabf #2}
255 \newcommand{\mytele}{\Delta}
256 \newcommand{\mytelee}{\delta}
257 \newcommand{\mydcctx}{\Gamma}
258 \newcommand{\mynamesyn}{\myse{name}}
259 \newcommand{\myvec}{\overrightarrow}
260 \newcommand{\mymeta}{\textsc}
261 \newcommand{\myhyps}{\mymeta{hyps}}
262 \newcommand{\mycc}{;}
263 \newcommand{\myemptytele}{\varepsilon}
264 \newcommand{\mymetagoes}{\Longrightarrow}
265 % \newcommand{\mytesctx}{\
266 \newcommand{\mytelesyn}{\myse{telescope}}
267 \newcommand{\myrecs}{\mymeta{recs}}
268 \newcommand{\myle}{\mathrel{\lcfun{$\le$}}}
269 \newcommand{\mylet}{\mysyn{let}}
270 \newcommand{\myhead}{\mymeta{head}}
271 \newcommand{\mytake}{\mymeta{take}}
272 \newcommand{\myix}{\mymeta{ix}}
273 \newcommand{\myapply}{\mymeta{apply}}
274 \newcommand{\mydataty}{\mymeta{datatype}}
275 \newcommand{\myisreco}{\mymeta{record}}
276 \newcommand{\mydcsep}{\ |\ }
277 \newcommand{\mytree}{\mytyc{Tree}}
278 \newcommand{\myproj}[1]{\myfun{$\pi_{#1}$}}
279 \newcommand{\mysigma}{\mytyc{$\Sigma$}}
280 \newcommand{\mynegder}{\vspace{-0.3cm}}
281 \newcommand{\myquot}{\Uparrow}
282 \newcommand{\mynquot}{\, \Downarrow}
283 \newcommand{\mycanquot}{\ensuremath{\textsc{quote}{\Downarrow}}}
284 \newcommand{\myneuquot}{\ensuremath{\textsc{quote}{\Uparrow}}}
285 \newcommand{\mymetaguard}{\ |\ }
286 \newcommand{\mybox}{\Box}
287 \newcommand{\mytermi}[1]{\text{\texttt{#1}}}
288 \newcommand{\mysee}[1]{\langle\myse{#1}\rangle}
290 \renewcommand{\[}{\begin{equation*}}
291 \renewcommand{\]}{\end{equation*}}
292 \newcommand{\mymacol}[2]{\text{\textcolor{#1}{$#2$}}}
294 \newtheorem*{mydef}{Definition}
295 \newtheoremstyle{named}{}{}{\itshape}{}{\bfseries}{}{.5em}{\textsc{#1}}
298 \pgfdeclarelayer{background}
299 \pgfdeclarelayer{foreground}
300 \pgfsetlayers{background,main,foreground}
302 \definecolor{webgreen}{rgb}{0,.5,0}
303 \definecolor{webbrown}{rgb}{.6,0,0}
304 \definecolor{webyellow}{rgb}{0.98,0.92,0.73}
307 colorlinks=true, linktocpage=true, pdfstartpage=3, pdfstartview=FitV,
308 breaklinks=true, pdfpagemode=UseNone, pageanchor=true, pdfpagemode=UseOutlines,
309 plainpages=false, bookmarksnumbered, bookmarksopen=true, bookmarksopenlevel=1,
310 hypertexnames=true, pdfhighlight=/O, urlcolor=webbrown, linkcolor=black, citecolor=webgreen}
313 %% -----------------------------------------------------------------------------
315 \title{\mykant: Implementing Observational Equality}
316 \author{Francesco Mazzoli \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{<fm2209@ic.ac.uk>}}}
327 \pagenumbering{gobble}
332 % Upper part of the page. The '~' is needed because \\
333 % only works if a paragraph has started.
334 \includegraphics[width=0.4\textwidth]{brouwer-cropped.png}~\\[1cm]
336 \textsc{\Large Final year project}\\[0.5cm]
339 { \huge \mykant: Implementing Observational Equality}\\[1.5cm]
341 {\Large Francesco \textsc{Mazzoli} \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{<fm2209@ic.ac.uk>}}}\\[0.8cm]
343 \begin{minipage}{0.4\textwidth}
344 \begin{flushleft} \large
346 Dr. Steffen \textsc{van Bakel}
349 \begin{minipage}{0.4\textwidth}
350 \begin{flushright} \large
351 \emph{Second marker:} \\
352 Dr. Philippa \textsc{Gardner}
368 The marriage between programming and logic has been a fertile one. In
369 particular, since the definition of the simply typed
370 $\lambda$-calculus, a number of type systems have been devised with
371 increasing expressive power.
373 Among this systems, Intuitionistic Type Theory (ITT) has been a
374 popular framework for theorem provers and programming languages.
375 However, reasoning about equality has always been a tricky business in
376 ITT and related theories. In this thesis we shall explain why this is
377 the case, and present Observational Type Theory (OTT), a solution to
378 some of the problems with equality.
380 To bring OTT closer to the current practice of interactive theorem
381 provers, we describe \mykant, a system featuring OTT in a setting more
382 close to the one found in widely used provers such as Agda and Coq.
383 Most notably, we feature user defined inductive and record types and a
384 cumulative, implicit type hierarchy. Having implemented part of
385 $\mykant$ as a Haskell program, we describe some of the implementation
394 \renewcommand{\abstractname}{Acknowledgements}
396 I would like to thank Steffen van Bakel, my supervisor, who was brave
397 enough to believe in my project and who provided support and
400 I would also like to thank the Haskell and Agda community on
401 \texttt{IRC}, which guided me through the strange world of types; and
402 in particular Andrea Vezzosi and James Deikun, with whom I entertained
403 countless insightful discussions over the past year. Andrea suggested
404 Observational Type Theory as a topic of study: this thesis would not
405 exist without him. Before them, Tony Field introduced me to Haskell,
406 unknowingly filling most of my free time from that time on.
408 Finally, most of the work stems from the research of Conor McBride,
409 who answered many of my doubts through these months. I also owe him
419 \section{Introduction}
421 \pagenumbering{arabic}
423 Functional programming is in good shape. In particular the `well-typed'
424 line of work originating from Milner's ML has been extremely fruitful,
425 in various directions. Nowadays functional, well-typed programming
426 languages like Haskell or OCaml are slowly being absorbed by the
427 mainstream. An important related development---and in fact the original
428 motivator for ML's existence---is the advancement of the practice of
429 \emph{interactive theorem provers}.
432 An interactive theorem prover, or proof assistant, is a tool that lets
433 the user develop formal proofs with the confidence of the machine
434 checking them for correctness. While the effort towards a full
435 formalisation of mathematics has been ongoing for more than a century,
436 theorem provers have been the first class of software whose
437 implementation depends directly on these theories.
439 In a fortunate turn of events, it was discovered that well-typed
440 functional programming and proving theorems in an \emph{intuitionistic}
441 logic are the same activity. Under this discipline, the types in our
442 programming language can be interpreted as proposition in our logic; and
443 the programs implementing the specification given by the types as their
444 proofs. This fact stimulated an active transfer of techniques and
445 knowledge between logic and programming language theory, in both
448 Mathematics could provide programming with a wealth of abstractions and
449 constructs developed over centuries. Moreover, identifying our types
450 with a logic lets us focus on foundational questions regarding
451 programming with a much more solid approach, given the years of rigorous
452 study of logic. Programmers, on the other hand, had already developed a
453 number of approaches to effectively collaborate with computers, through
454 the study of programming languages.
456 In this space, we shall follow the discipline of Intuitionistic Type
457 Theory, or Martin-L\"{o}f Type Theory, after its inventor. First
458 formulated in the 70s and then adjusted through a series of revisions,
459 it has endured as the core of many practical systems in wide use
460 today, and it is the most prominent instance of the proposition-as-types
461 and proofs-as-programs paradigm. One of the most debated subjects in
462 this field has been regarding what notion of equality should be
465 The tension when studying equality in type theory springs from the fact
466 that there is a divide between what the user can prove equal
467 \emph{inside} the theory---what is \emph{propositionally} equal---and
468 what the theorem prover identifies as equal in its meta-theory---what is
469 \emph{definitionally} equal. If we want our system to be well behaved
470 (mostly if we want to keep type checking decidable) we must keep the two
471 notions separate, with definitional equality inducing propositional
472 equality, but not the reverse. However in this scenario propositional
473 equality is weaker than we would like: we can only prove terms equal
474 based on their syntactical structure, and not based on their behaviour.
476 This thesis is concerned with exploring a new approach in this area,
477 \emph{observational} equality. Promising to provide a more adequate
478 propositional equality while retaining well-behavedness, it still is a
479 relatively unexplored notion. We set ourselves to change that by
480 studying it in a setting more akin to the one found in currently
481 available theorem provers.
483 \subsection{Structure}
485 Section \ref{sec:types} will give a brief overview of the
486 $\lambda$-calculus, both typed and untyped. This will give us the
487 chance to introduce most of the concepts mentioned above rigorously, and
488 gain some intuition about them. An excellent introduction to types in
489 general can be found in \cite{Pierce2002}, although not from the
490 perspective of theorem proving.
492 Section \ref{sec:itt} will describe a set of basic construct that form a
493 `baseline' Intuitionistic Type Theory. The goal is to familiarise with
494 the main concept of ITT before attacking the problem of equality. Given
495 the wealth of material covered the exposition is quite dense. Good
496 introductions can be found in \cite{Thompson1991}, \cite{Nordstrom1990},
497 and \cite{Martin-Lof1984} himself.
499 Section \ref{sec:equality} will introduce propositional equality. The
500 properties of propositional equality will be discussed along with its
501 limitations. After reviewing some extensions, we will explain why
502 identifying definitional equality with propositional equality causes
505 Section \ref{sec:ott} will introduce observational equality, following
506 closely the original exposition by \cite{Altenkirch2007}. The
507 presentation is free-standing but glosses over the meta-theoretic
508 properties of OTT, focusing on the mechanisms that make it work.
510 Section \ref{sec:kant-theory} is the central part of the thesis and will
511 describe \mykant, a system we have developed incorporating OTT along
512 constructs usually present in modern theorem provers. Along the way, we
513 discuss these additional features and their trade-offs. Section
514 \ref{sec:kant-practice} will describe an implementation implementing
515 part of \mykant. A high level design of the software is given, along
516 with a few specific implementation issues.
518 Finally, Section \ref{sec:evaluation} will asses the decisions made in
519 designing and implementing \mykant and the results achieved; and Section
520 \ref{sec:future-work} will give a roadmap to bring \mykant\ on par and
521 beyond the competition.
523 \subsection{Contributions}
524 \label{sec:contributions}
526 The contribution of this thesis is threefold:
529 \item Provide a description of observational equality `in context', to
530 make the subject more accessible. Considering the possibilities that
531 OTT brings to the table, we think that introducing it to a wider
532 audience can only be beneficial.
534 \item Fill in the gaps needed to make OTT work with user-defined
535 inductive types and a type hierarchy. We show how one notion of
536 equality is enough, instead of separate notions of value- and
537 type-equality as presented in the original paper. We are able to keep
538 the type equalities `small' while preserving subject reduction by
539 exploiting the fact that we work within a cumulative theory.
540 Incidentally, we also describe a generalised version of bidirectional
541 type checking for user defined types.
543 \item Provide an implementation to probe the possibilities of OTT in a
544 more realistic setting. We have implemented an ITT with user defined
545 types but due to the limited time constraints we were not able to
546 complete the implementation of observational equality. Nonetheless,
547 we describe some interesting implementation issues faced by the type
551 The system developed as part of this thesis, \mykant, incorporates OTT
552 with features that are familiar to users of existing theorem provers
553 adopting the proofs-as-programs mantra. The defining features of
557 \item[Full dependent types] In ITT, types are a very `first class' notion
558 and can be the result of computation---they can \emph{depend} on
559 values, thus the name \emph{dependent types}. \mykant\ espouses this
560 notion to its full consequences.
562 \item[User defined data types and records] Instead of forcing the user
563 to choose from a restricted toolbox, we let her define types for
564 greater flexibility. We have two kinds of user defined types:
565 inductive data types, formed by various data constructors whose type
566 signatures can contain recursive occurrences of the type being
567 defined; and records, where we have just one data constructor, and
568 projections to extract each each field in said constructor.
570 \item[Consistency] Our system is meant to be consistent with respect to
571 the logic it embodies. For this reason, we restrict recursion to
572 \emph{structural} recursion on the defined inductive types, through
573 the use of operators (destructors) computing on each type. Following
574 the types-as-propositions interpretation, each destructor expresses an
575 induction principle on the data type it operates on. To achieve the
576 consistency of these operations we make sure that our recursive data
577 types are \emph{strictly positive}.
579 \item[Bidirectional type checking] We take advantage of a
580 \emph{bidirectional} type inference system in the style of
581 \cite{Pierce2000}. This cuts down the type annotations by a
582 considerable amount in an elegant way and at a very low cost.
583 Bidirectional type checking is usually employed in core calculi, but
584 in \mykant\ we extend the concept to user defined types.
586 \item[Type hierarchy] In set theory we have to take powerset-like
587 objects with care, if we want to avoid paradoxes. However, the
588 working mathematician is rarely concerned by this, and the consistency
589 in this regard is implicitly assumed. In the tradition of
590 \cite{Russell1927}, in \mykant\ we employ a \emph{type hierarchy} to
591 make sure that these size issues are taken care of; and we employ
592 system so that the user will be free from thinking about the
593 hierarchy, just like the mathematician is.
595 \item[Observational equality] The motivator of this thesis, \mykant\
596 incorporates a notion of observational equality, modifying the
597 original presentation by \cite{Altenkirch2007} to fit our more
598 expressive system. As mentioned, we reconcile OTT with user defined
599 types and a type hierarchy.
601 \item[Type holes] When building up programs interactively, it is useful
602 to leave parts unfinished while exploring the current context. This
603 is what type holes are for.
606 \subsection{Notation and syntax}
608 Appendix \ref{app:notation} describes the notation and syntax used in
611 \section{Simple and not-so-simple types}
614 \epigraph{\emph{Well typed programs can't go wrong.}}{Robin Milner}
616 \subsection{The untyped $\lambda$-calculus}
619 Along with Turing's machines, the earliest attempts to formalise
620 computation lead to the definition of the $\lambda$-calculus
621 \citep{Church1936}. This early programming language encodes computation
622 with a minimal syntax and no `data' in the traditional sense, but just
623 functions. Here we give a brief overview of the language, which will
624 give the chance to introduce concepts central to the analysis of all the
625 following calculi. The exposition follows the one found in Chapter 5 of
628 \begin{mydef}[$\lambda$-terms]
629 Syntax of the $\lambda$-calculus: variables, abstractions, and
635 \begin{array}{r@{\ }c@{\ }l}
636 \mytmsyn & ::= & \myb{x} \mysynsep \myabs{\myb{x}}{\mytmsyn} \mysynsep (\myapp{\mytmsyn}{\mytmsyn}) \\
637 x & \in & \text{Some enumerable set of symbols}
642 Parenthesis will be omitted in the usual way, with application being
645 Abstractions roughly corresponds to functions, and their semantics is more
646 formally explained by the $\beta$-reduction rule.
648 \begin{mydef}[$\beta$-reduction]
649 $\beta$-reduction and substitution for the $\lambda$-calculus.
652 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
655 \myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{\myb{x}}{\mytmn}\text{ \textbf{where}} \\
657 \begin{array}{l@{\ }c@{\ }l}
658 \mysub{\myb{y}}{\myb{x}}{\mytmn} \mymetaguard \myb{x} = \myb{y} & \mymetagoes & \mytmn \\
659 \mysub{\myb{y}}{\myb{x}}{\mytmn} & \mymetagoes & \myb{y} \\
660 \mysub{(\myapp{\mytmt}{\mytmm})}{\myb{x}}{\mytmn} & \mymetagoes & (\myapp{\mysub{\mytmt}{\myb{x}}{\mytmn}}{\mysub{\mytmm}{\myb{x}}{\mytmn}}) \\
661 \mysub{(\myabs{\myb{x}}{\mytmm})}{\myb{x}}{\mytmn} & \mymetagoes & \myabs{\myb{x}}{\mytmm} \\
662 \mysub{(\myabs{\myb{y}}{\mytmm})}{\myb{x}}{\mytmn} & \mymetagoes & \myabs{\myb{z}}{\mysub{\mysub{\mytmm}{\myb{y}}{\myb{z}}}{\myb{x}}{\mytmn}} \\
663 \multicolumn{3}{l}{\myind{2} \text{\textbf{with} $\myb{x} \neq \myb{y}$ and $\myb{z}$ not free in $\myapp{\mytmm}{\mytmn}$}}
669 The care required during substituting variables for terms is to avoid
670 name capturing. We will use substitution in the future for other
671 name-binding constructs assuming similar precautions.
673 These few elements have a remarkable expressiveness, and are in fact
674 Turing complete. As a corollary, we must be able to devise a term that
675 reduces forever (`loops' in imperative terms):
677 (\myapp{\omega}{\omega}) \myred (\myapp{\omega}{\omega}) \myred \cdots \text{, \textbf{where} $\omega = \myabs{x}{\myapp{x}{x}}$}
680 A \emph{redex} is a term that can be reduced.
682 In the untyped $\lambda$-calculus this will be the case for an
683 application in which the first term is an abstraction, but in general we
684 call a term reducible if it appears to the left of a reduction rule.
685 \begin{mydef}[normal form]
686 A term that contains no redexes is said to be in \emph{normal form}.
688 \begin{mydef}[normalising terms and systems]
689 Terms that reduce in a finite number of reduction steps to a normal
690 form are \emph{normalising}. A system in which all terms are
691 normalising is said to have the \emph{normalisation property}, or
692 to be \emph{normalising}.
694 Given the reduction behaviour of $(\myapp{\omega}{\omega})$, it is clear
695 that the untyped $\lambda$-calculus does not have the normalisation
698 We have not presented reduction in an algorithmic way, but
699 \emph{evaluation strategies} can be employed to reduce term
700 systematically. Common evaluation strategies include \emph{call by
701 value} (or \emph{strict}), where arguments of abstractions are reduced
702 before being applied to the abstraction; and conversely \emph{call by
703 name} (or \emph{lazy}), where we reduce only when we need to do so to
704 proceed---in other words when we have an application where the function
705 is still not a $\lambda$. In both these strategies we never
706 reduce under an abstraction. For this reason a weaker form of
707 normalisation is used, where all abstractions are said to be in
708 \emph{weak head normal form} even if their body is not.
710 \subsection{The simply typed $\lambda$-calculus}
712 A convenient way to `discipline' and reason about $\lambda$-terms is to
713 assign \emph{types} to them, and then check that the terms that we are
714 forming make sense given our typing rules \citep{Curry1934}. The first
715 most basic instance of this idea takes the name of \emph{simply typed
716 $\lambda$-calculus} (STLC).
717 \begin{mydef}[Simply typed $\lambda$-calculus]
718 The syntax and typing rules for the STLC are given in Figure \ref{fig:stlc}.
721 Our types contain a set of \emph{type variables} $\Phi$, which might
722 correspond to some `primitive' types; and $\myarr$, the type former for
723 `arrow' types, the types of functions. The language is explicitly
724 typed: when we bring a variable into scope with an abstraction, we
725 declare its type. Reduction is unchanged from the untyped
731 \begin{array}{r@{\ }c@{\ }l}
732 \mytmsyn & ::= & \myb{x} \mysynsep \myabss{\myb{x}}{\mytysyn}{\mytmsyn} \mysynsep
733 (\myapp{\mytmsyn}{\mytmsyn}) \\
734 \mytysyn & ::= & \myse{\phi} \mysynsep \mytysyn \myarr \mytysyn \mysynsep \\
735 \myb{x} & \in & \text{Some enumerable set of symbols} \\
736 \myse{\phi} & \in & \Phi
741 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
743 \AxiomC{$\myctx(x) = A$}
744 \UnaryInfC{$\myjud{\myb{x}}{A}$}
747 \AxiomC{$\myjudd{\myctx;\myb{x} : A}{\mytmt}{\mytyb}$}
748 \UnaryInfC{$\myjud{\myabss{x}{A}{\mytmt}}{\mytyb}$}
751 \AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$}
752 \AxiomC{$\myjud{\mytmn}{\mytya}$}
753 \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mytyb}$}
757 \caption{Syntax and typing rules for the STLC. Reduction is unchanged from
758 the untyped $\lambda$-calculus.}
762 In the typing rules, a context $\myctx$ is used to store the types of
763 bound variables: $\myemptyctx$ is the empty context, and $\myctx;
764 \myb{x} : \mytya$ adds a variable to the context. $\myctx(x)$ extracts
765 the type of the rightmost occurrence of $x$.
767 This typing system takes the name of `simply typed lambda calculus' (STLC), and
768 enjoys a number of properties. Two of them are expected in most type systems
770 \begin{mydef}[Progress]
771 A well-typed term is not stuck---it is either a variable, or it does
772 not appear on the left of the $\myred$ relation , or it can take a
773 step according to the evaluation rules.
775 \begin{mydef}[Subject reduction]
776 If a well-typed term takes a step of evaluation, then the
777 resulting term is also well-typed, and preserves the previous type.
780 However, STLC buys us much more: every well-typed term is normalising
781 \citep{Tait1967}. It is easy to see that we cannot fill the blanks if we want to
782 give types to the non-normalising term shown before:
784 \myapp{(\myabss{\myb{x}}{\myhole{?}}{\myapp{\myb{x}}{\myb{x}}})}{(\myabss{\myb{x}}{\myhole{?}}{\myapp{\myb{x}}{\myb{x}}})}
786 This makes the STLC Turing incomplete. We can recover the ability to loop by
787 adding a combinator that recurses:
788 \begin{mydef}[Fixed-point combinator]\end{mydef}
791 \begin{minipage}{0.5\textwidth}
793 $ \mytmsyn ::= \cdots b \mysynsep \myfix{\myb{x}}{\mytysyn}{\mytmsyn} $
797 \begin{minipage}{0.5\textwidth}
798 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}} {
799 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytmt}{\mytya}$}
800 \UnaryInfC{$\myjud{\myfix{\myb{x}}{\mytya}{\mytmt}}{\mytya}$}
805 \mydesc{reduction:}{\myjud{\mytmsyn}{\mytmsyn}}{
806 $ \myfix{\myb{x}}{\mytya}{\mytmt} \myred \mysub{\mytmt}{\myb{x}}{(\myfix{\myb{x}}{\mytya}{\mytmt})}$
809 \mysyn{fix} will deprive us of normalisation, which is a particularly bad thing if we
810 want to use the STLC as described in the next section.
812 Another important property of the STLC is the Church-Rosser property:
813 \begin{mydef}[Church-Rosser property]
814 A system is said to have the \emph{Church-Rosser} property, or to be
815 \emph{confluent}, if given any two reductions $\mytmm$ and $\mytmn$ of
816 a given term $\mytmt$, there is exist a term to which both $\mytmm$
817 and $\mytmn$ can be reduced.
819 Given that the STLC has the normalisation property and the Church-Rosser
820 property, each term has a \emph{unique} normal form.
822 \subsection{The Curry-Howard correspondence}
824 As hinted in the introduction, it turns out that the STLC can be seen a
825 natural deduction system for intuitionistic propositional logic. Terms
826 correspond to proofs, and their types correspond to the propositions
827 they prove. This remarkable fact is known as the Curry-Howard
828 correspondence, or isomorphism.
830 The arrow ($\myarr$) type corresponds to implication. If we wish to prove that
831 that $(\mytya \myarr \mytyb) \myarr (\mytyb \myarr \mytycc) \myarr (\mytya
832 \myarr \mytycc)$, all we need to do is to devise a $\lambda$-term that has the
835 \myabss{\myb{f}}{(\mytya \myarr \mytyb)}{\myabss{\myb{g}}{(\mytyb \myarr \mytycc)}{\myabss{\myb{x}}{\mytya}{\myapp{\myb{g}}{(\myapp{\myb{f}}{\myb{x}})}}}}
837 Which is known to functional programmers as function composition. Going
838 beyond arrow types, we can extend our bare lambda calculus with useful
839 types to represent other logical constructs.
840 \begin{mydef}[The extended STLC]
841 Figure \ref{fig:natded} shows syntax, reduction, and typing rules for
842 the \emph{extended simply typed $\lambda$-calculus}.
848 \begin{array}{r@{\ }c@{\ }l}
849 \mytmsyn & ::= & \cdots \\
850 & | & \mytt \mysynsep \myapp{\myabsurd{\mytysyn}}{\mytmsyn} \\
851 & | & \myapp{\myleft{\mytysyn}}{\mytmsyn} \mysynsep
852 \myapp{\myright{\mytysyn}}{\mytmsyn} \mysynsep
853 \myapp{\mycase{\mytmsyn}{\mytmsyn}}{\mytmsyn} \\
854 & | & \mypair{\mytmsyn}{\mytmsyn} \mysynsep
855 \myapp{\myfst}{\mytmsyn} \mysynsep \myapp{\mysnd}{\mytmsyn} \\
856 \mytysyn & ::= & \cdots \mysynsep \myunit \mysynsep \myempty \mysynsep \mytmsyn \mysum \mytmsyn \mysynsep \mytysyn \myprod \mytysyn
861 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
864 \begin{array}{l@{ }l@{\ }c@{\ }l}
865 \myapp{\mycase{\mytmm}{\mytmn}}{(\myapp{\myleft{\mytya} &}{\mytmt})} & \myred &
866 \myapp{\mytmm}{\mytmt} \\
867 \myapp{\mycase{\mytmm}{\mytmn}}{(\myapp{\myright{\mytya} &}{\mytmt})} & \myred &
868 \myapp{\mytmn}{\mytmt}
873 \begin{array}{l@{ }l@{\ }c@{\ }l}
874 \myapp{\myfst &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmm \\
875 \myapp{\mysnd &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmn
881 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
883 \AxiomC{\phantom{$\myjud{\mytmt}{\myempty}$}}
884 \UnaryInfC{$\myjud{\mytt}{\myunit}$}
887 \AxiomC{$\myjud{\mytmt}{\myempty}$}
888 \UnaryInfC{$\myjud{\myapp{\myabsurd{\mytya}}{\mytmt}}{\mytya}$}
895 \AxiomC{$\myjud{\mytmt}{\mytya}$}
896 \UnaryInfC{$\myjud{\myapp{\myleft{\mytyb}}{\mytmt}}{\mytya \mysum \mytyb}$}
899 \AxiomC{$\myjud{\mytmt}{\mytyb}$}
900 \UnaryInfC{$\myjud{\myapp{\myright{\mytya}}{\mytmt}}{\mytya \mysum \mytyb}$}
908 \AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$}
909 \AxiomC{$\myjud{\mytmn}{\mytya \myarr \mytycc}$}
910 \AxiomC{$\myjud{\mytmt}{\mytya \mysum \mytyb}$}
911 \TrinaryInfC{$\myjud{\myapp{\mycase{\mytmm}{\mytmn}}{\mytmt}}{\mytycc}$}
918 \AxiomC{$\myjud{\mytmm}{\mytya}$}
919 \AxiomC{$\myjud{\mytmn}{\mytyb}$}
920 \BinaryInfC{$\myjud{\mypair{\mytmm}{\mytmn}}{\mytya \myprod \mytyb}$}
923 \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
924 \UnaryInfC{$\myjud{\myapp{\myfst}{\mytmt}}{\mytya}$}
927 \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
928 \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mytyb}$}
932 \caption{Rules for the extended STLC. Only the new features are shown, all the
933 rules and syntax for the STLC apply here too.}
937 Tagged unions (or sums, or coproducts---$\mysum$ here, \texttt{Either}
938 in Haskell) correspond to disjunctions, and dually tuples (or pairs, or
939 products---$\myprod$ here, tuples in Haskell) correspond to
940 conjunctions. This is apparent looking at the ways to construct and
941 destruct the values inhabiting those types: for $\mysum$ $\myleft{ }$
942 and $\myright{ }$ correspond to $\vee$ introduction, and
943 $\mycase{\myarg}{\myarg}$ to $\vee$ elimination; for $\myprod$
944 $\mypair{\myarg}{\myarg}$ corresponds to $\wedge$ introduction, $\myfst$
945 and $\mysnd$ to $\wedge$ elimination.
947 The trivial type $\myunit$ corresponds to the logical $\top$ (true), and
948 dually $\myempty$ corresponds to the logical $\bot$ (false). $\myunit$
949 has one introduction rule ($\mytt$), and thus one inhabitant; and no
950 eliminators---we cannot gain any information from a witness of the
951 single member of $\myunit$. $\myempty$ has no introduction rules, and
952 thus no inhabitants; and one eliminator ($\myabsurd{ }$), corresponding
953 to the logical \emph{ex falso quodlibet}.
955 With these rules, our STLC now looks remarkably similar in power and use to the
956 natural deduction we already know.
957 \begin{mydef}[Negation]
958 $\myneg \mytya$ can be expressed as $\mytya \myarr \myempty$.
960 However, there is an important omission: there is no term of
961 the type $\mytya \mysum \myneg \mytya$ (excluded middle), or equivalently
962 $\myneg \myneg \mytya \myarr \mytya$ (double negation), or indeed any term with
963 a type equivalent to those.
965 This has a considerable effect on our logic and it is no coincidence, since there
966 is no obvious computational behaviour for laws like the excluded middle.
967 Logics of this kind are called \emph{intuitionistic}, or \emph{constructive},
968 and all the systems analysed will have this characteristic since they build on
969 the foundation of the STLC.\footnote{There is research to give computational
970 behaviour to classical logic, but I will not touch those subjects.}
972 As in logic, if we want to keep our system consistent, we must make sure that no
973 closed terms (in other words terms not under a $\lambda$) inhabit $\myempty$.
974 The variant of STLC presented here is indeed
975 consistent, a result that follows from the fact that it is
977 Going back to our $\mysyn{fix}$ combinator, it is easy to see how it ruins our
978 desire for consistency. The following term works for every type $\mytya$,
980 \[(\myfix{\myb{x}}{\mytya}{\myb{x}}) : \mytya\]
982 \subsection{Inductive data}
985 To make the STLC more useful as a programming language or reasoning tool it is
986 common to include (or let the user define) inductive data types. These comprise
987 of a type former, various constructors, and an eliminator (or destructor) that
988 serves as primitive recursor.
990 \begin{mydef}[Finite lists for the STLC]
991 We add a $\mylist$ type constructor, along with an `empty
992 list' ($\mynil{ }$) and `cons cell' ($\mycons$) constructor. The eliminator for
993 lists will be the usual folding operation ($\myfoldr$). Full rules in Figure
1000 \begin{array}{r@{\ }c@{\ }l}
1001 \mytmsyn & ::= & \cdots \mysynsep \mynil{\mytysyn} \mysynsep \mytmsyn \mycons \mytmsyn
1003 \myapp{\myapp{\myapp{\myfoldr}{\mytmsyn}}{\mytmsyn}}{\mytmsyn} \\
1004 \mytysyn & ::= & \cdots \mysynsep \myapp{\mylist}{\mytysyn}
1008 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
1010 \begin{array}{l@{\ }c@{\ }l}
1011 \myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{\mynil{\mytya}} & \myred & \mytmt \\
1013 \myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{(\mytmm \mycons \mytmn)} & \myred &
1014 \myapp{\myapp{\myse{f}}{\mytmm}}{(\myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{\mytmn})}
1018 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
1020 \AxiomC{\phantom{$\myjud{\mytmm}{\mytya}$}}
1021 \UnaryInfC{$\myjud{\mynil{\mytya}}{\myapp{\mylist}{\mytya}}$}
1024 \AxiomC{$\myjud{\mytmm}{\mytya}$}
1025 \AxiomC{$\myjud{\mytmn}{\myapp{\mylist}{\mytya}}$}
1026 \BinaryInfC{$\myjud{\mytmm \mycons \mytmn}{\myapp{\mylist}{\mytya}}$}
1031 \AxiomC{$\myjud{\mysynel{f}}{\mytya \myarr \mytyb \myarr \mytyb}$}
1032 \AxiomC{$\myjud{\mytmm}{\mytyb}$}
1033 \AxiomC{$\myjud{\mytmn}{\myapp{\mylist}{\mytya}}$}
1034 \TrinaryInfC{$\myjud{\myapp{\myapp{\myapp{\myfoldr}{\mysynel{f}}}{\mytmm}}{\mytmn}}{\mytyb}$}
1037 \caption{Rules for lists in the STLC.}
1041 In Section \ref{sec:well-order} we will see how to give a general account of
1044 \section{Intuitionistic Type Theory}
1047 \epigraph{\emph{Martin-L{\"o}f's type theory is a well established and
1048 convenient arena in which computational Christians are regularly
1049 fed to logical lions.}}{Conor McBride}
1051 \subsection{Extending the STLC}
1053 \cite{Barendregt1991} succinctly expressed geometrically how we can add
1054 expressively to the STLC:
1056 \xymatrix@!0@=1.5cm{
1057 & \lambda\omega \ar@{-}[rr]\ar@{-}'[d][dd]
1058 & & \lambda C \ar@{-}[dd]
1060 \lambda2 \ar@{-}[ur]\ar@{-}[rr]\ar@{-}[dd]
1061 & & \lambda P2 \ar@{-}[ur]\ar@{-}[dd]
1063 & \lambda\underline\omega \ar@{-}'[r][rr]
1064 & & \lambda P\underline\omega
1066 \lambda{\to} \ar@{-}[rr]\ar@{-}[ur]
1067 & & \lambda P \ar@{-}[ur]
1070 Here $\lambda{\to}$, in the bottom left, is the STLC. From there can move along
1073 \item[Terms depending on types (towards $\lambda{2}$)] We can quantify over
1074 types in our type signatures. For example, we can define a polymorphic
1075 identity function, where $\mytyp$ denotes the `type of types':
1077 (\myabss{\myb{A}}{\mytyp}{\myabss{\myb{x}}{\myb{A}}{\myb{x}}}) : (\myb{A} {:} \mytyp) \myarr \myb{A} \myarr \myb{A}
1079 The first and most famous instance of this idea has been System F.
1080 This form of polymorphism and has been wildly successful, also thanks
1081 to a well known inference algorithm for a restricted version of System
1082 F known as Hindley-Milner \citep{milner1978theory}. Languages like
1083 Haskell and SML are based on this discipline. In Haskell the above
1089 Where \texttt{a} implicitly quantifies over a type, and will be
1090 instantiated automatically when \texttt{id} is used thanks to the type inference.
1091 \item[Types depending on types (towards $\lambda{\underline{\omega}}$)] We have
1092 type operators. For example we could define a function that given types $R$
1093 and $\mytya$ forms the type that represents a value of type $\mytya$ in
1094 continuation passing style:
1095 \[\displaystyle(\myabss{\myb{R} \myappsp \myb{A}}{\mytyp}{(\myb{A}
1096 \myarr \myb{R}) \myarr \myb{R}}) : \mytyp \myarr \mytyp \myarr \mytyp
1098 In Haskell we can define type operator of sorts, although we must
1099 pair them with data constructors, to keep inference manageable:
1101 newtype Cont r a = Cont ((a -> r) -> r)
1103 Where the `type' (kind in Haskell parlance) of \texttt{Cont} will be
1104 \texttt{* -> * -> *}, with \texttt{*} signifying the type of types.
1105 \item[Types depending on terms (towards $\lambda{P}$)] Also known as `dependent
1106 types', give great expressive power. For example, we can have values of whose
1107 type depend on a boolean:
1108 \[\displaystyle(\myabss{\myb{x}}{\mybool}{\myite{\myb{x}}{\mynat}{\myrat}}) : \mybool
1109 \myarr \mytyp\] We cannot give an Haskell example that expresses this
1110 concept since Haskell does not support dependent types---it would be a
1111 very different language if it did.
1114 All the systems placed on the cube preserve the properties that make the
1115 STLC well behaved. The one we are going to focus on, Intuitionistic
1116 Type Theory, has all of the above additions, and thus would sit where
1117 $\lambda{C}$ sits. It will serve as the logical
1118 `core' of all the other extensions that we will present and ultimately
1119 our implementation of a similar logic.
1121 \subsection{A Bit of History}
1123 Logic frameworks and programming languages based on type theory have a
1124 long history. Per Martin-L\"{o}f described the first version of his
1125 theory in 1971, but then revised it since the original version was
1126 inconsistent due to its impredicativity.\footnote{In the early version
1127 there was only one universe $\mytyp$ and $\mytyp : \mytyp$; see
1128 Section \ref{sec:term-types} for an explanation on why this causes
1129 problems.} For this reason he later gave a revised and consistent
1130 definition \citep{Martin-Lof1984}.
1132 A related development is the polymorphic $\lambda$-calculus, and specifically
1133 the previously mentioned System F, which was developed independently by Girard
1134 and Reynolds. An overview can be found in \citep{Reynolds1994}. The surprising
1135 fact is that while System F is impredicative it is still consistent and strongly
1136 normalising. \cite{Coquand1986} further extended this line of work with the
1137 Calculus of Constructions (CoC).
1139 Most widely used interactive theorem provers are based on ITT. Popular
1140 ones include Agda \citep{Norell2007}, Coq \citep{Coq}, Epigram
1141 \citep{McBride2004, EpigramTut}, Isabelle \citep{Paulson1990}, and many
1144 \subsection{A simple type theory}
1147 The calculus I present follows the exposition in \cite{Thompson1991},
1148 and is quite close to the original formulation of \cite{Martin-Lof1984}.
1149 Agda and \mykant\ renditions of the presented theory and all the
1150 examples (even the ones presented only as type signatures) are
1151 reproduced in Appendix \ref{app:itt-code}.
1152 \begin{mydef}[Intuitionistic Type Theory (ITT)]
1153 The syntax and reduction rules are shown in Figure \ref{fig:core-tt-syn}.
1154 The typing rules are presented piece by piece in the following sections.
1160 \begin{array}{r@{\ }c@{\ }l}
1161 \mytmsyn & ::= & \myb{x} \mysynsep
1162 \mytyp_{level} \mysynsep
1163 \myunit \mysynsep \mytt \mysynsep
1164 \myempty \mysynsep \myapp{\myabsurd{\mytmsyn}}{\mytmsyn} \\
1165 & | & \mybool \mysynsep \mytrue \mysynsep \myfalse \mysynsep
1166 \myitee{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
1167 & | & \myfora{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
1168 \myabss{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
1169 (\myapp{\mytmsyn}{\mytmsyn}) \\
1170 & | & \myexi{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
1171 \mypairr{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn} \\
1172 & | & \myapp{\myfst}{\mytmsyn} \mysynsep \myapp{\mysnd}{\mytmsyn} \\
1173 & | & \myw{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
1174 \mytmsyn \mynode{\myb{x}}{\mytmsyn} \mytmsyn \\
1175 & | & \myrec{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn} \\
1176 level & \in & \mathbb{N}
1181 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
1182 \begin{tabular}{ccc}
1184 \begin{array}{l@{ }l@{\ }c@{\ }l}
1185 \myitee{\mytrue &}{\myb{x}}{\myse{P}}{\mytmm}{\mytmn} & \myred & \mytmm \\
1186 \myitee{\myfalse &}{\myb{x}}{\myse{P}}{\mytmm}{\mytmn} & \myred & \mytmn \\
1191 \myapp{(\myabss{\myb{x}}{\mytya}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{\myb{x}}{\mytmn}
1195 \begin{array}{l@{ }l@{\ }c@{\ }l}
1196 \myapp{\myfst &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmm \\
1197 \myapp{\mysnd &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmn
1205 \myrec{(\myse{s} \mynode{\myb{x}}{\myse{T}} \myse{f})}{\myb{y}}{\myse{P}}{\myse{p}} \myred
1206 \myapp{\myapp{\myapp{\myse{p}}{\myse{s}}}{\myse{f}}}{(\myabss{\myb{t}}{\mysub{\myse{T}}{\myb{x}}{\myse{s}}}{
1207 \myrec{\myapp{\myse{f}}{\myb{t}}}{\myb{y}}{\myse{P}}{\mytmt}
1211 \caption{Syntax and reduction rules for our type theory.}
1212 \label{fig:core-tt-syn}
1215 \subsubsection{Types are terms, some terms are types}
1216 \label{sec:term-types}
1218 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1220 \AxiomC{$\myjud{\mytmt}{\mytya}$}
1221 \AxiomC{$\mytya \mydefeq \mytyb$}
1222 \BinaryInfC{$\myjud{\mytmt}{\mytyb}$}
1225 \AxiomC{\phantom{$\myjud{\mytmt}{\mytya}$}}
1226 \UnaryInfC{$\myjud{\mytyp_l}{\mytyp_{l + 1}}$}
1231 The first thing to notice is that the barrier between values and types that we had
1232 in the STLC is gone: values can appear in types, and the two are treated
1233 uniformly in the syntax.
1235 While the usefulness of doing this will become clear soon, a consequence is
1236 that since types can be the result of computation, deciding type equality is
1237 not immediate as in the STLC.
1238 \begin{mydef}[Definitional equality]
1239 We define \emph{definitional
1240 equality}, $\mydefeq$, as the congruence relation extending
1241 $\myred$. Moreover, when comparing terms syntactically we do it up to
1242 renaming of bound names ($\alpha$-renaming).
1244 For example under this discipline we will find that
1247 \myabss{\myb{x}}{\mytya}{\myb{x}} \mydefeq \myabss{\myb{y}}{\mytya}{\myb{y}} \\
1248 \myapp{(\myabss{\myb{f}}{\mytya \myarr \mytya}{\myb{f}})}{(\myabss{\myb{y}}{\mytya}{\myb{y}})} \mydefeq \myabss{\myb{quux}}{\mytya}{\myb{quux}}
1251 Types that are definitionally equal can be used interchangeably. Here
1252 the `conversion' rule is not syntax directed, but it is possible to
1253 employ $\myred$ to decide term equality in a systematic way, comparing
1254 terms by reducing them to their unique normal forms first; so that a separate conversion rule is not needed.
1255 Another thing to notice is that, considering the need to reduce terms to
1256 decide equality, for type checking to be decidable a dependently typed
1257 must be terminating and confluent; since every type needs to have a
1258 unique normal form for definitional equality to be decidable.
1260 Moreover, we specify a \emph{type hierarchy} to talk about `large'
1261 types: $\mytyp_0$ will be the type of types inhabited by data:
1262 $\mybool$, $\mynat$, $\mylist$, etc. $\mytyp_1$ will be the type of
1263 $\mytyp_0$, and so on---for example we have $\mytrue : \mybool :
1264 \mytyp_0 : \mytyp_1 : \cdots$. Each type `level' is often called a
1265 universe in the literature. While it is possible to simplify things by
1266 having only one universe $\mytyp$ with $\mytyp : \mytyp$, this plan is
1267 inconsistent for much the same reason that impredicative na\"{\i}ve set
1268 theory is \citep{Hurkens1995}. However various techniques can be
1269 employed to lift the burden of explicitly handling universes, as we will
1270 see in Section \ref{sec:term-hierarchy}.
1272 \subsubsection{Contexts}
1274 \begin{minipage}{0.5\textwidth}
1275 \mydesc{context validity:}{\myvalid{\myctx}}{
1277 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
1278 \UnaryInfC{$\myvalid{\myemptyctx}$}
1281 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
1282 \UnaryInfC{$\myvalid{\myctx ; \myb{x} : \mytya}$}
1287 \begin{minipage}{0.5\textwidth}
1288 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1289 \AxiomC{$\myctx(x) = \mytya$}
1290 \UnaryInfC{$\myjud{\myb{x}}{\mytya}$}
1296 We need to refine the notion of context to make sure that every variable appearing
1297 is typed correctly, or that in other words each type appearing in the context is
1298 indeed a type and not a value. In every other rule, if no premises are present,
1299 we assume the context in the conclusion to be valid.
1301 Then we can re-introduce the old rule to get the type of a variable for a
1304 \subsubsection{$\myunit$, $\myempty$}
1306 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1307 \begin{tabular}{ccc}
1308 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
1309 \UnaryInfC{$\myjud{\myunit}{\mytyp_0}$}
1311 \UnaryInfC{$\myjud{\myempty}{\mytyp_0}$}
1314 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
1315 \UnaryInfC{$\myjud{\mytt}{\myunit}$}
1317 \UnaryInfC{\phantom{$\myjud{\myempty}{\mytyp_0}$}}
1320 \AxiomC{$\myjud{\mytmt}{\myempty}$}
1321 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
1322 \BinaryInfC{$\myjud{\myapp{\myabsurd{\mytya}}{\mytmt}}{\mytya}$}
1324 \UnaryInfC{\phantom{$\myjud{\myempty}{\mytyp_0}$}}
1329 Nothing surprising here: $\myunit$ and $\myempty$ are unchanged from the STLC,
1330 with the added rules to type $\myunit$ and $\myempty$ themselves, and to make
1331 sure that we are invoking $\myabsurd{}$ over a type.
1333 \subsubsection{$\mybool$, and dependent $\myfun{if}$}
1335 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1336 \begin{tabular}{ccc}
1338 \UnaryInfC{$\myjud{\mybool}{\mytyp_0}$}
1342 \UnaryInfC{$\myjud{\mytrue}{\mybool}$}
1346 \UnaryInfC{$\myjud{\myfalse}{\mybool}$}
1351 \AxiomC{$\myjud{\mytmt}{\mybool}$}
1352 \AxiomC{$\myjudd{\myctx : \mybool}{\mytya}{\mytyp_l}$}
1354 \BinaryInfC{$\myjud{\mytmm}{\mysub{\mytya}{x}{\mytrue}}$ \hspace{0.7cm} $\myjud{\mytmn}{\mysub{\mytya}{x}{\myfalse}}$}
1355 \UnaryInfC{$\myjud{\myitee{\mytmt}{\myb{x}}{\mytya}{\mytmm}{\mytmn}}{\mysub{\mytya}{\myb{x}}{\mytmt}}$}
1359 With booleans we get the first taste of the `dependent' in `dependent
1360 types'. While the two introduction rules for $\mytrue$ and $\myfalse$
1361 are not surprising, the rule for $\myfun{if}$ is. In most
1362 strongly typed languages we expect the branches of an $\myfun{if}$
1363 statements to be of the same type, to preserve subject reduction, since
1364 execution could take both paths. This is a pity, since the type system
1365 does not reflect the fact that in each branch we gain knowledge on the
1366 term we are branching on. Which means that programs along the lines of
1368 if null xs then head xs else 0
1370 are a necessary, well-typed, danger.
1372 However, in a more expressive system, we can do better: the branches'
1373 type can depend on the value of the scrutinised boolean. This is what
1374 the typing rule expresses: the user provides a type $\mytya$ ranging
1375 over an $\myb{x}$ representing the boolean we are operating the
1376 $\myfun{if}$ switch with, and each branch is type checked against
1377 $\mytya$ with the updated knowledge of the value of $\myb{x}$.
1379 \subsubsection{$\myarr$, or dependent function}
1382 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1383 \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
1384 \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
1385 \BinaryInfC{$\myjud{\myfora{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
1391 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytmt}{\mytyb}$}
1392 \UnaryInfC{$\myjud{\myabss{\myb{x}}{\mytya}{\mytmt}}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
1395 \AxiomC{$\myjud{\mytmm}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
1396 \AxiomC{$\myjud{\mytmn}{\mytya}$}
1397 \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mysub{\mytyb}{\myb{x}}{\mytmn}}$}
1402 Dependent functions are one of the two key features that characterise
1403 dependent types---the other being dependent products. With dependent
1404 functions, the result type can depend on the value of the argument.
1405 This feature, together with the fact that the result type might be a
1406 type itself, brings a lot of interesting possibilities. In the
1407 introduction rule, the return type is type checked in a context with an
1408 abstracted variable of domain's type; and in the elimination rule the
1409 actual argument is substituted in the return type. Keeping the
1410 correspondence with logic alive, dependent functions are much like
1411 universal quantifiers ($\forall$) in logic.
1413 For example, assuming that we have lists and natural numbers in our
1414 language, using dependent functions we can write functions of
1418 \myfun{length} : (\myb{A} {:} \mytyp_0) \myarr \myapp{\mylist}{\myb{A}} \myarr \mynat \\
1419 \myarg \myfun{$>$} \myarg : \mynat \myarr \mynat \myarr \mytyp_0 \\
1420 \myfun{head} : (\myb{A} {:} \mytyp_0) \myarr (\myb{l} {:} \myapp{\mylist}{\myb{A}})
1421 \myarr \myapp{\myapp{\myfun{length}}{\myb{A}}}{\myb{l}} \mathrel{\myfun{$>$}} 0 \myarr
1426 \myfun{length} is the usual polymorphic length
1427 function. $\myarg\myfun{$>$}\myarg$ is a function that takes two
1428 naturals and returns a type: if the lhs is greater then the rhs,
1429 $\myunit$ is returned, $\myempty$ otherwise. This way, we can express a
1430 `non-emptiness' condition in $\myfun{head}$, by including a proof that
1431 the length of the list argument is non-zero. This allows us to rule out
1432 the empty list case by invoking \myfun{absurd} in \myfun{length}, so
1433 that we can safely return the first element.
1435 Finally, we need to make sure that the type hierarchy is respected, which
1436 is the reason why a type formed by $\myarr$ will live in the least upper
1437 bound of the levels of argument and return type.
1439 \subsubsection{$\myprod$, or dependent product}
1442 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1443 \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
1444 \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
1445 \BinaryInfC{$\myjud{\myexi{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
1451 \AxiomC{$\myjud{\mytmm}{\mytya}$}
1452 \AxiomC{$\myjud{\mytmn}{\mysub{\mytyb}{\myb{x}}{\mytmm}}$}
1453 \BinaryInfC{$\myjud{\mypairr{\mytmm}{\myb{x}}{\mytyb}{\mytmn}}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
1455 \UnaryInfC{\phantom{$--$}}
1458 \AxiomC{$\myjud{\mytmt}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
1459 \UnaryInfC{$\hspace{0.7cm}\myjud{\myapp{\myfst}{\mytmt}}{\mytya}\hspace{0.7cm}$}
1461 \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mysub{\mytyb}{\myb{x}}{\myapp{\myfst}{\mytmt}}}$}
1466 If dependent functions are a generalisation of $\myarr$ in the STLC,
1467 dependent products are a generalisation of $\myprod$ in the STLC. The
1468 improvement is that the second element's type can depend on the value of
1469 the first element. The correspondence with logic is through the
1470 existential quantifier: $\exists x \in \mathbb{N}. even(x)$ can be
1471 expressed as $\myexi{\myb{x}}{\mynat}{\myapp{\myfun{even}}{\myb{x}}}$.
1472 The first element will be a number, and the second evidence that the
1473 number is even. This highlights the fact that we are working in a
1474 constructive logic: if we have an existence proof, we can always ask for
1475 a witness. This means, for instance, that $\neg \forall \neg$ is not
1476 equivalent to $\exists$. Additionally, we need to specify the type of
1477 the second element (ranging over the first element) explicitly when
1478 using $\mypair{\myarg}{\myarg}$.
1480 Another perhaps more `dependent' application of products, paired with
1481 $\mybool$, is to offer choice between different types. For example we
1482 can easily recover disjunctions:
1485 \myarg\myfun{$\vee$}\myarg : \mytyp_0 \myarr \mytyp_0 \myarr \mytyp_0 \\
1486 \myb{A} \mathrel{\myfun{$\vee$}} \myb{B} \mapsto \myexi{\myb{x}}{\mybool}{\myite{\myb{x}}{\myb{A}}{\myb{B}}} \\ \ \\
1487 \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} \\
1488 \myfun{case} \myappsp \myb{A} \myappsp \myb{B} \myappsp \myb{C} \myappsp \myb{f} \myappsp \myb{g} \myappsp \myb{x} \mapsto \\
1489 \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}})}
1493 \subsubsection{$\mytyc{W}$, or well-order}
1494 \label{sec:well-order}
1496 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1498 \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
1499 \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
1500 \BinaryInfC{$\myjud{\myw{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
1505 \AxiomC{$\myjud{\mytmt}{\mytya}$}
1506 \AxiomC{$\myjud{\mysynel{f}}{\mysub{\mytyb}{\myb{x}}{\mytmt} \myarr \myw{\myb{x}}{\mytya}{\mytyb}}$}
1507 \BinaryInfC{$\myjud{\mytmt \mynode{\myb{x}}{\mytyb} \myse{f}}{\myw{\myb{x}}{\mytya}{\mytyb}}$}
1513 \AxiomC{$\myjud{\myse{u}}{\myw{\myb{x}}{\myse{S}}{\myse{T}}}$}
1514 \AxiomC{$\myjudd{\myctx; \myb{w} : \myw{\myb{x}}{\myse{S}}{\myse{T}}}{\myse{P}}{\mytyp_l}$}
1516 \BinaryInfC{$\myjud{\myse{p}}{
1517 \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}}}}
1519 \UnaryInfC{$\myjud{\myrec{\myse{u}}{\myb{w}}{\myse{P}}{\myse{p}}}{\mysub{\myse{P}}{\myb{w}}{\myse{u}}}$}
1523 Finally, the well-order type, or in short $\mytyc{W}$-type, which will
1524 let us represent inductive data in a general way. We can form `nodes'
1525 of the shape \[\mytmt \mynode{\myb{x}}{\mytyb} \myse{f} :
1526 \myw{\myb{x}}{\mytya}{\mytyb}\] where $\mytmt$ is of type $\mytya$ and
1527 is the data present in the node, and $\myse{f}$ specifies a `child' of
1528 the node for each member of $\mysub{\mytyb}{\myb{x}}{\mytmt}$. The
1529 $\myfun{rec}\ \myfun{with}$ acts as an induction principle on
1530 $\mytyc{W}$, given a predicate and a function dealing with the inductive
1531 case---we will gain more intuition about inductive data in Section
1532 \ref{sec:user-type}.
1534 For example, if we want to form natural numbers, we can take
1537 \mytyc{Tr} : \mybool \myarr \mytyp_0 \\
1538 \mytyc{Tr} \myappsp \myb{b} \mapsto \myfun{if}\, \myb{b}\, \myfun{then}\, \myunit\, \myfun{else}\, \myempty \\
1540 \mynat : \mytyp_0 \\
1541 \mynat \mapsto \myw{\myb{b}}{\mybool}{(\mytyc{Tr}\myappsp\myb{b})}
1544 Each node will contain a boolean. If $\mytrue$, the number is non-zero,
1545 and we will have one child representing its predecessor, given that
1546 $\mytyc{Tr}$ will return $\myunit$. If $\myfalse$, the number is zero,
1547 and we will have no predecessors (children), given the $\myempty$:
1550 \mydc{zero} : \mynat \\
1551 \mydc{zero} \mapsto \myfalse \mynodee (\myabs{\myb{x}}{\myabsurd{\mynat} \myappsp \myb{x}}) \\
1553 \mydc{suc} : \mynat \myarr \mynat \\
1554 \mydc{suc}\myappsp \myb{x} \mapsto \mytrue \mynodee (\myabs{\myarg}{\myb{x}})
1557 And with a bit of effort, we can recover addition:
1560 \myfun{plus} : \mynat \myarr \mynat \myarr \mynat \\
1561 \myfun{plus} \myappsp \myb{x} \myappsp \myb{y} \mapsto \\
1562 \myind{2} \myfun{rec}\, \myb{x} / \myb{b}.\mynat \, \\
1563 \myind{2} \myfun{with}\, \myabs{\myb{b}}{\\
1564 \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) \\
1565 \myind{2}\myind{2}\myfun{then}\,(\myabs{\myarg\, \myb{f}}{\mydc{suc}\myappsp (\myapp{\myb{f}}{\mytt})})\, \myfun{else}\, (\myabs{\myarg\, \myarg}{\myb{y}})}
1568 Note how we explicitly have to type the branches to make them match
1569 with the definition of $\mynat$. This gives a taste of the clumsiness
1570 of $\mytyc{W}$-types but not the whole story. Well-orders are
1571 inadequate not only because they are verbose, but also because they
1572 face deeper problems due to the weakness of the notion of equality
1573 present in most type theories, which we will present in the next
1574 section \citep{dybjer1997representing}. The `better' equality we will
1575 present in Section \ref{sec:ott} helps but does not fully resolve
1576 these issues.\footnote{See \url{http://www.e-pig.org/epilogue/?p=324},
1577 which concludes with `W-types are a powerful conceptual tool, but
1578 they’re no basis for an implementation of recursive data types in
1579 decidable type theories.'} For this reasons \mytyc{W}-types have
1580 remained nothing more than a reasoning tool, and practical systems
1581 must implement more manageable ways to represent data.
1583 \section{The struggle for equality}
1584 \label{sec:equality}
1586 \epigraph{\emph{Half of my time spent doing research involves thinking up clever
1587 schemes to avoid needing functional extensionality.}}{@larrytheliquid}
1589 In the previous section we learnt how a type checker for ITT needs
1590 a notion of \emph{definitional equality}. Beyond this meta-theoretic
1591 notion, in this section we will explore the ways of expressing equality
1592 \emph{inside} the theory, as a reasoning tool available to the user.
1593 This area is the main concern of this thesis, and in general a very
1594 active research topic, since we do not have a fully satisfactory
1595 solution, yet. As in the previous section, everything presented is
1596 formalised in Agda in Appendix \ref{app:agda-itt}.
1598 \subsection{Propositional equality}
1600 \begin{mydef}[Propositional equality] The syntax, reduction, and typing
1601 rules for propositional equality and related constructs are defined
1606 \begin{minipage}{0.5\textwidth}
1609 \begin{array}{r@{\ }c@{\ }l}
1610 \mytmsyn & ::= & \cdots \\
1611 & | & \mypeq \myappsp \mytmsyn \myappsp \mytmsyn \myappsp \mytmsyn \mysynsep
1612 \myapp{\myrefl}{\mytmsyn} \\
1613 & | & \myjeq{\mytmsyn}{\mytmsyn}{\mytmsyn}
1618 \begin{minipage}{0.5\textwidth}
1619 \mydesc{\phantom{y}reduction:}{\mytmsyn \myred \mytmsyn}{
1621 \myjeq{\myse{P}}{(\myapp{\myrefl}{\mytmm})}{\mytmn} \myred \mytmn
1627 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1628 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
1629 \AxiomC{$\myjud{\mytmm}{\mytya}$}
1630 \AxiomC{$\myjud{\mytmn}{\mytya}$}
1631 \TrinaryInfC{$\myjud{\mypeq \myappsp \mytya \myappsp \mytmm \myappsp \mytmn}{\mytyp_l}$}
1637 \AxiomC{$\begin{array}{c}\ \\\myjud{\mytmm}{\mytya}\hspace{1.1cm}\mytmm \mydefeq \mytmn\end{array}$}
1638 \UnaryInfC{$\myjud{\myapp{\myrefl}{\mytmm}}{\mypeq \myappsp \mytya \myappsp \mytmm \myappsp \mytmn}$}
1643 \myjud{\myse{P}}{\myfora{\myb{x}\ \myb{y}}{\mytya}{\myfora{q}{\mypeq \myappsp \mytya \myappsp \myb{x} \myappsp \myb{y}}{\mytyp_l}}} \\
1644 \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})}}
1647 \UnaryInfC{$\myjud{\myjeq{\myse{P}}{\myse{q}}{\myse{p}}}{\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmn}}{q}}$}
1653 To express equality between two terms inside ITT, the obvious way to do
1654 so is to have equality to be a type. Here we present what has survived
1655 as the dominating form of equality in systems based on ITT up since
1656 \cite{Martin-Lof1984} up to the present day.
1658 Our type former is $\mypeq$, which given a type relates equal terms of
1659 that type. $\mypeq$ has one introduction rule, $\myrefl$, which
1660 introduces an equality between definitionally equal terms---a proof by
1663 Finally, we have one eliminator for $\mypeq$ , $\myjeqq$ (also known as
1664 `\myfun{J} axiom' in the literature).
1665 $\myjeq{\myse{P}}{\myse{q}}{\myse{p}}$ takes
1667 \item $\myse{P}$, a predicate working with two terms of a certain type (say
1668 $\mytya$) and a proof of their equality;
1669 \item $\myse{q}$, a proof that two terms in $\mytya$ (say $\myse{m}$ and
1670 $\myse{n}$) are equal;
1671 \item and $\myse{p}$, an inhabitant of $\myse{P}$ applied to $\myse{m}$
1672 twice, plus the trivial proof by reflexivity showing that $\myse{m}$
1675 Given these ingredients, $\myjeqq$ returns a member of $\myse{P}$
1676 applied to $\mytmm$, $\mytmn$, and $\myse{q}$. In other words $\myjeqq$
1677 takes a witness that $\myse{P}$ works with \emph{definitionally equal}
1678 terms, and returns a witness of $\myse{P}$ working with
1679 \emph{propositionally equal} terms. Given its reduction rules,
1680 invocations of $\myjeqq$ will vanish when the equality proofs will
1681 reduce to invocations to reflexivity, at which point the arguments must
1682 be definitionally equal, and thus the provided
1683 $\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmm}}{(\myapp{\myrefl}{\mytmm})}$
1684 can be returned. This means that $\myjeqq$ will not compute with
1685 hypothetical proofs, which makes sense given that they might be false.
1687 While the $\myjeqq$ rule is slightly convoluted, we can derive many more
1688 `friendly' rules from it, for example a more obvious `substitution' rule, that
1689 replaces equal for equal in predicates:
1692 \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}}}}} \\
1693 \myfun{subst}\myappsp \myb{A}\myappsp\myb{P}\myappsp\myb{x}\myappsp\myb{y}\myappsp\myb{q}\myappsp\myb{p} \mapsto
1694 \myjeq{(\myabs{\myb{x}\ \myb{y}\ \myb{q}}{\myapp{\myb{P}}{\myb{y}}})}{\myb{p}}{\myb{q}}
1697 Once we have $\myfun{subst}$, we can easily prove more familiar laws
1698 regarding equality, such as symmetry, transitivity, congruence laws,
1699 etc.\footnote{For definitions of these functions, refer to Appendix \ref{app:itt-code}.}
1701 \subsection{Common extensions}
1702 \label{sec:extensions}
1704 Our definitional and propositional equalities can be enhanced in various
1705 ways. Obviously if we extend the definitional equality we are also
1706 automatically extend propositional equality, given how $\myrefl$ works.
1708 \subsubsection{$\eta$-expansion}
1709 \label{sec:eta-expand}
1711 A simple extension to our definitional equality is achieved by $\eta$-expansion.
1712 Given an abstract variable $\myb{f} : \mytya \myarr \mytyb$ the aim is
1713 to have that $\myb{f} \mydefeq
1714 \myabss{\myb{x}}{\mytya}{\myapp{\myb{f}}{\myb{x}}}$. We can achieve
1715 this by `expanding' terms depending on their types, a process known as
1716 \emph{quotation}---a term borrowed from the practice of
1717 \emph{normalisation by evaluation}, where we embed terms in some host
1718 language with an existing notion of computation, and then reify them
1719 back into terms, which will `smooth out' differences like the one above
1722 The same concept applies to $\myprod$, where we expand each inhabitant
1723 reconstructing it by getting its projections, so that $\myb{x}
1724 \mydefeq \mypair{\myfst \myappsp \myb{x}}{\mysnd \myappsp \myb{x}}$.
1725 Similarly, all one inhabitants of $\myunit$ and all zero inhabitants of
1726 $\myempty$ can be considered equal. Quotation can be performed in a
1727 type-directed way, as we will witness in Section \ref{sec:kant-irr}.
1729 \begin{mydef}[Congruence and $\eta$-laws]
1730 To justify quotation in our type system we add a congruence law for
1731 abstractions and a similar law for products, plus the fact that all
1732 elements of $\myunit$ or $\myempty$ are equal.
1735 \mydesc{definitional equality:}{\myjud{\mytmm \mydefeq \mytmn}{\mytmsyn}}{
1737 \AxiomC{$\myjudd{\myctx; \myb{y} : \mytya}{\myapp{\myse{f}}{\myb{x}} \mydefeq \myapp{\myse{g}}{\myb{x}}}{\mysub{\mytyb}{\myb{x}}{\myb{y}}}$}
1738 \UnaryInfC{$\myjud{\myse{f} \mydefeq \myse{g}}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
1741 \AxiomC{$\myjud{\mypair{\myapp{\myfst}{\mytmm}}{\myapp{\mysnd}{\mytmm}} \mydefeq \mypair{\myapp{\myfst}{\mytmn}}{\myapp{\mysnd}{\mytmn}}}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
1742 \UnaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
1749 \AxiomC{$\myjud{\mytmm}{\myunit}$}
1750 \AxiomC{$\myjud{\mytmn}{\myunit}$}
1751 \BinaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\myunit}$}
1754 \AxiomC{$\myjud{\mytmm}{\myempty}$}
1755 \AxiomC{$\myjud{\mytmn}{\myempty}$}
1756 \BinaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\myempty}$}
1761 \subsubsection{Uniqueness of identity proofs}
1763 Another common but controversial addition to propositional equality is
1764 the $\myfun{K}$ axiom, which essentially states that all equality proofs
1767 \begin{mydef}[$\myfun{K}$ axiom]\end{mydef}
1768 \mydesc{typing:}{\myjud{\mytmm \mydefeq \mytmn}{\mytmsyn}}{
1771 \myjud{\myse{P}}{\myfora{\myb{x}}{\mytya}{\mypeq \myappsp \mytya \myappsp \myb{x}\myappsp \myb{x} \myarr \mytyp}} \\\
1772 \myjud{\mytmt}{\mytya} \hspace{1cm}
1773 \myjud{\myse{p}}{\myse{P} \myappsp \mytmt \myappsp (\myrefl \myappsp \mytmt)} \hspace{1cm}
1774 \myjud{\myse{q}}{\mytmt \mypeq{\mytya} \mytmt}
1777 \UnaryInfC{$\myjud{\myfun{K} \myappsp \myse{P} \myappsp \myse{t} \myappsp \myse{p} \myappsp \myse{q}}{\myse{P} \myappsp \mytmt \myappsp \myse{q}}$}
1781 \cite{Hofmann1994} showed that $\myfun{K}$ is not derivable from
1782 $\myjeqq$, and \cite{McBride2004} showed that it is needed to implement
1783 `dependent pattern matching', as first proposed by \cite{Coquand1992}.\footnote{See Section \ref{sec:future-work} for more on dependent pattern matching.}
1784 Thus, $\myfun{K}$ is derivable in the systems that implement dependent
1785 pattern matching, such as Epigram and Agda; but for example not in Coq.
1787 $\myfun{K}$ is controversial mainly because it is at odds with
1788 equalities that include computational content, most notably Voevodsky's
1789 \emph{Univalent Foundations}, which feature a \emph{univalence} axiom
1790 that identifies isomorphisms between types with propositional equality.
1791 For example we would have two isomorphisms, and thus two equalities,
1792 between $\mybool$ and $\mybool$, corresponding to the two
1793 permutations---one is the identity, and one swaps the elements. Given
1794 this, $\myfun{K}$ and univalence are inconsistent, and thus a form of
1795 dependent pattern matching that does not imply $\myfun{K}$ is subject of
1796 research.\footnote{More information about univalence can be found at
1797 \url{http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations.html}.}
1799 \subsection{Limitations}
1801 Propositional equality as described is quite restricted when
1802 reasoning about equality beyond the term structure, which is what definitional
1803 equality gives us (extensions notwithstanding).
1805 \begin{mydef}[Extensional equality]
1806 Given two functions $\myse{f}$ and $\myse{g}$ of type $\mytya \myarr \mytyb$, they are are said to be \emph{extensionally equal} if
1807 \[ (\myb{x} {:} \mytya) \myarr \mypeq \myappsp \mytyb \myappsp (\myse{f} \myappsp \myb{x}) \myappsp (\myse{g} \myappsp \myb{x}) \]
1810 The problem is best exemplified by \emph{function extensionality}. In
1811 mathematics, we would expect to be able to treat functions that give
1812 equal output for equal input as equal. When reasoning in a mechanised
1813 framework we ought to be able to do the same: in the end, without
1814 considering the operational behaviour, all functions equal extensionally
1815 are going to be replaceable with one another.
1817 However in ITT this is not the case, or in other words with the tools we have there is no closed term of type
1819 \myfun{ext} : \myfora{\myb{A}\ \myb{B}}{\mytyp}{\myfora{\myb{f}\ \myb{g}}{
1820 \myb{A} \myarr \myb{B}}{
1821 (\myfora{\myb{x}}{\myb{A}}{\mypeq \myappsp \myb{B} \myappsp (\myapp{\myb{f}}{\myb{x}}) \myappsp (\myapp{\myb{g}}{\myb{x}})}) \myarr
1822 \mypeq \myappsp (\myb{A} \myarr \myb{B}) \myappsp \myb{f} \myappsp \myb{g}
1826 To see why this is the case, consider the functions
1827 \[\myabs{\myb{x}}{0 \mathrel{\myfun{$+$}} \myb{x}}$ and $\myabs{\myb{x}}{\myb{x} \mathrel{\myfun{$+$}} 0}\]
1828 where $\myfun{$+$}$ is defined by recursion on the first argument,
1829 gradually destructing it to build up successors of the second argument.
1830 The two functions are clearly extensionally equal, and we can in fact
1833 \myfora{\myb{x}}{\mynat}{\mypeq \myappsp \mynat \myappsp (0 \mathrel{\myfun{$+$}} \myb{x}) \myappsp (\myb{x} \mathrel{\myfun{$+$}} 0)}
1835 By induction on $\mynat$ applied to $\myb{x}$. However, the two
1836 functions are not definitionally equal, and thus we will not be able to get
1837 rid of the quantification.
1839 For the reasons given above, theories that offer a propositional equality
1840 similar to what we presented are called \emph{intensional}, as opposed
1841 to \emph{extensional}. Most systems widely used today (such as Agda,
1842 Coq, and Epigram) are of the former kind.
1844 This is quite an annoyance that often makes reasoning awkward or
1845 impossible to execute. For example, we might want to represent terms of
1846 some language in Agda and give their denotation by embedding them in
1847 Agda---if we had $\lambda$-terms, functions will be Agda functions,
1848 application will be Agda's function application, and so on. Then we
1849 would like to perform optimisation passes on the terms, and verify that
1850 they are sound by proving that the denotation of the optimised version
1851 is equal to the denotation of the starting term.
1853 But if the embedding uses functions---and it probably will---we are
1854 stuck with an equality that identifies as equal only syntactically equal
1855 functions! Since the point of optimising is about preserving the
1856 denotational but changing the operational behaviour of terms, our
1857 equality falls short of our needs. Moreover, the problem extends to
1858 other fields beyond functions, such as bisimulation between processes
1859 specified by coinduction, or in general proving equivalences based on
1860 the behaviour of a term.
1862 \subsection{Equality reflection}
1864 One way to `solve' this problem is by identifying propositional equality
1865 with definitional equality.
1867 \begin{mydef}[Equality reflection]\end{mydef}
1868 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1869 \AxiomC{$\myjud{\myse{q}}{\mypeq \myappsp \mytya \myappsp \mytmm \myappsp \mytmn}$}
1870 \UnaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\mytya}$}
1874 The \emph{equality reflection} rule is a very different rule from the
1875 ones we saw up to now: it links a typing judgement internal to the type
1876 theory to a meta-theoretic judgement that the type checker uses to work
1877 with terms. It is easy to see the dangerous consequences that this
1880 \item The rule is not syntax directed, and the type checker is
1881 presumably expected to come up with equality proofs when needed.
1882 \item More worryingly, type checking becomes undecidable also because
1883 computing under false assumptions becomes unsafe, since we derive any
1884 equality proof and then use equality reflection and the conversion
1885 rule to have terms of any type.
1888 Given these facts theories employing equality reflection, like NuPRL
1889 \citep{NuPRL}, carry the derivations that gave rise to each typing judgement
1890 to keep the systems manageable.
1892 For all its faults, equality reflection does allow us to prove extensionality,
1893 using the extensions given in Section \ref{sec:extensions}. Assuming that $\myctx$ contains
1894 \[\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}}}\]
1898 \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}})}$}
1899 \RightLabel{equality reflection}
1900 \UnaryInfC{$\myjudd{\myctx; \myb{x} : \myb{A}}{\myapp{\myb{f}}{\myb{x}} \mydefeq \myapp{\myb{g}}{\myb{x}}}{\myb{B}}$}
1901 \RightLabel{congruence for $\lambda$s}
1902 \UnaryInfC{$\myjud{(\myabs{\myb{x}}{\myapp{\myb{f}}{\myb{x}}}) \mydefeq (\myabs{\myb{x}}{\myapp{\myb{g}}{\myb{x}}})}{\myb{A} \myarr \myb{B}}$}
1903 \RightLabel{$\eta$-law for $\lambda$}
1904 \UnaryInfC{$\myjud{\myb{f} \mydefeq \myb{g}}{\myb{A} \myarr \myb{B}}$}
1905 \RightLabel{$\myrefl$}
1906 \UnaryInfC{$\myjud{\myapp{\myrefl}{\myb{f}}}{\mypeq \myappsp (\myb{A} \myarr \myb{B}) \myappsp \myb{f} \myappsp \myb{g}}$}
1908 For this reason, theories employing equality reflection are often
1909 grouped under the name of \emph{Extensional Type Theory} (ETT). Now,
1910 the question is: do we need to give up well-behavedness of our theory to
1911 gain extensionality?
1913 \section{The observational approach}
1916 A recent development by \citet{Altenkirch2007}, \emph{Observational Type
1917 Theory} (OTT), promises to keep the well behavedness of ITT while
1918 being able to gain many useful equality proofs,\footnote{It is suspected
1919 that OTT gains \emph{all} the equality proofs of ETT, but no proof
1920 exists yet.} including function extensionality. The main idea is have
1921 equalities to express structural properties of the equated terms,
1922 instead of blindly comparing the syntax structure. In the case of
1923 functions, this will correspond to extensionality, in the case of
1924 products it will correspond to having equal projections, and so on.
1925 Moreover, we are given a way to \emph{coerce} values from $\mytya$ to
1926 $\mytyb$, if we can prove $\mytya$ equal to $\mytyb$, following similar
1927 principles to the ones described above. Here we give an exposition
1928 which follows closely the original paper.
1930 \subsection{A simpler theory, a propositional fragment}
1932 \begin{mydef}[OTT's simple theory, with propositions]\ \end{mydef}
1935 $\mytyp_l$ is replaced by $\mytyp$. \\\ \\
1937 \begin{array}{r@{\ }c@{\ }l}
1938 \mytmsyn & ::= & \cdots \mysynsep \myprdec{\myprsyn} \mysynsep
1939 \myITE{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
1940 \myprsyn & ::= & \mybot \mysynsep \mytop \mysynsep \myprsyn \myand \myprsyn
1941 \mysynsep \myprfora{\myb{x}}{\mytmsyn}{\myprsyn}
1948 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
1950 \begin{array}{l@{}l@{\ }c@{\ }l}
1951 \myITE{\mytrue &}{\mytya}{\mytyb} & \myred & \mytya \\
1952 \myITE{\myfalse &}{\mytya}{\mytyb} & \myred & \mytyb
1959 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1961 \AxiomC{$\myjud{\myse{P}}{\myprop}$}
1962 \UnaryInfC{$\myjud{\myprdec{\myse{P}}}{\mytyp}$}
1965 \AxiomC{$\myjud{\mytmt}{\mybool}$}
1966 \AxiomC{$\myjud{\mytya}{\mytyp}$}
1967 \AxiomC{$\myjud{\mytyb}{\mytyp}$}
1968 \TrinaryInfC{$\myjud{\myITE{\mytmt}{\mytya}{\mytyb}}{\mytyp}$}
1975 \mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
1976 \begin{tabular}{ccc}
1977 \AxiomC{\phantom{$\myjud{\myse{P}}{\myprop}$}}
1978 \UnaryInfC{$\myjud{\mytop}{\myprop}$}
1980 \UnaryInfC{$\myjud{\mybot}{\myprop}$}
1983 \AxiomC{$\myjud{\myse{P}}{\myprop}$}
1984 \AxiomC{$\myjud{\myse{Q}}{\myprop}$}
1985 \BinaryInfC{$\myjud{\myse{P} \myand \myse{Q}}{\myprop}$}
1987 \UnaryInfC{\phantom{$\myjud{\mybot}{\myprop}$}}
1990 \AxiomC{$\myjud{\myse{A}}{\mytyp}$}
1991 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\myse{P}}{\myprop}$}
1992 \BinaryInfC{$\myjud{\myprfora{\myb{x}}{\mytya}{\myse{P}}}{\myprop}$}
1994 \UnaryInfC{\phantom{$\myjud{\mybot}{\myprop}$}}
1999 Our foundation will be a type theory like the one of Section
2000 \ref{sec:itt}, with only one level: $\mytyp_0$. In this context we will
2001 drop the $0$ and call $\mytyp_0$ $\mytyp$. Moreover, since the old
2002 $\myfun{if}\myarg\myfun{then}\myarg\myfun{else}$ was able to return
2003 types thanks to the hierarchy (which is gone), we need to reintroduce an
2004 ad-hoc conditional for types, where the reduction rule is the obvious
2007 However, we have an addition: a universe of \emph{propositions},
2008 $\myprop$.\footnote{Note that we do not need syntax for the type of props, $\myprop$, since the user cannot abstract over them. In fact, we do not not need syntax for $\mytyp$ either, for the same reason.} $\myprop$ isolates a fragment of types at large, and
2009 indeed we can `inject' any $\myprop$ back in $\mytyp$ with $\myprdec{\myarg}$.
2010 \begin{mydef}[Proposition decoding]\ \end{mydef}
2011 \mydesc{proposition decoding:}{\myprdec{\mytmsyn} \myred \mytmsyn}{
2014 \begin{array}{l@{\ }c@{\ }l}
2015 \myprdec{\mybot} & \myred & \myempty \\
2016 \myprdec{\mytop} & \myred & \myunit
2021 \begin{array}{r@{ }c@{ }l@{\ }c@{\ }l}
2022 \myprdec{&\myse{P} \myand \myse{Q} &} & \myred & \myprdec{\myse{P}} \myprod \myprdec{\myse{Q}} \\
2023 \myprdec{&\myprfora{\myb{x}}{\mytya}{\myse{P}} &} & \myred &
2024 \myfora{\myb{x}}{\mytya}{\myprdec{\myse{P}}}
2029 Propositions are what we call the types of \emph{proofs}, or types
2030 whose inhabitants contain no `data', much like $\myunit$. Types of
2031 these kind are called \emph{irrelevant}. Irrelevance can be exploited
2032 in various ways---we can identify all equivalent proportions as
2033 definitionally equal equal, as we will see later; and erase all the top
2034 level propositions when compiling.
2036 Why did we choose what we have in $\myprop$? Given the above
2037 criteria, $\mytop$ obviously fits the bill, since it has one element.
2038 A pair of propositions $\myse{P} \myand \myse{Q}$ still won't get us
2039 data, since if they both have one element the only possible pair is
2040 the one formed by said elements. Finally, if $\myse{P}$ is a
2041 proposition and we have $\myprfora{\myb{x}}{\mytya}{\myse{P}}$, the
2042 decoding will be a constant function for propositional content. The
2043 only threat is $\mybot$, by which we can fabricate anything we want:
2044 however if we are consistent there will be no closed term of type
2045 $\mybot$ at, which is enough regarding proof erasure and
2048 As an example of types that are \emph{not} propositional, consider
2049 $\mydc{Bool}$eans, which are the quintessential `relevant' data, since
2050 they are often used to decide the execution path of a program through
2051 $\myfun{if}\myarg\myfun{then}\myarg\myfun{else}\myarg$ constructs.
2053 \subsection{Equality proofs}
2055 \begin{mydef}[Equality proofs and related operations]\ \end{mydef}
2059 \begin{array}{r@{\ }c@{\ }l}
2060 \mytmsyn & ::= & \cdots \mysynsep
2061 \mycoee{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \mysynsep
2062 \mycohh{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
2063 \myprsyn & ::= & \cdots \mysynsep \mytmsyn \myeq \mytmsyn \mysynsep
2064 \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn}
2069 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
2071 \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
2072 \AxiomC{$\myjud{\mytmt}{\mytya}$}
2073 \BinaryInfC{$\myjud{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}$}
2076 \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
2077 \AxiomC{$\myjud{\mytmt}{\mytya}$}
2078 \BinaryInfC{$\myjud{\mycohh{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\myprdec{\myjm{\mytmt}{\mytya}{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}}}$}
2084 \mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
2089 \myjud{\myse{A}}{\mytyp} \hspace{1cm} \myjud{\myse{B}}{\mytyp}
2092 \UnaryInfC{$\myjud{\mytya \myeq \mytyb}{\myprop}$}
2097 \myjud{\myse{A}}{\mytyp} \hspace{1cm} \myjud{\mytmm}{\myse{A}} \\
2098 \myjud{\myse{B}}{\mytyp} \hspace{1cm} \myjud{\mytmn}{\myse{B}}
2101 \UnaryInfC{$\myjud{\myjm{\mytmm}{\myse{A}}{\mytmn}{\myse{B}}}{\myprop}$}
2108 While isolating a propositional universe as presented can be a useful
2109 exercises on its own, what we are really after is a useful notion of
2110 equality. In OTT we want to maintain that things judged to be equal are
2111 still always replaceable for one another with no additional
2112 changes. Note that this is not the same as saying that they are
2113 definitionally equal, since as we saw extensionally equal functions,
2114 while satisfying the above requirement, are not.
2116 Towards this goal we introduce two equality constructs in
2117 $\myprop$---the fact that they are in $\myprop$ indicates that they
2118 indeed have no computational content. The first construct, $\myarg
2119 \myeq \myarg$, relates types, the second,
2120 $\myjm{\myarg}{\myarg}{\myarg}{\myarg}$, relates values. The
2121 value-level equality is different from our old propositional equality:
2122 instead of ranging over only one type, we might form equalities between
2123 values of different types---the usefulness of this construct will be
2124 clear soon. In the literature this equality is known as `heterogeneous'
2125 or `John Major', since
2128 John Major's `classless society' widened people's aspirations to
2129 equality, but also the gap between rich and poor. After all, aspiring
2130 to be equal to others than oneself is the politics of envy. In much
2131 the same way, $\myjm{\myarg}{\myarg}{\myarg}{\myarg}$ forms equations
2132 between members of any type, but they cannot be treated as equals (ie
2133 substituted) unless they are of the same type. Just as before, each
2134 thing is only equal to itself. \citep{McBride1999}.
2137 Correspondingly, at the term level, $\myfun{coe}$ (`coerce') lets us
2138 transport values between equal types; and $\myfun{coh}$ (`coherence')
2139 guarantees that $\myfun{coe}$ respects the value-level equality, or in
2140 other words that it really has no computational component. If we
2141 transport $\mytmm : \mytya$ to $\mytmn : \mytyb$, $\mytmm$ and $\mytmn$
2142 will still be the same.
2144 Before introducing the core machinery of OTT work, let us distinguish
2145 between \emph{canonical} and \emph{neutral} terms and types.
2147 \begin{mydef}[Canonical and neutral terms and types]
2148 In a type theory, \emph{neutral} terms are those formed by an
2149 abstracted variable or by an eliminator (including function
2150 application). Everything else is \emph{canonical}.
2152 In the current system, data constructors ($\mytt$, $\mytrue$,
2153 $\myfalse$, $\myabss{\myb{x}}{\mytya}{\mytmt}$, ...) will be
2154 canonical, the rest neutral. Correspondingly, canonical types are
2155 those arising from the ground types ($\myempty$, $\myunit$, $\mybool$)
2156 and the three type formers ($\myarr$, $\myprod$, $\mytyc{W}$).
2157 Neutral types are those formed by
2158 $\myfun{If}\myarg\myfun{Then}\myarg\myfun{Else}\myarg$.
2160 \begin{mydef}[Canonicity]
2161 If in a system all canonical types are inhabited by canonical terms
2162 the system is said to have the \emph{canonicity} property.
2164 The current system, and well-behaved systems in general, has the
2165 canonicity property. Another consequence of normalisation is that all
2166 closed terms will reduce to a canonical term.
2168 \subsubsection{Type equality, and coercions}
2170 The plan is to decompose type-level equalities between canonical types
2171 into decodable propositions containing equalities regarding the
2172 subtypes. So if are equating two product types, the equality will
2173 reduce to two subequalities regarding the first and second type. Then,
2174 we can \myfun{coe}rce to transport values between equal types.
2175 Following the subequalities, \myfun{coe} will proceed recursively on the
2178 This interplay between the canonicity of equated types, type equalities,
2179 and \myfun{coe}, ensures that invocations of $\myfun{coe}$ will vanish
2180 when we have evidence of the structural equality of the types we are
2181 transporting terms across. If the type is neutral, the equality will
2182 not reduce and thus $\myfun{coe}$ will not reduce either. If we come
2183 across an equality between different canonical types, then we reduce the
2184 equality to bottom, thus making sure that no such proof can exist, and
2185 providing an `escape hatch' in $\myfun{coe}$.
2189 \mydesc{equality reduction:}{\myprsyn \myred \myprsyn}{
2191 \begin{array}{c@{\ }c@{\ }c@{\ }l}
2192 \myempty & \myeq & \myempty & \myred \mytop \\
2193 \myunit & \myeq & \myunit & \myred \mytop \\
2194 \mybool & \myeq & \mybool & \myred \mytop \\
2195 \myexi{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myexi{\myb{x_2}}{\mytya_2}{\mytya_2} & \myred \\
2197 \myind{2} \mytya_1 \myeq \mytya_2 \myand
2198 \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}]}
2200 \myfora{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myfora{\myb{x_2}}{\mytya_2}{\mytyb_2} & \myred \cdots \\
2201 \myw{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myw{\myb{x_2}}{\mytya_2}{\mytyb_2} & \myred \cdots \\
2202 \mytya & \myeq & \mytyb & \myred \mybot\ \text{if $\mytya$ and $\mytyb$ are canonical.}
2207 \mydesc{reduction}{\mytmsyn \myred \mytmsyn}{
2209 \begin{array}[t]{@{}l@{\ }l@{\ }l@{\ }l@{\ }l@{\ }c@{\ }l@{\ }}
2210 \mycoe & \myempty & \myempty & \myse{Q} & \myse{t} & \myred & \myse{t} \\
2211 \mycoe & \myunit & \myunit & \myse{Q} & \myse{t} & \myred & \mytt \\
2212 \mycoe & \mybool & \mybool & \myse{Q} & \mytrue & \myred & \mytrue \\
2213 \mycoe & \mybool & \mybool & \myse{Q} & \myfalse & \myred & \myfalse \\
2214 \mycoe & (\myexi{\myb{x_1}}{\mytya_1}{\mytyb_1}) &
2215 (\myexi{\myb{x_2}}{\mytya_2}{\mytyb_2}) & \myse{Q} &
2216 \mytmt_1 & \myred & \\
2218 \myind{2}\begin{array}[t]{l@{\ }l@{\ }c@{\ }l}
2219 \mysyn{let} & \myb{\mytmm_1} & \mapsto & \myapp{\myfst}{\mytmt_1} : \mytya_1 \\
2220 & \myb{\mytmn_1} & \mapsto & \myapp{\mysnd}{\mytmt_1} : \mysub{\mytyb_1}{\myb{x_1}}{\myb{\mytmm_1}} \\
2221 & \myb{Q_A} & \mapsto & \myapp{\myfst}{\myse{Q}} : \mytya_1 \myeq \mytya_2 \\
2222 & \myb{\mytmm_2} & \mapsto & \mycoee{\mytya_1}{\mytya_2}{\myb{Q_A}}{\myb{\mytmm_1}} : \mytya_2 \\
2223 & \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}}} \\
2224 & \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}} \\
2225 \mysyn{in} & \multicolumn{3}{@{}l}{\mypair{\myb{\mytmm_2}}{\myb{\mytmn_2}}}
2228 \mycoe & (\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}) &
2229 (\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}) & \myse{Q} &
2233 \mycoe & (\myw{\myb{x_1}}{\mytya_1}{\mytyb_1}) &
2234 (\myw{\myb{x_2}}{\mytya_2}{\mytyb_2}) & \myse{Q} &
2238 \mycoe & \mytya & \mytyb & \myse{Q} & \mytmt & \myred & \myapp{\myabsurd{\mytyb}}{\myse{Q}}\ \text{if $\mytya$ and $\mytyb$ are canonical.}
2242 \caption{Reducing type equalities, and using them when
2243 $\myfun{coe}$rcing.}
2247 \begin{mydef}[Type equalities reduction, and \myfun{coe}rcions] Figure
2248 \ref{fig:eqred} illustrates the rules to reduce equalities and to
2249 coerce terms. We use a $\mysyn{let}$ syntax for legibility.
2251 For ground types, the proof is the trivial element, and \myfun{coe} is
2252 the identity. For $\myunit$, we can do better: we return its only
2253 member without matching on the term. For the three type binders the
2254 choices we make in the type equality are dictated by the desire of
2255 writing the $\myfun{coe}$ in a natural way.
2257 $\myprod$ is the easiest case: we decompose the proof into proofs that
2258 the first element's types are equal ($\mytya_1 \myeq \mytya_2$), and a
2259 proof that given equal values in the first element, the types of the
2260 second elements are equal too
2261 ($\myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{\myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2}}
2262 \myimpl \mytyb_1[\myb{x_1}] \myeq \mytyb_2[\myb{x_2}]}$).\footnote{We
2263 are using $\myimpl$ to indicate a $\forall$ where we discard the
2264 quantified value. We write $\mytyb_1[\myb{x_1}]$ to indicate that the
2265 $\myb{x_1}$ in $\mytyb_1$ is re-bound to the $\myb{x_1}$ quantified by
2266 the $\forall$, and similarly for $\myb{x_2}$ and $\mytyb_2$.} This
2267 also explains the need for heterogeneous equality, since in the second
2268 proof we need to equate terms of possibly different types. In the
2269 respective $\myfun{coe}$ case, since the types are canonical, we know at
2270 this point that the proof of equality is a pair of the shape described
2271 above. Thus, we can immediately coerce the first element of the pair
2272 using the first element of the proof, and then instantiate the second
2273 element of the proof with the two first elements and a proof by
2274 coherence of their equality, since we know that the types are equal.
2276 The cases for the other binders are omitted for brevity, but they follow
2277 the same principle with some twists to make $\myfun{coe}$ work with the
2278 generated proofs; the reader can refer to the paper for details.
2280 \subsubsection{$\myfun{coe}$, laziness, and $\myfun{coh}$erence}
2283 It is important to notice that the reduction rules for $\myfun{coe}$
2284 are never obstructed by the structure of the proofs. With the exception
2285 of comparisons between different canonical types we never `pattern
2286 match' on the proof pairs, but always look at the projections. This
2287 means that, as long as we are consistent, and thus as long as we don't
2288 have $\mybot$-inducing proofs, we can add propositional axioms for
2289 equality and $\myfun{coe}$ will still compute. Thus, we can take
2290 $\myfun{coh}$ as axiomatic, and we can add back familiar useful equality
2293 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
2294 \AxiomC{$\myjud{\mytmt}{\mytya}$}
2295 \UnaryInfC{$\myjud{\myapp{\myrefl}{\mytmt}}{\myprdec{\myjm{\mytmt}{\mytya}{\mytmt}{\mytya}}}$}
2300 \AxiomC{$\myjud{\mytya}{\mytyp}$}
2301 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytyb}{\mytyp}$}
2302 \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}}}}}$}
2306 $\myrefl$ is the equivalent of the reflexivity rule in propositional
2307 equality, and $\mytyc{R}$ asserts that if we have a we have a $\mytyp$
2308 abstracting over a value we can substitute equal for equal---this lets
2309 us recover $\myfun{subst}$. Note that while we need to provide ad-hoc
2310 rules in the restricted, non-hierarchical theory that we have, if our
2311 theory supports abstraction over $\mytyp$s we can easily add these
2312 axioms as top-level abstracted variables.
2314 \subsubsection{Value-level equality}
2316 \begin{mydef}[Value-level equality]\ \end{mydef}
2318 \mydesc{equality reduction:}{\myprsyn \myred \myprsyn}{
2320 \begin{array}{r@{ }c@{\ }c@{\ }c@{}l@{\ }c@{\ }r@{}c@{\ }c@{\ }c@{}l@{\ }l}
2321 (&\mytmt_1 & : & \myempty&) & \myeq & (&\mytmt_2 & : & \myempty &) & \myred \mytop \\
2322 (&\mytmt_1 & : & \myunit&) & \myeq & (&\mytmt_2 & : & \myunit&) & \myred \mytop \\
2323 (&\mytrue & : & \mybool&) & \myeq & (&\mytrue & : & \mybool&) & \myred \mytop \\
2324 (&\myfalse & : & \mybool&) & \myeq & (&\myfalse & : & \mybool&) & \myred \mytop \\
2325 (&\mytrue & : & \mybool&) & \myeq & (&\myfalse & : & \mybool&) & \myred \mybot \\
2326 (&\myfalse & : & \mybool&) & \myeq & (&\mytrue & : & \mybool&) & \myred \mybot \\
2327 (&\mytmt_1 & : & \myexi{\mytya_1}{\myb{x_1}}{\mytyb_1}&) & \myeq & (&\mytmt_2 & : & \myexi{\mytya_2}{\myb{x_2}}{\mytyb_2}&) & \myred \\
2328 & \multicolumn{11}{@{}l}{
2329 \myind{2} \myjm{\myapp{\myfst}{\mytmt_1}}{\mytya_1}{\myapp{\myfst}{\mytmt_2}}{\mytya_2} \myand
2330 \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}}}
2332 (&\myse{f}_1 & : & \myfora{\mytya_1}{\myb{x_1}}{\mytyb_1}&) & \myeq & (&\myse{f}_2 & : & \myfora{\mytya_2}{\myb{x_2}}{\mytyb_2}&) & \myred \\
2333 & \multicolumn{11}{@{}l}{
2334 \myind{2} \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{
2335 \myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2} \myimpl
2336 \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}]}
2339 (&\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 \\
2340 (&\mytmt_1 & : & \mytya_1&) & \myeq & (&\mytmt_2 & : & \mytya_2 &) & \myred \mybot\ \text{if $\mytya_1$ and $\mytya_2$ are canonical.}
2345 As with type-level equality, we want value-level equality to reduce
2346 based on the structure of the compared terms. When matching
2347 propositional data, such as $\myempty$ and $\myunit$, we automatically
2348 return the trivial type, since if a type has zero or one members, all
2349 members will be equal. When matching on data-bearing types, such as
2350 $\mybool$, we check that such data matches, and return bottom otherwise.
2351 When matching on records and functions, we rebuild the records to
2352 achieve $\eta$-expansion, and relate functions if they are extensionally
2353 equal---exactly what we wanted. The case for \mytyc{W} is omitted but
2354 unsurprising, checking that equal data in the nodes will bring equal
2357 \subsection{Proof irrelevance and stuck coercions}
2358 \label{sec:ott-quot}
2360 The last effort is required to make sure that proofs (members of
2361 $\myprop$) are \emph{irrelevant}. Since they are devoid of
2362 computational content, we would like to identify all equivalent
2363 propositions as the same, in a similar way as we identified all
2364 $\myempty$ and all $\myunit$ as the same in section
2365 \ref{sec:eta-expand}.
2367 Thus we will have a quotation that will not only perform
2368 $\eta$-expansion, but will also identify and mark proofs that could not
2369 be decoded (that is, equalities on neutral types). Then, when
2370 comparing terms, marked proofs will be considered equal without
2371 analysing their contents, thus gaining irrelevance.
2373 Moreover we can safely advance `stuck' $\myfun{coe}$rcions between
2374 non-canonical but definitionally equal types. Consider for example
2376 \mycoee{(\myITE{\myb{b}}{\mynat}{\mybool})}{(\myITE{\myb{b}}{\mynat}{\mybool})}{\myb{x}}
2378 Where $\myb{b}$ and $\myb{x}$ are abstracted variables. This
2379 $\myfun{coe}$ will not advance, since the types are not canonical.
2380 However they are definitionally equal, and thus we can safely remove the
2381 coerce and return $\myb{x}$ as it is.
2383 \section{\mykant: the theory}
2384 \label{sec:kant-theory}
2386 \epigraph{\emph{The construction itself is an art, its application to the world an evil parasite.}}{Luitzen Egbertus Jan `Bertus' Brouwer}
2388 \mykant\ is an interactive theorem prover developed as part of this thesis.
2389 The plan is to present a core language which would be capable of serving as
2390 the basis for a more featureful system, while still presenting interesting
2391 features and more importantly observational equality.
2393 We will first present the features of the system, along with motivations
2394 and trade-offs for the design decisions made. Then we describe the
2395 implementation we have developed in Section \ref{sec:kant-practice}.
2396 For an overview of the features of \mykant, see
2397 Section \ref{sec:contributions}, here we present them one by one. The
2398 exception is type holes, which we do not describe holes rigorously, but
2399 provide more information about them in Section \ref{sec:type-holes}.
2401 Note that in this section we will present \mykant\ terms in a fancy
2402 \LaTeX\ dress to keep up with the presentation, but every term, reduced
2403 to its concrete syntax (which we will present in Section
2404 \ref{sec:syntax}), is a valid \mykant\ term accepted by \mykant\ the
2405 software, and not only \mykant\ the theory. Appendix
2406 \ref{app:kant-examples} displays most of the terms in this section in
2407 their concrete syntax.
2409 \subsection{Bidirectional type checking}
2411 We start by describing bidirectional type checking since it calls for
2412 fairly different typing rules that what we have seen up to now. The
2413 idea is to have two kinds of terms: terms for which a type can always be
2414 inferred, and terms that need to be checked against a type. A nice
2415 observation is that this duality is in correspondence with the notion of
2416 canonical and neutral terms: neutral terms
2417 (abstracted or defined variables, function application, record
2418 projections, primitive recursors, etc.) \emph{infer} types, canonical
2419 terms (abstractions, record/data types data constructors, etc.) need to
2422 To introduce the concept and notation, we will revisit the STLC in a
2423 bidirectional style. The presentation follows \cite{Loh2010}. The
2424 syntax for our bidirectional STLC is the same as the untyped
2425 $\lambda$-calculus, but with an extra construct to annotate terms
2426 explicitly---this will be necessary when dealing with top-level
2427 canonical terms. The types are the same as those found in the normal
2430 \begin{mydef}[Syntax for the annotated $\lambda$-calculus]\ \end{mydef}
2434 \begin{array}{r@{\ }c@{\ }l}
2435 \mytmsyn & ::= & \myb{x} \mysynsep \myabs{\myb{x}}{\mytmsyn} \mysynsep (\myapp{\mytmsyn}{\mytmsyn}) \mysynsep (\mytmsyn : \mytysyn)
2440 We will have two kinds of typing judgements: \emph{inference} and
2441 \emph{checking}. $\myinf{\mytmt}{\mytya}$ indicates that $\mytmt$
2442 infers the type $\mytya$, while $\mychk{\mytmt}{\mytya}$ can be checked
2443 against type $\mytya$. The arrows indicate the direction of the type
2444 checking---inference pushes types up, checking propagates types
2447 The type of variables in context is inferred. The type of applications
2448 and annotated terms is inferred too, propagating types down the applied
2449 and annotated term, respectively. Abstractions are checked. Finally,
2450 we have a rule to check the type of an inferrable term.
2452 \begin{mydef}[Bidirectional type checking for the STLC]\ \end{mydef}
2454 \mydesc{typing:}{\myctx \vdash \mytmsyn \Updownarrow \mytmsyn}{
2456 \AxiomC{$\myctx(x) = A$}
2457 \UnaryInfC{$\myinf{\myb{x}}{A}$}
2460 \AxiomC{$\myjudd{\myctx;\myb{x} : A}{\mytmt}{\mytyb}$}
2461 \UnaryInfC{$\mychk{\myabs{x}{\mytmt}}{(\myb{x} {:} \mytya) \myarr \mytyb}$}
2467 \begin{tabular}{ccc}
2468 \AxiomC{$\myinf{\mytmm}{\mytya \myarr \mytyb}$}
2469 \AxiomC{$\mychk{\mytmn}{\mytya}$}
2470 \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mytyb}$}
2473 \AxiomC{$\mychk{\mytmt}{\mytya}$}
2474 \UnaryInfC{$\myinf{\myann{\mytmt}{\mytya}}{\mytya}$}
2477 \AxiomC{$\myinf{\mytmt}{\mytya}$}
2478 \UnaryInfC{$\mychk{\mytmt}{\mytya}$}
2483 For example, if we wanted to type function composition (in this case for
2484 naturals), we would have to annotate the term:
2487 \myfun{comp} : (\mynat \myarr \mynat) \myarr (\mynat \myarr \mynat) \myarr \mynat \myarr \mynat \\
2488 \myfun{comp} \myappsp \myb{f} \myappsp \myb{g} \myappsp \myb{x} \mapsto \myb{f}\myappsp(\myb{g}\myappsp\myb{x})
2491 But we would not have to annotate functions passed to it, since the type would be propagated to the arguments:
2493 \myfun{comp}\myappsp (\myabs{\myb{x}}{\myb{x} \mathrel{\myfun{$+$}} 3}) \myappsp (\myabs{\myb{x}}{\myb{x} \mathrel{\myfun{$*$}} 4}) \myappsp 42
2496 \subsection{Base terms and types}
2498 Let us begin by describing the primitives available without the user
2499 defining any data types, and without equality. The way we handle
2500 variables and substitution is left unspecified, and explained in section
2501 \ref{sec:term-repr}, along with other implementation issues. We are
2502 also going to give an account of the implicit type hierarchy separately
2503 in Section \ref{sec:term-hierarchy}, so as not to clutter derivation
2504 rules too much, and just treat types as impredicative for the time
2507 \begin{mydef}[Syntax for base types in \mykant]\ \end{mydef}
2511 \begin{array}{r@{\ }c@{\ }l}
2512 \mytmsyn & ::= & \mynamesyn \mysynsep \mytyp \\
2513 & | & \myfora{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
2514 \myabs{\myb{x}}{\mytmsyn} \mysynsep
2515 (\myapp{\mytmsyn}{\mytmsyn}) \mysynsep
2516 (\myann{\mytmsyn}{\mytmsyn}) \\
2517 \mynamesyn & ::= & \myb{x} \mysynsep \myfun{f}
2522 The syntax for our calculus includes just two basic constructs:
2523 abstractions and $\mytyp$s. Everything else will be user-defined.
2524 Since we let the user define values too, we will need a context capable
2525 of carrying the body of variables along with their type.
2527 \begin{mydef}[Context validity]
2528 Bound names and defined names are treated separately in the syntax, and
2529 while both can be associated to a type in the context, only defined
2530 names can be associated with a body.
2533 \mydesc{context validity:}{\myvalid{\myctx}}{
2534 \begin{tabular}{ccc}
2535 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
2536 \UnaryInfC{$\myvalid{\myemptyctx}$}
2539 \AxiomC{$\mychk{\mytya}{\mytyp}$}
2540 \AxiomC{$\mynamesyn \not\in \myctx$}
2541 \BinaryInfC{$\myvalid{\myctx ; \mynamesyn : \mytya}$}
2544 \AxiomC{$\mychk{\mytmt}{\mytya}$}
2545 \AxiomC{$\myfun{f} \not\in \myctx$}
2546 \BinaryInfC{$\myvalid{\myctx ; \myfun{f} \mapsto \mytmt : \mytya}$}
2551 Now we can present the reduction rules, which are unsurprising. We have
2552 the usual function application ($\beta$-reduction), but also a rule to
2553 replace names with their bodies ($\delta$-reduction), and one to discard
2554 type annotations. For this reason reduction is done in-context, as
2555 opposed to what we have seen in the past.
2557 \begin{mydef}[Reduction rules for base types in \mykant]\ \end{mydef}
2559 \mydesc{reduction:}{\myctx \vdash \mytmsyn \myred \mytmsyn}{
2560 \begin{tabular}{ccc}
2561 \AxiomC{\phantom{$\myb{x} \mapsto \mytmt : \mytya \in \myctx$}}
2562 \UnaryInfC{$\myctx \vdash \myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn}
2563 \myred \mysub{\mytmm}{\myb{x}}{\mytmn}$}
2566 \AxiomC{$\myfun{f} \mapsto \mytmt : \mytya \in \myctx$}
2567 \UnaryInfC{$\myctx \vdash \myfun{f} \myred \mytmt$}
2570 \AxiomC{\phantom{$\myb{x} \mapsto \mytmt : \mytya \in \myctx$}}
2571 \UnaryInfC{$\myctx \vdash \myann{\mytmm}{\mytya} \myred \mytmm$}
2576 We can now give types to our terms. Although we include the usual
2577 conversion rule, we defer a detailed account of definitional equality to
2578 Section \ref{sec:kant-irr}.
2580 \begin{mydef}[Bidirectional type checking for base types in \mykant]\ \end{mydef}
2582 \mydesc{typing:}{\myctx \vdash \mytmsyn \Updownarrow \mytmsyn}{
2583 \begin{tabular}{cccc}
2584 \AxiomC{$\myse{name} : A \in \myctx$}
2585 \UnaryInfC{$\myinf{\myse{name}}{A}$}
2588 \AxiomC{$\myfun{f} \mapsto \mytmt : A \in \myctx$}
2589 \UnaryInfC{$\myinf{\myfun{f}}{A}$}
2592 \AxiomC{$\mychk{\mytmt}{\mytya}$}
2593 \UnaryInfC{$\myinf{\myann{\mytmt}{\mytya}}{\mytya}$}
2596 \AxiomC{$\myinf{\mytmt}{\mytya}$}
2597 \AxiomC{$\myctx \vdash \mytya \mydefeq \mytyb$}
2598 \BinaryInfC{$\mychk{\mytmt}{\mytyb}$}
2606 \AxiomC{\phantom{$\mychkk{\myctx; \myb{x}: \mytya}{\mytmt}{\mytyb}$}}
2607 \UnaryInfC{$\myinf{\mytyp}{\mytyp}$}
2610 \AxiomC{$\mychk{\mytya}{\mytyp}$}
2611 \AxiomC{$\mychkk{\myctx; \myb{x} : \mytya}{\mytyb}{\mytyp}$}
2612 \BinaryInfC{$\myinf{(\myb{x} {:} \mytya) \myarr \mytyb}{\mytyp}$}
2621 \AxiomC{$\myinf{\mytmm}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
2622 \AxiomC{$\mychk{\mytmn}{\mytya}$}
2623 \BinaryInfC{$\myinf{\myapp{\mytmm}{\mytmn}}{\mysub{\mytyb}{\myb{x}}{\mytmn}}$}
2628 \AxiomC{$\mychkk{\myctx; \myb{x}: \mytya}{\mytmt}{\mytyb}$}
2629 \UnaryInfC{$\mychk{\myabs{\myb{x}}{\mytmt}}{\myfora{\myb{x}}{\mytyb}{\mytyb}}$}
2635 \subsection{Elaboration}
2637 As we mentioned, $\mykant$\ allows the user to define not only values
2638 but also custom data types and records. \emph{Elaboration} consists of
2639 turning these declarations into workable syntax, types, and reduction
2640 rules. The treatment of custom types in $\mykant$\ is heavily inspired
2641 by McBride's and McKinna's early work on Epigram \citep{McBride2004},
2642 although with some differences.
2644 \subsubsection{Term vectors, telescopes, and assorted notation}
2646 \begin{mydef}[Term vector]
2647 A \emph{term vector} is a series of terms. The empty vector is
2648 represented by $\myemptyctx$, and a new element is added with
2649 $\myarg;\myarg$, similarly to contexts---$\vec{t};\mytmm$.
2652 We denote term vectors with the usual arrow notation,
2653 e.g. $\vec{\mytmt}$, $\vec{\mytmt};\mytmm$, etc. We often use term
2654 vectors to refer to a series of term applied to another. For example
2655 $\mytyc{D} \myappsp \vec{A}$ is a shorthand for $\mytyc{D} \myappsp
2656 \mytya_1 \cdots \mytya_n$, for some $n$. $n$ is consistently used to
2657 refer to the length of such vectors, and $i$ to refer to an index such
2658 that $1 \le i \le n$.
2660 \begin{mydef}[Telescope]
2661 A \emph{telescope} is a series of typed bindings. The empty telescope
2662 is represented by $\myemptyctx$, and a binding is added via
2666 To present the elaboration and operations on user defined data types, we
2667 frequently make use what \cite{Bruijn91} called \emph{telescopes}, a
2668 construct that will prove useful when dealing with the types of type and
2669 data constructors. We refer to telescopes with $\mytele$, $\mytele'$,
2670 $\mytele_i$, etc. If $\mytele$ refers to a telescope, $\mytelee$ refers
2671 to the term vector made up of all the variables bound by $\mytele$.
2672 $\mytele \myarr \mytya$ refers to the type made by turning the telescope
2673 into a series of $\myarr$. For example we have that
2675 (\myb{x} {:} \mynat); (\myb{p} : \myapp{\myfun{even}}{\myb{x}}) \myarr \mynat =
2676 (\myb{x} {:} \mynat) \myarr (\myb{p} : \myapp{\myfun{even}}{\myb{x}}) \myarr \mynat
2679 We make use of various operations to manipulate telescopes:
2681 \item $\myhead(\mytele)$ refers to the first type appearing in
2682 $\mytele$: $\myhead((\myb{x} {:} \mynat); (\myb{p} :
2683 \myapp{\myfun{even}}{\myb{x}})) = \mynat$. Similarly,
2684 $\myix_i(\mytele)$ refers to the $i^{th}$ type in a telescope
2686 \item $\mytake_i(\mytele)$ refers to the telescope created by taking the
2687 first $i$ elements of $\mytele$: $\mytake_1((\myb{x} {:} \mynat); (\myb{p} :
2688 \myapp{\myfun{even}}{\myb{x}})) = (\myb{x} {:} \mynat)$.
2689 \item $\mytele \vec{A}$ refers to the telescope made by `applying' the
2690 terms in $\vec{A}$ on $\mytele$: $((\myb{x} {:} \mynat); (\myb{p} :
2691 \myapp{\myfun{even}}{\myb{x}}))42 = (\myb{p} :
2692 \myapp{\myfun{even}}{42})$.
2695 Additionally, when presenting syntax elaboration, We use $\mytmsyn^n$ to
2696 indicate a term vector composed of $n$ elements. When clear from the
2697 context, we use term vectors to signify their length,
2698 e.g. $\mytmsyn^{\mytele}$, or $1 \le i \le \mytele$.
2700 \subsubsection{Declarations syntax}
2702 \begin{mydef}[Syntax of declarations in \mykant]\ \end{mydef}
2706 \begin{array}{r@{\ }c@{\ }l}
2707 \mydeclsyn & ::= & \myval{\myb{x}}{\mytmsyn}{\mytmsyn} \\
2708 & | & \mypost{\myb{x}}{\mytmsyn} \\
2709 & | & \myadt{\mytyc{D}}{\myappsp \mytelesyn}{}{\mydc{c} : \mytelesyn\ |\ \cdots } \\
2710 & | & \myreco{\mytyc{D}}{\myappsp \mytelesyn}{}{\myfun{f} : \mytmsyn,\ \cdots } \\
2712 \mytelesyn & ::= & \myemptytele \mysynsep \mytelesyn \mycc (\myb{x} {:} \mytmsyn) \\
2713 \mynamesyn & ::= & \cdots \mysynsep \mytyc{D} \mysynsep \mytyc{D}.\mydc{c} \mysynsep \mytyc{D}.\myfun{f}
2717 In \mykant\ we have four kind of declarations:
2720 \item[Defined value] A variable, together with a type and a body.
2721 \item[Abstract variable] An abstract variable, with a type but no body.
2722 \item[Inductive data] A \emph{data type}, with a \emph{type constructor}
2723 (denoted in blue, capitalised, sans serif: $\mytyc{D}$) various
2724 \emph{data constructors} (denoted in red, lowercase, sans serif:
2725 $\mydc{c}$), quite similar to what we find in Haskell. A primitive
2726 \emph{eliminator} (or \emph{destructor}, or \emph{recursor}; denoted
2727 by green, lowercase, roman: \myfun{elim}) will be used to compute with
2729 \item[Record] A \emph{record}, which like data types consists of a type
2730 constructor but only one data constructor. The user can also define
2731 various \emph{fields}, with no recursive occurrences of the type. The
2732 functions extracting the fields' values from an instance of a record
2733 are called \emph{projections} (denoted in the same way as destructors).
2736 Elaborating defined variables consists of type checking the body against
2737 the given type, and updating the context to contain the new binding.
2738 Elaborating abstract variables and abstract variables consists of type
2739 checking the type, and updating the context with a new typed variable.
2741 \begin{mydef}[Elaboration of defined and abstract variables]\ \end{mydef}
2743 \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
2745 \AxiomC{$\mychk{\mytmt}{\mytya}$}
2746 \AxiomC{$\myfun{f} \not\in \myctx$}
2748 $\myctx \myelabt \myval{\myfun{f}}{\mytya}{\mytmt} \ \ \myelabf\ \ \myctx; \myfun{f} \mapsto \mytmt : \mytya$
2752 \AxiomC{$\mychk{\mytya}{\mytyp}$}
2753 \AxiomC{$\myfun{f} \not\in \myctx$}
2756 \myctx \myelabt \mypost{\myfun{f}}{\mytya}
2757 \ \ \myelabf\ \ \myctx; \myfun{f} : \mytya
2764 \subsubsection{User defined types}
2765 \label{sec:user-type}
2767 Elaborating user defined types is the real effort. First, we will
2768 explain what we can define, with some examples.
2771 \item[Natural numbers] To define natural numbers, we create a data type
2772 with two constructors: one with zero arguments ($\mydc{zero}$) and one
2773 with one recursive argument ($\mydc{suc}$):
2776 \myadt{\mynat}{ }{ }{
2777 \mydc{zero} \mydcsep \mydc{suc} \myappsp \mynat
2781 This is very similar to what we would write in Haskell:
2783 data Nat = Zero | Suc Nat
2785 Once the data type is defined, $\mykant$\ will generate syntactic
2786 constructs for the type and data constructors, so that we will have
2789 \begin{tabular}{ccc}
2790 \AxiomC{\phantom{$\mychk{\mytmt}{\mynat}$}}
2791 \UnaryInfC{$\myinf{\mynat}{\mytyp}$}
2794 \AxiomC{\phantom{$\mychk{\mytmt}{\mynat}$}}
2795 \UnaryInfC{$\myinf{\mytyc{\mynat}.\mydc{zero}}{\mynat}$}
2798 \AxiomC{$\mychk{\mytmt}{\mynat}$}
2799 \UnaryInfC{$\myinf{\mytyc{\mynat}.\mydc{suc} \myappsp \mytmt}{\mynat}$}
2803 While in Haskell (or indeed in Agda or Coq) data constructors are
2804 treated the same way as functions, in $\mykant$\ they are syntax, so
2805 for example using $\mytyc{\mynat}.\mydc{suc}$ on its own will give a
2806 syntax error. This is necessary so that we can easily infer the type
2807 of polymorphic data constructors, as we will see later.
2809 Moreover, each data constructor is prefixed by the type constructor
2810 name, since we need to retrieve the type constructor of a data
2811 constructor when type checking. This measure aids in the presentation
2812 of the theory but it is not needed in the implementation, where
2813 we can have a dictionary to look up the type constructor corresponding
2814 to each data constructor. When using data constructors in examples I
2815 will omit the type constructor prefix for brevity, in this case
2816 writing $\mydc{zero}$ instead of $\mynat.\mydc{zero}$ and $\mydc{suc}$ instead of
2817 $\mynat.\mydc{suc}$.
2819 Along with user defined constructors, $\mykant$\ automatically
2820 generates an \emph{eliminator}, or \emph{destructor}, to compute with
2821 natural numbers: If we have $\mytmt : \mynat$, we can destruct
2822 $\mytmt$ using the generated eliminator `$\mynat.\myfun{elim}$':
2825 \AxiomC{$\mychk{\mytmt}{\mynat}$}
2827 \myinf{\mytyc{\mynat}.\myfun{elim} \myappsp \mytmt}{
2829 \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}}
2833 $\mynat.\myfun{elim}$ corresponds to the induction principle for
2834 natural numbers: if we have a predicate on numbers ($\myb{P}$), and we
2835 know that predicate holds for the base case
2836 ($\myapp{\myb{P}}{\mydc{zero}}$) and for each inductive step
2837 ($\myfora{\myb{x}}{\mynat}{\myapp{\myb{P}}{\myb{x}} \myarr
2838 \myapp{\myb{P}}{(\myapp{\mydc{suc}}{\myb{x}})}}$), then $\myb{P}$
2839 holds for any number. As with the data constructors, we require the
2840 eliminator to be applied to the `destructed' element.
2842 While the induction principle is usually seen as a mean to prove
2843 properties about numbers, in the intuitionistic setting it is also a
2844 mean to compute. In this specific case $\mynat.\myfun{elim}$
2845 returns the base case if the provided number is $\mydc{zero}$, and
2846 recursively applies the inductive step if the number is a
2849 \begin{array}{@{}l@{}l}
2850 \mytyc{\mynat}.\myfun{elim} \myappsp \mydc{zero} & \myappsp \myse{P} \myappsp \myse{pz} \myappsp \myse{ps} \myred \myse{pz} \\
2851 \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})
2854 The Haskell equivalent would be
2856 elim :: Nat -> a -> (Nat -> a -> a) -> a
2857 elim Zero pz ps = pz
2858 elim (Suc n) pz ps = ps n (elim n pz ps)
2860 Which buys us the computational behaviour, but not the reasoning power,
2861 since we cannot express the notion of a predicate depending on
2862 $\mynat$---the type system is far too weak.
2864 \item[Binary trees] Now for a polymorphic data type: binary trees, since
2865 lists are too similar to natural numbers to be interesting.
2868 \myadt{\mytree}{\myappsp (\myb{A} {:} \mytyp)}{ }{
2869 \mydc{leaf} \mydcsep \mydc{node} \myappsp (\myapp{\mytree}{\myb{A}}) \myappsp \myb{A} \myappsp (\myapp{\mytree}{\myb{A}})
2873 Now the purpose of `constructors as syntax' can be explained: what would
2874 the type of $\mydc{leaf}$ be? If we were to treat it as a `normal'
2875 term, we would have to specify the type parameter of the tree each
2876 time the constructor is applied:
2878 \begin{array}{@{}l@{\ }l}
2879 \mydc{leaf} & : \myfora{\myb{A}}{\mytyp}{\myapp{\mytree}{\myb{A}}} \\
2880 \mydc{node} & : \myfora{\myb{A}}{\mytyp}{\myapp{\mytree}{\myb{A}} \myarr \myb{A} \myarr \myapp{\mytree}{\myb{A}} \myarr \myapp{\mytree}{\myb{A}}}
2883 The problem with this approach is that creating terms is incredibly
2884 verbose and dull, since we would need to specify the type parameter of
2885 $\mytyc{Tree}$ each time. For example if we wished to create a
2886 $\mytree \myappsp \mynat$ with two nodes and three leaves, we would
2889 \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)
2891 The redundancy of $\mynat$s is quite irritating. Instead, if we treat
2892 constructors as syntactic elements, we can `extract' the type of the
2893 parameter from the type that the term gets checked against, much like
2894 what we do to type abstractions:
2898 \AxiomC{$\mychk{\mytya}{\mytyp}$}
2899 \UnaryInfC{$\mychk{\mydc{leaf}}{\myapp{\mytree}{\mytya}}$}
2902 \AxiomC{$\mychk{\mytmm}{\mytree \myappsp \mytya}$}
2903 \AxiomC{$\mychk{\mytmt}{\mytya}$}
2904 \AxiomC{$\mychk{\mytmm}{\mytree \myappsp \mytya}$}
2905 \TrinaryInfC{$\mychk{\mydc{node} \myappsp \mytmm \myappsp \mytmt \myappsp \mytmn}{\mytree \myappsp \mytya}$}
2909 Which enables us to write, much more concisely
2911 \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}
2913 We gain an annotation, but we lose the myriad of types applied to the
2914 constructors. Conversely, with the eliminator for $\mytree$, we can
2915 infer the type of the arguments given the type of the destructed:
2918 \AxiomC{$\myinf{\mytmt}{\myapp{\mytree}{\mytya}}$}
2920 \myinf{\mytree.\myfun{elim} \myappsp \mytmt}{
2922 (\myb{P} {:} \myapp{\mytree}{\mytya} \myarr \mytyp) \myarr \\
2923 \myapp{\myb{P}}{\mydc{leaf}} \myarr \\
2924 ((\myb{l} {:} \myapp{\mytree}{\mytya}) (\myb{x} {:} \mytya) (\myb{r} {:} \myapp{\mytree}{\mytya}) \myarr \myapp{\myb{P}}{\myb{l}} \myarr
2925 \myapp{\myb{P}}{\myb{r}} \myarr \myb{P} \myappsp (\mydc{node} \myappsp \myb{l} \myappsp \myb{x} \myappsp \myb{r})) \myarr \\
2926 \myapp{\myb{P}}{\mytmt}
2931 As expected, the eliminator embodies structural induction on trees.
2932 We have a base case for $\myb{P} \myappsp \mydc{leaf}$, and an
2933 inductive step that given two subtrees and the predicate applied to
2934 them needs to return the predicate applied to the tree formed by a
2935 node with the two subtrees as children.
2937 \item[Empty type] We have presented types that have at least one
2938 constructors, but nothing prevents us from defining types with
2939 \emph{no} constructors:
2940 \[\myadt{\mytyc{Empty}}{ }{ }{ }\]
2941 What shall the `induction principle' on $\mytyc{Empty}$ be? Does it
2942 even make sense to talk about induction on $\mytyc{Empty}$?
2943 $\mykant$\ does not care, and generates an eliminator with no `cases':
2946 \AxiomC{$\myinf{\mytmt}{\mytyc{Empty}}$}
2947 \UnaryInfC{$\myinf{\myempty.\myfun{elim} \myappsp \mytmt}{(\myb{P} {:} \mytmt \myarr \mytyp) \myarr \myapp{\myb{P}}{\mytmt}}$}
2949 which lets us write the $\myfun{absurd}$ that we know and love:
2952 \myfun{absurd} : (\myb{A} {:} \mytyp) \myarr \myempty \myarr \myb{A} \\
2953 \myfun{absurd}\myappsp \myb{A} \myappsp \myb{x} \mapsto \myempty.\myfun{elim} \myappsp \myb{x} \myappsp (\myabs{\myarg}{\myb{A}})
2957 \item[Ordered lists] Up to this point, the examples shown are nothing
2958 new to the \{Haskell, SML, OCaml, functional\} programmer. However
2959 dependent types let us express much more than that. A useful example
2960 is the type of ordered lists. There are many ways to define such a
2961 thing, but we will define ours to store the bounds of the list, making
2962 sure that $\mydc{cons}$ing respects that.
2964 First, using $\myunit$ and $\myempty$, we define a type expressing the
2965 ordering on natural numbers, $\myfun{le}$---`less or equal'.
2966 $\myfun{le}\myappsp \mytmm \myappsp \mytmn$ will be inhabited only if
2967 $\mytmm \le \mytmn$:
2970 \myfun{le} : \mynat \myarr \mynat \myarr \mytyp \\
2971 \myfun{le} \myappsp \myb{n} \mapsto \\
2972 \myind{2} \mynat.\myfun{elim} \\
2973 \myind{2}\myind{2} \myb{n} \\
2974 \myind{2}\myind{2} (\myabs{\myarg}{\mynat \myarr \mytyp}) \\
2975 \myind{2}\myind{2} (\myabs{\myarg}{\myunit}) \\
2976 \myind{2}\myind{2} (\myabs{\myb{n}\, \myb{f}\, \myb{m}}{
2977 \mynat.\myfun{elim} \myappsp \myb{m} \myappsp (\myabs{\myarg}{\mytyp}) \myappsp \myempty \myappsp (\myabs{\myb{m'}\, \myarg}{\myapp{\myb{f}}{\myb{m'}}})
2981 We return $\myunit$ if the scrutinised is $\mydc{zero}$ (every
2982 number in less or equal than zero), $\myempty$ if the first number is
2983 a $\mydc{suc}$cessor and the second a $\mydc{zero}$, and we recurse if
2984 they are both successors. Since we want the list to have possibly
2985 `open' bounds, for example for empty lists, we create a type for
2986 `lifted' naturals with a bottom ($\le$ everything but itself) and top
2987 ($\ge$ everything but itself) elements, along with an associated comparison
2991 \myadt{\mytyc{Lift}}{ }{ }{\mydc{bot} \mydcsep \mydc{lift} \myappsp \mynat \mydcsep \mydc{top}}\\
2992 \myfun{le'} : \mytyc{Lift} \myarr \mytyc{Lift} \myarr \mytyp\\
2993 \myfun{le'} \myappsp \myb{l_1} \mapsto \\
2994 \myind{2} \mytyc{Lift}.\myfun{elim} \\
2995 \myind{2}\myind{2} \myb{l_1} \\
2996 \myind{2}\myind{2} (\myabs{\myarg}{\mytyc{Lift} \myarr \mytyp}) \\
2997 \myind{2}\myind{2} (\myabs{\myarg}{\myunit}) \\
2998 \myind{2}\myind{2} (\myabs{\myb{n_1}\, \myb{l_2}}{
2999 \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
3001 \myind{2}\myind{2} (\myabs{\myb{l_2}}{
3002 \mytyc{Lift}.\myfun{elim} \myappsp \myb{l_2} \myappsp (\myabs{\myarg}{\mytyp}) \myappsp \myempty \myappsp (\myabs{\myarg}{\myempty}) \myappsp \myunit
3006 Finally, we can define a type of ordered lists. The type is
3007 parametrised over two \emph{values} representing the lower and upper
3008 bounds of the elements, as opposed to the \emph{type} parameters
3009 that we are used to in Haskell or similar languages. An empty
3010 list will have to have evidence that the bounds are ordered, and
3011 each time we add an element we require the list to have a matching
3015 \myadt{\mytyc{OList}}{\myappsp (\myb{low}\ \myb{upp} {:} \mytyc{Lift})}{\\ \myind{2}}{
3016 \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})
3020 Note that in the $\mydc{cons}$ constructor we quantify over the first
3021 argument, which will determine the type of the following
3022 arguments---again something we cannot do in systems like Haskell. If
3023 we want we can then employ this structure to write and prove correct
3024 various sorting algorithms.\footnote{See this presentation by Conor
3026 \url{https://personal.cis.strath.ac.uk/conor.mcbride/Pivotal.pdf},
3027 and this blog post by the author:
3028 \url{http://mazzo.li/posts/AgdaSort.html}.}
3030 \item[Dependent products] Apart from $\mysyn{data}$, $\mykant$\ offers
3031 us another way to define types: $\mysyn{record}$. A record is a
3032 data type with one constructor and `projections' to extract specific
3033 fields of the said constructor.
3035 For example, we can recover dependent products:
3038 \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}}}
3041 Here $\myfst$ and $\mysnd$ are the projections, with their respective
3042 types. Note that each field can refer to the preceding fields---in
3043 this case we have the type of $\myfun{snd}$ depending on the value of
3044 $\myfun{fst}$. A constructor will be automatically generated, under
3045 the name of $\mytyc{Prod}.\mydc{constr}$. Dually to data types, we
3046 will omit the type constructor prefix for record projections.
3048 Following the bidirectionality of the system, we have that projections
3049 (the destructors of the record) infer the type, while the constructor
3054 \AxiomC{$\mychk{\mytmm}{\mytya}$}
3055 \AxiomC{$\mychk{\mytmn}{\myapp{\mytyb}{\mytmm}}$}
3056 \BinaryInfC{$\mychk{\mytyc{Prod}.\mydc{constr} \myappsp \mytmm \myappsp \mytmn}{\mytyc{Prod} \myappsp \mytya \myappsp \mytyb}$}
3058 \UnaryInfC{\phantom{$\myinf{\myfun{snd} \myappsp \mytmt}{\mytyb \myappsp (\myfst \myappsp \mytmt)}$}}
3061 \AxiomC{$\hspace{0.2cm}\myinf{\mytmt}{\mytyc{Prod} \myappsp \mytya \myappsp \mytyb}\hspace{0.2cm}$}
3062 \UnaryInfC{$\myinf{\myfun{fst} \myappsp \mytmt}{\mytya}$}
3064 \UnaryInfC{$\myinf{\myfun{snd} \myappsp \mytmt}{\mytyb \myappsp (\myfst \myappsp \mytmt)}$}
3068 What we have defined here is equivalent to ITT's dependent products.
3077 \mynamesyn ::= \cdots \mysynsep \mytyc{D} \mysynsep \mytyc{D}.\mydc{c} \mysynsep \mytyc{D}.\myfun{f}
3084 \mydesc{syntax elaboration:}{\mydeclsyn \myelabf \mytmsyn ::= \cdots}{
3087 \begin{array}{r@{\ }l}
3088 & \myadt{\mytyc{D}}{\mytele}{}{\cdots\ |\ \mydc{c}_n : \mytele_n } \\
3091 \begin{array}{r@{\ }c@{\ }l}
3092 \mytmsyn & ::= & \cdots \mysynsep \myapp{\mytyc{D}}{\mytmsyn^{\mytele}} \mysynsep \cdots \mysynsep
3093 \mytyc{D}.\mydc{c}_n \myappsp \mytmsyn^{\mytele_n} \mysynsep \mytyc{D}.\myfun{elim} \myappsp \mytmsyn \\
3101 \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
3106 \myinf{\mytele \myarr \mytyp}{\mytyp}\hspace{0.8cm}
3107 \mytyc{D} \not\in \myctx \\
3108 \myinff{\myctx;\ \mytyc{D} : \mytele \myarr \mytyp}{\mytele \mycc \mytele_i \myarr \myapp{\mytyc{D}}{\mytelee}}{\mytyp}\ \ \ (1 \leq i \leq n) \\
3109 \text{For each $(\myb{x} {:} \mytya)$ in each $\mytele_i$, if $\mytyc{D} \in \mytya$, then $\mytya = \myapp{\mytyc{D}}{\vec{\mytmt}}$.}
3113 \begin{array}{r@{\ }c@{\ }l}
3114 \myctx & \myelabt & \myadt{\mytyc{D}}{\mytele}{}{ \cdots \ |\ \mydc{c}_n : \mytele_n } \\
3115 & & \vspace{-0.2cm} \\
3116 & \myelabf & \myctx;\ \mytyc{D} : \mytele \myarr \mytyp;\ \cdots;\ \mytyc{D}.\mydc{c}_n : \mytele \mycc \mytele_n \myarr \myapp{\mytyc{D}}{\mytelee}; \\
3118 \begin{array}{@{}r@{\ }l l}
3119 \mytyc{D}.\myfun{elim} : & \mytele \myarr (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr & \textbf{target} \\
3120 & (\myb{P} {:} \myapp{\mytyc{D}}{\mytelee} \myarr \mytyp) \myarr & \textbf{motive} \\
3124 (\mytele_n \mycc \myhyps(\myb{P}, \mytele_n) \myarr \myapp{\myb{P}}{(\myapp{\mytyc{D}.\mydc{c}_n}{\mytelee_n})}) \myarr
3125 \end{array} \right \}
3126 & \textbf{methods} \\
3127 & \myapp{\myb{P}}{\myb{x}} &
3131 \DisplayProof \\ \vspace{0.2cm}\ \\
3133 \begin{array}{@{}l l@{\ } l@{} r c l}
3134 \textbf{where} & \myhyps(\myb{P}, & \myemptytele &) & \mymetagoes & \myemptytele \\
3135 & \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) \\
3136 & \myhyps(\myb{P}, & (\myb{x} {:} \mytya) \mycc \mytele & ) & \mymetagoes & \myhyps(\myb{P}, \mytele)
3144 \mydesc{reduction elaboration:}{\mydeclsyn \myelabf \myctx \vdash \mytmsyn \myred \mytmsyn}{
3146 $\myadt{\mytyc{D}}{\mytele}{}{ \cdots \ |\ \mydc{c}_n : \mytele_n } \ \ \myelabf$
3147 \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
3148 \AxiomC{$\mytyc{D}.\mydc{c}_i : \mytele;\mytele_i \myarr \myapp{\mytyc{D}}{\mytelee} \in \myctx$}
3150 \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)}
3152 \DisplayProof \\ \vspace{0.2cm}\ \\
3154 \begin{array}{@{}l l@{\ } l@{} r c l}
3155 \textbf{where} & \myrecs(\myse{P}, \vec{m}, & \myemptytele &) & \mymetagoes & \myemptytele \\
3156 & \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) \\
3157 & \myrecs(\myse{P}, \vec{m}, & (\myb{x} {:} \mytya); \mytele &) & \mymetagoes & \myrecs(\myse{P}, \vec{m}, \mytele)
3164 \mydesc{syntax elaboration:}{\myelab{\mydeclsyn}{\mytmsyn ::= \cdots}}{
3167 \begin{array}{r@{\ }c@{\ }l}
3168 \myctx & \myelabt & \myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \\
3171 \begin{array}{r@{\ }c@{\ }l}
3172 \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 \\
3180 \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
3184 \myinf{\mytele \myarr \mytyp}{\mytyp}\hspace{0.8cm}
3185 \mytyc{D} \not\in \myctx \\
3186 \myinff{\myctx; \mytele; (\myb{f}_j : \myse{F}_j)_{j=1}^{i - 1}}{F_i}{\mytyp} \myind{3} (1 \le i \le n)
3190 \begin{array}{r@{\ }c@{\ }l}
3191 \myctx & \myelabt & \myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \\
3192 & & \vspace{-0.2cm} \\
3193 & \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}; \\
3194 & & \mytyc{D}.\mydc{constr} : \mytele \myarr \myse{F}_1 \myarr \cdots \myarr \myse{F}_n \myarr \myapp{\mytyc{D}}{\mytelee};
3202 \mydesc{reduction elaboration:}{\mydeclsyn \myelabf \myctx \vdash \mytmsyn \myred \mytmsyn}{
3204 $\myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \ \ \myelabf$
3205 \AxiomC{$\mytyc{D} \in \myctx$}
3206 \UnaryInfC{$\myctx \vdash \myapp{\mytyc{D}.\myfun{f}_i}{(\mytyc{D}.\mydc{constr} \myappsp \vec{t})} \myred t_i$}
3210 \caption{Elaboration for data types and records.}
3214 \begin{mydef}[Elaboration for user defined types]
3215 Following the intuition given by the examples, the full elaboration
3216 machinery is presented Figure \ref{fig:elab}.
3218 Our elaboration is essentially a modification of Figure 9 of
3219 \cite{McBride2004}. However, our data types are not inductive
3220 families,\footnote{See Section \ref{sec:future-work} for a brief
3221 description of inductive families.} we do bidirectional type checking
3222 by treating constructors/destructors as syntax, and we have records.
3224 \begin{mydef}[Strict positivity]
3225 A inductive type declaration is \emph{strictly positive} if recursive
3226 occurrences of the type we are defining do not appear embedded
3227 anywhere in the domain part of any function in the types for the data
3230 In data type declarations we allow recursive occurrences as long as they
3231 are strictly positive, which ensures the consistency of the theory. To
3232 achieve that we employing a syntactic check to make sure that this is
3233 the case---in fact the check is stricter than necessary for simplicity,
3234 given that we allow recursive occurrences only at the top level of data
3235 constructor arguments. For example a definition of the $\mytyc{W}$ type
3236 is accepted in Agda but rejected in \mykant. This is to make the
3237 eliminator generation simpler, and in practice it is seldom an
3240 Without these precautions, we can easily derive any type with no
3243 data Fix a = Fix (Fix a -> a) -- Negative occurrence of `Fix a'
3244 -- Term inhabiting any type `a'
3246 boom = (\f -> f (Fix f)) (\x -> (\(Fix f) -> f) x x)
3248 See \cite{Dybjer1991} for a more formal treatment of inductive
3251 For what concerns records, recursive occurrences are disallowed. The
3252 reason for this choice is answered by the reason for the choice of
3253 having records at all: we need records to give the user types with
3254 $\eta$-laws for equality, as we saw in Section \ref{sec:eta-expand}
3255 and in the treatment of OTT in Section \ref{sec:ott}. If we tried to
3256 $\eta$-expand recursive data types, we would expand forever.
3258 \begin{mydef}[Bidirectional type checking for elaborated types]
3259 To implement bidirectional type checking for constructors and
3260 destructors, we store their types in full in the context, and then
3261 instantiate when due.
3264 \mydesc{typing:}{\myctx
3265 \vdash \mytmsyn \Updownarrow \mytmsyn}{ \AxiomC{$
3267 \mytyc{D} : \mytele \myarr \mytyp \in \myctx \hspace{1cm}
3268 \mytyc{D}.\mydc{c} : \mytele \mycc \mytele' \myarr
3269 \myapp{\mytyc{D}}{\mytelee} \in \myctx \\
3270 \mytele'' = (\mytele;\mytele')\vec{A} \hspace{1cm}
3271 \mychkk{\myctx; \mytake_{i-1}(\mytele'')}{t_i}{\myix_i( \mytele'')}\ \
3272 (1 \le i \le \mytele'')
3275 \UnaryInfC{$\mychk{\myapp{\mytyc{D}.\mydc{c}}{\vec{t}}}{\myapp{\mytyc{D}}{\vec{A}}}$}
3280 \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
3281 \AxiomC{$\mytyc{D}.\myfun{f} : \mytele \mycc (\myb{x} {:}
3282 \myapp{\mytyc{D}}{\mytelee}) \myarr \myse{F}$}
3283 \AxiomC{$\myjud{\mytmt}{\myapp{\mytyc{D}}{\vec{A}}}$}
3284 \TrinaryInfC{$\myinf{\myapp{\mytyc{D}.\myfun{f}}{\mytmt}}{(\mytele
3285 \mycc (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr
3286 \myse{F})(\vec{A};\mytmt)}$}
3289 Note that for 0-ary type constructors, like $\mynat$, we do not need to
3290 check canonical terms: we can automatically infer that $\mydc{zero}$ and
3291 $\mydc{suc}\myappsp n$ are of type $\mynat$. \mykant\ implements this measure, even
3292 if it is not shown in the typing rule for simplicity.
3294 \subsubsection{Why user defined types? Why eliminators?}
3296 The hardest design choice in developing $\mykant$\ was to decide whether
3297 user defined types should be included, and how to handle them. As we
3298 saw, while we can devise general structures like $\mytyc{W}$, they are
3299 unsuitable both for for direct usage and `mechanical' usage. Thus most
3300 theorem provers in the wild provide some means for the user to define
3301 structures tailored to specific uses.
3303 Even if we take user defined types for granted, while there is not much
3304 debate on how to handle records, there are two broad schools of thought
3305 regarding the handling of data types:
3307 \item[Fixed points and pattern matching] The road chosen by Agda and Coq.
3308 Functions are written like in Haskell---matching on the input and with
3309 explicit recursion. An external check on the recursive arguments
3310 ensures that they are decreasing, and thus that all functions
3311 terminate. This approach is the best in terms of user usability, but
3312 it is tricky to implement correctly.
3314 \item[Elaboration into eliminators] The road chose by \mykant, and
3315 pioneered by the Epigram line of work. The advantage is that we can
3316 reduce every data type to simple definitions which guarantee
3317 termination and are simple to reduce and type. It is however more
3318 cumbersome to use than pattern matching, although \cite{McBride2004}
3319 has shown how to implement an expressive pattern matching interface on
3320 top of a larger set of combinators of those provided by \mykant.
3322 We can go ever further down this road and elaborate the declarations
3323 for data types themselves to a small set of primitives, so that our `core'
3324 language will be very small and manageable
3325 \citep{dagand2012elaborating, chapman2010gentle}.
3328 We chose the safer and easier to implement path, given the time
3329 constraints and the higher confidence of correctness. See also Section
3330 \ref{sec:future-work} for a brief overview of ways to extend or treat
3333 \subsection{Cumulative hierarchy and typical ambiguity}
3334 \label{sec:term-hierarchy}
3336 Having a well founded type hierarchy is crucial if we want to retain
3337 consistency, otherwise we can break our type systems by proving bottom,
3338 as shown in Appendix \ref{app:hurkens}.
3340 However, hierarchy as presented in section \ref{sec:itt} is a
3341 considerable burden on the user, on various levels. Consider for
3342 example how we recovered disjunctions in Section \ref{sec:disju}: we
3343 have a function that takes two $\mytyp_0$ and forms a new $\mytyp_0$.
3344 What if we wanted to form a disjunction containing something a
3345 $\mytyp_1$, or $\mytyp_{42}$? Our definition would fail us, since
3346 $\mytyp_1 : \mytyp_2$.
3350 \mydesc{cumulativity:}{\myctx \vdash \mytmsyn \mycumul \mytmsyn}{
3351 \begin{tabular}{ccc}
3352 \AxiomC{$\myctx \vdash \mytya \mydefeq \mytyb$}
3353 \UnaryInfC{$\myctx \vdash \mytya \mycumul \mytyb$}
3356 \AxiomC{\phantom{$\myctx \vdash \mytya \mydefeq \mytyb$}}
3357 \UnaryInfC{$\myctx \vdash \mytyp_l \mycumul \mytyp_{l+1}$}
3360 \AxiomC{$\myctx \vdash \mytya \mycumul \mytyb$}
3361 \AxiomC{$\myctx \vdash \mytyb \mycumul \myse{C}$}
3362 \BinaryInfC{$\myctx \vdash \mytya \mycumul \myse{C}$}
3368 \begin{tabular}{ccc}
3369 \AxiomC{$\myjud{\mytmt}{\mytya}$}
3370 \AxiomC{$\myctx \vdash \mytya \mycumul \mytyb$}
3371 \BinaryInfC{$\myjud{\mytmt}{\mytyb}$}
3374 \AxiomC{$\myctx \vdash \mytya_1 \mydefeq \mytya_2$}
3375 \AxiomC{$\myctx; \myb{x} : \mytya_1 \vdash \mytyb_1 \mycumul \mytyb_2$}
3376 \BinaryInfC{$\myctx (\myb{x} {:} \mytya_1) \myarr \mytyb_1 \mycumul (\myb{x} {:} \mytya_2) \myarr \mytyb_2$}
3380 \caption{Cumulativity rules for base types in \mykant, plus a
3381 `conversion' rule for cumulative types.}
3382 \label{fig:cumulativity}
3385 One way to solve this issue is a \emph{cumulative} hierarchy, where
3386 $\mytyp_{l_1} : \mytyp_{l_2}$ iff $l_1 < l_2$. This way we retain
3387 consistency, while allowing for `large' definitions that work on small
3390 \begin{mydef}[Cumulativity for \mykant' base types]
3391 Figure \ref{fig:cumulativity} gives a formal definition of
3392 \emph{cumulativity} for the base types. Similar measures can be taken
3393 for user defined types, withe the type living in the least upper bound
3394 of the levels where the types contained data live.
3396 For example we might define our disjunction to be
3398 \myarg\myfun{$\vee$}\myarg : \mytyp_{100} \myarr \mytyp_{100} \myarr \mytyp_{100}
3400 And hope that $\mytyp_{100}$ will be large enough to fit all the types
3401 that we want to use with our disjunction. However, there are two
3402 problems with this. First, clumsiness of having to manually specify the
3403 size of types is still there. More importantly, if we want to use
3404 $\myfun{$\vee$}$ itself as an argument to other type-formers, we need to
3405 make sure that those allow for types at least as large as
3408 A better option is to employ a mechanised version of what Russell called
3409 \emph{typical ambiguity}: we let the user live under the illusion that
3410 $\mytyp : \mytyp$, but check that the statements about types are
3411 consistent under the hood. $\mykant$\ implements this following the
3412 plan given by \cite{Huet1988}. See also \cite{Harper1991} for a
3413 published reference, although describing a more complex system allowing
3414 for both explicit and explicit hierarchy at the same time.
3416 We define a partial ordering on the levels, with both weak ($\le$) and
3417 strong ($<$) constraints, the laws governing them being the same as the
3418 ones governing $<$ and $\le$ for the natural numbers. Each occurrence
3419 of $\mytyp$ is decorated with a unique reference. We keep a set of
3420 constraints regarding the ordering of each occurrence of $\mytyp$, each
3421 represented by its unique reference. We add new constraints as we type
3422 check, generating new references when needed.
3424 For example, when type checking the type $\mytyp\, r_1$, where $r_1$
3425 denotes the unique reference assigned to that term, we will generate a
3426 new fresh reference and return the type $\mytyp\, r_2$, adding the
3427 constraint $r_1 < r_2$ to the set. When type checking $\myctx \vdash
3428 \myfora{\myb{x}}{\mytya}{\mytyb}$, if $\myctx \vdash \mytya : \mytyp\,
3429 r_1$ and $\myctx; \myb{x} : \mytyb \vdash \mytyb : \mytyp\,r_2$; we will
3430 generate new reference $r$ and add $r_1 \le r$ and $r_2 \le r$ to the
3433 If at any point the constraint set becomes inconsistent, type checking
3434 fails. Moreover, when comparing two $\mytyp$ terms---during the process
3435 of deciding definitional equality for two terms---we equate their
3436 respective references with two $\le$ constraints. Implementation
3437 details are given in Section \ref{sec:hier-impl}.
3439 Another more flexible but also more verbose alternative is the one
3440 chosen by Agda, where levels can be quantified so that the relationship
3441 between arguments and result in type formers can be explicitly
3444 \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}
3446 Inference algorithms to automatically derive this kind of relationship
3447 are currently subject of research. We choose a less flexible but more
3448 concise way, since it is easier to implement and better understood.
3450 \subsection{Observational equality, \mykant\ style}
3452 There are two correlated differences between $\mykant$\ and the theory
3453 used to present OTT. The first is that in $\mykant$ we have a type
3454 hierarchy, which lets us, for example, abstract over types. The second
3455 is that we let the user define inductive types and records.
3457 Reconciling propositions for OTT and a hierarchy had already been
3458 investigated by Conor McBride,\footnote{See
3459 \url{http://www.e-pig.org/epilogue/index.html?p=1098.html}.} and we
3460 follow some of his suggestions, with some innovation. Most of the dirty
3461 work, as an extension of elaboration, is to handle reduction rules and
3462 coercions for data types---both type constructors and data constructors.
3464 \subsubsection{The \mykant\ prelude, and $\myprop$ositions}
3466 Before defining $\myprop$, we define some basic types inside $\mykant$,
3467 as the target for the $\myprop$ decoder.
3468 \begin{mydef}[\mykant' propositional prelude]\ \end{mydef}
3471 \myadt{\mytyc{Empty}}{}{ }{ } \\
3472 \myfun{absurd} : (\myb{A} {:} \mytyp) \myarr \mytyc{Empty} \myarr \myb{A} \mapsto \\
3473 \myind{2} \myabs{\myb{A\ \myb{bot}}}{\mytyc{Empty}.\myfun{elim} \myappsp \myb{bot} \myappsp (\myabs{\_}{\myb{A}})} \\
3476 \myreco{\mytyc{Unit}}{}{}{ } \\ \ \\
3478 \myreco{\mytyc{Prod}}{\myappsp (\myb{A}\ \myb{B} {:} \mytyp)}{ }{\myfun{fst} : \myb{A}, \myfun{snd} : \myb{B} }
3482 \begin{mydef}[Propositions and decoding]\ \end{mydef}
3486 \begin{array}{r@{\ }c@{\ }l}
3487 \mytmsyn & ::= & \cdots \mysynsep \myprdec{\myprsyn} \\
3488 \myprsyn & ::= & \mybot \mysynsep \mytop \mysynsep \myprsyn \myand \myprsyn \mysynsep \myprfora{\myb{x}}{\mytmsyn}{\myprsyn}
3493 \mydesc{proposition decoding:}{\myprdec{\mytmsyn} \myred \mytmsyn}{
3496 \begin{array}{l@{\ }c@{\ }l}
3497 \myprdec{\mybot} & \myred & \myempty \\
3498 \myprdec{\mytop} & \myred & \myunit
3503 \begin{array}{r@{ }c@{ }l@{\ }c@{\ }l}
3504 \myprdec{&\myse{P} \myand \myse{Q} &} & \myred & \mytyc{Prod} \myappsp \myprdec{\myse{P}} \myappsp \myprdec{\myse{Q}} \\
3505 \myprdec{&\myprfora{\myb{x}}{\mytya}{\myse{P}} &} & \myred &
3506 \myfora{\myb{x}}{\mytya}{\myprdec{\myse{P}}}
3512 We will overload the $\myand$ symbol to define `nested' products, and
3513 $\myproj{n}$ to project elements from them, so that
3516 \mytya \myand \mytyb = \mytya \myand (\mytyb \myand \mytop) \\
3517 \mytya \myand \mytyb \myand \myse{C} = \mytya \myand (\mytyb \myand (\myse{C} \myand \mytop)) \\
3519 \myproj{1} : \myprdec{\mytya \myand \mytyb} \myarr \myprdec{\mytya} \\
3520 \myproj{2} : \myprdec{\mytya \myand \mytyb \myand \myse{C}} \myarr \myprdec{\mytyb} \\
3524 And so on, so that $\myproj{n}$ will work with all products with at
3525 least than $n$ elements. Logically a 0-ary $\myand$ will correspond to
3528 \subsubsection{Some OTT examples}
3530 Before presenting the direction that $\mykant$\ takes, let us consider
3531 two examples of use-defined data types, and the result we would expect
3532 given what we already know about OTT, assuming the same propositional
3537 \item[Product types] Let us consider first the already mentioned
3538 dependent product, using the alternate name $\mysigma$\footnote{For
3539 extra confusion, `dependent products' are often called `dependent
3540 sums' in the literature, referring to the interpretation that
3541 identifies the first element as a `tag' deciding the type of the
3542 second element, which lets us recover sum types (disjuctions), as we
3543 saw in Section \ref{sec:depprod}. Thus, $\mysigma$.} to
3544 avoid confusion with the $\mytyc{Prod}$ in the prelude:
3547 \myreco{\mysigma}{\myappsp (\myb{A} {:} \mytyp) \myappsp (\myb{B} {:} \myb{A} \myarr \mytyp)}{\\ \myind{2}}{\myfst : \myb{A}, \mysnd : \myapp{\myb{B}}{\myb{fst}}}
3550 First type-level equality. The result we want is
3553 \mysigma \myappsp \mytya_1 \myappsp \mytyb_1 \myeq \mysigma \myappsp \mytya_2 \myappsp \mytyb_2 \myred \\
3554 \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}}}
3557 The difference here is that in the original presentation of OTT the
3558 type binders are explicit, while here $\mytyb_1$ and $\mytyb_2$ are
3559 functions returning types. We can do this thanks to the type
3560 hierarchy, and this hints at the fact that heterogeneous equality will
3561 have to allow $\mytyp$ `to the right of the colon'. Indeed,
3562 heterogeneous equalities involving abstractions over types will
3563 provide the solution to simplify the equality above.
3565 If we take, just like we saw previously in OTT
3568 \myjm{\myse{f}_1}{\myfora{\mytya_1}{\myb{x_1}}{\mytyb_1}}{\myse{f}_2}{\myfora{\mytya_2}{\myb{x_2}}{\mytyb_2}} \myred \\
3569 \myind{2} \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{
3570 \myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2} \myimpl
3571 \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}]}
3575 Then we can simply have
3578 \mysigma \myappsp \mytya_1 \myappsp \mytyb_1 \myeq \mysigma \myappsp \mytya_2 \myappsp \mytyb_2 \myred \\ \myind{2} \mytya_1 \myeq \mytya_2 \myand \myjm{\mytyb_1}{\mytya_1 \myarr \mytyp}{\mytyb_2}{\mytya_2 \myarr \mytyp}
3581 Which will reduce to precisely what we desire, but with an
3582 heterogeneous equalities relating types instead of values:
3585 \mytya_1 \myeq \mytya_2 \myand \myjm{\mytyb_1}{\mytya_1 \myarr \mytyp}{\mytyb_2}{\mytya_2 \myarr \mytyp} \myred \\
3586 \mytya_1 \myeq \mytya_2 \myand
3587 \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{
3588 \myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2} \myimpl
3589 \myjm{\myapp{\mytyb_1}{\myb{x_1}}}{\mytyp}{\myapp{\mytyb_2}{\myb{x_2}}}{\mytyp}
3593 If we pretend for the moment that those heterogeneous equalities were
3594 type equalities, things run smoothly. For what concerns coercions and
3595 quotation, things stay the same (apart from the fact that we apply to
3596 the second argument instead of substituting). We can recognise
3597 records such as $\mysigma$ as such and employ projections in value
3598 equality and coercions; as to not impede progress if not necessary.
3600 \item[Lists] Now for finite lists, which will give us a taste for data
3604 \myadt{\mylist}{\myappsp (\myb{A} {:} \mytyp)}{ }{\mydc{nil} \mydcsep \mydc{cons} \myappsp \myb{A} \myappsp (\myapp{\mylist}{\myb{A}})}
3607 Type equality is simple---we only need to compare the parameter:
3609 \mylist \myappsp \mytya_1 \myeq \mylist \myappsp \mytya_2 \myred \mytya_1 \myeq \mytya_2
3611 For coercions, we transport based on the constructor, recycling the
3612 proof for the inductive occurrence:
3614 \begin{array}{@{}l@{\ }c@{\ }l}
3615 \mycoe \myappsp (\mylist \myappsp \mytya_1) \myappsp (\mylist \myappsp \mytya_2) \myappsp \myse{Q} \myappsp \mydc{nil} & \myred & \mydc{nil} \\
3616 \mycoe \myappsp (\mylist \myappsp \mytya_1) \myappsp (\mylist \myappsp \mytya_2) \myappsp \myse{Q} \myappsp (\mydc{cons} \myappsp \mytmm \myappsp \mytmn) & \myred & \\
3617 \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)}
3620 Value equality is unsurprising---we match the constructors, and
3621 return bottom for mismatches. However, we also need to equate the
3622 parameter in $\mydc{nil}$:
3624 \begin{array}{r@{ }c@{\ }c@{\ }c@{}l@{\ }c@{\ }r@{}c@{\ }c@{\ }c@{}l@{\ }l}
3625 (& \mydc{nil} & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{nil} & : & \myapp{\mylist}{\mytya_2} &) \myred \mytya_1 \myeq \mytya_2 \\
3626 (& \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 \\
3627 & \multicolumn{11}{@{}l}{ \myind{2}
3628 \myjm{\mytmm_1}{\mytya_1}{\mytmm_2}{\mytya_2} \myand \myjm{\mytmn_1}{\myapp{\mylist}{\mytya_1}}{\mytmn_2}{\myapp{\mylist}{\mytya_2}}
3630 (& \mydc{nil} & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{cons} \myappsp \mytmm_2 \myappsp \mytmn_2 & : & \myapp{\mylist}{\mytya_2} &) \myred \mybot \\
3631 (& \mydc{cons} \myappsp \mytmm_1 \myappsp \mytmn_1 & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{nil} & : & \myapp{\mylist}{\mytya_2} &) \myred \mybot
3636 \subsubsection{Only one equality}
3638 Given the examples above, a more `flexible' heterogeneous equality must
3639 emerge, since of the fact that in $\mykant$ we re-gain the possibility
3640 of abstracting and in general handling types in a way that was not
3641 possible in the original OTT presentation. Moreover, we found that the
3642 rules for value equality work well if used with user defined type
3643 abstractions---for example in the case of dependent products we recover
3644 the original definition with explicit binders, in a natural manner.
3646 \begin{mydef}[Propositions, coercions, coherence, equalities and
3647 equality reduction for \mykant] See Figure \ref{fig:kant-eq-red}.
3650 \begin{mydef}[Type equality in \mykant]
3651 We define $\mytya \myeq \mytyb$ as an abbreviation for
3652 $\myjm{\mytya}{\mytyp}{\mytyb}{\mytyp}$.
3655 In fact, we can drop a separate notion of type-equality, which will
3656 simply be served by $\myjm{\mytya}{\mytyp}{\mytyb}{\mytyp}$. We shall
3657 still distinguish equalities relating types for hierarchical
3658 purposes. We exploit record to perform $\eta$-expansion. Moreover,
3659 given the nested $\myand$s, values of data types with zero constructors
3660 (such as $\myempty$) and records with zero destructors (such as
3661 $\myunit$) will be automatically always identified as equal. As in the
3662 original OTT, and for the same reasons, we can take $\myfun{coh}$ as
3670 \begin{array}{r@{\ }c@{\ }l}
3671 \mytmsyn & ::= & \cdots \mysynsep \mycoee{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \mysynsep
3672 \mycohh{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
3673 \myprsyn & ::= & \cdots \mysynsep \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
3680 \mydesc{typing:}{\myctx \vdash \mytmsyn \Leftrightarrow \mytmsyn}{
3683 \AxiomC{$\mychk{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
3684 \AxiomC{$\mychk{\mytmt}{\mytya}$}
3685 \BinaryInfC{$\myinf{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}$}
3688 \AxiomC{$\mychk{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
3689 \AxiomC{$\mychk{\mytmt}{\mytya}$}
3690 \BinaryInfC{$\myinf{\mycohh{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\myprdec{\myjm{\mytmt}{\mytya}{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}}}$}
3697 \mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
3700 \AxiomC{\phantom{$\myjud{\myse{P}}{\myprop}$}}
3701 \UnaryInfC{$\myjud{\mytop}{\myprop}$}
3703 \UnaryInfC{$\myjud{\mybot}{\myprop}$}
3706 \AxiomC{$\myjud{\myse{P}}{\myprop}$}
3707 \AxiomC{$\myjud{\myse{Q}}{\myprop}$}
3708 \BinaryInfC{$\myjud{\myse{P} \myand \myse{Q}}{\myprop}$}
3710 \UnaryInfC{\phantom{$\myjud{\mybot}{\myprop}$}}
3719 \phantom{\myjud{\myse{A}}{\mytyp} \hspace{0.8cm} \myjud{\mytmm}{\myse{A}}} \\
3720 \myjud{\myse{A}}{\mytyp}\hspace{0.8cm}
3721 \myjudd{\myctx; \myb{x} : \mytya}{\myse{P}}{\myprop}
3724 \UnaryInfC{$\myjud{\myprfora{\myb{x}}{\mytya}{\myse{P}}}{\myprop}$}
3729 \myjud{\myse{A}}{\mytyp} \hspace{0.8cm} \myjud{\mytmm}{\myse{A}} \\
3730 \myjud{\myse{B}}{\mytyp} \hspace{0.8cm} \myjud{\mytmn}{\myse{B}}
3733 \UnaryInfC{$\myjud{\myjm{\mytmm}{\myse{A}}{\mytmn}{\myse{B}}}{\myprop}$}
3740 \mydesc{equality reduction:}{\myctx \vdash \myprsyn \myred \myprsyn}{
3744 \UnaryInfC{$\myctx \vdash \myjm{\mytyp}{\mytyp}{\mytyp}{\mytyp} \myred \mytop$}
3748 \UnaryInfC{$\myctx \vdash \myjm{\myprdec{\myse{P}}}{\mytyp}{\myprdec{\myse{Q}}}{\mytyp} \myred \mytop$}
3756 \begin{array}{@{}r@{\ }l}
3758 \myjm{\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}}{\mytyp}{\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}}{\mytyp} \myred \\
3759 & \myind{2} \mytya_2 \myeq \mytya_1 \myand \myprfora{\myb{x_2}}{\mytya_2}{\myprfora{\myb{x_1}}{\mytya_1}{
3760 \myjm{\myb{x_2}}{\mytya_2}{\myb{x_1}}{\mytya_1} \myimpl \mytyb_1[\myb{x_1}] \myeq \mytyb_2[\myb{x_2}]
3770 \begin{array}{@{}r@{\ }l}
3772 \myjm{\myse{f}_1}{\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}}{\myse{f}_2}{\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}} \myred \\
3773 & \myind{2} \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{
3774 \myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2} \myimpl
3775 \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}]}
3784 \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
3786 \begin{array}{r@{\ }l}
3788 \myjm{\mytyc{D} \myappsp \vec{A}}{\mytyp}{\mytyc{D} \myappsp \vec{B}}{\mytyp} \myred \\
3789 & \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}))})
3798 \mydataty(\mytyc{D}, \myctx)\hspace{0.8cm}
3799 \mytyc{D}.\mydc{c} : \mytele;\mytele' \myarr \mytyc{D} \myappsp \mytelee \in \myctx \hspace{0.8cm}
3800 \mytele_A = (\mytele;\mytele')\vec{A}\hspace{0.8cm}
3801 \mytele_B = (\mytele;\mytele')\vec{B}
3805 \begin{array}{@{}l@{\ }l}
3806 \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 \\
3807 & \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}))})
3814 \AxiomC{$\mydataty(\mytyc{D}, \myctx)$}
3816 \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
3824 \myisreco(\mytyc{D}, \myctx)\hspace{0.8cm}
3825 \mytyc{D}.\myfun{f}_i : \mytele; (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr \myse{F}_i \in \myctx\\
3829 \begin{array}{@{}l@{\ }l}
3830 \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})})
3837 \UnaryInfC{$\myjm{\mytmm}{\mytya}{\mytmn}{\mytyb} \myred \mybot\ \text{if $\mytya$ and $\mytyb$ are canonical types.}$}
3840 \caption{Propositions and equality reduction in $\mykant$. We assume
3841 the presence of $\mydataty$ and $\myisreco$ as operations on the
3842 context to recognise whether a user defined type is a data type or a
3844 \label{fig:kant-eq-red}
3847 \subsubsection{Coercions}
3849 For coercions the algorithm is messier and not reproduced here for lack
3850 of a decent notation---the details are hairy but uninteresting. To give
3851 an idea of the possible complications, let us conceive a type that
3852 showcases trouble not arising in the previous examples.
3855 \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}}{
3856 \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})
3860 For type equalities we will have
3862 \begin{array}{@{}l@{\ }l}
3863 \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]
3865 \myjm{\mytya_1}{\mynat \myarr \mytyp}{\mytya_2}{\mynat \myarr \mytyp} \myand \\
3866 \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} \\
3867 \myjm{\myse{k}_1}{\mynat}{\myse{k}_2}{\mynat}
3868 \end{array} & \myred \\[0.7cm]
3870 (\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 \\
3871 (\mynat \myeq \mynat \myand \left(
3873 \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}}
3876 \myjm{\myse{k}_1}{\mynat}{\myse{k}_2}{\mynat}
3877 \end{array} & \myred \\[0.9cm]
3879 (\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 \\
3880 (\mytop \myand \left(
3882 \myprfora{\myb{x_1}\, \myb{x_2}}{\mynat}{\myjm{\myb{x_1}}{\mynat}{\myb{x_2}}{\mynat} \myimpl \\
3883 \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 \\
3884 \mytyb_1 \myappsp \myb{x_1} \myappsp \myb{y_1} \myeq \mytyb_2 \myappsp \myb{x_2} \myappsp \myb{y_2}}}}
3887 \myjm{\myse{k}_1}{\mynat}{\myse{k}_2}{\mynat}
3891 The result, while looking complicated, is actually saying something
3892 simple---given equal inputs, the parameters for $\mytyc{Max}$ will
3893 return equal types. Moreover, we have evidence that the two $\myb{k}$
3894 parameters are equal. When coercing, we need to mechanically generate
3895 one proof of equality for each argument, and then coerce:
3898 \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 \\
3900 \begin{array}[t]{l@{\ }l@{\ }c@{\ }l}
3901 \mysyn{let} & \myb{Q_{Ak}} & \mapsto & \myhole{?} : \myprdec{\mytya_1 \myappsp \myse{k}_1 \myeq \mytya_2 \myappsp \myse{k}_2} \\
3902 & \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 \\
3903 & \myb{Q_{\mathbb{N}}} & \mapsto & \myhole{?} : \myprdec{\mynat \myeq \mynat} \\
3904 & \myb{n_2} & \mapsto & \mycoee{\mynat}{\mynat}{\myb{Q_{\mathbb{N}}}}{\myse{n_1}} : \mynat \\
3905 & \myb{Q_A} & \mapsto & \myhole{?} : \myprdec{\mytya_1 \myappsp \myse{n_1} \myeq \mytya_2 \myappsp \myb{n_2}} \\
3906 & \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} \\
3907 & \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}} \\
3908 & \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} \\
3909 \mysyn{in} & \multicolumn{3}{@{}l}{\mydc{max} \myappsp \myb{ak_2} \myappsp \myb{n_2} \myappsp \myb{a_2} \myappsp \myb{b_2}}
3913 For equalities regarding types that are external to the data type we can
3914 derive a proof by reflexivity by invoking $\mydc{refl}$ as defined in
3915 Section \ref{sec:lazy}, and the instantiate arguments if we need too.
3916 In this case, for $\mynat$, we do not have any arguments. For
3917 equalities concerning arguments of the type constructor or already
3918 coerced arguments of the type constructor we have to refer to the right
3919 proof and use $\mycoh$erence when due, which is where the technical
3923 \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 \\
3925 \begin{array}[t]{l@{\ }l@{\ }c@{\ }l}
3926 \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} \\
3927 & \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 \\
3928 & \myb{Q_{\mathbb{N}}} & \mapsto & \mydc{refl} \myappsp \mynat : \myprdec{\mynat \myeq \mynat} \\
3929 & \myb{n_2} & \mapsto & \mycoee{\mynat}{\mynat}{\myb{Q_{\mathbb{N}}}}{\myse{n_1}} : \mynat \\
3930 & \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}} \\
3931 & \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} \\
3932 & \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}} \\
3933 & \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} \\
3934 \mysyn{in} & \multicolumn{3}{@{}l}{\mydc{max} \myappsp \myb{ak_2} \myappsp \myb{n_2} \myappsp \myb{a_2} \myappsp \myb{b_2}}
3939 \subsubsection{$\myprop$ and the hierarchy}
3941 We shall have, at each universe level, not only a $\mytyp_l$ but also a
3942 $\myprop_l$. Where will propositions placed in the type hierarchy? The
3943 main indicator is the decoding operator, since it converts into things
3944 that already live in the hierarchy. For example, if we have
3946 \myprdec{\mynat \myarr \mybool \myeq \mynat \myarr \mybool} \myred
3947 \mytop \myand ((\myb{x}\, \myb{y} : \mynat) \myarr \mytop \myarr \mytop)
3949 we will better make sure that the `to be decoded' is at level compatible
3950 (read: larger) with its reduction. In the example above, we will have
3951 that proposition to be at least as large as the type of $\mynat$, since
3952 the reduced proof will abstract over it. Pretending that we had
3953 explicit, non cumulative levels, it would be tempting to have
3956 \AxiomC{$\myjud{\myse{Q}}{\myprop_l}$}
3957 \UnaryInfC{$\myjud{\myprdec{\myse{Q}}}{\mytyp_l}$}
3960 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
3961 \AxiomC{$\myjud{\mytyb}{\mytyp_l}$}
3962 \BinaryInfC{$\myjud{\myjm{\mytya}{\mytyp_{l}}{\mytyb}{\mytyp_{l}}}{\myprop_l}$}
3966 $\mybot$ and $\mytop$ living at any level, $\myand$ and $\forall$
3967 following rules similar to the ones for $\myprod$ and $\myarr$ in
3968 Section \ref{sec:itt}. However, we need to be careful with value
3969 equality since for example we have that
3971 \myprdec{\myjm{\myse{f}_1}{\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}}{\myse{f}_2}{\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}}}
3973 \myfora{\myb{x_1}}{\mytya_1}{\myfora{\myb{x_2}}{\mytya_2}{\cdots}}
3975 where the proposition decodes into something of at least type $\mytyp_l$, where
3976 $\mytya_l : \mytyp_l$ and $\mytyb_l : \mytyp_l$. We can resolve this
3977 tension by making all equalities larger:
3979 \AxiomC{$\myjud{\mytmm}{\mytya}$}
3980 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
3981 \AxiomC{$\myjud{\mytmn}{\mytyb}$}
3982 \AxiomC{$\myjud{\mytyb}{\mytyp_l}$}
3983 \QuaternaryInfC{$\myjud{\myjm{\mytmm}{\mytya}{\mytmm}{\mytya}}{\myprop_l}$}
3985 This is disappointing, since type equalities will be needlessly large:
3986 $\myprdec{\myjm{\mytya}{\mytyp_l}{\mytyb}{\mytyp_l}} : \mytyp_{l + 1}$.
3988 However, considering that our theory is cumulative, we can do better.
3989 Assuming rules for $\myprop$ cumulativity similar to the ones for
3990 $\mytyp$, we will have (with the conversion rule reproduced as a
3994 \AxiomC{$\myctx \vdash \mytya \mycumul \mytyb$}
3995 \AxiomC{$\myjud{\mytmt}{\mytya}$}
3996 \BinaryInfC{$\myjud{\mytmt}{\mytyb}$}
3999 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
4000 \AxiomC{$\myjud{\mytyb}{\mytyp_l}$}
4001 \BinaryInfC{$\myjud{\myjm{\mytya}{\mytyp_{l}}{\mytyb}{\mytyp_{l}}}{\myprop_l}$}
4007 \AxiomC{$\myjud{\mytmm}{\mytya}$}
4008 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
4009 \AxiomC{$\myjud{\mytmn}{\mytyb}$}
4010 \AxiomC{$\myjud{\mytyb}{\mytyp_l}$}
4011 \AxiomC{$\mytya$ and $\mytyb$ are not $\mytyp_{l'}$}
4012 \QuinaryInfC{$\myjud{\myjm{\mytmm}{\mytya}{\mytmm}{\mytya}}{\myprop_l}$}
4016 That is, we are small when we can (type equalities) and large otherwise.
4017 This would not work in a non-cumulative theory because subject reduction
4018 would not hold. Consider for instance
4020 \myjm{\mynat}{\myITE{\mytrue}{\mytyp_0}{\mytyp_0}}{\mybool}{\myITE{\mytrue}{\mytyp_0}{\mytyp_0}}
4024 \[\myjm{\mynat}{\mytyp_0}{\mybool}{\mytyp_0} : \myprop_0 \]
4025 We need members of $\myprop_0$ to be members of $\myprop_1$ too, which
4026 will be the case with cumulativity. This buys us a cheap type level
4027 equality without having to replicate functionality with a dedicated
4030 \subsubsection{Quotation and definitional equality}
4031 \label{sec:kant-irr}
4033 Now we can give an account of definitional equality, by explaining how
4034 to perform quotation (as defined in Section \ref{sec:eta-expand})
4035 towards the goal described in Section \ref{sec:ott-quot}.
4039 \item Perform $\eta$-expansion on functions and records.
4041 \item As a consequence of the previous point, identify all records with
4042 no projections as equal, since they will have only one element.
4044 \item Identify all members of types with no constructors (and thus no
4047 \item Identify all equivalent proofs as equal---with `equivalent proof'
4048 we mean those proving the same propositions.
4050 \item Advance coercions working across definitionally equal types.
4052 Towards these goals and following the intuition between bidirectional
4053 type checking we define two mutually recursive functions, one quoting
4054 canonical terms against their types (since we need the type to type check
4055 canonical terms), one quoting neutral terms while recovering their
4057 \begin{mydef}[Quotation for \mykant]
4058 The full procedure for quotation is shown in Figure
4059 \ref{fig:kant-quot}.
4061 We $\boxed{\text{box}}$ the neutral proofs and
4062 neutral members of empty types, following the notation in
4063 \cite{Altenkirch2007}, and we make use of $\mydefeq_{\mybox}$ which
4064 compares terms syntactically up to $\alpha$-renaming, but also up to
4065 equivalent proofs: we consider all boxed content as equal.
4067 Our quotation will work on normalised terms, so that all defined values
4068 will have been replaced. Moreover, we match on data type eliminators
4069 and all their arguments, so that $\mynat.\myfun{elim} \myappsp \mytmm
4070 \myappsp \myse{P} \myappsp \vec{\mytmn}$ will stand for
4071 $\mynat.\myfun{elim}$ applied to the scrutinised $\mynat$, the
4072 predicate, and the two cases. This measure can be easily implemented by
4073 checking the head of applications and `consuming' the needed terms.
4074 Thus, we gain proof irrelevance, and not only for a more useful
4075 definitional equality, but also for example to eliminate all
4076 propositional content when compiling.
4079 \mydesc{canonical quotation:}{\mycanquot(\myctx, \mytmsyn : \mytmsyn) \mymetagoes \mytmsyn}{
4082 \begin{array}{@{}l@{}l}
4083 \mycanquot(\myctx,\ \mytmt : \mytyc{D} \myappsp \vec{A} &) \mymetaguard \mymeta{empty}(\myctx, \mytyc{D}) \mymetagoes \boxed{\mytmt} \\
4084 \mycanquot(\myctx,\ \mytmt : \mytyc{D} \myappsp \vec{A} &) \mymetaguard \mymeta{record}(\myctx, \mytyc{D}) \mymetagoes
4085 \mytyc{D}.\mydc{constr} \myappsp \cdots \myappsp \mycanquot(\myctx, \mytyc{D}.\myfun{f}_n : (\myctx(\mytyc{D}.\myfun{f}_n))(\vec{A};\mytmt)) \\
4086 \mycanquot(\myctx,\ \mytyc{D}.\mydc{c} \myappsp \vec{t} : \mytyc{D} \myappsp \vec{A} &) \mymetagoes \cdots \\
4087 \mycanquot(\myctx,\ \myse{f} : \myfora{\myb{x}}{\mytya}{\mytyb} &) \mymetagoes \myabs{\myb{x}}{\mycanquot(\myctx; \myb{x} : \mytya, \myapp{\myse{f}}{\myb{x}} : \mytyb)} \\
4088 \mycanquot(\myctx,\ \myse{p} : \myprdec{\myse{P}} &) \mymetagoes \boxed{\myse{p}}
4090 \mycanquot(\myctx,\ \mytmt : \mytya &) \mymetagoes \mytmt'\ \text{\textbf{where}}\ \mytmt' : \myarg = \myneuquot(\myctx, \mytmt)
4097 \mydesc{neutral quotation:}{\myneuquot(\myctx, \mytmsyn) \mymetagoes \mytmsyn : \mytmsyn}{
4100 \begin{array}{@{}l@{}l}
4101 \myneuquot(\myctx,\ \myb{x} &) \mymetagoes \myb{x} : \myctx(\myb{x}) \\
4102 \myneuquot(\myctx,\ \mytyp &) \mymetagoes \mytyp : \mytyp \\
4103 \myneuquot(\myctx,\ \myfora{\myb{x}}{\mytya}{\mytyb} & ) \mymetagoes
4104 \myfora{\myb{x}}{\myneuquot(\myctx, \mytya)}{\myneuquot(\myctx; \myb{x} : \mytya, \mytyb)} : \mytyp \\
4105 \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 \\
4106 \myneuquot(\myctx,\ \myprdec{\myjm{\mytmm}{\mytya}{\mytmn}{\mytyb}} &) \mymetagoes \\
4107 \multicolumn{2}{l}{\myind{2}\myprdec{\myjm{\mycanquot(\myctx, \mytmm : \mytya)}{\mytya'}{\mycanquot(\myctx, \mytmn : \mytyb)}{\mytyb'}} : \mytyp} \\
4108 \multicolumn{2}{@{}l}{\myind{2}\text{\textbf{where}}\ \mytya' : \myarg = \myneuquot(\myctx, \mytya)} \\
4109 \multicolumn{2}{@{}l}{\myind{2}\phantom{\text{\textbf{where}}}\ \mytyb' : \myarg = \myneuquot(\myctx, \mytyb)} \\
4110 \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) \\
4111 \multicolumn{2}{@{}l}{\myind{2}\text{\textbf{where}}\ \mytmt' : \mytyc{D} \myappsp \vec{A} = \myneuquot(\myctx, \mytmt)} \\
4112 \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 \\
4113 \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\\
4114 \multicolumn{2}{@{}l}{\myind{2}\text{\textbf{where}}\ \mytmm' : \mytyc{D} \myappsp \vec{A} = \myneuquot(\myctx, \mytmm)} \\
4115 \myneuquot(\myctx,\ \myapp{\myse{f}}{\mytmt} &) \mymetagoes \myapp{\myse{f'}}{\mycanquot(\myctx, \mytmt : \mytya)} : \mysub{\mytyb}{\myb{x}}{\mytmt} \\
4116 \multicolumn{2}{@{}l}{\myind{2}\text{\textbf{where}}\ \myse{f'} : \myfora{\myb{x}}{\mytya}{\mytyb} = \myneuquot(\myctx, \myse{f})} \\
4117 \myneuquot(\myctx,\ \mycoee{\mytya}{\mytyb}{\myse{Q}}{\mytmt} &) \mymetaguard \myneuquot(\myctx, \mytya) \mydefeq_{\mybox} \myneuquot(\myctx, \mytyb) \mymetagoes \myneuquot(\myctx, \mytmt) \\
4118 \myneuquot(\myctx,\ \mycoee{\mytya}{\mytyb}{\myse{Q}}{\mytmt} &) \mymetagoes
4119 \mycoee{\myneuquot(\myctx, \mytya)}{\myneuquot(\myctx, \mytyb)}{\boxed{\myse{Q}}}{\myneuquot(\myctx, \mytmt)}
4123 \caption{Quotation in \mykant. Along the already used
4124 $\mymeta{record}$ meta-operation on the context we make use of
4125 $\mymeta{empty}$, which checks if a certain type constructor has
4126 zero data constructor. The `data constructor' cases for non-record,
4127 non-empty, data types are omitted for brevity.}
4128 \label{fig:kant-quot}
4131 \subsubsection{Why $\myprop$?}
4133 It is worth to ask if $\myprop$ is needed at all. It is perfectly
4134 possible to have the type checker identify propositional types
4135 automatically, and in fact in some sense we already do during equality
4136 reduction and quotation. However, this has the considerable
4137 disadvantage that we can never identify abstracted
4138 variables\footnote{And in general neutral terms, although we currently
4139 do not have neutral propositions apart from equalities on neutral
4140 terms.} of type $\mytyp$ as $\myprop$, thus forbidding the user to
4141 talk about $\myprop$ explicitly.
4143 This is a considerable impediment, for example when implementing
4144 \emph{quotient types}. With quotients, we let the user specify an
4145 equivalence class over a certain type, and then exploit this in various
4146 way---crucially, we need to be sure that the equivalence given is
4147 propositional, a fact which prevented the use of quotients in dependent
4148 type theories \citep{Jacobs1994}.
4150 \section{\mykant : the practice}
4151 \label{sec:kant-practice}
4153 \epigraph{\emph{It's alive!}}{Henry Frankenstein}
4155 The codebase consists of around 2500 lines of Haskell,\footnote{The full
4156 source code is available under the GPL3 license at
4157 \url{https://github.com/bitonic/kant}. `Kant' was a previous
4158 incarnation of the software, and the name remained.} as reported by
4159 the \texttt{cloc} utility.
4161 We implement the type theory as described in Section
4162 \ref{sec:kant-theory}. The author learnt the hard way the
4163 implementation challenges for such a project, and ran out of time while
4164 implementing observational equality. While the constructs and typing
4165 rules are present, the machinery to make it happen (equality reduction,
4166 coercions, quotation, etc.) is not present yet.
4168 This considered, everything else presented in Section
4169 \ref{sec:kant-theory} is implemented and working well---and in fact all
4170 the examples presented in this thesis, apart from the ones that are
4171 equality related, have been encoded in \mykant\ in the Appendix.
4172 Moreover, given the detailed plan in the previous section, finishing off
4173 should not prove too much work.
4175 The interaction with the user takes place in a loop living in and
4176 updating a context of \mykant\ declarations, which presents itself as in
4177 Figure \ref{fig:kant-web}. Files with lists of declarations can also be
4178 loaded. The REPL is a available both as a command-line application and in
4179 a web interface, which is available at \url{bertus.mazzo.li}.
4181 A REPL cycle starts with the user inputting a \mykant\
4182 declaration or another REPL command, which then goes through various
4183 stages that can end up in a context update, or in failures of various
4184 kind. The process is described diagrammatically in figure
4185 \ref{fig:kant-process}.
4188 {\small\begin{Verbatim}[frame=leftline,xleftmargin=3cm]
4190 Version 0.0, made in London, year 2013.
4192 <decl> Declare value/data type/record
4195 :p <term> Pretty print
4197 :r <file> Reload file (erases previous environment)
4198 :i <name> Info about an identifier
4200 >>> :l data/samples/good/common.ka
4202 >>> :e plus three two
4203 suc (suc (suc (suc (suc zero))))
4204 >>> :t plus three two
4209 \caption{A sample run of the \mykant\ prompt.}
4210 \label{fig:kant-web}
4216 \item[Parse] In this phase the text input gets converted to a sugared
4217 version of the core language. For example, we accept multiple
4218 arguments in arrow types and abstractions, and we represent variables
4219 with names, while as we will see in Section \ref{sec:term-repr} the
4220 final term types uses a \emph{nameless} representation.
4222 \item[Desugar] The sugared declaration is converted to a core term.
4223 Most notably we go from names to nameless.
4225 \item[ConDestr] Short for `Constructors/Destructors', converts
4226 applications of data destructors and constructors to a special form,
4227 to perform bidirectional type checking.
4229 \item[Reference] Occurrences of $\mytyp$ get decorated by a unique reference,
4230 which is necessary to implement the type hierarchy check.
4232 \item[Elaborate/Typecheck/Evaluate] \textbf{Elaboration} converts the
4233 declaration to some context items, which might be a value declaration
4234 (type and body) or a data type declaration (constructors and
4235 destructors). This phase works in tandem with \textbf{Type checking},
4236 which in turns needs to \textbf{Evaluate} terms.
4238 \item[Distill] and report the result. `Distilling' refers to the
4239 process of converting a core term back to a sugared version that we
4240 can show to the user. This can be necessary both to display errors
4241 including terms or to display result of evaluations or type checking
4242 that the user has requested. Among the other things in this stage we
4243 go from nameless back to names by recycling the names that the user
4244 used originally, as to fabricate a term which is as close as possible
4245 to what it originated from.
4247 \item[Pretty print] Format the terms in a nice way, and display them to
4254 \tikzstyle{block} = [rectangle, draw, text width=5em, text centered, rounded
4255 corners, minimum height=2.5em, node distance=0.7cm]
4257 \tikzstyle{decision} = [diamond, draw, text width=4.5em, text badly
4258 centered, inner sep=0pt, node distance=0.7cm]
4260 \tikzstyle{line} = [draw, -latex']
4262 \tikzstyle{cloud} = [draw, ellipse, minimum height=2em, text width=5em, text
4263 centered, node distance=1.5cm]
4266 \begin{tikzpicture}[auto]
4267 \node [cloud] (user) {User};
4268 \node [block, below left=1cm and 0.1cm of user] (parse) {Parse};
4269 \node [block, below=of parse] (desugar) {Desugar};
4270 \node [block, below=of desugar] (condestr) {ConDestr};
4271 \node [block, below=of condestr] (reference) {Reference};
4272 \node [block, below=of reference] (elaborate) {Elaborate};
4273 \node [block, left=of elaborate] (tycheck) {Typecheck};
4274 \node [block, left=of tycheck] (evaluate) {Evaluate};
4275 \node [decision, right=of elaborate] (error) {Error?};
4276 \node [block, right=of parse] (pretty) {Pretty print};
4277 \node [block, below=of pretty] (distill) {Distill};
4278 \node [block, below=of distill] (update) {Update context};
4280 \path [line] (user) -- (parse);
4281 \path [line] (parse) -- (desugar);
4282 \path [line] (desugar) -- (condestr);
4283 \path [line] (condestr) -- (reference);
4284 \path [line] (reference) -- (elaborate);
4285 \path [line] (elaborate) edge[bend right] (tycheck);
4286 \path [line] (tycheck) edge[bend right] (elaborate);
4287 \path [line] (elaborate) -- (error);
4288 \path [line] (error) edge[out=0,in=0] node [near start] {yes} (distill);
4289 \path [line] (error) -- node [near start] {no} (update);
4290 \path [line] (update) -- (distill);
4291 \path [line] (pretty) -- (user);
4292 \path [line] (distill) -- (pretty);
4293 \path [line] (tycheck) edge[bend right] (evaluate);
4294 \path [line] (evaluate) edge[bend right] (tycheck);
4297 \caption{High level overview of the life of a \mykant\ prompt cycle.}
4298 \label{fig:kant-process}
4301 Here we will review only a sampling of the more interesting
4302 implementation challenges present when implementing an interactive
4308 The syntax of \mykant\ is presented in Figure \ref{fig:syntax}.
4309 Examples showing the usage of most of the constructs---excluding the
4310 OTT-related ones---are present in Appendices \ref{app:kant-itt},
4311 \ref{app:kant-examples}, and \ref{app:hurkens}; plus a tutorial in
4312 Section \ref{sec:type-holes}. The syntax has grown organically with the
4313 needs of the language, and thus is not very sophisticated. The grammar
4314 is specified in and processed by the \texttt{happy} parser generator for
4315 Haskell.\footnote{Available at \url{http://www.haskell.org/happy}.}
4316 Tokenisation is performed by a simple hand written lexer.
4321 \begin{array}{@{\ \ }l@{\ }c@{\ }l}
4322 \multicolumn{3}{@{}l}{\text{A name, in regexp notation.}} \\
4323 \mysee{name} & ::= & \texttt{[a-zA-Z] [a-zA-Z0-9'\_-]*} \\
4324 \multicolumn{3}{@{}l}{\text{A binder might or might not (\texttt{\_}) bind a name.}} \\
4325 \mysee{binder} & ::= & \mytermi{\_} \mysynsep \mysee{name} \\
4326 \multicolumn{3}{@{}l}{\text{A series of typed bindings.}} \\
4327 \mysee{telescope}\, \ \ \ & ::= & (\mytermi{[}\ \mysee{binder}\ \mytermi{:}\ \mysee{term}\ \mytermi{]}){*} \\
4328 \multicolumn{3}{@{}l}{\text{Terms, including propositions.}} \\
4329 \multicolumn{3}{@{}l}{
4330 \begin{array}{@{\ \ }l@{\ }c@{\ }l@{\ \ \ \ \ }l}
4331 \mysee{term} & ::= & \mysee{name} & \text{A variable.} \\
4332 & | & \mytermi{*} & \text{\mytyc{Type}.} \\
4333 & | & \mytermi{\{|}\ \mysee{term}{*}\ \mytermi{|\}} & \text{Type holes.} \\
4334 & | & \mytermi{Prop} & \text{\mytyc{Prop}.} \\
4335 & | & \mytermi{Top} \mysynsep \mytermi{Bot} & \text{$\mytop$ and $\mybot$.} \\
4336 & | & \mysee{term}\ \mytermi{/\textbackslash}\ \mysee{term} & \text{Conjuctions.} \\
4337 & | & \mytermi{[|}\ \mysee{term}\ \mytermi{|]} & \text{Proposition decoding.} \\
4338 & | & \mytermi{coe}\ \mysee{term}\ \mysee{term}\ \mysee{term}\ \mysee{term} & \text{Coercion.} \\
4339 & | & \mytermi{coh}\ \mysee{term}\ \mysee{term}\ \mysee{term}\ \mysee{term} & \text{Coherence.} \\
4340 & | & \mytermi{(}\ \mysee{term}\ \mytermi{:}\ \mysee{term}\ \mytermi{)}\ \mytermi{=}\ \mytermi{(}\ \mysee{term}\ \mytermi{:}\ \mysee{term}\ \mytermi{)} & \text{Heterogeneous equality.} \\
4341 & | & \mytermi{(}\ \mysee{compound}\ \mytermi{)} & \text{Parenthesised term.} \\
4342 \mysee{compound} & ::= & \mytermi{\textbackslash}\ \mysee{binder}{*}\ \mytermi{=>}\ \mysee{term} & \text{Untyped abstraction.} \\
4343 & | & \mytermi{\textbackslash}\ \mysee{telescope}\ \mytermi{:}\ \mysee{term}\ \mytermi{=>}\ \mysee{term} & \text{Typed abstraction.} \\
4344 & | & \mytermi{forall}\ \mysee{telescope}\ \mysee{term} & \text{Universal quantification.} \\
4345 & | & \mysee{arr} \\
4346 \mysee{arr} & ::= & \mysee{telescope}\ \mytermi{->}\ \mysee{arr} & \text{Dependent function.} \\
4347 & | & \mysee{term}\ \mytermi{->}\ \mysee{arr} & \text{Non-dependent function.} \\
4348 & | & \mysee{term}{+} & \text {Application.}
4351 \multicolumn{3}{@{}l}{\text{Typed names.}} \\
4352 \mysee{typed} & ::= & \mysee{name}\ \mytermi{:}\ \mysee{term} \\
4353 \multicolumn{3}{@{}l}{\text{Declarations.}} \\
4354 \mysee{decl}& ::= & \mysee{value} \mysynsep \mysee{abstract} \mysynsep \mysee{data} \mysynsep \mysee{record} \\
4355 \multicolumn{3}{@{}l}{\text{Defined values. The telescope specifies named arguments.}} \\
4356 \mysee{value} & ::= & \mysee{name}\ \mysee{telescope}\ \mytermi{:}\ \mysee{term}\ \mytermi{=>}\ \mysee{term} \\
4357 \multicolumn{3}{@{}l}{\text{Abstracted variables.}} \\
4358 \mysee{abstract} & ::= & \mytermi{postulate}\ \mysee{typed} \\
4359 \multicolumn{3}{@{}l}{\text{Data types, and their constructors.}} \\
4360 \mysee{data} & ::= & \mytermi{data}\ \mysee{name}\ \mytermi{:}\ \mysee{telescope}\ \mytermi{->}\ \mytermi{*}\ \mytermi{=>}\ \mytermi{\{}\ \mysee{constrs}\ \mytermi{\}} \\
4361 \mysee{constrs} & ::= & \mysee{typed} \\
4362 & | & \mysee{typed}\ \mytermi{|}\ \mysee{constrs} \\
4363 \multicolumn{3}{@{}l}{\text{Records, and their projections. The $\mysee{name}$ before the projections is the constructor name.}} \\
4364 \mysee{record} & ::= & \mytermi{record}\ \mysee{name}\ \mytermi{:}\ \mysee{telescope}\ \mytermi{->}\ \mytermi{*}\ \mytermi{=>}\ \mysee{name}\ \mytermi{\{}\ \mysee{projs}\ \mytermi{\}} \\
4365 \mysee{projs} & ::= & \mysee{typed} \\
4366 & | & \mysee{typed}\ \mytermi{,}\ \mysee{projs}
4370 \caption{\mykant' syntax. The non-terminals are marked with
4371 $\langle\text{angle brackets}\rangle$ for greater clarity. The
4372 syntax in the implementation is actually more liberal, for example
4373 giving the possibility of using arrow types directly in
4374 constructor/projection declarations.\\
4375 Additionally, we give the user the possibility of using Unicode
4376 characters instead of their ASCII counterparts, e.g. \texttt{→} in
4377 place of \texttt{->}, \texttt{λ} in place of
4378 \texttt{\textbackslash}, etc.}
4382 \subsection{Term representation}
4383 \label{sec:term-repr}
4385 \subsubsection{Naming and substituting}
4387 Perhaps surprisingly, one of the most difficult challenges in
4388 implementing a theory of the kind presented is choosing a good data type
4389 for terms, and specifically handling substitutions in a sane way.
4391 There are two broad schools of thought when it comes to naming
4392 variables, and thus substituting:
4394 \item[Nameful] Bound variables are represented by some enumerable data
4395 type, just as we have described up to now, starting from Section
4396 \ref{sec:untyped}. The problem is that avoiding name capturing is a
4397 nightmare, both in the sense that it is not performant---given that we
4398 need to rename rename substitute each time we `enter' a binder---but
4399 most importantly given the fact that in even slightly more complicated
4400 systems it is very hard to get right, even for experts.
4402 One of the sore spots of explicit names is comparing terms up to
4403 $\alpha$-renaming, which again generates a huge amounts of
4404 substitutions and requires special care.
4406 \item[Nameless] We can capture the relationship between variables and
4407 their binders, by getting rid of names altogether, and representing
4408 bound variables with an index referring to the `binding' structure, a
4409 notion introduced by \cite{de1972lambda}. Usually $0$ represents the
4410 variable bound by the innermost binding structure, $1$ the
4411 second-innermost, and so on. For instance with simple abstractions we
4415 \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} \\
4416 \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
4420 While this technique is obviously terrible in terms of human
4421 usability,\footnote{With some people going as far as defining it akin
4422 to an inverse Turing test.} it is much more convenient as an
4423 internal representation to deal with terms mechanically---at least in
4424 simple cases. $\alpha$-renaming ceases to be an issue, and
4425 term comparison is purely syntactical.
4427 Nonetheless, more complex constructs such as pattern matching put
4428 some strain on the indices and many systems end up using explicit
4433 In the past decade or so advancements in the Haskell's type system and
4434 in general the spread new programming practices have made the nameless
4435 option much more amenable. \mykant\ thus takes the nameless path
4436 through the use of Edward Kmett's excellent \texttt{bound}
4437 library.\footnote{Available at
4438 \url{http://hackage.haskell.org/package/bound}.} We describe the
4439 advantages of \texttt{bound}'s approach, but also its pitfalls in the
4440 previously relatively unknown territory of dependent
4441 types---\texttt{bound} being created mostly to handle more simply typed
4444 \texttt{bound} builds on the work of \cite{Bird1999}, who suggested to
4445 parametrising the term type over the type of the variables, and `nest'
4446 the type each time we enter a scope. If we wanted to define a term
4447 for the untyped $\lambda$-calculus, we might have
4449 -- A type with no members.
4452 data Var v = Bound | Free v
4455 = V v -- Bound variable
4456 | App (Tm v) (Tm v) -- Term application
4457 | Lam (Tm (Var v)) -- Abstraction
4459 Closed terms would be of type \texttt{Tm Empty}, so that there would be
4460 no occurrences of \texttt{V}. However, inside an abstraction, we can
4461 have \texttt{V Bound}, representing the bound variable, and inside a
4462 second abstraction we can have \texttt{V Bound} or \texttt{V (Free
4463 Bound)}. Thus the term
4464 \[\myabs{\myb{x}}{\myabs{\myb{y}}{\myb{x}}}\]
4465 can be represented as
4467 -- The top level term is of type `Tm Empty'.
4468 -- The inner term `Lam (Free Bound)' is of type `Tm (Var Empty)'.
4469 -- The second inner term `V (Free Bound)' is of type `Tm (Var (Var
4471 Lam (Lam (V (Free Bound)))
4473 This allows us to reflect the `nestedness' of a type at the type level,
4474 and since we usually work with functions polymorphic on the parameter
4475 \texttt{v} it's very hard to make mistakes by putting terms of the wrong
4476 nestedness where they do not belong.
4478 Even more interestingly, the substitution operation is perfectly
4479 captured by the \verb|>>=| (bind) operator of the \texttt{Monad}
4484 (>>=) :: m a -> (a -> m b) -> m b
4486 instance Monad Tm where
4487 -- `return'ing turns a variable into a `Tm'
4490 -- `t >>= f' takes a term `t' and a mapping from variables to terms
4491 -- `f' and applies `f' to all the variables in `t', replacing them
4492 -- with the mapped terms.
4494 App m n >>= f = App (m >>= f) (n >>= f)
4496 -- `Lam' is the tricky case: we modify the function to work with bound
4497 -- variables, so that if it encounters `Bound' it leaves it untouched
4498 -- (since the mapping refers to the outer scope); if it encounters a
4499 -- free variable it asks `f' for the term and then updates all the
4500 -- variables to make them refer to the outer scope they were meant to
4502 Lam s >>= f = Lam (s >>= bump)
4503 where bump Bound = return Bound
4504 bump (Free v) = f v >>= V . Free
4506 With this in mind, we can define functions which will not only work on
4507 \verb|Tm|, but on any \verb|Monad|!
4509 -- Replaces free variable `v' with `m' in `n'.
4510 subst :: (Eq v, Monad m) => v -> m v -> m v -> m v
4511 subst v m n = n >>= \v' -> if v == v' then m else return v'
4513 -- Replace the variable bound by `s' with term `t'.
4514 inst :: Monad m => m v -> m (Var v) -> m v
4515 inst t s = s >>= \v -> case v of
4517 Free v' -> return v'
4519 The beauty of this technique is that with a few simple functions we have
4520 defined all the core operations in a general and `obviously correct'
4521 way, with the extra confidence of having the type checker looking our
4522 back. For what concerns term equality, we can just ask the H Haskell
4523 compiler to derive the instance for the \verb|Eq| type class and since
4524 we are nameless that will be enough (modulo fancy quotation).
4526 Moreover, if we take the top level term type to be \verb|Tm String|, we
4527 get a representation of terms with top-level definitions; where closed
4528 terms contain only \verb|String| references to said definitions---see
4529 also \cite{McBride2004b}.
4531 What are then the pitfalls of this seemingly invincible technique? The
4532 most obvious impediment is the need for polymorphic recursion.
4533 Functions traversing terms parameterized by the variable type will have
4536 -- Infer the type of a term, or return an error.
4537 infer :: Tm v -> Either Error (Tm v)
4539 When traversing under a \verb|Scope| the parameter changes from \verb|v|
4540 to \verb|Var v|, and thus if we do not specify the type for our function explicitly
4541 inference will fail---type inference for polymorphic recursion being
4542 undecidable \citep{henglein1993type}. This causes some annoyance,
4543 especially in the presence of many local definitions that we would like
4546 But the real issue is the fact that giving a type parameterized over a
4547 variable---say \verb|m v|---a \verb|Monad| instance means being able to
4548 only substitute variables for values of type \verb|m v|. This is a
4549 considerable inconvenience. Consider for instance the case of
4550 telescopes, which are a central tool to deal with contexts and other
4551 constructs. In Haskell we can give them a faithful representation
4552 with a data type along the lines of
4554 data Tele m v = Empty (m v) | Bind (m v) (Tele m (Var v))
4555 type TeleTm = Tele Tm
4557 The problem here is that what we want to substitute for variables in
4558 \verb|Tele m v| is \verb|m v| (probably \verb|Tm v|), not \verb|Tele m v| itself! What we need is
4560 bindTele :: Monad m => Tele m a -> (a -> m b) -> Tele m b
4561 substTele :: (Eq v, Monad m) => v -> m v -> Tele m v -> Tele m v
4562 instTele :: Monad m => m v -> Tele m (Var v) -> Tele m v
4564 Not what \verb|Monad| gives us. Solving this issue in an elegant way
4565 has been a major sink of time and source of headaches for the author,
4566 who analysed some of the alternatives---most notably the work by
4567 \cite{weirich2011binders}---but found it impossible to give up the
4568 simplicity of the model above.
4570 That said, our term type is still reasonably brief, as shown in full in
4571 Appendix \ref{app:termrep}. The fact that propositions cannot be
4572 factored out in another data type is an instance of the problem
4573 described above. However the real pain is during elaboration, where we
4574 are forced to treat everything as a type while we would much rather have
4575 telescopes. Future work would include writing a library that marries
4576 more flexibility with a nice interface similar to the one of
4579 We also make use of a `forgetful' data type (as provided by
4580 \verb|bound|) to store user-provided variables names along with the
4581 `nameless' representation, so that the names will not be considered when
4582 compared terms, but will be available when distilling so that we can
4583 recover variable names that are as close as possible to what the user
4586 \subsubsection{Evaluation}
4588 Another source of contention related to term representation is dealing
4589 with evaluation. Here \mykant\ does not make bold moves, and simply
4590 employs substitution. When type checking we match types by reducing
4591 them to their weak head normal form, as to avoid unnecessary evaluation.
4593 We treat data types eliminators and record projections in an uniform
4594 way, by elaborating declarations in a series of \emph{rewriting rules}:
4598 Tm v -> -- Term to which the destructor is applied
4599 [Tm v] -> -- List of other arguments
4600 -- The result of the rewriting, if the eliminator reduces.
4603 A rewriting rule is polymorphic in the variable type, guaranteeing that
4604 it just pattern matches on terms structure and rearranges them in some
4605 way, and making it possible to apply it at any level in the term. When
4606 reducing a series of applications we match the first term and check if
4607 it is a destructor, and if that's the case we apply the reduction rule
4608 and reduce further if it yields a new list of terms.
4610 This has the advantage of simplicity, at the expense of being quite poor
4611 in terms of performance and that we need to do quotation manually. An
4612 alternative that solves both of these is the already mentioned
4613 \emph{normalisation by evaluation}, where we would compute by turning
4614 terms into Haskell values, and then reify back to terms to compare
4615 them---a useful tutorial on this technique is given by \cite{Loh2010}.
4617 However, quotation has its disadvantages. The most obvious one is that
4618 it is less simple: we need to set up some infrastructure to handle the
4619 quotation and reification, while with substitution we have a uniform
4620 representation through the process of type checking. The second is that
4621 performance advantages can be rendered less effective by the continuous
4622 quoting and reifying, although this can probably be mitigated with some
4625 \subsubsection{Parameterize everything!}
4628 Through the life of a REPL cycle we need to execute two broad
4629 `effectful' actions:
4631 \item Retrieve, add, and modify elements to an environment. The
4632 environment will contain not only types, but also the rewriting rules
4633 presented in the previous section, and a counter to generate fresh
4634 references for the type hierarchy.
4636 \item Throw various kinds of errors when something goes wrong: parsing,
4637 type checking, input/output error when reading files, and more.
4639 Haskell taught us the value of monads in programming languages, and in
4640 \mykant\ we keep this lesson in mind. All of the plumbing required to do
4641 the two actions above is provided by a very general \emph{monad
4642 transformer} that we use through the codebase, \texttt{KMonadT}:
4644 newtype KMonad f v m a = KMonad (StateT (f v) (ErrorT KError m) a)
4652 Without delving into the details of what a monad transformer
4654 \url{https://en.wikibooks.org/wiki/Haskell/Monad_transformers.}} this
4655 is what \texttt{KMonadT} works with and provides:
4657 \item The \verb|v| parameter represents the parameterized variable for
4658 the term type that we spoke about at the beginning of this section.
4661 \item The \verb|f| parameter indicates what kind of environment we are
4662 holding. Sometimes we want to traverse terms without carrying the
4663 entire environment, for various reasons---\texttt{KMonatT} lets us do
4664 that. Note that \verb|f| is itself parameterized over \verb|v|. The
4665 inner \verb|StateT| monad transformer lets us retrieve and modify this
4666 environment at any time.
4668 \item The \verb|m| is the `inner' monad that we can `plug in' to be able
4669 to perform more effectful actions in \texttt{KMonatT}. For example if we
4670 plug the \texttt{IO} monad in, we will be able to do input/output.
4672 \item The inner \verb|ErrorT| lets us throw errors at any time. The
4673 error type is \verb|KError|, which describes all the possible errors
4674 that a \mykant\ process can throw.
4676 \item Finally, the \verb|a| parameter represents the return type of the
4677 computation we are executing.
4680 The clever trick in \texttt{KMonadT} is to have it to be parametrised
4681 over the same type as the term type. This way, we can easily carry the
4682 environment while traversing under binders. For example, if we only
4683 needed to carry types of bound variables in the environment, we can
4684 quickly set up the following infrastructure:
4688 -- A context is a mapping from variables to types.
4689 newtype Ctx v = Ctx (v -> Tm v)
4691 -- A context monad holds a context.
4692 type CtxMonad v m = KMonadT Ctx v m
4694 -- Enter into a scope binding a type to the variable, execute a
4695 -- computation there, and return exit the scope returning to the `current'
4697 nestM :: Monad m => Tm v -> CtxMonad (Var v) m a -> CtxMonad v m a
4700 Again, the types guard our back guaranteeing that we add a type when we
4701 enter a scope, and we discharge it when we get out. The author
4702 originally started with a more traditional representation and often
4703 forgot to add the right variable at the right moment. Using this
4704 practices it is very difficult to do so---we achieve correctness through
4707 In the actual \mykant\ codebase, we have also abstracted the concept of
4708 `context' further, so that we can easily embed contexts into other
4709 structures and write generic operations on all context-like
4710 structures.\footnote{See the \texttt{Kant.Cursor} module for details.}
4712 \subsection{Turning a hierarchy into some graphs}
4713 \label{sec:hier-impl}
4715 In this section we will explain how to implement the typical ambiguity
4716 we have spoken about in \ref{sec:term-hierarchy} efficiently, a subject
4717 which is often dismissed in the literature. As mentioned, we have to
4718 verify a the consistency of a set of constraints each time we add a new
4719 one. The constraints range over some set of variables whose members we
4720 will denote with $x, y, z, \dots$. and are of two kinds:
4727 Predictably, $\le$ expresses a reflexive order, and $<$ expresses an
4728 irreflexive order, both working with the same notion of equality, where
4729 $x < y$ implies $x \le y$---they behave like $\le$ and $<$ do for natural
4730 numbers (or in our case, levels in a type hierarchy). We also need an
4731 equality constraint ($x = y$), which can be reduced to two constraints
4732 $x \le y$ and $y \le x$.
4734 Given this specification, we have implemented a standalone Haskell
4735 module---that we plan to release as a library---to efficiently store and
4736 check the consistency of constraints. The problem predictably reduces
4737 to a graph algorithm, and for this reason we also implement a library
4738 for labelled graphs, since the existing Haskell graph libraries fell
4739 short in different areas.\footnote{We tried the \texttt{Data.Graph}
4740 module in \url{http://hackage.haskell.org/package/containers}, and the
4741 much more featureful \texttt{fgl} library
4742 \url{http://hackage.haskell.org/package/fgl}.} The interfaces for
4743 these modules are shown in Appendix \ref{app:constraint}. The graph
4744 library is implemented as a modification of the code described by
4747 We represent the set by building a graph where vertices are variables,
4748 and edges are constraints between them, labelled with the appropriate
4749 constraint: $x < y$ gives rise to a $<$-labelled edge from $x$ to $y$,
4750 and $x \le y$ to a $\le$-labelled edge from $x$ to $y$. As we add
4751 constraints, $\le$ constraints are replaced by $<$ constraints, so that
4752 if we started with an empty set and added
4754 x < y,\ y \le z,\ z \le k,\ k < j,\ j \le y\
4756 it would generate the graph shown in Figure \ref{fig:graph-one-before},
4757 but adding $z < k$ would strengthen the edge from $z$ to $k$, as shown
4758 in \ref{fig:graph-one-after}.
4762 \begin{subfigure}[b]{0.3\textwidth}
4763 \begin{tikzpicture}[node distance=1.5cm]
4766 \node [right of=x] (y) {$y$};
4767 \node [right of=y] (z) {$z$};
4768 \node [below of=z] (k) {$k$};
4769 \node [left of=k] (j) {$j$};
4772 (x) edge node [above] {$<$} (y)
4773 (y) edge node [above] {$\le$} (z)
4774 (z) edge node [right] {$\le$} (k)
4775 (k) edge node [below] {$\le$} (j)
4776 (j) edge node [left ] {$\le$} (y);
4778 \caption{Before $z < k$.}
4779 \label{fig:graph-one-before}
4782 \begin{subfigure}[b]{0.3\textwidth}
4783 \begin{tikzpicture}[node distance=1.5cm]
4786 \node [right of=x] (y) {$y$};
4787 \node [right of=y] (z) {$z$};
4788 \node [below of=z] (k) {$k$};
4789 \node [left of=k] (j) {$j$};
4792 (x) edge node [above] {$<$} (y)
4793 (y) edge node [above] {$\le$} (z)
4794 (z) edge node [right] {$<$} (k)
4795 (k) edge node [below] {$\le$} (j)
4796 (j) edge node [left ] {$\le$} (y);
4798 \caption{After $z < k$.}
4799 \label{fig:graph-one-after}
4802 \begin{subfigure}[b]{0.3\textwidth}
4803 \begin{tikzpicture}[remember picture, node distance=1.5cm]
4804 \begin{pgfonlayer}{foreground}
4807 \node [right of=x] (y) {$y$};
4808 \node [right of=y] (z) {$z$};
4809 \node [below of=z] (k) {$k$};
4810 \node [left of=k] (j) {$j$};
4813 (x) edge node [above] {$<$} (y)
4814 (y) edge node [above] {$\le$} (z)
4815 (z) edge node [right] {$<$} (k)
4816 (k) edge node [below] {$\le$} (j)
4817 (j) edge node [left ] {$\le$} (y);
4818 \end{pgfonlayer}{foreground}
4820 \begin{tikzpicture}[remember picture, overlay]
4821 \begin{pgfonlayer}{background}
4822 \fill [red, opacity=0.3, rounded corners]
4823 (-2.7,2.6) rectangle (-0.2,0.05)
4824 (-4.1,2.4) rectangle (-3.3,1.6);
4825 \end{pgfonlayer}{background}
4828 \label{fig:graph-one-scc}
4830 \caption{Strong constraints overrule weak constraints.}
4831 \label{fig:graph-one}
4834 \begin{mydef}[Strongly connected component]
4835 A \emph{strongly connected component} in a graph with vertices $V$ is
4836 a subset of $V$, say $V'$, such that for each $(v_1,v_2) \in V' \times
4837 V'$ there is a path from $v_1$ to $v_2$.
4840 The SCCs in the graph for the constraints above is shown in Figure
4841 \ref{fig:graph-one-scc}. If we have a strongly connected component with
4842 a $<$ edge---say $x < y$---in it, we have an inconsistency, since there
4843 must also be a path from $y$ to $x$, and by transitivity it must either
4844 be the case that $y \le x$ or $y < x$, which are both at odds with $x <
4847 Moreover, if we have a SCC with no $<$ edges, it means that all members
4848 of said SCC are equal, since for every $x \le y$ we have a path from $y$
4849 to $x$, which again by transitivity means that $y \le x$. Thus, we can
4850 \emph{condense} the SCC to a single vertex, by choosing a variable among
4851 the SCC as a representative for all the others. This can be done
4852 efficiently with disjoint set data structure, and is crucial to keep the
4853 graph compact, given the very large number of constraints generated when
4856 \subsection{(Web) REPL}
4858 Finally, we take a break from the types by giving a brief account of the
4859 design of our REPL, being a good example of modular design using various
4860 constructs dear to the Haskell programmer.
4862 Keeping in mind the \texttt{KMonadT} monad described in Section
4863 \ref{sec:parame}, the REPL is represented as a function in
4864 \texttt{KMonadT} consuming input and hopefully producing output. Then,
4865 front ends can very easily written by marshalling data in and out of the
4869 = ITyCheck String -- Type check a term
4870 | IEval String -- Evaluate a term
4871 | IDecl String -- Declare something
4875 = OTyCheck TmRefId [HoleCtx] -- Type checked term, with holes
4876 | OPretty TmRefId -- Term to pretty print, after evaluation
4877 -- Just holes, classically after loading a file
4881 -- KMonadT is parametrised over the type of the variables, which depends
4882 -- on how deep in the term structure we are. For the REPL, we only deal
4883 -- with top-level terms, and thus only `Id' variables---top level names.
4884 type REPL m = KMonadT Id m
4886 repl :: ReadFile m => Input -> REPL m Output
4889 The \texttt{ReadFile} monad embodies the only `extra' action that we
4890 need to have access too when running the REPL: reading files. We could
4891 simply use the \texttt{IO} monad, but this will not serve us well when
4892 implementing front end facing untrusted parties accessing the application
4893 running on our servers. In our case we expose the REPL as a web
4894 application, and we want the user to be able to load only from a
4895 pre-defined directory, not from the entire file system.
4897 For this reason we specify \texttt{ReadFile} to have just one function:
4899 class Monad m => ReadFile m where
4900 readFile' :: FilePath -> m (Either IOError String)
4902 While in the command-line application we will use the \texttt{IO} monad
4903 and have \texttt{readFile'} to work in the `obvious' way---by reading
4904 the file corresponding to the given file path---in the web prompt we
4905 will have it to accept only a file name, not a path, and read it from a
4906 pre-defined directory:
4908 -- The monad that will run the web REPL. The `ReaderT' holds the
4909 -- filepath to the directory where the files loadable by the user live.
4910 -- The underlying `IO' monad will be used to actually read the files.
4911 newtype DirRead a = DirRead (ReaderT FilePath IO a)
4913 instance ReadFile DirRead where
4915 do -- We get the base directory in the `ReaderT' with `ask'
4917 -- Is the filepath provided an unqualified file name?
4918 if snd (splitFileName fp) == fp
4919 -- If yes, go ahead and read the file, by lifting
4920 -- `readFile'' into the IO monad
4921 then DirRead (lift (readFile' (dir </> fp)))
4922 -- If not, return an error
4923 else return (Left (strMsg ("Invalid file name `" ++ fp ++ "'")))
4925 Once this light-weight infrastructure is in place, adding a web
4926 interface was an easy exercise. We use Jasper Van der Jeugt's
4927 \texttt{websockets} library\footnote{Available at
4928 \url{http://hackage.haskell.org/package/websockets}.} to create a
4929 proxy that receives \texttt{JSON}\footnote{\texttt{JSON} is a popular data interchange
4930 format, see \url{http://json.org} for more info.} messages with the
4931 user input, turns them into \texttt{Input} messages for the REPL, and
4932 then sends back a \texttt{JSON} message with the response. Moreover, each client
4933 is handled in a separate threads, so crashes of the REPL for a certain
4934 client will not bring the whole application down.
4936 On the front end side, we had to write some JavaScript to accept input
4937 from a form, and to make the responses appear on the screen. The web
4938 prompt is publicly available at \url{http://bertus.mazzo.li}, a sample
4939 session is shown Figure \ref{fig:web-prompt-one}.
4942 \includegraphics[width=\textwidth]{web-prompt.png}
4943 \caption{A sample run of the web prompt.}
4944 \label{fig:web-prompt-one}
4949 \section{Evaluation}
4950 \label{sec:evaluation}
4952 Going back to our goals in Section \ref{sec:contributions}, we feel that
4953 this thesis fills a gap in the description of observational type theory.
4954 In the design of \mykant\ we willingly patterned the core features
4955 against the ones present in Agda, with the hope that future implementors
4956 will be able to refer to this document without embarking on the same
4957 adventure themselves. We gave an original account of heterogeneous
4958 equality by showing that in a cumulative hierarchy we can keep
4959 equalities as small as we would be able too with a separate notion of
4960 type equality. As a side effect of developing \mykant, we also gave an
4961 original account of bidirectional type checking for user defined types,
4962 which get rid of many types while keeping the language very simple.
4964 Through the design of the theory of \mykant\ we have followed an
4965 approach where study and implementation were continuously interleaved,
4966 as a `reality check' for the ideas that we wished to implement. Given
4967 the great effort necessary to build a theorem prover capable of
4968 `real-world' proofs we have not attempted to compare \mykant's
4969 capabilities to those of Agda and Coq, the theorem provers that the
4970 author is most familiar with and in general two of the main players in
4971 the field. However we have ported a lot of simpler examples to check
4972 that the key features are working, some of which have been used in the
4973 previous sections and are reproduced in the appendices\footnote{The full
4974 list is available in the repository:
4975 \url{https://github.com/bitonic/kant/tree/master/data/samples/good}.}.
4976 A full example of interaction with \mykant\ is given in Section
4977 \ref{sec:type-holes}.
4979 The main culprits for the delays in the implementation are two issues
4980 that revealed themselves to be far less obvious than what the author
4981 predicted. The first, as we have already remarked in Section
4982 \ref{sec:term-repr}, is to have an adequate term representation that
4983 lets us express the right constructs in a safe way. There is still no
4984 widely accepted solution to this problem, which is approached in many
4985 different ways both in the literature and in the programming
4986 practice. The second aspect is the treatment of user defined data types.
4987 Again, the best techniques to implement them in a dependently typed
4988 setting still have not crystallised and implementors reinvent many
4989 wheels each time a new system is built. The author is still conflicted
4990 on whether having user defined types at all it is the right decision:
4991 while they are essential, the recent discovery of a paper by
4992 \cite{dagand2012elaborating} describing a way to efficiently encode
4993 user-defined data types to a set of core primitives---an option that
4994 seems very attractive.
4996 In general, implementing dependently typed languages is still a poorly
4997 understood practice, and almost every stage requires experimentation on
4998 behalf of the author. Another example is the treatment of the implicit
4999 hierarchy, where no resources are present describing the problem from an
5000 implementation perspective (we described our approach in Section
5001 \ref{sec:hier-impl}). Hopefully this state of things will change in the
5002 near future, and recent publications are promising in this direction,
5003 for example an unpublished paper by \cite{Brady2013} describing his
5004 implementation of the Idris programming language. Our ultimate goal is
5005 to be a part of this collective effort.
5007 \subsection{A type holes tutorial}
5008 \label{sec:type-holes}
5010 As a taster and showcase for the capabilities of \mykant, we present an
5011 interactive session with the \mykant\ REPL. While doing so, we present
5012 a feature that we still have not covered: type holes.
5014 Type holes are, in the author's opinion, one of the `killer' features of
5015 interactive theorem provers, and one that is begging to be exported to
5016 mainstream programming---although it is much more effective in a
5017 well-typed, functional setting. The idea is that when we are developing
5018 a proof or a program we can insert a hole to have the software tell us
5019 the type expected at that point. Furthermore, we can ask for the type
5020 of variables in context, to better understand our surroundings.
5022 In \mykant\ we use type holes by putting them where a term should go.
5023 We need to specify a name for the hole and then we can put as many terms
5024 as we like in it. \mykant\ will tell us which type it is expecting for
5025 the term where the hole is, and the type for each term that we have
5026 included. For example if we had:
5028 plus [m n : Nat] : Nat ⇒ (
5032 And we loaded the file in \mykant, we would get:
5033 \begin{Verbatim}[frame=leftline]
5041 Suppose we wanted to define the `less or equal' ordering on natural
5042 numbers as described in Section \ref{sec:user-type}. We will
5043 incrementally build our functions in a file called \texttt{le.ka}.
5044 First we define the necessary types, all of which we know well by now:
5046 data Nat : ⋆ ⇒ { zero : Nat | suc : Nat → Nat }
5048 data Empty : ⋆ ⇒ { }
5049 absurd [A : ⋆] [p : Empty] : A ⇒ (
5050 Empty-Elim p (λ _ ⇒ A)
5053 record Unit : ⋆ ⇒ tt { }
5055 Then fire up \mykant, and load the file:
5056 \begin{Verbatim}[frame=leftline]
5059 Version 0.0, made in London, year 2013.
5063 So far so good. Our definition will be defined by recursion on a
5064 natural number \texttt{n}, which will return a function that given
5065 another number \texttt{m} will return the trivial type \texttt{Unit} if
5066 $\texttt{n} \le \texttt{m}$, and the \texttt{Empty} type otherwise.
5067 However we are still not sure on how to define it, so we invoke
5068 $\texttt{Nat-Elim}$, the eliminator for natural numbers, and place holes
5069 instead of arguments. In the file we will write:
5071 le [n : Nat] : Nat → ⋆ ⇒ (
5072 Nat-Elim n (λ _ ⇒ Nat → ⋆)
5077 And then we reload in \mykant:
5078 \begin{Verbatim}[frame=leftline]
5082 h2 : Nat → (Nat → ⋆) → Nat → ⋆
5084 Which tells us what types we need to satisfy in each hole. However, it
5085 is not that clear what does what in each hole, and thus it is useful to
5086 have a definition vacuous in its arguments just to clear things up. We
5087 will use \texttt{Le} aid in reading the goal, with \texttt{Le m n} as a
5088 reminder that we to return the type corresponding to $\texttt{m} ≤
5091 Le [m n : Nat] : ⋆ ⇒ ⋆
5093 le [n : Nat] : [m : Nat] → Le n m ⇒ (
5094 Nat-Elim n (λ n ⇒ [m : Nat] → Le n m)
5099 \begin{Verbatim}[frame=leftline]
5102 h1 : [m : Nat] → Le zero m
5103 h2 : [x : Nat] → ([m : Nat] → Le x m) → [m : Nat] → Le (suc x) m
5105 This is much better! \mykant, when printing terms, does not substitute
5106 top-level names for their bodies, since usually the resulting term is
5107 much clearer. As a nice side-effect, we can use tricks like this to
5110 In this case in the first case we need to return, given any number
5111 \texttt{m}, $0 \le \texttt{m}$. The trivial type will do, since every
5112 number is less or equal than zero:
5114 le [n : Nat] : [m : Nat] → Le n m ⇒ (
5115 Nat-Elim n (λ n ⇒ [m : Nat] → Le n m)
5120 \begin{Verbatim}[frame=leftline]
5123 h2 : [x : Nat] → ([m : Nat] → Le x m) → [m : Nat] → Le (suc x) m
5125 Now for the important case. We are given our comparison function for a
5126 number, and we need to produce the function for the successor. Thus, we
5127 need to re-apply the induction principle on the other number, \texttt{m}:
5129 le [n : Nat] : [m : Nat] → Le n m ⇒ (
5130 Nat-Elim n (λ n ⇒ [m : Nat] → Le n m)
5132 (λ n' f m ⇒ Nat-Elim m (λ m' ⇒ Le (suc n') m') {|h2|} {|h3|})
5135 \begin{Verbatim}[frame=leftline]
5139 h3 : [x : Nat] → Le (suc n') x → Le (suc n') (suc x)
5141 In the first hole we know that the second number is zero, and thus we
5142 can return empty. In the second case, we can use the recursive argument
5143 \texttt{f} on the two numbers:
5145 le [n : Nat] : [m : Nat] → Le n m ⇒ (
5146 Nat-Elim n (λ n ⇒ [m : Nat] → Le n m)
5149 Nat-Elim m (λ m' ⇒ Le (suc n') m') Empty (λ f _ ⇒ f m'))
5152 We can verify that our function works as expected:
5153 \begin{Verbatim}[frame=leftline]
5156 >>> :e le zero (suc zero)
5158 >>> :e le (suc (suc zero)) (suc zero)
5161 The other functionality of type holes is examining types of things in
5162 context. Going back to the examples in Section \ref{sec:term-types}, we can
5163 implement the safe \texttt{head} function with our newly defined
5166 data List : [A : ⋆] → ⋆ ⇒
5167 { nil : List A | cons : A → List A → List A }
5169 length [A : ⋆] [l : List A] : Nat ⇒ (
5170 List-Elim l (λ _ ⇒ Nat) zero (λ _ _ n ⇒ suc n)
5173 gt [n m : Nat] : ⋆ ⇒ (le (suc m) n)
5175 head [A : ⋆] [l : List A] : gt (length A l) zero → A ⇒ (
5176 List-Elim l (λ l ⇒ gt (length A l) zero → A)
5181 We define \texttt{List}s, a polymorphic \texttt{length} function, and
5182 express $<$ (\texttt{gt}) in terms of $\le$. Then, we set up the type
5183 for our \texttt{head} function. Given a list and a proof that its
5184 length is greater than zero, we return the first element. If we load
5185 this in \mykant, we get:
5186 \begin{Verbatim}[frame=leftline]
5191 h2 : [x : A] [x1 : List A] →
5192 (gt (length A x1) zero → A) →
5193 gt (length A (cons x x1)) zero → A
5195 In the first case (the one for \texttt{nil}), we have a proof of
5196 \texttt{Empty}---surely we can use \texttt{absurd} to get rid of that
5197 case. In the second case we simply return the element in the
5200 head [A : ⋆] [l : List A] : gt (length A l) zero → A ⇒ (
5201 List-Elim l (λ l ⇒ gt (length A l) zero → A)
5206 Now, if we tried to get the head of an empty list, we face a problem:
5207 \begin{Verbatim}[frame=leftline]
5211 We would have to provide something of type \texttt{Empty}, which
5212 hopefully should be impossible. For non-empty lists, on the other hand,
5213 things run smoothly:
5214 \begin{Verbatim}[frame=leftline]
5215 >>> :t head Nat (cons zero nil)
5217 >>> :e head Nat (cons zero nil) tt
5220 This should give a vague idea of why type holes are so useful and in
5221 more in general about the development process in \mykant. Most
5222 interactive theorem provers offer some kind of facility
5223 to... interactively develop proofs, usually much more powerful than the
5224 fairly bare tools present in \mykant. Agda in particular offers a
5225 celebrated interactive mode for the \texttt{Emacs} text editor.
5227 \section{Future work}
5228 \label{sec:future-work}
5230 The first move that the author plans to make is to work towards a simple
5231 but powerful term representation. A good plan seems to be to associate
5232 each type (terms, telescopes, etc.) with what we can substitute
5233 variables with, so that the term type will be associated with itself,
5234 while telescopes and propositions will be associated to terms. This can
5235 probably be accomplished elegantly with Haskell's \emph{type families}
5236 \citep{chakravarty2005associated}. After achieving a more solid
5237 machinery for terms, implementing observational equality fully should
5238 prove relatively easy.
5240 Beyond this steps, we can go in many directions to improve the
5241 system that we described---here we review the main ones.
5244 \item[Pattern matching and recursion] Eliminators are very clumsy,
5245 and using them can be especially frustrating if we are used to writing
5246 functions via explicit recursion. \cite{Gimenez1995} showed how to
5247 reduce well-founded recursive definitions to primitive recursors.
5248 Intuitively, defining a function through an eliminators corresponds to
5249 pattern matching and recursively calling the function on the recursive
5250 occurrences of the type we matched against.
5252 Nested pattern matching can be justified by identifying a notion of
5253 `structurally smaller', and allowing recursive calls on all smaller
5254 arguments. Epigram goes all the way and actually implements recursion
5255 exclusively by providing a convenient interface to the two constructs
5256 above \citep{EpigramTut, McBride2004}.
5258 However as we extend the flexibility in our recursion elaborating
5259 definitions to eliminators becomes more and more laborious. For
5260 example we might want mutually recursive definitions and definitions
5261 that terminate relying on the structure of two arguments instead of
5262 just one. For this reason both Agda and Coq (Agda putting more
5263 effort) let the user write recursive definitions freely, and then
5264 employ an external syntactic one the recursive calls to ensure that
5265 the definitions are terminating.
5267 Moreover, if we want to use dependently typed languages for
5268 programming purposes, we will probably want to sidestep the
5269 termination checker and write a possibly non-terminating function;
5270 maybe because proving termination is particularly difficult. With
5271 explicit recursion this amounts to turning off a check, if we have
5272 only eliminators it is impossible.
5274 \item[More powerful data types] A popular improvement on basic data
5275 types are inductive families \citep{Dybjer1991}, where the parameters
5276 for the type constructors can change based on the data constructors,
5277 which lets us express naturally types such as $\mytyc{Vec} : \mynat
5278 \myarr \mytyp$, which given a number returns the type of lists of that
5279 length, or $\mytyc{Fin} : \mynat \myarr \mytyp$, which given a number
5280 $n$ gives the type of numbers less than $n$. This apparent omission
5281 was motivated by the fact that inductive families can be represented
5282 by adding equalities concerning the parameters of the type
5283 constructors as arguments to the data constructor, in much the same
5284 way that Generalised Abstract Data Types \citep{GHC} are handled in
5285 Haskell. Interestingly the modified version of System F that lies at
5286 the core of recent versions of GHC features coercions reminiscent of
5287 those found in OTT, motivated precisely by the need to implement GADTs
5288 in an elegant way \citep{Sulzmann2007}.
5290 Another concept introduced by \cite{dybjer2000general} is
5291 induction-recursion, where we define a data type in tandem with a
5292 function on that type. This technique has proven extremely useful to
5293 define embeddings of other calculi in an host language, by defining
5294 the representation of the embedded language as a data type and at the
5295 same time a function decoding from the representation to a type in the
5296 host language. The decoding function is then used to define the data
5297 type for the embedding itself, for example by reusing the host's
5298 language functions to describe functions in the embedded language,
5299 with decoded types as arguments.
5301 It is also worth mentioning that in recent times there has been work
5302 \citep{dagand2012elaborating, chapman2010gentle} to show how to define
5303 a set of primitives that data types can be elaborated into. The big
5304 advantage of the approach proposed is enabling a very powerful notion
5305 of generic programming, by writing functions working on the
5306 `primitive' types as to be workable by all the other `compatible'
5307 elaborated user defined types. This has been a considerable problem
5308 in the dependently type world, where we often define types which are
5309 more `strongly typed' version of similar structures,\footnote{For
5310 example the $\mytyc{OList}$ presented in Section \ref{sec:user-type}
5311 being a `more typed' version of an ordinary list.} and then find
5312 ourselves forced to redefine identical operations on both types.
5314 \item[Pattern matching and inductive families] The notion of inductive
5315 family also yields a more interesting notion of pattern matching,
5316 since matching on an argument influences the value of the parameters
5317 of the type of said argument. This means that pattern matching
5318 influences the context, which can be exploited to constraint the
5319 possible data constructors for \emph{other} arguments
5320 \citep{McBride2004}.
5322 \item[Type inference] While bidirectional type checking helps at a very
5323 low cost of implementation and complexity, a much more powerful weapon
5324 is found in \emph{pattern unification}, which allows Hindley-Milner
5325 style inference for dependently typed languages. Unification for
5326 higher order terms is undecidable and unification problems do not
5327 always have a most general unifier \citep{huet1973undecidability}.
5328 However \cite{miller1992unification} identified a decidable fragment
5329 of higher order unification commonly known as pattern unification,
5330 which is employed in most theorem provers to drastically reduce the
5331 number of type annotations. \cite{gundrytutorial} provide a tutorial
5334 \item[Coinductive data types] When we specify inductive data types, we
5335 do it by specifying its \emph{constructors}---functions with the type
5336 we are defining as codomain. Then, we are offered way of compute by
5337 recursively \emph{destructing} or \emph{eliminating} a member of the
5340 Coinductive data types are the dual of this approach. We specify ways
5341 to destruct data, and we are given a way to generate the defined type
5342 by repeatedly `unfolding' starting from some seed. For example,
5343 we could defined infinite streams by specifying a $\myfun{head}$ and
5344 $\myfun{tail}$ destructors---here using a syntax reminiscent of
5348 \mysyn{codata}\ \mytyc{Stream}\myappsp (\myb{A} {:} \mytyp)\ \mysyn{where} \\
5349 \myind{2} \{ \myfun{head} : \myb{A}, \myfun{tail} : \mytyc{Stream} \myappsp \myb{A}\}
5352 which will hopefully give us something like
5355 \myfun{head} : (\myb{A}{:}\mytyp) \myarr \mytyc{Stream} \myappsp \myb{A} \myarr \myb{A} \\
5356 \myfun{tail} : (\myb{A}{:}\mytyp) \myarr \mytyc{Stream} \myappsp \myb{A} \myarr \mytyc{Stream} \myappsp \myb{A} \\
5357 \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}
5360 Where, in $\mydc{unfold}$, $\myb{B} \myprod \myb{A}$ represents the
5361 fields of $\mytyc{Stream}$ but with the recursive occurrence replaced
5362 by the `seed' type $\myb{A}$.
5364 Beyond simple infinite types like $\mytyc{Stream}$, coinduction is
5365 particularly useful to write non-terminating programs like servers or
5366 software interacting with a user, while guaranteeing their liveliness.
5367 Moreover it lets us model possibly non-terminating computations in an
5368 elegant way \citep{Capretta2005}, enabling for example the study of
5369 operational semantics for non-terminating languages
5370 \citep{Danielsson2012}.
5372 \cite{cockett1992charity} pioneered this approach in their programming
5373 language Charity, and coinduction has since been adopted in systems
5374 such as Coq \citep{Gimenez1996} and Agda. However these
5375 implementations are unsatisfactory, since Coq's break subject
5376 reduction; and Agda, to avoid this problem, does not allow types to
5377 depend on the unfolding of codata. \cite{mcbride2009let} has shown
5378 how observational equality can help to resolve these issues, since we
5379 can reason about the unfoldings in a better way, like we reason about
5380 functions' extensional behaviour.
5383 The author looks forward to the study and possibly the implementation of
5384 these ideas in the years to come.
5390 \section{Notation and syntax}
5391 \label{app:notation}
5393 Syntax, derivation rules, and reduction rules, are enclosed in frames describing
5394 the type of relation being established and the syntactic elements appearing,
5397 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
5398 Typing derivations here.
5401 In the languages presented and Agda code samples we also highlight the syntax,
5402 following a uniform colour, capitalisation, and font style convention:
5405 \begin{tabular}{c | l}
5406 $\mytyc{Sans}$ & Type constructors. \\
5407 $\mydc{sans}$ & Data constructors. \\
5408 % $\myfld{sans}$ & Field accessors (e.g. \myfld{fst} and \myfld{snd} for products). \\
5409 $\mysyn{roman}$ & Keywords of the language. \\
5410 $\myfun{roman}$ & Defined values and destructors. \\
5411 $\myb{math}$ & Bound variables.
5415 When presenting grammars, we use a word in $\mysynel{math}$ font
5416 (e.g. $\mytmsyn$ or $\mytysyn$) to indicate indicate
5417 nonterminals. Additionally, we use quite flexibly a $\mysynel{math}$
5418 font to indicate a syntactic element in derivations or meta-operations.
5419 More specifically, terms are usually indicated by lowercase letters
5420 (often $\mytmt$, $\mytmm$, or $\mytmn$); and types by an uppercase
5421 letter (often $\mytya$, $\mytyb$, or $\mytycc$).
5423 When presenting type derivations, we often abbreviate and present multiple
5424 conclusions, each on a separate line:
5426 \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
5427 \UnaryInfC{$\myjud{\myapp{\myfst}{\mytmt}}{\mytya}$}
5429 \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mytyb}$}
5431 We often present `definitions' in the described calculi and in
5432 $\mykant$\ itself, like so:
5435 \myfun{name} : \mytysyn \\
5436 \myfun{name} \myappsp \myb{arg_1} \myappsp \myb{arg_2} \myappsp \cdots \mapsto \mytmsyn
5439 To define operators, we use a mixfix notation similar
5440 to Agda, where $\myarg$s denote arguments:
5443 \myarg \mathrel{\myfun{$\wedge$}} \myarg : \mybool \myarr \mybool \myarr \mybool \\
5444 \myb{b_1} \mathrel{\myfun{$\wedge$}} \myb{b_2} \mapsto \cdots
5447 In explicitly typed systems, we omit type annotations when they
5448 are obvious, e.g. by not annotating the type of parameters of
5449 abstractions or of dependent pairs.\\
5450 We introduce multiple arguments in one go in arrow types:
5452 (\myb{x}\, \myb{y} {:} \mytya) \myarr \cdots = (\myb{x} {:} \mytya) \myarr (\myb{y} {:} \mytya) \myarr \cdots
5454 and in abstractions:
5456 \myabs{\myb{x}\myappsp\myb{y}}{\cdots} = \myabs{\myb{x}}{\myabs{\myb{y}}{\cdots}}
5458 We also omit arrows to abbreviate types:
5460 (\myb{x} {:} \mytya)(\myb{y} {:} \mytyb) \myarr \cdots =
5461 (\myb{x} {:} \mytya) \myarr (\myb{y} {:} \mytyb) \myarr \cdots
5464 Meta operations names are displayed in $\mymeta{smallcaps}$ and
5465 written in a pattern matching style, also making use of boolean guards.
5466 For example, a meta operation operating on a context and terms might
5470 \mymeta{quux}(\myctx, \myb{x}) \mymetaguard \myb{x} \in \myctx \mymetagoes \myctx(\myb{x}) \\
5471 \mymeta{quux}(\myctx, \myb{x}) \mymetagoes \mymeta{outofbounds} \\
5476 From time to time we give examples in the Haskell programming
5477 language as defined by \cite{Haskell2010}, which we typeset in
5478 \texttt{teletype} font. I assume that the reader is already familiar
5479 with Haskell, plenty of good introductions are available
5480 \citep{LYAH,ProgInHask}.
5482 Examples of \mykant\ code will be typeset nicely with \LaTeX in Section
5483 \ref{sec:kant-theory}, to adjust with the rest of the presentation; and
5484 in \texttt{teletype} font in the rest of the document, including Section
5485 \ref{sec:kant-practice} and in the appendices. All the \mykant\ code
5486 shown is meant to be working and ready to be inputted in a \mykant\
5487 prompt or loaded from a file. Snippets of sessions in the \mykant\
5488 prompt will be displayed with a left border, to distinguish them from
5490 \begin{Verbatim}[frame=leftline]
5497 \subsection{ITT renditions}
5498 \label{app:itt-code}
5500 \subsubsection{Agda}
5501 \label{app:agda-itt}
5503 Note that in what follows rules for `base' types are
5504 universe-polymorphic, to reflect the exposition. Derived definitions,
5505 on the other hand, mostly work with \mytyc{Set}, reflecting the fact
5506 that in the theory presented we don't have universe polymorphism.
5512 data Empty : Set where
5514 absurd : ∀ {a} {A : Set a} → Empty → A
5517 ¬_ : ∀ {a} → (A : Set a) → Set a
5520 record Unit : Set where
5523 record _×_ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
5530 data Bool : Set where
5533 if_/_then_else_ : ∀ {a} (x : Bool) (P : Bool → Set a) → P true → P false → P x
5534 if true / _ then x else _ = x
5535 if false / _ then _ else x = x
5537 if_then_else_ : ∀ {a} (x : Bool) {P : Bool → Set a} → P true → P false → P x
5538 if_then_else_ x {P} = if_/_then_else_ x P
5540 data W {s p} (S : Set s) (P : S → Set p) : Set (s ⊔ p) where
5541 _◁_ : (s : S) → (P s → W S P) → W S P
5543 rec : ∀ {a b} {S : Set a} {P : S → Set b}
5544 (C : W S P → Set) → -- some conclusion we hope holds
5545 ((s : S) → -- given a shape...
5546 (f : P s → W S P) → -- ...and a bunch of kids...
5547 ((p : P s) → C (f p)) → -- ...and C for each kid in the bunch...
5548 C (s ◁ f)) → -- ...does C hold for the node?
5549 (x : W S P) → -- If so, ...
5550 C x -- ...C always holds.
5551 rec C c (s ◁ f) = c s f (λ p → rec C c (f p))
5553 module Examples-→ where
5560 -- These pragmas are needed so we can use number literals.
5561 {-# BUILTIN NATURAL ℕ #-}
5562 {-# BUILTIN ZERO zero #-}
5563 {-# BUILTIN SUC suc #-}
5565 data List (A : Set) : Set where
5567 _∷_ : A → List A → List A
5569 length : ∀ {A} → List A → ℕ
5571 length (_ ∷ l) = suc (length l)
5576 suc x > suc y = x > y
5578 head : ∀ {A} → (l : List A) → length l > 0 → A
5579 head [] p = absurd p
5582 module Examples-× where
5588 even (suc zero) = Empty
5589 even (suc (suc n)) = even n
5594 5-not-even : ¬ (even 5)
5597 there-is-an-even-number : ℕ × even
5598 there-is-an-even-number = 6 , 6-even
5600 _∨_ : (A B : Set) → Set
5601 A ∨ B = Bool × (λ b → if b then A else B)
5603 left : ∀ {A B} → A → A ∨ B
5606 right : ∀ {A B} → B → A ∨ B
5609 [_,_] : {A B C : Set} → (A → C) → (B → C) → A ∨ B → C
5611 (if (fst x) / (λ b → if b then _ else _ → _) then f else g) (snd x)
5613 module Examples-W where
5618 Tr b = if b then Unit else Empty
5624 zero = false ◁ absurd
5627 suc n = true ◁ (λ _ → n)
5633 if b / (λ b → (Tr b → ℕ) → (Tr b → ℕ) → ℕ)
5634 then (λ _ f → (suc (f tt))) else (λ _ _ → y))
5637 module Equality where
5640 data _≡_ {a} {A : Set a} : A → A → Set a where
5643 ≡-elim : ∀ {a b} {A : Set a}
5644 (P : (x y : A) → x ≡ y → Set b) →
5645 ∀ {x y} → P x x (refl x) → (x≡y : x ≡ y) → P x y x≡y
5646 ≡-elim P p (refl x) = p
5648 subst : ∀ {A : Set} (P : A → Set) → ∀ {x y} → (x≡y : x ≡ y) → P x → P y
5649 subst P x≡y p = ≡-elim (λ _ y _ → P y) p x≡y
5651 sym : ∀ {A : Set} (x y : A) → x ≡ y → y ≡ x
5652 sym x y p = subst (λ y′ → y′ ≡ x) p (refl x)
5654 trans : ∀ {A : Set} (x y z : A) → x ≡ y → y ≡ z → x ≡ z
5655 trans x y z p q = subst (λ z′ → x ≡ z′) q p
5657 cong : ∀ {A B : Set} (x y : A) → x ≡ y → (f : A → B) → f x ≡ f y
5658 cong x y p f = subst (λ z → f x ≡ f z) p (refl (f x))
5661 \subsubsection{\mykant}
5662 \label{app:kant-itt}
5664 The following things are missing: $\mytyc{W}$-types, since our
5665 positivity check is overly strict, and equality, since we haven't
5666 implemented that yet.
5669 \verbatiminput{itt.ka}
5672 \subsection{\mykant\ examples}
5673 \label{app:kant-examples}
5676 \verbatiminput{examples.ka}
5679 \subsection{\mykant' hierachy}
5682 This rendition of the Hurken's paradox does not type check with the
5683 hierachy enabled, type checks and loops without it. Adapted from an
5684 Agda version, available at
5685 \url{http://code.haskell.org/Agda/test/succeed/Hurkens.agda}.
5688 \verbatiminput{hurkens.ka}
5691 \subsection{Term representation}
5694 Data type for terms in \mykant.
5696 {\small\begin{verbatim}-- A top-level name.
5698 -- A data/type constructor name.
5701 -- A term, parametrised over the variable (`v') and over the reference
5702 -- type used in the type hierarchy (`r').
5705 | Ty r -- Type, with a hierarchy reference.
5706 | Lam (TmScope r v) -- Abstraction.
5707 | Arr (Tm r v) (TmScope r v) -- Dependent function.
5708 | App (Tm r v) (Tm r v) -- Application.
5709 | Ann (Tm r v) (Tm r v) -- Annotated term.
5710 -- Data constructor, the first ConId is the type constructor and
5711 -- the second is the data constructor.
5712 | Con ADTRec ConId ConId [Tm r v]
5713 -- Data destrutor, again first ConId being the type constructor
5714 -- and the second the name of the eliminator.
5715 | Destr ADTRec ConId Id (Tm r v)
5717 | Hole HoleId [Tm r v]
5718 -- Decoding of propositions.
5722 | Prop r -- The type of proofs, with hierarchy reference.
5725 | And (Tm r v) (Tm r v)
5726 | Forall (Tm r v) (TmScope r v)
5727 -- Heterogeneous equality.
5728 | Eq (Tm r v) (Tm r v) (Tm r v) (Tm r v)
5730 -- Either a data type, or a record.
5731 data ADTRec = ADT | Rc
5733 -- Either a coercion, or coherence.
5734 data Coeh = Coe | Coh\end{verbatim}
5737 \subsection{Graph and constraints modules}
5738 \label{app:constraint}
5740 The modules are respectively named \texttt{Data.LGraph} (short for
5741 `labelled graph'), and \texttt{Data.Constraint}. The type class
5742 constraints on the type parameters are not shown for clarity, unless
5743 they are meaningful to the function. In practice we use the
5744 \texttt{Hashable} type class on the vertex to implement the graph
5745 efficiently with hash maps.
5747 \subsubsection{\texttt{Data.LGraph}}
5750 \verbatiminput{graph.hs}
5753 \subsubsection{\texttt{Data.Constraint}}
5756 \verbatiminput{constraint.hs}
5761 \bibliographystyle{authordate1}
5762 \bibliography{final}