2 %% THIS LATEX HURTS YOUR EYES. DO NOT READ.
7 \documentclass[11pt, fleqn, twoside]{article}
10 \usepackage[sc,slantedGreek]{mathpazo}
14 % \oddsidemargin .50in
15 % \evensidemargin -.25in
33 \usepackage[pdftex, pdfborderstyle={/S/U/W 0}]{hyperref}
39 \usepackage[fleqn]{amsmath}
40 \usepackage{stmaryrd} %llbracket
43 \usepackage{bussproofs}
55 \usepackage{subcaption}
60 \RecustomVerbatimEnvironment
66 \usetikzlibrary{shapes,arrows,positioning}
67 \usetikzlibrary{intersections}
68 % \usepackage{tikz-cd}
69 % \usepackage{pgfplots}
72 %% -----------------------------------------------------------------------------
74 \usepackage[english]{babel}
75 \usepackage[conor]{agda}
76 \renewcommand{\AgdaKeywordFontStyle}[1]{\ensuremath{\mathrm{\underline{#1}}}}
77 \renewcommand{\AgdaFunction}[1]{\textbf{\textcolor{AgdaFunction}{#1}}}
78 \renewcommand{\AgdaField}{\AgdaFunction}
79 % \definecolor{AgdaBound} {HTML}{000000}
80 \definecolor{AgdaHole} {HTML} {FFFF33}
82 \DeclareUnicodeCharacter{9665}{\ensuremath{\lhd}}
83 \DeclareUnicodeCharacter{964}{\ensuremath{\tau}}
84 \DeclareUnicodeCharacter{963}{\ensuremath{\sigma}}
85 \DeclareUnicodeCharacter{915}{\ensuremath{\Gamma}}
86 \DeclareUnicodeCharacter{8799}{\ensuremath{\stackrel{?}{=}}}
87 \DeclareUnicodeCharacter{9655}{\ensuremath{\rhd}}
89 \renewenvironment{code}%
90 {\noindent\ignorespaces\advance\leftskip\mathindent\AgdaCodeStyle\pboxed\small}%
91 {\endpboxed\par\noindent%
92 \ignorespacesafterend\small}
95 %% -----------------------------------------------------------------------------
98 \newcommand{\mysmall}{}
99 \newcommand{\mysyn}{\AgdaKeyword}
100 \newcommand{\mytyc}[1]{\textup{\AgdaDatatype{#1}}}
101 \newcommand{\mydc}[1]{\textup{\AgdaInductiveConstructor{#1}}}
102 \newcommand{\myfld}[1]{\textup{\AgdaField{#1}}}
103 \newcommand{\myfun}[1]{\textup{\AgdaFunction{#1}}}
104 \newcommand{\myb}[1]{\AgdaBound{$#1$}}
105 \newcommand{\myfield}{\AgdaField}
106 \newcommand{\myind}{\AgdaIndent}
107 \newcommand{\mykant}{\textmd{\textsc{Bertus}}}
108 \newcommand{\mysynel}[1]{#1}
109 \newcommand{\myse}{\mysynel}
110 \newcommand{\mytmsyn}{\mysynel{term}}
111 \newcommand{\mysp}{\ }
112 \newcommand{\myabs}[2]{\mydc{$\lambda$} #1 \mathrel{\mydc{$\mapsto$}} #2}
113 \newcommand{\myappsp}{\hspace{0.07cm}}
114 \newcommand{\myapp}[2]{#1 \myappsp #2}
115 \newcommand{\mysynsep}{\ \ |\ \ }
116 \newcommand{\myITE}[3]{\myfun{If}\, #1\, \myfun{Then}\, #2\, \myfun{Else}\, #3}
117 \newcommand{\mycumul}{\preceq}
120 \newcommand{\mydesc}[3]{
126 \hfill \textup{\textbf{#1}} $#2$
127 \framebox[\textwidth]{
142 \newcommand{\mytmt}{\mysynel{t}}
143 \newcommand{\mytmm}{\mysynel{m}}
144 \newcommand{\mytmn}{\mysynel{n}}
145 \newcommand{\myred}{\leadsto}
146 \newcommand{\mysub}[3]{#1[#3 / #2]}
147 \newcommand{\mytysyn}{\mysynel{type}}
148 \newcommand{\mybasetys}{K}
149 \newcommand{\mybasety}[1]{B_{#1}}
150 \newcommand{\mytya}{\myse{A}}
151 \newcommand{\mytyb}{\myse{B}}
152 \newcommand{\mytycc}{\myse{C}}
153 \newcommand{\myarr}{\mathrel{\textcolor{AgdaDatatype}{\to}}}
154 \newcommand{\myprod}{\mathrel{\textcolor{AgdaDatatype}{\times}}}
155 \newcommand{\myctx}{\Gamma}
156 \newcommand{\myvalid}[1]{#1 \vdash \underline{\mathrm{valid}}}
157 \newcommand{\myjudd}[3]{#1 \vdash #2 : #3}
158 \newcommand{\myjud}[2]{\myjudd{\myctx}{#1}{#2}}
159 \newcommand{\myabss}[3]{\mydc{$\lambda$} #1 {:} #2 \mathrel{\mydc{$\mapsto$}} #3}
160 \newcommand{\mytt}{\mydc{$\langle\rangle$}}
161 \newcommand{\myunit}{\mytyc{Unit}}
162 \newcommand{\mypair}[2]{\mathopen{\mydc{$\langle$}}#1\mathpunct{\mydc{,}} #2\mathclose{\mydc{$\rangle$}}}
163 \newcommand{\myfst}{\myfld{fst}}
164 \newcommand{\mysnd}{\myfld{snd}}
165 \newcommand{\myconst}{\myse{c}}
166 \newcommand{\myemptyctx}{\varepsilon}
167 \newcommand{\myhole}{\AgdaHole}
168 \newcommand{\myfix}[3]{\mysyn{fix} \myappsp #1 {:} #2 \mapsto #3}
169 \newcommand{\mysum}{\mathbin{\textcolor{AgdaDatatype}{+}}}
170 \newcommand{\myleft}[1]{\mydc{left}_{#1}}
171 \newcommand{\myright}[1]{\mydc{right}_{#1}}
172 \newcommand{\myempty}{\mytyc{Empty}}
173 \newcommand{\mycase}[2]{\mathopen{\myfun{[}}#1\mathpunct{\myfun{,}} #2 \mathclose{\myfun{]}}}
174 \newcommand{\myabsurd}[1]{\myfun{absurd}_{#1}}
175 \newcommand{\myarg}{\_}
176 \newcommand{\myderivsp}{}
177 \newcommand{\myderivspp}{\vspace{0.3cm}}
178 \newcommand{\mytyp}{\mytyc{Type}}
179 \newcommand{\myneg}{\myfun{$\neg$}}
180 \newcommand{\myar}{\,}
181 \newcommand{\mybool}{\mytyc{Bool}}
182 \newcommand{\mytrue}{\mydc{true}}
183 \newcommand{\myfalse}{\mydc{false}}
184 \newcommand{\myitee}[5]{\myfun{if}\,#1 / {#2.#3}\,\myfun{then}\,#4\,\myfun{else}\,#5}
185 \newcommand{\mynat}{\mytyc{$\mathbb{N}$}}
186 \newcommand{\myrat}{\mytyc{$\mathbb{R}$}}
187 \newcommand{\myite}[3]{\myfun{if}\,#1\,\myfun{then}\,#2\,\myfun{else}\,#3}
188 \newcommand{\myfora}[3]{(#1 {:} #2) \myarr #3}
189 \newcommand{\myexi}[3]{(#1 {:} #2) \myprod #3}
190 \newcommand{\mypairr}[4]{\mathopen{\mydc{$\langle$}}#1\mathpunct{\mydc{,}} #4\mathclose{\mydc{$\rangle$}}_{#2{.}#3}}
191 \newcommand{\mylist}{\mytyc{List}}
192 \newcommand{\mynil}[1]{\mydc{[]}_{#1}}
193 \newcommand{\mycons}{\mathbin{\mydc{∷}}}
194 \newcommand{\myfoldr}{\myfun{foldr}}
195 \newcommand{\myw}[3]{\myapp{\myapp{\mytyc{W}}{(#1 {:} #2)}}{#3}}
196 \newcommand{\mynodee}{\mathbin{\mydc{$\lhd$}}}
197 \newcommand{\mynode}[2]{\mynodee_{#1.#2}}
198 \newcommand{\myrec}[4]{\myfun{rec}\,#1 / {#2.#3}\,\myfun{with}\,#4}
199 \newcommand{\mylub}{\sqcup}
200 \newcommand{\mydefeq}{\cong}
201 \newcommand{\myrefl}{\mydc{refl}}
202 \newcommand{\mypeq}{\mytyc{=}}
203 \newcommand{\myjeqq}{\myfun{$=$-elim}}
204 \newcommand{\myjeq}[3]{\myapp{\myapp{\myapp{\myjeqq}{#1}}{#2}}{#3}}
205 \newcommand{\mysubst}{\myfun{subst}}
206 \newcommand{\myprsyn}{\myse{prop}}
207 \newcommand{\myprdec}[1]{\mathopen{\mytyc{$\llbracket$}} #1 \mathclose{\mytyc{$\rrbracket$}}}
208 \newcommand{\myand}{\mathrel{\mytyc{$\wedge$}}}
209 \newcommand{\mybigand}{\mathrel{\mytyc{$\bigwedge$}}}
210 \newcommand{\myprfora}[3]{\forall #1 {:} #2.\, #3}
211 \newcommand{\myimpl}{\mathrel{\mytyc{$\Rightarrow$}}}
212 \newcommand{\mybot}{\mytyc{$\bot$}}
213 \newcommand{\mytop}{\mytyc{$\top$}}
214 \newcommand{\mycoe}{\myfun{coe}}
215 \newcommand{\mycoee}[4]{\myapp{\myapp{\myapp{\myapp{\mycoe}{#1}}{#2}}{#3}}{#4}}
216 \newcommand{\mycoh}{\myfun{coh}}
217 \newcommand{\mycohh}[4]{\myapp{\myapp{\myapp{\myapp{\mycoh}{#1}}{#2}}{#3}}{#4}}
218 \newcommand{\myjm}[4]{(#1 {:} #2) \mathrel{\mytyc{=}} (#3 {:} #4)}
219 \newcommand{\myeq}{\mathrel{\mytyc{=}}}
220 \newcommand{\myprop}{\mytyc{Prop}}
221 \newcommand{\mytmup}{\mytmsyn\uparrow}
222 \newcommand{\mydefs}{\Delta}
223 \newcommand{\mynf}{\Downarrow}
224 \newcommand{\myinff}[3]{#1 \vdash #2 \Uparrow #3}
225 \newcommand{\myinf}[2]{\myinff{\myctx}{#1}{#2}}
226 \newcommand{\mychkk}[3]{#1 \vdash #2 \Downarrow #3}
227 \newcommand{\mychk}[2]{\mychkk{\myctx}{#1}{#2}}
228 \newcommand{\myann}[2]{#1 : #2}
229 \newcommand{\mydeclsyn}{\myse{decl}}
230 \newcommand{\myval}[3]{#1 : #2 \mapsto #3}
231 \newcommand{\mypost}[2]{\mysyn{abstract}\ #1 : #2}
232 \newcommand{\myadt}[4]{\mysyn{data}\ #1 #2\ \mysyn{where}\ #3\{ #4 \}}
233 \newcommand{\myreco}[4]{\mysyn{record}\ #1 #2\ \mysyn{where}\ \{ #4 \}}
234 \newcommand{\myelabt}{\vdash}
235 \newcommand{\myelabf}{\rhd}
236 \newcommand{\myelab}[2]{\myctx \myelabt #1 \myelabf #2}
237 \newcommand{\mytele}{\Delta}
238 \newcommand{\mytelee}{\delta}
239 \newcommand{\mydcctx}{\Gamma}
240 \newcommand{\mynamesyn}{\myse{name}}
241 \newcommand{\myvec}{\overrightarrow}
242 \newcommand{\mymeta}{\textsc}
243 \newcommand{\myhyps}{\mymeta{hyps}}
244 \newcommand{\mycc}{;}
245 \newcommand{\myemptytele}{\varepsilon}
246 \newcommand{\mymetagoes}{\Longrightarrow}
247 % \newcommand{\mytesctx}{\
248 \newcommand{\mytelesyn}{\myse{telescope}}
249 \newcommand{\myrecs}{\mymeta{recs}}
250 \newcommand{\myle}{\mathrel{\lcfun{$\le$}}}
251 \newcommand{\mylet}{\mysyn{let}}
252 \newcommand{\myhead}{\mymeta{head}}
253 \newcommand{\mytake}{\mymeta{take}}
254 \newcommand{\myix}{\mymeta{ix}}
255 \newcommand{\myapply}{\mymeta{apply}}
256 \newcommand{\mydataty}{\mymeta{datatype}}
257 \newcommand{\myisreco}{\mymeta{record}}
258 \newcommand{\mydcsep}{\ |\ }
259 \newcommand{\mytree}{\mytyc{Tree}}
260 \newcommand{\myproj}[1]{\myfun{$\pi_{#1}$}}
261 \newcommand{\mysigma}{\mytyc{$\Sigma$}}
262 \newcommand{\mynegder}{\vspace{-0.3cm}}
263 \newcommand{\myquot}{\Uparrow}
264 \newcommand{\mynquot}{\, \Downarrow}
265 \newcommand{\mycanquot}{\ensuremath{\textsc{quote}{\Downarrow}}}
266 \newcommand{\myneuquot}{\ensuremath{\textsc{quote}{\Uparrow}}}
267 \newcommand{\mymetaguard}{\ |\ }
268 \newcommand{\mybox}{\Box}
269 \newcommand{\mytermi}[1]{\text{\texttt{#1}}}
270 \newcommand{\mysee}[1]{\langle\myse{#1}\rangle}
272 \renewcommand{\[}{\begin{equation*}}
273 \renewcommand{\]}{\end{equation*}}
274 \newcommand{\mymacol}[2]{\text{\textcolor{#1}{$#2$}}}
276 \newtheorem*{mydef}{Definition}
277 \newtheoremstyle{named}{}{}{\itshape}{}{\bfseries}{}{.5em}{\textsc{#1}}
280 \pgfdeclarelayer{background}
281 \pgfdeclarelayer{foreground}
282 \pgfsetlayers{background,main,foreground}
284 %% -----------------------------------------------------------------------------
286 \title{\mykant: Implementing Observational Equality}
287 \author{Francesco Mazzoli \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{<fm2209@ic.ac.uk>}}}
302 % Upper part of the page. The '~' is needed because \\
303 % only works if a paragraph has started.
304 \includegraphics[width=0.4\textwidth]{brouwer-cropped.png}~\\[1cm]
306 \textsc{\Large Final year project}\\[0.5cm]
309 { \huge \mykant: Implementing Observational Equality}\\[1.5cm]
311 {\Large Francesco \textsc{Mazzoli} \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{<fm2209@ic.ac.uk>}}}\\[0.8cm]
313 \begin{minipage}{0.4\textwidth}
314 \begin{flushleft} \large
316 Dr. Steffen \textsc{van Bakel}
319 \begin{minipage}{0.4\textwidth}
320 \begin{flushright} \large
321 \emph{Second marker:} \\
322 Dr. Philippa \textsc{Gardner}
333 \pagenumbering{gobble}
339 \thispagestyle{empty}
342 The marriage between programming and logic has been a very fertile
343 one. In particular, since the definition of the simply typed
344 $\lambda$-calculus, a number of type systems have been devised with
345 increasing expressive power.
347 Among this systems, Inutitionistic Type Theory (ITT) has been a very
348 popular framework for theorem provers and programming languages.
349 However, reasoning about equality has always been a tricky business in
350 ITT and related theories. In this thesis we will explain why this is
351 the case, and present Observational Type Theory (OTT), a solution to
352 some of the problems with equality.
354 To bring OTT closer to the current practice of interactive theorem
355 provers, we describe \mykant, a system featuring OTT in a setting more
356 close to the one found in widely used provers such as Agda and Coq.
357 Nost notably, we feature used defined inductive and record types and a
358 cumulative, implicit type hierarchy. Having implemented part of
359 $\mykant$ as a Haskell program, we describe some of the implementation
367 \renewcommand{\abstractname}{Acknowledgements}
369 I would like to thank Steffen van Bakel, my supervisor, who was brave
370 enough to believe in my project and who provided much advice and
373 I would also like to thank the Haskell and Agda community on
374 \texttt{IRC}, which guided me through the strange world of types; and
375 in particular Andrea Vezzosi and James Deikun, with whom I entertained
376 countless insightful discussions over the past year. Andrea suggested
377 Observational Type Theory as a topic of study: this thesis would not
378 exist without him. Before them, Tony Field introduced me to Haskell,
379 unknowingly filling most of my free time from that time on.
381 Finally, much of the work stems from the research of Conor McBride,
382 who answered many of my doubts through these months. I also owe him
390 \thispagestyle{empty}
396 \pagenumbering{arabic}
398 \section{Introduction}
400 Functional programming is in good shape. In particular the `well-typed'
401 line of work originating from Milner's ML has been extremely fruitful,
402 in various directions. Nowadays functional, well-typed programming
403 languages like Haskell or OCaml are slowly being absorbed by the
404 mainstream. An important related development---and in fact the original
405 motivator for ML's existence---is the advancement of the practice of
406 \emph{interactive theorem provers}.
409 An interactive theorem prover, or proof assistant, is a tool that lets
410 the user develop formal proofs with the confidence of the machine
411 checking it for correctness. While the effort towards a full
412 formalisation of mathematics has been ongoing for more than a century,
413 theorem provers have been the first class of software whose
414 implementation depends directly on these theories.
416 In a fortunate turn of events, it was discovered that well-typed
417 functional programming and proving theorems in an \emph{intuitionistic}
418 logic are the same activity. Under this discipline, the types in our
419 programming language can be interpreted as proposition in our logic; and
420 the programs implementing the specification given by the types as their
421 proofs. This fact stimulated a very active transfer of techniques and
422 knowledge between logic and programming language theory, in both
425 Mathematics could provide programming with a huge wealth of abstractions
426 and constructs developed over centuries. Moreover, identifying our
427 types with a logic lets us focus on foundational questions regarding
428 programming with a much more solid approach, given the years of rigorous
429 study of logic. Programmers, on the other hand, had already developed a
430 wealth of approaches to effectively collaborate with computers, through
431 the study of programming languages.
433 We will follow the discipline of Intuitionistic Type Theory, or
434 Martin-L\"{o}f Type Theory, after its inventor. First formulated in the
435 70s and then adjusted through a series of revisions, it has endured as
436 the core of many practical systems widely in use today, and it is
437 probably the most prominent instance of the proposition-as-types and
438 proofs-as-programs discipline. One of the most debated subjects in this
439 field has been regarding what notion of \emph{equality} should be
442 The tension in the field of equality springs from the fact that there is
443 a divide between what the user can prove equal \emph{inside} the
444 theory---what is \emph{propositionally} equal--- and what the theorem
445 prover identifies as equal in its meta-theory---what is
446 \emph{definitionally} equal. If we want our system to be well behaved
447 (for example if we want type checking to be decidable) we must keep the
448 two notions separate, with definitional equality inducing propositional
449 equality, but not the reverse. However in this scenario propositional
450 equality is weaker than we would like: we can only prove terms equal
451 based on their syntactical structure, and not based on their observable
454 This thesis is concerned with exploring a new approach in this area,
455 \emph{observational} equality. Promising to provide a more adequate
456 propositional equality while retaining well-behavedness, it still is a
457 relatively unexplored notion. We set ourselves to change that by
458 studying it in a setting more akin the one found in currently available
461 \subsection{Structure}
463 Section \ref{sec:types} will give a brief overview of the
464 $\lambda$-calculus, both typed and untyped. This will give us the
465 chance to introduce most of the concepts mentioned above rigorously, and
466 gain some intuition about them. An excellent introduction to types in
467 general can be found in \cite{Pierce2002}, although not from the
468 perspective of theorem proving.
470 Section \ref{sec:itt} will describe a set of basic construct that form a
471 `baseline' Intuitionistic Type Theory. The goal is to familiarise with
472 the main concept of ITT before attacking the problem of equality. Given
473 the wealth of material covered the exposition is quite dense. Good
474 introductions can be found in \cite{Thompson1991}, \cite{Nordstrom1990},
475 and \cite{Martin-Lof1984} himself.
477 Section \ref{sec:equality} will introduce propositional equality. The
478 properties of propositional equality will be discussed along with its
479 limitations. After reviewing some extensions to propositional equality,
480 we will explain why identifying definitional equality with propositional
481 equality causes problems.
483 Section \ref{sec:ott} will introduce observational equality, following
484 closely the original exposition by \cite{Altenkirch2007}. The
485 presentation is free-standing but glosses over the meta-theoretic
486 properties of OTT, focusing on the mechanism that make it work.
488 Section \ref{sec:kant-theory} will describe \mykant, a system we have
489 developed incorporating OTT along constructs usually present in modern
490 theorem provers. Along the way, we describe these additional features
491 and their advantages. Section \ref{sec:kant-practice} will describe an
492 implementation implementing part of \mykant. A high level design of the
493 software is given, along with a few specific implementation issues
495 Finally, Section \ref{sec:evaluation} will asses the decisions made in
496 designing and implementing \mykant, and Section \ref{sec:future-work}
497 will give a roadmap to bring \mykant\ on par and beyond the
500 \subsection{Contribution}
502 The goal of this thesis is threefold:
505 \item Provide a description of observational equality `in context', to
506 make the subject more accessible. Considering the possibilities that
507 OTT brings to the table, we think that introducing it to a wider
508 audience can only be beneficial.
510 \item Fill in the gaps needed to make OTT work with user-defined
511 inductive types and a type hierarchy. We show how one notion of
512 equality is enough, instead of separate notions of value- and
513 type-equality as presented in the original paper. We are able to keep
514 the type equalities `small' while preserving subject reduction by
515 exploiting the fact that we work within a cumulative theory.
516 Incidentally, we also describe a generalised version of bidirectional
517 type checking for user defined types.
519 \item Provide an implementation to probe the possibilities of OTT in a
520 more realistic setting. We have implemented an ITT with user defined
521 types but due to the limited time constraints we were not able to
522 complete the implementation of observational equality. Nonetheless,
523 we describe some interesting implementation issues faced by the type
527 \section{Simple and not-so-simple types}
530 \subsection{The untyped $\lambda$-calculus}
533 Along with Turing's machines, the earliest attempts to formalise
534 computation lead to the definition of the $\lambda$-calculus
535 \citep{Church1936}. This early programming language encodes computation
536 with a minimal syntax and no `data' in the traditional sense, but just
537 functions. Here we give a brief overview of the language, which will
538 give the chance to introduce concepts central to the analysis of all the
539 following calculi. The exposition follows the one found in Chapter 5 of
542 \begin{mydef}[$\lambda$-terms]
543 Syntax of the $\lambda$-calculus: variables, abstractions, and
549 \begin{array}{r@{\ }c@{\ }l}
550 \mytmsyn & ::= & \myb{x} \mysynsep \myabs{\myb{x}}{\mytmsyn} \mysynsep (\myapp{\mytmsyn}{\mytmsyn}) \\
551 x & \in & \text{Some enumerable set of symbols}
556 Parenthesis will be omitted in the usual way, with application being
559 Abstractions roughly corresponds to functions, and their semantics is more
560 formally explained by the $\beta$-reduction rule.
562 \begin{mydef}[$\beta$-reduction]
563 $\beta$-reduction and substitution for the $\lambda$-calculus.
566 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
569 \myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{\myb{x}}{\mytmn}\text{ \textbf{where}} \\
571 \begin{array}{l@{\ }c@{\ }l}
572 \mysub{\myb{x}}{\myb{x}}{\mytmn} & = & \mytmn \\
573 \mysub{\myb{y}}{\myb{x}}{\mytmn} & = & y\text{ \textbf{with} } \myb{x} \neq y \\
574 \mysub{(\myapp{\mytmt}{\mytmm})}{\myb{x}}{\mytmn} & = & (\myapp{\mysub{\mytmt}{\myb{x}}{\mytmn}}{\mysub{\mytmm}{\myb{x}}{\mytmn}}) \\
575 \mysub{(\myabs{\myb{x}}{\mytmm})}{\myb{x}}{\mytmn} & = & \myabs{\myb{x}}{\mytmm} \\
576 \mysub{(\myabs{\myb{y}}{\mytmm})}{\myb{x}}{\mytmn} & = & \myabs{\myb{z}}{\mysub{\mysub{\mytmm}{\myb{y}}{\myb{z}}}{\myb{x}}{\mytmn}} \\
577 \multicolumn{3}{l}{\myind{2} \text{\textbf{with} $\myb{x} \neq \myb{y}$ and $\myb{z}$ not free in $\myapp{\mytmm}{\mytmn}$}}
583 The care required during substituting variables for terms is to avoid
584 name capturing. We will use substitution in the future for other
585 name-binding constructs assuming similar precautions.
587 These few elements have a remarkable expressiveness, and are in fact
588 Turing complete. As a corollary, we must be able to devise a term that
589 reduces forever (`loops' in imperative terms):
591 (\myapp{\omega}{\omega}) \myred (\myapp{\omega}{\omega}) \myred \cdots \text{, with $\omega = \myabs{x}{\myapp{x}{x}}$}
594 A \emph{redex} is a term that can be reduced.
596 In the untyped $\lambda$-calculus this will be the case for an
597 application in which the first term is an abstraction, but in general we
598 call aterm reducible if it appears to the left of a reduction rule.
599 \begin{mydef}[normal form]
600 A term that contains no redexes is said to be in \emph{normal form}.
602 \begin{mydef}[normalising terms and systems]
603 Terms that reduce in a finite number of reduction steps to a normal
604 form are \emph{normalising}. A system in which all terms are
605 normalising is said to be have the \emph{normalisation property}, or
608 Given the reduction behaviour of $(\myapp{\omega}{\omega})$, it is clear
609 that the untyped $\lambda$-calculus does not have the normalisation
612 We have not presented reduction in an algorithmic way, but
613 \emph{evaluation strategies} can be employed to reduce term
614 systematically. Common evaluation strategies include \emph{call by
615 value} (or \emph{strict}), where arguments of abstractions are reduced
616 before being applied to the abstraction; and conversely \emph{call by
617 name} (or \emph{lazy}), where we reduce only when we need to do so to
618 proceed---in other words when we have an application where the function
619 is still not a $\lambda$. In both these reduction strategies we never
620 reduce under an abstraction: for this reason a weaker form of
621 normalisation is used, where both abstractions and normal forms are said
622 to be in \emph{weak head normal form}.
624 \subsection{The simply typed $\lambda$-calculus}
626 A convenient way to `discipline' and reason about $\lambda$-terms is to assign
627 \emph{types} to them, and then check that the terms that we are forming make
628 sense given our typing rules \citep{Curry1934}.The first most basic instance
629 of this idea takes the name of \emph{simply typed $\lambda$-calculus} (STLC).
630 \begin{mydef}[Simply typed $\lambda$-calculus]
631 The syntax and typing rules for the STLC are given in Figure \ref{fig:stlc}.
634 Our types contain a set of \emph{type variables} $\Phi$, which might
635 correspond to some `primitive' types; and $\myarr$, the type former for
636 `arrow' types, the types of functions. The language is explicitly
637 typed: when we bring a variable into scope with an abstraction, we
638 declare its type. Reduction is unchanged from the untyped
644 \begin{array}{r@{\ }c@{\ }l}
645 \mytmsyn & ::= & \myb{x} \mysynsep \myabss{\myb{x}}{\mytysyn}{\mytmsyn} \mysynsep
646 (\myapp{\mytmsyn}{\mytmsyn}) \\
647 \mytysyn & ::= & \myse{\phi} \mysynsep \mytysyn \myarr \mytysyn \mysynsep \\
648 \myb{x} & \in & \text{Some enumerable set of symbols} \\
649 \myse{\phi} & \in & \Phi
654 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
656 \AxiomC{$\myctx(x) = A$}
657 \UnaryInfC{$\myjud{\myb{x}}{A}$}
660 \AxiomC{$\myjudd{\myctx;\myb{x} : A}{\mytmt}{\mytyb}$}
661 \UnaryInfC{$\myjud{\myabss{x}{A}{\mytmt}}{\mytyb}$}
664 \AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$}
665 \AxiomC{$\myjud{\mytmn}{\mytya}$}
666 \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mytyb}$}
670 \caption{Syntax and typing rules for the STLC. Reduction is unchanged from
671 the untyped $\lambda$-calculus.}
675 In the typing rules, a context $\myctx$ is used to store the types of bound
676 variables: $\myctx; \myb{x} : \mytya$ adds a variable to the context and
677 $\myctx(x)$ extracts the type of the rightmost occurrence of $x$.
679 This typing system takes the name of `simply typed lambda calculus' (STLC), and
680 enjoys a number of properties. Two of them are expected in most type systems
682 \begin{mydef}[Progress]
683 A well-typed term is not stuck---it is either a variable, or it
684 does not appear on the left of the $\myred$ relation (currently
685 only $\lambda$), or it can take a step according to the evaluation rules.
687 \begin{mydef}[Subject reduction]
688 If a well-typed term takes a step of evaluation, then the
689 resulting term is also well-typed, and preserves the previous type.
692 However, STLC buys us much more: every well-typed term is normalising
693 \citep{Tait1967}. It is easy to see that we cannot fill the blanks if we want to
694 give types to the non-normalising term shown before:
696 \myapp{(\myabss{\myb{x}}{\myhole{?}}{\myapp{\myb{x}}{\myb{x}}})}{(\myabss{\myb{x}}{\myhole{?}}{\myapp{\myb{x}}{\myb{x}}})}
698 This makes the STLC Turing incomplete. We can recover the ability to loop by
699 adding a combinator that recurses:
700 \begin{mydef}[Fixed-point combinator]\end{mydef}
703 \begin{minipage}{0.5\textwidth}
705 $ \mytmsyn ::= \cdots b \mysynsep \myfix{\myb{x}}{\mytysyn}{\mytmsyn} $
709 \begin{minipage}{0.5\textwidth}
710 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}} {
711 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytmt}{\mytya}$}
712 \UnaryInfC{$\myjud{\myfix{\myb{x}}{\mytya}{\mytmt}}{\mytya}$}
717 \mydesc{reduction:}{\myjud{\mytmsyn}{\mytmsyn}}{
718 $ \myfix{\myb{x}}{\mytya}{\mytmt} \myred \mysub{\mytmt}{\myb{x}}{(\myfix{\myb{x}}{\mytya}{\mytmt})}$
721 This will deprive us of normalisation, which is a particularly bad thing if we
722 want to use the STLC as described in the next section.
724 Another important property of the STLC is the Church-Rosser property:
725 \begin{mydef}[Church-Rosser property]
726 A system is said to have the \emph{Church-Rosser} property, or to be
727 \emph{confluent}, if given any two reductions $\mytmm$ and $\mytmn$ of
728 a given term $\mytmt$, there is exist a term to which both $\mytmm$
729 and $\mytmn$ can be reduced.
731 Given that the STLC has the normalisation property and the Church-Rosser
732 property, each term has a unique normal form for definitional equality
735 \subsection{The Curry-Howard correspondence}
737 As hinted in the introduction, it turns out that the STLC can be seen a
738 natural deduction system for intuitionistic propositional logic. Terms
739 correspond to proofs, and their types correspond to the propositions
740 they prove. This remarkable fact is known as the Curry-Howard
741 correspondence, or isomorphism.
743 The arrow ($\myarr$) type corresponds to implication. If we wish to prove that
744 that $(\mytya \myarr \mytyb) \myarr (\mytyb \myarr \mytycc) \myarr (\mytya
745 \myarr \mytycc)$, all we need to do is to devise a $\lambda$-term that has the
748 \myabss{\myb{f}}{(\mytya \myarr \mytyb)}{\myabss{\myb{g}}{(\mytyb \myarr \mytycc)}{\myabss{\myb{x}}{\mytya}{\myapp{\myb{g}}{(\myapp{\myb{f}}{\myb{x}})}}}}
750 Which is known to functional programmers as function composition. Going
751 beyond arrow types, we can extend our bare lambda calculus with useful
752 types to represent other logical constructs.
753 \begin{mydef}[The extended STLC]
754 Figure \ref{fig:natded} shows syntax, reduction, and typing rules for
755 the \emph{extendend simply typed $\lambda$-calculus}.
761 \begin{array}{r@{\ }c@{\ }l}
762 \mytmsyn & ::= & \cdots \\
763 & | & \mytt \mysynsep \myapp{\myabsurd{\mytysyn}}{\mytmsyn} \\
764 & | & \myapp{\myleft{\mytysyn}}{\mytmsyn} \mysynsep
765 \myapp{\myright{\mytysyn}}{\mytmsyn} \mysynsep
766 \myapp{\mycase{\mytmsyn}{\mytmsyn}}{\mytmsyn} \\
767 & | & \mypair{\mytmsyn}{\mytmsyn} \mysynsep
768 \myapp{\myfst}{\mytmsyn} \mysynsep \myapp{\mysnd}{\mytmsyn} \\
769 \mytysyn & ::= & \cdots \mysynsep \myunit \mysynsep \myempty \mysynsep \mytmsyn \mysum \mytmsyn \mysynsep \mytysyn \myprod \mytysyn
774 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
777 \begin{array}{l@{ }l@{\ }c@{\ }l}
778 \myapp{\mycase{\mytmm}{\mytmn}}{(\myapp{\myleft{\mytya} &}{\mytmt})} & \myred &
779 \myapp{\mytmm}{\mytmt} \\
780 \myapp{\mycase{\mytmm}{\mytmn}}{(\myapp{\myright{\mytya} &}{\mytmt})} & \myred &
781 \myapp{\mytmn}{\mytmt}
786 \begin{array}{l@{ }l@{\ }c@{\ }l}
787 \myapp{\myfst &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmm \\
788 \myapp{\mysnd &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmn
794 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
796 \AxiomC{\phantom{$\myjud{\mytmt}{\myempty}$}}
797 \UnaryInfC{$\myjud{\mytt}{\myunit}$}
800 \AxiomC{$\myjud{\mytmt}{\myempty}$}
801 \UnaryInfC{$\myjud{\myapp{\myabsurd{\mytya}}{\mytmt}}{\mytya}$}
808 \AxiomC{$\myjud{\mytmt}{\mytya}$}
809 \UnaryInfC{$\myjud{\myapp{\myleft{\mytyb}}{\mytmt}}{\mytya \mysum \mytyb}$}
812 \AxiomC{$\myjud{\mytmt}{\mytyb}$}
813 \UnaryInfC{$\myjud{\myapp{\myright{\mytya}}{\mytmt}}{\mytya \mysum \mytyb}$}
821 \AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$}
822 \AxiomC{$\myjud{\mytmn}{\mytya \myarr \mytycc}$}
823 \AxiomC{$\myjud{\mytmt}{\mytya \mysum \mytyb}$}
824 \TrinaryInfC{$\myjud{\myapp{\mycase{\mytmm}{\mytmn}}{\mytmt}}{\mytycc}$}
831 \AxiomC{$\myjud{\mytmm}{\mytya}$}
832 \AxiomC{$\myjud{\mytmn}{\mytyb}$}
833 \BinaryInfC{$\myjud{\mypair{\mytmm}{\mytmn}}{\mytya \myprod \mytyb}$}
836 \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
837 \UnaryInfC{$\myjud{\myapp{\myfst}{\mytmt}}{\mytya}$}
840 \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
841 \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mytyb}$}
845 \caption{Rules for the extendend STLC. Only the new features are shown, all the
846 rules and syntax for the STLC apply here too.}
850 Tagged unions (or sums, or coproducts---$\mysum$ here, \texttt{Either}
851 in Haskell) correspond to disjunctions, and dually tuples (or pairs, or
852 products---$\myprod$ here, tuples in Haskell) correspond to
853 conjunctions. This is apparent looking at the ways to construct and
854 destruct the values inhabiting those types: for $\mysum$ $\myleft{ }$
855 and $\myright{ }$ correspond to $\vee$ introduction, and
856 $\mycase{\myarg}{\myarg}$ to $\vee$ elimination; for $\myprod$
857 $\mypair{\myarg}{\myarg}$ corresponds to $\wedge$ introduction, $\myfst$
858 and $\mysnd$ to $\wedge$ elimination.
860 The trivial type $\myunit$ corresponds to the logical $\top$ (true), and
861 dually $\myempty$ corresponds to the logical $\bot$ (false). $\myunit$
862 has one introduction rule ($\mytt$), and thus one inhabitant; and no
863 eliminators. $\myempty$ has no introduction rules, and thus no
864 inhabitants; and one eliminator ($\myabsurd{ }$), corresponding to the
865 logical \emph{ex falso quodlibet}.
867 With these rules, our STLC now looks remarkably similar in power and use to the
868 natural deduction we already know.
869 \begin{mydef}[Negation]
870 $\myneg \mytya$ can be expressed as $\mytya \myarr \myempty$.
872 However, there is an important omission: there is no term of
873 the type $\mytya \mysum \myneg \mytya$ (excluded middle), or equivalently
874 $\myneg \myneg \mytya \myarr \mytya$ (double negation), or indeed any term with
875 a type equivalent to those.
877 This has a considerable effect on our logic and it is no coincidence, since there
878 is no obvious computational behaviour for laws like the excluded middle.
879 Logics of this kind are called \emph{intuitionistic}, or \emph{constructive},
880 and all the systems analysed will have this characteristic since they build on
881 the foundation of the STLC.\footnote{There is research to give computational
882 behaviour to classical logic, but I will not touch those subjects.}
884 As in logic, if we want to keep our system consistent, we must make sure that no
885 closed terms (in other words terms not under a $\lambda$) inhabit $\myempty$.
886 The variant of STLC presented here is indeed
887 consistent, a result that follows from the fact that it is
889 Going back to our $\mysyn{fix}$ combinator, it is easy to see how it ruins our
890 desire for consistency. The following term works for every type $\mytya$,
892 \[(\myfix{\myb{x}}{\mytya}{\myb{x}}) : \mytya\]
894 \subsection{Inductive data}
897 To make the STLC more useful as a programming language or reasoning tool it is
898 common to include (or let the user define) inductive data types. These comprise
899 of a type former, various constructors, and an eliminator (or destructor) that
900 serves as primitive recursor.
902 \begin{mydef}[Finite lists for the STLC]
903 We add a $\mylist$ type constructor, along with an `empty
904 list' ($\mynil{ }$) and `cons cell' ($\mycons$) constructor. The eliminator for
905 lists will be the usual folding operation ($\myfoldr$). Full rules in Figure
912 \begin{array}{r@{\ }c@{\ }l}
913 \mytmsyn & ::= & \cdots \mysynsep \mynil{\mytysyn} \mysynsep \mytmsyn \mycons \mytmsyn
915 \myapp{\myapp{\myapp{\myfoldr}{\mytmsyn}}{\mytmsyn}}{\mytmsyn} \\
916 \mytysyn & ::= & \cdots \mysynsep \myapp{\mylist}{\mytysyn}
920 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
922 \begin{array}{l@{\ }c@{\ }l}
923 \myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{\mynil{\mytya}} & \myred & \mytmt \\
925 \myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{(\mytmm \mycons \mytmn)} & \myred &
926 \myapp{\myapp{\myse{f}}{\mytmm}}{(\myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{\mytmn})}
930 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
932 \AxiomC{\phantom{$\myjud{\mytmm}{\mytya}$}}
933 \UnaryInfC{$\myjud{\mynil{\mytya}}{\myapp{\mylist}{\mytya}}$}
936 \AxiomC{$\myjud{\mytmm}{\mytya}$}
937 \AxiomC{$\myjud{\mytmn}{\myapp{\mylist}{\mytya}}$}
938 \BinaryInfC{$\myjud{\mytmm \mycons \mytmn}{\myapp{\mylist}{\mytya}}$}
943 \AxiomC{$\myjud{\mysynel{f}}{\mytya \myarr \mytyb \myarr \mytyb}$}
944 \AxiomC{$\myjud{\mytmm}{\mytyb}$}
945 \AxiomC{$\myjud{\mytmn}{\myapp{\mylist}{\mytya}}$}
946 \TrinaryInfC{$\myjud{\myapp{\myapp{\myapp{\myfoldr}{\mysynel{f}}}{\mytmm}}{\mytmn}}{\mytyb}$}
949 \caption{Rules for lists in the STLC.}
953 In Section \ref{sec:well-order} we will see how to give a general account of
956 \section{Intuitionistic Type Theory}
959 \subsection{Extending the STLC}
961 The STLC can be made more expressive in various ways. \cite{Barendregt1991}
962 succinctly expressed geometrically how we can add expressivity:
965 & \lambda\omega \ar@{-}[rr]\ar@{-}'[d][dd]
966 & & \lambda C \ar@{-}[dd]
968 \lambda2 \ar@{-}[ur]\ar@{-}[rr]\ar@{-}[dd]
969 & & \lambda P2 \ar@{-}[ur]\ar@{-}[dd]
971 & \lambda\underline\omega \ar@{-}'[r][rr]
972 & & \lambda P\underline\omega
974 \lambda{\to} \ar@{-}[rr]\ar@{-}[ur]
975 & & \lambda P \ar@{-}[ur]
978 Here $\lambda{\to}$, in the bottom left, is the STLC. From there can move along
981 \item[Terms depending on types (towards $\lambda{2}$)] We can quantify over
982 types in our type signatures. For example, we can define a polymorphic
983 identity function, where $\mytyp$ denotes the `type of types':
985 (\myabss{\myb{A}}{\mytyp}{\myabss{\myb{x}}{\myb{A}}{\myb{x}}}) : (\myb{A} {:} \mytyp) \myarr \myb{A} \myarr \myb{A}
987 The first and most famous instance of this idea has been System F.
988 This form of polymorphism and has been wildly successful, also thanks
989 to a well known inference algorithm for a restricted version of System
990 F known as Hindley-Milner \citep{milner1978theory}. Languages like
991 Haskell and SML are based on this discipline.
992 \item[Types depending on types (towards $\lambda{\underline{\omega}}$)] We have
993 type operators. For example we could define a function that given types $R$
994 and $\mytya$ forms the type that represents a value of type $\mytya$ in
995 continuation passing style:
996 \[\displaystyle(\myabss{\myb{A} \myar \myb{R}}{\mytyp}{(\myb{A}
997 \myarr \myb{R}) \myarr \myb{R}}) : \mytyp \myarr \mytyp \myarr \mytyp
999 \item[Types depending on terms (towards $\lambda{P}$)] Also known as `dependent
1000 types', give great expressive power. For example, we can have values of whose
1001 type depend on a boolean:
1002 \[\displaystyle(\myabss{\myb{x}}{\mybool}{\myite{\myb{x}}{\mynat}{\myrat}}) : \mybool
1006 All the systems preserve the properties that make the STLC well behaved. The
1007 system we are going to focus on, Intuitionistic Type Theory, has all of the
1008 above additions, and thus would sit where $\lambda{C}$ sits in the
1009 `$\lambda$-cube'. It will serve as the logical `core' of all the other
1010 extensions that we will present and ultimately our implementation of a similar
1013 \subsection{A Bit of History}
1015 Logic frameworks and programming languages based on type theory have a
1016 long history. Per Martin-L\"{o}f described the first version of his
1017 theory in 1971, but then revised it since the original version was
1018 inconsistent due to its impredicativity.\footnote{In the early version
1019 there was only one universe $\mytyp$ and $\mytyp : \mytyp$; see
1020 Section \ref{sec:term-types} for an explanation on why this causes
1021 problems.} For this reason he later gave a revised and consistent
1022 definition \citep{Martin-Lof1984}.
1024 A related development is the polymorphic $\lambda$-calculus, and specifically
1025 the previously mentioned System F, which was developed independently by Girard
1026 and Reynolds. An overview can be found in \citep{Reynolds1994}. The surprising
1027 fact is that while System F is impredicative it is still consistent and strongly
1028 normalising. \cite{Coquand1986} further extended this line of work with the
1029 Calculus of Constructions (CoC).
1031 Most widely used interactive theorem provers are based on ITT. Popular ones
1032 include Agda \citep{Norell2007, Bove2009}, Coq \citep{Coq}, and Epigram
1033 \citep{McBride2004, EpigramTut}.
1035 \subsection{A simple type theory}
1038 The calculus I present follows the exposition in \citep{Thompson1991},
1039 and is quite close to the original formulation of predicative ITT as
1040 found in \citep{Martin-Lof1984}.
1041 \begin{mydef}[Intuitionistic Type Theory (ITT)]
1042 The syntax and reduction rules are shown in Figure \ref{fig:core-tt-syn}.
1043 The typing rules are presented piece by piece in the following sections.
1045 Agda and \mykant\ renditions of the presented theory and all the
1046 examples is reproduced in Appendix \ref{app:itt-code}.
1051 \begin{array}{r@{\ }c@{\ }l}
1052 \mytmsyn & ::= & \myb{x} \mysynsep
1053 \mytyp_{level} \mysynsep
1054 \myunit \mysynsep \mytt \mysynsep
1055 \myempty \mysynsep \myapp{\myabsurd{\mytmsyn}}{\mytmsyn} \\
1056 & | & \mybool \mysynsep \mytrue \mysynsep \myfalse \mysynsep
1057 \myitee{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
1058 & | & \myfora{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
1059 \myabss{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
1060 (\myapp{\mytmsyn}{\mytmsyn}) \\
1061 & | & \myexi{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
1062 \mypairr{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn} \\
1063 & | & \myapp{\myfst}{\mytmsyn} \mysynsep \myapp{\mysnd}{\mytmsyn} \\
1064 & | & \myw{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
1065 \mytmsyn \mynode{\myb{x}}{\mytmsyn} \mytmsyn \\
1066 & | & \myrec{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn} \\
1067 level & \in & \mathbb{N}
1072 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
1073 \begin{tabular}{ccc}
1075 \begin{array}{l@{ }l@{\ }c@{\ }l}
1076 \myitee{\mytrue &}{\myb{x}}{\myse{P}}{\mytmm}{\mytmn} & \myred & \mytmm \\
1077 \myitee{\myfalse &}{\myb{x}}{\myse{P}}{\mytmm}{\mytmn} & \myred & \mytmn \\
1082 \myapp{(\myabss{\myb{x}}{\mytya}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{\myb{x}}{\mytmn}
1086 \begin{array}{l@{ }l@{\ }c@{\ }l}
1087 \myapp{\myfst &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmm \\
1088 \myapp{\mysnd &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmn
1096 \myrec{(\myse{s} \mynode{\myb{x}}{\myse{T}} \myse{f})}{\myb{y}}{\myse{P}}{\myse{p}} \myred
1097 \myapp{\myapp{\myapp{\myse{p}}{\myse{s}}}{\myse{f}}}{(\myabss{\myb{t}}{\mysub{\myse{T}}{\myb{x}}{\myse{s}}}{
1098 \myrec{\myapp{\myse{f}}{\myb{t}}}{\myb{y}}{\myse{P}}{\mytmt}
1102 \caption{Syntax and reduction rules for our type theory.}
1103 \label{fig:core-tt-syn}
1106 \subsubsection{Types are terms, some terms are types}
1107 \label{sec:term-types}
1109 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1111 \AxiomC{$\myjud{\mytmt}{\mytya}$}
1112 \AxiomC{$\mytya \mydefeq \mytyb$}
1113 \BinaryInfC{$\myjud{\mytmt}{\mytyb}$}
1116 \AxiomC{\phantom{$\myjud{\mytmt}{\mytya}$}}
1117 \UnaryInfC{$\myjud{\mytyp_l}{\mytyp_{l + 1}}$}
1122 The first thing to notice is that a barrier between values and types that we had
1123 in the STLC is gone: values can appear in types, and the two are treated
1124 uniformly in the syntax.
1126 While the usefulness of doing this will become clear soon, a consequence is
1127 that since types can be the result of computation, deciding type equality is
1128 not immediate as in the STLC. For this reason we define \emph{definitional
1129 equality}, $\mydefeq$, as the congruence relation extending
1130 $\myred$---moreover, when comparing types syntactically we do it up to
1131 renaming of bound names ($\alpha$-renaming). For example under this
1132 discipline we will find that
1134 \myabss{\myb{x}}{\mytya}{\myb{x}} \mydefeq \myabss{\myb{y}}{\mytya}{\myb{y}}
1136 Types that are definitionally equal can be used interchangeably. Here
1137 the `conversion' rule is not syntax directed, but it is possible to
1138 employ $\myred$ to decide term equality in a systematic way, comparing
1139 terms by reducing to their normal forms and then comparing them
1140 syntactically; so that a separate conversion rule is not needed.
1141 Another thing to notice is that considering the need to reduce terms to
1142 decide equality it is essential for a dependently typed system to be
1143 terminating and confluent for type checking to be decidable, since every
1144 type needs to have a \emph{unique} normal form.
1146 Moreover, we specify a \emph{type hierarchy} to talk about `large'
1147 types: $\mytyp_0$ will be the type of types inhabited by data:
1148 $\mybool$, $\mynat$, $\mylist$, etc. $\mytyp_1$ will be the type of
1149 $\mytyp_0$, and so on---for example we have $\mytrue : \mybool :
1150 \mytyp_0 : \mytyp_1 : \cdots$. Each type `level' is often called a
1151 universe in the literature. While it is possible to simplify things by
1152 having only one universe $\mytyp$ with $\mytyp : \mytyp$, this plan is
1153 inconsistent for much the same reason that impredicative na\"{\i}ve set
1154 theory is \citep{Hurkens1995}. However various techniques can be
1155 employed to lift the burden of explicitly handling universes, as we will
1156 see in Section \ref{sec:term-hierarchy}.
1158 \subsubsection{Contexts}
1160 \begin{minipage}{0.5\textwidth}
1161 \mydesc{context validity:}{\myvalid{\myctx}}{
1163 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
1164 \UnaryInfC{$\myvalid{\myemptyctx}$}
1167 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
1168 \UnaryInfC{$\myvalid{\myctx ; \myb{x} : \mytya}$}
1173 \begin{minipage}{0.5\textwidth}
1174 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1175 \AxiomC{$\myctx(x) = \mytya$}
1176 \UnaryInfC{$\myjud{\myb{x}}{\mytya}$}
1182 We need to refine the notion context to make sure that every variable appearing
1183 is typed correctly, or that in other words each type appearing in the context is
1184 indeed a type and not a value. In every other rule, if no premises are present,
1185 we assume the context in the conclusion to be valid.
1187 Then we can re-introduce the old rule to get the type of a variable for a
1190 \subsubsection{$\myunit$, $\myempty$}
1192 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1193 \begin{tabular}{ccc}
1194 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
1195 \UnaryInfC{$\myjud{\myunit}{\mytyp_0}$}
1197 \UnaryInfC{$\myjud{\myempty}{\mytyp_0}$}
1200 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
1201 \UnaryInfC{$\myjud{\mytt}{\myunit}$}
1203 \UnaryInfC{\phantom{$\myjud{\myempty}{\mytyp_0}$}}
1206 \AxiomC{$\myjud{\mytmt}{\myempty}$}
1207 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
1208 \BinaryInfC{$\myjud{\myapp{\myabsurd{\mytya}}{\mytmt}}{\mytya}$}
1210 \UnaryInfC{\phantom{$\myjud{\myempty}{\mytyp_0}$}}
1215 Nothing surprising here: $\myunit$ and $\myempty$ are unchanged from the STLC,
1216 with the added rules to type $\myunit$ and $\myempty$ themselves, and to make
1217 sure that we are invoking $\myabsurd{}$ over a type.
1219 \subsubsection{$\mybool$, and dependent $\myfun{if}$}
1221 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1222 \begin{tabular}{ccc}
1224 \UnaryInfC{$\myjud{\mybool}{\mytyp_0}$}
1228 \UnaryInfC{$\myjud{\mytrue}{\mybool}$}
1232 \UnaryInfC{$\myjud{\myfalse}{\mybool}$}
1237 \AxiomC{$\myjud{\mytmt}{\mybool}$}
1238 \AxiomC{$\myjudd{\myctx : \mybool}{\mytya}{\mytyp_l}$}
1240 \BinaryInfC{$\myjud{\mytmm}{\mysub{\mytya}{x}{\mytrue}}$ \hspace{0.7cm} $\myjud{\mytmn}{\mysub{\mytya}{x}{\myfalse}}$}
1241 \UnaryInfC{$\myjud{\myitee{\mytmt}{\myb{x}}{\mytya}{\mytmm}{\mytmn}}{\mysub{\mytya}{\myb{x}}{\mytmt}}$}
1245 With booleans we get the first taste of the `dependent' in `dependent
1246 types'. While the two introduction rules for $\mytrue$ and $\myfalse$
1247 are not surprising, the typing rules for $\myfun{if}$ are. In most
1248 strongly typed languages we expect the branches of an $\myfun{if}$
1249 statements to be of the same type, to preserve subject reduction, since
1250 execution could take both paths. This is a pity, since the type system
1251 does not reflect the fact that in each branch we gain knowledge on the
1252 term we are branching on. Which means that programs along the lines of
1254 if null xs then head xs else 0
1256 are a necessary, well-typed, danger.
1258 However, in a more expressive system, we can do better: the branches' type can
1259 depend on the value of the scrutinised boolean. This is what the typing rule
1260 expresses: the user provides a type $\mytya$ ranging over an $\myb{x}$
1261 representing the scrutinised boolean type, and the branches are typechecked with
1262 the updated knowledge on the value of $\myb{x}$.
1264 \subsubsection{$\myarr$, or dependent function}
1267 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1268 \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
1269 \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
1270 \BinaryInfC{$\myjud{\myfora{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
1276 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytmt}{\mytyb}$}
1277 \UnaryInfC{$\myjud{\myabss{\myb{x}}{\mytya}{\mytmt}}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
1280 \AxiomC{$\myjud{\mytmm}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
1281 \AxiomC{$\myjud{\mytmn}{\mytya}$}
1282 \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mysub{\mytyb}{\myb{x}}{\mytmn}}$}
1287 Dependent functions are one of the two key features that perhaps most
1288 characterise dependent types---the other being dependent products. With
1289 dependent functions, the result type can depend on the value of the
1290 argument. This feature, together with the fact that the result type
1291 might be a type itself, brings a lot of interesting possibilities.
1292 Following this intuition, in the introduction rule, the return type is
1293 typechecked in a context with an abstracted variable of lhs' type, and
1294 in the elimination rule the actual argument is substituted in the return
1295 type. Keeping the correspondence with logic alive, dependent functions
1296 are much like universal quantifiers ($\forall$) in logic.
1298 For example, assuming that we have lists and natural numbers in our
1299 language, using dependent functions we can write functions of types
1302 \myfun{length} : (\myb{A} {:} \mytyp_0) \myarr \myapp{\mylist}{\myb{A}} \myarr \mynat \\
1303 \myarg \myfun{$>$} \myarg : \mynat \myarr \mynat \myarr \mytyp_0 \\
1304 \myfun{head} : (\myb{A} {:} \mytyp_0) \myarr (\myb{l} {:} \myapp{\mylist}{\myb{A}})
1305 \myarr \myapp{\myapp{\myfun{length}}{\myb{A}}}{\myb{l}} \mathrel{\myfun{$>$}} 0 \myarr
1310 \myfun{length} is the usual polymorphic length
1311 function. $\myarg\myfun{$>$}\myarg$ is a function that takes two naturals
1312 and returns a type: if the lhs is greater then the rhs, $\myunit$ is
1313 returned, $\myempty$ otherwise. This way, we can express a
1314 `non-emptyness' condition in $\myfun{head}$, by including a proof that
1315 the length of the list argument is non-zero. This allows us to rule out
1316 the `empty list' case, so that we can safely return the first element.
1319 Again, we need to make sure that the type hierarchy is respected, which
1320 is the reason why a type formed by $\myarr$ will live in the least upper
1321 bound of the levels of argument and return type. If this was not the
1322 case, we would be able to form a `powerset' function along the lines of
1325 \myfun{P} : \mytyp_0 \myarr \mytyp_0 \\
1326 \myfun{P} \myappsp \myb{A} \mapsto \myb{A} \myarr \mytyp_0
1329 Where the type of $\myb{A} \myarr \mytyp_0$ is in $\mytyp_0$ itself.
1330 Using this and similar devices we would be able to derive falsity
1331 \citep{Hurkens1995}. This trend will continue with the other type-level
1332 binders, $\myprod$ and $\mytyc{W}$.
1334 \subsubsection{$\myprod$, or dependent product}
1337 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1338 \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
1339 \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
1340 \BinaryInfC{$\myjud{\myexi{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
1346 \AxiomC{$\myjud{\mytmm}{\mytya}$}
1347 \AxiomC{$\myjud{\mytmn}{\mysub{\mytyb}{\myb{x}}{\mytmm}}$}
1348 \BinaryInfC{$\myjud{\mypairr{\mytmm}{\myb{x}}{\mytyb}{\mytmn}}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
1350 \UnaryInfC{\phantom{$--$}}
1353 \AxiomC{$\myjud{\mytmt}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
1354 \UnaryInfC{$\hspace{0.7cm}\myjud{\myapp{\myfst}{\mytmt}}{\mytya}\hspace{0.7cm}$}
1356 \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mysub{\mytyb}{\myb{x}}{\myapp{\myfst}{\mytmt}}}$}
1361 If dependent functions are a generalisation of $\myarr$ in the STLC,
1362 dependent products are a generalisation of $\myprod$ in the STLC. The
1363 improvement is that the second element's type can depend on the value of
1364 the first element. The corrispondence with logic is through the
1365 existential quantifier: $\exists x \in \mathbb{N}. even(x)$ can be
1366 expressed as $\myexi{\myb{x}}{\mynat}{\myapp{\myfun{even}}{\myb{x}}}$.
1367 The first element will be a number, and the second evidence that the
1368 number is even. This highlights the fact that we are working in a
1369 constructive logic: if we have an existence proof, we can always ask for
1370 a witness. This means, for instance, that $\neg \forall \neg$ is not
1371 equivalent to $\exists$.
1373 Another perhaps more `dependent' application of products, paired with
1374 $\mybool$, is to offer choice between different types. For example we
1375 can easily recover disjunctions:
1378 \myarg\myfun{$\vee$}\myarg : \mytyp_0 \myarr \mytyp_0 \myarr \mytyp_0 \\
1379 \myb{A} \mathrel{\myfun{$\vee$}} \myb{B} \mapsto \myexi{\myb{x}}{\mybool}{\myite{\myb{x}}{\myb{A}}{\myb{B}}} \\ \ \\
1380 \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} \\
1381 \myfun{case} \myappsp \myb{A} \myappsp \myb{B} \myappsp \myb{C} \myappsp \myb{f} \myappsp \myb{g} \myappsp \myb{x} \mapsto \\
1382 \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}})}
1386 \subsubsection{$\mytyc{W}$, or well-order}
1387 \label{sec:well-order}
1389 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1391 \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
1392 \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
1393 \BinaryInfC{$\myjud{\myw{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
1398 \AxiomC{$\myjud{\mytmt}{\mytya}$}
1399 \AxiomC{$\myjud{\mysynel{f}}{\mysub{\mytyb}{\myb{x}}{\mytmt} \myarr \myw{\myb{x}}{\mytya}{\mytyb}}$}
1400 \BinaryInfC{$\myjud{\mytmt \mynode{\myb{x}}{\mytyb} \myse{f}}{\myw{\myb{x}}{\mytya}{\mytyb}}$}
1406 \AxiomC{$\myjud{\myse{u}}{\myw{\myb{x}}{\myse{S}}{\myse{T}}}$}
1407 \AxiomC{$\myjudd{\myctx; \myb{w} : \myw{\myb{x}}{\myse{S}}{\myse{T}}}{\myse{P}}{\mytyp_l}$}
1409 \BinaryInfC{$\myjud{\myse{p}}{
1410 \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}}}}
1412 \UnaryInfC{$\myjud{\myrec{\myse{u}}{\myb{w}}{\myse{P}}{\myse{p}}}{\mysub{\myse{P}}{\myb{w}}{\myse{u}}}$}
1416 Finally, the well-order type, or in short $\mytyc{W}$-type, which will
1417 let us represent inductive data in a general (but clumsy) way. We can
1418 form `nodes' of the shape $\mytmt \mynode{\myb{x}}{\mytyb} \myse{f} :
1419 \myw{\myb{x}}{\mytya}{\mytyb}$ that contain data ($\mytmt$) of type and
1420 one `child' for each member of $\mysub{\mytyb}{\myb{x}}{\mytmt}$. The
1421 $\myfun{rec}\ \myfun{with}$ acts as an induction principle on
1422 $\mytyc{W}$, given a predicate and a function dealing with the inductive
1423 case---we will gain more intuition about inductive data in ITT in
1424 Section \ref{sec:user-type}.
1426 For example, if we want to form natural numbers, we can take
1429 \mytyc{Tr} : \mybool \myarr \mytyp_0 \\
1430 \mytyc{Tr} \myappsp \myb{b} \mapsto \myfun{if}\, \myb{b}\, \myfun{then}\, \myunit\, \myfun{else}\, \myempty \\
1432 \mynat : \mytyp_0 \\
1433 \mynat \mapsto \myw{\myb{b}}{\mybool}{(\mytyc{Tr}\myappsp\myb{b})}
1436 Each node will contain a boolean. If $\mytrue$, the number is non-zero,
1437 and we will have one child representing its predecessor, given that
1438 $\mytyc{Tr}$ will return $\myunit$. If $\myfalse$, the number is zero,
1439 and we will have no predecessors (children), given the $\myempty$:
1442 \mydc{zero} : \mynat \\
1443 \mydc{zero} \mapsto \myfalse \mynodee (\myabs{\myb{x}}{\myabsurd{\mynat} \myappsp \myb{x}}) \\
1445 \mydc{suc} : \mynat \myarr \mynat \\
1446 \mydc{suc}\myappsp \myb{x} \mapsto \mytrue \mynodee (\myabs{\myarg}{\myb{x}})
1449 And with a bit of effort, we can recover addition:
1452 \myfun{plus} : \mynat \myarr \mynat \myarr \mynat \\
1453 \myfun{plus} \myappsp \myb{x} \myappsp \myb{y} \mapsto \\
1454 \myind{2} \myfun{rec}\, \myb{x} / \myb{b}.\mynat \, \\
1455 \myind{2} \myfun{with}\, \myabs{\myb{b}}{\\
1456 \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) \\
1457 \myind{2}\myind{2}\myfun{then}\,(\myabs{\myarg\, \myb{f}}{\mydc{suc}\myappsp (\myapp{\myb{f}}{\mytt})})\, \myfun{else}\, (\myabs{\myarg\, \myarg}{\myb{y}})}
1460 Note how we explicitly have to type the branches to make them match
1461 with the definition of $\mynat$. This gives a taste of the
1462 `clumsiness' of $\mytyc{W}$-types but not the whole story: well-orders
1463 are inadequate not only because they are verbose, but present deeper
1464 problems because the notion of equality present in most type theory
1465 (which we will present in the next section) is too weak
1466 \citep{dybjer1997representing}. The `better' equality we will present
1467 in Section \ref{sec:ott} helps but does not fully resolve these
1468 issues.\footnote{See \url{http://www.e-pig.org/epilogue/?p=324}, which
1469 concludes with `W-types are a powerful conceptual tool, but they’re
1470 no basis for an implementation of recursive datatypes in decidable
1471 type theories.'} For this reasons \mytyc{W}-types have remained
1472 nothing more than a reasoning tool, and practical systems implement
1473 more expressive ways to represent data.
1475 \section{The struggle for equality}
1476 \label{sec:equality}
1478 In the previous section we saw how a type checker (or a human) needs a
1479 notion of \emph{definitional equality}. Beyond this meta-theoretic
1480 notion, in this section we will explore the ways of expressing equality
1481 \emph{inside} the theory, as a reasoning tool available to the user.
1482 This area is the main concern of this thesis, and in general a very
1483 active research topic, since we do not have a fully satisfactory
1484 solution, yet. As in the previous section, everything presented is
1485 formalised in Agda in Appendix \ref{app:agda-itt}.
1487 \subsection{Propositional equality}
1489 \begin{mydef}[Propositional equality] The syntax, reduction, and typing
1490 rules for propositional equality and related constructs is defined as:
1494 \begin{minipage}{0.5\textwidth}
1497 \begin{array}{r@{\ }c@{\ }l}
1498 \mytmsyn & ::= & \cdots \\
1499 & | & \mypeq \myappsp \mytmsyn \myappsp \mytmsyn \myappsp \mytmsyn \mysynsep
1500 \myapp{\myrefl}{\mytmsyn} \\
1501 & | & \myjeq{\mytmsyn}{\mytmsyn}{\mytmsyn}
1506 \begin{minipage}{0.5\textwidth}
1507 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
1509 \myjeq{\myse{P}}{(\myapp{\myrefl}{\mytmm})}{\mytmn} \myred \mytmn
1515 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1516 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
1517 \AxiomC{$\myjud{\mytmm}{\mytya}$}
1518 \AxiomC{$\myjud{\mytmn}{\mytya}$}
1519 \TrinaryInfC{$\myjud{\mypeq \myappsp \mytya \myappsp \mytmm \myappsp \mytmn}{\mytyp_l}$}
1525 \AxiomC{$\begin{array}{c}\ \\\myjud{\mytmm}{\mytya}\hspace{1.1cm}\mytmm \mydefeq \mytmn\end{array}$}
1526 \UnaryInfC{$\myjud{\myapp{\myrefl}{\mytmm}}{\mypeq \myappsp \mytya \myappsp \mytmm \myappsp \mytmn}$}
1531 \myjud{\myse{P}}{\myfora{\myb{x}\ \myb{y}}{\mytya}{\myfora{q}{\mypeq \myappsp \mytya \myappsp \myb{x} \myappsp \myb{y}}{\mytyp_l}}} \\
1532 \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})}}
1535 \UnaryInfC{$\myjud{\myjeq{\myse{P}}{\myse{q}}{\myse{p}}}{\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmn}}{q}}$}
1540 To express equality between two terms inside ITT, the obvious way to do
1541 so is to have equality to be a type. Here we present what has survived
1542 as the dominating form of equality in systems based on ITT up to the
1545 Our type former is $\mypeq$, which given a type (in this case
1546 $\mytya$) relates equal terms of that type. $\mypeq$ has one introduction
1547 rule, $\myrefl$, which introduces an equality relation between definitionally
1550 Finally, we have one eliminator for $\mypeq$, $\myjeqq$. $\myjeq{\myse{P}}{\myse{q}}{\myse{p}}$ takes
1552 \item $\myse{P}$, a predicate working with two terms of a certain type (say
1553 $\mytya$) and a proof of their equality;
1554 \item $\myse{q}$, a proof that two terms in $\mytya$ (say $\myse{m}$ and
1555 $\myse{n}$) are equal;
1556 \item and $\myse{p}$, an inhabitant of $\myse{P}$ applied to $\myse{m}$
1557 twice, plus the trivial proof by reflexivity showing that $\myse{m}$
1560 Given these ingredients, $\myjeqq$ retuns a member of $\myse{P}$ applied
1561 to $\mytmm$, $\mytmn$, and $\myse{q}$. In other words $\myjeqq$ takes a
1562 witness that $\myse{P}$ works with \emph{definitionally equal} terms,
1563 and returns a witness of $\myse{P}$ working with \emph{propositionally
1564 equal} terms. Invokations of $\myjeqq$ will vanish when the equality
1565 proofs will reduce to invocations to reflexivity, at which point the
1566 arguments must be definitionally equal, and thus the provided
1567 $\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmm}}{(\myapp{\myrefl}{\mytmm})}$
1568 can be returned. This means that $\myjeqq$ will not compute with
1569 hypotetical proofs, which makes sense given that they might be false.
1571 While the $\myjeqq$ rule is slightly convoluted, we can derive many more
1572 `friendly' rules from it, for example a more obvious `substitution' rule, that
1573 replaces equal for equal in predicates:
1576 \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}}}}} \\
1577 \myfun{subst}\myappsp \myb{A}\myappsp\myb{P}\myappsp\myb{x}\myappsp\myb{y}\myappsp\myb{q}\myappsp\myb{p} \mapsto
1578 \myjeq{(\myabs{\myb{x}\ \myb{y}\ \myb{q}}{\myapp{\myb{P}}{\myb{y}}})}{\myb{p}}{\myb{q}}
1581 Once we have $\myfun{subst}$, we can easily prove more familiar laws regarding
1582 equality, such as symmetry, transitivity, congruence laws, etc.
1584 \subsection{Common extensions}
1586 Our definitional and propositional equalities can be enhanced in various
1587 ways. Obviously if we extend the definitional equality we are also
1588 automatically extend propositional equality, given how $\myrefl$ works.
1590 \subsubsection{$\eta$-expansion}
1591 \label{sec:eta-expand}
1593 A simple extension to our definitional equality is $\eta$-expansion.
1594 Given an abstract variable $\myb{f} : \mytya \myarr \mytyb$ the aim is
1595 to have that $\myb{f} \mydefeq
1596 \myabss{\myb{x}}{\mytya}{\myapp{\myb{f}}{\myb{x}}}$. We can achieve
1597 this by `expanding' terms based on their types, a process also known as
1598 \emph{quotation}---a term borrowed from the practice of
1599 \emph{normalisation by evaluation}, where we embed terms in some host
1600 language with an existing notion of computation, and then reify them
1601 back into terms, which will `smooth out' differences like the one above
1604 The same concept applies to $\myprod$, where we expand each inhabitant
1605 by reconstructing it by getting its projections, so that $\myb{x}
1606 \mydefeq \mypair{\myfst \myappsp \myb{x}}{\mysnd \myappsp \myb{x}}$.
1607 Similarly, all one inhabitants of $\myunit$ and all zero inhabitants of
1608 $\myempty$ can be considered equal. Quotation can be performed in a
1609 type-directed way, as we will witness in Section \ref{sec:kant-irr}.
1611 \begin{mydef}[Congruence and $\eta$-laws]
1612 To justify quotation in our type system we will add a congruence law
1613 for abstractions and a similar law for products, plus the fact that all
1614 elements of $\myunit$ or $\myempty$ are equal.
1617 \mydesc{definitional equality:}{\myjud{\mytmm \mydefeq \mytmn}{\mytmsyn}}{
1619 \AxiomC{$\myjudd{\myctx; \myb{y} : \mytya}{\myapp{\myse{f}}{\myb{x}} \mydefeq \myapp{\myse{g}}{\myb{x}}}{\mysub{\mytyb}{\myb{x}}{\myb{y}}}$}
1620 \UnaryInfC{$\myjud{\myse{f} \mydefeq \myse{g}}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
1623 \AxiomC{$\myjud{\mypair{\myapp{\myfst}{\mytmm}}{\myapp{\mysnd}{\mytmm}} \mydefeq \mypair{\myapp{\myfst}{\mytmn}}{\myapp{\mysnd}{\mytmn}}}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
1624 \UnaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
1631 \AxiomC{$\myjud{\mytmm}{\myunit}$}
1632 \AxiomC{$\myjud{\mytmn}{\myunit}$}
1633 \BinaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\myunit}$}
1636 \AxiomC{$\myjud{\mytmm}{\myempty}$}
1637 \AxiomC{$\myjud{\mytmn}{\myempty}$}
1638 \BinaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\myempty}$}
1643 \subsubsection{Uniqueness of identity proofs}
1645 Another common but controversial addition to propositional equality is
1646 the $\myfun{K}$ axiom, which essentially states that all equality proofs
1649 \begin{mydef}[$\myfun{K}$ axiom]\end{mydef}
1650 \mydesc{typing:}{\myjud{\mytmm \mydefeq \mytmn}{\mytmsyn}}{
1653 \myjud{\myse{P}}{\myfora{\myb{x}}{\mytya}{\mypeq \myappsp \mytya \myappsp \myb{x}\myappsp \myb{x} \myarr \mytyp}} \\\
1654 \myjud{\mytmt}{\mytya} \hspace{1cm}
1655 \myjud{\myse{p}}{\myse{P} \myappsp \mytmt \myappsp (\myrefl \myappsp \mytmt)} \hspace{1cm}
1656 \myjud{\myse{q}}{\mytmt \mypeq{\mytya} \mytmt}
1659 \UnaryInfC{$\myjud{\myfun{K} \myappsp \myse{P} \myappsp \myse{t} \myappsp \myse{p} \myappsp \myse{q}}{\myse{P} \myappsp \mytmt \myappsp \myse{q}}$}
1663 \cite{Hofmann1994} showed that $\myfun{K}$ is not derivable from the
1664 $\myjeqq$ axiom that we presented, and \cite{McBride2004} showed that it is
1665 needed to implement `dependent pattern matching', as first proposed by
1666 \cite{Coquand1992}. Thus, $\myfun{K}$ is derivable in the systems that
1667 implement dependent pattern matching, such as Epigram and Agda; but for
1670 $\myfun{K}$ is controversial mainly because it is at odds with
1671 equalities that include computational behaviour, most notably
1672 Voevodsky's `Univalent Foundations', which includes a \emph{univalence}
1673 axiom that identifies isomorphisms between types with propositional
1674 equality. For example we would have two isomorphisms, and thus two
1675 equalities, between $\mybool$ and $\mybool$, corresponding to the two
1676 permutations---one is the identity, and one swaps the elements. Given
1677 this, $\myfun{K}$ and univalence are inconsistent, and thus a form of
1678 dependent pattern matching that does not imply $\myfun{K}$ is subject of
1679 research.\footnote{More information about univalence can be found at
1680 \url{http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations.html}.}
1682 \subsection{Limitations}
1684 \epigraph{\emph{Half of my time spent doing research involves thinking up clever
1685 schemes to avoid needing functional extensionality.}}{@larrytheliquid}
1687 Propositional equality as described is quite restricted when
1688 reasoning about equality beyond the term structure, which is what definitional
1689 equality gives us (extensions notwithstanding).
1691 The problem is best exemplified by \emph{function extensionality}. In
1692 mathematics, we would expect to be able to treat functions that give equal
1693 output for equal input as the same. When reasoning in a mechanised framework
1694 we ought to be able to do the same: in the end, without considering the
1695 operational behaviour, all functions equal extensionally are going to be
1696 replaceable with one another.
1698 However this is not the case, or in other words with the tools we have we have
1701 \myfun{ext} : \myfora{\myb{A}\ \myb{B}}{\mytyp}{\myfora{\myb{f}\ \myb{g}}{
1702 \myb{A} \myarr \myb{B}}{
1703 (\myfora{\myb{x}}{\myb{A}}{\mypeq \myappsp \myb{B} \myappsp (\myapp{\myb{f}}{\myb{x}}) \myappsp (\myapp{\myb{g}}{\myb{x}})}) \myarr
1704 \mypeq \myappsp (\myb{A} \myarr \myb{B}) \myappsp \myb{f} \myappsp \myb{g}
1708 To see why this is the case, consider the functions
1709 \[\myabs{\myb{x}}{0 \mathrel{\myfun{$+$}} \myb{x}}$ and $\myabs{\myb{x}}{\myb{x} \mathrel{\myfun{$+$}} 0}\]
1710 where $\myfun{$+$}$ is defined by recursion on the first argument,
1711 gradually destructing it to build up successors of the second argument.
1712 The two functions are clearly extensionally equal, and we can in fact
1715 \myfora{\myb{x}}{\mynat}{\mypeq \myappsp \mynat \myappsp (0 \mathrel{\myfun{$+$}} \myb{x}) \myappsp (\myb{x} \mathrel{\myfun{$+$}} 0)}
1717 By analysis on the $\myb{x}$. However, the two functions are not
1718 definitionally equal, and thus we won't be able to get rid of the
1721 For the reasons given above, theories that offer a propositional equality
1722 similar to what we presented are called \emph{intensional}, as opposed
1723 to \emph{extensional}. Most systems widely used today (such as Agda,
1724 Coq, and Epigram) are of this kind.
1726 This is quite an annoyance that often makes reasoning awkward to execute. It
1727 also extends to other fields, for example proving bisimulation between
1728 processes specified by coinduction, or in general proving equivalences based
1729 on the behaviour of a term.
1731 \subsection{Equality reflection}
1733 One way to `solve' this problem is by identifying propositional equality with
1734 definitional equality.
1736 \begin{mydef}[Equality reflection]\end{mydef}
1737 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1738 \AxiomC{$\myjud{\myse{q}}{\mytmm \mypeq{\mytya} \mytmn}$}
1739 \UnaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\mytya}$}
1743 The \emph{equality reflection} rule is a very different rule from the
1744 ones we saw up to now: it links a typing judgement internal to the type
1745 theory to a meta-theoretic judgement that the type checker uses to work
1746 with terms. It is easy to see the dangerous consequences that this
1749 \item The rule is not syntax directed, and the type checker is
1750 presumably expected to come up with equality proofs when needed.
1751 \item More worryingly, type checking becomes undecidable also because
1752 computing under false assumptions becomes unsafe, since we derive any
1753 equality proof and then use equality reflection and the conversion
1754 rule to have terms of any type.
1756 For example, assuming that we are in a context that contains
1758 \myb{A} : \mytyp; \myb{q} : \mypeq \myappsp \mytyp
1759 \myappsp (\mytya \myarr \mytya) \myappsp \mytya
1761 we can write a looping term similar to the one we saw in Section
1766 Given these facts theories employing equality reflection, like NuPRL
1767 \citep{NuPRL}, carry the derivations that gave rise to each typing judgement
1768 to keep the systems manageable.
1770 For all its faults, equality reflection does allow us to prove extensionality,
1771 using the extensions we gave above. Assuming that $\myctx$ contains
1772 \[\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}}}\]
1776 \AxiomC{$\hspace{1.1cm}\myjudd{\myctx; \myb{x} : \myb{A}}{\myapp{\myb{q}}{\myb{x}}}{\myapp{\myb{f}}{\myb{x}} \mypeq{} \myapp{\myb{g}}{\myb{x}}}\hspace{1.1cm}$}
1777 \RightLabel{equality reflection}
1778 \UnaryInfC{$\myjudd{\myctx; \myb{x} : \myb{A}}{\myapp{\myb{f}}{\myb{x}} \mydefeq \myapp{\myb{g}}{\myb{x}}}{\myb{B}}$}
1779 \RightLabel{congruence for $\lambda$s}
1780 \UnaryInfC{$\myjud{(\myabs{\myb{x}}{\myapp{\myb{f}}{\myb{x}}}) \mydefeq (\myabs{\myb{x}}{\myapp{\myb{g}}{\myb{x}}})}{\myb{A} \myarr \myb{B}}$}
1781 \RightLabel{$\eta$-law for $\lambda$}
1782 \UnaryInfC{$\hspace{1.45cm}\myjud{\myb{f} \mydefeq \myb{g}}{\myb{A} \myarr \myb{B}}\hspace{1.45cm}$}
1783 \RightLabel{$\myrefl$}
1784 \UnaryInfC{$\myjud{\myapp{\myrefl}{\myb{f}}}{\myb{f} \mypeq{} \myb{g}}$}
1787 Now, the question is: do we need to give up well-behavedness of our theory to
1788 gain extensionality?
1790 \section{The observational approach}
1793 % TODO add \begin{mydef}s
1795 A recent development by \citet{Altenkirch2007}, \emph{Observational Type
1796 Theory} (OTT), promises to keep the well behavedness of ITT while
1797 being able to gain many useful equality proofs,\footnote{It is suspected
1798 that OTT gains \emph{all} the equality proofs of ETT, but no proof
1799 exists yet.} including function extensionality. The main idea is to
1800 give the user the possibility to \emph{coerce} (or transport) values
1801 from a type $\mytya$ to a type $\mytyb$, if the type checker can prove
1802 structurally that $\mytya$ and $\mytyb$ are equal; and providing a
1803 value-level equality based on similar principles. Here we give an
1804 exposition which follows closely the original paper.
1806 \subsection{A simpler theory, a propositional fragment}
1808 \begin{mydef}[OTT's simple theory, with propositions]\ \end{mydef}
1811 $\mytyp_l$ is replaced by $\mytyp$. \\\ \\
1813 \begin{array}{r@{\ }c@{\ }l}
1814 \mytmsyn & ::= & \cdots \mysynsep \myprdec{\myprsyn} \mysynsep
1815 \myITE{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
1816 \myprsyn & ::= & \mybot \mysynsep \mytop \mysynsep \myprsyn \myand \myprsyn
1817 \mysynsep \myprfora{\myb{x}}{\mytmsyn}{\myprsyn}
1824 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
1826 \begin{array}{l@{}l@{\ }c@{\ }l}
1827 \myITE{\mytrue &}{\mytya}{\mytyb} & \myred & \mytya \\
1828 \myITE{\myfalse &}{\mytya}{\mytyb} & \myred & \mytyb
1835 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1837 \AxiomC{$\myjud{\myse{P}}{\myprop}$}
1838 \UnaryInfC{$\myjud{\myprdec{\myse{P}}}{\mytyp}$}
1841 \AxiomC{$\myjud{\mytmt}{\mybool}$}
1842 \AxiomC{$\myjud{\mytya}{\mytyp}$}
1843 \AxiomC{$\myjud{\mytyb}{\mytyp}$}
1844 \TrinaryInfC{$\myjud{\myITE{\mytmt}{\mytya}{\mytyb}}{\mytyp}$}
1851 \mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
1852 \begin{tabular}{ccc}
1853 \AxiomC{\phantom{$\myjud{\myse{P}}{\myprop}$}}
1854 \UnaryInfC{$\myjud{\mytop}{\myprop}$}
1856 \UnaryInfC{$\myjud{\mybot}{\myprop}$}
1859 \AxiomC{$\myjud{\myse{P}}{\myprop}$}
1860 \AxiomC{$\myjud{\myse{Q}}{\myprop}$}
1861 \BinaryInfC{$\myjud{\myse{P} \myand \myse{Q}}{\myprop}$}
1863 \UnaryInfC{\phantom{$\myjud{\mybot}{\myprop}$}}
1866 \AxiomC{$\myjud{\myse{A}}{\mytyp}$}
1867 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\myse{P}}{\myprop}$}
1868 \BinaryInfC{$\myjud{\myprfora{\myb{x}}{\mytya}{\myse{P}}}{\myprop}$}
1870 \UnaryInfC{\phantom{$\myjud{\mybot}{\myprop}$}}
1875 Our foundation will be a type theory like the one of Section
1876 \ref{sec:itt}, with only one level: $\mytyp_0$. In this context we will
1877 drop the $0$ and call $\mytyp_0$ $\mytyp$. Moreover, since the old
1878 $\myfun{if}\myarg\myfun{then}\myarg\myfun{else}$ was able to return
1879 types thanks to the hierarchy (which is gone), we need to reintroduce an
1880 ad-hoc conditional for types, where the reduction rule is the obvious
1883 However, we have an addition: a universe of \emph{propositions},
1884 $\myprop$. $\myprop$ isolates a fragment of types at large, and
1885 indeed we can `inject' any $\myprop$ back in $\mytyp$ with $\myprdec{\myarg}$.
1886 \begin{mydef}[Proposition decoding]\ \end{mydef}
1887 \mydesc{proposition decoding:}{\myprdec{\mytmsyn} \myred \mytmsyn}{
1890 \begin{array}{l@{\ }c@{\ }l}
1891 \myprdec{\mybot} & \myred & \myempty \\
1892 \myprdec{\mytop} & \myred & \myunit
1897 \begin{array}{r@{ }c@{ }l@{\ }c@{\ }l}
1898 \myprdec{&\myse{P} \myand \myse{Q} &} & \myred & \myprdec{\myse{P}} \myprod \myprdec{\myse{Q}} \\
1899 \myprdec{&\myprfora{\myb{x}}{\mytya}{\myse{P}} &} & \myred &
1900 \myfora{\myb{x}}{\mytya}{\myprdec{\myse{P}}}
1905 Propositions are what we call the types of \emph{proofs}, or types
1906 whose inhabitants contain no `data', much like $\myunit$. The goal
1907 when isolating \mytyc{Prop} is twofold: erasing all top-level
1908 propositions when compiling; and to identify all equivalent
1909 propositions as the same, as we will see later.
1911 Why did we choose what we have in $\myprop$? Given the above
1912 criteria, $\mytop$ obviously fits the bill, since it has one element.
1913 A pair of propositions $\myse{P} \myand \myse{Q}$ still won't get us
1914 data, since if they both have one element the only possible pair is
1915 the one formed by said elements. Finally, if $\myse{P}$ is a
1916 proposition and we have $\myprfora{\myb{x}}{\mytya}{\myse{P}}$, the
1917 decoding will be a constant function for propositional content. The
1918 only threat is $\mybot$, by which we can fabricate anything we want:
1919 however if we are consistent there will be no closed term of type
1920 $\mybot$ at, which is what we care about regarding proof erasure and
1923 \subsection{Equality proofs}
1925 \begin{mydef}[Equality proofs and related operations]\ \end{mydef}
1929 \begin{array}{r@{\ }c@{\ }l}
1930 \mytmsyn & ::= & \cdots \mysynsep
1931 \mycoee{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \mysynsep
1932 \mycohh{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
1933 \myprsyn & ::= & \cdots \mysynsep \mytmsyn \myeq \mytmsyn \mysynsep
1934 \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn}
1939 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1941 \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
1942 \AxiomC{$\myjud{\mytmt}{\mytya}$}
1943 \BinaryInfC{$\myjud{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}$}
1946 \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
1947 \AxiomC{$\myjud{\mytmt}{\mytya}$}
1948 \BinaryInfC{$\myjud{\mycohh{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\myprdec{\myjm{\mytmt}{\mytya}{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}}}$}
1954 \mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
1959 \myjud{\myse{A}}{\mytyp} \hspace{1cm} \myjud{\myse{B}}{\mytyp}
1962 \UnaryInfC{$\myjud{\mytya \myeq \mytyb}{\myprop}$}
1967 \myjud{\myse{A}}{\mytyp} \hspace{1cm} \myjud{\mytmm}{\myse{A}} \\
1968 \myjud{\myse{B}}{\mytyp} \hspace{1cm} \myjud{\mytmn}{\myse{B}}
1971 \UnaryInfC{$\myjud{\myjm{\mytmm}{\myse{A}}{\mytmn}{\myse{B}}}{\myprop}$}
1978 While isolating a propositional universe as presented can be a useful
1979 exercises on its own, what we are really after is a useful notion of
1980 equality. In OTT we want to maintain that things judged to be equal are
1981 still always repleaceable for one another with no additional
1982 changes. Note that this is not the same as saying that they are
1983 definitionally equal, since as we saw extensionally equal functions,
1984 while satisfying the above requirement, are not.
1986 Towards this goal we introduce two equality constructs in
1987 $\myprop$---the fact that they are in $\myprop$ indicates that they
1988 indeed have no computational content. The first construct, $\myarg
1989 \myeq \myarg$, relates types, the second,
1990 $\myjm{\myarg}{\myarg}{\myarg}{\myarg}$, relates values. The
1991 value-level equality is different from our old propositional equality:
1992 instead of ranging over only one type, we might form equalities between
1993 values of different types---the usefulness of this construct will be
1994 clear soon. In the literature this equality is known as `heterogeneous'
1995 or `John Major', since
1998 John Major's `classless society' widened people's aspirations to
1999 equality, but also the gap between rich and poor. After all, aspiring
2000 to be equal to others than oneself is the politics of envy. In much
2001 the same way, forms equations between members of any type, but they
2002 cannot be treated as equals (ie substituted) unless they are of the
2003 same type. Just as before, each thing is only equal to
2004 itself. \citep{McBride1999}.
2007 Correspondingly, at the term level, $\myfun{coe}$ (`coerce') lets us
2008 transport values between equal types; and $\myfun{coh}$ (`coherence')
2009 guarantees that $\myfun{coe}$ respects the value-level equality, or in
2010 other words that it really has no computational component: if we
2011 transport $\mytmm : \mytya$ to $\mytmn : \mytyb$, $\mytmm$ and $\mytmn$
2012 will still be the same.
2014 Before introducing the core ideas that make OTT work, let us distinguish
2015 between \emph{canonical} and \emph{neutral} terms and types.
2017 \begin{mydef}[Canonical and neutral types and terms]
2018 \emph{Canonical} types are those arising from the ground types
2019 ($\myempty$, $\myunit$, $\mybool$) and the three type formers
2020 ($\myarr$, $\myprod$, $\mytyc{W}$). \emph{Neutral} types are those
2021 formed by $\myfun{If}\myarg\myfun{Then}\myarg\myfun{Else}\myarg$.
2022 Correspondingly, canonical terms are those inhabiting data
2023 constructors ($\mytt$, $\mytrue$, $\myfalse$,
2024 $\myabss{\myb{x}}{\mytya}{\mytmt}$, ...); all the others being
2025 neutral, including eliminators and abstracted variables.
2028 In the current system (and hopefully in well-behaved systems), all
2029 closed terms reduce to a canonical term (as a consequence or
2030 normalisation), and all canonical types are inhabited by canonical
2031 terms (a property known as \emph{canonicity}).
2033 \subsubsection{Type equality, and coercions}
2035 The plan is to decompose type-level equalities between canonical types
2036 into decodable propositions containing equalities regarding the
2037 subterms, and to use coerce recursively on the subterms using the
2038 generated equalities. This interplay between the canonicity of equated
2039 types, type equalities, and \myfun{coe} ensures that invocations of
2040 $\myfun{coe}$ will vanish when we have evidence of the structural
2041 equality of the types we are transporting terms across. If the type is
2042 neutral, the equality will not reduce and thus $\myfun{coe}$ will not
2043 reduce either. If we come an equality between different canonical
2044 types, then we reduce the equality to bottom, making sure that no such
2045 proof can exist, and providing an `escape hatch' in $\myfun{coe}$.
2049 \mydesc{equality reduction:}{\myprsyn \myred \myprsyn}{
2051 \begin{array}{c@{\ }c@{\ }c@{\ }l}
2052 \myempty & \myeq & \myempty & \myred \mytop \\
2053 \myunit & \myeq & \myunit & \myred \mytop \\
2054 \mybool & \myeq & \mybool & \myred \mytop \\
2055 \myexi{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myexi{\myb{x_2}}{\mytya_2}{\mytya_2} & \myred \\
2057 \myind{2} \mytya_1 \myeq \mytya_2 \myand
2058 \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}]}
2060 \myfora{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myfora{\myb{x_2}}{\mytya_2}{\mytyb_2} & \myred \cdots \\
2061 \myw{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myw{\myb{x_2}}{\mytya_2}{\mytyb_2} & \myred \cdots \\
2062 \mytya & \myeq & \mytyb & \myred \mybot\ \text{if $\mytya$ and $\mytyb$ are canonical.}
2067 \mydesc{reduction}{\mytmsyn \myred \mytmsyn}{
2069 \begin{array}[t]{@{}l@{\ }l@{\ }l@{\ }l@{\ }l@{\ }c@{\ }l@{\ }}
2070 \mycoe & \myempty & \myempty & \myse{Q} & \myse{t} & \myred & \myse{t} \\
2071 \mycoe & \myunit & \myunit & \myse{Q} & \myse{t} & \myred & \mytt \\
2072 \mycoe & \mybool & \mybool & \myse{Q} & \mytrue & \myred & \mytrue \\
2073 \mycoe & \mybool & \mybool & \myse{Q} & \myfalse & \myred & \myfalse \\
2074 \mycoe & (\myexi{\myb{x_1}}{\mytya_1}{\mytyb_1}) &
2075 (\myexi{\myb{x_2}}{\mytya_2}{\mytyb_2}) & \myse{Q} &
2076 \mytmt_1 & \myred & \\
2078 \myind{2}\begin{array}[t]{l@{\ }l@{\ }c@{\ }l}
2079 \mysyn{let} & \myb{\mytmm_1} & \mapsto & \myapp{\myfst}{\mytmt_1} : \mytya_1 \\
2080 & \myb{\mytmn_1} & \mapsto & \myapp{\mysnd}{\mytmt_1} : \mysub{\mytyb_1}{\myb{x_1}}{\myb{\mytmm_1}} \\
2081 & \myb{Q_A} & \mapsto & \myapp{\myfst}{\myse{Q}} : \mytya_1 \myeq \mytya_2 \\
2082 & \myb{\mytmm_2} & \mapsto & \mycoee{\mytya_1}{\mytya_2}{\myb{Q_A}}{\myb{\mytmm_1}} : \mytya_2 \\
2083 & \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}}} \\
2084 & \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}} \\
2085 \mysyn{in} & \multicolumn{3}{@{}l}{\mypair{\myb{\mytmm_2}}{\myb{\mytmn_2}}}
2088 \mycoe & (\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}) &
2089 (\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}) & \myse{Q} &
2093 \mycoe & (\myw{\myb{x_1}}{\mytya_1}{\mytyb_1}) &
2094 (\myw{\myb{x_2}}{\mytya_2}{\mytyb_2}) & \myse{Q} &
2098 \mycoe & \mytya & \mytyb & \myse{Q} & \mytmt & \myred & \myapp{\myabsurd{\mytyb}}{\myse{Q}}\ \text{if $\mytya$ and $\mytyb$ are canonical.}
2102 \caption{Reducing type equalities, and using them when
2103 $\myfun{coe}$rcing.}
2107 \begin{mydef}[Type equalities reduction, and \myfun{coe}rcions] Figure
2108 \ref{fig:eqred} illustrates the rules to reduce equalities and to
2111 For ground types, the proof is the trivial element, and \myfun{coe} is
2112 the identity. For $\myunit$, we can do better: we return its only
2113 member without matching on the term. For the three type binders, things
2114 are similar but subtly different---the choices we make in the type
2115 equality are dictated by the desire of writing the $\myfun{coe}$ in a
2118 $\myprod$ is the easiest case: we decompose the proof into proofs that
2119 the first element's types are equal ($\mytya_1 \myeq \mytya_2$), and a
2120 proof that given equal values in the first element, the types of the
2121 second elements are equal too
2122 ($\myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{\myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2}}
2123 \myimpl \mytyb_1[\myb{x_1}] \myeq \mytyb_2[\myb{x_2}]}$).\footnote{We
2124 are using $\myimpl$ to indicate a $\forall$ where we discard the first
2125 value. We write $\mytyb_1[\myb{x_1}]$ to indicate that the
2126 $\myb{x_1}$ in $\mytyb_1$ is re-bound to the $\myb{x_1}$ quantified by
2127 the $\forall$, and similarly for $\myb{x_2}$ and $\mytyb_2$.} This
2128 also explains the need for heterogeneous equality, since in the second
2129 proof we need to equate terms of possibly different types. In the respective $\myfun{coe}$ case, since
2130 the types are canonical, we know at this point that the proof of
2131 equality is a pair of the shape described above. Thus, we can
2132 immediately coerce the first element of the pair using the first element
2133 of the proof, and then instantiate the second element with the two first
2134 elements and a proof by coherence of their equality, since we know that
2135 the types are equal.
2137 The cases for the other binders are omitted for brevity, but they follow
2138 the same principle with some twists to make $\myfun{coe}$ work with the
2139 generated proofs; the reader can refer to the paper for details.
2141 \subsubsection{$\myfun{coe}$, laziness, and $\myfun{coh}$erence}
2144 It is important to notice that in the reduction rules for $\myfun{coe}$
2145 are never obstructed by the proofs: with the exception of comparisons
2146 between different canonical types we never `pattern match' on the proof
2147 pairs, but always look at the projections. This means that, as long as
2148 we are consistent, and thus as long as we don't have $\mybot$-inducing
2149 proofs, we can add propositional axioms for equality and $\myfun{coe}$
2150 will still compute. Thus, we can take $\myfun{coh}$ as axiomatic, and
2151 we can add back familiar useful equality rules:
2153 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
2154 \AxiomC{$\myjud{\mytmt}{\mytya}$}
2155 \UnaryInfC{$\myjud{\myapp{\myrefl}{\mytmt}}{\myprdec{\myjm{\mytmt}{\mytya}{\mytmt}{\mytya}}}$}
2160 \AxiomC{$\myjud{\mytya}{\mytyp}$}
2161 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytyb}{\mytyp}$}
2162 \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}}}}}$}
2166 $\myrefl$ is the equivalent of the reflexivity rule in propositional
2167 equality, and $\mytyc{R}$ asserts that if we have a we have a $\mytyp$
2168 abstracting over a value we can substitute equal for equal---this lets
2169 us recover $\myfun{subst}$. Note that while we need to provide ad-hoc
2170 rules in the restricted, non-hierarchical theory that we have, if our
2171 theory supports abstraction over $\mytyp$s we can easily add these
2172 axioms as abstracted variables.
2174 \subsubsection{Value-level equality}
2176 \begin{mydef}[Value-level equality]\ \end{mydef}
2178 \mydesc{equality reduction:}{\myprsyn \myred \myprsyn}{
2180 \begin{array}{r@{ }c@{\ }c@{\ }c@{}l@{\ }c@{\ }r@{}c@{\ }c@{\ }c@{}l@{\ }l}
2181 (&\mytmt_1 & : & \myempty&) & \myeq & (&\mytmt_2 & : & \myempty &) & \myred \mytop \\
2182 (&\mytmt_1 & : & \myunit&) & \myeq & (&\mytmt_2 & : & \myunit&) & \myred \mytop \\
2183 (&\mytrue & : & \mybool&) & \myeq & (&\mytrue & : & \mybool&) & \myred \mytop \\
2184 (&\myfalse & : & \mybool&) & \myeq & (&\myfalse & : & \mybool&) & \myred \mytop \\
2185 (&\mytrue & : & \mybool&) & \myeq & (&\myfalse & : & \mybool&) & \myred \mybot \\
2186 (&\myfalse & : & \mybool&) & \myeq & (&\mytrue & : & \mybool&) & \myred \mybot \\
2187 (&\mytmt_1 & : & \myexi{\mytya_1}{\myb{x_1}}{\mytyb_1}&) & \myeq & (&\mytmt_2 & : & \myexi{\mytya_2}{\myb{x_2}}{\mytyb_2}&) & \myred \\
2188 & \multicolumn{11}{@{}l}{
2189 \myind{2} \myjm{\myapp{\myfst}{\mytmt_1}}{\mytya_1}{\myapp{\myfst}{\mytmt_2}}{\mytya_2} \myand
2190 \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}}}
2192 (&\myse{f}_1 & : & \myfora{\mytya_1}{\myb{x_1}}{\mytyb_1}&) & \myeq & (&\myse{f}_2 & : & \myfora{\mytya_2}{\myb{x_2}}{\mytyb_2}&) & \myred \\
2193 & \multicolumn{11}{@{}l}{
2194 \myind{2} \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{
2195 \myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2} \myimpl
2196 \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}]}
2199 (&\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 \\
2200 (&\mytmt_1 & : & \mytya_1&) & \myeq & (&\mytmt_2 & : & \mytya_2 &) & \myred \mybot\ \text{if $\mytya_1$ and $\mytya_2$ are canonical.}
2205 As with type-level equality, we want value-level equality to reduce
2206 based on the structure of the compared terms. When matching
2207 propositional data, such as $\myempty$ and $\myunit$, we automatically
2208 return the trivial type, since if a type has zero one members, all
2209 members will be equal. When matching on data-bearing types, such as
2210 $\mybool$, we check that such data matches, and return bottom otherwise.
2212 \subsection{Proof irrelevance and stuck coercions}
2213 \label{sec:ott-quot}
2215 The last effort is required to make sure that proofs (members of
2216 $\myprop$) are \emph{irrelevant}. Since they are devoid of
2217 computational content, we would like to identify all equivalent
2218 propositions as the same, in a similar way as we identified all
2219 $\myempty$ and all $\myunit$ as the same in section
2220 \ref{sec:eta-expand}.
2222 Thus we will have a quotation that will not only perform
2223 $\eta$-expansion, but will also identify and mark proofs that could not
2224 be decoded (that is, equalities on neutral types). Then, when
2225 comparing terms, marked proofs will be considered equal without
2226 analysing their contents, thus gaining irrelevance.
2228 Moreover we can safely advance `stuck' $\myfun{coe}$rcions between
2229 non-canonical but definitionally equal types. Consider for example
2231 \mycoee{(\myITE{\myb{b}}{\mynat}{\mybool})}{(\myITE{\myb{b}}{\mynat}{\mybool})}{\myb{x}}
2233 Where $\myb{b}$ and $\myb{x}$ are abstracted variables. This
2234 $\myfun{coe}$ will not advance, since the types are not canonical.
2235 However they are definitionally equal, and thus we can safely remove the
2236 coerce and return $\myb{x}$ as it is.
2238 \section{\mykant: the theory}
2239 \label{sec:kant-theory}
2241 \mykant\ is an interactive theorem prover developed as part of this thesis.
2242 The plan is to present a core language which would be capable of serving as
2243 the basis for a more featureful system, while still presenting interesting
2244 features and more importantly observational equality.
2246 We will first present the features of the system, and then describe the
2247 implementation we have developed in Section \ref{sec:kant-practice}.
2249 The defining features of \mykant\ are:
2252 \item[Full dependent types] As we would expect, we have dependent a system
2253 which is as expressive as the `best' corner in the lambda cube described in
2254 Section \ref{sec:itt}.
2256 \item[Implicit, cumulative universe hierarchy] The user does not need to
2257 specify universe level explicitly, and universes are \emph{cumulative}.
2259 \item[User defined data types and records] Instead of forcing the user to
2260 choose from a restricted toolbox, we let her define inductive data types,
2261 with associated primitive recursion operators; or records, with associated
2262 projections for each field.
2264 \item[Bidirectional type checking] While no `fancy' inference via
2265 unification is present, we take advantage of a type synthesis system
2266 in the style of \cite{Pierce2000}, extending the concept for user
2269 \item[Observational equality] As described in Section \ref{sec:ott} but
2270 extended to work with the type hierarchy and to admit equality between
2271 arbitrary data types.
2273 \item[Type holes] When building up programs interactively, it is useful
2274 to leave parts unfinished while exploring the current context. This
2275 is what type holes are for. We do not describe holes rigorously, but
2276 provide more information about them in Section \ref{sec:type-holes}.
2280 We will analyse the features one by one, along with motivations and
2281 tradeoffs for the design decisions made.
2283 \subsection{Bidirectional type checking}
2285 We start by describing bidirectional type checking since it calls for
2286 fairly different typing rules that what we have seen up to now. The
2287 idea is to have two kinds of terms: terms for which a type can always be
2288 inferred, and terms that need to be checked against a type. A nice
2289 observation is that this duality is in correspondence with the notion of
2290 canonical and neutral terms: neutral terms
2291 (abstracted or defined variables, function application, record
2292 projections, primitive recursors, etc.) \emph{infer} types, canonical
2293 terms (abstractions, record/data types data constructors, etc.) need to
2296 To introduce the concept and notation, we will revisit the STLC in a
2297 bidirectional style. The presentation follows \cite{Loh2010}. The
2298 syntax for our bidirectional STLC is the same as the untyped
2299 $\lambda$-calculus, but with an extra construct to annotate terms
2300 explicitly---this will be necessary when having top-level canonical
2301 terms. The types are the same as those found in the normal STLC.
2303 \begin{mydef}[Syntax for the annotated $\lambda$-calculus]\ \end{mydef}
2307 \begin{array}{r@{\ }c@{\ }l}
2308 \mytmsyn & ::= & \myb{x} \mysynsep \myabs{\myb{x}}{\mytmsyn} \mysynsep (\myapp{\mytmsyn}{\mytmsyn}) \mysynsep (\mytmsyn : \mytysyn)
2312 We will have two kinds of typing judgements: \emph{inference} and
2313 \emph{checking}. $\myinf{\mytmt}{\mytya}$ indicates that $\mytmt$
2314 infers the type $\mytya$, while $\mychk{\mytmt}{\mytya}$ can be checked
2315 against type $\mytya$. The type of variables in context is inferred,
2316 and so are annotate terms. The type of applications is inferred too,
2317 propagating types down the applied term. Abstractions are checked.
2318 Finally, we have a rule to check the type of an inferrable term.
2320 \begin{mydef}[Bidirectional type checking for the STLC]\ \end{mydef}
2322 \mydesc{typing:}{\myctx \vdash \mytmsyn \Updownarrow \mytmsyn}{
2324 \AxiomC{$\myctx(x) = A$}
2325 \UnaryInfC{$\myinf{\myb{x}}{A}$}
2328 \AxiomC{$\myjudd{\myctx;\myb{x} : A}{\mytmt}{\mytyb}$}
2329 \UnaryInfC{$\mychk{\myabs{x}{\mytmt}}{(\myb{x} {:} \mytya) \myarr \mytyb}$}
2335 \begin{tabular}{ccc}
2336 \AxiomC{$\myinf{\mytmm}{\mytya \myarr \mytyb}$}
2337 \AxiomC{$\mychk{\mytmn}{\mytya}$}
2338 \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mytyb}$}
2341 \AxiomC{$\mychk{\mytmt}{\mytya}$}
2342 \UnaryInfC{$\myinf{\myann{\mytmt}{\mytya}}{\mytya}$}
2345 \AxiomC{$\myinf{\mytmt}{\mytya}$}
2346 \UnaryInfC{$\mychk{\mytmt}{\mytya}$}
2351 For example, if we wanted to type function composition (in this case for
2352 naturals), we would have to annotate the term:
2354 \myfun{comp} \mapsto (\myabs{\myb{f}\, \myb{g}\, \myb{x}}{\myb{f}\myappsp(\myb{g}\myappsp\myb{x})}) : (\mynat \myarr \mynat) \myarr (\mynat \myarr \mynat) \myarr \mynat \myarr \mynat
2356 But we would not have to annotate functions passed to it, since the type would be propagated to the arguments:
2358 \myfun{comp}\myappsp (\myabs{\myb{x}}{\myb{x} \mathrel{\myfun{$+$}} 3}) \myappsp (\myabs{\myb{x}}{\myb{x} \mathrel{\myfun{$*$}} 4}) \myappsp 42
2361 \subsection{Base terms and types}
2363 Let us begin by describing the primitives available without the user
2364 defining any data types, and without equality. The way we handle
2365 variables and substitution is left unspecified, and explained in section
2366 \ref{sec:term-repr}, along with other implementation issues. We are
2367 also going to give an account of the implicit type hierarchy separately
2368 in Section \ref{sec:term-hierarchy}, so as not to clutter derivation
2369 rules too much, and just treat types as impredicative for the time
2372 \begin{mydef}[Syntax for base types in \mykant]\ \end{mydef}
2376 \begin{array}{r@{\ }c@{\ }l}
2377 \mytmsyn & ::= & \mynamesyn \mysynsep \mytyp \\
2378 & | & \myfora{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
2379 \myabs{\myb{x}}{\mytmsyn} \mysynsep
2380 (\myapp{\mytmsyn}{\mytmsyn}) \mysynsep
2381 (\myann{\mytmsyn}{\mytmsyn}) \\
2382 \mynamesyn & ::= & \myb{x} \mysynsep \myfun{f}
2387 The syntax for our calculus includes just two basic constructs:
2388 abstractions and $\mytyp$s. Everything else will be user-defined.
2389 Since we let the user define values too, we will need a context capable
2390 of carrying the body of variables along with their type.
2392 \begin{mydef}[Context validity]
2393 Bound names and defined names are treated separately in the syntax, and
2394 while both can be associated to a type in the context, only defined
2395 names can be associated with a body.
2398 \mydesc{context validity:}{\myvalid{\myctx}}{
2399 \begin{tabular}{ccc}
2400 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
2401 \UnaryInfC{$\myvalid{\myemptyctx}$}
2404 \AxiomC{$\myjud{\mytya}{\mytyp}$}
2405 \AxiomC{$\mynamesyn \not\in \myctx$}
2406 \BinaryInfC{$\myvalid{\myctx ; \mynamesyn : \mytya}$}
2409 \AxiomC{$\myjud{\mytmt}{\mytya}$}
2410 \AxiomC{$\myfun{f} \not\in \myctx$}
2411 \BinaryInfC{$\myvalid{\myctx ; \myfun{f} \mapsto \mytmt : \mytya}$}
2416 Now we can present the reduction rules, which are unsurprising. We have
2417 the usual function application ($\beta$-reduction), but also a rule to
2418 replace names with their bodies ($\delta$-reduction), and one to discard
2419 type annotations. For this reason reduction is done in-context, as
2420 opposed to what we have seen in the past.
2422 \begin{mydef}[Reduction rules for base types in \mykant]\ \end{mydef}
2424 \mydesc{reduction:}{\myctx \vdash \mytmsyn \myred \mytmsyn}{
2425 \begin{tabular}{ccc}
2426 \AxiomC{\phantom{$\myb{x} \mapsto \mytmt : \mytya \in \myctx$}}
2427 \UnaryInfC{$\myctx \vdash \myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn}
2428 \myred \mysub{\mytmm}{\myb{x}}{\mytmn}$}
2431 \AxiomC{$\myfun{f} \mapsto \mytmt : \mytya \in \myctx$}
2432 \UnaryInfC{$\myctx \vdash \myfun{f} \myred \mytmt$}
2435 \AxiomC{\phantom{$\myb{x} \mapsto \mytmt : \mytya \in \myctx$}}
2436 \UnaryInfC{$\myctx \vdash \myann{\mytmm}{\mytya} \myred \mytmm$}
2441 We can now give types to our terms. Although we include the usual
2442 conversion rule, we defer a detailed account of definitional equality to
2443 Section \ref{sec:kant-irr}.
2445 \begin{mydef}[Bidirectional type checking for base types in \mykant]\ \end{mydef}
2447 \mydesc{typing:}{\myctx \vdash \mytmsyn \Updownarrow \mytmsyn}{
2448 \begin{tabular}{cccc}
2449 \AxiomC{$\myse{name} : A \in \myctx$}
2450 \UnaryInfC{$\myinf{\myse{name}}{A}$}
2453 \AxiomC{$\myfun{f} \mapsto \mytmt : A \in \myctx$}
2454 \UnaryInfC{$\myinf{\myfun{f}}{A}$}
2457 \AxiomC{$\mychk{\mytmt}{\mytya}$}
2458 \UnaryInfC{$\myinf{\myann{\mytmt}{\mytya}}{\mytya}$}
2461 \AxiomC{$\myinf{\mytmt}{\mytya}$}
2462 \AxiomC{$\myctx \vdash \mytya \mydefeq \mytyb$}
2463 \BinaryInfC{$\mychk{\mytmt}{\mytyb}$}
2471 \AxiomC{\phantom{$\mychkk{\myctx; \myb{x}: \mytya}{\mytmt}{\mytyb}$}}
2472 \UnaryInfC{$\myinf{\mytyp}{\mytyp}$}
2475 \AxiomC{$\myinf{\mytya}{\mytyp}$}
2476 \AxiomC{$\myinff{\myctx; \myb{x} : \mytya}{\mytyb}{\mytyp}$}
2477 \BinaryInfC{$\myinf{(\myb{x} {:} \mytya) \myarr \mytyb}{\mytyp}$}
2486 \AxiomC{$\myinf{\mytmm}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
2487 \AxiomC{$\mychk{\mytmn}{\mytya}$}
2488 \BinaryInfC{$\myinf{\myapp{\mytmm}{\mytmn}}{\mysub{\mytyb}{\myb{x}}{\mytmn}}$}
2493 \AxiomC{$\mychkk{\myctx; \myb{x}: \mytya}{\mytmt}{\mytyb}$}
2494 \UnaryInfC{$\mychk{\myabs{\myb{x}}{\mytmt}}{\myfora{\myb{x}}{\mytyb}{\mytyb}}$}
2500 \subsection{Elaboration}
2502 As we mentioned, $\mykant$\ allows the user to define not only values
2503 but also custom data types and records. \emph{Elaboration} consists of
2504 turning these declarations into workable syntax, types, and reduction
2505 rules. The treatment of custom types in $\mykant$\ is heavily inspired
2506 by McBride's and McKinna's early work on Epigram \citep{McBride2004},
2507 although with some differences.
2509 \subsubsection{Term vectors, telescopes, and assorted notation}
2511 \begin{mydef}[Term vector]
2512 A \emph{term vector} is a series of terms. The empty vector is
2513 represented by $\myemptyctx$, and a new element is added with a
2514 semicolon, similarly to contexts---$\vec{t};\mytmm$.
2517 We use term vectors to refer to a series of term applied to another. For
2518 example $\mytyc{D} \myappsp \vec{A}$ is a shorthand for $\mytyc{D}
2519 \myappsp \mytya_1 \cdots \mytya_n$, for some $n$. $n$ is consistently
2520 used to refer to the length of such vectors, and $i$ to refer to an
2521 index in such vectors.
2523 \begin{mydef}[Telescope]
2524 A \emph{telescope} is a series of typed bindings. The empty telescope
2525 is represented by $\myemptyctx$, and a binding is added via
2529 To present the elaboration and operations on user defined data types, we
2530 frequently make use what de Bruijn called \emph{telescopes}
2531 \citep{Bruijn91}, a construct that will prove useful when dealing with
2532 the types of type and data constructors. We refer to telescopes with
2533 $\mytele$, $\mytele'$, $\mytele_i$, etc. If $\mytele$ refers to a
2534 telescope, $\mytelee$ refers to the term vector made up of all the
2535 variables bound by $\mytele$. $\mytele \myarr \mytya$ refers to the
2536 type made by turning the telescope into a series of $\myarr$. For
2537 example we have that
2539 (\myb{x} {:} \mynat); (\myb{p} : \myapp{\myfun{even}}{\myb{x}}) \myarr \mynat =
2540 (\myb{x} {:} \mynat) \myarr (\myb{p} : \myapp{\myfun{even}}{\myb{x}}) \myarr \mynat
2543 We make use of various operations to manipulate telescopes:
2545 \item $\myhead(\mytele)$ refers to the first type appearing in
2546 $\mytele$: $\myhead((\myb{x} {:} \mynat); (\myb{p} :
2547 \myapp{\myfun{even}}{\myb{x}})) = \mynat$. Similarly,
2548 $\myix_i(\mytele)$ refers to the $i^{th}$ type in a telescope
2550 \item $\mytake_i(\mytele)$ refers to the telescope created by taking the
2551 first $i$ elements of $\mytele$: $\mytake_1((\myb{x} {:} \mynat); (\myb{p} :
2552 \myapp{\myfun{even}}{\myb{x}})) = (\myb{x} {:} \mynat)$.
2553 \item $\mytele \vec{A}$ refers to the telescope made by `applying' the
2554 terms in $\vec{A}$ on $\mytele$: $((\myb{x} {:} \mynat); (\myb{p} :
2555 \myapp{\myfun{even}}{\myb{x}}))42 = (\myb{p} :
2556 \myapp{\myfun{even}}{42})$.
2559 Additionally, when presenting syntax elaboration, I'll use $\mytmsyn^n$
2560 to indicate a term vector composed of $n$ elements, or
2561 $\mytmsyn^{\mytele}$ for one composed by as many elements as the
2564 \subsubsection{Declarations syntax}
2566 \begin{mydef}[Syntax of declarations in \mykant]\ \end{mydef}
2570 \begin{array}{r@{\ }c@{\ }l}
2571 \mydeclsyn & ::= & \myval{\myb{x}}{\mytmsyn}{\mytmsyn} \\
2572 & | & \mypost{\myb{x}}{\mytmsyn} \\
2573 & | & \myadt{\mytyc{D}}{\myappsp \mytelesyn}{}{\mydc{c} : \mytelesyn\ |\ \cdots } \\
2574 & | & \myreco{\mytyc{D}}{\myappsp \mytelesyn}{}{\myfun{f} : \mytmsyn,\ \cdots } \\
2576 \mytelesyn & ::= & \myemptytele \mysynsep \mytelesyn \mycc (\myb{x} {:} \mytmsyn) \\
2577 \mynamesyn & ::= & \cdots \mysynsep \mytyc{D} \mysynsep \mytyc{D}.\mydc{c} \mysynsep \mytyc{D}.\myfun{f}
2581 In \mykant\ we have four kind of declarations:
2584 \item[Defined value] A variable, together with a type and a body.
2585 \item[Abstract variable] An abstract variable, with a type but no body.
2586 \item[Inductive data] A \emph{data type}, with a \emph{type constructor}
2587 and various \emph{data constructors}, quite similar to what we find in
2588 Haskell. A primitive \emph{eliminator} (or \emph{destructor}, or
2589 \emph{recursor}) will be used to compute with each data type.
2590 \item[Record] A \emph{record}, which consists of one data constructor
2591 and various \emph{fields}, with no recursive occurrences. The
2592 functions extracting the fields' values from an instance of a record
2593 are called \emph{projections}.
2596 Elaborating defined variables consists of type checking the body against
2597 the given type, and updating the context to contain the new binding.
2598 Elaborating abstract variables and abstract variables consists of type
2599 checking the type, and updating the context with a new typed variable.
2601 \begin{mydef}[Elaboration of defined and abstract variables]\ \end{mydef}
2603 \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
2605 \AxiomC{$\mychk{\mytmt}{\mytya}$}
2606 \AxiomC{$\myfun{f} \not\in \myctx$}
2608 $\myctx \myelabt \myval{\myfun{f}}{\mytya}{\mytmt} \ \ \myelabf\ \ \myctx; \myfun{f} \mapsto \mytmt : \mytya$
2612 \AxiomC{$\mychk{\mytya}{\mytyp}$}
2613 \AxiomC{$\myfun{f} \not\in \myctx$}
2616 \myctx \myelabt \mypost{\myfun{f}}{\mytya}
2617 \ \ \myelabf\ \ \myctx; \myfun{f} : \mytya
2624 \subsubsection{User defined types}
2625 \label{sec:user-type}
2627 Elaborating user defined types is the real effort. First, we will
2628 explain what we can define, with some examples.
2631 \item[Natural numbers] To define natural numbers, we create a data type
2632 with two constructors: one with zero arguments ($\mydc{zero}$) and one
2633 with one recursive argument ($\mydc{suc}$):
2636 \myadt{\mynat}{ }{ }{
2637 \mydc{zero} \mydcsep \mydc{suc} \myappsp \mynat
2641 This is very similar to what we would write in Haskell:
2643 data Nat = Zero | Suc Nat
2645 Once the data type is defined, $\mykant$\ will generate syntactic
2646 constructs for the type and data constructors, so that we will have
2649 \begin{tabular}{ccc}
2650 \AxiomC{\phantom{$\mychk{\mytmt}{\mynat}$}}
2651 \UnaryInfC{$\myinf{\mynat}{\mytyp}$}
2654 \AxiomC{\phantom{$\mychk{\mytmt}{\mynat}$}}
2655 \UnaryInfC{$\myinf{\mytyc{\mynat}.\mydc{zero}}{\mynat}$}
2658 \AxiomC{$\mychk{\mytmt}{\mynat}$}
2659 \UnaryInfC{$\myinf{\mytyc{\mynat}.\mydc{suc} \myappsp \mytmt}{\mynat}$}
2663 While in Haskell (or indeed in Agda or Coq) data constructors are
2664 treated the same way as functions, in $\mykant$\ they are syntax, so
2665 for example using $\mytyc{\mynat}.\mydc{suc}$ on its own will give a
2666 syntax error. This is necessary so that we can easily infer the type
2667 of polymorphic data constructors, as we will see later.
2669 Moreover, each data constructor is prefixed by the type constructor
2670 name, since we need to retrieve the type constructor of a data
2671 constructor when type checking. This measure aids in the presentation
2672 of various features but it is not needed in the implementation, where
2673 we can have a dictionary to lookup the type constructor corresponding
2674 to each data constructor. When using data constructors in examples I
2675 will omit the type constructor prefix for brevity, in this case
2676 writing $\mydc{zero}$ instead of $\mynat.\mydc{suc}$ and $\mydc{suc}$ instead of
2677 $\mynat.\mydc{suc}$.
2679 Along with user defined constructors, $\mykant$\ automatically
2680 generates an \emph{eliminator}, or \emph{destructor}, to compute with
2681 natural numbers: If we have $\mytmt : \mynat$, we can destruct
2682 $\mytmt$ using the generated eliminator `$\mynat.\myfun{elim}$':
2685 \AxiomC{$\mychk{\mytmt}{\mynat}$}
2687 \myinf{\mytyc{\mynat}.\myfun{elim} \myappsp \mytmt}{
2689 \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}}
2693 $\mynat.\myfun{elim}$ corresponds to the induction principle for
2694 natural numbers: if we have a predicate on numbers ($\myb{P}$), and we
2695 know that predicate holds for the base case
2696 ($\myapp{\myb{P}}{\mydc{zero}}$) and for each inductive step
2697 ($\myfora{\myb{x}}{\mynat}{\myapp{\myb{P}}{\myb{x}} \myarr
2698 \myapp{\myb{P}}{(\myapp{\mydc{suc}}{\myb{x}})}}$), then $\myb{P}$
2699 holds for any number. As with the data constructors, we require the
2700 eliminator to be applied to the `destructed' element.
2702 While the induction principle is usually seen as a mean to prove
2703 properties about numbers, in the intuitionistic setting it is also a
2704 mean to compute. In this specific case $\mynat.\myfun{elim}$
2705 returns the base case if the provided number is $\mydc{zero}$, and
2706 recursively applies the inductive step if the number is a
2709 \begin{array}{@{}l@{}l}
2710 \mytyc{\mynat}.\myfun{elim} \myappsp \mydc{zero} & \myappsp \myse{P} \myappsp \myse{pz} \myappsp \myse{ps} \myred \myse{pz} \\
2711 \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})
2714 The Haskell equivalent would be
2716 elim :: Nat -> a -> (Nat -> a -> a) -> a
2717 elim Zero pz ps = pz
2718 elim (Suc n) pz ps = ps n (elim n pz ps)
2720 Which buys us the computational behaviour, but not the reasoning power,
2721 since we cannot express the notion of a predicate depending on
2722 $\mynat$---the type system is far too weak.
2724 \item[Binary trees] Now for a polymorphic data type: binary trees, since
2725 lists are too similar to natural numbers to be interesting.
2728 \myadt{\mytree}{\myappsp (\myb{A} {:} \mytyp)}{ }{
2729 \mydc{leaf} \mydcsep \mydc{node} \myappsp (\myapp{\mytree}{\myb{A}}) \myappsp \myb{A} \myappsp (\myapp{\mytree}{\myb{A}})
2733 Now the purpose of `constructors as syntax' can be explained: what would
2734 the type of $\mydc{leaf}$ be? If we were to treat it as a `normal'
2735 term, we would have to specify the type parameter of the tree each
2736 time the constructor is applied:
2738 \begin{array}{@{}l@{\ }l}
2739 \mydc{leaf} & : \myfora{\myb{A}}{\mytyp}{\myapp{\mytree}{\myb{A}}} \\
2740 \mydc{node} & : \myfora{\myb{A}}{\mytyp}{\myapp{\mytree}{\myb{A}} \myarr \myb{A} \myarr \myapp{\mytree}{\myb{A}} \myarr \myapp{\mytree}{\myb{A}}}
2743 The problem with this approach is that creating terms is incredibly
2744 verbose and dull, since we would need to specify the type parameters
2745 each time. For example if we wished to create a $\mytree \myappsp
2746 \mynat$ with two nodes and three leaves, we would write
2748 \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)
2750 The redundancy of $\mynat$s is quite irritating. Instead, if we treat
2751 constructors as syntactic elements, we can `extract' the type of the
2752 parameter from the type that the term gets checked against, much like
2753 what we do to type abstractions:
2757 \AxiomC{$\mychk{\mytya}{\mytyp}$}
2758 \UnaryInfC{$\mychk{\mydc{leaf}}{\myapp{\mytree}{\mytya}}$}
2761 \AxiomC{$\mychk{\mytmm}{\mytree \myappsp \mytya}$}
2762 \AxiomC{$\mychk{\mytmt}{\mytya}$}
2763 \AxiomC{$\mychk{\mytmm}{\mytree \myappsp \mytya}$}
2764 \TrinaryInfC{$\mychk{\mydc{node} \myappsp \mytmm \myappsp \mytmt \myappsp \mytmn}{\mytree \myappsp \mytya}$}
2768 Which enables us to write, much more concisely
2770 \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}
2772 We gain an annotation, but we lose the myriad of types applied to the
2773 constructors. Conversely, with the eliminator for $\mytree$, we can
2774 infer the type of the arguments given the type of the destructed:
2777 \AxiomC{$\myinf{\mytmt}{\myapp{\mytree}{\mytya}}$}
2779 \myinf{\mytree.\myfun{elim} \myappsp \mytmt}{
2781 (\myb{P} {:} \myapp{\mytree}{\mytya} \myarr \mytyp) \myarr \\
2782 \myapp{\myb{P}}{\mydc{leaf}} \myarr \\
2783 ((\myb{l} {:} \myapp{\mytree}{\mytya}) (\myb{x} {:} \mytya) (\myb{r} {:} \myapp{\mytree}{\mytya}) \myarr \myapp{\myb{P}}{\myb{l}} \myarr
2784 \myapp{\myb{P}}{\myb{r}} \myarr \myb{P} \myappsp (\mydc{node} \myappsp \myb{l} \myappsp \myb{x} \myappsp \myb{r})) \myarr \\
2785 \myapp{\myb{P}}{\mytmt}
2790 As expected, the eliminator embodies structural induction on trees.
2791 We have a base case for $\myb{P} \myappsp \mydc{leaf}$, and an
2792 inductive step that given two subtrees and the predicate applied to
2793 them needs to return the predicate applied to the tree formed by a
2794 node with the two subtrees as children.
2796 \item[Empty type] We have presented types that have at least one
2797 constructors, but nothing prevents us from defining types with
2798 \emph{no} constructors:
2799 \[\myadt{\mytyc{Empty}}{ }{ }{ }\]
2800 What shall the `induction principle' on $\mytyc{Empty}$ be? Does it
2801 even make sense to talk about induction on $\mytyc{Empty}$?
2802 $\mykant$\ does not care, and generates an eliminator with no `cases':
2805 \AxiomC{$\myinf{\mytmt}{\mytyc{Empty}}$}
2806 \UnaryInfC{$\myinf{\myempty.\myfun{elim} \myappsp \mytmt}{(\myb{P} {:} \mytmt \myarr \mytyp) \myarr \myapp{\myb{P}}{\mytmt}}$}
2808 which lets us write the $\myfun{absurd}$ that we know and love:
2811 \myfun{absurd} : (\myb{A} {:} \mytyp) \myarr \myempty \myarr \myb{A} \\
2812 \myfun{absurd}\myappsp \myb{A} \myappsp \myb{x} \mapsto \myempty.\myfun{elim} \myappsp \myb{x} \myappsp (\myabs{\myarg}{\myb{A}})
2816 \item[Ordered lists] Up to this point, the examples shown are nothing
2817 new to the \{Haskell, SML, OCaml, functional\} programmer. However
2818 dependent types let us express much more than that. A useful example
2819 is the type of ordered lists. There are many ways to define such a
2820 thing, but we will define our type to store the bounds of the list,
2821 making sure that $\mydc{cons}$ing respects that.
2823 First, using $\myunit$ and $\myempty$, we define a type expressing the
2824 ordering on natural numbers, $\myfun{le}$---`less or equal'.
2825 $\myfun{le}\myappsp \mytmm \myappsp \mytmn$ will be inhabited only if
2826 $\mytmm \le \mytmn$:
2829 \myfun{le} : \mynat \myarr \mynat \myarr \mytyp \\
2830 \myfun{le} \myappsp \myb{n} \mapsto \\
2831 \myind{2} \mynat.\myfun{elim} \\
2832 \myind{2}\myind{2} \myb{n} \\
2833 \myind{2}\myind{2} (\myabs{\myarg}{\mynat \myarr \mytyp}) \\
2834 \myind{2}\myind{2} (\myabs{\myarg}{\myunit}) \\
2835 \myind{2}\myind{2} (\myabs{\myb{n}\, \myb{f}\, \myb{m}}{
2836 \mynat.\myfun{elim} \myappsp \myb{m} \myappsp (\myabs{\myarg}{\mytyp}) \myappsp \myempty \myappsp (\myabs{\myb{m'}\, \myarg}{\myapp{\myb{f}}{\myb{m'}}})
2840 We return $\myunit$ if the scrutinised is $\mydc{zero}$ (every
2841 number in less or equal than zero), $\myempty$ if the first number is
2842 a $\mydc{suc}$cessor and the second a $\mydc{zero}$, and we recurse if
2843 they are both successors. Since we want the list to have possibly
2844 `open' bounds, for example for empty lists, we create a type for
2845 `lifted' naturals with a bottom ($\le$ everything but itself) and top
2846 ($\ge$ everything but itself) elements, along with an associated comparison
2850 \myadt{\mytyc{Lift}}{ }{ }{\mydc{bot} \mydcsep \mydc{lift} \myappsp \mynat \mydcsep \mydc{top}}\\
2851 \myfun{le'} : \mytyc{Lift} \myarr \mytyc{Lift} \myarr \mytyp\\
2852 \myfun{le'} \myappsp \myb{l_1} \mapsto \\
2853 \myind{2} \mytyc{Lift}.\myfun{elim} \\
2854 \myind{2}\myind{2} \myb{l_1} \\
2855 \myind{2}\myind{2} (\myabs{\myarg}{\mytyc{Lift} \myarr \mytyp}) \\
2856 \myind{2}\myind{2} (\myabs{\myarg}{\myunit}) \\
2857 \myind{2}\myind{2} (\myabs{\myb{n_1}\, \myb{n_2}}{
2858 \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
2860 \myind{2}\myind{2} (\myabs{\myb{n_1}\, \myb{n_2}}{
2861 \mytyc{Lift}.\myfun{elim} \myappsp \myb{l_2} \myappsp (\myabs{\myarg}{\mytyp}) \myappsp \myempty \myappsp (\myabs{\myarg}{\myempty}) \myappsp \myunit
2865 Finally, we can defined a type of ordered lists. The type is
2866 parametrised over two values representing the lower and upper bounds
2867 of the elements, as opposed to the type parameters that we are used
2868 to. Then, an empty list will have to have evidence that the bounds
2869 are ordered, and each time we add an element we require the list to
2870 have a matching lower bound:
2873 \myadt{\mytyc{OList}}{\myappsp (\myb{low}\ \myb{upp} {:} \mytyc{Lift})}{\\ \myind{2}}{
2874 \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})
2878 Note that in the $\mydc{cons}$ constructor we quantify over the first
2879 argument, which will determine the type of the following
2880 arguments---again something we cannot do in systems like Haskell. If
2881 we want we can then employ this structure to write and prove correct
2882 various sorting algorithms.\footnote{See this presentation by Conor
2884 \url{https://personal.cis.strath.ac.uk/conor.mcbride/Pivotal.pdf},
2885 and this blog post by the author:
2886 \url{http://mazzo.li/posts/AgdaSort.html}.}
2888 \item[Dependent products] Apart from $\mysyn{data}$, $\mykant$\ offers
2889 us another way to define types: $\mysyn{record}$. A record is a
2890 datatype with one constructor and `projections' to extract specific
2891 fields of the said constructor.
2893 For example, we can recover dependent products:
2896 \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}}}
2899 Here $\myfst$ and $\mysnd$ are the projections, with their respective
2900 types. Note that each field can refer to the preceding fields---in
2901 this case we have the type of $\myfun{snd}$ depending on the value of
2902 $\myfun{fst}$. A constructor will be automatically generated, under
2903 the name of $\mytyc{Prod}.\mydc{constr}$. Dually to data types, we
2904 will omit the type constructor prefix for record projections.
2906 Following the bidirectionality of the system, we have that projections
2907 (the destructors of the record) infer the type, while the constructor
2912 \AxiomC{$\mychk{\mytmm}{\mytya}$}
2913 \AxiomC{$\mychk{\mytmn}{\myapp{\mytyb}{\mytmm}}$}
2914 \BinaryInfC{$\mychk{\mytyc{Prod}.\mydc{constr} \myappsp \mytmm \myappsp \mytmn}{\mytyc{Prod} \myappsp \mytya \myappsp \mytyb}$}
2916 \UnaryInfC{\phantom{$\myinf{\myfun{snd} \myappsp \mytmt}{\mytyb \myappsp (\myfst \myappsp \mytmt)}$}}
2919 \AxiomC{$\hspace{0.2cm}\myinf{\mytmt}{\mytyc{Prod} \myappsp \mytya \myappsp \mytyb}\hspace{0.2cm}$}
2920 \UnaryInfC{$\myinf{\myfun{fst} \myappsp \mytmt}{\mytya}$}
2922 \UnaryInfC{$\myinf{\myfun{snd} \myappsp \mytmt}{\mytyb \myappsp (\myfst \myappsp \mytmt)}$}
2926 What we have defined here is equivalent to ITT's dependent products.
2934 \mynamesyn ::= \cdots \mysynsep \mytyc{D} \mysynsep \mytyc{D}.\mydc{c} \mysynsep \mytyc{D}.\myfun{f}
2941 \mydesc{syntax elaboration:}{\mydeclsyn \myelabf \mytmsyn ::= \cdots}{
2944 \begin{array}{r@{\ }l}
2945 & \myadt{\mytyc{D}}{\mytele}{}{\cdots\ |\ \mydc{c}_n : \mytele_n } \\
2948 \begin{array}{r@{\ }c@{\ }l}
2949 \mytmsyn & ::= & \cdots \mysynsep \myapp{\mytyc{D}}{\mytmsyn^{\mytele}} \mysynsep \cdots \mysynsep
2950 \mytyc{D}.\mydc{c}_n \myappsp \mytmsyn^{\mytele_n} \mysynsep \mytyc{D}.\myfun{elim} \myappsp \mytmsyn \\
2958 \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
2963 \myinf{\mytele \myarr \mytyp}{\mytyp}\hspace{0.8cm}
2964 \mytyc{D} \not\in \myctx \\
2965 \myinff{\myctx;\ \mytyc{D} : \mytele \myarr \mytyp}{\mytele \mycc \mytele_i \myarr \myapp{\mytyc{D}}{\mytelee}}{\mytyp}\ \ \ (1 \leq i \leq n) \\
2966 \text{For each $(\myb{x} {:} \mytya)$ in each $\mytele_i$, if $\mytyc{D} \in \mytya$, then $\mytya = \myapp{\mytyc{D}}{\vec{\mytmt}}$.}
2970 \begin{array}{r@{\ }c@{\ }l}
2971 \myctx & \myelabt & \myadt{\mytyc{D}}{\mytele}{}{ \cdots \ |\ \mydc{c}_n : \mytele_n } \\
2972 & & \vspace{-0.2cm} \\
2973 & \myelabf & \myctx;\ \mytyc{D} : \mytele \myarr \mytyp;\ \cdots;\ \mytyc{D}.\mydc{c}_n : \mytele \mycc \mytele_n \myarr \myapp{\mytyc{D}}{\mytelee}; \\
2975 \begin{array}{@{}r@{\ }l l}
2976 \mytyc{D}.\myfun{elim} : & \mytele \myarr (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr & \textbf{target} \\
2977 & (\myb{P} {:} \myapp{\mytyc{D}}{\mytelee} \myarr \mytyp) \myarr & \textbf{motive} \\
2981 (\mytele_n \mycc \myhyps(\myb{P}, \mytele_n) \myarr \myapp{\myb{P}}{(\myapp{\mytyc{D}.\mydc{c}_n}{\mytelee_n})}) \myarr
2982 \end{array} \right \}
2983 & \textbf{methods} \\
2984 & \myapp{\myb{P}}{\myb{x}} &
2988 \DisplayProof \\ \vspace{0.2cm}\ \\
2990 \begin{array}{@{}l l@{\ } l@{} r c l}
2991 \textbf{where} & \myhyps(\myb{P}, & \myemptytele &) & \mymetagoes & \myemptytele \\
2992 & \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) \\
2993 & \myhyps(\myb{P}, & (\myb{x} {:} \mytya) \mycc \mytele & ) & \mymetagoes & \myhyps(\myb{P}, \mytele)
3001 \mydesc{reduction elaboration:}{\mydeclsyn \myelabf \myctx \vdash \mytmsyn \myred \mytmsyn}{
3003 $\myadt{\mytyc{D}}{\mytele}{}{ \cdots \ |\ \mydc{c}_n : \mytele_n } \ \ \myelabf$
3004 \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
3005 \AxiomC{$\mytyc{D}.\mydc{c}_i : \mytele;\mytele_i \myarr \myapp{\mytyc{D}}{\mytelee} \in \myctx$}
3007 \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)}
3009 \DisplayProof \\ \vspace{0.2cm}\ \\
3011 \begin{array}{@{}l l@{\ } l@{} r c l}
3012 \textbf{where} & \myrecs(\myse{P}, \vec{m}, & \myemptytele &) & \mymetagoes & \myemptytele \\
3013 & \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) \\
3014 & \myrecs(\myse{P}, \vec{m}, & (\myb{x} {:} \mytya); \mytele &) & \mymetagoes & \myrecs(\myse{P}, \vec{m}, \mytele)
3021 \mydesc{syntax elaboration:}{\myelab{\mydeclsyn}{\mytmsyn ::= \cdots}}{
3024 \begin{array}{r@{\ }c@{\ }l}
3025 \myctx & \myelabt & \myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \\
3028 \begin{array}{r@{\ }c@{\ }l}
3029 \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 \\
3037 \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
3041 \myinf{\mytele \myarr \mytyp}{\mytyp}\hspace{0.8cm}
3042 \mytyc{D} \not\in \myctx \\
3043 \myinff{\myctx; \mytele; (\myb{f}_j : \myse{F}_j)_{j=1}^{i - 1}}{F_i}{\mytyp} \myind{3} (1 \le i \le n)
3047 \begin{array}{r@{\ }c@{\ }l}
3048 \myctx & \myelabt & \myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \\
3049 & & \vspace{-0.2cm} \\
3050 & \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}; \\
3051 & & \mytyc{D}.\mydc{constr} : \mytele \myarr \myse{F}_1 \myarr \cdots \myarr \myse{F}_n \myarr \myapp{\mytyc{D}}{\mytelee};
3059 \mydesc{reduction elaboration:}{\mydeclsyn \myelabf \myctx \vdash \mytmsyn \myred \mytmsyn}{
3061 $\myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \ \ \myelabf$
3062 \AxiomC{$\mytyc{D} \in \myctx$}
3063 \UnaryInfC{$\myctx \vdash \myapp{\mytyc{D}.\myfun{f}_i}{(\mytyc{D}.\mydc{constr} \myappsp \vec{t})} \myred t_i$}
3067 \caption{Elaboration for data types and records.}
3071 \begin{mydef}[Elaboration for user defined types]
3072 Following the intuition given by the examples, the full elaboration
3073 machinery is presented Figure \ref{fig:elab}.
3075 Our elaboration is essentially a modification of Figure 9 of
3076 \cite{McBride2004}. However, our data types are not inductive
3077 families,\footnote{See Section \ref{sec:future-work} for a brief
3078 description of inductive families.} we do bidirectional type checking
3079 by treating constructors/destructors as syntax, and we have records.
3081 \begin{mydef}[Strict positivity]
3082 A inductive type declaration is \emph{strictly positive} if recursive
3083 occurrences of the type we are defining do not appear embedded
3084 anywhere in the domain part of any function in the types for the data
3087 In data type declarations we allow recursive occurrences as long as they
3088 are strictly positive, which ensures the consistency of the theory. To
3089 achieve that we employing a syntactic check to make sure that this is
3090 the case---in fact the check is stricter than necessary for simplicity,
3091 given that we allow recursive occurrences only at the top level of data
3092 constructor arguments.
3094 Without these precautions, we can easily derive any type with no
3097 data Fix a = Fix (Fix a -> a) -- Negative occurrence of `Fix a'
3098 -- Term inhabiting any type `a'
3100 boom = (\f -> f (Fix f)) (\x -> (\(Fix f) -> f) x x)
3102 See \cite{Dybjer1991} for a more formal treatment of inductive
3105 For what concerns records, recursive occurrences are disallowed. The
3106 reason for this choice is answered by the reason for the choice of
3107 having records at all: we need records to give the user types with
3108 $\eta$-laws for equality, as we saw in Section \ref{sec:eta-expand}
3109 and in the treatment of OTT in Section \ref{sec:ott}. If we tried to
3110 $\eta$-expand recursive data types, we would expand forever.
3112 \begin{mydef}[Bidirectional type checking for elaborated types]
3113 To implement bidirectional type checking for constructors and
3114 destructors, we store their types in full in the context, and then
3115 instantiate when due.
3118 \mydesc{typing:}{\myctx \vdash \mytmsyn \Updownarrow \mytmsyn}{
3121 \mytyc{D} : \mytele \myarr \mytyp \in \myctx \hspace{1cm}
3122 \mytyc{D}.\mydc{c} : \mytele \mycc \mytele' \myarr
3123 \myapp{\mytyc{D}}{\mytelee} \in \myctx \\
3124 \mytele'' = (\mytele;\mytele')\vec{A} \hspace{1cm}
3125 \mychkk{\myctx; \mytake_{i-1}(\mytele'')}{t_i}{\myix_i( \mytele'')}\ \
3126 (1 \le i \le \mytele'')
3129 \UnaryInfC{$\mychk{\myapp{\mytyc{D}.\mydc{c}}{\vec{t}}}{\myapp{\mytyc{D}}{\vec{A}}}$}
3134 \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
3135 \AxiomC{$\mytyc{D}.\myfun{f} : \mytele \mycc (\myb{x} {:}
3136 \myapp{\mytyc{D}}{\mytelee}) \myarr \myse{F}$}
3137 \AxiomC{$\myjud{\mytmt}{\myapp{\mytyc{D}}{\vec{A}}}$}
3138 \TrinaryInfC{$\myinf{\myapp{\mytyc{D}.\myfun{f}}{\mytmt}}{(\mytele
3139 \mycc (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr
3140 \myse{F})(\vec{A};\mytmt)}$}
3144 \subsubsection{Why user defined types? Why eliminators?}
3146 The hardest design choice when designing $\mykant$\ was to decide
3147 whether user defined types should be included, and how to handle them.
3148 In the end, as we saw, we can devise general structures like $\mytyc{W}$
3149 that can express all inductive structures. However, using those tools
3150 beyond very simple examples is near-impossible for a human user. Thus
3151 most theorem provers in the wild provide some means for the user to
3152 define structures tailored to specific uses.
3154 Even if we take user defined types for granted, while there is not much
3155 debate on how to handle record, there are two broad schools of thought
3156 regarding the handling of data types:
3158 \item[Fixed points and pattern matching] The road chosen by Agda and Coq.
3159 Functions are written like in Haskell---matching on the input and with
3160 explicit recursion. An external check on the recursive arguments
3161 ensures that they are decreasing, and thus that all functions
3162 terminate. This approach is the best in terms of user usability, but
3163 it is tricky to implement correctly.
3165 \item[Elaboration into eliminators] The road chose by \mykant, and
3166 pioneered by the Epigram line of work. The advantage is that we can
3167 reduce every data type to simple definitions which guarantee
3168 termination and are simple to reduce and type. It is however more
3169 cumbersome to use than pattern maching, although \cite{McBride2004}
3170 has shown how to implement an expressive pattern matching interface on
3171 top of a larger set of combinators of those provided by \mykant.
3174 We chose the safer and easier to implement path, given the time
3175 constraints and the higher confidence of correctness. See also Section
3176 \ref{sec:future-work} for a brief overview of ways to extend or treat
3179 \subsection{Cumulative hierarchy and typical ambiguity}
3180 \label{sec:term-hierarchy}
3182 Having a well founded type hierarchy is crucial if we want to retain
3183 consistency, otherwise we can break our type systems by proving bottom,
3184 as shown in Appendix \ref{app:hurkens}.
3186 However, hierarchy as presented in section \ref{sec:itt} is a
3187 considerable burden on the user, on various levels. Consider for
3188 example how we recovered disjunctions in Section \ref{sec:disju}: we
3189 have a function that takes two $\mytyp_0$ and forms a new $\mytyp_0$.
3190 What if we wanted to form a disjunction containing something a
3191 $\mytyp_1$, or $\mytyp_{42}$? Our definition would fail us, since
3192 $\mytyp_1 : \mytyp_2$.
3196 \mydesc{cumulativity:}{\myctx \vdash \mytmsyn \mycumul \mytmsyn}{
3197 \begin{tabular}{ccc}
3198 \AxiomC{$\myctx \vdash \mytya \mydefeq \mytyb$}
3199 \UnaryInfC{$\myctx \vdash \mytya \mycumul \mytyb$}
3202 \AxiomC{\phantom{$\myctx \vdash \mytya \mydefeq \mytyb$}}
3203 \UnaryInfC{$\myctx \vdash \mytyp_l \mycumul \mytyp_{l+1}$}
3206 \AxiomC{$\myctx \vdash \mytya \mycumul \mytyb$}
3207 \AxiomC{$\myctx \vdash \mytyb \mycumul \myse{C}$}
3208 \BinaryInfC{$\myctx \vdash \mytya \mycumul \myse{C}$}
3214 \begin{tabular}{ccc}
3215 \AxiomC{$\myjud{\mytmt}{\mytya}$}
3216 \AxiomC{$\myctx \vdash \mytya \mycumul \mytyb$}
3217 \BinaryInfC{$\myjud{\mytmt}{\mytyb}$}
3220 \AxiomC{$\myctx \vdash \mytya_1 \mydefeq \mytya_2$}
3221 \AxiomC{$\myctx; \myb{x} : \mytya_1 \vdash \mytyb_1 \mycumul \mytyb_2$}
3222 \BinaryInfC{$\myctx (\myb{x} {:} \mytya_1) \myarr \mytyb_1 \mycumul (\myb{x} {:} \mytya_2) \myarr \mytyb_2$}
3226 \caption{Cumulativity rules for base types in \mykant, plus a
3227 `conversion' rule for cumulative types.}
3228 \label{fig:cumulativity}
3231 One way to solve this issue is a \emph{cumulative} hierarchy, where
3232 $\mytyp_{l_1} : \mytyp_{l_2}$ iff $l_1 < l_2$. This way we retain
3233 consistency, while allowing for `large' definitions that work on small
3236 \begin{mydef}[Cumulativity for \mykant' base types]
3237 Figure \ref{fig:cumulativity} gives a formal definition of
3238 cumulativity for the base types. Similar measures can be taken for
3239 user defined types, withe the type living in the least upper bound of
3240 the levels where the types contained data live.
3243 For example we might define our disjunction to be
3245 \myarg\myfun{$\vee$}\myarg : \mytyp_{100} \myarr \mytyp_{100} \myarr \mytyp_{100}
3247 And hope that $\mytyp_{100}$ will be large enough to fit all the types
3248 that we want to use with our disjunction. However, there are two
3249 problems with this. First, there is the obvious clumsyness of having to
3250 manually specify the size of types. More importantly, if we want to use
3251 $\myfun{$\vee$}$ itself as an argument to other type-formers, we need to
3252 make sure that those allow for types at least as large as
3255 A better option is to employ a mechanised version of what Russell called
3256 \emph{typical ambiguity}: we let the user live under the illusion that
3257 $\mytyp : \mytyp$, but check that the statements about types are
3258 consistent under the hood. $\mykant$\ implements this along the lines
3259 of \cite{Huet1988}. See also \cite{Harper1991} for a published
3260 reference, although describing a more complex system allowing for both
3261 explicit and explicit hierarchy at the same time.
3263 We define a partial ordering on the levels, with both weak ($\le$) and
3264 strong ($<$) constraints---the laws governing them being the same as the
3265 ones governing $<$ and $\le$ for the natural numbers. Each occurrence
3266 of $\mytyp$ is decorated with a unique reference, and we keep a set of
3267 constraints and add new constraints as we type check, generating new
3268 references when needed.
3270 For example, when type checking the type $\mytyp\, r_1$, where $r_1$
3271 denotes the unique reference assigned to that term, we will generate a
3272 new fresh reference $\mytyp\, r_2$, and add the constraint $r_1 < r_2$
3273 to the set. When type checking $\myctx \vdash
3274 \myfora{\myb{x}}{\mytya}{\mytyb}$, if $\myctx \vdash \mytya : \mytyp\,
3275 r_1$ and $\myctx; \myb{x} : \mytyb \vdash \mytyb : \mytyp\,r_2$; we will
3276 generate new reference $r$ and add $r_1 \le r$ and $r_2 \le r$ to the
3279 If at any point the constraint set becomes inconsistent, type checking
3280 fails. Moreover, when comparing two $\mytyp$ terms we equate their
3281 respective references with two $\le$ constraints. Implementation
3282 details are given in Section \ref{sec:hier-impl}.
3284 Another more flexible but also more verbose alternative is the one
3285 chosen by Agda, where levels can be quantified so that the relationship
3286 between arguments and result in type formers can be explicitly
3289 \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}
3291 Inference algorithms to automatically derive this kind of relationship
3292 are currently subject of research. We chose less flexible but more
3293 concise way, since it is easier to implement and better understood.
3295 \subsection{Observational equality, \mykant\ style}
3297 There are two correlated differences between $\mykant$\ and the theory
3298 used to present OTT. The first is that in $\mykant$ we have a type
3299 hierarchy, which lets us, for example, abstract over types. The second
3300 is that we let the user define inductive types and records.
3302 Reconciling propositions for OTT and a hierarchy had already been
3303 investigated by Conor McBride,\footnote{See
3304 \url{http://www.e-pig.org/epilogue/index.html?p=1098.html}.} and we
3305 follow his broad design plan, although with some innovation. Most of
3306 the work, as an extension of elaboration, is to handle reduction rules
3307 and coercions for data types---both type constructors and data
3310 \subsubsection{The \mykant\ prelude, and $\myprop$ositions}
3312 Before defining $\myprop$, we define some basic types inside $\mykant$,
3313 as the target for the $\myprop$ decoder.
3315 \begin{mydef}[\mykant' propositional prelude]\ \end{mydef}
3318 \myadt{\mytyc{Empty}}{}{ }{ } \\
3319 \myfun{absurd} : (\myb{A} {:} \mytyp) \myarr \mytyc{Empty} \myarr \myb{A} \mapsto \\
3320 \myind{2} \myabs{\myb{A\ \myb{bot}}}{\mytyc{Empty}.\myfun{elim} \myappsp \myb{bot} \myappsp (\myabs{\_}{\myb{A}})} \\
3323 \myreco{\mytyc{Unit}}{}{}{ } \\ \ \\
3325 \myreco{\mytyc{Prod}}{\myappsp (\myb{A}\ \myb{B} {:} \mytyp)}{ }{\myfun{fst} : \myb{A}, \myfun{snd} : \myb{B} }
3329 \begin{mydef}[Propositions and decoding]\ \end{mydef}
3333 \begin{array}{r@{\ }c@{\ }l}
3334 \mytmsyn & ::= & \cdots \mysynsep \myprdec{\myprsyn} \\
3335 \myprsyn & ::= & \mybot \mysynsep \mytop \mysynsep \myprsyn \myand \myprsyn \mysynsep \myprfora{\myb{x}}{\mytmsyn}{\myprsyn}
3340 \mydesc{proposition decoding:}{\myprdec{\mytmsyn} \myred \mytmsyn}{
3343 \begin{array}{l@{\ }c@{\ }l}
3344 \myprdec{\mybot} & \myred & \myempty \\
3345 \myprdec{\mytop} & \myred & \myunit
3350 \begin{array}{r@{ }c@{ }l@{\ }c@{\ }l}
3351 \myprdec{&\myse{P} \myand \myse{Q} &} & \myred & \mytyc{Prod} \myappsp \myprdec{\myse{P}} \myappsp \myprdec{\myse{Q}} \\
3352 \myprdec{&\myprfora{\myb{x}}{\mytya}{\myse{P}} &} & \myred &
3353 \myfora{\myb{x}}{\mytya}{\myprdec{\myse{P}}}
3359 We will overload the $\myand$ symbol to define `nested' products, and
3360 $\myproj{n}$ to project elements from them, so that
3363 \mytya \myand \mytyb = \mytya \myand (\mytyb \myand \mytop) \\
3364 \mytya \myand \mytyb \myand \myse{C} = \mytya \myand (\mytyb \myand (\myse{C} \myand \mytop)) \\
3366 \myproj{1} : \myprdec{\mytya \myand \mytyb} \myarr \myprdec{\mytya} \\
3367 \myproj{2} : \myprdec{\mytya \myand \mytyb \myand \myse{C}} \myarr \myprdec{\mytyb} \\
3371 And so on, so that $\myproj{n}$ will work with all products with at
3372 least than $n$ elements. Logically a 0-ary $\myand$ will correspond to
3375 \subsubsection{Some OTT examples}
3377 Before presenting the direction that $\mykant$\ takes, let us consider
3378 two examples of use-defined data types, and the result we would expect
3379 given what we already know about OTT, assuming the same propositional
3384 \item[Product types] Let us consider first the already mentioned
3385 dependent product, using the alternate name $\mysigma$\footnote{For
3386 extra confusion, `dependent products' are often called `dependent
3387 sums' in the literature, referring to the interpretation that
3388 identifies the first element as a `tag' deciding the type of the
3389 second element, which lets us recover sum types (disjuctions), as we
3390 saw in Section \ref{sec:depprod}. Thus, $\mysigma$.} to
3391 avoid confusion with the $\mytyc{Prod}$ in the prelude:
3394 \myreco{\mysigma}{\myappsp (\myb{A} {:} \mytyp) \myappsp (\myb{B} {:} \myb{A} \myarr \mytyp)}{\\ \myind{2}}{\myfst : \myb{A}, \mysnd : \myapp{\myb{B}}{\myb{fst}}}
3397 First type-level equality. The result we want is
3400 \mysigma \myappsp \mytya_1 \myappsp \mytyb_1 \myeq \mysigma \myappsp \mytya_2 \myappsp \mytyb_2 \myred \\
3401 \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}}}
3404 The difference here is that in the original presentation of OTT
3405 the type binders are explicit, while here $\mytyb_1$ and $\mytyb_2$ are
3406 functions returning types. We can do this thanks to the type
3407 hierarchy, and this hints at the fact that heterogeneous equality will
3408 have to allow $\mytyp$ `to the right of the colon', and in fact this
3409 provides the solution to simplify the equality above.
3411 If we take, just like we saw previously in OTT
3414 \myjm{\myse{f}_1}{\myfora{\mytya_1}{\myb{x_1}}{\mytyb_1}}{\myse{f}_2}{\myfora{\mytya_2}{\myb{x_2}}{\mytyb_2}} \myred \\
3415 \myind{2} \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{
3416 \myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2} \myimpl
3417 \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}]}
3421 Then we can simply take
3424 \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}
3427 Which will reduce to precisely what we desire. For what
3428 concerns coercions and quotation, things stay the same (apart from the
3429 fact that we apply to the second argument instead of substituting).
3430 We can recognise records such as $\mysigma$ as such and employ
3431 projections in value equality and coercions; as to not
3432 impede progress if not necessary.
3434 \item[Lists] Now for finite lists, which will give us a taste for data
3438 \myadt{\mylist}{\myappsp (\myb{A} {:} \mytyp)}{ }{\mydc{nil} \mydcsep \mydc{cons} \myappsp \myb{A} \myappsp (\myapp{\mylist}{\myb{A}})}
3441 Type equality is simple---we only need to compare the parameter:
3443 \mylist \myappsp \mytya_1 \myeq \mylist \myappsp \mytya_2 \myred \mytya_1 \myeq \mytya_2
3445 For coercions, we transport based on the constructor, recycling the
3446 proof for the inductive occurrence:
3448 \begin{array}{@{}l@{\ }c@{\ }l}
3449 \mycoe \myappsp (\mylist \myappsp \mytya_1) \myappsp (\mylist \myappsp \mytya_2) \myappsp \myse{Q} \myappsp \mydc{nil} & \myred & \mydc{nil} \\
3450 \mycoe \myappsp (\mylist \myappsp \mytya_1) \myappsp (\mylist \myappsp \mytya_2) \myappsp \myse{Q} \myappsp (\mydc{cons} \myappsp \mytmm \myappsp \mytmn) & \myred & \\
3451 \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)}
3454 Value equality is unsurprising---we match the constructors, and
3455 return bottom for mismatches. However, we also need to equate the
3456 parameter in $\mydc{nil}$:
3458 \begin{array}{r@{ }c@{\ }c@{\ }c@{}l@{\ }c@{\ }r@{}c@{\ }c@{\ }c@{}l@{\ }l}
3459 (& \mydc{nil} & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{nil} & : & \myapp{\mylist}{\mytya_2} &) \myred \mytya_1 \myeq \mytya_2 \\
3460 (& \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 \\
3461 & \multicolumn{11}{@{}l}{ \myind{2}
3462 \myjm{\mytmm_1}{\mytya_1}{\mytmm_2}{\mytya_2} \myand \myjm{\mytmn_1}{\myapp{\mylist}{\mytya_1}}{\mytmn_2}{\myapp{\mylist}{\mytya_2}}
3464 (& \mydc{nil} & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{cons} \myappsp \mytmm_2 \myappsp \mytmn_2 & : & \myapp{\mylist}{\mytya_2} &) \myred \mybot \\
3465 (& \mydc{cons} \myappsp \mytmm_1 \myappsp \mytmn_1 & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{nil} & : & \myapp{\mylist}{\mytya_2} &) \myred \mybot
3470 Now for something useless but complicated. % TODO finish
3474 \subsubsection{Only one equality}
3476 Given the examples above, a more `flexible' heterogeneous equality must
3477 emerge, since of the fact that in $\mykant$ we re-gain the possibility
3478 of abstracting and in general handling types in a way that was not
3479 possible in the original OTT presentation. Moreover, we found that the
3480 rules for value equality work very well if used with user defined type
3481 abstractions---for example in the case of dependent products we recover
3482 the original definition with explicit binders, in a very simple manner.
3484 In fact, we can drop a separate notion of type-equality, which will
3485 simply be served by $\myjm{\mytya}{\mytyp}{\mytyb}{\mytyp}$, from now on
3486 abbreviated as $\mytya \myeq \mytyb$. We shall still distinguish
3487 equalities relating types for hierarchical purposes. The full rules for
3488 equality reductions, along with the syntax for propositions, are given
3489 in figure \ref{fig:kant-eq-red}. We exploit record to perform
3490 $\eta$-expansion. Moreover, given the nested $\myand$s, values of data
3491 types with zero constructors (such as $\myempty$) and records with zero
3492 destructors (such as $\myunit$) will be automatically always identified
3499 \begin{array}{r@{\ }c@{\ }l}
3500 \myprsyn & ::= & \cdots \mysynsep \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
3505 % \mytmsyn & ::= & \cdots \mysynsep \mycoee{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \mysynsep
3506 % \mycohh{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
3507 % \myprsyn & ::= & \cdots \mysynsep \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
3511 % \mydesc{typing:}{\myctx \vdash \mytmsyn \Leftrightarrow \mytmsyn}{
3513 % \begin{tabular}{cc}
3514 % \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
3515 % \AxiomC{$\myjud{\mytmt}{\mytya}$}
3516 % \BinaryInfC{$\myinf{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}$}
3519 % \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
3520 % \AxiomC{$\myjud{\mytmt}{\mytya}$}
3521 % \BinaryInfC{$\myinf{\mycohh{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\myprdec{\myjm{\mytmt}{\mytya}{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}}}$}
3528 \mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
3531 \AxiomC{\phantom{$\myjud{\myse{P}}{\myprop}$}}
3532 \UnaryInfC{$\myjud{\mytop}{\myprop}$}
3534 \UnaryInfC{$\myjud{\mybot}{\myprop}$}
3537 \AxiomC{$\myjud{\myse{P}}{\myprop}$}
3538 \AxiomC{$\myjud{\myse{Q}}{\myprop}$}
3539 \BinaryInfC{$\myjud{\myse{P} \myand \myse{Q}}{\myprop}$}
3541 \UnaryInfC{\phantom{$\myjud{\mybot}{\myprop}$}}
3550 \phantom{\myjud{\myse{A}}{\mytyp} \hspace{0.8cm} \myjud{\mytmm}{\myse{A}}} \\
3551 \myjud{\myse{A}}{\mytyp}\hspace{0.8cm}
3552 \myjudd{\myctx; \myb{x} : \mytya}{\myse{P}}{\myprop}
3555 \UnaryInfC{$\myjud{\myprfora{\myb{x}}{\mytya}{\myse{P}}}{\myprop}$}
3560 \myjud{\myse{A}}{\mytyp} \hspace{0.8cm} \myjud{\mytmm}{\myse{A}} \\
3561 \myjud{\myse{B}}{\mytyp} \hspace{0.8cm} \myjud{\mytmn}{\myse{B}}
3564 \UnaryInfC{$\myjud{\myjm{\mytmm}{\myse{A}}{\mytmn}{\myse{B}}}{\myprop}$}
3570 % TODO add syntax and types for coe and coh
3571 \mydesc{equality reduction:}{\myctx \vdash \myprsyn \myred \myprsyn}{
3575 \UnaryInfC{$\myctx \vdash \myjm{\mytyp}{\mytyp}{\mytyp}{\mytyp} \myred \mytop$}
3579 \UnaryInfC{$\myctx \vdash \myjm{\myprdec{\myse{P}}}{\mytyp}{\myprdec{\myse{Q}}}{\mytyp} \myred \mytop$}
3587 \begin{array}{@{}r@{\ }l}
3589 \myjm{\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}}{\mytyp}{\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}}{\mytyp} \myred \\
3590 & \myind{2} \mytya_2 \myeq \mytya_1 \myand \myprfora{\myb{x_2}}{\mytya_2}{\myprfora{\myb{x_1}}{\mytya_1}{
3591 \myjm{\myb{x_2}}{\mytya_2}{\myb{x_1}}{\mytya_1} \myimpl \mytyb_1[\myb{x_1}] \myeq \mytyb_2[\myb{x_2}]
3601 \begin{array}{@{}r@{\ }l}
3603 \myjm{\myse{f}_1}{\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}}{\myse{f}_2}{\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}} \myred \\
3604 & \myind{2} \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{
3605 \myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2} \myimpl
3606 \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}]}
3615 \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
3617 \begin{array}{r@{\ }l}
3619 \myjm{\mytyc{D} \myappsp \vec{A}}{\mytyp}{\mytyc{D} \myappsp \vec{B}}{\mytyp} \myred \\
3620 & \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}))})
3629 \mydataty(\mytyc{D}, \myctx)\hspace{0.8cm}
3630 \mytyc{D}.\mydc{c} : \mytele;\mytele' \myarr \mytyc{D} \myappsp \mytelee \in \myctx \hspace{0.8cm}
3631 \mytele_A = (\mytele;\mytele')\vec{A}\hspace{0.8cm}
3632 \mytele_B = (\mytele;\mytele')\vec{B}
3636 \begin{array}{@{}l@{\ }l}
3637 \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 \\
3638 & \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}))})
3645 \AxiomC{$\mydataty(\mytyc{D}, \myctx)$}
3647 \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
3655 \myisreco(\mytyc{D}, \myctx)\hspace{0.8cm}
3656 \mytyc{D}.\myfun{f}_i : \mytele; (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr \myse{F}_i \in \myctx\\
3660 \begin{array}{@{}l@{\ }l}
3661 \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})})
3668 \UnaryInfC{$\myjm{\mytmm}{\mytya}{\mytmn}{\mytyb} \myred \mybot\ \text{if $\mytya$ and $\mytyb$ are canonical types.}$}
3671 \caption{Propositions and equality reduction in $\mykant$. We assume
3672 the presence of $\mydataty$ and $\myisreco$ as operations on the
3673 context to recognise whether a user defined type is a data type or a
3675 \label{fig:kant-eq-red}
3678 \subsubsection{Coercions}
3680 For coercions the algorithm is messier and not reproduced here for lack
3681 of a decent notation---the details are hairy but uninteresting. To give
3682 an idea of the possible complications, let us conceive a type that
3683 showcases trouble not arising in the previous examples.
3686 \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}}{
3687 \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})
3691 For type equalities we will have
3693 \begin{array}{@{}l@{\ }l}
3694 \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]
3696 \myjm{\mytya_1}{\mynat \myarr \mytyp}{\mytya_2}{\mynat \myarr \mytyp} \myand \\
3697 \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} \\
3698 \myjm{\myse{k}_1}{\mynat}{\myse{k}_2}{\mynat}
3699 \end{array} & \myred \\[0.7cm]
3701 (\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 \\
3702 (\mynat \myeq \mynat \myand \left(
3704 \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}}
3707 \myjm{\myse{k}_1}{\mynat}{\myse{k}_2}{\mynat}
3708 \end{array} & \myred \\[0.9cm]
3710 (\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 \\
3711 (\mytop \myand \left(
3713 \myprfora{\myb{x_1}\, \myb{x_2}}{\mynat}{\myjm{\myb{x_1}}{\mynat}{\myb{x_2}}{\mynat} \myimpl \\
3714 \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 \\
3715 \mytyb_1 \myappsp \myb{x_1} \myappsp \myb{y_1} \myeq \mytyb_2 \myappsp \myb{x_2} \myappsp \myb{y_2}}}}
3718 \myjm{\myse{k}_1}{\mynat}{\myse{k}_2}{\mynat}
3722 The result, while looking complicated, is actually saying something
3723 simple---given equal inputs, the parameters for $\mytyc{Max}$ will
3724 return equal types. Moreover, we have evidence that the two $\myb{k}$
3725 parameters are equal. When coercing, we need to mechanically generate
3726 one proof of equality for each argument, and then coerce:
3729 \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 \\
3731 \begin{array}[t]{l@{\ }l@{\ }c@{\ }l}
3732 \mysyn{let} & \myb{Q_{Ak}} & \mapsto & \myhole{?} : \myprdec{\mytya_1 \myappsp \myse{k}_1 \myeq \mytya_2 \myappsp \myse{k}_2} \\
3733 & \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 \\
3734 & \myb{Q_{\mathbb{N}}} & \mapsto & \myhole{?} : \myprdec{\mynat \myeq \mynat} \\
3735 & \myb{n_2} & \mapsto & \mycoee{\mynat}{\mynat}{\myb{Q_{\mathbb{N}}}}{\myse{n_1}} : \mynat \\
3736 & \myb{Q_A} & \mapsto & \myhole{?} : \myprdec{\mytya_1 \myappsp \myse{n_1} \myeq \mytya_2 \myappsp \myb{n_2}} \\
3737 & \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} \\
3738 & \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}} \\
3739 & \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} \\
3740 \mysyn{in} & \multicolumn{3}{@{}l}{\mydc{max} \myappsp \myb{ak_2} \myappsp \myb{n_2} \myappsp \myb{a_2} \myappsp \myb{b_2}}
3744 For equalities regarding types that are external to the data type we can
3745 derive a proof by reflexivity by invoking $\mydc{refl}$ as defined in
3746 Section \ref{sec:lazy}, and the instantiate arguments if we need too.
3747 In this case, for $\mynat$, we do not have any arguments. For
3748 equalities concerning arguments of the type constructor or already
3749 coerced arguments of the type constructor we have to refer to the right
3750 proof and use $\mycoh$erence when due, which is where the technical
3754 \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 \\
3756 \begin{array}[t]{l@{\ }l@{\ }c@{\ }l}
3757 \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} \\
3758 & \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 \\
3759 & \myb{Q_{\mathbb{N}}} & \mapsto & \mydc{refl} \myappsp \mynat : \myprdec{\mynat \myeq \mynat} \\
3760 & \myb{n_2} & \mapsto & \mycoee{\mynat}{\mynat}{\myb{Q_{\mathbb{N}}}}{\myse{n_1}} : \mynat \\
3761 & \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}} \\
3762 & \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} \\
3763 & \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}} \\
3764 & \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} \\
3765 \mysyn{in} & \multicolumn{3}{@{}l}{\mydc{max} \myappsp \myb{ak_2} \myappsp \myb{n_2} \myappsp \myb{a_2} \myappsp \myb{b_2}}
3773 \subsubsection{$\myprop$ and the hierarchy}
3775 We shall have, at earch universe level, not only a $\mytyp_l$ but also a
3776 $\myprop_l$. Where will propositions placed in the type hierarchy? The
3777 main indicator is the decoding operator, since it converts into things
3778 that already live in the hierarchy. For example, if we have
3780 \myprdec{\mynat \myarr \mybool \myeq \mynat \myarr \mybool} \myred
3781 \mytop \myand ((\myb{x}\, \myb{y} : \mynat) \myarr \mytop \myarr \mytop)
3783 we will better make sure that the `to be decoded' is at level compatible
3784 (read: larger) with its reduction. In the example above, we'll have
3785 that proposition to be at least as large as the type of $\mynat$, since
3786 the reduced proof will abstract over it. Pretending that we had
3787 explicit, non cumulative levels, it would be tempting to have
3790 \AxiomC{$\myjud{\myse{Q}}{\myprop_l}$}
3791 \UnaryInfC{$\myjud{\myprdec{\myse{Q}}}{\mytyp_l}$}
3794 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
3795 \AxiomC{$\myjud{\mytyb}{\mytyp_l}$}
3796 \BinaryInfC{$\myjud{\myjm{\mytya}{\mytyp_{l}}{\mytyb}{\mytyp_{l}}}{\myprop_l}$}
3800 $\mybot$ and $\mytop$ living at any level, $\myand$ and $\forall$
3801 following rules similar to the ones for $\myprod$ and $\myarr$ in
3802 Section \ref{sec:itt}. However, we need to be careful with value
3803 equality since for example we have that
3805 \myprdec{\myjm{\myse{f}_1}{\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}}{\myse{f}_2}{\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}}}
3807 \myfora{\myb{x_1}}{\mytya_1}{\myfora{\myb{x_2}}{\mytya_2}{\cdots}}
3809 where the proposition decodes into something of at least type $\mytyp_l$, where
3810 $\mytya_l : \mytyp_l$ and $\mytyb_l : \mytyp_l$. We can resolve this
3811 tension by making all equalities larger:
3813 \AxiomC{$\myjud{\mytmm}{\mytya}$}
3814 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
3815 \AxiomC{$\myjud{\mytmn}{\mytyb}$}
3816 \AxiomC{$\myjud{\mytyb}{\mytyp_l}$}
3817 \QuaternaryInfC{$\myjud{\myjm{\mytmm}{\mytya}{\mytmm}{\mytya}}{\myprop_l}$}
3819 This is disappointing, since type equalities will be needlessly large:
3820 $\myprdec{\myjm{\mytya}{\mytyp_l}{\mytyb}{\mytyp_l}} : \mytyp_{l + 1}$.
3822 However, considering that our theory is cumulative, we can do better.
3823 Assuming rules for $\myprop$ cumulativity similar to the ones for
3824 $\mytyp$, we will have (with the conversion rule reproduced as a
3828 \AxiomC{$\myctx \vdash \mytya \mycumul \mytyb$}
3829 \AxiomC{$\myjud{\mytmt}{\mytya}$}
3830 \BinaryInfC{$\myjud{\mytmt}{\mytyb}$}
3833 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
3834 \AxiomC{$\myjud{\mytyb}{\mytyp_l}$}
3835 \BinaryInfC{$\myjud{\myjm{\mytya}{\mytyp_{l}}{\mytyb}{\mytyp_{l}}}{\myprop_l}$}
3841 \AxiomC{$\myjud{\mytmm}{\mytya}$}
3842 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
3843 \AxiomC{$\myjud{\mytmn}{\mytyb}$}
3844 \AxiomC{$\myjud{\mytyb}{\mytyp_l}$}
3845 \AxiomC{$\mytya$ and $\mytyb$ are not $\mytyp_{l'}$}
3846 \QuinaryInfC{$\myjud{\myjm{\mytmm}{\mytya}{\mytmm}{\mytya}}{\myprop_l}$}
3850 That is, we are small when we can (type equalities) and large otherwise.
3851 This would not work in a non-cumulative theory because subject reduction
3852 would not hold. Consider for instance
3854 \myjm{\mynat}{\myITE{\mytrue}{\mytyp_0}{\mytyp_0}}{\mybool}{\myITE{\mytrue}{\mytyp_0}{\mytyp_0}}
3858 \[\myjm{\mynat}{\mytyp_0}{\mybool}{\mytyp_0} : \myprop_0 \]
3859 We need members of $\myprop_0$ to be members of $\myprop_1$ too, which
3860 will be the case with cumulativity. This is not the most elegant of
3861 systems, but it buys us a cheap type level equality without having to
3862 replicate functionality with a dedicated construct.
3864 \subsubsection{Quotation and definitional equality}
3865 \label{sec:kant-irr}
3867 Now we can give an account of definitional equality, by explaining how
3868 to perform quotation (as defined in Section \ref{sec:eta-expand})
3869 towards the goal described in Section \ref{sec:ott-quot}.
3873 \item Perform $\eta$-expansion on functions and records.
3875 \item As a consequence of the previous point, identify all records with
3876 no projections as equal, since they will have only one element.
3878 \item Identify all members of types with no elements as equal.
3880 \item Identify all equivalent proofs as equal---with `equivalent proof'
3881 we mean those proving the same propositions.
3883 \item Advance coercions working across definitionally equal types.
3885 Towards these goals and following the intuition between bidirectional
3886 type checking we define two mutually recursive functions, one quoting
3887 canonical terms against their types (since we need the type to typecheck
3888 canonical terms), one quoting neutral terms while recovering their
3889 types. The full procedure for quotation is shown in Figure
3890 \ref{fig:kant-quot}. We $\boxed{\text{box}}$ the neutral proofs and
3891 neutral members of empty types, following the notation in
3892 \cite{Altenkirch2007}, and we make use of $\mydefeq_{\mybox}$ which
3893 compares terms syntactically up to $\alpha$-renaming, but also up to
3894 equivalent proofs: we consider all boxed content as equal.
3896 Our quotation will work on normalised terms, so that all defined values
3897 will have been replaced. Moreover, we match on datatype eliminators and
3898 all their arguments, so that $\mynat.\myfun{elim} \myappsp \mytmm
3899 \myappsp \myse{P} \myappsp \vec{\mytmn}$ will stand for
3900 $\mynat.\myfun{elim}$ applied to the scrutinised $\mynat$, the
3901 predicate, and the two cases. This measure can be easily implemented by
3902 checking the head of applications and `consuming' the needed terms.
3905 \mydesc{canonical quotation:}{\mycanquot(\myctx, \mytmsyn : \mytmsyn) \mymetagoes \mytmsyn}{
3908 \begin{array}{@{}l@{}l}
3909 \mycanquot(\myctx,\ \mytmt : \mytyc{D} \myappsp \vec{A} &) \mymetaguard \mymeta{empty}(\myctx, \mytyc{D}) \mymetagoes \boxed{\mytmt} \\
3910 \mycanquot(\myctx,\ \mytmt : \mytyc{D} \myappsp \vec{A} &) \mymetaguard \mymeta{record}(\myctx, \mytyc{D}) \mymetagoes \mytyc{D}.\mydc{constr} \myappsp \cdots \myappsp \mycanquot(\myctx, \mytyc{D}.\myfun{f}_n : (\myctx(\mytyc{D}.\myfun{f}_n))(\vec{A};\mytmt)) \\
3911 \mycanquot(\myctx,\ \mytyc{D}.\mydc{c} \myappsp \vec{t} : \mytyc{D} \myappsp \vec{A} &) \mymetagoes \cdots \\
3912 \mycanquot(\myctx,\ \myse{f} : \myfora{\myb{x}}{\mytya}{\mytyb} &) \mymetagoes \myabs{\myb{x}}{\mycanquot(\myctx; \myb{x} : \mytya, \myapp{\myse{f}}{\myb{x}} : \mytyb)} \\
3913 \mycanquot(\myctx,\ \myse{p} : \myprdec{\myse{P}} &) \mymetagoes \boxed{\myse{p}}
3915 \mycanquot(\myctx,\ \mytmt : \mytya &) \mymetagoes \mytmt'\ \text{\textbf{where}}\ \mytmt' : \myarg = \myneuquot(\myctx, \mytmt)
3922 \mydesc{neutral quotation:}{\myneuquot(\myctx, \mytmsyn) \mymetagoes \mytmsyn : \mytmsyn}{
3925 \begin{array}{@{}l@{}l}
3926 \myneuquot(\myctx,\ \myb{x} &) \mymetagoes \myb{x} : \myctx(\myb{x}) \\
3927 \myneuquot(\myctx,\ \mytyp &) \mymetagoes \mytyp : \mytyp \\
3928 \myneuquot(\myctx,\ \myfora{\myb{x}}{\mytya}{\mytyb} & ) \mymetagoes
3929 \myfora{\myb{x}}{\myneuquot(\myctx, \mytya)}{\myneuquot(\myctx; \myb{x} : \mytya, \mytyb)} : \mytyp \\
3930 \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 \\
3931 \myneuquot(\myctx,\ \myprdec{\myjm{\mytmm}{\mytya}{\mytmn}{\mytyb}} &) \mymetagoes \myprdec{\myjm{\mycanquot(\myctx, \mytmm : \mytya)}{\mytya'}{\mycanquot(\myctx, \mytmn : \mytyb)}{\mytyb'}} : \mytyp \\
3932 \multicolumn{2}{@{}l}{\myind{2}\text{\textbf{where}}\ \mytya' : \myarg = \myneuquot(\myctx, \mytya)} \\
3933 \multicolumn{2}{@{}l}{\myind{2}\phantom{\text{\textbf{where}}}\ \mytyb' : \myarg = \myneuquot(\myctx, \mytyb)} \\
3934 \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) \\
3935 \multicolumn{2}{@{}l}{\myind{2}\text{\textbf{where}}\ \mytmt' : \mytyc{D} \myappsp \vec{A} = \myneuquot(\myctx, \mytmt)} \\
3936 \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 \\
3937 \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\\
3938 \multicolumn{2}{@{}l}{\myind{2}\text{\textbf{where}}\ \mytmm' : \mytyc{D} \myappsp \vec{A} = \myneuquot(\myctx, \mytmm)} \\
3939 \myneuquot(\myctx,\ \myapp{\myse{f}}{\mytmt} &) \mymetagoes \myapp{\myse{f'}}{\mycanquot(\myctx, \mytmt : \mytya)} : \mysub{\mytyb}{\myb{x}}{\mytmt} \\
3940 \multicolumn{2}{@{}l}{\myind{2}\text{\textbf{where}}\ \myse{f'} : \myfora{\myb{x}}{\mytya}{\mytyb} = \myneuquot(\myctx, \myse{f})} \\
3941 \myneuquot(\myctx,\ \mycoee{\mytya}{\mytyb}{\myse{Q}}{\mytmt} &) \mymetaguard \myneuquot(\myctx, \mytya) \mydefeq_{\mybox} \myneuquot(\myctx, \mytyb) \mymetagoes \myneuquot(\myctx, \mytmt) \\
3942 \myneuquot(\myctx,\ \mycoee{\mytya}{\mytyb}{\myse{Q}}{\mytmt} &) \mymetagoes
3943 \mycoee{\myneuquot(\myctx, \mytya)}{\myneuquot(\myctx, \mytyb)}{\boxed{\myse{Q}}}{\myneuquot(\myctx, \mytmt)}
3947 \caption{Quotation in \mykant. Along the already used
3948 $\mymeta{record}$ meta-operation on the context we make use of
3949 $\mymeta{empty}$, which checks if a certain type constructor has
3950 zero data constructor. The `data constructor' cases for non-record,
3951 non-empty, data types are omitted for brevity.}
3952 \label{fig:kant-quot}
3955 \subsubsection{Why $\myprop$?}
3957 It is worth to ask if $\myprop$ is needed at all. It is perfectly
3958 possible to have the type checker identify propositional types
3959 automatically, and in fact in some sense we already do during equality
3960 reduction and quotation. However, this has the considerable
3961 disadvantage that we can never identify abstracted
3962 variables\footnote{And in general neutral terms, although we currently
3963 don't have neutral propositions apart from equalities on neutral
3964 terms.} of type $\mytyp$ as $\myprop$, thus forbidding the user to
3965 talk about $\myprop$ explicitly.
3967 This is a considerable impediment, for example when implementing
3968 \emph{quotient types}. With quotients, we let the user specify an
3969 equivalence class over a certain type, and then exploit this in various
3970 way---crucially, we need to be sure that the equivalence given is
3971 propositional, a fact which prevented the use of quotients in dependent
3972 type theories \citep{Jacobs1994}.
3974 \section{\mykant : the practice}
3975 \label{sec:kant-practice}
3977 The codebase consists of around 2500 lines of Haskell,\footnote{The full
3978 source code is available under the GPL3 license at
3979 \url{https://github.com/bitonic/kant}. `Kant' was a previous
3980 incarnation of the software, and the name remained.} as reported by
3981 the \texttt{cloc} utility. The high level design is inspired by the
3982 work on various incarnations of Epigram, and specifically by the first
3983 version as described \citep{McBride2004}.
3985 The author learnt the hard way the implementation challenges for such a
3986 project, and ran out of time while implementing observational equality.
3987 While the constructs and typing rules are present, the machinery to make
3988 it happen (equality reduction, coercions, quotation, etc.) is not
3989 present yet. Everything else presented is implemented and working
3990 reasonably well, and given the detailed plan in the previous section,
3991 finishing off should not prove too much work.
3993 The interaction with the user takes place in a loop living in and
3994 updating a context of \mykant\ declarations, which presents itself as in
3995 Figure \ref{fig:kant-web}. Files with lists of declarations can also be
3996 loaded. The REPL is a available both as a commandline application and in
3997 a web interface, which is available at \url{bertus.mazzo.li}.
3999 A REPL cycle starts with the user inputing a \mykant\
4000 declaration or another REPL command, which then goes through various
4001 stages that can end up in a context update, or in failures of various
4002 kind. The process is described diagrammatically in figure
4003 \ref{fig:kant-process}.
4006 {\small\begin{Verbatim}[frame=leftline,xleftmargin=3cm]
4008 Version 0.0, made in London, year 2013.
4010 <decl> Declare value/data type/record
4013 :p <term> Pretty print
4015 :r <file> Reload file (erases previous environment)
4016 :i <name> Info about an identifier
4018 >>> :l data/samples/good/common.ka
4020 >>> :e plus three two
4021 suc (suc (suc (suc (suc zero))))
4022 >>> :t plus three two
4027 \caption{A sample run of the \mykant\ prompt.}
4028 \label{fig:kant-web}
4034 \item[Parse] In this phase the text input gets converted to a sugared
4035 version of the core language. For example, we accept multiple
4036 arguments in arrow types and abstractions, and we represent variables
4037 with names, while as we will see in Section \ref{sec:term-repr} the
4038 final term types uses a \emph{nameless} representation.
4040 \item[Desugar] The sugared declaration is converted to a core term.
4041 Most notably we go from names to nameless.
4043 \item[ConDestr] Short for `Constructors/Destructors', converts
4044 applications of data destructors and constructors to a special form,
4045 to perform bidirectional type checking.
4047 \item[Reference] Occurrences of $\mytyp$ get decorated by a unique reference,
4048 which is necessary to implement the type hierarchy check.
4050 \item[Elaborate] Converts the declaration to some context items, which
4051 might be a value declaration (type and body) or a data type
4052 declaration (constructors and destructors). This phase works in
4053 tandem with \textbf{Type checking}, which in turns needs to
4054 \textbf{Evaluate} terms.
4056 \item[Distill] and report the result. `Distilling' refers to the
4057 process of converting a core term back to a sugared version that the
4058 user can visualise. This can be necessary both to display errors
4059 including terms or to display result of evaluations or type checking
4060 that the user has requested. Among the other things in this stage we
4061 go from nameless back to names by recycling the names that the user
4062 used originally, as to fabricate a term which is as close as possible
4063 to what it originated from.
4065 \item[Pretty print] Format the terms in a nice way, and display the result to
4072 \tikzstyle{block} = [rectangle, draw, text width=5em, text centered, rounded
4073 corners, minimum height=2.5em, node distance=0.7cm]
4075 \tikzstyle{decision} = [diamond, draw, text width=4.5em, text badly
4076 centered, inner sep=0pt, node distance=0.7cm]
4078 \tikzstyle{line} = [draw, -latex']
4080 \tikzstyle{cloud} = [draw, ellipse, minimum height=2em, text width=5em, text
4081 centered, node distance=1.5cm]
4084 \begin{tikzpicture}[auto]
4085 \node [cloud] (user) {User};
4086 \node [block, below left=1cm and 0.1cm of user] (parse) {Parse};
4087 \node [block, below=of parse] (desugar) {Desugar};
4088 \node [block, below=of desugar] (condestr) {ConDestr};
4089 \node [block, below=of condestr] (reference) {Reference};
4090 \node [block, below=of reference] (elaborate) {Elaborate};
4091 \node [block, left=of elaborate] (tycheck) {Typecheck};
4092 \node [block, left=of tycheck] (evaluate) {Evaluate};
4093 \node [decision, right=of elaborate] (error) {Error?};
4094 \node [block, right=of parse] (pretty) {Pretty print};
4095 \node [block, below=of pretty] (distill) {Distill};
4096 \node [block, below=of distill] (update) {Update context};
4098 \path [line] (user) -- (parse);
4099 \path [line] (parse) -- (desugar);
4100 \path [line] (desugar) -- (condestr);
4101 \path [line] (condestr) -- (reference);
4102 \path [line] (reference) -- (elaborate);
4103 \path [line] (elaborate) edge[bend right] (tycheck);
4104 \path [line] (tycheck) edge[bend right] (elaborate);
4105 \path [line] (elaborate) -- (error);
4106 \path [line] (error) edge[out=0,in=0] node [near start] {yes} (distill);
4107 \path [line] (error) -- node [near start] {no} (update);
4108 \path [line] (update) -- (distill);
4109 \path [line] (pretty) -- (user);
4110 \path [line] (distill) -- (pretty);
4111 \path [line] (tycheck) edge[bend right] (evaluate);
4112 \path [line] (evaluate) edge[bend right] (tycheck);
4115 \caption{High level overview of the life of a \mykant\ prompt cycle.}
4116 \label{fig:kant-process}
4119 Here we will review only a sampling of the more interesting
4120 implementation challenges present when implementing an interactive
4125 The syntax of \mykant\ is presented in Figure \ref{fig:syntax}.
4126 Examples showing the usage of most of the constructs are present in
4127 Appendices \ref{app:kant-itt}, \ref{app:kant-examples}, and
4128 \ref{app:hurkens}; plus a tutorial in Section \ref{sec:type-holes}. The
4129 syntax has grown organically with the needs of the language, and thus it
4130 is not very sophisticated, being specified in and processed by a parser
4131 generated with the \texttt{happy} parser generated for Haskell.
4132 Tokenisation is performed by a simple hand written lexer.
4137 \begin{array}{@{\ \ }l@{\ }c@{\ }l}
4138 \multicolumn{3}{@{}l}{\text{A name, in regexp notation.}} \\
4139 \mysee{name} & ::= & \texttt{[a-zA-Z] [a-zA-Z0-9'\_-]*} \\
4140 \multicolumn{3}{@{}l}{\text{A binder might or might not (\texttt{\_}) bind a name.}} \\
4141 \mysee{binder} & ::= & \mytermi{\_} \mysynsep \mysee{name} \\
4142 \multicolumn{3}{@{}l}{\text{A series of typed bindings.}} \\
4143 \mysee{telescope}\, \ \ \ & ::= & (\mytermi{[}\ \mysee{binder}\ \mytermi{:}\ \mysee{term}\ \mytermi{]}){*} \\
4144 \multicolumn{3}{@{}l}{\text{Terms, including propositions.}} \\
4145 \multicolumn{3}{@{}l}{
4146 \begin{array}{@{\ \ }l@{\ }c@{\ }l@{\ \ \ \ \ }l}
4147 \mysee{term} & ::= & \mysee{name} & \text{A variable.} \\
4148 & | & \mytermi{*} & \text{\mytyc{Type}.} \\
4149 & | & \mytermi{\{|}\ \mysee{term}{*}\ \mytermi{|\}} & \text{Type holes.} \\
4150 & | & \mytermi{Prop} & \text{\mytyc{Prop}.} \\
4151 & | & \mytermi{Top} \mysynsep \mytermi{Bot} & \text{$\mytop$ and $\mybot$.} \\
4152 & | & \mysee{term}\ \mytermi{/\textbackslash}\ \mysee{term} & \text{Conjuctions.} \\
4153 & | & \mytermi{[|}\ \mysee{term}\ \mytermi{|]} & \text{Proposition decoding.} \\
4154 & | & \mytermi{coe}\ \mysee{term}\ \mysee{term}\ \mysee{term}\ \mysee{term} & \text{Coercion.} \\
4155 & | & \mytermi{coh}\ \mysee{term}\ \mysee{term}\ \mysee{term}\ \mysee{term} & \text{Coherence.} \\
4156 & | & \mytermi{(}\ \mysee{term}\ \mytermi{:}\ \mysee{term}\ \mytermi{)}\ \mytermi{=}\ \mytermi{(}\ \mysee{term}\ \mytermi{:}\ \mysee{term}\ \mytermi{)} & \text{Heterogeneous equality.} \\
4157 & | & \mytermi{(}\ \mysee{compound}\ \mytermi{)} & \text{Parenthesised term.} \\
4158 \mysee{compound} & ::= & \mytermi{\textbackslash}\ \mysee{binder}{*}\ \mytermi{=>}\ \mysee{term} & \text{Untyped abstraction.} \\
4159 & | & \mytermi{\textbackslash}\ \mysee{telescope}\ \mytermi{:}\ \mysee{term}\ \mytermi{=>}\ \mysee{term} & \text{Typed abstraction.} \\
4160 & | & \mytermi{forall}\ \mysee{telescope}\ \mysee{term} & \text{Universal quantification.} \\
4161 & | & \mysee{arr} \\
4162 \mysee{arr} & ::= & \mysee{telescope}\ \mytermi{->}\ \mysee{arr} & \text{Dependent function.} \\
4163 & | & \mysee{term}\ \mytermi{->}\ \mysee{arr} & \text{Non-dependent function.} \\
4164 & | & \mysee{term}{+} & \text {Application.}
4167 \multicolumn{3}{@{}l}{\text{Typed names.}} \\
4168 \mysee{typed} & ::= & \mysee{name}\ \mytermi{:}\ \mysee{term} \\
4169 \multicolumn{3}{@{}l}{\text{Declarations.}} \\
4170 \mysee{decl}& ::= & \mysee{value} \mysynsep \mysee{abstract} \mysynsep \mysee{data} \mysynsep \mysee{record} \\
4171 \multicolumn{3}{@{}l}{\text{Defined values. The telescope specifies named arguments.}} \\
4172 \mysee{value} & ::= & \mysee{name}\ \mysee{telescope}\ \mytermi{:}\ \mysee{term}\ \mytermi{=>}\ \mysee{term} \\
4173 \multicolumn{3}{@{}l}{\text{Abstracted variables.}} \\
4174 \mysee{abstract} & ::= & \mytermi{postulate}\ \mysee{typed} \\
4175 \multicolumn{3}{@{}l}{\text{Data types, and their constructors.}} \\
4176 \mysee{data} & ::= & \mytermi{data}\ \mysee{name}\ \mysee{telescope}\ \mytermi{->}\ \mytermi{*}\ \mytermi{=>}\ \mytermi{\{}\ \mysee{constrs}\ \mytermi{\}} \\
4177 \mysee{constrs} & ::= & \mysee{typed} \\
4178 & | & \mysee{typed}\ \mytermi{|}\ \mysee{constrs} \\
4179 \multicolumn{3}{@{}l}{\text{Records, and their projections. The $\mysee{name}$ before the projections is the constructor name.}} \\
4180 \mysee{record} & ::= & \mytermi{record}\ \mysee{name}\ \mysee{telescope}\ \mytermi{->}\ \mytermi{*}\ \mytermi{=>}\ \mysee{name}\ \mytermi{\{}\ \mysee{projs}\ \mytermi{\}} \\
4181 \mysee{projs} & ::= & \mysee{typed} \\
4182 & | & \mysee{typed}\ \mytermi{,}\ \mysee{projs}
4186 \caption{\mykant' syntax. The non-terminals are marked with
4187 $\langle\text{angle brackets}\rangle$ for greater clarity. The
4188 syntax in the implementation is actually more liberal, for example
4189 giving the possibility of using arrow types directly in
4190 constructor/projection declarations.\\
4191 Additionally, we give the user the possibility of using Unicode
4192 characters instead of their ASCII counterparts, e.g. \texttt{→} in
4193 place of \texttt{->}, \texttt{λ} in place of
4194 \texttt{\textbackslash}, etc.}
4198 \subsection{Term representation}
4199 \label{sec:term-repr}
4201 \subsubsection{Naming and substituting}
4203 Perhaps surprisingly, one of the most difficult challenges in
4204 implementing a theory of the kind presented is choosing a good data type
4205 for terms, and specifically handling substitutions in a sane way.
4207 There are two broad schools of thought when it comes to naming
4208 variables, and thus substituting:
4210 \item[Nameful] Bound variables are represented by some enumerable data
4211 type, just as we have described up to now, starting from Section
4212 \ref{sec:untyped}. The problem is that avoiding name capturing is a
4213 nightmare, both in the sense that it is not performant---given that we
4214 need to rename rename substitute each time we `enter' a binder---but
4215 most importantly given the fact that in even more slightly complicated
4216 systems it is very hard to get right, even for experts.
4218 One of the sore spots of explicit names is comparing terms up
4219 $\alpha$-renaming, which again generates a huge amounts of
4220 substitutions and requires special care. We can represent the
4221 relationship between variables and their binders, by...
4223 \item[Nameless] ...getting rid of names altogether, and representing
4224 bound variables with an index referring to the `binding' structure, a
4225 notion introduced by \cite{de1972lambda}. Classically $0$ represents
4226 the variable bound by the innermost binding structure, $1$ the
4227 second-innermost, and so on. For instance with simple abstractions we
4231 \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} \\
4232 \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
4236 While this technique is obviously terrible in terms of human
4237 usability,\footnote{With some people going as far as defining it akin
4238 to an inverse Turing test.} it is much more convenient as an
4239 internal representation to deal with terms mechanically---at least in
4240 simple cases. Moreover, $\alpha$ renaming ceases to be an issue, and
4241 term comparison is purely syntactical.
4243 Nonetheless, more complex, constructs such as pattern matching put
4244 some strain on the indices and many systems end up using explicit
4245 names anyway (Agda, Coq, \dots).
4249 In the past decade or so advancements in the Haskell's type system and
4250 in general the spread new programming practices have enabled to make the
4251 second option much more amenable. \mykant\ thus takes the second path
4252 through the use of Edward Kmett's excellent \texttt{bound}
4253 library.\footnote{Available at
4254 \url{http://hackage.haskell.org/package/bound}.} We decribe its
4255 advantages but also pitfalls in the previously relatively unknown
4256 territory of dependent types---\texttt{bound} being created mostly to
4257 handle more simply typed systems.
4259 \texttt{bound} builds on the work of \cite{Bird1999}, who suggest to
4260 parametrising the term type over the type of the variables, and `nest'
4261 the type each time we enter a scope. If we wanted to define a term for
4262 the untyped $\lambda$-calculus, we might have
4264 -- A type with no members.
4267 data Var v = Bound | Free v
4270 = V v -- Bound variable
4271 | App (Tm v) (Tm v) -- Term application
4272 | Lam (Tm (Var v)) -- Abstraction
4274 Closed terms would be of type \texttt{Tm Empty}, so that there would be
4275 no occurrences of \texttt{V}. However, inside an abstraction, we can
4276 have \texttt{V Bound}, representing the bound variable, and inside a
4277 second abstraction we can have \texttt{V Bound} or \texttt{V (Free
4278 Bound)}. Thus the term
4279 \[\myabs{\myb{x}}{\myabs{\myb{y}}{\myb{x}}}\]
4280 can be represented as
4282 -- The top level term is of type `Tm Empty'.
4283 -- The inner term `Lam (Free Bound)' is of type `Tm (Var Empty)'.
4284 -- The second inner term `V (Free Bound)' is of type `Tm (Var (Var
4286 Lam (Lam (V (Free Bound)))
4288 This allows us to reflect the of a type `nestedness' at the type level,
4289 and since we usually work with functions polymorphic on the parameter
4290 \texttt{v} it's very hard to make mistakes by putting terms of the wrong
4291 nestedness where they don't belong.
4293 Even more interestingly, the substitution operation is perfectly
4294 captured by the \verb|>>=| (bind) operator of the \texttt{Monad}
4299 (>>=) :: m a -> (a -> m b) -> m b
4301 instance Monad Tm where
4302 -- `return'ing turns a variable into a `Tm'
4305 -- `t >>= f' takes a term `t' and a mapping from variables to terms
4306 -- `f' and applies `f' to all the variables in `t', replacing them
4307 -- with the mapped terms.
4309 App m n >>= f = App (m >>= f) (n >>= f)
4311 -- `Lam' is the tricky case: we modify the function to work with bound
4312 -- variables, so that if it encounters `Bound' it leaves it untouched
4313 -- (since the mapping refers to the outer scope); if it encounters a
4314 -- free variable it asks `f' for the term and then updates all the
4315 -- variables to make them refer to the outer scope they were meant to
4317 Lam s >>= f = Lam (s >>= bump)
4318 where bump Bound = return Bound
4319 bump (Free v) = f v >>= V . Free
4321 With this in mind, we can define functions which will not only work on
4322 \verb|Tm|, but on any \verb|Monad|!
4324 -- Replaces free variable `v' with `m' in `n'.
4325 subst :: (Eq v, Monad m) => v -> m v -> m v -> m v
4326 subst v m n = n >>= \v' -> if v == v' then m else return v'
4328 -- Replace the variable bound by `s' with term `t'.
4329 inst :: Monad m => m v -> m (Var v) -> m v
4330 inst t s = do v <- s
4333 Free v' -> return v'
4335 The beauty of this technique is that in a few simple function we have
4336 defined all the core operations in a general and `obviously correct'
4337 way, with the extra confidence of having the type checker looking our
4338 back. For what concerns term equality, we can just ask the Haskell
4339 compiler to derive the instance for the \verb|Eq| type class and since
4340 we are nameless that will be enough (modulo fancy quotation).
4342 Moreover, if we take the top level term type to be \verb|Tm String|, we
4343 get for free a representation of terms with top-level, definitions;
4344 where closed terms contain only \verb|String| references to said
4345 definitions---see also \cite{McBride2004b}.
4347 What are then the pitfalls of this seemingly invincible technique? The
4348 most obvious impediment is the need for polymorphic recursion.
4349 Functions traversing terms parametrised by the variable type will have
4352 -- Infer the type of a term, or return an error.
4353 infer :: Tm v -> Either Error (Tm v)
4355 When traversing under a \verb|Scope| the parameter changes from \verb|v|
4356 to \verb|Var v|, and thus if we do not specify the type for our function explicitly
4357 inference will fail---type inference for polymorphic recursion being
4358 undecidable \citep{henglein1993type}. This causes some annoyance,
4359 especially in the presence of many local definitions that we would like
4362 But the real issue is the fact that giving a type parametrised over a
4363 variable---say \verb|m v|---a \verb|Monad| instance means being able to
4364 only substitute variables for values of type \verb|m v|. This is a
4365 considerable inconvenience. Consider for instance the case of
4366 telescopes, which are a central tool to deal with contexts and other
4367 constructs. In Haskell we can give them a faithful representation
4368 with a data type along the lines of
4370 data Tele m v = End (m v) | Bind (m v) (Tele (Var v))
4371 type TeleTm = Tele Tm
4373 The problem here is that what we want to substitute for variables in
4374 \verb|Tele m v| is \verb|m v| (probably \verb|Tm v|), not \verb|Tele m v| itself! What we need is
4376 bindTele :: Monad m => Tele m a -> (a -> m b) -> Tele m b
4377 substTele :: (Eq v, Monad m) => v -> m v -> Tele m v -> Tele m v
4378 instTele :: Monad m => m v -> Tele m (Var v) -> Tele m v
4380 Not what \verb|Monad| gives us. Solving this issue in an elegant way
4381 has been a major sink of time and source of headaches for the author,
4382 who analysed some of the alternatives---most notably the work by
4383 \cite{weirich2011binders}---but found it impossible to give up the
4384 simplicity of the model above.
4386 That said, our term type is still reasonably brief, as shown in full in
4387 Appendix \ref{app:termrep}. The fact that propositions cannot be
4388 factored out in another data type is an instance of the problem
4389 described above. However the real pain is during elaboration, where we
4390 are forced to treat everything as a type while we would much rather have
4391 telescopes. Future work would include writing a library that marries a
4392 nice interface similar to the one of \verb|bound| with a more flexible
4395 We also make use of a `forgetful' data type (as provided by
4396 \verb|bound|) to store user-provided variables names along with the
4397 `nameless' representation, so that the names will not be considered when
4398 compared terms, but will be available when distilling so that we can
4399 recover variable names that are as close as possible to what the user
4402 \subsubsection{Evaluation}
4404 Another source of contention related to term representation is dealing
4405 with evaluation. Here \mykant\ does not make bold moves, and simply
4406 employs substitution. When type checking we match types by reducing
4407 them to their wheak head normal form, as to avoid unnecessary evaluation.
4409 We treat data types eliminators and record projections in an uniform
4410 way, by elaborating declarations in a series of \emph{rewriting rules}:
4414 TmRef v -> -- Term to which the destructor is applied
4415 [TmRef v] -> -- List of other arguments
4416 -- The result of the rewriting, if the eliminator reduces.
4419 A rewriting rule is polymorphic in the variable type, guaranteeing that
4420 it just pattern matches on terms structure and rearranges them in some
4421 way, and making it possible to apply it at any level in the term. When
4422 reducing a series of applications we match the first term and check if
4423 it is a destructor, and if that's the case we apply the reduction rule
4424 and reduce further if it yields a new list of terms.
4426 This has the advantage of being very simple, but has the disadvantage of
4427 being quite poor in terms of performance and that we need to do
4428 quotation manually. An alternative that solves both of these is the
4429 already mentioned \emph{normalization by evaluation}, where we would
4430 compute by turning terms into Haskell values, and then reify back to
4431 terms to compare them---a useful tutorial on this technique is given by
4434 \subsection{Turning constraints into graphs}
4435 \label{sec:hier-impl}
4437 In this section we will explain how to implement the typical ambiguity
4438 we have spoken about in \ref{sec:term-hierarchy} efficiently, a subject
4439 which is often dismissed in the literature. As mentioned, we have to
4440 verify a the consistency of a set of constraints each time we add a new
4441 one. The constraints range over some set of variables whose members we
4442 will denote with $x, y, z, \dots$. and are of two kinds:
4449 Predictably, $\le$ expresses a reflexive order, and $<$ expresses an
4450 irreflexive order, both working with the same notion of equality, where
4451 $x < y$ implies $x \le y$---they behave like $\le$ and $<$ do for natural
4452 numbers (or in our case, levels in a type hierarchy). We also need an
4453 equality constraint ($x = y$), which can be reduced to two constraints
4454 $x \le y$ and $y \le x$.
4456 Given this specification, we have implemented a standalone Haskell
4457 module---that we plan to release as a standalone library---to
4458 efficiently store and check the consistency of constraints. The problem
4459 predictably reduces to a graph algorithm, and for this reason we also
4460 implement a library for labelled graphs, since the existing Haskell
4461 graph libraries fell short in different areas.\footnote{We tried the
4462 \texttt{Data.Graph} module in
4463 \url{http://hackage.haskell.org/package/containers}, and the much more
4464 featureful \texttt{fgl} library
4465 \url{http://hackage.haskell.org/package/fgl}.}. The interfaces for
4466 these modules are shown in Appendix \ref{app:constraint}. The graph
4467 library is implemented as a modification of the code described by
4470 We represent the set by building a graph where vertices are variables,
4471 and edges are constraints between them, labelled with the appropriate
4472 constraint: $x < y$ gives rise to a $<$-labelled edge from $x$ to $y$<
4473 and $x \le y$ to a $\le$-labelled edge from $x$ to $y$. As we add
4474 constraints, $\le$ constraints are replaced by $<$ constraints, so that
4475 if we started with an empty set and added
4477 x < y,\ y \le z,\ z \le k,\ k < j,\ j \le y\
4479 it would generate the graph shown in Figure \ref{fig:graph-one-before},
4480 but adding $z < k$ would strengthen the edge from $z$ to $k$, as shown
4481 in \ref{fig:graph-one-after}.
4485 \begin{subfigure}[b]{0.3\textwidth}
4486 \begin{tikzpicture}[node distance=1.5cm]
4489 \node [right of=x] (y) {$y$};
4490 \node [right of=y] (z) {$z$};
4491 \node [below of=z] (k) {$k$};
4492 \node [left of=k] (j) {$j$};
4495 (x) edge node [above] {$<$} (y)
4496 (y) edge node [above] {$\le$} (z)
4497 (z) edge node [right] {$\le$} (k)
4498 (k) edge node [below] {$\le$} (j)
4499 (j) edge node [left ] {$\le$} (y);
4501 \caption{Before $z < k$.}
4502 \label{fig:graph-one-before}
4505 \begin{subfigure}[b]{0.3\textwidth}
4506 \begin{tikzpicture}[node distance=1.5cm]
4509 \node [right of=x] (y) {$y$};
4510 \node [right of=y] (z) {$z$};
4511 \node [below of=z] (k) {$k$};
4512 \node [left of=k] (j) {$j$};
4515 (x) edge node [above] {$<$} (y)
4516 (y) edge node [above] {$\le$} (z)
4517 (z) edge node [right] {$<$} (k)
4518 (k) edge node [below] {$\le$} (j)
4519 (j) edge node [left ] {$\le$} (y);
4521 \caption{After $z < k$.}
4522 \label{fig:graph-one-after}
4525 \begin{subfigure}[b]{0.3\textwidth}
4526 \begin{tikzpicture}[remember picture, node distance=1.5cm]
4527 \begin{pgfonlayer}{foreground}
4530 \node [right of=x] (y) {$y$};
4531 \node [right of=y] (z) {$z$};
4532 \node [below of=z] (k) {$k$};
4533 \node [left of=k] (j) {$j$};
4536 (x) edge node [above] {$<$} (y)
4537 (y) edge node [above] {$\le$} (z)
4538 (z) edge node [right] {$<$} (k)
4539 (k) edge node [below] {$\le$} (j)
4540 (j) edge node [left ] {$\le$} (y);
4541 \end{pgfonlayer}{foreground}
4543 \begin{tikzpicture}[remember picture, overlay]
4544 \begin{pgfonlayer}{background}
4545 \fill [red, opacity=0.3, rounded corners]
4546 (-2.7,2.6) rectangle (-0.2,0.05)
4547 (-4.1,2.4) rectangle (-3.3,1.6);
4548 \end{pgfonlayer}{background}
4551 \label{fig:graph-one-scc}
4553 \caption{Strong constraints overrule weak constraints.}
4554 \label{fig:graph-one}
4557 Each time we add a new constraint, we check if any strongly connected
4558 component (SCC) arises, a SCC being a subset $V$ of vertices where for
4559 each $v_1,v_2 \in V$ there is a path from $v_1$ to $v_2$. The SCCs in
4560 the graph for the constraints above is shown in Figure
4561 \ref{fig:graph-one-scc}. If we have a strongly connected component with
4562 a $<$ edge---say $x < y$---in it, we have an inconsistency, since there
4563 must also be a path from $y$ to $x$, and by transitivity it must either
4564 be the case that $y \le x$ or $y < x$, which are both at odds with $x <
4567 Moreover, if we have a SCC with no $<$ edges, it means that all members
4568 of said SCC are equal, since for every $x \le y$ we have a path from $y$
4569 to $x$, which again by transitivity means that $y \le x$. Thus, we can
4570 \emph{condense} the SCC to a single vertex, by choosing a variable among
4571 the SCC as a representative for all the others. This can be done
4572 efficiently with disjoint set data structure.
4574 \subsection{Tooling}
4576 \subsubsection{A type holes tutorial}
4577 \label{sec:type-holes}
4579 Type holes are, in the author's opinion, one of the `killer' features of
4580 interactive theorem provers, and one that is begging to be exported to
4581 the word of mainstream programming. The idea is that when we are
4582 developing a proof or a program we can insert a hole to have the
4583 software tell us the type expected at that point. Furthermore, we can
4584 ask for the type of variables in context, to better understand our
4585 surroundings. Here we give a short tutorial in \mykant\ of this tool to
4586 give an idea of its usefulness.
4588 Suppose we wanted to define the `less or equal' ordering on natural
4589 numbers as described in Section \ref{sec:user-type}. We will
4590 incrementally build our functions in a file called \texttt{le.ka}.
4591 First we define the necessary types, all of which we know well by now:
4593 data Nat : ⋆ ⇒ { zero : Nat | suc : Nat → Nat }
4595 data Empty : ⋆ ⇒ { }
4596 absurd [A : ⋆] [p : Empty] : A ⇒ (
4597 Empty-Elim p (λ _ ⇒ A)
4600 record Unit : ⋆ ⇒ tt { }
4602 Then fire up \mykant, and load the file:
4603 \begin{Verbatim}[frame=leftline]
4606 Version 0.0, made in London, year 2013.
4610 So far so good. Our definition will be defined by recursion on a
4611 natural number \texttt{n}, which will return a function that given
4612 another number \texttt{m} will return the trivial type \texttt{Unit} if
4613 $\texttt{n} \le \texttt{m}$, and the \texttt{Empty} type otherwise.
4614 However we are still not sure on how to define it, so we invoke
4615 $\texttt{Nat-Elim}$, the eliminator for natural numbers, and place holes
4616 instead of arguments. In the file we will write:
4618 le [n : Nat] : Nat → ⋆ ⇒ (
4619 Nat-Elim n (λ _ ⇒ Nat → ⋆)
4624 And then we reload in \mykant:
4625 \begin{Verbatim}[frame=leftline]
4629 h2 : Nat → (Nat → ⋆) → Nat → ⋆
4631 Which tells us what types we need to satisfy in each hole. However, it
4632 is not that clear what does what in each hole, and thus it is useful to
4633 have a definition vacuous in its arguments just to clear things up. We
4634 will use \texttt{Le} aid in reading the goal, with \texttt{Le m n} as a
4635 reminder that we to return the type corresponding to $\texttt{m} ≤
4638 Le [m n : Nat] : ⋆ ⇒ ⋆
4640 le [n : Nat] : [m : Nat] → Le n m ⇒ (
4641 Nat-Elim n (λ n ⇒ [m : Nat] → Le n m)
4646 \begin{Verbatim}[frame=leftline]
4649 h1 : [m : Nat] → Le zero m
4650 h2 : [x : Nat] → ([m : Nat] → Le x m) → [m : Nat] → Le (suc x) m
4652 This is much better! \mykant, when printing terms, does not substitute
4653 top-level names for their bodies, since usually the resulting term is
4654 much clearer. As a nice side-effect, we can use tricks like this to
4657 In this case in the first case we need to return, given any number
4658 \texttt{m}, $0 \le \texttt{m}$. The trivial type will do, since every
4659 number is less or equal than zero:
4661 le [n : Nat] : [m : Nat] → Le n m ⇒ (
4662 Nat-Elim n (λ n ⇒ [m : Nat] → Le n m)
4667 \begin{Verbatim}[frame=leftline]
4670 h2 : [x : Nat] → ([m : Nat] → Le x m) → [m : Nat] → Le (suc x) m
4672 Now for the important case. We are given our comparison function for a
4673 number, and we need to produce the function for the successor. Thus, we
4674 need to re-apply the induction principle on the other number, \texttt{m}:
4676 le [n : Nat] : [m : Nat] → Le n m ⇒ (
4677 Nat-Elim n (λ n ⇒ [m : Nat] → Le n m)
4679 (λ n' f m ⇒ Nat-Elim m (λ m' ⇒ Le (suc n') m') {|h2|} {|h3|})
4682 \begin{Verbatim}[frame=leftline]
4686 h3 : [x : Nat] → Le (suc n') x → Le (suc n') (suc x)
4688 In the first hole we know that the second number is zero, and thus we
4689 can return empty. In the second case, we can use the recursive argument
4690 \texttt{f} on the two numbers:
4692 le [n : Nat] : [m : Nat] → Le n m ⇒ (
4693 Nat-Elim n (λ n ⇒ [m : Nat] → Le n m)
4696 Nat-Elim m (λ m' ⇒ Le (suc n') m') Empty (λ f _ ⇒ f m'))
4699 We can verify that our function works as expected:
4700 \begin{Verbatim}[frame=leftline]
4703 >>> :e le zero (suc zero)
4705 >>> :e le (suc (suc zero)) (suc zero)
4708 Another functionality of type holes is examining types of things in
4709 context. Going back to the examples in Section \ref{sec:term-types}, we can
4710 implement the safe \texttt{head} function with our newly defined
4713 data List : [A : ⋆] → ⋆ ⇒
4714 { nil : List A | cons : A → List A → List A }
4716 length [A : ⋆] [l : List A] : Nat ⇒ (
4717 List-Elim l (λ _ ⇒ Nat) zero (λ _ _ n ⇒ suc n)
4720 gt [n m : Nat] : ⋆ ⇒ (le (suc m) n)
4722 head [A : ⋆] [l : List A] : gt (length A l) zero → A ⇒ (
4723 List-Elim l (λ l ⇒ gt (length A l) zero → A)
4728 We define \texttt{List}s, a polymorphic \texttt{length} function, and
4729 express $<$ (\texttt{gt}) in terms of $\le$. Then, we set up the type
4730 for our \texttt{head} function. Given a list and a proof that its
4731 length is greater than zero, we return the first element. If we load
4732 this in \mykant, we get:
4733 \begin{Verbatim}[frame=leftline]
4738 h2 : [x : A] [x1 : List A] →
4739 (gt (length A x1) zero → A) →
4740 gt (length A (cons x x1)) zero → A
4742 In the first case (the one for \texttt{nil}), we have a proof of
4743 \texttt{Empty}---surely we can use \texttt{absurd} to get rid of that
4744 case. In the second case we simply return the element in the
4747 head [A : ⋆] [l : List A] : gt (length A l) zero → A ⇒ (
4748 List-Elim l (λ l ⇒ gt (length A l) zero → A)
4754 This should give a vague idea of why type holes are so useful and in
4755 more in general about the development process in \mykant. Most
4756 interactive theorem provers offer some kind of facility
4757 to... interactively develop proofs, usually much more powerful than the
4758 fairly bare tools present in \mykant. Agda in particular offers a
4759 particularly powerful mode for the \texttt{Emacs} text editor.
4761 \subsubsection{Web REPL}
4763 \section{Evaluation}
4764 \label{sec:evaluation}
4766 \section{Future work}
4767 \label{sec:future-work}
4769 As mentioned, the first move that the author plans to make is to work
4770 towards a simple but powerful term representation, and then adjust
4771 \mykant\ to this new representation. A good plan seems to be to
4772 associate each type (terms, telescopes, etc.) with what we can
4773 substitute variables with, so that the term type will be associated with
4774 itself, while telescopes and propositions will be associated to terms.
4775 This can probably be accomplished elegantly with Haskell's \emph{type
4776 families} \citep{chakravarty2005associated}. After achieving a more
4777 solid machinery for terms, implementing observational equality fully
4778 should prove relatively easy.
4780 Beyond this steps, \mykant\ would still need many additions to compete
4781 as a reasonable alternative to the existing systems:
4784 \item[Pattern matching] Eliminators are very clumsy to use, and
4786 \item[More powerful data types] A popular improvement on basic data
4787 types are inductive families \cite{Dybjer1991}, where the parameters
4788 for the type constructors can change based on the data constructors,
4789 which lets us express naturally types such as $\mytyc{Vec} : \mynat
4790 \myarr \mytyp$, which given a number returns the type of lists of that
4791 length, or $\mytyc{Fin} : \mynat \myarr \mytyp$, which given a number
4792 $n$ gives the type of numbers less than $n$. This apparent omission
4793 was motivated by the fact that inductive families can be represented
4794 by adding equalities concerning the parameters of the type
4795 constructors as arguments to the data constructor, in much the same
4796 way that Generalised Abstract Data Types \citep{GHC} are handled in
4797 Haskell, where interestingly the modified version of System F that
4798 lies at the core of recent versions of GHC features coercions similar
4799 to those found in OTT \citep{Sulzmann2007}.
4801 The notion of inductive family also yields a more interesting notion
4802 of pattern matching, since matching on an argument influences the
4803 value of the parameters of the type of said argument. This means that
4804 pattern matching influences the context, which can be exploited to
4805 constraint the possible constructors in \emph{other} arguments
4808 Another popular extension introduced by \cite{dybjer2000general} is
4809 induction-recursion, where we define a data type in tandem with a
4810 function on that type. This technique has proven extremely useful to
4811 define embeddings of other calculi in an host language, by defining
4812 the representation of the embedded language as a data type and at the
4813 same time a function decoding from the representation to a type in the
4816 It is also worth mentionning that in recent times there has been work
4817 by \cite{dagand2012elaborating, chapman2010gentle} to show how to
4818 define a set of primitives that data types can be elaborated into,
4819 with the additional advantage of having the possibility of having a
4820 very powerful notion of generic programming by writing functions
4821 working on the `primitive' types as to be workable by all `compatible'
4822 user-defined data types. This has been a considerable problem in the
4823 dependently type world, where we often define types which are more
4824 `strongly typed' version of similar structures,\footnote{For example
4825 the $\mytyc{OList}$ presented in Section \ref{sec:user-type} being a
4826 `more typed' version of an ordinary list.} and then find ourselves
4827 forced to redefine identical operations on both types.
4829 \item[Type inference] While bidirectional type checking helps, for a
4830 syts \cite{miller1992unification} \cite{gundrytutorial}
4831 \cite{huet1973undecidability}.
4833 \item[Coinduction] \cite{cockett1992charity} \cite{mcbride2009let}.
4836 % TODO coinduction (obscoin, gimenez, jacobs), pattern unification (miller,
4837 % gundry), partiality monad (NAD)
4841 \section{Notation and syntax}
4843 Syntax, derivation rules, and reduction rules, are enclosed in frames describing
4844 the type of relation being established and the syntactic elements appearing,
4847 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
4848 Typing derivations here.
4851 In the languages presented and Agda code samples I also highlight the syntax,
4852 following a uniform color and font convention:
4855 \begin{tabular}{c | l}
4856 $\mytyc{Sans}$ & Type constructors. \\
4857 $\mydc{sans}$ & Data constructors. \\
4858 % $\myfld{sans}$ & Field accessors (e.g. \myfld{fst} and \myfld{snd} for products). \\
4859 $\mysyn{roman}$ & Keywords of the language. \\
4860 $\myfun{roman}$ & Defined values and destructors. \\
4861 $\myb{math}$ & Bound variables.
4865 When presenting grammars, I will use a word in $\mysynel{math}$ font
4866 (e.g. $\mytmsyn$ or $\mytysyn$) to indicate indicate
4867 nonterminals. Additionally, I will use quite flexibly a $\mysynel{math}$
4868 font to indicate a syntactic element in derivations or meta-operations.
4869 More specifically, terms are usually indicated by lowercase letters
4870 (often $\mytmt$, $\mytmm$, or $\mytmn$); and types by an uppercase
4871 letter (often $\mytya$, $\mytyb$, or $\mytycc$).
4873 When presenting type derivations, I will often abbreviate and present multiple
4874 conclusions, each on a separate line:
4876 \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
4877 \UnaryInfC{$\myjud{\myapp{\myfst}{\mytmt}}{\mytya}$}
4879 \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mytyb}$}
4882 I will often present `definitions' in the described calculi and in
4883 $\mykant$\ itself, like so:
4886 \myfun{name} : \mytysyn \\
4887 \myfun{name} \myappsp \myb{arg_1} \myappsp \myb{arg_2} \myappsp \cdots \mapsto \mytmsyn
4890 To define operators, I use a mixfix notation similar
4891 to Agda, where $\myarg$s denote arguments:
4894 \myarg \mathrel{\myfun{$\wedge$}} \myarg : \mybool \myarr \mybool \myarr \mybool \\
4895 \myb{b_1} \mathrel{\myfun{$\wedge$}} \myb{b_2} \mapsto \cdots
4899 In explicitly typed systems, I will also omit type annotations when they
4900 are obvious, e.g. by not annotating the type of parameters of
4901 abstractions or of dependent pairs.
4903 I will introduce multiple arguments in one go in arrow types:
4905 (\myb{x}\, \myb{y} {:} \mytya) \myarr \cdots = (\myb{x} {:} \mytya) \myarr (\myb{y} {:} \mytya) \myarr \cdots
4907 and in abstractions:
4909 \myabs{\myb{x}\myappsp\myb{y}}{\cdots} = \myabs{\myb{x}}{\myabs{\myb{y}}{\cdots}}
4911 I will also omit arrows to abbreviate types:
4913 (\myb{x} {:} \mytya)(\myb{y} {:} \mytyb) \myarr \cdots =
4914 (\myb{x} {:} \mytya) \myarr (\myb{y} {:} \mytyb) \myarr \cdots
4916 Meta operations names will be displayed in $\mymeta{smallcaps}$ and
4917 written in a pattern matching style, also making use of boolean guards.
4918 For example, a meta operation operating on a context and terms might
4922 \mymeta{quux}(\myctx, \myb{x}) \mymetaguard \myb{x} \in \myctx \mymetagoes \myctx(\myb{x}) \\
4923 \mymeta{quux}(\myctx, \myb{x}) \mymetagoes \mymeta{outofbounds} \\
4928 I will from time to time give examples in the Haskell programming
4929 language as defined in \citep{Haskell2010}, which I will typeset in
4930 \texttt{teletype} font. I assume that the reader is already familiar
4931 with Haskell, plenty of good introductions are available
4932 \citep{LYAH,ProgInHask}.
4934 Examples of \mykant\ code will be typeset nicely with \LaTeX in Section
4935 \ref{sec:kant-theory}, to adjust with the rest of the presentation; and
4936 in \texttt{teletype} font in the rest of the document, including Section
4937 \ref{sec:kant-practice} and in the appendices. Snippets of sessions in
4938 the \mykant\ prompt will be displayed with a left border, to distinguish
4939 them from snippets of code:
4940 \begin{Verbatim}[frame=leftline]
4947 \subsection{ITT renditions}
4948 \label{app:itt-code}
4950 \subsubsection{Agda}
4951 \label{app:agda-itt}
4953 Note that in what follows rules for `base' types are
4954 universe-polymorphic, to reflect the exposition. Derived definitions,
4955 on the other hand, mostly work with \mytyc{Set}, reflecting the fact
4956 that in the theory presented we don't have universe polymorphism.
4962 data Empty : Set where
4964 absurd : ∀ {a} {A : Set a} → Empty → A
4967 ¬_ : ∀ {a} → (A : Set a) → Set a
4970 record Unit : Set where
4973 record _×_ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
4980 data Bool : Set where
4983 if_/_then_else_ : ∀ {a} (x : Bool) (P : Bool → Set a) → P true → P false → P x
4984 if true / _ then x else _ = x
4985 if false / _ then _ else x = x
4987 if_then_else_ : ∀ {a} (x : Bool) {P : Bool → Set a} → P true → P false → P x
4988 if_then_else_ x {P} = if_/_then_else_ x P
4990 data W {s p} (S : Set s) (P : S → Set p) : Set (s ⊔ p) where
4991 _◁_ : (s : S) → (P s → W S P) → W S P
4993 rec : ∀ {a b} {S : Set a} {P : S → Set b}
4994 (C : W S P → Set) → -- some conclusion we hope holds
4995 ((s : S) → -- given a shape...
4996 (f : P s → W S P) → -- ...and a bunch of kids...
4997 ((p : P s) → C (f p)) → -- ...and C for each kid in the bunch...
4998 C (s ◁ f)) → -- ...does C hold for the node?
4999 (x : W S P) → -- If so, ...
5000 C x -- ...C always holds.
5001 rec C c (s ◁ f) = c s f (λ p → rec C c (f p))
5003 module Examples-→ where
5010 -- These pragmas are needed so we can use number literals.
5011 {-# BUILTIN NATURAL ℕ #-}
5012 {-# BUILTIN ZERO zero #-}
5013 {-# BUILTIN SUC suc #-}
5015 data List (A : Set) : Set where
5017 _∷_ : A → List A → List A
5019 length : ∀ {A} → List A → ℕ
5021 length (_ ∷ l) = suc (length l)
5026 suc x > suc y = x > y
5028 head : ∀ {A} → (l : List A) → length l > 0 → A
5029 head [] p = absurd p
5032 module Examples-× where
5038 even (suc zero) = Empty
5039 even (suc (suc n)) = even n
5044 5-not-even : ¬ (even 5)
5047 there-is-an-even-number : ℕ × even
5048 there-is-an-even-number = 6 , 6-even
5050 _∨_ : (A B : Set) → Set
5051 A ∨ B = Bool × (λ b → if b then A else B)
5053 left : ∀ {A B} → A → A ∨ B
5056 right : ∀ {A B} → B → A ∨ B
5059 [_,_] : {A B C : Set} → (A → C) → (B → C) → A ∨ B → C
5061 (if (fst x) / (λ b → if b then _ else _ → _) then f else g) (snd x)
5063 module Examples-W where
5068 Tr b = if b then Unit else Empty
5074 zero = false ◁ absurd
5077 suc n = true ◁ (λ _ → n)
5083 if b / (λ b → (Tr b → ℕ) → (Tr b → ℕ) → ℕ)
5084 then (λ _ f → (suc (f tt))) else (λ _ _ → y))
5087 module Equality where
5090 data _≡_ {a} {A : Set a} : A → A → Set a where
5093 ≡-elim : ∀ {a b} {A : Set a}
5094 (P : (x y : A) → x ≡ y → Set b) →
5095 ∀ {x y} → P x x (refl x) → (x≡y : x ≡ y) → P x y x≡y
5096 ≡-elim P p (refl x) = p
5098 subst : ∀ {A : Set} (P : A → Set) → ∀ {x y} → (x≡y : x ≡ y) → P x → P y
5099 subst P x≡y p = ≡-elim (λ _ y _ → P y) p x≡y
5101 sym : ∀ {A : Set} (x y : A) → x ≡ y → y ≡ x
5102 sym x y p = subst (λ y′ → y′ ≡ x) p (refl x)
5104 trans : ∀ {A : Set} (x y z : A) → x ≡ y → y ≡ z → x ≡ z
5105 trans x y z p q = subst (λ z′ → x ≡ z′) q p
5107 cong : ∀ {A B : Set} (x y : A) → x ≡ y → (f : A → B) → f x ≡ f y
5108 cong x y p f = subst (λ z → f x ≡ f z) p (refl (f x))
5111 \subsubsection{\mykant}
5112 \label{app:kant-itt}
5114 The following things are missing: $\mytyc{W}$-types, since our
5115 positivity check is overly strict, and equality, since we haven't
5116 implemented that yet.
5119 \verbatiminput{itt.ka}
5122 \subsection{\mykant\ examples}
5123 \label{app:kant-examples}
5126 \verbatiminput{examples.ka}
5129 \subsection{\mykant' hierachy}
5132 This rendition of the Hurken's paradox does not type check with the
5133 hierachy enabled, type checks and loops without it. Adapted from an
5134 Agda version, available at
5135 \url{http://code.haskell.org/Agda/test/succeed/Hurkens.agda}.
5138 \verbatiminput{hurkens.ka}
5141 \subsection{Term representation}
5144 Data type for terms in \mykant.
5146 {\small\begin{verbatim}-- A top-level name.
5148 -- A data/type constructor name.
5151 -- A term, parametrised over the variable (`v') and over the reference
5152 -- type used in the type hierarchy (`r').
5155 | Ty r -- Type, with a hierarchy reference.
5156 | Lam (TmScope r v) -- Abstraction.
5157 | Arr (Tm r v) (TmScope r v) -- Dependent function.
5158 | App (Tm r v) (Tm r v) -- Application.
5159 | Ann (Tm r v) (Tm r v) -- Annotated term.
5160 -- Data constructor, the first ConId is the type constructor and
5161 -- the second is the data constructor.
5162 | Con ADTRec ConId ConId [Tm r v]
5163 -- Data destrutor, again first ConId being the type constructor
5164 -- and the second the name of the eliminator.
5165 | Destr ADTRec ConId Id (Tm r v)
5167 | Hole HoleId [Tm r v]
5168 -- Decoding of propositions.
5172 | Prop r -- The type of proofs, with hierarchy reference.
5175 | And (Tm r v) (Tm r v)
5176 | Forall (Tm r v) (TmScope r v)
5177 -- Heterogeneous equality.
5178 | Eq (Tm r v) (Tm r v) (Tm r v) (Tm r v)
5180 -- Either a data type, or a record.
5181 data ADTRec = ADT | Rec
5183 -- Either a coercion, or coherence.
5184 data Coeh = Coe | Coh\end{verbatim}
5187 \subsection{Graph and constraints modules}
5188 \label{app:constraint}
5190 The modules are respectively named \texttt{Data.LGraph} (short for
5191 `labelled graph'), and \texttt{Data.Constraint}. The type class
5192 constraints on the type parameters are not shown for clarity, unless
5193 they are meaningful to the function. In practice we use the
5194 \texttt{Hashable} type class on the vertex to implement the graph
5195 efficiently with hash maps.
5197 \subsubsection{\texttt{Data.LGraph}}
5200 \verbatiminput{graph.hs}
5203 \subsubsection{\texttt{Data.Constraint}}
5206 \verbatiminput{constraint.hs}
5211 \bibliographystyle{authordate1}
5212 \bibliography{thesis}