2 %% THIS LATEX HURTS YOUR EYES. DO NOT READ.
7 \documentclass[11pt, fleqn, twoside]{article}
10 \usepackage[sc,slantedGreek]{mathpazo}
15 \evensidemargin -.25in
31 \usepackage[pdftex, pdfborderstyle={/S/U/W 0}]{hyperref}
37 \usepackage[fleqn]{amsmath}
38 \usepackage{stmaryrd} %llbracket
41 \usepackage{bussproofs}
53 \usepackage{subcaption}
58 \RecustomVerbatimEnvironment
64 \usetikzlibrary{shapes,arrows,positioning}
65 \usetikzlibrary{intersections}
66 % \usepackage{tikz-cd}
67 % \usepackage{pgfplots}
70 %% -----------------------------------------------------------------------------
72 \usepackage[english]{babel}
73 \usepackage[conor]{agda}
74 \renewcommand{\AgdaKeywordFontStyle}[1]{\ensuremath{\mathrm{\underline{#1}}}}
75 \renewcommand{\AgdaFunction}[1]{\textbf{\textcolor{AgdaFunction}{#1}}}
76 \renewcommand{\AgdaField}{\AgdaFunction}
77 % \definecolor{AgdaBound} {HTML}{000000}
78 \definecolor{AgdaHole} {HTML} {FFFF33}
80 \DeclareUnicodeCharacter{9665}{\ensuremath{\lhd}}
81 \DeclareUnicodeCharacter{964}{\ensuremath{\tau}}
82 \DeclareUnicodeCharacter{963}{\ensuremath{\sigma}}
83 \DeclareUnicodeCharacter{915}{\ensuremath{\Gamma}}
84 \DeclareUnicodeCharacter{8799}{\ensuremath{\stackrel{?}{=}}}
85 \DeclareUnicodeCharacter{9655}{\ensuremath{\rhd}}
87 \renewenvironment{code}%
88 {\noindent\ignorespaces\advance\leftskip\mathindent\AgdaCodeStyle\pboxed\small}%
89 {\endpboxed\par\noindent%
90 \ignorespacesafterend\small}
93 %% -----------------------------------------------------------------------------
96 \newcommand{\mysmall}{}
97 \newcommand{\mysyn}{\AgdaKeyword}
98 \newcommand{\mytyc}[1]{\textup{\AgdaDatatype{#1}}}
99 \newcommand{\mydc}[1]{\textup{\AgdaInductiveConstructor{#1}}}
100 \newcommand{\myfld}[1]{\textup{\AgdaField{#1}}}
101 \newcommand{\myfun}[1]{\textup{\AgdaFunction{#1}}}
102 \newcommand{\myb}[1]{\AgdaBound{$#1$}}
103 \newcommand{\myfield}{\AgdaField}
104 \newcommand{\myind}{\AgdaIndent}
105 \newcommand{\mykant}{\textmd{\textsc{Bertus}}}
106 \newcommand{\mysynel}[1]{#1}
107 \newcommand{\myse}{\mysynel}
108 \newcommand{\mytmsyn}{\mysynel{term}}
109 \newcommand{\mysp}{\ }
110 \newcommand{\myabs}[2]{\mydc{$\lambda$} #1 \mathrel{\mydc{$\mapsto$}} #2}
111 \newcommand{\myappsp}{\hspace{0.07cm}}
112 \newcommand{\myapp}[2]{#1 \myappsp #2}
113 \newcommand{\mysynsep}{\ \ |\ \ }
114 \newcommand{\myITE}[3]{\myfun{If}\, #1\, \myfun{Then}\, #2\, \myfun{Else}\, #3}
115 \newcommand{\mycumul}{\preceq}
118 \newcommand{\mydesc}[3]{
124 \hfill \textup{\textbf{#1}} $#2$
125 \framebox[\textwidth]{
140 \newcommand{\mytmt}{\mysynel{t}}
141 \newcommand{\mytmm}{\mysynel{m}}
142 \newcommand{\mytmn}{\mysynel{n}}
143 \newcommand{\myred}{\leadsto}
144 \newcommand{\mysub}[3]{#1[#2 / #3]}
145 \newcommand{\mytysyn}{\mysynel{type}}
146 \newcommand{\mybasetys}{K}
147 \newcommand{\mybasety}[1]{B_{#1}}
148 \newcommand{\mytya}{\myse{A}}
149 \newcommand{\mytyb}{\myse{B}}
150 \newcommand{\mytycc}{\myse{C}}
151 \newcommand{\myarr}{\mathrel{\textcolor{AgdaDatatype}{\to}}}
152 \newcommand{\myprod}{\mathrel{\textcolor{AgdaDatatype}{\times}}}
153 \newcommand{\myctx}{\Gamma}
154 \newcommand{\myvalid}[1]{#1 \vdash \underline{\mathrm{valid}}}
155 \newcommand{\myjudd}[3]{#1 \vdash #2 : #3}
156 \newcommand{\myjud}[2]{\myjudd{\myctx}{#1}{#2}}
157 \newcommand{\myabss}[3]{\mydc{$\lambda$} #1 {:} #2 \mathrel{\mydc{$\mapsto$}} #3}
158 \newcommand{\mytt}{\mydc{$\langle\rangle$}}
159 \newcommand{\myunit}{\mytyc{Unit}}
160 \newcommand{\mypair}[2]{\mathopen{\mydc{$\langle$}}#1\mathpunct{\mydc{,}} #2\mathclose{\mydc{$\rangle$}}}
161 \newcommand{\myfst}{\myfld{fst}}
162 \newcommand{\mysnd}{\myfld{snd}}
163 \newcommand{\myconst}{\myse{c}}
164 \newcommand{\myemptyctx}{\varepsilon}
165 \newcommand{\myhole}{\AgdaHole}
166 \newcommand{\myfix}[3]{\mysyn{fix} \myappsp #1 {:} #2 \mapsto #3}
167 \newcommand{\mysum}{\mathbin{\textcolor{AgdaDatatype}{+}}}
168 \newcommand{\myleft}[1]{\mydc{left}_{#1}}
169 \newcommand{\myright}[1]{\mydc{right}_{#1}}
170 \newcommand{\myempty}{\mytyc{Empty}}
171 \newcommand{\mycase}[2]{\mathopen{\myfun{[}}#1\mathpunct{\myfun{,}} #2 \mathclose{\myfun{]}}}
172 \newcommand{\myabsurd}[1]{\myfun{absurd}_{#1}}
173 \newcommand{\myarg}{\_}
174 \newcommand{\myderivsp}{}
175 \newcommand{\myderivspp}{\vspace{0.3cm}}
176 \newcommand{\mytyp}{\mytyc{Type}}
177 \newcommand{\myneg}{\myfun{$\neg$}}
178 \newcommand{\myar}{\,}
179 \newcommand{\mybool}{\mytyc{Bool}}
180 \newcommand{\mytrue}{\mydc{true}}
181 \newcommand{\myfalse}{\mydc{false}}
182 \newcommand{\myitee}[5]{\myfun{if}\,#1 / {#2.#3}\,\myfun{then}\,#4\,\myfun{else}\,#5}
183 \newcommand{\mynat}{\mytyc{$\mathbb{N}$}}
184 \newcommand{\myrat}{\mytyc{$\mathbb{R}$}}
185 \newcommand{\myite}[3]{\myfun{if}\,#1\,\myfun{then}\,#2\,\myfun{else}\,#3}
186 \newcommand{\myfora}[3]{(#1 {:} #2) \myarr #3}
187 \newcommand{\myexi}[3]{(#1 {:} #2) \myprod #3}
188 \newcommand{\mypairr}[4]{\mathopen{\mydc{$\langle$}}#1\mathpunct{\mydc{,}} #4\mathclose{\mydc{$\rangle$}}_{#2{.}#3}}
189 \newcommand{\mylist}{\mytyc{List}}
190 \newcommand{\mynil}[1]{\mydc{[]}_{#1}}
191 \newcommand{\mycons}{\mathbin{\mydc{∷}}}
192 \newcommand{\myfoldr}{\myfun{foldr}}
193 \newcommand{\myw}[3]{\myapp{\myapp{\mytyc{W}}{(#1 {:} #2)}}{#3}}
194 \newcommand{\mynodee}{\mathbin{\mydc{$\lhd$}}}
195 \newcommand{\mynode}[2]{\mynodee_{#1.#2}}
196 \newcommand{\myrec}[4]{\myfun{rec}\,#1 / {#2.#3}\,\myfun{with}\,#4}
197 \newcommand{\mylub}{\sqcup}
198 \newcommand{\mydefeq}{\cong}
199 \newcommand{\myrefl}{\mydc{refl}}
200 \newcommand{\mypeq}{\mytyc{=}}
201 \newcommand{\myjeqq}{\myfun{$=$-elim}}
202 \newcommand{\myjeq}[3]{\myapp{\myapp{\myapp{\myjeqq}{#1}}{#2}}{#3}}
203 \newcommand{\mysubst}{\myfun{subst}}
204 \newcommand{\myprsyn}{\myse{prop}}
205 \newcommand{\myprdec}[1]{\mathopen{\mytyc{$\llbracket$}} #1 \mathclose{\mytyc{$\rrbracket$}}}
206 \newcommand{\myand}{\mathrel{\mytyc{$\wedge$}}}
207 \newcommand{\mybigand}{\mathrel{\mytyc{$\bigwedge$}}}
208 \newcommand{\myprfora}[3]{\forall #1 {:} #2. #3}
209 \newcommand{\myimpl}{\mathrel{\mytyc{$\Rightarrow$}}}
210 \newcommand{\mybot}{\mytyc{$\bot$}}
211 \newcommand{\mytop}{\mytyc{$\top$}}
212 \newcommand{\mycoe}{\myfun{coe}}
213 \newcommand{\mycoee}[4]{\myapp{\myapp{\myapp{\myapp{\mycoe}{#1}}{#2}}{#3}}{#4}}
214 \newcommand{\mycoh}{\myfun{coh}}
215 \newcommand{\mycohh}[4]{\myapp{\myapp{\myapp{\myapp{\mycoh}{#1}}{#2}}{#3}}{#4}}
216 \newcommand{\myjm}[4]{(#1 {:} #2) \mathrel{\mytyc{=}} (#3 {:} #4)}
217 \newcommand{\myeq}{\mathrel{\mytyc{=}}}
218 \newcommand{\myprop}{\mytyc{Prop}}
219 \newcommand{\mytmup}{\mytmsyn\uparrow}
220 \newcommand{\mydefs}{\Delta}
221 \newcommand{\mynf}{\Downarrow}
222 \newcommand{\myinff}[3]{#1 \vdash #2 \Uparrow #3}
223 \newcommand{\myinf}[2]{\myinff{\myctx}{#1}{#2}}
224 \newcommand{\mychkk}[3]{#1 \vdash #2 \Downarrow #3}
225 \newcommand{\mychk}[2]{\mychkk{\myctx}{#1}{#2}}
226 \newcommand{\myann}[2]{#1 : #2}
227 \newcommand{\mydeclsyn}{\myse{decl}}
228 \newcommand{\myval}[3]{#1 : #2 \mapsto #3}
229 \newcommand{\mypost}[2]{\mysyn{abstract}\ #1 : #2}
230 \newcommand{\myadt}[4]{\mysyn{data}\ #1 #2\ \mysyn{where}\ #3\{ #4 \}}
231 \newcommand{\myreco}[4]{\mysyn{record}\ #1 #2\ \mysyn{where}\ \{ #4 \}}
232 \newcommand{\myelabt}{\vdash}
233 \newcommand{\myelabf}{\rhd}
234 \newcommand{\myelab}[2]{\myctx \myelabt #1 \myelabf #2}
235 \newcommand{\mytele}{\Delta}
236 \newcommand{\mytelee}{\delta}
237 \newcommand{\mydcctx}{\Gamma}
238 \newcommand{\mynamesyn}{\myse{name}}
239 \newcommand{\myvec}{\overrightarrow}
240 \newcommand{\mymeta}{\textsc}
241 \newcommand{\myhyps}{\mymeta{hyps}}
242 \newcommand{\mycc}{;}
243 \newcommand{\myemptytele}{\varepsilon}
244 \newcommand{\mymetagoes}{\Longrightarrow}
245 % \newcommand{\mytesctx}{\
246 \newcommand{\mytelesyn}{\myse{telescope}}
247 \newcommand{\myrecs}{\mymeta{recs}}
248 \newcommand{\myle}{\mathrel{\lcfun{$\le$}}}
249 \newcommand{\mylet}{\mysyn{let}}
250 \newcommand{\myhead}{\mymeta{head}}
251 \newcommand{\mytake}{\mymeta{take}}
252 \newcommand{\myix}{\mymeta{ix}}
253 \newcommand{\myapply}{\mymeta{apply}}
254 \newcommand{\mydataty}{\mymeta{datatype}}
255 \newcommand{\myisreco}{\mymeta{record}}
256 \newcommand{\mydcsep}{\ |\ }
257 \newcommand{\mytree}{\mytyc{Tree}}
258 \newcommand{\myproj}[1]{\myfun{$\pi_{#1}$}}
259 \newcommand{\mysigma}{\mytyc{$\Sigma$}}
260 \newcommand{\mynegder}{\vspace{-0.3cm}}
261 \newcommand{\myquot}{\Uparrow}
262 \newcommand{\mynquot}{\, \Downarrow}
263 \newcommand{\mycanquot}{\ensuremath{\textsc{quote}{\Downarrow}}}
264 \newcommand{\myneuquot}{\ensuremath{\textsc{quote}{\Uparrow}}}
265 \newcommand{\mymetaguard}{\ |\ }
266 \newcommand{\mybox}{\Box}
267 \newcommand{\mytermi}[1]{\text{\texttt{#1}}}
268 \newcommand{\mysee}[1]{\langle\myse{#1}\rangle}
270 \renewcommand{\[}{\begin{equation*}}
271 \renewcommand{\]}{\end{equation*}}
272 \newcommand{\mymacol}[2]{\text{\textcolor{#1}{$#2$}}}
274 \newtheorem*{mydef}{Definition}
275 \newtheoremstyle{named}{}{}{\itshape}{}{\bfseries}{}{.5em}{\textsc{#1}}
278 \pgfdeclarelayer{background}
279 \pgfdeclarelayer{foreground}
280 \pgfsetlayers{background,main,foreground}
282 %% -----------------------------------------------------------------------------
284 \title{\mykant: Implementing Observational Equality}
285 \author{Francesco Mazzoli \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{<fm2209@ic.ac.uk>}}}
299 % Upper part of the page. The '~' is needed because \\
300 % only works if a paragraph has started.
301 \includegraphics[width=0.4\textwidth]{brouwer-cropped.png}~\\[1cm]
303 \textsc{\Large Final year project}\\[0.5cm]
306 { \huge \mykant: Implementing Observational Equality}\\[1.5cm]
308 {\Large Francesco \textsc{Mazzoli} \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{<fm2209@ic.ac.uk>}}}\\[0.8cm]
310 \begin{minipage}{0.4\textwidth}
311 \begin{flushleft} \large
313 Dr. Steffen \textsc{van Bakel}
316 \begin{minipage}{0.4\textwidth}
317 \begin{flushright} \large
318 \emph{Second marker:} \\
319 Dr. Philippa \textsc{Gardner}
331 The marriage between programming and logic has been a very fertile
332 one. In particular, since the definition of the simply typed lambda
333 calculus, a number of type systems have been devised with increasing
336 Among this systems, Inutitionistic Type Theory (ITT) has been a very
337 popular framework for theorem provers and programming languages.
338 However, reasoning about equality has always been a tricky business in
339 ITT and related theories. In this thesis we will explain why this is
340 the case, and present Observational Type Theory (OTT), a solution to
341 some of the problems with equality.
343 To bring OTT closer to the current practice of interactive theorem
344 provers, we describe \mykant, a system featuring OTT in a setting more
345 close to the one found in widely used provers such as Agda and Coq.
346 Nost notably, we feature used defined inductive and record types and a
347 cumulative, implicit type hierarchy. Having implemented part of
348 $\mykant$ as a Haskell program, we describe some of the implementation
354 \renewcommand{\abstractname}{Acknowledgements}
356 I would like to thank Steffen van Bakel, my supervisor, who was brave
357 enough to believe in my project and who provided much advice and
360 I would also like to thank the Haskell and Agda community on
361 \texttt{IRC}, which guided me through the strange world of types; and
362 in particular Andrea Vezzosi and James Deikun, with whom I entertained
363 countless insightful discussions over the past year. Andrea suggested
364 Observational Type Theory as a topic of study: this thesis would not
365 exist without him. Before them, Tony Field introduced me to Haskell,
366 unknowingly filling most of my free time from that time on.
368 Finally, much of the work stems from the research of Conor McBride,
369 who answered many of my doubts through these months. I also owe him
379 \section{Introduction}
383 \section{Simple and not-so-simple types}
386 \subsection{The untyped $\lambda$-calculus}
389 Along with Turing's machines, the earliest attempts to formalise
390 computation lead to the definition of the $\lambda$-calculus
391 \citep{Church1936}. This early programming language encodes computation
392 with a minimal syntax and no `data' in the traditional sense, but just
393 functions. Here we give a brief overview of the language, which will
394 give the chance to introduce concepts central to the analysis of all the
395 following calculi. The exposition follows the one found in chapter 5 of
398 \begin{mydef}[$\lambda$-terms]
399 Syntax of the $\lambda$-calculus: variables, abstractions, and
405 \begin{array}{r@{\ }c@{\ }l}
406 \mytmsyn & ::= & \myb{x} \mysynsep \myabs{\myb{x}}{\mytmsyn} \mysynsep (\myapp{\mytmsyn}{\mytmsyn}) \\
407 x & \in & \text{Some enumerable set of symbols}
412 Parenthesis will be omitted in the usual way, with application being
415 Abstractions roughly corresponds to functions, and their semantics is more
416 formally explained by the $\beta$-reduction rule.
418 \begin{mydef}[$\beta$-reduction]
419 $\beta$-reduction and substitution for the $\lambda$-calculus.
422 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
425 \myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{\myb{x}}{\mytmn}\text{, where} \\
427 \begin{array}{l@{\ }c@{\ }l}
428 \mysub{\myb{x}}{\myb{x}}{\mytmn} & = & \mytmn \\
429 \mysub{\myb{y}}{\myb{x}}{\mytmn} & = & y\text{, with } \myb{x} \neq y \\
430 \mysub{(\myapp{\mytmt}{\mytmm})}{\myb{x}}{\mytmn} & = & (\myapp{\mysub{\mytmt}{\myb{x}}{\mytmn}}{\mysub{\mytmm}{\myb{x}}{\mytmn}}) \\
431 \mysub{(\myabs{\myb{x}}{\mytmm})}{\myb{x}}{\mytmn} & = & \myabs{\myb{x}}{\mytmm} \\
432 \mysub{(\myabs{\myb{y}}{\mytmm})}{\myb{x}}{\mytmn} & = & \myabs{\myb{z}}{\mysub{\mysub{\mytmm}{\myb{y}}{\myb{z}}}{\myb{x}}{\mytmn}}, \\
433 \multicolumn{3}{l}{\myind{2} \text{with $\myb{x} \neq \myb{y}$ and $\myb{z}$ not free in $\myapp{\mytmm}{\mytmn}$}}
439 The care required during substituting variables for terms is required to avoid
440 name capturing. We will use substitution in the future for other name-binding
441 constructs assuming similar precautions.
443 These few elements have a remarkable expressiveness, and are in fact
444 Turing complete. As a corollary, we must be able to devise a term that
445 reduces forever (`loops' in imperative terms):
447 (\myapp{\omega}{\omega}) \myred (\myapp{\omega}{\omega}) \myred \cdots \text{, with $\omega = \myabs{x}{\myapp{x}{x}}$}
450 A \emph{redex} is a term that can be reduced.
452 In the untyped $\lambda$-calculus this will be the case for an
453 application in which the first term is an abstraction, but in general we
454 call aterm reducible if it appears to the left of a reduction rule.
455 \begin{mydef}[normal form]
456 A term that contains no redexes is said to be in \emph{normal form}.
458 \begin{mydef}[normalising terms and systems]
459 Terms that reduce in a finite number of reduction steps to a normal
460 form are \emph{normalising}. A system in which all terms are
461 normalising is said to be have the \emph{normalisation property}, or
464 Given the reduction behaviour of $(\myapp{\omega}{\omega})$, it is clear
465 that the untyped $\lambda$-calculus does not have the normalisation
468 We have not presented reduction in an algorithmic way, but
469 \emph{evaluation strategies} can be employed to reduce term
470 systematically. Common evaluation strategies include \emph{call by
471 value} (or \emph{strict}), where arguments of abstractions are reduced
472 before being applied to the abstraction; and conversely \emph{call by
473 name} (or \emph{lazy}), where we reduce only when we need to do so to
474 proceed---in other words when we have an application where the function
475 is still not a $\lambda$. In both these reduction strategies we never
476 reduce under an abstraction: for this reason a weaker form of
477 normalisation is used, where both abstractions and normal forms are said
478 to be in \emph{weak head normal form}.
480 \subsection{The simply typed $\lambda$-calculus}
482 A convenient way to `discipline' and reason about $\lambda$-terms is to assign
483 \emph{types} to them, and then check that the terms that we are forming make
484 sense given our typing rules \citep{Curry1934}.The first most basic instance
485 of this idea takes the name of \emph{simply typed $\lambda$-calculus} (STLC).
486 \begin{mydef}[Simply typed $\lambda$-calculus]
487 The syntax and typing rules for the STLC are given in Figure \ref{fig:stlc}.
490 Our types contain a set of \emph{type variables} $\Phi$, which might
491 correspond to some `primitive' types; and $\myarr$, the type former for
492 `arrow' types, the types of functions. The language is explicitly
493 typed: when we bring a variable into scope with an abstraction, we
494 declare its type. Reduction is unchanged from the untyped
500 \begin{array}{r@{\ }c@{\ }l}
501 \mytmsyn & ::= & \myb{x} \mysynsep \myabss{\myb{x}}{\mytysyn}{\mytmsyn} \mysynsep
502 (\myapp{\mytmsyn}{\mytmsyn}) \\
503 \mytysyn & ::= & \myse{\phi} \mysynsep \mytysyn \myarr \mytysyn \mysynsep \\
504 \myb{x} & \in & \text{Some enumerable set of symbols} \\
505 \myse{\phi} & \in & \Phi
510 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
512 \AxiomC{$\myctx(x) = A$}
513 \UnaryInfC{$\myjud{\myb{x}}{A}$}
516 \AxiomC{$\myjudd{\myctx;\myb{x} : A}{\mytmt}{\mytyb}$}
517 \UnaryInfC{$\myjud{\myabss{x}{A}{\mytmt}}{\mytyb}$}
520 \AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$}
521 \AxiomC{$\myjud{\mytmn}{\mytya}$}
522 \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mytyb}$}
526 \caption{Syntax and typing rules for the STLC. Reduction is unchanged from
527 the untyped $\lambda$-calculus.}
531 In the typing rules, a context $\myctx$ is used to store the types of bound
532 variables: $\myctx; \myb{x} : \mytya$ adds a variable to the context and
533 $\myctx(x)$ extracts the type of the rightmost occurrence of $x$.
535 This typing system takes the name of `simply typed lambda calculus' (STLC), and
536 enjoys a number of properties. Two of them are expected in most type systems
538 \begin{mydef}[Progress]
539 A well-typed term is not stuck---it is either a variable, or it
540 does not appear on the left of the $\myred$ relation (currently
541 only $\lambda$), or it can take a step according to the evaluation rules.
543 \begin{mydef}[Subject reduction]
544 If a well-typed term takes a step of evaluation, then the
545 resulting term is also well-typed, and preserves the previous type.
548 However, STLC buys us much more: every well-typed term is normalising
549 \citep{Tait1967}. It is easy to see that we cannot fill the blanks if we want to
550 give types to the non-normalising term shown before:
552 \myapp{(\myabss{\myb{x}}{\myhole{?}}{\myapp{\myb{x}}{\myb{x}}})}{(\myabss{\myb{x}}{\myhole{?}}{\myapp{\myb{x}}{\myb{x}}})}
555 This makes the STLC Turing incomplete. We can recover the ability to loop by
556 adding a combinator that recurses:
557 \begin{mydef}[Fixed-point combinator]\end{mydef}
560 \begin{minipage}{0.5\textwidth}
562 $ \mytmsyn ::= \cdots b \mysynsep \myfix{\myb{x}}{\mytysyn}{\mytmsyn} $
566 \begin{minipage}{0.5\textwidth}
567 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}} {
568 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytmt}{\mytya}$}
569 \UnaryInfC{$\myjud{\myfix{\myb{x}}{\mytya}{\mytmt}}{\mytya}$}
574 \mydesc{reduction:}{\myjud{\mytmsyn}{\mytmsyn}}{
575 $ \myfix{\myb{x}}{\mytya}{\mytmt} \myred \mysub{\mytmt}{\myb{x}}{(\myfix{\myb{x}}{\mytya}{\mytmt})}$
578 This will deprive us of normalisation, which is a particularly bad thing if we
579 want to use the STLC as described in the next section.
581 \subsection{The Curry-Howard correspondence}
583 It turns out that the STLC can be seen a natural deduction system for
584 intuitionistic propositional logic. Terms correspond to proofs, and
585 their types correspond to the propositions they prove. This remarkable
586 fact is known as the Curry-Howard correspondence, or isomorphism.
588 The arrow ($\myarr$) type corresponds to implication. If we wish to prove that
589 that $(\mytya \myarr \mytyb) \myarr (\mytyb \myarr \mytycc) \myarr (\mytya
590 \myarr \mytycc)$, all we need to do is to devise a $\lambda$-term that has the
593 \myabss{\myb{f}}{(\mytya \myarr \mytyb)}{\myabss{\myb{g}}{(\mytyb \myarr \mytycc)}{\myabss{\myb{x}}{\mytya}{\myapp{\myb{g}}{(\myapp{\myb{f}}{\myb{x}})}}}}
595 Which is known to functional programmers as function composition. Going
596 beyond arrow types, we can extend our bare lambda calculus with useful
597 types to represent other logical constructs.
598 \begin{mydef}[The extended STLC]
599 Figure \ref{fig:natded} shows syntax, reduction, and typing rules for
600 the \emph{extendend simply typed $\lambda$-calculus}.
606 \begin{array}{r@{\ }c@{\ }l}
607 \mytmsyn & ::= & \cdots \\
608 & | & \mytt \mysynsep \myapp{\myabsurd{\mytysyn}}{\mytmsyn} \\
609 & | & \myapp{\myleft{\mytysyn}}{\mytmsyn} \mysynsep
610 \myapp{\myright{\mytysyn}}{\mytmsyn} \mysynsep
611 \myapp{\mycase{\mytmsyn}{\mytmsyn}}{\mytmsyn} \\
612 & | & \mypair{\mytmsyn}{\mytmsyn} \mysynsep
613 \myapp{\myfst}{\mytmsyn} \mysynsep \myapp{\mysnd}{\mytmsyn} \\
614 \mytysyn & ::= & \cdots \mysynsep \myunit \mysynsep \myempty \mysynsep \mytmsyn \mysum \mytmsyn \mysynsep \mytysyn \myprod \mytysyn
619 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
622 \begin{array}{l@{ }l@{\ }c@{\ }l}
623 \myapp{\mycase{\mytmm}{\mytmn}}{(\myapp{\myleft{\mytya} &}{\mytmt})} & \myred &
624 \myapp{\mytmm}{\mytmt} \\
625 \myapp{\mycase{\mytmm}{\mytmn}}{(\myapp{\myright{\mytya} &}{\mytmt})} & \myred &
626 \myapp{\mytmn}{\mytmt}
631 \begin{array}{l@{ }l@{\ }c@{\ }l}
632 \myapp{\myfst &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmm \\
633 \myapp{\mysnd &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmn
639 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
641 \AxiomC{\phantom{$\myjud{\mytmt}{\myempty}$}}
642 \UnaryInfC{$\myjud{\mytt}{\myunit}$}
645 \AxiomC{$\myjud{\mytmt}{\myempty}$}
646 \UnaryInfC{$\myjud{\myapp{\myabsurd{\mytya}}{\mytmt}}{\mytya}$}
653 \AxiomC{$\myjud{\mytmt}{\mytya}$}
654 \UnaryInfC{$\myjud{\myapp{\myleft{\mytyb}}{\mytmt}}{\mytya \mysum \mytyb}$}
657 \AxiomC{$\myjud{\mytmt}{\mytyb}$}
658 \UnaryInfC{$\myjud{\myapp{\myright{\mytya}}{\mytmt}}{\mytya \mysum \mytyb}$}
666 \AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$}
667 \AxiomC{$\myjud{\mytmn}{\mytya \myarr \mytycc}$}
668 \AxiomC{$\myjud{\mytmt}{\mytya \mysum \mytyb}$}
669 \TrinaryInfC{$\myjud{\myapp{\mycase{\mytmm}{\mytmn}}{\mytmt}}{\mytycc}$}
676 \AxiomC{$\myjud{\mytmm}{\mytya}$}
677 \AxiomC{$\myjud{\mytmn}{\mytyb}$}
678 \BinaryInfC{$\myjud{\mypair{\mytmm}{\mytmn}}{\mytya \myprod \mytyb}$}
681 \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
682 \UnaryInfC{$\myjud{\myapp{\myfst}{\mytmt}}{\mytya}$}
685 \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
686 \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mytyb}$}
690 \caption{Rules for the extendend STLC. Only the new features are shown, all the
691 rules and syntax for the STLC apply here too.}
695 Tagged unions (or sums, or coproducts---$\mysum$ here, \texttt{Either}
696 in Haskell) correspond to disjunctions, and dually tuples (or pairs, or
697 products---$\myprod$ here, tuples in Haskell) correspond to
698 conjunctions. This is apparent looking at the ways to construct and
699 destruct the values inhabiting those types: for $\mysum$ $\myleft{ }$
700 and $\myright{ }$ correspond to $\vee$ introduction, and
701 $\mycase{\myarg}{\myarg}$ to $\vee$ elimination; for $\myprod$
702 $\mypair{\myarg}{\myarg}$ corresponds to $\wedge$ introduction, $\myfst$
703 and $\mysnd$ to $\wedge$ elimination.
705 The trivial type $\myunit$ corresponds to the logical $\top$ (true), and
706 dually $\myempty$ corresponds to the logical $\bot$ (false). $\myunit$
707 has one introduction rule ($\mytt$), and thus one inhabitant; and no
708 eliminators. $\myempty$ has no introduction rules, and thus no
709 inhabitants; and one eliminator ($\myabsurd{ }$), corresponding to the
710 logical \emph{ex falso quodlibet}.
712 With these rules, our STLC now looks remarkably similar in power and use to the
713 natural deduction we already know.
714 \begin{mydef}[Negation]
715 $\myneg \mytya$ can be expressed as $\mytya \myarr \myempty$.
717 However, there is an important omission: there is no term of
718 the type $\mytya \mysum \myneg \mytya$ (excluded middle), or equivalently
719 $\myneg \myneg \mytya \myarr \mytya$ (double negation), or indeed any term with
720 a type equivalent to those.
722 This has a considerable effect on our logic and it is no coincidence, since there
723 is no obvious computational behaviour for laws like the excluded middle.
724 Logics of this kind are called \emph{intuitionistic}, or \emph{constructive},
725 and all the systems analysed will have this characteristic since they build on
726 the foundation of the STLC.\footnote{There is research to give computational
727 behaviour to classical logic, but I will not touch those subjects.}
729 As in logic, if we want to keep our system consistent, we must make sure that no
730 closed terms (in other words terms not under a $\lambda$) inhabit $\myempty$.
731 The variant of STLC presented here is indeed
732 consistent, a result that follows from the fact that it is
734 Going back to our $\mysyn{fix}$ combinator, it is easy to see how it ruins our
735 desire for consistency. The following term works for every type $\mytya$,
737 \[(\myfix{\myb{x}}{\mytya}{\myb{x}}) : \mytya\]
739 \subsection{Inductive data}
742 To make the STLC more useful as a programming language or reasoning tool it is
743 common to include (or let the user define) inductive data types. These comprise
744 of a type former, various constructors, and an eliminator (or destructor) that
745 serves as primitive recursor.
747 \begin{mydef}[Finite lists for the STLC]
748 We add a $\mylist$ type constructor, along with an `empty
749 list' ($\mynil{ }$) and `cons cell' ($\mycons$) constructor. The eliminator for
750 lists will be the usual folding operation ($\myfoldr$). Full rules in Figure
757 \begin{array}{r@{\ }c@{\ }l}
758 \mytmsyn & ::= & \cdots \mysynsep \mynil{\mytysyn} \mysynsep \mytmsyn \mycons \mytmsyn
760 \myapp{\myapp{\myapp{\myfoldr}{\mytmsyn}}{\mytmsyn}}{\mytmsyn} \\
761 \mytysyn & ::= & \cdots \mysynsep \myapp{\mylist}{\mytysyn}
765 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
767 \begin{array}{l@{\ }c@{\ }l}
768 \myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{\mynil{\mytya}} & \myred & \mytmt \\
770 \myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{(\mytmm \mycons \mytmn)} & \myred &
771 \myapp{\myapp{\myse{f}}{\mytmm}}{(\myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{\mytmn})}
775 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
777 \AxiomC{\phantom{$\myjud{\mytmm}{\mytya}$}}
778 \UnaryInfC{$\myjud{\mynil{\mytya}}{\myapp{\mylist}{\mytya}}$}
781 \AxiomC{$\myjud{\mytmm}{\mytya}$}
782 \AxiomC{$\myjud{\mytmn}{\myapp{\mylist}{\mytya}}$}
783 \BinaryInfC{$\myjud{\mytmm \mycons \mytmn}{\myapp{\mylist}{\mytya}}$}
788 \AxiomC{$\myjud{\mysynel{f}}{\mytya \myarr \mytyb \myarr \mytyb}$}
789 \AxiomC{$\myjud{\mytmm}{\mytyb}$}
790 \AxiomC{$\myjud{\mytmn}{\myapp{\mylist}{\mytya}}$}
791 \TrinaryInfC{$\myjud{\myapp{\myapp{\myapp{\myfoldr}{\mysynel{f}}}{\mytmm}}{\mytmn}}{\mytyb}$}
794 \caption{Rules for lists in the STLC.}
798 In Section \ref{sec:well-order} we will see how to give a general account of
801 \section{Intuitionistic Type Theory}
804 \subsection{Extending the STLC}
806 The STLC can be made more expressive in various ways. \cite{Barendregt1991}
807 succinctly expressed geometrically how we can add expressivity:
810 & \lambda\omega \ar@{-}[rr]\ar@{-}'[d][dd]
811 & & \lambda C \ar@{-}[dd]
813 \lambda2 \ar@{-}[ur]\ar@{-}[rr]\ar@{-}[dd]
814 & & \lambda P2 \ar@{-}[ur]\ar@{-}[dd]
816 & \lambda\underline\omega \ar@{-}'[r][rr]
817 & & \lambda P\underline\omega
819 \lambda{\to} \ar@{-}[rr]\ar@{-}[ur]
820 & & \lambda P \ar@{-}[ur]
823 Here $\lambda{\to}$, in the bottom left, is the STLC. From there can move along
826 \item[Terms depending on types (towards $\lambda{2}$)] We can quantify over
827 types in our type signatures. For example, we can define a polymorphic
828 identity function, where $\mytyp$ denotes the `type of types':
830 (\myabss{\myb{A}}{\mytyp}{\myabss{\myb{x}}{\myb{A}}{\myb{x}}}) : (\myb{A} {:} \mytyp) \myarr \myb{A} \myarr \myb{A}
832 The first and most famous instance of this idea has been System F.
833 This form of polymorphism and has been wildly successful, also thanks
834 to a well known inference algorithm for a restricted version of System
835 F known as Hindley-Milner \citep{milner1978theory}. Languages like
836 Haskell and SML are based on this discipline.
837 \item[Types depending on types (towards $\lambda{\underline{\omega}}$)] We have
838 type operators. For example we could define a function that given types $R$
839 and $\mytya$ forms the type that represents a value of type $\mytya$ in
840 continuation passing style:
841 \[\displaystyle(\myabss{\myb{A} \myar \myb{R}}{\mytyp}{(\myb{A}
842 \myarr \myb{R}) \myarr \myb{R}}) : \mytyp \myarr \mytyp \myarr \mytyp
844 \item[Types depending on terms (towards $\lambda{P}$)] Also known as `dependent
845 types', give great expressive power. For example, we can have values of whose
846 type depend on a boolean:
847 \[\displaystyle(\myabss{\myb{x}}{\mybool}{\myite{\myb{x}}{\mynat}{\myrat}}) : \mybool
851 All the systems preserve the properties that make the STLC well behaved. The
852 system we are going to focus on, Intuitionistic Type Theory, has all of the
853 above additions, and thus would sit where $\lambda{C}$ sits in the
854 `$\lambda$-cube'. It will serve as the logical `core' of all the other
855 extensions that we will present and ultimately our implementation of a similar
858 \subsection{A Bit of History}
860 Logic frameworks and programming languages based on type theory have a
861 long history. Per Martin-L\"{o}f described the first version of his
862 theory in 1971, but then revised it since the original version was
863 inconsistent due to its impredicativity.\footnote{In the early version
864 there was only one universe $\mytyp$ and $\mytyp : \mytyp$; see
865 Section \ref{sec:term-types} for an explanation on why this causes
866 problems.} For this reason he later gave a revised and consistent
867 definition \citep{Martin-Lof1984}.
869 A related development is the polymorphic $\lambda$-calculus, and specifically
870 the previously mentioned System F, which was developed independently by Girard
871 and Reynolds. An overview can be found in \citep{Reynolds1994}. The surprising
872 fact is that while System F is impredicative it is still consistent and strongly
873 normalising. \cite{Coquand1986} further extended this line of work with the
874 Calculus of Constructions (CoC).
876 Most widely used interactive theorem provers are based on ITT. Popular ones
877 include Agda \citep{Norell2007, Bove2009}, Coq \citep{Coq}, and Epigram
878 \citep{McBride2004, EpigramTut}.
880 \subsection{A simple type theory}
883 The calculus I present follows the exposition in \citep{Thompson1991},
884 and is quite close to the original formulation of predicative ITT as
885 found in \citep{Martin-Lof1984}.
886 \begin{mydef}[Intuitionistic Type Theory (ITT)]
887 The syntax and reduction rules are shown in Figure \ref{fig:core-tt-syn}.
888 The typing rules are presented piece by piece in the following sections.
890 Agda and \mykant\ renditions of the presented theory and all the
891 examples is reproduced in Appendix \ref{app:itt-code}.
896 \begin{array}{r@{\ }c@{\ }l}
897 \mytmsyn & ::= & \myb{x} \mysynsep
898 \mytyp_{level} \mysynsep
899 \myunit \mysynsep \mytt \mysynsep
900 \myempty \mysynsep \myapp{\myabsurd{\mytmsyn}}{\mytmsyn} \\
901 & | & \mybool \mysynsep \mytrue \mysynsep \myfalse \mysynsep
902 \myitee{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
903 & | & \myfora{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
904 \myabss{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
905 (\myapp{\mytmsyn}{\mytmsyn}) \\
906 & | & \myexi{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
907 \mypairr{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn} \\
908 & | & \myapp{\myfst}{\mytmsyn} \mysynsep \myapp{\mysnd}{\mytmsyn} \\
909 & | & \myw{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
910 \mytmsyn \mynode{\myb{x}}{\mytmsyn} \mytmsyn \\
911 & | & \myrec{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn} \\
912 level & \in & \mathbb{N}
917 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
920 \begin{array}{l@{ }l@{\ }c@{\ }l}
921 \myitee{\mytrue &}{\myb{x}}{\myse{P}}{\mytmm}{\mytmn} & \myred & \mytmm \\
922 \myitee{\myfalse &}{\myb{x}}{\myse{P}}{\mytmm}{\mytmn} & \myred & \mytmn \\
927 \myapp{(\myabss{\myb{x}}{\mytya}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{\myb{x}}{\mytmn}
931 \begin{array}{l@{ }l@{\ }c@{\ }l}
932 \myapp{\myfst &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmm \\
933 \myapp{\mysnd &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmn
941 \myrec{(\myse{s} \mynode{\myb{x}}{\myse{T}} \myse{f})}{\myb{y}}{\myse{P}}{\myse{p}} \myred
942 \myapp{\myapp{\myapp{\myse{p}}{\myse{s}}}{\myse{f}}}{(\myabss{\myb{t}}{\mysub{\myse{T}}{\myb{x}}{\myse{s}}}{
943 \myrec{\myapp{\myse{f}}{\myb{t}}}{\myb{y}}{\myse{P}}{\mytmt}
947 \caption{Syntax and reduction rules for our type theory.}
948 \label{fig:core-tt-syn}
951 \subsubsection{Types are terms, some terms are types}
952 \label{sec:term-types}
954 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
956 \AxiomC{$\myjud{\mytmt}{\mytya}$}
957 \AxiomC{$\mytya \mydefeq \mytyb$}
958 \BinaryInfC{$\myjud{\mytmt}{\mytyb}$}
961 \AxiomC{\phantom{$\myjud{\mytmt}{\mytya}$}}
962 \UnaryInfC{$\myjud{\mytyp_l}{\mytyp_{l + 1}}$}
967 The first thing to notice is that a barrier between values and types that we had
968 in the STLC is gone: values can appear in types, and the two are treated
969 uniformly in the syntax.
971 While the usefulness of doing this will become clear soon, a consequence is
972 that since types can be the result of computation, deciding type equality is
973 not immediate as in the STLC. For this reason we define \emph{definitional
974 equality}, $\mydefeq$, as the congruence relation extending
975 $\myred$---moreover, when comparing types syntactically we do it up to
976 renaming of bound names ($\alpha$-renaming). For example under this
977 discipline we will find that
979 \myabss{\myb{x}}{\mytya}{\myb{x}} \mydefeq \myabss{\myb{y}}{\mytya}{\myb{y}}
981 Types that are definitionally equal can be used interchangeably. Here
982 the `conversion' rule is not syntax directed, but it is possible to
983 employ $\myred$ to decide term equality in a systematic way, by
984 comparing terms by reducing to their normal forms and then comparing
985 them syntactically; so that a separate conversion rule is not needed.
986 Another thing to notice is that considering the need to reduce terms to
987 decide equality it is essential for a dependently typed system to be
988 terminating and confluent for type checking to be decidable, since every
989 type needs to have a \emph{unique} normal form.
991 Moreover, we specify a \emph{type hierarchy} to talk about `large'
992 types: $\mytyp_0$ will be the type of types inhabited by data:
993 $\mybool$, $\mynat$, $\mylist$, etc. $\mytyp_1$ will be the type of
994 $\mytyp_0$, and so on---for example we have $\mytrue : \mybool :
995 \mytyp_0 : \mytyp_1 : \cdots$. Each type `level' is often called a
996 universe in the literature. While it is possible to simplify things by
997 having only one universe $\mytyp$ with $\mytyp : \mytyp$, this plan is
998 inconsistent for much the same reason that impredicative na\"{\i}ve set
999 theory is \citep{Hurkens1995}. However various techniques can be
1000 employed to lift the burden of explicitly handling universes, as we will
1001 see in Section \ref{sec:term-hierarchy}.
1003 \subsubsection{Contexts}
1005 \begin{minipage}{0.5\textwidth}
1006 \mydesc{context validity:}{\myvalid{\myctx}}{
1008 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
1009 \UnaryInfC{$\myvalid{\myemptyctx}$}
1012 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
1013 \UnaryInfC{$\myvalid{\myctx ; \myb{x} : \mytya}$}
1018 \begin{minipage}{0.5\textwidth}
1019 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1020 \AxiomC{$\myctx(x) = \mytya$}
1021 \UnaryInfC{$\myjud{\myb{x}}{\mytya}$}
1027 We need to refine the notion context to make sure that every variable appearing
1028 is typed correctly, or that in other words each type appearing in the context is
1029 indeed a type and not a value. In every other rule, if no premises are present,
1030 we assume the context in the conclusion to be valid.
1032 Then we can re-introduce the old rule to get the type of a variable for a
1035 \subsubsection{$\myunit$, $\myempty$}
1037 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1038 \begin{tabular}{ccc}
1039 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
1040 \UnaryInfC{$\myjud{\myunit}{\mytyp_0}$}
1042 \UnaryInfC{$\myjud{\myempty}{\mytyp_0}$}
1045 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
1046 \UnaryInfC{$\myjud{\mytt}{\myunit}$}
1048 \UnaryInfC{\phantom{$\myjud{\myempty}{\mytyp_0}$}}
1051 \AxiomC{$\myjud{\mytmt}{\myempty}$}
1052 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
1053 \BinaryInfC{$\myjud{\myapp{\myabsurd{\mytya}}{\mytmt}}{\mytya}$}
1055 \UnaryInfC{\phantom{$\myjud{\myempty}{\mytyp_0}$}}
1060 Nothing surprising here: $\myunit$ and $\myempty$ are unchanged from the STLC,
1061 with the added rules to type $\myunit$ and $\myempty$ themselves, and to make
1062 sure that we are invoking $\myabsurd{}$ over a type.
1064 \subsubsection{$\mybool$, and dependent $\myfun{if}$}
1066 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1067 \begin{tabular}{ccc}
1069 \UnaryInfC{$\myjud{\mybool}{\mytyp_0}$}
1073 \UnaryInfC{$\myjud{\mytrue}{\mybool}$}
1077 \UnaryInfC{$\myjud{\myfalse}{\mybool}$}
1082 \AxiomC{$\myjud{\mytmt}{\mybool}$}
1083 \AxiomC{$\myjudd{\myctx : \mybool}{\mytya}{\mytyp_l}$}
1085 \BinaryInfC{$\myjud{\mytmm}{\mysub{\mytya}{x}{\mytrue}}$ \hspace{0.7cm} $\myjud{\mytmn}{\mysub{\mytya}{x}{\myfalse}}$}
1086 \UnaryInfC{$\myjud{\myitee{\mytmt}{\myb{x}}{\mytya}{\mytmm}{\mytmn}}{\mysub{\mytya}{\myb{x}}{\mytmt}}$}
1090 With booleans we get the first taste of the `dependent' in `dependent
1091 types'. While the two introduction rules for $\mytrue$ and $\myfalse$
1092 are not surprising, the typing rules for $\myfun{if}$ are. In most
1093 strongly typed languages we expect the branches of an $\myfun{if}$
1094 statements to be of the same type, to preserve subject reduction, since
1095 execution could take both paths. This is a pity, since the type system
1096 does not reflect the fact that in each branch we gain knowledge on the
1097 term we are branching on. Which means that programs along the lines of
1099 if null xs then head xs else 0
1101 are a necessary, well typed, danger.
1103 However, in a more expressive system, we can do better: the branches' type can
1104 depend on the value of the scrutinised boolean. This is what the typing rule
1105 expresses: the user provides a type $\mytya$ ranging over an $\myb{x}$
1106 representing the scrutinised boolean type, and the branches are typechecked with
1107 the updated knowledge on the value of $\myb{x}$.
1109 \subsubsection{$\myarr$, or dependent function}
1112 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1113 \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
1114 \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
1115 \BinaryInfC{$\myjud{\myfora{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
1121 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytmt}{\mytyb}$}
1122 \UnaryInfC{$\myjud{\myabss{\myb{x}}{\mytya}{\mytmt}}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
1125 \AxiomC{$\myjud{\mytmm}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
1126 \AxiomC{$\myjud{\mytmn}{\mytya}$}
1127 \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mysub{\mytyb}{\myb{x}}{\mytmn}}$}
1132 Dependent functions are one of the two key features that perhaps most
1133 characterise dependent types---the other being dependent products. With
1134 dependent functions, the result type can depend on the value of the
1135 argument. This feature, together with the fact that the result type
1136 might be a type itself, brings a lot of interesting possibilities.
1137 Following this intuition, in the introduction rule, the return type is
1138 typechecked in a context with an abstracted variable of lhs' type, and
1139 in the elimination rule the actual argument is substituted in the return
1140 type. Keeping the correspondence with logic alive, dependent functions
1141 are much like universal quantifiers ($\forall$) in logic.
1143 For example, assuming that we have lists and natural numbers in our
1144 language, using dependent functions we are write functions of type:
1147 \myfun{length} : (\myb{A} {:} \mytyp_0) \myarr \myapp{\mylist}{\myb{A}} \myarr \mynat \\
1148 \myarg \myfun{$>$} \myarg : \mynat \myarr \mynat \myarr \mytyp_0 \\
1149 \myfun{head} : (\myb{A} {:} \mytyp_0) \myarr (\myb{l} {:} \myapp{\mylist}{\myb{A}})
1150 \myarr \myapp{\myapp{\myfun{length}}{\myb{A}}}{\myb{l}} \mathrel{\myfun{$>$}} 0 \myarr
1155 \myfun{length} is the usual polymorphic length
1156 function. $\myarg\myfun{$>$}\myarg$ is a function that takes two naturals
1157 and returns a type: if the lhs is greater then the rhs, $\myunit$ is
1158 returned, $\myempty$ otherwise. This way, we can express a
1159 `non-emptyness' condition in $\myfun{head}$, by including a proof that
1160 the length of the list argument is non-zero. This allows us to rule out
1161 the `empty list' case, so that we can safely return the first element.
1163 Again, we need to make sure that the type hierarchy is respected, which
1164 is the reason why a type formed by $\myarr$ will live in the least upper
1165 bound of the levels of argument and return type. If this was not the
1166 case, we would be able to form a `powerset' function along the lines of
1169 \myfun{P} : \mytyp_0 \myarr \mytyp_0 \\
1170 \myfun{P} \myappsp \myb{A} \mapsto \myb{A} \myarr \mytyp_0
1173 Where the type of $\myb{A} \myarr \mytyp_0$ is in $\mytyp_0$ itself.
1174 Using this and similar devices we would be able to derive falsity
1175 \citep{Hurkens1995}. This trend will continue with the other type-level
1176 binders, $\myprod$ and $\mytyc{W}$.
1178 \subsubsection{$\myprod$, or dependent product}
1181 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1182 \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
1183 \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
1184 \BinaryInfC{$\myjud{\myexi{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
1190 \AxiomC{$\myjud{\mytmm}{\mytya}$}
1191 \AxiomC{$\myjud{\mytmn}{\mysub{\mytyb}{\myb{x}}{\mytmm}}$}
1192 \BinaryInfC{$\myjud{\mypairr{\mytmm}{\myb{x}}{\mytyb}{\mytmn}}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
1194 \UnaryInfC{\phantom{$--$}}
1197 \AxiomC{$\myjud{\mytmt}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
1198 \UnaryInfC{$\hspace{0.7cm}\myjud{\myapp{\myfst}{\mytmt}}{\mytya}\hspace{0.7cm}$}
1200 \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mysub{\mytyb}{\myb{x}}{\myapp{\myfst}{\mytmt}}}$}
1205 If dependent functions are a generalisation of $\myarr$ in the STLC,
1206 dependent products are a generalisation of $\myprod$ in the STLC. The
1207 improvement is that the second element's type can depend on the value of
1208 the first element. The corrispondence with logic is through the
1209 existential quantifier: $\exists x \in \mathbb{N}. even(x)$ can be
1210 expressed as $\myexi{\myb{x}}{\mynat}{\myapp{\myfun{even}}{\myb{x}}}$.
1211 The first element will be a number, and the second evidence that the
1212 number is even. This highlights the fact that we are working in a
1213 constructive logic: if we have an existence proof, we can always ask for
1214 a witness. This means, for instance, that $\neg \forall \neg$ is not
1215 equivalent to $\exists$.
1217 Another perhaps more `dependent' application of products, paired with
1218 $\mybool$, is to offer choice between different types. For example we
1219 can easily recover disjunctions:
1222 \myarg\myfun{$\vee$}\myarg : \mytyp_0 \myarr \mytyp_0 \myarr \mytyp_0 \\
1223 \myb{A} \mathrel{\myfun{$\vee$}} \myb{B} \mapsto \myexi{\myb{x}}{\mybool}{\myite{\myb{x}}{\myb{A}}{\myb{B}}} \\ \ \\
1224 \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} \\
1225 \myfun{case} \myappsp \myb{A} \myappsp \myb{B} \myappsp \myb{C} \myappsp \myb{f} \myappsp \myb{g} \myappsp \myb{x} \mapsto \\
1226 \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}})}
1230 \subsubsection{$\mytyc{W}$, or well-order}
1231 \label{sec:well-order}
1233 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1235 \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
1236 \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
1237 \BinaryInfC{$\myjud{\myw{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
1242 \AxiomC{$\myjud{\mytmt}{\mytya}$}
1243 \AxiomC{$\myjud{\mysynel{f}}{\mysub{\mytyb}{\myb{x}}{\mytmt} \myarr \myw{\myb{x}}{\mytya}{\mytyb}}$}
1244 \BinaryInfC{$\myjud{\mytmt \mynode{\myb{x}}{\mytyb} \myse{f}}{\myw{\myb{x}}{\mytya}{\mytyb}}$}
1250 \AxiomC{$\myjud{\myse{u}}{\myw{\myb{x}}{\myse{S}}{\myse{T}}}$}
1251 \AxiomC{$\myjudd{\myctx; \myb{w} : \myw{\myb{x}}{\myse{S}}{\myse{T}}}{\myse{P}}{\mytyp_l}$}
1253 \BinaryInfC{$\myjud{\myse{p}}{
1254 \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}}}}
1256 \UnaryInfC{$\myjud{\myrec{\myse{u}}{\myb{w}}{\myse{P}}{\myse{p}}}{\mysub{\myse{P}}{\myb{w}}{\myse{u}}}$}
1260 Finally, the well-order type, or in short $\mytyc{W}$-type, which will
1261 let us represent inductive data in a general (but clumsy) way. We can
1262 form `nodes' of the shape $\mytmt \mynode{\myb{x}}{\mytyb} \myse{f} :
1263 \myw{\myb{x}}{\mytya}{\mytyb}$ that contain data ($\mytmt$) of type and
1264 one `child' for each member of $\mysub{\mytyb}{\myb{x}}{\mytmt}$. The
1265 $\myfun{rec}\ \myfun{with}$ acts as an induction principle on
1266 $\mytyc{W}$, given a predicate an a function dealing with the inductive
1267 case---we will gain more intuition about inductive data in ITT in
1268 Section \ref{sec:user-type}.
1270 For example, if we want to form natural numbers, we can take
1273 \mytyc{Tr} : \mybool \myarr \mytyp_0 \\
1274 \mytyc{Tr} \myappsp \myb{b} \mapsto \myfun{if}\, \myb{b}\, \myunit\, \myfun{else}\, \myempty \\
1276 \mynat : \mytyp_0 \\
1277 \mynat \mapsto \myw{\myb{b}}{\mybool}{(\mytyc{Tr}\myappsp\myb{b})}
1280 Each node will contain a boolean. If $\mytrue$, the number is non-zero,
1281 and we will have one child representing its predecessor, given that
1282 $\mytyc{Tr}$ will return $\myunit$. If $\myfalse$, the number is zero,
1283 and we will have no predecessors (children), given the $\myempty$:
1286 \mydc{zero} : \mynat \\
1287 \mydc{zero} \mapsto \myfalse \mynodee (\myabs{\myb{z}}{\myabsurd{\mynat} \myappsp \myb{x}}) \\
1289 \mydc{suc} : \mynat \myarr \mynat \\
1290 \mydc{suc}\myappsp \myb{x} \mapsto \mytrue \mynodee (\myabs{\myarg}{\myb{x}})
1293 And with a bit of effort, we can recover addition:
1296 \myfun{plus} : \mynat \myarr \mynat \myarr \mynat \\
1297 \myfun{plus} \myappsp \myb{x} \myappsp \myb{y} \mapsto \\
1298 \myind{2} \myfun{rec}\, \myb{x} / \myb{b}.\mynat \, \\
1299 \myind{2} \myfun{with}\, \myabs{\myb{b}}{\\
1300 \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) \\
1301 \myind{2}\myind{2}\myfun{then}\,(\myabs{\myarg\, \myb{f}}{\mydc{suc}\myappsp (\myapp{\myb{f}}{\mytt})})\, \myfun{else}\, (\myabs{\myarg\, \myarg}{\myb{y}})}
1304 Note how we explicitly have to type the branches to make them
1305 match with the definition of $\mynat$---which gives a taste of the
1306 `clumsiness' of $\mytyc{W}$-types, which while useful as a reasoning
1307 tool are useless to the user modelling data types.
1309 \section{The struggle for equality}
1310 \label{sec:equality}
1312 In the previous section we saw how a type checker (or a human) needs a
1313 notion of \emph{definitional equality}. Beyond this meta-theoretic
1314 notion, in this section we will explore the ways of expressing equality
1315 \emph{inside} the theory, as a reasoning tool available to the user.
1316 This area is the main concern of this thesis, and in general a very
1317 active research topic, since we do not have a fully satisfactory
1318 solution, yet. As in the previous section, everything presented is
1319 formalised in Agda in Appendix \ref{app:agda-itt}.
1321 \subsection{Propositional equality}
1323 \begin{mydef}[Propositional equality] The syntax, reduction, and typing
1324 rules for propositional equality and related constructs is defined as:
1328 \begin{minipage}{0.5\textwidth}
1331 \begin{array}{r@{\ }c@{\ }l}
1332 \mytmsyn & ::= & \cdots \\
1333 & | & \mypeq \myappsp \mytmsyn \myappsp \mytmsyn \myappsp \mytmsyn \mysynsep
1334 \myapp{\myrefl}{\mytmsyn} \\
1335 & | & \myjeq{\mytmsyn}{\mytmsyn}{\mytmsyn}
1340 \begin{minipage}{0.5\textwidth}
1341 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
1343 \myjeq{\myse{P}}{(\myapp{\myrefl}{\mytmm})}{\mytmn} \myred \mytmn
1349 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1350 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
1351 \AxiomC{$\myjud{\mytmm}{\mytya}$}
1352 \AxiomC{$\myjud{\mytmn}{\mytya}$}
1353 \TrinaryInfC{$\myjud{\mypeq \myappsp \mytya \myappsp \mytmm \myappsp \mytmn}{\mytyp_l}$}
1359 \AxiomC{$\begin{array}{c}\ \\\myjud{\mytmm}{\mytya}\hspace{1.1cm}\mytmm \mydefeq \mytmn\end{array}$}
1360 \UnaryInfC{$\myjud{\myapp{\myrefl}{\mytmm}}{\mypeq \myappsp \mytya \myappsp \mytmm \myappsp \mytmn}$}
1365 \myjud{\myse{P}}{\myfora{\myb{x}\ \myb{y}}{\mytya}{\myfora{q}{\mypeq \myappsp \mytya \myappsp \myb{x} \myappsp \myb{y}}{\mytyp_l}}} \\
1366 \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})}}
1369 \UnaryInfC{$\myjud{\myjeq{\myse{P}}{\myse{q}}{\myse{p}}}{\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmn}}{q}}$}
1374 To express equality between two terms inside ITT, the obvious way to do
1375 so is to have equality to be a type. Here we present what has survived
1376 as the dominating form of equality in systems based on ITT up to the
1379 Our type former is $\mypeq$, which given a type (in this case
1380 $\mytya$) relates equal terms of that type. $\mypeq$ has one introduction
1381 rule, $\myrefl$, which introduces an equality relation between definitionally
1384 Finally, we have one eliminator for $\mypeq$, $\myjeqq$. $\myjeq{\myse{P}}{\myse{q}}{\myse{p}}$ takes
1386 \item $\myse{P}$, a predicate working with two terms of a certain type (say
1387 $\mytya$) and a proof of their equality
1388 \item $\myse{q}$, a proof that two terms in $\mytya$ (say $\myse{m}$ and
1389 $\myse{n}$) are equal
1390 \item and $\myse{p}$, an inhabitant of $\myse{P}$ applied to $\myse{m}$
1391 twice, plus the trivial proof by reflexivity showing that $\myse{m}$
1394 Given these ingredients, $\myjeqq$ retuns a member of $\myse{P}$ applied
1395 to $\mytmm$, $\mytmn$, and $\myse{q}$. In other words $\myjeqq$ takes a
1396 witness that $\myse{P}$ works with \emph{definitionally equal} terms,
1397 and returns a witness of $\myse{P}$ working with \emph{propositionally
1398 equal} terms. Invokations of $\myjeqq$ will vanish when the equality
1399 proofs will reduce to invocations to reflexivity, at which point the
1400 arguments must be definitionally equal, and thus the provided
1401 $\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmm}}{(\myapp{\myrefl}{\mytmm})}$
1402 can be returned. This means that $\myjeqq$ will not compute with
1403 hypotetical proofs, which makes sense given that they might be false.
1405 While the $\myjeqq$ rule is slightly convoluted, ve can derive many more
1406 `friendly' rules from it, for example a more obvious `substitution' rule, that
1407 replaces equal for equal in predicates:
1410 \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}}}}} \\
1411 \myfun{subst}\myappsp \myb{A}\myappsp\myb{P}\myappsp\myb{x}\myappsp\myb{y}\myappsp\myb{q}\myappsp\myb{p} \mapsto
1412 \myjeq{(\myabs{\myb{x}\ \myb{y}\ \myb{q}}{\myapp{\myb{P}}{\myb{y}}})}{\myb{p}}{\myb{q}}
1415 Once we have $\myfun{subst}$, we can easily prove more familiar laws regarding
1416 equality, such as symmetry, transitivity, congruence laws, etc.
1418 \subsection{Common extensions}
1420 Our definitional and propositional equalities can be enhanced in various
1421 ways. Obviously if we extend the definitional equality we are also
1422 automatically extend propositional equality, given how $\myrefl$ works.
1424 \subsubsection{$\eta$-expansion}
1425 \label{sec:eta-expand}
1427 A simple extension to our definitional equality is $\eta$-expansion.
1428 Given an abstract variable $\myb{f} : \mytya \myarr \mytyb$ the aim is
1429 to have that $\myb{f} \mydefeq
1430 \myabss{\myb{x}}{\mytya}{\myapp{\myb{f}}{\myb{x}}}$. We can achieve
1431 this by `expanding' terms based on their types, a process also known as
1432 \emph{quotation}---a term borrowed from the practice of
1433 \emph{normalisation by evaluation}, where we embed terms in some host
1434 language with an existing notion of computation, and then reify them
1435 back into terms, which will `smooth out' differences like the one above
1438 The same concept applies to $\myprod$, where we expand each inhabitant
1439 by reconstructing it by getting its projections, so that $\myb{x}
1440 \mydefeq \mypair{\myfst \myappsp \myb{x}}{\mysnd \myappsp \myb{x}}$.
1441 Similarly, all one inhabitants of $\myunit$ and all zero inhabitants of
1442 $\myempty$ can be considered equal. Quotation can be performed in a
1443 type-directed way, as we will witness in Section \ref{sec:kant-irr}.
1445 \begin{mydef}[Congruence and $\eta$-laws]
1446 To justify quotation in our type system we will add a congruence law
1447 for abstractions and a similar law for products, plus the fact that all
1448 elements of $\myunit$ or $\myempty$ are equal.
1451 \mydesc{definitional equality:}{\myjud{\mytmm \mydefeq \mytmn}{\mytmsyn}}{
1453 \AxiomC{$\myjudd{\myctx; \myb{y} : \mytya}{\myapp{\myse{f}}{\myb{x}} \mydefeq \myapp{\myse{g}}{\myb{x}}}{\mysub{\mytyb}{\myb{x}}{\myb{y}}}$}
1454 \UnaryInfC{$\myjud{\myse{f} \mydefeq \myse{g}}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
1457 \AxiomC{$\myjud{\mypair{\myapp{\myfst}{\mytmm}}{\myapp{\mysnd}{\mytmm}} \mydefeq \mypair{\myapp{\myfst}{\mytmn}}{\myapp{\mysnd}{\mytmn}}}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
1458 \UnaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
1465 \AxiomC{$\myjud{\mytmm}{\myunit}$}
1466 \AxiomC{$\myjud{\mytmn}{\myunit}$}
1467 \BinaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\myunit}$}
1470 \AxiomC{$\myjud{\mytmm}{\myempty}$}
1471 \AxiomC{$\myjud{\mytmn}{\myempty}$}
1472 \BinaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\myempty}$}
1477 \subsubsection{Uniqueness of identity proofs}
1479 Another common but controversial addition to propositional equality is
1480 the $\myfun{K}$ axiom, which essentially states that all equality proofs
1483 \begin{mydef}[$\myfun{K}$ axiom]\end{mydef}
1484 \mydesc{typing:}{\myjud{\mytmm \mydefeq \mytmn}{\mytmsyn}}{
1487 \myjud{\myse{P}}{\myfora{\myb{x}}{\mytya}{\myb{x} \mypeq{\mytya} \myb{x} \myarr \mytyp}} \\\
1488 \myjud{\mytmt}{\mytya} \hspace{1cm}
1489 \myjud{\myse{p}}{\myse{P} \myappsp \mytmt \myappsp (\myrefl \myappsp \mytmt)} \hspace{1cm}
1490 \myjud{\myse{q}}{\mytmt \mypeq{\mytya} \mytmt}
1493 \UnaryInfC{$\myjud{\myfun{K} \myappsp \myse{P} \myappsp \myse{t} \myappsp \myse{p} \myappsp \myse{q}}{\myse{P} \myappsp \mytmt \myappsp \myse{q}}$}
1497 \cite{Hofmann1994} showed that $\myfun{K}$ is not derivable from the
1498 $\myjeqq$ axiom that we presented, and \cite{McBride2004} showed that it is
1499 needed to implement `dependent pattern matching', as first proposed by
1500 \cite{Coquand1992}. Thus, $\myfun{K}$ is derivable in the systems that
1501 implement dependent pattern matching, such as Epigram and Agda; but for
1504 $\myfun{K}$ is controversial mainly because it is at odds with
1505 equalities that include computational behaviour, most notably
1506 Voevodsky's `Univalent Foundations', which includes a \emph{univalence}
1507 axiom that identifies isomorphisms between types with propositional
1508 equality. For example we would have two isomorphisms, and thus two
1509 equalities, between $\mybool$ and $\mybool$, corresponding to the two
1510 permutations---one is the identity, and one swaps the elements. Given
1511 this, $\myfun{K}$ and univalence are inconsistent, and thus a form of
1512 dependent pattern matching that does not imply $\myfun{K}$ is subject of
1513 research.\footnote{More information about univalence can be found at
1514 \url{http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations.html}.}
1516 \subsection{Limitations}
1518 \epigraph{\emph{Half of my time spent doing research involves thinking up clever
1519 schemes to avoid needing functional extensionality.}}{@larrytheliquid}
1521 Propositional equality as described is quite restricted when
1522 reasoning about equality beyond the term structure, which is what definitional
1523 equality gives us (extension notwithstanding).
1525 The problem is best exemplified by \emph{function extensionality}. In
1526 mathematics, we would expect to be able to treat functions that give equal
1527 output for equal input as the same. When reasoning in a mechanised framework
1528 we ought to be able to do the same: in the end, without considering the
1529 operational behaviour, all functions equal extensionally are going to be
1530 replaceable with one another.
1532 However this is not the case, or in other words with the tools we have we have
1535 \myfun{ext} : \myfora{\myb{A}\ \myb{B}}{\mytyp}{\myfora{\myb{f}\ \myb{g}}{
1536 \myb{A} \myarr \myb{B}}{
1537 (\myfora{\myb{x}}{\myb{A}}{\mypeq \myappsp \myb{B} \myappsp (\myapp{\myb{f}}{\myb{x}}) \myappsp (\myapp{\myb{g}}{\myb{x}})}) \myarr
1538 \mypeq \myappsp (\myb{A} \myarr \myb{B}) \myappsp \myb{f} \myappsp \myb{g}
1542 To see why this is the case, consider the functions
1543 \[\myabs{\myb{x}}{0 \mathrel{\myfun{$+$}} \myb{x}}$ and $\myabs{\myb{x}}{\myb{x} \mathrel{\myfun{$+$}} 0}\]
1544 where $\myfun{$+$}$ is defined by recursion on the first argument,
1545 gradually destructing it to build up successors of the second argument.
1546 The two functions are clearly extensionally equal, and we can in fact
1549 \myfora{\myb{x}}{\mynat}{(0 \mathrel{\myfun{$+$}} \myb{x}) \mypeq{\mynat} (\myb{x} \mathrel{\myfun{$+$}} 0)}
1551 By analysis on the $\myb{x}$. However, the two functions are not
1552 definitionally equal, and thus we won't be able to get rid of the
1555 For the reasons given above, theories that offer a propositional equality
1556 similar to what we presented are called \emph{intensional}, as opposed
1557 to \emph{extensional}. Most systems widely used today (such as Agda,
1558 Coq, and Epigram) are of this kind.
1560 This is quite an annoyance that often makes reasoning awkward to execute. It
1561 also extends to other fields, for example proving bisimulation between
1562 processes specified by coinduction, or in general proving equivalences based
1563 on the behaviour on a term.
1565 \subsection{Equality reflection}
1567 One way to `solve' this problem is by identifying propositional equality with
1568 definitional equality.
1570 \begin{mydef}[Equality reflection]\end{mydef}
1571 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1572 \AxiomC{$\myjud{\myse{q}}{\mytmm \mypeq{\mytya} \mytmn}$}
1573 \UnaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\mytya}$}
1577 The \emph{equality reflection} rule is a very different rule from the
1578 ones we saw up to now: it links a typing judgement internal to the type
1579 theory to a meta-theoretic judgement that the type checker uses to work
1580 with terms. It is easy to see the dangerous consequences that this
1583 \item The rule is not syntax directed, and the type checker is
1584 presumably expected to come up with equality proofs when needed.
1585 \item More worryingly, type checking becomes undecidable also because
1586 computing under false assumptions becomes unsafe, since we derive any
1587 equality proof and then use equality reflection and the conversion
1588 rule to have terms of any type.
1590 For example, assuming that we are in a context that contains
1592 \myb{A} : \mytyp; \myb{q} : \mypeq \myappsp \mytyp
1593 \myappsp (\mytya \myarr \mytya) \myappsp \mytya
1595 we can write a looping term similar to the one we saw in Section
1600 Given these facts theories employing equality reflection, like NuPRL
1601 \citep{NuPRL}, carry the derivations that gave rise to each typing judgement
1602 to keep the systems manageable.
1604 For all its faults, equality reflection does allow us to prove extensionality,
1605 using the extensions we gave above. Assuming that $\myctx$ contains
1606 \[\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}}}\]
1610 \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}$}
1611 \RightLabel{equality reflection}
1612 \UnaryInfC{$\myjudd{\myctx; \myb{x} : \myb{A}}{\myapp{\myb{f}}{\myb{x}} \mydefeq \myapp{\myb{g}}{\myb{x}}}{\myb{B}}$}
1613 \RightLabel{congruence for $\lambda$s}
1614 \UnaryInfC{$\myjud{(\myabs{\myb{x}}{\myapp{\myb{f}}{\myb{x}}}) \mydefeq (\myabs{\myb{x}}{\myapp{\myb{g}}{\myb{x}}})}{\myb{A} \myarr \myb{B}}$}
1615 \RightLabel{$\eta$-law for $\lambda$}
1616 \UnaryInfC{$\hspace{1.45cm}\myjud{\myb{f} \mydefeq \myb{g}}{\myb{A} \myarr \myb{B}}\hspace{1.45cm}$}
1617 \RightLabel{$\myrefl$}
1618 \UnaryInfC{$\myjud{\myapp{\myrefl}{\myb{f}}}{\myb{f} \mypeq{} \myb{g}}$}
1621 Now, the question is: do we need to give up well-behavedness of our theory to
1622 gain extensionality?
1624 \section{The observational approach}
1627 % TODO add \begin{mydef}s
1629 A recent development by \citet{Altenkirch2007}, \emph{Observational Type
1630 Theory} (OTT), promises to keep the well behavedness of ITT while
1631 being able to gain many useful equality proofs,\footnote{It is suspected
1632 that OTT gains \emph{all} the equality proofs of ETT, but no proof
1633 exists yet.} including function extensionality. The main idea is to
1634 give the user the possibility to \emph{coerce} (or transport) values
1635 from a type $\mytya$ to a type $\mytyb$, if the type checker can prove
1636 structurally that $\mytya$ and $\mytyb$ are equal; and providing a
1637 value-level equality based on similar principles. Here we give an
1638 exposition which follows closely the original paper.
1640 \subsection{A simpler theory, a propositional fragment}
1643 $\mytyp_l$ is replaced by $\mytyp$. \\\ \\
1645 \begin{array}{r@{\ }c@{\ }l}
1646 \mytmsyn & ::= & \cdots \mysynsep \myprdec{\myprsyn} \mysynsep
1647 \myITE{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
1648 \myprsyn & ::= & \mybot \mysynsep \mytop \mysynsep \myprsyn \myand \myprsyn
1649 \mysynsep \myprfora{\myb{x}}{\mytmsyn}{\myprsyn}
1656 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
1658 \begin{array}{l@{}l@{\ }c@{\ }l}
1659 \myITE{\mytrue &}{\mytya}{\mytyb} & \myred & \mytya \\
1660 \myITE{\myfalse &}{\mytya}{\mytyb} & \myred & \mytyb
1667 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1669 \AxiomC{$\myjud{\myse{P}}{\myprop}$}
1670 \UnaryInfC{$\myjud{\myprdec{\myse{P}}}{\mytyp}$}
1673 \AxiomC{$\myjud{\mytmt}{\mybool}$}
1674 \AxiomC{$\myjud{\mytya}{\mytyp}$}
1675 \AxiomC{$\myjud{\mytyb}{\mytyp}$}
1676 \TrinaryInfC{$\myjud{\myITE{\mytmt}{\mytya}{\mytyb}}{\mytyp}$}
1683 \mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
1684 \begin{tabular}{ccc}
1685 \AxiomC{\phantom{$\myjud{\myse{P}}{\myprop}$}}
1686 \UnaryInfC{$\myjud{\mytop}{\myprop}$}
1688 \UnaryInfC{$\myjud{\mybot}{\myprop}$}
1691 \AxiomC{$\myjud{\myse{P}}{\myprop}$}
1692 \AxiomC{$\myjud{\myse{Q}}{\myprop}$}
1693 \BinaryInfC{$\myjud{\myse{P} \myand \myse{Q}}{\myprop}$}
1695 \UnaryInfC{\phantom{$\myjud{\mybot}{\myprop}$}}
1698 \AxiomC{$\myjud{\myse{A}}{\mytyp}$}
1699 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\myse{P}}{\myprop}$}
1700 \BinaryInfC{$\myjud{\myprfora{\myb{x}}{\mytya}{\myse{P}}}{\myprop}$}
1702 \UnaryInfC{\phantom{$\myjud{\mybot}{\myprop}$}}
1707 Our foundation will be a type theory like the one of section
1708 \ref{sec:itt}, with only one level: $\mytyp_0$. In this context we will
1709 drop the $0$ and call $\mytyp_0$ $\mytyp$. Moreover, since the old
1710 $\myfun{if}\myarg\myfun{then}\myarg\myfun{else}$ was able to return
1711 types thanks to the hierarchy (which is gone), we need to reintroduce an
1712 ad-hoc conditional for types, where the reduction rule is the obvious
1715 However, we have an addition: a universe of \emph{propositions},
1716 $\myprop$. $\myprop$ isolates a fragment of types at large, and
1717 indeed we can `inject' any $\myprop$ back in $\mytyp$ with $\myprdec{\myarg}$: \\
1718 \mydesc{proposition decoding:}{\myprdec{\mytmsyn} \myred \mytmsyn}{
1721 \begin{array}{l@{\ }c@{\ }l}
1722 \myprdec{\mybot} & \myred & \myempty \\
1723 \myprdec{\mytop} & \myred & \myunit
1728 \begin{array}{r@{ }c@{ }l@{\ }c@{\ }l}
1729 \myprdec{&\myse{P} \myand \myse{Q} &} & \myred & \myprdec{\myse{P}} \myprod \myprdec{\myse{Q}} \\
1730 \myprdec{&\myprfora{\myb{x}}{\mytya}{\myse{P}} &} & \myred &
1731 \myfora{\myb{x}}{\mytya}{\myprdec{\myse{P}}}
1736 Propositions are what we call the types of \emph{proofs}, or types
1737 whose inhabitants contain no `data', much like $\myunit$. The goal of
1738 doing this is twofold: erasing all top-level propositions when
1739 compiling; and to identify all equivalent propositions as the same, as
1742 Why did we choose what we have in $\myprop$? Given the above
1743 criteria, $\mytop$ obviously fits the bill, since it us one element.
1744 A pair of propositions $\myse{P} \myand \myse{Q}$ still won't get us
1745 data, since if they both have one element the only possible pair is
1746 the one formed by said elements. Finally, if $\myse{P}$ is a
1747 proposition and we have $\myprfora{\myb{x}}{\mytya}{\myse{P}}$, the
1748 decoding will be a function which returns propositional content. The
1749 only threat is $\mybot$, by which we can fabricate anything we want:
1750 however if we are consistent there will be nothing of type $\mybot$ at
1751 the top level, which is what we care about regarding proof erasure.
1753 \subsection{Equality proofs}
1757 \begin{array}{r@{\ }c@{\ }l}
1758 \mytmsyn & ::= & \cdots \mysynsep
1759 \mycoee{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \mysynsep
1760 \mycohh{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
1761 \myprsyn & ::= & \cdots \mysynsep \mytmsyn \myeq \mytmsyn \mysynsep
1762 \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn}
1767 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1769 \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
1770 \AxiomC{$\myjud{\mytmt}{\mytya}$}
1771 \BinaryInfC{$\myjud{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}$}
1774 \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
1775 \AxiomC{$\myjud{\mytmt}{\mytya}$}
1776 \BinaryInfC{$\myjud{\mycohh{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\myprdec{\myjm{\mytmt}{\mytya}{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}}}$}
1782 \mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
1787 \myjud{\myse{A}}{\mytyp} \hspace{1cm} \myjud{\myse{B}}{\mytyp}
1790 \UnaryInfC{$\myjud{\mytya \myeq \mytyb}{\myprop}$}
1795 \myjud{\myse{A}}{\mytyp} \hspace{1cm} \myjud{\mytmm}{\myse{A}} \\
1796 \myjud{\myse{B}}{\mytyp} \hspace{1cm} \myjud{\mytmn}{\myse{B}}
1799 \UnaryInfC{$\myjud{\myjm{\mytmm}{\myse{A}}{\mytmn}{\myse{B}}}{\myprop}$}
1806 While isolating a propositional universe as presented can be a useful
1807 exercises on its own, what we are really after is a useful notion of
1808 equality. In OTT we want to maintain the notion that things judged to
1809 be equal are still always repleaceable for one another with no
1810 additional changes. Note that this is not the same as saying that they
1811 are definitionally equal, since as we saw extensionally equal functions,
1812 while satisfying the above requirement, are not definitionally equal.
1814 Towards this goal we introduce two equality constructs in
1815 $\myprop$---the fact that they are in $\myprop$ indicates that they
1816 indeed have no computational content. The first construct, $\myarg
1817 \myeq \myarg$, relates types, the second,
1818 $\myjm{\myarg}{\myarg}{\myarg}{\myarg}$, relates values. The
1819 value-level equality is different from our old propositional equality:
1820 instead of ranging over only one type, we might form equalities between
1821 values of different types---the usefulness of this construct will be
1822 clear soon. In the literature this equality is known as `heterogeneous'
1823 or `John Major', since
1826 John Major's `classless society' widened people's aspirations to
1827 equality, but also the gap between rich and poor. After all, aspiring
1828 to be equal to others than oneself is the politics of envy. In much
1829 the same way, forms equations between members of any type, but they
1830 cannot be treated as equals (ie substituted) unless they are of the
1831 same type. Just as before, each thing is only equal to
1832 itself. \citep{McBride1999}.
1835 Correspondingly, at the term level, $\myfun{coe}$ (`coerce') lets us
1836 transport values between equal types; and $\myfun{coh}$ (`coherence')
1837 guarantees that $\myfun{coe}$ respects the value-level equality, or in
1838 other words that it really has no computational component: if we
1839 transport $\mytmm : \mytya$ to $\mytmn : \mytyb$, $\mytmm$ and $\mytmn$
1840 will still be the same.
1842 Before introducing the core ideas that make OTT work, let us distinguish
1843 between \emph{canonical} and \emph{neutral} types. Canonical types are
1844 those arising from the ground types ($\myempty$, $\myunit$, $\mybool$)
1845 and the three type formers ($\myarr$, $\myprod$, $\mytyc{W}$). Neutral
1846 types are those formed by
1847 $\myfun{If}\myarg\myfun{Then}\myarg\myfun{Else}\myarg$.
1848 Correspondingly, canonical terms are those inhabiting canonical types
1849 ($\mytt$, $\mytrue$, $\myfalse$, $\myabss{\myb{x}}{\mytya}{\mytmt}$,
1850 ...), and neutral terms those formed by eliminators.\footnote{Using the
1851 terminology from Section \ref{sec:types}, we'd say that canonical
1852 terms are in \emph{weak head normal form}.} In the current system
1853 (and hopefully in well-behaved systems), all closed terms reduce to a
1854 canonical term, and all canonical types are inhabited by canonical
1857 \subsubsection{Type equality, and coercions}
1859 The plan is to decompose type-level equalities between canonical types
1860 into decodable propositions containing equalities regarding the
1861 subterms, and to use coerce recursively on the subterms using the
1862 generated equalities. This interplay between type equalities and
1863 \myfun{coe} ensures that invocations of $\myfun{coe}$ will vanish when
1864 we have evidence of the structural equality of the types we are
1865 transporting terms across. If the type is neutral, the equality won't
1866 reduce and thus $\myfun{coe}$ won't reduce either. If we come an
1867 equality between different canonical types, then we reduce the equality
1868 to bottom, making sure that no such proof can exist, and providing an
1869 `escape hatch' in $\myfun{coe}$.
1873 \mydesc{equality reduction:}{\myprsyn \myred \myprsyn}{
1875 \begin{array}{c@{\ }c@{\ }c@{\ }l}
1876 \myempty & \myeq & \myempty & \myred \mytop \\
1877 \myunit & \myeq & \myunit & \myred \mytop \\
1878 \mybool & \myeq & \mybool & \myred \mytop \\
1879 \myexi{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myexi{\myb{x_2}}{\mytya_2}{\mytya_2} & \myred \\
1881 \myind{2} \mytya_1 \myeq \mytyb_1 \myand
1882 \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}]}
1884 \myfora{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myfora{\myb{x_2}}{\mytya_2}{\mytyb_2} & \myred \cdots \\
1885 \myw{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myw{\myb{x_2}}{\mytya_2}{\mytyb_2} & \myred \cdots \\
1886 \mytya & \myeq & \mytyb & \myred \mybot\ \text{if $\mytya$ and $\mytyb$ are canonical.}
1891 \mydesc{reduction}{\mytmsyn \myred \mytmsyn}{
1893 \begin{array}[t]{@{}l@{\ }l@{\ }l@{\ }l@{\ }l@{\ }c@{\ }l@{\ }}
1894 \mycoe & \myempty & \myempty & \myse{Q} & \myse{t} & \myred & \myse{t} \\
1895 \mycoe & \myunit & \myunit & \myse{Q} & \myse{t} & \myred & \mytt \\
1896 \mycoe & \mybool & \mybool & \myse{Q} & \mytrue & \myred & \mytrue \\
1897 \mycoe & \mybool & \mybool & \myse{Q} & \myfalse & \myred & \myfalse \\
1898 \mycoe & (\myexi{\myb{x_1}}{\mytya_1}{\mytyb_1}) &
1899 (\myexi{\myb{x_2}}{\mytya_2}{\mytyb_2}) & \myse{Q} &
1900 \mytmt_1 & \myred & \\
1902 \myind{2}\begin{array}[t]{l@{\ }l@{\ }c@{\ }l}
1903 \mysyn{let} & \myb{\mytmm_1} & \mapsto & \myapp{\myfst}{\mytmt_1} : \mytya_1 \\
1904 & \myb{\mytmn_1} & \mapsto & \myapp{\mysnd}{\mytmt_1} : \mysub{\mytyb_1}{\myb{x_1}}{\myb{\mytmm_1}} \\
1905 & \myb{Q_A} & \mapsto & \myapp{\myfst}{\myse{Q}} : \mytya_1 \myeq \mytya_2 \\
1906 & \myb{\mytmm_2} & \mapsto & \mycoee{\mytya_1}{\mytya_2}{\myb{Q_A}}{\myb{\mytmm_1}} : \mytya_2 \\
1907 & \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}}} \\
1908 & \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}} \\
1909 \mysyn{in} & \multicolumn{3}{@{}l}{\mypair{\myb{\mytmm_2}}{\myb{\mytmn_2}}}
1912 \mycoe & (\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}) &
1913 (\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}) & \myse{Q} &
1917 \mycoe & (\myw{\myb{x_1}}{\mytya_1}{\mytyb_1}) &
1918 (\myw{\myb{x_2}}{\mytya_2}{\mytyb_2}) & \myse{Q} &
1922 \mycoe & \mytya & \mytyb & \myse{Q} & \mytmt & \myred & \myapp{\myabsurd{\mytyb}}{\myse{Q}}\ \text{if $\mytya$ and $\mytyb$ are canonical.}
1926 \caption{Reducing type equalities, and using them when
1927 $\myfun{coe}$rcing.}
1931 Figure \ref{fig:eqred} illustrates this idea in practice. For ground
1932 types, the proof is the trivial element, and \myfun{coe} is the
1933 identity. For $\myunit$, we can do better: we return its only member
1934 without matching on the term. For the three type binders, things are
1935 similar but subtly different---the choices we make in the type equality
1936 are dictated by the desire of writing the $\myfun{coe}$ in a natural
1939 $\myprod$ is the easiest case: we decompose the proof into proofs that
1940 the first element's types are equal ($\mytya_1 \myeq \mytya_2$), and a
1941 proof that given equal values in the first element, the types of the
1942 second elements are equal too
1943 ($\myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{\myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2}}
1944 \myimpl \mytyb_1 \myeq \mytyb_2}$).\footnote{We are using $\myimpl$ to
1945 indicate a $\forall$ where we discard the first value. We write
1946 $\mytyb_1[\myb{x_1}]$ to indicate that the $\myb{x_1}$ in $\mytyb_1$
1947 is re-bound to the $\myb{x_1}$ quantified by the $\forall$, and
1948 similarly for $\myb{x_2}$ and $\mytyb_2$.} This also explains the
1949 need for heterogeneous equality, since in the second proof it would be
1950 awkward to express the fact that $\myb{A_1}$ is the same as $\myb{A_2}$.
1951 In the respective $\myfun{coe}$ case, since the types are canonical, we
1952 know at this point that the proof of equality is a pair of the shape
1953 described above. Thus, we can immediately coerce the first element of
1954 the pair using the first element of the proof, and then instantiate the
1955 second element with the two first elements and a proof by coherence of
1956 their equality, since we know that the types are equal.
1958 The cases for the other binders are omitted for brevity, but they follow
1959 the same principle with some twists to make $\myfun{coe}$ work with the
1960 generated proofs; the reader can refer to the paper for details.
1962 \subsubsection{$\myfun{coe}$, laziness, and $\myfun{coh}$erence}
1964 It is important to notice that in the reduction rules for $\myfun{coe}$
1965 are never obstructed by the proofs: with the exception of comparisons
1966 between different canonical types we never `pattern match' on the proof
1967 pairs, but always look at the projections. This means that, as long as
1968 we are consistent, and thus as long as we don't have $\mybot$-inducing
1969 proofs, we can add propositional axioms for equality and $\myfun{coe}$
1970 will still compute. Thus, we can take $\myfun{coh}$ as axiomatic, and
1971 we can add back familiar useful equality rules:
1973 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1974 \AxiomC{$\myjud{\mytmt}{\mytya}$}
1975 \UnaryInfC{$\myjud{\myapp{\myrefl}{\mytmt}}{\myprdec{\myjm{\mytmt}{\mytya}{\mytmt}{\mytya}}}$}
1980 \AxiomC{$\myjud{\mytya}{\mytyp}$}
1981 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytyb}{\mytyp}$}
1982 \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}}}}}$}
1986 $\myrefl$ is the equivalent of the reflexivity rule in propositional
1987 equality, and $\mytyc{R}$ asserts that if we have a we have a $\mytyp$
1988 abstracting over a value we can substitute equal for equal---this lets
1989 us recover $\myfun{subst}$. Note that while we need to provide ad-hoc
1990 rules in the restricted, non-hierarchical theory that we have, if our
1991 theory supports abstraction over $\mytyp$s we can easily add these
1992 axioms as abstracted variables.
1994 \subsubsection{Value-level equality}
1996 \mydesc{equality reduction:}{\myprsyn \myred \myprsyn}{
1998 \begin{array}{r@{ }c@{\ }c@{\ }c@{}l@{\ }c@{\ }r@{}c@{\ }c@{\ }c@{}l@{\ }l}
1999 (&\mytmt_1 & : & \myempty&) & \myeq & (&\mytmt_2 & : & \myempty &) & \myred \mytop \\
2000 (&\mytmt_1 & : & \myunit&) & \myeq & (&\mytmt_2 & : & \myunit&) & \myred \mytop \\
2001 (&\mytrue & : & \mybool&) & \myeq & (&\mytrue & : & \mybool&) & \myred \mytop \\
2002 (&\myfalse & : & \mybool&) & \myeq & (&\myfalse & : & \mybool&) & \myred \mytop \\
2003 (&\mytrue & : & \mybool&) & \myeq & (&\myfalse & : & \mybool&) & \myred \mybot \\
2004 (&\myfalse & : & \mybool&) & \myeq & (&\mytrue & : & \mybool&) & \myred \mybot \\
2005 (&\mytmt_1 & : & \myexi{\mytya_1}{\myb{x_1}}{\mytyb_1}&) & \myeq & (&\mytmt_2 & : & \myexi{\mytya_2}{\myb{x_2}}{\mytyb_2}&) & \myred \\
2006 & \multicolumn{11}{@{}l}{
2007 \myind{2} \myjm{\myapp{\myfst}{\mytmt_1}}{\mytya_1}{\myapp{\myfst}{\mytmt_2}}{\mytya_2} \myand
2008 \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}}}
2010 (&\myse{f}_1 & : & \myfora{\mytya_1}{\myb{x_1}}{\mytyb_1}&) & \myeq & (&\myse{f}_2 & : & \myfora{\mytya_2}{\myb{x_2}}{\mytyb_2}&) & \myred \\
2011 & \multicolumn{11}{@{}l}{
2012 \myind{2} \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{
2013 \myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2} \myimpl
2014 \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}]}
2017 (&\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 \\
2018 (&\mytmt_1 & : & \mytya_1&) & \myeq & (&\mytmt_2 & : & \mytya_2 &) & \myred \mybot\ \text{if $\mytya_1$ and $\mytya_2$ are canonical.}
2023 As with type-level equality, we want value-level equality to reduce
2024 based on the structure of the compared terms. When matching
2025 propositional data, such as $\myempty$ and $\myunit$, we automatically
2026 return the trivial type, since if a type has zero one members, all
2027 members will be equal. When matching on data-bearing types, such as
2028 $\mybool$, we check that such data matches, and return bottom otherwise.
2030 \subsection{Proof irrelevance and stuck coercions}
2031 \label{sec:ott-quot}
2033 The last effort is required to make sure that proofs (members of
2034 $\myprop$) are \emph{irrelevant}. Since they are devoid of
2035 computational content, we would like to identify all equivalent
2036 propositions as the same, in a similar way as we identified all
2037 $\myempty$ and all $\myunit$ as the same in section
2038 \ref{sec:eta-expand}.
2040 Thus we will have a quotation that will not only perform
2041 $\eta$-expansion, but will also identify and mark proofs that could not
2042 be decoded (that is, equalities on neutral types). Then, when
2043 comparing terms, marked proofs will be considered equal without
2044 analysing their contents, thus gaining irrelevance.
2046 Moreover we can safely advance `stuck' $\myfun{coe}$rcions between
2047 non-canonical but definitionally equal types. Consider for example
2049 \mycoee{(\myITE{\myb{b}}{\mynat}{\mybool})}{(\myITE{\myb{b}}{\mynat}{\mybool})}{\myb{x}}
2051 Where $\myb{b}$ and $\myb{x}$ are abstracted variables. This
2052 $\myfun{coe}$ will not advance, since the types are not canonical.
2053 However they are definitionally equal, and thus we can safely remove the
2054 coerce and return $\myb{x}$ as it is.
2056 \section{\mykant : the theory}
2057 \label{sec:kant-theory}
2059 \mykant\ is an interactive theorem prover developed as part of this thesis.
2060 The plan is to present a core language which would be capable of serving as
2061 the basis for a more featureful system, while still presenting interesting
2062 features and more importantly observational equality.
2064 We will first present the features of the system, and then describe the
2065 implementation we have developed in Section \ref{sec:kant-practice}.
2067 The defining features of \mykant\ are:
2070 \item[Full dependent types] As we would expect, we have dependent a system
2071 which is as expressive as the `best' corner in the lambda cube described in
2072 Section \ref{sec:itt}.
2074 \item[Implicit, cumulative universe hierarchy] The user does not need to
2075 specify universe level explicitly, and universes are \emph{cumulative}.
2077 \item[User defined data types and records] Instead of forcing the user to
2078 choose from a restricted toolbox, we let her define inductive data types,
2079 with associated primitive recursion operators; or records, with associated
2080 projections for each field.
2082 \item[Bidirectional type checking] While no `fancy' inference via
2083 unification is present, we take advantage of a type synthesis system
2084 in the style of \cite{Pierce2000}, extending the concept for user
2087 \item[Observational equality] As described in Section \ref{sec:ott} but
2088 extended to work with the type hierarchy and to admit equality between
2089 arbitrary data types.
2091 \item[Type holes] When building up programs interactively, it is useful
2092 to leave parts unfinished while exploring the current context. This
2093 is what type holes are for. We do not describe holes rigorously, but
2094 provide more information about them from the implementation and usage
2095 perspective in Section \ref{sec:type-holes}.
2099 We will analyse the features one by one, along with motivations and
2100 tradeoffs for the design decisions made.
2102 \subsection{Bidirectional type checking}
2104 We start by describing bidirectional type checking since it calls for
2105 fairly different typing rules that what we have seen up to now. The
2106 idea is to have two kinds of terms: terms for which a type can always be
2107 inferred, and terms that need to be checked against a type. A nice
2108 observation is that this duality runs through the semantics of the
2109 terms: neutral terms (abstracted or defined variables, function
2110 application, record projections, primitive recursors, etc.) \emph{infer}
2111 types, canonical terms (abstractions, record/data types data
2112 constructors, etc.) need to be \emph{checked}.
2114 To introduce the concept and notation, we will revisit the STLC in a
2115 bidirectional style. The presentation follows \cite{Loh2010}. The
2116 syntax for our bidirectional STLC is the same as the untyped
2117 $\lambda$-calculus, but with an extra construct to annotate terms
2118 explicitly---this will be necessary when having top-level canonical
2119 terms. The types are the same as those found in the normal STLC.
2123 \begin{array}{r@{\ }c@{\ }l}
2124 \mytmsyn & ::= & \myb{x} \mysynsep \myabs{\myb{x}}{\mytmsyn} \mysynsep (\myapp{\mytmsyn}{\mytmsyn}) \mysynsep (\mytmsyn : \mytysyn)
2128 We will have two kinds of typing judgements: \emph{inference} and
2129 \emph{checking}. $\myinf{\mytmt}{\mytya}$ indicates that $\mytmt$
2130 infers the type $\mytya$, while $\mychk{\mytmt}{\mytya}$ can be checked
2131 against type $\mytya$. The type of variables in context is inferred,
2132 and so are annotate terms. The type of applications is inferred too,
2133 propagating types down the applied term. Abstractions are checked.
2134 Finally, we have a rule to check the type of an inferrable term.
2136 \mydesc{typing:}{\myctx \vdash \mytmsyn \Updownarrow \mytmsyn}{
2138 \AxiomC{$\myctx(x) = A$}
2139 \UnaryInfC{$\myinf{\myb{x}}{A}$}
2142 \AxiomC{$\myjudd{\myctx;\myb{x} : A}{\mytmt}{\mytyb}$}
2143 \UnaryInfC{$\mychk{\myabs{x}{\mytmt}}{(\myb{x} {:} \mytya) \myarr \mytyb}$}
2149 \begin{tabular}{ccc}
2150 \AxiomC{$\myinf{\mytmm}{\mytya \myarr \mytyb}$}
2151 \AxiomC{$\mychk{\mytmn}{\mytya}$}
2152 \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mytyb}$}
2155 \AxiomC{$\mychk{\mytmt}{\mytya}$}
2156 \UnaryInfC{$\myinf{\myann{\mytmt}{\mytya}}{\mytya}$}
2159 \AxiomC{$\myinf{\mytmt}{\mytya}$}
2160 \UnaryInfC{$\myinf{\mytmt}{\mytya}$}
2165 For example, if we wanted to type function composition (in this case for
2166 naturals), we would have to annotate the term:
2168 \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
2170 But we would not have to annotate functions passed to it, since the type would be propagated to the arguments:
2172 \myfun{comp}\myappsp (\myabs{\myb{x}}{\myb{x} \mathrel{\myfun{$+$}} 3}) \myappsp (\myabs{\myb{x}}{\myb{x} \mathrel{\myfun{$*$}} 4}) \myappsp 42
2175 \subsection{Base terms and types}
2177 Let us begin by describing the primitives available without the user
2178 defining any data types, and without equality. The way we handle
2179 variables and substitution is left unspecified, and explained in section
2180 \ref{sec:term-repr}, along with other implementation issues. We are
2181 also going to give an account of the implicit type hierarchy separately
2182 in Section \ref{sec:term-hierarchy}, so as not to clutter derivation
2183 rules too much, and just treat types as impredicative for the time
2188 \begin{array}{r@{\ }c@{\ }l}
2189 \mytmsyn & ::= & \mynamesyn \mysynsep \mytyp \\
2190 & | & \myfora{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
2191 \myabs{\myb{x}}{\mytmsyn} \mysynsep
2192 (\myapp{\mytmsyn}{\mytmsyn}) \mysynsep
2193 (\myann{\mytmsyn}{\mytmsyn}) \\
2194 \mynamesyn & ::= & \myb{x} \mysynsep \myfun{f}
2199 The syntax for our calculus includes just two basic constructs:
2200 abstractions and $\mytyp$s. Everything else will be provided by
2201 user-definable constructs. Since we let the user define values, we will
2202 need a context capable of carrying the body of variables along with
2205 Bound names and defined names are treated separately in the syntax, and
2206 while both can be associated to a type in the context, only defined
2207 names can be associated with a body:
2209 \mydesc{context validity:}{\myvalid{\myctx}}{
2210 \begin{tabular}{ccc}
2211 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
2212 \UnaryInfC{$\myvalid{\myemptyctx}$}
2215 \AxiomC{$\myjud{\mytya}{\mytyp}$}
2216 \AxiomC{$\mynamesyn \not\in \myctx$}
2217 \BinaryInfC{$\myvalid{\myctx ; \mynamesyn : \mytya}$}
2220 \AxiomC{$\myjud{\mytmt}{\mytya}$}
2221 \AxiomC{$\myfun{f} \not\in \myctx$}
2222 \BinaryInfC{$\myvalid{\myctx ; \myfun{f} \mapsto \mytmt : \mytya}$}
2227 Now we can present the reduction rules, which are unsurprising. We have
2228 the usual function application ($\beta$-reduction), but also a rule to
2229 replace names with their bodies ($\delta$-reduction), and one to discard
2230 type annotations. For this reason reduction is done in-context, as
2231 opposed to what we have seen in the past:
2233 \mydesc{reduction:}{\myctx \vdash \mytmsyn \myred \mytmsyn}{
2234 \begin{tabular}{ccc}
2235 \AxiomC{\phantom{$\myb{x} \mapsto \mytmt : \mytya \in \myctx$}}
2236 \UnaryInfC{$\myctx \vdash \myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn}
2237 \myred \mysub{\mytmm}{\myb{x}}{\mytmn}$}
2240 \AxiomC{$\myfun{f} \mapsto \mytmt : \mytya \in \myctx$}
2241 \UnaryInfC{$\myctx \vdash \myfun{f} \myred \mytmt$}
2244 \AxiomC{\phantom{$\myb{x} \mapsto \mytmt : \mytya \in \myctx$}}
2245 \UnaryInfC{$\myctx \vdash \myann{\mytmm}{\mytya} \myred \mytmm$}
2250 We can now give types to our terms. Although we include the usual
2251 conversion rule, we defer a detailed account of definitional equality to
2252 Section \ref{sec:kant-irr}.
2254 \mydesc{typing:}{\myctx \vdash \mytmsyn \Updownarrow \mytmsyn}{
2255 \begin{tabular}{cccc}
2256 \AxiomC{$\myse{name} : A \in \myctx$}
2257 \UnaryInfC{$\myinf{\myse{name}}{A}$}
2260 \AxiomC{$\myfun{f} \mapsto \mytmt : A \in \myctx$}
2261 \UnaryInfC{$\myinf{\myfun{f}}{A}$}
2264 \AxiomC{$\mychk{\mytmt}{\mytya}$}
2265 \UnaryInfC{$\myinf{\myann{\mytmt}{\mytya}}{\mytya}$}
2268 \AxiomC{$\myinf{\mytmt}{\mytya}$}
2269 \AxiomC{$\myctx \vdash \mytya \mydefeq \mytyb$}
2270 \BinaryInfC{$\mychk{\mytmt}{\mytyb}$}
2278 \AxiomC{\phantom{$\mychkk{\myctx; \myb{x}: \mytya}{\mytmt}{\mytyb}$}}
2279 \UnaryInfC{$\myinf{\mytyp}{\mytyp}$}
2282 \AxiomC{$\myinf{\mytya}{\mytyp}$}
2283 \AxiomC{$\myinff{\myctx; \myb{x} : \mytya}{\mytyb}{\mytyp}$}
2284 \BinaryInfC{$\myinf{(\myb{x} {:} \mytya) \myarr \mytyb}{\mytyp}$}
2293 \AxiomC{$\myinf{\mytmm}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
2294 \AxiomC{$\mychk{\mytmn}{\mytya}$}
2295 \BinaryInfC{$\myinf{\myapp{\mytmm}{\mytmn}}{\mysub{\mytyb}{\myb{x}}{\mytmn}}$}
2300 \AxiomC{$\mychkk{\myctx; \myb{x}: \mytya}{\mytmt}{\mytyb}$}
2301 \UnaryInfC{$\mychk{\myabs{\myb{x}}{\mytmt}}{\myfora{\myb{x}}{\mytyb}{\mytyb}}$}
2307 \subsection{Elaboration}
2309 As we mentioned, $\mykant$\ allows the user to define not only values
2310 but also custom data types and records. \emph{Elaboration} consists of
2311 turning these declarations into workable syntax, types, and reduction
2312 rules. The treatment of custom types in $\mykant$\ is heavily inspired
2313 by McBride's and McKinna's early work on Epigram \citep{McBride2004},
2314 although with some differences.
2316 \subsubsection{Term vectors, telescopes, and assorted notation}
2318 We use a vector notation to refer to a series of term applied to
2319 another, for example $\mytyc{D} \myappsp \vec{A}$ is a shorthand for
2320 $\mytyc{D} \myappsp \mytya_1 \cdots \mytya_n$, for some $n$. $n$ is
2321 consistently used to refer to the length of such vectors, and $i$ to
2322 refer to an index in such vectors. We also often need to `build up'
2323 terms vectors, in which case we use $\myemptyctx$ for an empty vector
2324 and add elements to an existing vector with $\myarg ; \myarg$, similarly
2325 to what we do for contexts.
2327 To present the elaboration and operations on user defined data types, we
2328 frequently make use what de Bruijn called \emph{telescopes}
2329 \citep{Bruijn91}, a construct that will prove useful when dealing with
2330 the types of type and data constructors. A telescope is a series of
2331 nested typed bindings, such as $(\myb{x} {:} \mynat); (\myb{p} {:}
2332 \myapp{\myfun{even}}{\myb{x}})$. Consistent with the notation for
2333 contexts and term vectors, we use $\myemptyctx$ to denote an empty
2334 telescope and $\myarg ; \myarg$ to add a new binding to an existing
2337 We refer to telescopes with $\mytele$, $\mytele'$, $\mytele_i$, etc. If
2338 $\mytele$ refers to a telescope, $\mytelee$ refers to the term vector
2339 made up of all the variables bound by $\mytele$. $\mytele \myarr
2340 \mytya$ refers to the type made by turning the telescope into a series
2341 of $\myarr$. Returning to the examples above, we have that
2343 (\myb{x} {:} \mynat); (\myb{p} : \myapp{\myfun{even}}{\myb{x}}) \myarr \mynat =
2344 (\myb{x} {:} \mynat) \myarr (\myb{p} : \myapp{\myfun{even}}{\myb{x}}) \myarr \mynat
2347 We make use of various operations to manipulate telescopes:
2349 \item $\myhead(\mytele)$ refers to the first type appearing in
2350 $\mytele$: $\myhead((\myb{x} {:} \mynat); (\myb{p} :
2351 \myapp{\myfun{even}}{\myb{x}})) = \mynat$. Similarly,
2352 $\myix_i(\mytele)$ refers to the $i^{th}$ type in a telescope
2354 \item $\mytake_i(\mytele)$ refers to the telescope created by taking the
2355 first $i$ elements of $\mytele$: $\mytake_1((\myb{x} {:} \mynat); (\myb{p} :
2356 \myapp{\myfun{even}}{\myb{x}})) = (\myb{x} {:} \mynat)$.
2357 \item $\mytele \vec{A}$ refers to the telescope made by `applying' the
2358 terms in $\vec{A}$ on $\mytele$: $((\myb{x} {:} \mynat); (\myb{p} :
2359 \myapp{\myfun{even}}{\myb{x}}))42 = (\myb{p} :
2360 \myapp{\myfun{even}}{42})$.
2363 Additionally, when presenting syntax elaboration, I'll use $\mytmsyn^n$
2364 to indicate a term vector composed of $n$ elements, or
2365 $\mytmsyn^{\mytele}$ for one composed by as many elements as the
2368 \subsubsection{Declarations syntax}
2372 \begin{array}{r@{\ }c@{\ }l}
2373 \mydeclsyn & ::= & \myval{\myb{x}}{\mytmsyn}{\mytmsyn} \\
2374 & | & \mypost{\myb{x}}{\mytmsyn} \\
2375 & | & \myadt{\mytyc{D}}{\myappsp \mytelesyn}{}{\mydc{c} : \mytelesyn\ |\ \cdots } \\
2376 & | & \myreco{\mytyc{D}}{\myappsp \mytelesyn}{}{\myfun{f} : \mytmsyn,\ \cdots } \\
2378 \mytelesyn & ::= & \myemptytele \mysynsep \mytelesyn \mycc (\myb{x} {:} \mytmsyn) \\
2379 \mynamesyn & ::= & \cdots \mysynsep \mytyc{D} \mysynsep \mytyc{D}.\mydc{c} \mysynsep \mytyc{D}.\myfun{f}
2384 In \mykant\ we have four kind of declarations:
2387 \item[Defined value] A variable, together with a type and a body.
2388 \item[Abstract variable] An abstract variable, with a type but no body.
2389 \item[Inductive data] A datatype, with a type constructor and various
2390 data constructors, quite similar to what we find in Haskell. A
2391 primitive recursor (or `destructor') will be generated automatically.
2392 \item[Record] A record, which consists of one data constructor and various
2393 fields, with no recursive occurrences.
2396 Elaborating defined variables consists of type checking the body against
2397 the given type, and updating the context to contain the new binding.
2398 Elaborating abstract variables and abstract variables consists of type
2399 checking the type, and updating the context with a new typed variable:
2401 \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
2403 \AxiomC{$\mychk{\mytmt}{\mytya}$}
2404 \AxiomC{$\myfun{f} \not\in \myctx$}
2406 $\myctx \myelabt \myval{\myfun{f}}{\mytya}{\mytmt} \ \ \myelabf\ \ \myctx; \myfun{f} \mapsto \mytmt : \mytya$
2410 \AxiomC{$\mychk{\mytya}{\mytyp}$}
2411 \AxiomC{$\myfun{f} \not\in \myctx$}
2414 \myctx \myelabt \mypost{\myfun{f}}{\mytya}
2415 \ \ \myelabf\ \ \myctx; \myfun{f} : \mytya
2422 \subsubsection{User defined types}
2423 \label{sec:user-type}
2425 Elaborating user defined types is the real effort. First, we will
2426 explain what we can define, with some examples.
2429 \item[Natural numbers] To define natural numbers, we create a data type
2430 with two constructors: one with zero arguments ($\mydc{zero}$) and one
2431 with one recursive argument ($\mydc{suc}$):
2434 \myadt{\mynat}{ }{ }{
2435 \mydc{zero} \mydcsep \mydc{suc} \myappsp \mynat
2439 This is very similar to what we would write in Haskell:
2441 data Nat = Zero | Suc Nat
2443 Once the data type is defined, $\mykant$\ will generate syntactic
2444 constructs for the type and data constructors, so that we will have
2447 \begin{tabular}{ccc}
2448 \AxiomC{\phantom{$\mychk{\mytmt}{\mynat}$}}
2449 \UnaryInfC{$\myinf{\mynat}{\mytyp}$}
2452 \AxiomC{\phantom{$\mychk{\mytmt}{\mynat}$}}
2453 \UnaryInfC{$\myinf{\mytyc{\mynat}.\mydc{zero}}{\mynat}$}
2456 \AxiomC{$\mychk{\mytmt}{\mynat}$}
2457 \UnaryInfC{$\myinf{\mytyc{\mynat}.\mydc{suc} \myappsp \mytmt}{\mynat}$}
2461 While in Haskell (or indeed in Agda or Coq) data constructors are
2462 treated the same way as functions, in $\mykant$\ they are syntax, so
2463 for example using $\mytyc{\mynat}.\mydc{suc}$ on its own will give a
2464 syntax error. This is necessary so that we can easily infer the type
2465 of polymorphic data constructors, as we will see later.
2467 Moreover, each data constructor is prefixed by the type constructor
2468 name, since we need to retrieve the type constructor of a data
2469 constructor when type checking. This measure aids in the presentation
2470 of various features but it is not needed in the implementation, where
2471 we can have a dictionary to lookup the type constructor corresponding
2472 to each data constructor. When using data constructors in examples I
2473 will omit the type constructor prefix for brevity, in this case
2474 writing $\mydc{zero}$ instead of $\mynat.\mydc{suc}$ and $\mydc{suc}$ instead of
2475 $\mynat.\mydc{suc}$.
2477 Along with user defined constructors, $\mykant$\ automatically
2478 generates an \emph{eliminator}, or \emph{destructor}, to compute with
2479 natural numbers: If we have $\mytmt : \mynat$, we can destruct
2480 $\mytmt$ using the generated eliminator `$\mynat.\myfun{elim}$':
2483 \AxiomC{$\mychk{\mytmt}{\mynat}$}
2485 \myinf{\mytyc{\mynat}.\myfun{elim} \myappsp \mytmt}{
2487 \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}}
2491 $\mynat.\myfun{elim}$ corresponds to the induction principle for
2492 natural numbers: if we have a predicate on numbers ($\myb{P}$), and we
2493 know that predicate holds for the base case
2494 ($\myapp{\myb{P}}{\mydc{zero}}$) and for each inductive step
2495 ($\myfora{\myb{x}}{\mynat}{\myapp{\myb{P}}{\myb{x}} \myarr
2496 \myapp{\myb{P}}{(\myapp{\mydc{suc}}{\myb{x}})}}$), then $\myb{P}$
2497 holds for any number. As with the data constructors, we require the
2498 eliminator to be applied to the `destructed' element.
2500 While the induction principle is usually seen as a mean to prove
2501 properties about numbers, in the intuitionistic setting it is also a
2502 mean to compute. In this specific case $\mynat.\myfun{elim}$
2503 returns the base case if the provided number is $\mydc{zero}$, and
2504 recursively applies the inductive step if the number is a
2507 \begin{array}{@{}l@{}l}
2508 \mytyc{\mynat}.\myfun{elim} \myappsp \mydc{zero} & \myappsp \myse{P} \myappsp \myse{pz} \myappsp \myse{ps} \myred \myse{pz} \\
2509 \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})
2512 The Haskell equivalent would be
2514 elim :: Nat -> a -> (Nat -> a -> a) -> a
2515 elim Zero pz ps = pz
2516 elim (Suc n) pz ps = ps n (elim n pz ps)
2518 Which buys us the computational behaviour, but not the reasoning power,
2519 since we cannot express the notion of a predicate depending on $\mynat$,
2520 since the type system is far too weak.
2522 \item[Binary trees] Now for a polymorphic data type: binary trees, since
2523 lists are too similar to natural numbers to be interesting.
2526 \myadt{\mytree}{\myappsp (\myb{A} {:} \mytyp)}{ }{
2527 \mydc{leaf} \mydcsep \mydc{node} \myappsp (\myapp{\mytree}{\myb{A}}) \myappsp \myb{A} \myappsp (\myapp{\mytree}{\myb{A}})
2531 Now the purpose of constructors as syntax can be explained: what would
2532 the type of $\mydc{leaf}$ be? If we were to treat it as a `normal'
2533 term, we would have to specify the type parameter of the tree each
2534 time the constructor is applied:
2536 \begin{array}{@{}l@{\ }l}
2537 \mydc{leaf} & : \myfora{\myb{A}}{\mytyp}{\myapp{\mytree}{\myb{A}}} \\
2538 \mydc{node} & : \myfora{\myb{A}}{\mytyp}{\myapp{\mytree}{\myb{A}} \myarr \myb{A} \myarr \myapp{\mytree}{\myb{A}} \myarr \myapp{\mytree}{\myb{A}}}
2541 The problem with this approach is that creating terms is incredibly
2542 verbose and dull, since we would need to specify the type parameters
2543 each time. For example if we wished to create a $\mytree \myappsp
2544 \mynat$ with two nodes and three leaves, we would have to write
2546 \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)
2548 The redundancy of $\mynat$s is quite irritating. Instead, if we treat
2549 constructors as syntactic elements, we can `extract' the type of the
2550 parameter from the type that the term gets checked against, much like
2551 we get the type of abstraction arguments:
2555 \AxiomC{$\mychk{\mytya}{\mytyp}$}
2556 \UnaryInfC{$\mychk{\mydc{leaf}}{\myapp{\mytree}{\mytya}}$}
2559 \AxiomC{$\mychk{\mytmm}{\mytree \myappsp \mytya}$}
2560 \AxiomC{$\mychk{\mytmt}{\mytya}$}
2561 \AxiomC{$\mychk{\mytmm}{\mytree \myappsp \mytya}$}
2562 \TrinaryInfC{$\mychk{\mydc{node} \myappsp \mytmm \myappsp \mytmt \myappsp \mytmn}{\mytree \myappsp \mytya}$}
2566 Which enables us to write, much more concisely
2568 \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}
2570 We gain an annotation, but we lose the myriad of types applied to the
2571 constructors. Conversely, with the eliminator for $\mytree$, we can
2572 infer the type of the arguments given the type of the destructed:
2575 \AxiomC{$\myinf{\mytmt}{\myapp{\mytree}{\mytya}}$}
2577 \myinf{\mytree.\myfun{elim} \myappsp \mytmt}{
2579 (\myb{P} {:} \myapp{\mytree}{\mytya} \myarr \mytyp) \myarr \\
2580 \myapp{\myb{P}}{\mydc{leaf}} \myarr \\
2581 ((\myb{l} {:} \myapp{\mytree}{\mytya}) (\myb{x} {:} \mytya) (\myb{r} {:} \myapp{\mytree}{\mytya}) \myarr \myapp{\myb{P}}{\myb{l}} \myarr
2582 \myapp{\myb{P}}{\myb{r}} \myarr \myb{P} \myappsp (\mydc{node} \myappsp \myb{l} \myappsp \myb{x} \myappsp \myb{r})) \myarr \\
2583 \myapp{\myb{P}}{\mytmt}
2588 As expected, the eliminator embodies structural induction on trees.
2589 We have a base case for $\myb{P} \myappsp \mydc{leaf}$, and an
2590 inductive step that given two subtrees and the predicate applied to
2591 them we need to return the predicate applied to the tree formed by a
2592 node with the two subtrees as children.
2594 \item[Empty type] We have presented types that have at least one
2595 constructors, but nothing prevents us from defining types with
2596 \emph{no} constructors:
2597 \[\myadt{\mytyc{Empty}}{ }{ }{ }\]
2598 What shall the `induction principle' on $\mytyc{Empty}$ be? Does it
2599 even make sense to talk about induction on $\mytyc{Empty}$?
2600 $\mykant$\ does not care, and generates an eliminator with no `cases',
2601 and thus corresponding to the $\myfun{absurd}$ that we know and love:
2604 \AxiomC{$\myinf{\mytmt}{\mytyc{Empty}}$}
2605 \UnaryInfC{$\myinf{\myempty.\myfun{elim} \myappsp \mytmt}{(\myb{P} {:} \mytmt \myarr \mytyp) \myarr \myapp{\myb{P}}{\mytmt}}$}
2608 \item[Ordered lists] Up to this point, the examples shown are nothing
2609 new to the \{Haskell, SML, OCaml, functional\} programmer. However
2610 dependent types let us express much more than that. A useful example
2611 is the type of ordered lists. There are many ways to define such a
2612 thing, we will define our type to store the bounds of the list, making
2613 sure that $\mydc{cons}$ing respects that.
2615 First, using $\myunit$ and $\myempty$, we define a type expressing the
2616 ordering on natural numbers, $\myfun{le}$---`less or equal'.
2617 $\myfun{le}\myappsp \mytmm \myappsp \mytmn$ will be inhabited only if
2618 $\mytmm \le \mytmn$:
2621 \myfun{le} : \mynat \myarr \mynat \myarr \mytyp \\
2622 \myfun{le} \myappsp \myb{n} \mapsto \\
2623 \myind{2} \mynat.\myfun{elim} \\
2624 \myind{2}\myind{2} \myb{n} \\
2625 \myind{2}\myind{2} (\myabs{\myarg}{\mynat \myarr \mytyp}) \\
2626 \myind{2}\myind{2} (\myabs{\myarg}{\myunit}) \\
2627 \myind{2}\myind{2} (\myabs{\myb{n}\, \myb{f}\, \myb{m}}{
2628 \mynat.\myfun{elim} \myappsp \myb{m} \myappsp (\myabs{\myarg}{\mytyp}) \myappsp \myempty \myappsp (\myabs{\myb{m'}\, \myarg}{\myapp{\myb{f}}{\myb{m'}}})
2632 We return $\myunit$ if the scrutinised is $\mydc{zero}$ (every
2633 number in less or equal than zero), $\myempty$ if the first number is
2634 a $\mydc{suc}$cessor and the second a $\mydc{zero}$, and we recurse if
2635 they are both successors. Since we want the list to have possibly
2636 `open' bounds, for example for empty lists, we create a type for
2637 `lifted' naturals with a bottom (less than everything) and top
2638 (greater than everything) elements, along with an associated comparison
2642 \myadt{\mytyc{Lift}}{ }{ }{\mydc{bot} \mydcsep \mydc{lift} \myappsp \mynat \mydcsep \mydc{top}}\\
2643 \myfun{le'} : \mytyc{Lift} \myarr \mytyc{Lift} \myarr \mytyp\\
2644 \myfun{le'} \myappsp \myb{l_1} \mapsto \\
2645 \myind{2} \mytyc{Lift}.\myfun{elim} \\
2646 \myind{2}\myind{2} \myb{l_1} \\
2647 \myind{2}\myind{2} (\myabs{\myarg}{\mytyc{Lift} \myarr \mytyp}) \\
2648 \myind{2}\myind{2} (\myabs{\myarg}{\myunit}) \\
2649 \myind{2}\myind{2} (\myabs{\myb{n_1}\, \myb{n_2}}{
2650 \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
2652 \myind{2}\myind{2} (\myabs{\myb{n_1}\, \myb{n_2}}{
2653 \mytyc{Lift}.\myfun{elim} \myappsp \myb{l_2} \myappsp (\myabs{\myarg}{\mytyp}) \myappsp \myempty \myappsp (\myabs{\myarg}{\myempty}) \myappsp \myunit
2657 Finally, we can defined a type of ordered lists. The type is
2658 parametrised over two values representing the lower and upper bounds
2659 of the elements, as opposed to the type parameters that we are used
2660 to. Then, an empty list will have to have evidence that the bounds
2661 are ordered, and each time we add an element we require the list to
2662 have a matching lower bound:
2665 \myadt{\mytyc{OList}}{\myappsp (\myb{low}\ \myb{upp} {:} \mytyc{Lift})}{\\ \myind{2}}{
2666 \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})
2670 Note that in the $\mydc{cons}$ constructor we quantify over the first
2671 argument, which will determine the type of the following
2672 arguments---again something we cannot do in systems like Haskell. If
2673 we want we can then employ this structure to write and prove correct
2674 various sorting algorithms.\footnote{See this presentation by Conor
2676 \url{https://personal.cis.strath.ac.uk/conor.mcbride/Pivotal.pdf},
2677 and this blog post by the author:
2678 \url{http://mazzo.li/posts/AgdaSort.html}.}
2680 \item[Dependent products] Apart from $\mysyn{data}$, $\mykant$\ offers
2681 us another way to define types: $\mysyn{record}$. A record is a
2682 datatype with one constructor and `projections' to extract specific
2683 fields of the said constructor.
2685 For example, we can recover dependent products:
2688 \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}}}
2691 Here $\myfst$ and $\mysnd$ are the projections, with their respective
2692 types. Note that each field can refer to the preceding fields. A
2693 constructor will be automatically generated, under the name of
2694 $\mytyc{Prod}.\mydc{constr}$. Dually to data types, we will omit the
2695 type constructor prefix for record projections.
2697 Following the bidirectionality of the system, we have that projections
2698 (the destructors of the record) infer the type, while the constructor
2703 \AxiomC{$\mychk{\mytmm}{\mytya}$}
2704 \AxiomC{$\mychk{\mytmn}{\myapp{\mytyb}{\mytmm}}$}
2705 \BinaryInfC{$\mychk{\mytyc{Prod}.\mydc{constr} \myappsp \mytmm \myappsp \mytmn}{\mytyc{Prod} \myappsp \mytya \myappsp \mytyb}$}
2707 \UnaryInfC{\phantom{$\myinf{\myfun{snd} \myappsp \mytmt}{\mytyb \myappsp (\myfst \myappsp \mytmt)}$}}
2710 \AxiomC{$\myinf{\mytmt}{\mytyc{Prod} \myappsp \mytya \myappsp \mytyb}$}
2711 \UnaryInfC{$\myinf{\myfun{fst} \myappsp \mytmt}{\mytya}$}
2713 \UnaryInfC{$\myinf{\myfun{snd} \myappsp \mytmt}{\mytyb \myappsp (\myfst \myappsp \mytmt)}$}
2717 What we have is equivalent to ITT's dependent products.
2725 \mynamesyn ::= \cdots \mysynsep \mytyc{D} \mysynsep \mytyc{D}.\mydc{c} \mysynsep \mytyc{D}.\myfun{f}
2732 \mydesc{syntax elaboration:}{\mydeclsyn \myelabf \mytmsyn ::= \cdots}{
2735 \begin{array}{r@{\ }l}
2736 & \myadt{\mytyc{D}}{\mytele}{}{\cdots\ |\ \mydc{c}_n : \mytele_n } \\
2739 \begin{array}{r@{\ }c@{\ }l}
2740 \mytmsyn & ::= & \cdots \mysynsep \myapp{\mytyc{D}}{\mytmsyn^{\mytele}} \mysynsep \cdots \mysynsep
2741 \mytyc{D}.\mydc{c}_n \myappsp \mytmsyn^{\mytele_n} \mysynsep \mytyc{D}.\myfun{elim} \myappsp \mytmsyn \\
2749 \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
2754 \myinf{\mytele \myarr \mytyp}{\mytyp}\hspace{0.8cm}
2755 \mytyc{D} \not\in \myctx \\
2756 \myinff{\myctx;\ \mytyc{D} : \mytele \myarr \mytyp}{\mytele \mycc \mytele_i \myarr \myapp{\mytyc{D}}{\mytelee}}{\mytyp}\ \ \ (1 \leq i \leq n) \\
2757 \text{For each $(\myb{x} {:} \mytya)$ in each $\mytele_i$, if $\mytyc{D} \in \mytya$, then $\mytya = \myapp{\mytyc{D}}{\vec{\mytmt}}$.}
2761 \begin{array}{r@{\ }c@{\ }l}
2762 \myctx & \myelabt & \myadt{\mytyc{D}}{\mytele}{}{ \cdots \ |\ \mydc{c}_n : \mytele_n } \\
2763 & & \vspace{-0.2cm} \\
2764 & \myelabf & \myctx;\ \mytyc{D} : \mytele \myarr \mytyp;\ \cdots;\ \mytyc{D}.\mydc{c}_n : \mytele \mycc \mytele_n \myarr \myapp{\mytyc{D}}{\mytelee}; \\
2766 \begin{array}{@{}r@{\ }l l}
2767 \mytyc{D}.\myfun{elim} : & \mytele \myarr (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr & \textbf{target} \\
2768 & (\myb{P} {:} \myapp{\mytyc{D}}{\mytelee} \myarr \mytyp) \myarr & \textbf{motive} \\
2772 (\mytele_n \mycc \myhyps(\myb{P}, \mytele_n) \myarr \myapp{\myb{P}}{(\myapp{\mytyc{D}.\mydc{c}_n}{\mytelee_n})}) \myarr
2773 \end{array} \right \}
2774 & \textbf{methods} \\
2775 & \myapp{\myb{P}}{\myb{x}} &
2779 \DisplayProof \\ \vspace{0.2cm}\ \\
2781 \begin{array}{@{}l l@{\ } l@{} r c l}
2782 \textbf{where} & \myhyps(\myb{P}, & \myemptytele &) & \mymetagoes & \myemptytele \\
2783 & \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) \\
2784 & \myhyps(\myb{P}, & (\myb{x} {:} \mytya) \mycc \mytele & ) & \mymetagoes & \myhyps(\myb{P}, \mytele)
2792 \mydesc{reduction elaboration:}{\mydeclsyn \myelabf \myctx \vdash \mytmsyn \myred \mytmsyn}{
2794 $\myadt{\mytyc{D}}{\mytele}{}{ \cdots \ |\ \mydc{c}_n : \mytele_n } \ \ \myelabf$
2795 \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
2796 \AxiomC{$\mytyc{D}.\mydc{c}_i : \mytele;\mytele_i \myarr \myapp{\mytyc{D}}{\mytelee} \in \myctx$}
2798 \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)}
2800 \DisplayProof \\ \vspace{0.2cm}\ \\
2802 \begin{array}{@{}l l@{\ } l@{} r c l}
2803 \textbf{where} & \myrecs(\myse{P}, \vec{m}, & \myemptytele &) & \mymetagoes & \myemptytele \\
2804 & \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) \\
2805 & \myrecs(\myse{P}, \vec{m}, & (\myb{x} {:} \mytya); \mytele &) & \mymetagoes & \myrecs(\myse{P}, \vec{m}, \mytele)
2812 \mydesc{syntax elaboration:}{\myelab{\mydeclsyn}{\mytmsyn ::= \cdots}}{
2815 \begin{array}{r@{\ }c@{\ }l}
2816 \myctx & \myelabt & \myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \\
2819 \begin{array}{r@{\ }c@{\ }l}
2820 \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 \\
2828 \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
2832 \myinf{\mytele \myarr \mytyp}{\mytyp}\hspace{0.8cm}
2833 \mytyc{D} \not\in \myctx \\
2834 \myinff{\myctx; \mytele; (\myb{f}_j : \myse{F}_j)_{j=1}^{i - 1}}{F_i}{\mytyp} \myind{3} (1 \le i \le n)
2838 \begin{array}{r@{\ }c@{\ }l}
2839 \myctx & \myelabt & \myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \\
2840 & & \vspace{-0.2cm} \\
2841 & \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}; \\
2842 & & \mytyc{D}.\mydc{constr} : \mytele \myarr \myse{F}_1 \myarr \cdots \myarr \myse{F}_n \myarr \myapp{\mytyc{D}}{\mytelee};
2850 \mydesc{reduction elaboration:}{\mydeclsyn \myelabf \myctx \vdash \mytmsyn \myred \mytmsyn}{
2852 $\myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \ \ \myelabf$
2853 \AxiomC{$\mytyc{D} \in \myctx$}
2854 \UnaryInfC{$\myctx \vdash \myapp{\mytyc{D}.\myfun{f}_i}{(\mytyc{D}.\mydc{constr} \myappsp \vec{t})} \myred t_i$}
2858 \caption{Elaboration for data types and records.}
2862 Following the intuition given by the examples, the mechanised
2863 elaboration is presented in Figure \ref{fig:elab}, which is essentially
2864 a modification of Figure 9 of \citep{McBride2004}\footnote{However, our
2865 datatypes do not have indices, we do bidirectional typechecking by
2866 treating constructors/destructors as syntactic constructs, and we have
2869 In data type declarations we allow recursive occurrences as long as
2870 they are \emph{strictly positive}, employing a syntactic check to make
2871 sure that this is the case. See \cite{Dybjer1991} for a more formal
2872 treatment of inductive definitions in ITT.
2874 For what concerns records, recursive occurrences are disallowed. The
2875 reason for this choice is answered by the reason for the choice of
2876 having records at all: we need records to give the user types with
2877 $\eta$-laws for equality, as we saw in Section \ref{sec:eta-expand}
2878 and in the treatment of OTT in Section \ref{sec:ott}. If we tried to
2879 $\eta$-expand recursive data types, we would expand forever.
2881 To implement bidirectional type checking for constructors and
2882 destructors, we store their types in full in the context, and then
2883 instantiate when due:
2885 \mydesc{typing:}{\myctx \vdash \mytmsyn \Leftrightarrow \mytmsyn}{
2888 \mytyc{D} : \mytele \myarr \mytyp \in \myctx \hspace{1cm}
2889 \mytyc{D}.\mydc{c} : \mytele \mycc \mytele' \myarr
2890 \myapp{\mytyc{D}}{\mytelee} \in \myctx \\
2891 \mytele'' = (\mytele;\mytele')\vec{A} \hspace{1cm}
2892 \mychkk{\myctx; \mytake_{i-1}(\mytele'')}{t_i}{\myix_i( \mytele'')}\ \
2893 (1 \le i \le \mytele'')
2896 \UnaryInfC{$\mychk{\myapp{\mytyc{D}.\mydc{c}}{\vec{t}}}{\myapp{\mytyc{D}}{\vec{A}}}$}
2901 \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
2902 \AxiomC{$\mytyc{D}.\myfun{f} : \mytele \mycc (\myb{x} {:}
2903 \myapp{\mytyc{D}}{\mytelee}) \myarr \myse{F}$}
2904 \AxiomC{$\myjud{\mytmt}{\myapp{\mytyc{D}}{\vec{A}}}$}
2905 \TrinaryInfC{$\myinf{\myapp{\mytyc{D}.\myfun{f}}{\mytmt}}{(\mytele
2906 \mycc (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr
2907 \myse{F})(\vec{A};\mytmt)}$}
2911 \subsubsection{Why user defined types? Why eliminators?}
2913 The hardest design choice when designing $\mykant$\ was to decide
2914 whether user defined types should be included, and how to handle them.
2915 In the end, as we saw, we can devise general structures like $\mytyc{W}$
2916 that can express all inductive structures. However, using those tools
2917 beyond very simple examples is near-impossible for a human user. Thus
2918 all theorem provers in use provide some mean for the user to define
2919 structures tailored to specific uses.
2921 Even if we take user defined data types for granted, there are two broad
2922 schools of thought regarding how to manipulate them:
2924 \item[Fixed points and pattern matching] The road chose by Agda and Coq.
2925 Functions are written like in Haskell---matching on the input and with
2926 explicit recursion. An external check on the recursive arguments
2927 ensures that they are decreasing, and thus that all functions
2928 terminate. This approach is the best in terms of user usability, but
2929 it is tricky to implement correctly.
2931 \item[Elaboration into eliminators] The road chose by \mykant, and
2932 pioneered by the Epigram line of work. The advantage is that we can
2933 reduce every data type to simple definitions which guarantee
2934 termination and are simple to reduce and type. It is however more
2935 cumbersome to use than pattern maching, although \cite{McBride2004}
2936 has shown how to implement a pattern matching interface on top of a
2937 larger set of combinators of those provided by \mykant.
2940 We chose the safer and easier to implement path, given the time
2941 constraints and the higher confidence of correctness. See also Section
2942 \ref{sec:future-work} for a brief overview of ways to extend or treat
2945 \subsection{Cumulative hierarchy and typical ambiguity}
2946 \label{sec:term-hierarchy}
2948 Having a well founded type hierarchy is crucial if we want to retain
2949 consistency, otherwise we can break our type systems by proving bottom,
2950 as shown in Appendix \ref{app:hurkens}.
2952 However, hierarchy as presented in section \label{sec:itt} is a
2953 considerable burden on the user, on various levels. Consider for
2954 example how we recovered disjunctions in Section \ref{sec:disju}: we
2955 have a function that takes two $\mytyp_0$ and forms a new $\mytyp_0$.
2956 What if we wanted to form a disjunction containing something a
2957 $\mytyp_1$, or $\mytyp_{42}$? Our definition would fail us, since
2958 $\mytyp_1 : \mytyp_2$.
2962 \mydesc{cumulativity:}{\myctx \vdash \mytmsyn \mycumul \mytmsyn}{
2963 \begin{tabular}{ccc}
2964 \AxiomC{$\myctx \vdash \mytya \mydefeq \mytyb$}
2965 \UnaryInfC{$\myctx \vdash \mytya \mycumul \mytyb$}
2968 \AxiomC{\phantom{$\myctx \vdash \mytya \mydefeq \mytyb$}}
2969 \UnaryInfC{$\myctx \vdash \mytyp_l \mycumul \mytyp_{l+1}$}
2972 \AxiomC{$\myctx \vdash \mytya \mycumul \mytyb$}
2973 \AxiomC{$\myctx \vdash \mytyb \mycumul \myse{C}$}
2974 \BinaryInfC{$\myctx \vdash \mytya \mycumul \myse{C}$}
2980 \begin{tabular}{ccc}
2981 \AxiomC{$\myjud{\mytmt}{\mytya}$}
2982 \AxiomC{$\myctx \vdash \mytya \mycumul \mytyb$}
2983 \BinaryInfC{$\myjud{\mytmt}{\mytyb}$}
2986 \AxiomC{$\myctx \vdash \mytya_1 \mydefeq \mytya_2$}
2987 \AxiomC{$\myctx; \myb{x} : \mytya_1 \vdash \mytyb_1 \mycumul \mytyb_2$}
2988 \BinaryInfC{$\myctx (\myb{x} {:} \mytya_1) \myarr \mytyb_1 \mycumul (\myb{x} {:} \mytya_2) \myarr \mytyb_2$}
2992 \caption{Cumulativity rules for base types in \mykant, plus a
2993 `conversion' rule for cumulative types.}
2994 \label{fig:cumulativity}
2997 One way to solve this issue is a \emph{cumulative} hierarchy, where
2998 $\mytyp_{l_1} : \mytyp_{l_2}$ iff $l_1 < l_2$. This way we retain
2999 consistency, while allowing for `large' definitions that work on small
3000 types too. Figure \ref{fig:cumulativity} gives a formal definition of
3001 cumulativity for types, abstractions, and data constructors.
3003 For example we might define our disjunction to be
3005 \myarg\myfun{$\vee$}\myarg : \mytyp_{100} \myarr \mytyp_{100} \myarr \mytyp_{100}
3007 And hope that $\mytyp_{100}$ will be large enough to fit all the types
3008 that we want to use with our disjunction. However, there are two
3009 problems with this. First, there is the obvious clumsyness of having to
3010 manually specify the size of types. More importantly, if we want to use
3011 $\myfun{$\vee$}$ itself as an argument to other type-formers, we need to
3012 make sure that those allow for types at least as large as
3015 A better option is to employ a mechanised version of what Russell called
3016 \emph{typical ambiguity}: we let the user live under the illusion that
3017 $\mytyp : \mytyp$, but check that the statements about types are
3018 consistent under the hood. $\mykant$\ implements this following the
3019 lines of \cite{Huet1988}. See also \citep{Harper1991} for a published
3020 reference, although describing a more complex system allowing for both
3021 explicit and explicit hierarchy at the same time.
3023 We define a partial ordering on the levels, with both weak ($\le$) and
3024 strong ($<$) constraints---the laws governing them being the same as the
3025 ones governing $<$ and $\le$ for the natural numbers. Each occurrence
3026 of $\mytyp$ is decorated with a unique reference, and we keep a set of
3027 constraints and add new constraints as we type check, generating new
3028 references when needed.
3030 For example, when type checking the type $\mytyp\, r_1$, where $r_1$
3031 denotes the unique reference assigned to that term, we will generate a
3032 new fresh reference $\mytyp\, r_2$, and add the constraint $r_1 < r_2$
3033 to the set. When type checking $\myctx \vdash
3034 \myfora{\myb{x}}{\mytya}{\mytyb}$, if $\myctx \vdash \mytya : \mytyp\,
3035 r_1$ and $\myctx; \myb{x} : \mytyb \vdash \mytyb : \mytyp\,r_2$; we will
3036 generate new reference $r$ and add $r_1 \le r$ and $r_2 \le r$ to the
3039 If at any point the constraint set becomes inconsistent, type checking
3040 fails. Moreover, when comparing two $\mytyp$ terms we equate their
3041 respective references with two $\le$ constraints---the details are
3042 explained in Section \ref{sec:hier-impl}.
3044 Another more flexible but also more verbose alternative is the one
3045 chosen by Agda, where levels can be quantified so that the relationship
3046 between arguments and result in type formers can be explicitly
3049 \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}
3051 Inference algorithms to automatically derive this kind of relationship
3052 are currently subject of research. We chose less flexible but more
3053 concise way, since it is easier to implement and better understood.
3055 \subsection{Observational equality, \mykant\ style}
3057 There are two correlated differences between $\mykant$\ and the theory
3058 used to present OTT. The first is that in $\mykant$ we have a type
3059 hierarchy, which lets us, for example, abstract over types. The second
3060 is that we let the user define inductive types.
3062 Reconciling propositions for OTT and a hierarchy had already been
3063 investigated by Conor McBride,\footnote{See
3064 \url{http://www.e-pig.org/epilogue/index.html?p=1098.html}.} and we
3065 follow his broad design plan, although with some modifications. Most of
3066 the work, as an extension of elaboration, is to handle reduction rules
3067 and coercions for data types---both type constructors and data
3070 \subsubsection{The \mykant\ prelude, and $\myprop$ositions}
3072 Before defining $\myprop$, we define some basic types inside $\mykant$,
3073 as the target for the $\myprop$ decoder:
3076 \myadt{\mytyc{Empty}}{}{ }{ } \\
3077 \myfun{absurd} : (\myb{A} {:} \mytyp) \myarr \mytyc{Empty} \myarr \myb{A} \mapsto \\
3078 \myind{2} \myabs{\myb{A\ \myb{bot}}}{\mytyc{Empty}.\myfun{elim} \myappsp \myb{bot} \myappsp (\myabs{\_}{\myb{A}})} \\
3081 \myreco{\mytyc{Unit}}{}{}{ } \\ \ \\
3083 \myreco{\mytyc{Prod}}{\myappsp (\myb{A}\ \myb{B} {:} \mytyp)}{ }{\myfun{fst} : \myb{A}, \myfun{snd} : \myb{B} }
3086 When using $\mytyc{Prod}$, we shall use $\myprod$ to define `nested'
3087 products, and $\myproj{n}$ to project elements from them, so that
3090 \mytya \myprod \mytyb = \mytyc{Prod} \myappsp \mytya \myappsp (\mytyc{Prod} \myappsp \mytyb \myappsp \myunit) \\
3091 \mytya \myprod \mytyb \myprod \myse{C} = \mytyc{Prod} \myappsp \mytya \myappsp (\mytyc{Prod} \myappsp \mytyb \myappsp (\mytyc{Prod} \myappsp \mytyc \myappsp \myunit)) \\
3093 \myproj{1} : \mytyc{Prod} \myappsp \mytya \myappsp \mytyb \myarr \mytya \\
3094 \myproj{2} : \mytyc{Prod} \myappsp \mytya \myappsp (\mytyc{Prod} \myappsp \mytyb \myappsp \myse{C}) \myarr \mytyb \\
3098 And so on, so that $\myproj{n}$ will work with all products with at
3099 least than $n$ elements. Then we can define propositions, and decoding:
3103 \begin{array}{r@{\ }c@{\ }l}
3104 \mytmsyn & ::= & \cdots \mysynsep \myprdec{\myprsyn} \\
3105 \myprsyn & ::= & \mybot \mysynsep \mytop \mysynsep \myprsyn \myand \myprsyn \mysynsep \myprfora{\myb{x}}{\mytmsyn}{\myprsyn}
3110 \mydesc{proposition decoding:}{\myprdec{\mytmsyn} \myred \mytmsyn}{
3113 \begin{array}{l@{\ }c@{\ }l}
3114 \myprdec{\mybot} & \myred & \myempty \\
3115 \myprdec{\mytop} & \myred & \myunit
3120 \begin{array}{r@{ }c@{ }l@{\ }c@{\ }l}
3121 \myprdec{&\myse{P} \myand \myse{Q} &} & \myred & \myprdec{\myse{P}} \myprod \myprdec{\myse{Q}} \\
3122 \myprdec{&\myprfora{\myb{x}}{\mytya}{\myse{P}} &} & \myred &
3123 \myfora{\myb{x}}{\mytya}{\myprdec{\myse{P}}}
3129 Adopting the same convention as with $\mytyp$-level products, we will
3130 nest $\myand$ in the same way.
3132 \subsubsection{Some OTT examples}
3134 Before presenting the direction that $\mykant$\ takes, let us consider
3135 some examples of use-defined data types, and the result we would expect,
3136 given what we already know about OTT, assuming the same propositional
3141 \item[Product types] Let's consider first the already mentioned
3142 dependent product, using the alternate name $\mysigma$\footnote{For
3143 extra confusion, `dependent products' are often called `dependent
3144 sums' in the literature, referring to the interpretation that
3145 identifies the first element as a `tag' deciding the type of the
3146 second element, which lets us recover sum types (disjuctions), as we
3147 saw in Section \ref{sec:depprod}. Thus, $\mysigma$.} to
3148 avoid confusion with the $\mytyc{Prod}$ in the prelude:
3151 \myreco{\mysigma}{\myappsp (\myb{A} {:} \mytyp) \myappsp (\myb{B} {:} \myb{A} \myarr \mytyp)}{\\ \myind{2}}{\myfst : \myb{A}, \mysnd : \myapp{\myb{B}}{\myb{fst}}}
3154 Let's start with type-level equality. The result we want is
3157 \mysigma \myappsp \mytya_1 \myappsp \mytyb_1 \myeq \mysigma \myappsp \mytya_2 \myappsp \mytyb_2 \myred \\
3158 \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}}}
3161 The difference here is that in the original presentation of OTT
3162 the type binders are explicit, while here $\mytyb_1$ and $\mytyb_2$ are
3163 functions returning types. We can do this thanks to the type
3164 hierarchy, and this hints at the fact that heterogeneous equality will
3165 have to allow $\mytyp$ `to the right of the colon', and in fact this
3166 provides the solution to simplify the equality above.
3168 If we take, just like we saw previously in OTT
3171 \myjm{\myse{f}_1}{\myfora{\mytya_1}{\myb{x_1}}{\mytyb_1}}{\myse{f}_2}{\myfora{\mytya_2}{\myb{x_2}}{\mytyb_2}} \myred \\
3172 \myind{2} \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{
3173 \myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2} \myimpl
3174 \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}]}
3178 Then we can simply take
3181 \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}
3184 Which will reduce to precisely what we desire. For what
3185 concerns coercions and quotation, things stay the same (apart from the
3186 fact that we apply to the second argument instead of substituting).
3187 We can recognise records such as $\mysigma$ as such and employ
3188 projections in value equality and coercions; as to not
3189 impede progress if not necessary.
3191 \item[Lists] Now for finite lists, which will give us a taste for data
3195 \myadt{\mylist}{\myappsp (\myb{A} {:} \mytyp)}{ }{\mydc{nil} \mydcsep \mydc{cons} \myappsp \myb{A} \myappsp (\myapp{\mylist}{\myb{A}})}
3198 Type equality is simple---we only need to compare the parameter:
3200 \mylist \myappsp \mytya_1 \myeq \mylist \myappsp \mytya_2 \myred \mytya_1 \myeq \mytya_2
3202 For coercions, we transport based on the constructor, recycling the
3203 proof for the inductive occurrence:
3205 \begin{array}{@{}l@{\ }c@{\ }l}
3206 \mycoe \myappsp (\mylist \myappsp \mytya_1) \myappsp (\mylist \myappsp \mytya_2) \myappsp \myse{Q} \myappsp \mydc{nil} & \myred & \mydc{nil} \\
3207 \mycoe \myappsp (\mylist \myappsp \mytya_1) \myappsp (\mylist \myappsp \mytya_2) \myappsp \myse{Q} \myappsp (\mydc{cons} \myappsp \mytmm \myappsp \mytmn) & \myred & \\
3208 \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)}
3211 Value equality is unsurprising---we match the constructors, and
3212 return bottom for mismatches. However, we also need to equate the
3213 parameter in $\mydc{nil}$:
3215 \begin{array}{r@{ }c@{\ }c@{\ }c@{}l@{\ }c@{\ }r@{}c@{\ }c@{\ }c@{}l@{\ }l}
3216 (& \mydc{nil} & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{nil} & : & \myapp{\mylist}{\mytya_2} &) \myred \mytya_1 \myeq \mytya_2 \\
3217 (& \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 \\
3218 & \multicolumn{11}{@{}l}{ \myind{2}
3219 \myjm{\mytmm_1}{\mytya_1}{\mytmm_2}{\mytya_2} \myand \myjm{\mytmn_1}{\myapp{\mylist}{\mytya_1}}{\mytmn_2}{\myapp{\mylist}{\mytya_2}}
3221 (& \mydc{nil} & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{cons} \myappsp \mytmm_2 \myappsp \mytmn_2 & : & \myapp{\mylist}{\mytya_2} &) \myred \mybot \\
3222 (& \mydc{cons} \myappsp \mytmm_1 \myappsp \mytmn_1 & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{nil} & : & \myapp{\mylist}{\mytya_2} &) \myred \mybot
3228 Now for something useless but complicated.
3232 \subsubsection{Only one equality}
3234 Given the examples above, a more `flexible' heterogeneous emerged, since
3235 of the fact that in $\mykant$ we re-gain the possibility of abstracting
3236 and in general handling sets in a way that was not possible in the
3237 original OTT presentation. Moreover, we found that the rules for value
3238 equality work very well if used with user defined type
3239 abstractions---for example in the case of dependent products we recover
3240 the original definition with explicit binders, in a very simple manner.
3242 In fact, we can drop a separate notion of type-equality, which will
3243 simply be served by $\myjm{\mytya}{\mytyp}{\mytyb}{\mytyp}$, from now on
3244 abbreviated as $\mytya \myeq \mytyb$. We shall still distinguish
3245 equalities relating types for hierarchical purposes. The full rules for
3246 equality reductions, along with the syntax for propositions, are given
3247 in figure \ref{fig:kant-eq-red}. We exploit record to perform
3248 $\eta$-expansion. Moreover, given the nested $\myand$s, values of data
3249 types with zero constructors (such as $\myempty$) and records with zero
3250 destructors (such as $\myunit$) will be automatically always identified
3257 \begin{array}{r@{\ }c@{\ }l}
3258 \myprsyn & ::= & \cdots \mysynsep \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
3263 % \mytmsyn & ::= & \cdots \mysynsep \mycoee{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \mysynsep
3264 % \mycohh{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
3265 % \myprsyn & ::= & \cdots \mysynsep \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
3269 % \mydesc{typing:}{\myctx \vdash \mytmsyn \Leftrightarrow \mytmsyn}{
3271 % \begin{tabular}{cc}
3272 % \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
3273 % \AxiomC{$\myjud{\mytmt}{\mytya}$}
3274 % \BinaryInfC{$\myinf{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}$}
3277 % \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
3278 % \AxiomC{$\myjud{\mytmt}{\mytya}$}
3279 % \BinaryInfC{$\myinf{\mycohh{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\myprdec{\myjm{\mytmt}{\mytya}{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}}}$}
3286 \mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
3289 \AxiomC{\phantom{$\myjud{\myse{P}}{\myprop}$}}
3290 \UnaryInfC{$\myjud{\mytop}{\myprop}$}
3292 \UnaryInfC{$\myjud{\mybot}{\myprop}$}
3295 \AxiomC{$\myjud{\myse{P}}{\myprop}$}
3296 \AxiomC{$\myjud{\myse{Q}}{\myprop}$}
3297 \BinaryInfC{$\myjud{\myse{P} \myand \myse{Q}}{\myprop}$}
3299 \UnaryInfC{\phantom{$\myjud{\mybot}{\myprop}$}}
3308 \phantom{\myjud{\myse{A}}{\mytyp} \hspace{0.8cm} \myjud{\mytmm}{\myse{A}}} \\
3309 \myjud{\myse{A}}{\mytyp}\hspace{0.8cm}
3310 \myjudd{\myctx; \myb{x} : \mytya}{\myse{P}}{\myprop}
3313 \UnaryInfC{$\myjud{\myprfora{\myb{x}}{\mytya}{\myse{P}}}{\myprop}$}
3318 \myjud{\myse{A}}{\mytyp} \hspace{0.8cm} \myjud{\mytmm}{\myse{A}} \\
3319 \myjud{\myse{B}}{\mytyp} \hspace{0.8cm} \myjud{\mytmn}{\myse{B}}
3322 \UnaryInfC{$\myjud{\myjm{\mytmm}{\myse{A}}{\mytmn}{\myse{B}}}{\myprop}$}
3329 \mydesc{equality reduction:}{\myctx \vdash \myprsyn \myred \myprsyn}{
3333 \UnaryInfC{$\myctx \vdash \myjm{\mytyp}{\mytyp}{\mytyp}{\mytyp} \myred \mytop$}
3337 \UnaryInfC{$\myctx \vdash \myjm{\myprdec{\myse{P}}}{\mytyp}{\myprdec{\myse{Q}}}{\mytyp} \myred \mytop$}
3345 \begin{array}{@{}r@{\ }l}
3347 \myjm{\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}}{\mytyp}{\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}}{\mytyp} \myred \\
3348 & \myind{2} \mytya_2 \myeq \mytya_1 \myand \myprfora{\myb{x_2}}{\mytya_2}{\myprfora{\myb{x_1}}{\mytya_1}{
3349 \myjm{\myb{x_2}}{\mytya_2}{\myb{x_1}}{\mytya_1} \myimpl \mytyb_1[\myb{x_1}] \myeq \mytyb_2[\myb{x_2}]
3359 \begin{array}{@{}r@{\ }l}
3361 \myjm{\myse{f}_1}{\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}}{\myse{f}_2}{\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}} \myred \\
3362 & \myind{2} \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{
3363 \myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2} \myimpl
3364 \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}]}
3373 \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
3375 \begin{array}{r@{\ }l}
3377 \myjm{\mytyc{D} \myappsp \vec{A}}{\mytyp}{\mytyc{D} \myappsp \vec{B}}{\mytyp} \myred \\
3378 & \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}))})
3387 \mydataty(\mytyc{D}, \myctx)\hspace{0.8cm}
3388 \mytyc{D}.\mydc{c} : \mytele;\mytele' \myarr \mytyc{D} \myappsp \mytelee \in \myctx \hspace{0.8cm}
3389 \mytele_A = (\mytele;\mytele')\vec{A}\hspace{0.8cm}
3390 \mytele_B = (\mytele;\mytele')\vec{B}
3394 \begin{array}{@{}l@{\ }l}
3395 \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 \\
3396 & \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}))})
3403 \AxiomC{$\mydataty(\mytyc{D}, \myctx)$}
3405 \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
3413 \myisreco(\mytyc{D}, \myctx)\hspace{0.8cm}
3414 \mytyc{D}.\myfun{f}_i : \mytele; (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr \myse{F}_i \in \myctx\\
3418 \begin{array}{@{}l@{\ }l}
3419 \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})})
3426 \UnaryInfC{$\myjm{\mytmm}{\mytya}{\mytmn}{\mytyb} \myred \mybot\ \text{if $\mytya$ and $\mytyb$ are canonical types.}$}
3429 \caption{Propositions and equality reduction in $\mykant$. We assume
3430 the presence of $\mydataty$ and $\myisreco$ as operations on the
3431 context to recognise whether a user defined type is a data type or a
3433 \label{fig:kant-eq-red}
3436 \subsubsection{Coercions}
3440 \subsubsection{$\myprop$ and the hierarchy}
3442 We shall have, at earch universe level, not only a $\mytyp_l$ but also a
3443 $\myprop_l$. Where will propositions placed in the type hierarchy? The
3444 main indicator is the decoding operator, since it converts into things
3445 that already live in the hierarchy. For example, if we have
3447 \myprdec{\mynat \myarr \mybool \myeq \mynat \myarr \mybool} \myred
3448 \mytop \myand ((\myb{x}\, \myb{y} : \mynat) \myarr \mytop \myarr \mytop)
3450 we will better make sure that the `to be decoded' is at the same
3451 level as its reduction as to preserve subject reduction. In the example
3452 above, we'll have that proposition to be at least as large as the type
3453 of $\mynat$, since the reduced proof will abstract over it. Pretending
3454 that we had explicit, non cumulative levels, it would be tempting to have
3457 \AxiomC{$\myjud{\myse{Q}}{\myprop_l}$}
3458 \UnaryInfC{$\myjud{\myprdec{\myse{Q}}}{\mytyp_l}$}
3461 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
3462 \AxiomC{$\myjud{\mytyb}{\mytyp_l}$}
3463 \BinaryInfC{$\myjud{\myjm{\mytya}{\mytyp_{l}}{\mytyb}{\mytyp_{l}}}{\myprop_l}$}
3467 $\mybot$ and $\mytop$ living at any level, $\myand$ and $\forall$
3468 following rules similar to the ones for $\myprod$ and $\myarr$ in
3469 Section \ref{sec:itt}. However, we need to be careful with value
3470 equality since for example we have that
3472 \myprdec{\myjm{\myse{f}_1}{\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}}{\myse{f}_2}{\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}}}
3474 \myfora{\myb{x_1}}{\mytya_1}{\myfora{\myb{x_2}}{\mytya_2}{\cdots}}
3476 where the proposition decodes into something of at least type $\mytyp_l$, where
3477 $\mytya_l : \mytyp_l$ and $\mytyb_l : \mytyp_l$. We can resolve this
3478 tension by making all equalities larger:
3480 \AxiomC{$\myjud{\mytmm}{\mytya}$}
3481 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
3482 \AxiomC{$\myjud{\mytmn}{\mytyb}$}
3483 \AxiomC{$\myjud{\mytyb}{\mytyp_l}$}
3484 \QuaternaryInfC{$\myjud{\myjm{\mytmm}{\mytya}{\mytmm}{\mytya}}{\myprop_l}$}
3486 This is disappointing, since type equalities will be needlessly large:
3487 $\myprdec{\myjm{\mytya}{\mytyp_l}{\mytyb}{\mytyp_l}} : \mytyp_{l + 1}$.
3489 However, considering that our theory is cumulative, we can do better.
3490 Assuming rules for $\myprop$ cumulativity similar to the ones for
3491 $\mytyp$, we will have (with the conversion rule reproduced as a
3495 \AxiomC{$\myctx \vdash \mytya \mycumul \mytyb$}
3496 \AxiomC{$\myjud{\mytmt}{\mytya}$}
3497 \BinaryInfC{$\myjud{\mytmt}{\mytyb}$}
3500 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
3501 \AxiomC{$\myjud{\mytyb}{\mytyp_l}$}
3502 \BinaryInfC{$\myjud{\myjm{\mytya}{\mytyp_{l}}{\mytyb}{\mytyp_{l}}}{\myprop_l}$}
3508 \AxiomC{$\myjud{\mytmm}{\mytya}$}
3509 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
3510 \AxiomC{$\myjud{\mytmn}{\mytyb}$}
3511 \AxiomC{$\myjud{\mytyb}{\mytyp_l}$}
3512 \AxiomC{$\mytya$ and $\mytyb$ are not $\mytyp_{l'}$}
3513 \QuinaryInfC{$\myjud{\myjm{\mytmm}{\mytya}{\mytmm}{\mytya}}{\myprop_l}$}
3517 That is, we are small when we can (type equalities) and large otherwise.
3518 This would not work in a non-cumulative theory because subject reduction
3519 would not hold. Consider for instance
3521 \myjm{\mynat}{\myITE{\mytrue}{\mytyp_0}{\mytyp_0}}{\mybool}{\myITE{\mytrue}{\mytyp_0}{\mytyp_0}}
3525 \[\myjm{\mynat}{\mytyp_0}{\mybool}{\mytyp_0} : \myprop_0 \]
3526 We need $\myprop_0$ to be $\myprop_1$ too, which will be the case with
3527 cumulativity. This is not the most elegant of systems, but it buys us a
3528 cheap type level equality without having to replicate functionality with
3529 a dedicated construct.
3531 \subsubsection{Quotation and definitional equality}
3532 \label{sec:kant-irr}
3534 Now we can give an account of definitional equality, by explaining how
3535 to perform quotation (as defined in Section \ref{sec:eta-expand})
3536 towards the goal described in Section \ref{sec:ott-quot}.
3540 \item Perform $\eta$-expansion on functions and records.
3542 \item As a consequence of the previous point, identify all records with
3543 no projections as equal, since they will have only one element.
3545 \item Identify all members of types with no elements as equal.
3547 \item Identify all equivalent proofs as equal---with `equivalent proof'
3548 we mean those proving the same propositions.
3550 \item Advance coercions working across definitionally equal types.
3552 Towards these goals and following the intuition between bidirectional
3553 type checking we define two mutually recursive functions, one quoting
3554 canonical terms against their types (since we need the type to typecheck
3555 canonical terms), one quoting neutral terms while recovering their
3556 types. The full procedure for quotation is shown in Figure
3557 \ref{fig:kant-quot}. We $\boxed{\text{box}}$ the neutral proofs and
3558 neutral members of empty types, following the notation in
3559 \cite{Altenkirch2007}, and we make use of $\mydefeq_{\mybox}$ which
3560 compares terms syntactically up to $\alpha$-renaming, but also up to
3561 equivalent proofs: we consider all boxed content as equal.
3563 Our quotation will work on normalised terms, so that all defined values
3564 will have been replaced. Moreover, we match on datatype eliminators and
3565 all their arguments, so that $\mynat.\myfun{elim} \myappsp \mytmm
3566 \myappsp \myse{P} \myappsp \vec{\mytmn}$ will stand for
3567 $\mynat.\myfun{elim}$ applied to the scrutinised $\mynat$, the
3568 predicate, and the two cases. This measure can be easily implemented by
3569 checking the head of applications and `consuming' the needed terms.
3572 \mydesc{canonical quotation:}{\mycanquot(\myctx, \mytmsyn : \mytmsyn) \mymetagoes \mytmsyn}{
3575 \begin{array}{@{}l@{}l}
3576 \mycanquot(\myctx,\ \mytmt : \mytyc{D} \myappsp \vec{A} &) \mymetaguard \mymeta{empty}(\myctx, \mytyc{D}) \mymetagoes \boxed{\mytmt} \\
3577 \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)) \\
3578 \mycanquot(\myctx,\ \mytyc{D}.\mydc{c} \myappsp \vec{t} : \mytyc{D} \myappsp \vec{A} &) \mymetagoes \cdots \\
3579 \mycanquot(\myctx,\ \myse{f} : \myfora{\myb{x}}{\mytya}{\mytyb} &) \mymetagoes \myabs{\myb{x}}{\mycanquot(\myctx; \myb{x} : \mytya, \myapp{\myse{f}}{\myb{x}} : \mytyb)} \\
3580 \mycanquot(\myctx,\ \myse{p} : \myprdec{\myse{P}} &) \mymetagoes \boxed{\myse{p}}
3582 \mycanquot(\myctx,\ \mytmt : \mytya &) \mymetagoes \mytmt'\ \text{\textbf{where}}\ \mytmt' : \myarg = \myneuquot(\myctx, \mytmt)
3589 \mydesc{neutral quotation:}{\myneuquot(\myctx, \mytmsyn) \mymetagoes \mytmsyn : \mytmsyn}{
3592 \begin{array}{@{}l@{}l}
3593 \myneuquot(\myctx,\ \myb{x} &) \mymetagoes \myb{x} : \myctx(\myb{x}) \\
3594 \myneuquot(\myctx,\ \mytyp &) \mymetagoes \mytyp : \mytyp \\
3595 \myneuquot(\myctx,\ \myfora{\myb{x}}{\mytya}{\mytyb} & ) \mymetagoes
3596 \myfora{\myb{x}}{\myneuquot(\myctx, \mytya)}{\myneuquot(\myctx; \myb{x} : \mytya, \mytyb)} : \mytyp \\
3597 \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 \\
3598 \myneuquot(\myctx,\ \myprdec{\myjm{\mytmm}{\mytya}{\mytmn}{\mytyb}} &) \mymetagoes \myprdec{\myjm{\mycanquot(\myctx, \mytmm : \mytya)}{\mytya'}{\mycanquot(\myctx, \mytmn : \mytyb)}{\mytyb'}} : \mytyp \\
3599 \multicolumn{2}{@{}l}{\myind{2}\text{\textbf{where}}\ \mytya' : \myarg = \myneuquot(\myctx, \mytya)} \\
3600 \multicolumn{2}{@{}l}{\myind{2}\phantom{\text{\textbf{where}}}\ \mytyb' : \myarg = \myneuquot(\myctx, \mytyb)} \\
3601 \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) \\
3602 \multicolumn{2}{@{}l}{\myind{2}\text{\textbf{where}}\ \mytmt' : \mytyc{D} \myappsp \vec{A} = \myneuquot(\myctx, \mytmt)} \\
3603 \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 \\
3604 \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\\
3605 \multicolumn{2}{@{}l}{\myind{2}\text{\textbf{where}}\ \mytmm' : \mytyc{D} \myappsp \vec{A} = \myneuquot(\myctx, \mytmm)} \\
3606 \myneuquot(\myctx,\ \myapp{\myse{f}}{\mytmt} &) \mymetagoes \myapp{\myse{f'}}{\mycanquot(\myctx, \mytmt : \mytya)} : \mysub{\mytyb}{\myb{x}}{\mytmt} \\
3607 \multicolumn{2}{@{}l}{\myind{2}\text{\textbf{where}}\ \myse{f'} : \myfora{\myb{x}}{\mytya}{\mytyb} = \myneuquot(\myctx, \myse{f})} \\
3608 \myneuquot(\myctx,\ \mycoee{\mytya}{\mytyb}{\myse{Q}}{\mytmt} &) \mymetaguard \myneuquot(\myctx, \mytya) \mydefeq_{\mybox} \myneuquot(\myctx, \mytyb) \mymetagoes \myneuquot(\myctx, \mytmt) \\
3609 \myneuquot(\myctx,\ \mycoee{\mytya}{\mytyb}{\myse{Q}}{\mytmt} &) \mymetagoes
3610 \mycoee{\myneuquot(\myctx, \mytya)}{\myneuquot(\myctx, \mytyb)}{\boxed{\myse{Q}}}{\myneuquot(\myctx, \mytmt)}
3614 \caption{Quotation in \mykant. Along the already used
3615 $\mymeta{record}$ meta-operation on the context we make use of
3616 $\mymeta{empty}$, which checks if a certain type constructor has
3617 zero data constructor. The `data constructor' cases for non-record,
3618 non-empty, data types are omitted for brevity.}
3619 \label{fig:kant-quot}
3622 \subsubsection{Why $\myprop$?}
3624 It is worth to ask if $\myprop$ is needed at all. It is perfectly
3625 possible to have the type checker identify propositional types
3626 automatically, and in fact in some sense we already do during equality
3627 reduction and quotation. However, this has the considerable
3628 disadvantage that we can never identify abstracted
3629 variables\footnote{And in general neutral terms, although we currently
3630 don't have neutral propositions.} of type $\mytyp$ as $\myprop$, thus
3631 forbidding the user to talk about $\myprop$ explicitly.
3633 This is a considerable impediment, for example when implementing
3634 \emph{quotient types}. With quotients, we let the user specify an
3635 equivalence class over a certain type, and then exploit this in various
3636 way---crucially, we need to be sure that the equivalence given is
3637 propositional, a fact which prevented the use of quotients in dependent
3638 type theories \citep{Jacobs1994}.
3640 \section{\mykant : The practice}
3641 \label{sec:kant-practice}
3643 The codebase consists of around 2500 lines of Haskell, as reported by
3644 the \texttt{cloc} utility. The high level design is inspired by the
3645 work on various incarnations of Epigram, and specifically by the first
3646 version as described \citep{McBride2004} and the codebase for the new
3647 version.\footnote{Available intermittently as a \texttt{darcs}
3648 repository at \url{http://sneezy.cs.nott.ac.uk/darcs/Pig09}.} In many
3649 ways \mykant\ is something in between the first and second version of
3652 The author learnt the hard way the implementation challenges for such a
3653 project, and ran out of time while implementing observational equality.
3654 While the constructs and typing rules are present, the machinery to make
3655 it happen (equality reduction, coercions, quotation, etc.) is not
3656 present yet. Everything else presented is implemented and working
3657 reasonably well, and given the detailed plan in the previous section,
3658 finishing off should not prove too much work.
3660 The interaction with the user takes place in a loop living in and
3661 updating a context of \mykant\ declarations, which presents itself as in
3662 Figure \ref{fig:kant-web}. Files with lists of declarations can also be
3663 loaded. The REPL is a available both as a commandline application and in
3664 a web interface, which is available at \url{bertus.mazzo.li}.
3666 A REPL cycle starts with the user inputing a \mykant\
3667 declaration or another REPL command, which then goes through various
3668 stages that can end up in a context update, or in failures of various
3669 kind. The process is described diagrammatically in figure
3670 \ref{fig:kant-process}.
3673 {\small\begin{verbatim}B E R T U S
3674 Version 0.0, made in London, year 2013.
3676 <decl> Declare value/data type/record
3679 :p <term> Pretty print
3681 :r <file> Reload file (erases previous environment)
3682 :i <name> Info about an identifier
3684 >>> :l data/samples/good/common.ka
3686 >>> :e plus three two
3687 suc (suc (suc (suc (suc zero))))
3688 >>> :t plus three two
3689 Type: Nat\end{verbatim}
3692 \caption{A sample run of the \mykant\ prompt.}
3693 \label{fig:kant-web}
3699 \item[Parse] In this phase the text input gets converted to a sugared
3700 version of the core language. For example, we accept multiple
3701 arguments in arrow types and abstractions, and we represent variables
3702 with names, while as we will see in Section \ref{sec:term-repr} the
3703 final term types uses a \emph{nameless} representation.
3705 \item[Desugar] The sugared declaration is converted to a core term.
3706 Most notably we go from names to nameless.
3708 \item[ConDestr] Short for `Constructors/Destructors', converts
3709 applications of data destructors and constructors to a special form,
3710 to perform bidirectional type checking.
3712 \item[Reference] Occurrences of $\mytyp$ get decorated by a unique reference,
3713 which is necessary to implement the type hierarchy check.
3715 \item[Elaborate] Converts the declaration to some context items, which
3716 might be a value declaration (type and body) or a data type
3717 declaration (constructors and destructors). This phase works in
3718 tandem with \textbf{Type checking}, which in turns needs to
3719 \textbf{Evaluate} terms.
3721 \item[Distill] and report the result. `Distilling' refers to the
3722 process of converting a core term back to a sugared version that the
3723 user can visualise. This can be necessary both to display errors
3724 including terms or to display result of evaluations or type checking
3725 that the user has requested. Among the other things in this stage we
3726 go from nameless back to names by recycling the names that the user
3727 used originally, as to fabricate a term which is as close as possible
3728 to what it originated from.
3730 \item[Pretty print] Format the terms in a nice way, and display the result to
3737 \tikzstyle{block} = [rectangle, draw, text width=5em, text centered, rounded
3738 corners, minimum height=2.5em, node distance=0.7cm]
3740 \tikzstyle{decision} = [diamond, draw, text width=4.5em, text badly
3741 centered, inner sep=0pt, node distance=0.7cm]
3743 \tikzstyle{line} = [draw, -latex']
3745 \tikzstyle{cloud} = [draw, ellipse, minimum height=2em, text width=5em, text
3746 centered, node distance=1.5cm]
3749 \begin{tikzpicture}[auto]
3750 \node [cloud] (user) {User};
3751 \node [block, below left=1cm and 0.1cm of user] (parse) {Parse};
3752 \node [block, below=of parse] (desugar) {Desugar};
3753 \node [block, below=of desugar] (condestr) {ConDestr};
3754 \node [block, below=of condestr] (reference) {Reference};
3755 \node [block, below=of reference] (elaborate) {Elaborate};
3756 \node [block, left=of elaborate] (tycheck) {Typecheck};
3757 \node [block, left=of tycheck] (evaluate) {Evaluate};
3758 \node [decision, right=of elaborate] (error) {Error?};
3759 \node [block, right=of parse] (pretty) {Pretty print};
3760 \node [block, below=of pretty] (distill) {Distill};
3761 \node [block, below=of distill] (update) {Update context};
3763 \path [line] (user) -- (parse);
3764 \path [line] (parse) -- (desugar);
3765 \path [line] (desugar) -- (condestr);
3766 \path [line] (condestr) -- (reference);
3767 \path [line] (reference) -- (elaborate);
3768 \path [line] (elaborate) edge[bend right] (tycheck);
3769 \path [line] (tycheck) edge[bend right] (elaborate);
3770 \path [line] (elaborate) -- (error);
3771 \path [line] (error) edge[out=0,in=0] node [near start] {yes} (distill);
3772 \path [line] (error) -- node [near start] {no} (update);
3773 \path [line] (update) -- (distill);
3774 \path [line] (pretty) -- (user);
3775 \path [line] (distill) -- (pretty);
3776 \path [line] (tycheck) edge[bend right] (evaluate);
3777 \path [line] (evaluate) edge[bend right] (tycheck);
3780 \caption{High level overview of the life of a \mykant\ prompt cycle.}
3781 \label{fig:kant-process}
3784 Here we will review only a sampling of the more interesting
3785 implementation challenges present when implementing an interactive
3790 The syntax of \mykant\ is presented in Figure \ref{fig:syntax}.
3791 Examples showing the usage of most of the constructs are present in
3792 Appendices \ref{app:kant-itt}, \ref{app:kant-examples}, and
3797 \begin{array}{@{\ \ }l@{\ }c@{\ }l}
3798 \multicolumn{3}{@{}l}{\text{A name, in regexp notation.}} \\
3799 \mysee{name} & ::= & \texttt{[a-zA-Z] [a-zA-Z0-9'\_-]*} \\
3800 \multicolumn{3}{@{}l}{\text{A binder might or might not (\texttt{\_}) bind a name.}} \\
3801 \mysee{binder} & ::= & \mytermi{\_} \mysynsep \mysee{name} \\
3802 \multicolumn{3}{@{}l}{\text{A series of typed bindings.}} \\
3803 \mysee{telescope}\, \ \ \ & ::= & (\mytermi{[}\ \mysee{binder}\ \mytermi{:}\ \mysee{term}\ \mytermi{]}){*} \\
3804 \multicolumn{3}{@{}l}{\text{Terms, including propositions.}} \\
3805 \multicolumn{3}{@{}l}{
3806 \begin{array}{@{\ \ }l@{\ }c@{\ }l@{\ \ \ \ \ }l}
3807 \mysee{term} & ::= & \mysee{name} & \text{A variable.} \\
3808 & | & \mytermi{*} & \text{\mytyc{Type}.} \\
3809 & | & \mytermi{\{|}\ \mysee{term}{*}\ \mytermi{|\}} & \text{Type holes.} \\
3810 & | & \mytermi{Prop} & \text{\mytyc{Prop}.} \\
3811 & | & \mytermi{Top} \mysynsep \mytermi{Bot} & \text{$\mytop$ and $\mybot$.} \\
3812 & | & \mysee{term}\ \mytermi{/\textbackslash}\ \mysee{term} & \text{Conjuctions.} \\
3813 & | & \mytermi{[|}\ \mysee{term}\ \mytermi{|]} & \text{Proposition decoding.} \\
3814 & | & \mytermi{coe}\ \mysee{term}\ \mysee{term}\ \mysee{term}\ \mysee{term} & \text{Coercion.} \\
3815 & | & \mytermi{coh}\ \mysee{term}\ \mysee{term}\ \mysee{term}\ \mysee{term} & \text{Coherence.} \\
3816 & | & \mytermi{(}\ \mysee{term}\ \mytermi{:}\ \mysee{term}\ \mytermi{)}\ \mytermi{=}\ \mytermi{(}\ \mysee{term}\ \mytermi{:}\ \mysee{term}\ \mytermi{)} & \text{Heterogeneous equality.} \\
3817 & | & \mytermi{(}\ \mysee{compound}\ \mytermi{)} & \text{Parenthesised term.} \\
3818 \mysee{compound} & ::= & \mytermi{\textbackslash}\ \mysee{binder}{*}\ \mytermi{=>}\ \mysee{term} & \text{Untyped abstraction.} \\
3819 & | & \mytermi{\textbackslash}\ \mysee{telescope}\ \mytermi{:}\ \mysee{term}\ \mytermi{=>}\ \mysee{term} & \text{Typed abstraction.} \\
3820 & | & \mytermi{forall}\ \mysee{telescope}\ \mysee{term} & \text{Universal quantification.} \\
3821 & | & \mysee{arr} \\
3822 \mysee{arr} & ::= & \mysee{telescope}\ \mytermi{->}\ \mysee{arr} & \text{Dependent function.} \\
3823 & | & \mysee{term}\ \mytermi{->}\ \mysee{arr} & \text{Non-dependent function.} \\
3824 & | & \mysee{term}{+} & \text {Application.}
3827 \multicolumn{3}{@{}l}{\text{Typed names.}} \\
3828 \mysee{typed} & ::= & \mysee{name}\ \mytermi{:}\ \mysee{term} \\
3829 \multicolumn{3}{@{}l}{\text{Declarations.}} \\
3830 \mysee{decl}& ::= & \mysee{value} \mysynsep \mysee{abstract} \mysynsep \mysee{data} \mysynsep \mysee{record} \\
3831 \multicolumn{3}{@{}l}{\text{Defined values. The telescope specifies named arguments.}} \\
3832 \mysee{value} & ::= & \mysee{name}\ \mysee{telescope}\ \mytermi{:}\ \mysee{term}\ \mytermi{=>}\ \mysee{term} \\
3833 \multicolumn{3}{@{}l}{\text{Abstracted variables.}} \\
3834 \mysee{abstract} & ::= & \mytermi{postulate}\ \mysee{typed} \\
3835 \multicolumn{3}{@{}l}{\text{Data types, and their constructors.}} \\
3836 \mysee{data} & ::= & \mytermi{data}\ \mysee{name}\ \mysee{telescope}\ \mytermi{->}\ \mytermi{*}\ \mytermi{=>}\ \mytermi{\{}\ \mysee{constrs}\ \mytermi{\}} \\
3837 \mysee{constrs} & ::= & \mysee{typed} \\
3838 & | & \mysee{typed}\ \mytermi{|}\ \mysee{constrs} \\
3839 \multicolumn{3}{@{}l}{\text{Records, and their projections. The $\mysee{name}$ before the projections is the constructor name.}} \\
3840 \mysee{record} & ::= & \mytermi{record}\ \mysee{name}\ \mysee{telescope}\ \mytermi{->}\ \mytermi{*}\ \mytermi{=>}\ \mysee{name}\ \mytermi{\{}\ \mysee{projs}\ \mytermi{\}} \\
3841 \mysee{projs} & ::= & \mysee{typed} \\
3842 & | & \mysee{typed}\ \mytermi{,}\ \mysee{projs}
3846 \caption{\mykant' syntax. The non-terminals are marked with
3847 $\langle\text{angle brackets}\rangle$ for greater clarity. The
3848 syntax in the implementation is actually more liberal, for example
3849 giving the possibility of using arrow types directly in
3850 constructor/projection declarations.}
3854 \subsection{Term and context representation}
3855 \label{sec:term-repr}
3857 \subsubsection{Naming and substituting}
3859 Perhaps surprisingly, one of the most difficult challenges in
3860 implementing a theory of the kind presented is choosing a good data type
3861 for terms, and specifically handling substitutions in a sane way.
3863 There are two broad schools of thought when it comes to naming
3864 variables, and thus substituting:
3866 \item[Nameful] Bound variables are represented by some enumerable data
3867 type, just as we have described up to now, starting from Section
3868 \ref{sec:untyped}. The problem is that avoiding name capturing is a
3869 nightmare, both in the sense that it is not performant---given that we
3870 need to rename rename substitute each time we `enter' a binder---but
3871 most importantly given the fact that in even more slightly complicated
3872 systems it is very hard to get right, even for experts.
3874 One of the sore spots of explicit names is comparing terms up
3875 $\alpha$-renaming, which again generates a huge amounts of
3876 substitutions and requires special care. We can represent the
3877 relationship between variables and their binders, by...
3879 \item[Nameless] ...getting rid of names altogether, and representing
3880 bound variables with an index referring to the `binding' structure, a
3881 notion introduced by \cite{de1972lambda}. Classically $0$ represents
3882 the variable bound by the innermost binding structure, $1$ the
3883 second-innermost, and so on. For instance with simple abstractions we
3887 \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} \\
3888 \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
3892 While this technique is obviously terrible in terms of human
3893 usability,\footnote{With some people going as far as defining it akin
3894 to an inverse Turing test.} it is much more convenient as an
3895 internal representation to deal with terms mechanically---at least in
3896 simple cases. Moreover, $\alpha$ renaming ceases to be an issue, and
3897 term comparison is purely syntactical.
3899 Nonetheless, more complex, constructs such as pattern matching put
3900 some strain on the indices and many systems end up using explicit
3901 names anyway (Agda, Coq, \dots).
3905 In the past decade or so advancements in the Haskell's type system and
3906 in general the spread new programming practices have enabled to make the
3907 second option much more amenable. \mykant\ thus takes the second path
3908 through the use of Edward Kmett's excellent \texttt{bound}
3909 library.\footnote{Available at
3910 \url{http://hackage.haskell.org/package/bound}.} We decribe its
3911 advantages but also pitfalls in the previously relatively unknown
3912 territory of dependent types---\texttt{bound} being created mostly to
3913 handle more simply typed systems.
3915 \texttt{bound} builds on the work of \cite{Bird1999}, who suggest to
3916 parametrising the term type over the type of the variables, and `nest'
3917 the type each time we enter a scope. If we wanted to define a term for
3918 the untyped $\lambda$-calculus, we might have
3920 -- A type with no members.
3923 data Var v = Bound | Free v
3926 = V v -- Bound variable
3927 | App (Tm v) (Tm v) -- Term application
3928 | Lam (Tm (Var v)) -- Abstraction
3930 Closed terms would be of type \texttt{Tm Empty}, so that there would be
3931 no occurrences of \texttt{V}. However, inside an abstraction, we can
3932 have \texttt{V Bound}, representing the bound variable, and inside a
3933 second abstraction we can have \texttt{V Bound} or \texttt{V (Free
3934 Bound)}. Thus the term
3935 \[\myabs{\myb{x}}{\myabs{\myb{y}}{\myb{x}}}\]
3936 can be represented as
3938 -- The top level term is of type `Tm Empty'.
3939 -- The inner term `Lam (Free Bound)' is of type `Tm (Var Empty)'.
3940 -- The second inner term `V (Free Bound)' is of type `Tm (Var (Var
3942 Lam (Lam (V (Free Bound)))
3944 This allows us to reflect the of a type `nestedness' at the type level,
3945 and since we usually work with functions polymorphic on the parameter
3946 \texttt{v} it's very hard to make mistakes by putting terms of the wrong
3947 nestedness where they don't belong.
3949 Even more interestingly, the substitution operation is perfectly
3950 captured by the \verb|>>=| (bind) operator of the \texttt{Monad}
3955 (>>=) :: m a -> (a -> m b) -> m b
3957 instance Monad Tm where
3958 -- `return'ing turns a variable into a `Tm'
3961 -- `t >>= f' takes a term `t' and a mapping from variables to terms
3962 -- `f' and applies `f' to all the variables in `t', replacing them
3963 -- with the mapped terms.
3965 App m n >>= f = App (m >>= f) (n >>= f)
3967 -- `Lam' is the tricky case: we modify the function to work with bound
3968 -- variables, so that if it encounters `Bound' it leaves it untouched
3969 -- (since the mapping refers to the outer scope); if it encounters a
3970 -- free variable it asks `f' for the term and then updates all the
3971 -- variables to make them refer to the outer scope they were meant to
3973 Lam s >>= f = Lam (s >>= bump)
3974 where bump Bound = return Bound
3975 bump (Free v) = f v >>= V . Free
3977 With this in mind, we can define functions which will not only work on
3978 \verb|Tm|, but on any \verb|Monad|!
3980 -- Replaces free variable `v' with `m' in `n'.
3981 subst :: (Eq v, Monad m) => v -> m v -> m v -> m v
3982 subst v m n = n >>= \v' -> if v == v' then m else return v'
3984 -- Replace the variable bound by `s' with term `t'.
3985 inst :: Monad m => m v -> m (Var v) -> m v
3986 inst t s = do v <- s
3989 Free v' -> return v'
3991 The beauty of this technique is that in a few simple function we have
3992 defined all the core operations in a general and `obviously correct'
3993 way, with the extra confidence of having the type checker looking our
3994 back. For what concerns term equality, we can just ask the Haskell
3995 compiler to derive the instance for the \verb|Eq| type class and since
3996 we are nameless that will be enough (modulo fancy quotation).
3998 Moreover, if we take the top level term type to be \verb|Tm String|, we
3999 get for free a representation of terms with top-level, definitions;
4000 where closed terms contain only \verb|String| references to said
4001 definitions---see also \cite{McBride2004b}.
4003 What are then the pitfalls of this seemingly invincible technique? The
4004 most obvious impediment is the need for polymorphic recursion.
4005 Functions traversing terms parametrised by the variable type will have
4008 -- Infer the type of a term, or return an error.
4009 infer :: Tm v -> Either Error (Tm v)
4011 When traversing under a \verb|Scope| the parameter changes from \verb|v|
4012 to \verb|Var v|, and thus if we do not specify the type for our function explicitly
4013 inference will fail---type inference for polymorphic recursion being
4014 undecidable \citep{henglein1993type}. This causes some annoyance,
4015 especially in the presence of many local definitions that we would like
4018 But the real issue is the fact that giving a type parametrised over a
4019 variable---say \verb|m v|---a \verb|Monad| instance means being able to
4020 only substitute variables for values of type \verb|m v|. This is a
4021 considerable inconvenience. Consider for instance the case of
4022 telescopes, which are a central tool to deal with contexts and other
4023 constructs. In Haskell we can give them a faithful representation
4024 with a data type along the lines of
4026 data Tele m v = End (m v) | Bind (m v) (Tele (Var v))
4027 type TeleTm = Tele Tm
4029 The problem here is that what we want to substitute for variables in
4030 \verb|Tele m v| is \verb|m v| (probably \verb|Tm v|), not \verb|Tele m v| itself! What we need is
4032 bindTele :: Monad m => Tele m a -> (a -> m b) -> Tele m b
4033 substTele :: (Eq v, Monad m) => v -> m v -> Tele m v -> Tele m v
4034 instTele :: Monad m => m v -> Tele m (Var v) -> Tele m v
4036 Not what \verb|Monad| gives us. Solving this issue in an elegant way
4037 has been a major sink of time and source of headaches for the author,
4038 who analysed some of the alternatives---most notably the work by
4039 \cite{weirich2011binders}---but found it impossible to give up the
4040 simplicity of the model above.
4042 That said, our term type is still reasonably brief, as shown in full in
4043 Appendix \ref{app:termrep}. The fact that propositions cannot be
4044 factored out in another data type is an instance of the problem
4045 described above. However the real pain is during elaboration, where we
4046 are forced to treat everything as a type while we would much rather have
4047 telescopes. Future work would include writing a library that marries a
4048 nice interface similar to the one of \verb|bound| with a more flexible
4051 We also make use of a `forgetful' data type (as provided by
4052 \verb|bound|) to store user-provided variables names along with the
4053 `nameless' representation, so that the names will not be considered when
4054 compared terms, but will be available when distilling so that we can
4055 recover variable names that are as close as possible to what the user
4058 \subsubsection{Evaluation}
4060 Another source of contention related to term representation is dealing
4061 with evaluation. Here \mykant\ does not make bold moves, and simply
4062 employs substitution. When type checking we match types by reducing
4063 them to their wheak head normal form, as to avoid unnecessary evaluation.
4065 We treat data types eliminators and record projections in an uniform
4066 way, by elaborating declarations in a series of \emph{rewriting rules}:
4070 TmRef v -> -- Term to which the destructor is applied
4071 [TmRef v] -> -- List of other arguments
4072 -- The result of the rewriting, if the eliminator reduces.
4075 A rewriting rule is polymorphic in the variable type, guaranteeing that
4076 it just pattern matches on terms structure and rearranges them in some
4077 way, and making it possible to apply it at any level in the term. When
4078 reducing a series of applications we match the first term and check if
4079 it is a destructor, and if that's the case we apply the reduction rule
4080 and reduce further if it yields a new list of terms.
4082 This has the advantage of being very simple, but has the disadvantage of
4083 being quite poor in terms of performance and that we need to do
4084 quotation manually. An alternative that solves both of these is the
4085 already mentioned \emph{normalization by evaluation}, where we would
4086 compute by turning terms into Haskell values, and then reify back to
4087 terms to compare them---a useful tutorial on this technique is given by
4090 \subsubsection{Context}
4092 Given our term type parametrised on the type of the variables,
4096 \subsection{Turning constraints into graphs}
4097 \label{sec:hier-impl}
4099 As an interlude from all the types, we will explain how to
4100 implement the typical ambiguity we have spoken about in
4101 \ref{sec:term-hierarchy} efficiently. As mentioned, we have to verify a the
4102 consistency of a set of constraints each time we add a new one. The
4103 constraints range over some set of variables whose members we will
4104 denote with $x, y, z, \dots$. and are of two kinds:
4111 Predictably, $\le$ expresses a reflexive order, and $<$ expresses an
4112 irreflexive order, both working with the same notion of equality, where
4113 $x < y$ implies $x \le y$---they behave like $\le$ and $<$ do for natural
4114 numbers (or in our case, levels in a type hierarchy). We also need an
4115 equality constraint ($x = y$), which can be reduced to two constraints
4116 $x \le y$ and $y \le x$.
4118 Given this specification, we have implemented a standalone Haskell
4119 module---that we plan to release as a standalone library---to
4120 efficiently store and check the consistency of constraints. The problem
4121 predictably reduces to a graph algorithm, and for this reason we also
4122 implement a library for labelled graphs, since the existing Haskell
4123 graph libraries fell short in different areas.\footnote{We tried the
4124 \texttt{Data.Graph} module in
4125 \url{http://hackage.haskell.org/package/containers}, and the much more
4126 featureful \texttt{fgl} library
4127 \url{http://hackage.haskell.org/package/fgl}.}. The interfaces for
4128 these modules are shown in Appendix \ref{app:constraint}. The graph
4129 library is implemented as a modification of the code described by
4132 We represent the set by building a graph where vertices are variables,
4133 and edges are constraints between them, labelled with the appropriate
4134 constraint: $x < y$ gives rise to a $<$-labelled edge from $x$ to $y$<
4135 and $x \le y$ to a $\le$-labelled edge from $x$ to $y$. As we add
4136 constraints, $\le$ constraints are replaced by $<$ constraints, so that
4137 if we started with an empty set and added
4139 x < y,\ y \le z,\ z \le k,\ k < j,\ j \le y\, z < k
4141 it would generate the graph shown in Figure \ref{fig:graph-one}.
4145 \begin{subfigure}[b]{0.3\textwidth}
4146 \begin{tikzpicture}[node distance=1.5cm]
4149 \node [right of=x] (y) {$y$};
4150 \node [right of=y] (z) {$z$};
4151 \node [below of=z] (k) {$k$};
4152 \node [left of=k] (j) {$j$};
4155 (x) edge node [above] {$<$} (y)
4156 (y) edge node [above] {$\le$} (z)
4157 (z) edge node [right] {$<$} (k)
4158 (k) edge node [below] {$\le$} (j)
4159 (j) edge node [left ] {$\le$} (y);
4161 \caption{Before $z < k$.}
4162 \label{fig:graph-one-before}
4165 \begin{subfigure}[b]{0.3\textwidth}
4166 \begin{tikzpicture}[node distance=1.5cm]
4169 \node [right of=x] (y) {$y$};
4170 \node [right of=y] (z) {$z$};
4171 \node [below of=z] (k) {$k$};
4172 \node [left of=k] (j) {$j$};
4175 (x) edge node [above] {$<$} (y)
4176 (y) edge node [above] {$\le$} (z)
4177 (z) edge node [right] {$<$} (k)
4178 (k) edge node [below] {$\le$} (j)
4179 (j) edge node [left ] {$\le$} (y);
4181 \caption{After $z < k$.}
4182 \label{fig:graph-one-after}
4185 \begin{subfigure}[b]{0.3\textwidth}
4186 \begin{tikzpicture}[remember picture, node distance=1.5cm]
4187 \begin{pgfonlayer}{foreground}
4190 \node [right of=x] (y) {$y$};
4191 \node [right of=y] (z) {$z$};
4192 \node [below of=z] (k) {$k$};
4193 \node [left of=k] (j) {$j$};
4196 (x) edge node [above] {$<$} (y)
4197 (y) edge node [above] {$\le$} (z)
4198 (z) edge node [right] {$<$} (k)
4199 (k) edge node [below] {$\le$} (j)
4200 (j) edge node [left ] {$\le$} (y);
4201 \end{pgfonlayer}{foreground}
4203 \begin{tikzpicture}[remember picture, overlay]
4204 \begin{pgfonlayer}{background}
4205 \fill [red, opacity=0.3]
4206 (-2.5,2.4) rectangle (-0.4,0.2)
4207 (-4,2.4) rectangle (-3.3,1.6);
4208 \end{pgfonlayer}{background}
4211 \label{fig:graph-one-scc}
4213 \caption{Strong constraints overrule weak constraints.}
4214 \label{fig:graph-one}
4217 \subsection{Type holes}
4218 \label{sec:type-holes}
4220 Type holes are, in the author's opinion, one of the `killer' features of
4221 interactive theorem provers, and one that is begging to be exported to
4222 the word of mainstream programming. The idea is that when we are
4223 developing a proof or a program we can insert a hole to have the
4224 software tell us the type expected at that point. Furthermore, we can
4225 ask for the type of variables in context, to better understand our
4230 \subsection{Web REPL}
4233 \section{Evaluation}
4235 \section{Future work}
4236 \label{sec:future-work}
4238 As mentioned, the first move that the author plans to make is to work
4239 towards a simple but powerful term representation, and then adjust
4240 \mykant\ to this new representation. A good plan seems to be to
4241 associate each type (terms, telescopes, etc.) with what we can
4242 substitute variables with, so that the term type will be associated with
4243 itself, while telescopes and propositions will be associated to terms.
4244 This can probably be accomplished elegantly with Haskell's \emph{type
4245 families} \citep{chakravarty2005associated}. After achieving a more
4246 solid machinery for terms, implementing observational equality fully
4247 should prove relatively easy.
4249 Beyond this steps, \mykant\ would still need many additions to compete
4250 as a reasonable alternative to the existing systems:
4253 \item[Pattern matching] Eliminators are very clumsy to use, and
4255 \item[More powerful data types] Beyond normal inductive data types,
4256 \mykant\ does not in more sophisticated notions. A popular
4257 improvements on basic data types are inductive families, where the
4258 parameters for the type constructors change based on the data
4259 constructors, which lets us express naturally types such as
4260 $\mytyc{Vec} : \mynat \myarr \mytyp$, which given a number returns the
4261 type of lists of that length, or $\mytyc{Fin} : \mynat \myarr \mytyp$,
4262 which given a number $n$ gives the type of numbers less than $n$.
4263 This apparent omission was motivated by the fact that inductive
4264 families can be represented by adding equalities concerning the
4265 parameters of the type constructors as arguments to the data
4266 constructor, in much the same way that Generalised Abstract Data Types
4267 \citep{GHC} are handled in Haskell, where interestingly the modified
4268 version of System F that lies at the core of recent versions of GHC
4269 features coercions similar to those found in OTT \citep{Sulzmann2007}.
4271 Another popular extension introduced by \cite{dybjer2000general} is
4272 induction-recursion, where we define a data type in tandem with a
4273 function on that type. This technique has proven extremely useful to
4274 define embeddings of other calculi in an host language, by defining
4275 the representation of the embedded language as a data type and at the
4276 same time a function decoding from the representation to a type in the
4279 It is also worth mentionning that in recent times there has been work
4280 by \cite{dagand2012elaborating, chapman2010gentle} to show how to
4281 define a set of primitives that data types can be elaborated into,
4282 with the additional advantage of having the possibility of having a
4283 very powerful notion of generic programming by writing functions
4284 working on the `primitive' types as to be workable by all `compatible'
4285 user-defined data types. This has been a considerable problem in the
4286 dependently type world, where we often define types which are more
4287 `strongly typed' version of similar structures,\footnote{For example
4288 the $\mytyc{OList}$ presented in Section \ref{sec:user-type} being a
4289 `more typed' version of an ordinary list.} and then find ourselves
4290 forced to redefine identical operations on both types.
4292 \item[Type inference] While bidirectional type checking helps, for a
4293 syts \cite{miller1992unification} \cite{gundrytutorial}
4294 \cite{huet1973undecidability}.
4296 \item[Coinduction] \cite{cockett1992charity} \cite{mcbride2009let}.
4301 \subsection{Coinduction}
4303 \subsection{Quotient types}
4305 \subsection{Partiality}
4307 \subsection{Pattern matching}
4309 \subsection{Pattern unification}
4311 % TODO coinduction (obscoin, gimenez, jacobs), pattern unification (miller,
4312 % gundry), partiality monad (NAD)
4316 \section{Notation and syntax}
4318 Syntax, derivation rules, and reduction rules, are enclosed in frames describing
4319 the type of relation being established and the syntactic elements appearing,
4322 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
4323 Typing derivations here.
4326 In the languages presented and Agda code samples I also highlight the syntax,
4327 following a uniform color and font convention:
4330 \begin{tabular}{c | l}
4331 $\mytyc{Sans}$ & Type constructors. \\
4332 $\mydc{sans}$ & Data constructors. \\
4333 % $\myfld{sans}$ & Field accessors (e.g. \myfld{fst} and \myfld{snd} for products). \\
4334 $\mysyn{roman}$ & Keywords of the language. \\
4335 $\myfun{roman}$ & Defined values and destructors. \\
4336 $\myb{math}$ & Bound variables.
4340 Moreover, I will from time to time give examples in the Haskell programming
4341 language as defined in \citep{Haskell2010}, which I will typeset in
4342 \texttt{teletype} font. I assume that the reader is already familiar with
4343 Haskell, plenty of good introductions are available \citep{LYAH,ProgInHask}.
4345 When presenting grammars, I will use a word in $\mysynel{math}$ font
4346 (e.g. $\mytmsyn$ or $\mytysyn$) to indicate indicate
4347 nonterminals. Additionally, I will use quite flexibly a $\mysynel{math}$
4348 font to indicate a syntactic element in derivations or meta-operations.
4349 More specifically, terms are usually indicated by lowercase letters
4350 (often $\mytmt$, $\mytmm$, or $\mytmn$); and types by an uppercase
4351 letter (often $\mytya$, $\mytyb$, or $\mytycc$).
4353 When presenting type derivations, I will often abbreviate and present multiple
4354 conclusions, each on a separate line:
4356 \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
4357 \UnaryInfC{$\myjud{\myapp{\myfst}{\mytmt}}{\mytya}$}
4359 \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mytyb}$}
4362 I will often present `definitions' in the described calculi and in
4363 $\mykant$\ itself, like so:
4366 \myfun{name} : \mytysyn \\
4367 \myfun{name} \myappsp \myb{arg_1} \myappsp \myb{arg_2} \myappsp \cdots \mapsto \mytmsyn
4370 To define operators, I use a mixfix notation similar
4371 to Agda, where $\myarg$s denote arguments:
4374 \myarg \mathrel{\myfun{$\wedge$}} \myarg : \mybool \myarr \mybool \myarr \mybool \\
4375 \myb{b_1} \mathrel{\myfun{$\wedge$}} \myb{b_2} \mapsto \cdots
4379 In explicitly typed systems, I will also omit type annotations when they
4380 are obvious, e.g. by not annotating the type of parameters of
4381 abstractions or of dependent pairs.
4383 I will introduce multiple arguments in one go in arrow types:
4385 (\myb{x}\, \myb{y} {:} \mytya) \myarr \cdots = (\myb{x} {:} \mytya) \myarr (\myb{y} {:} \mytya) \myarr \cdots
4387 and in abstractions:
4389 \myabs{\myb{x}\myappsp\myb{y}}{\cdots} = \myabs{\myb{x}}{\myabs{\myb{y}}{\cdots}}
4391 I will also omit arrows to abbreviate types:
4393 (\myb{x} {:} \mytya)(\myb{y} {:} \mytyb) \myarr \cdots =
4394 (\myb{x} {:} \mytya) \myarr (\myb{y} {:} \mytyb) \myarr \cdots
4396 Meta operations names will be displayed in $\mymeta{smallcaps}$ and
4397 written in a pattern matching style, also making use of boolean guards.
4398 For example, a meta operation operating on a context and terms might
4402 \mymeta{quux}(\myctx, \myb{x}) \mymetaguard \myb{x} \in \myctx \mymetagoes \myctx(\myb{x}) \\
4403 \mymeta{quux}(\myctx, \myb{x}) \mymetagoes \mymeta{outofbounds} \\
4410 \subsection{ITT renditions}
4411 \label{app:itt-code}
4413 \subsubsection{Agda}
4414 \label{app:agda-itt}
4416 Note that in what follows rules for `base' types are
4417 universe-polymorphic, to reflect the exposition. Derived definitions,
4418 on the other hand, mostly work with \mytyc{Set}, reflecting the fact
4419 that in the theory presented we don't have universe polymorphism.
4425 data Empty : Set where
4427 absurd : ∀ {a} {A : Set a} → Empty → A
4430 ¬_ : ∀ {a} → (A : Set a) → Set a
4433 record Unit : Set where
4436 record _×_ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
4443 data Bool : Set where
4446 if_/_then_else_ : ∀ {a} (x : Bool) (P : Bool → Set a) → P true → P false → P x
4447 if true / _ then x else _ = x
4448 if false / _ then _ else x = x
4450 if_then_else_ : ∀ {a} (x : Bool) {P : Bool → Set a} → P true → P false → P x
4451 if_then_else_ x {P} = if_/_then_else_ x P
4453 data W {s p} (S : Set s) (P : S → Set p) : Set (s ⊔ p) where
4454 _◁_ : (s : S) → (P s → W S P) → W S P
4456 rec : ∀ {a b} {S : Set a} {P : S → Set b}
4457 (C : W S P → Set) → -- some conclusion we hope holds
4458 ((s : S) → -- given a shape...
4459 (f : P s → W S P) → -- ...and a bunch of kids...
4460 ((p : P s) → C (f p)) → -- ...and C for each kid in the bunch...
4461 C (s ◁ f)) → -- ...does C hold for the node?
4462 (x : W S P) → -- If so, ...
4463 C x -- ...C always holds.
4464 rec C c (s ◁ f) = c s f (λ p → rec C c (f p))
4466 module Examples-→ where
4473 -- These pragmas are needed so we can use number literals.
4474 {-# BUILTIN NATURAL ℕ #-}
4475 {-# BUILTIN ZERO zero #-}
4476 {-# BUILTIN SUC suc #-}
4478 data List (A : Set) : Set where
4480 _∷_ : A → List A → List A
4482 length : ∀ {A} → List A → ℕ
4484 length (_ ∷ l) = suc (length l)
4489 suc x > suc y = x > y
4491 head : ∀ {A} → (l : List A) → length l > 0 → A
4492 head [] p = absurd p
4495 module Examples-× where
4501 even (suc zero) = Empty
4502 even (suc (suc n)) = even n
4507 5-not-even : ¬ (even 5)
4510 there-is-an-even-number : ℕ × even
4511 there-is-an-even-number = 6 , 6-even
4513 _∨_ : (A B : Set) → Set
4514 A ∨ B = Bool × (λ b → if b then A else B)
4516 left : ∀ {A B} → A → A ∨ B
4519 right : ∀ {A B} → B → A ∨ B
4522 [_,_] : {A B C : Set} → (A → C) → (B → C) → A ∨ B → C
4524 (if (fst x) / (λ b → if b then _ else _ → _) then f else g) (snd x)
4526 module Examples-W where
4531 Tr b = if b then Unit else Empty
4537 zero = false ◁ absurd
4540 suc n = true ◁ (λ _ → n)
4546 if b / (λ b → (Tr b → ℕ) → (Tr b → ℕ) → ℕ)
4547 then (λ _ f → (suc (f tt))) else (λ _ _ → y))
4550 module Equality where
4553 data _≡_ {a} {A : Set a} : A → A → Set a where
4556 ≡-elim : ∀ {a b} {A : Set a}
4557 (P : (x y : A) → x ≡ y → Set b) →
4558 ∀ {x y} → P x x (refl x) → (x≡y : x ≡ y) → P x y x≡y
4559 ≡-elim P p (refl x) = p
4561 subst : ∀ {A : Set} (P : A → Set) → ∀ {x y} → (x≡y : x ≡ y) → P x → P y
4562 subst P x≡y p = ≡-elim (λ _ y _ → P y) p x≡y
4564 sym : ∀ {A : Set} (x y : A) → x ≡ y → y ≡ x
4565 sym x y p = subst (λ y′ → y′ ≡ x) p (refl x)
4567 trans : ∀ {A : Set} (x y z : A) → x ≡ y → y ≡ z → x ≡ z
4568 trans x y z p q = subst (λ z′ → x ≡ z′) q p
4570 cong : ∀ {A B : Set} (x y : A) → x ≡ y → (f : A → B) → f x ≡ f y
4571 cong x y p f = subst (λ z → f x ≡ f z) p (refl (f x))
4574 \subsubsection{\mykant}
4575 \label{app:kant-itt}
4577 The following things are missing: $\mytyc{W}$-types, since our
4578 positivity check is overly strict, and equality, since we haven't
4579 implemented that yet.
4582 \verbatiminput{itt.ka}
4585 \subsection{\mykant\ examples}
4586 \label{app:kant-examples}
4589 \verbatiminput{examples.ka}
4592 \subsection{\mykant' hierachy}
4595 This rendition of the Hurken's paradox does not type check with the
4596 hierachy enabled, type checks and loops without it. Adapted from an
4597 Agda version, available at
4598 \url{http://code.haskell.org/Agda/test/succeed/Hurkens.agda}.
4601 \verbatiminput{hurkens.ka}
4604 \subsection{Term representation}
4607 Data type for terms in \mykant.
4609 {\small\begin{verbatim}-- A top-level name.
4611 -- A data/type constructor name.
4614 -- A term, parametrised over the variable (`v') and over the reference
4615 -- type used in the type hierarchy (`r').
4618 | Ty r -- Type, with a hierarchy reference.
4619 | Lam (TmScope r v) -- Abstraction.
4620 | Arr (Tm r v) (TmScope r v) -- Dependent function.
4621 | App (Tm r v) (Tm r v) -- Application.
4622 | Ann (Tm r v) (Tm r v) -- Annotated term.
4623 -- Data constructor, the first ConId is the type constructor and
4624 -- the second is the data constructor.
4625 | Con ADTRec ConId ConId [Tm r v]
4626 -- Data destrutor, again first ConId being the type constructor
4627 -- and the second the name of the eliminator.
4628 | Destr ADTRec ConId Id (Tm r v)
4630 | Hole HoleId [Tm r v]
4631 -- Decoding of propositions.
4635 | Prop r -- The type of proofs, with hierarchy reference.
4638 | And (Tm r v) (Tm r v)
4639 | Forall (Tm r v) (TmScope r v)
4640 -- Heterogeneous equality.
4641 | Eq (Tm r v) (Tm r v) (Tm r v) (Tm r v)
4643 -- Either a data type, or a record.
4644 data ADTRec = ADT | Rec
4646 -- Either a coercion, or coherence.
4647 data Coeh = Coe | Coh\end{verbatim}
4650 \subsection{Graph and constraints modules}
4651 \label{app:constraint}
4653 The modules are respectively named \texttt{Data.LGraph} (short for
4654 `labelled graph'), and \texttt{Data.Constraint}. The type class
4655 constraints on the type parameters are not shown for clarity, unless
4656 they are meaningful to the function. In practice we use the
4657 \texttt{Hashable} type class on the vertex to implement the graph
4658 efficiently with hash maps.
4660 \subsubsection{\texttt{Data.LGraph}}
4663 \verbatiminput{graph.hs}
4666 \subsubsection{\texttt{Data.Constraint}}
4669 \verbatiminput{constraint.hs}
4674 \bibliographystyle{authordate1}
4675 \bibliography{thesis}