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 % \usepackage{tikz-cd}
66 % \usepackage{pgfplots}
69 %% -----------------------------------------------------------------------------
71 \usepackage[english]{babel}
72 \usepackage[conor]{agda}
73 \renewcommand{\AgdaKeywordFontStyle}[1]{\ensuremath{\mathrm{\underline{#1}}}}
74 \renewcommand{\AgdaFunction}[1]{\textbf{\textcolor{AgdaFunction}{#1}}}
75 \renewcommand{\AgdaField}{\AgdaFunction}
76 % \definecolor{AgdaBound} {HTML}{000000}
77 \definecolor{AgdaHole} {HTML} {FFFF33}
79 \DeclareUnicodeCharacter{9665}{\ensuremath{\lhd}}
80 \DeclareUnicodeCharacter{964}{\ensuremath{\tau}}
81 \DeclareUnicodeCharacter{963}{\ensuremath{\sigma}}
82 \DeclareUnicodeCharacter{915}{\ensuremath{\Gamma}}
83 \DeclareUnicodeCharacter{8799}{\ensuremath{\stackrel{?}{=}}}
84 \DeclareUnicodeCharacter{9655}{\ensuremath{\rhd}}
86 \renewenvironment{code}%
87 {\noindent\ignorespaces\advance\leftskip\mathindent\AgdaCodeStyle\pboxed\small}%
88 {\endpboxed\par\noindent%
89 \ignorespacesafterend\small}
92 %% -----------------------------------------------------------------------------
95 \newcommand{\mysmall}{}
96 \newcommand{\mysyn}{\AgdaKeyword}
97 \newcommand{\mytyc}[1]{\textup{\AgdaDatatype{#1}}}
98 \newcommand{\mydc}[1]{\textup{\AgdaInductiveConstructor{#1}}}
99 \newcommand{\myfld}[1]{\textup{\AgdaField{#1}}}
100 \newcommand{\myfun}[1]{\textup{\AgdaFunction{#1}}}
101 \newcommand{\myb}[1]{\AgdaBound{$#1$}}
102 \newcommand{\myfield}{\AgdaField}
103 \newcommand{\myind}{\AgdaIndent}
104 \newcommand{\mykant}{\textmd{\textsc{Bertus}}}
105 \newcommand{\mysynel}[1]{#1}
106 \newcommand{\myse}{\mysynel}
107 \newcommand{\mytmsyn}{\mysynel{term}}
108 \newcommand{\mysp}{\ }
109 \newcommand{\myabs}[2]{\mydc{$\lambda$} #1 \mathrel{\mydc{$\mapsto$}} #2}
110 \newcommand{\myappsp}{\hspace{0.07cm}}
111 \newcommand{\myapp}[2]{#1 \myappsp #2}
112 \newcommand{\mysynsep}{\ \ |\ \ }
113 \newcommand{\myITE}[3]{\myfun{If}\, #1\, \myfun{Then}\, #2\, \myfun{Else}\, #3}
114 \newcommand{\mycumul}{\preceq}
117 \newcommand{\mydesc}[3]{
123 \hfill \textup{\textbf{#1}} $#2$
124 \framebox[\textwidth]{
139 \newcommand{\mytmt}{\mysynel{t}}
140 \newcommand{\mytmm}{\mysynel{m}}
141 \newcommand{\mytmn}{\mysynel{n}}
142 \newcommand{\myred}{\leadsto}
143 \newcommand{\mysub}[3]{#1[#2 / #3]}
144 \newcommand{\mytysyn}{\mysynel{type}}
145 \newcommand{\mybasetys}{K}
146 \newcommand{\mybasety}[1]{B_{#1}}
147 \newcommand{\mytya}{\myse{A}}
148 \newcommand{\mytyb}{\myse{B}}
149 \newcommand{\mytycc}{\myse{C}}
150 \newcommand{\myarr}{\mathrel{\textcolor{AgdaDatatype}{\to}}}
151 \newcommand{\myprod}{\mathrel{\textcolor{AgdaDatatype}{\times}}}
152 \newcommand{\myctx}{\Gamma}
153 \newcommand{\myvalid}[1]{#1 \vdash \underline{\mathrm{valid}}}
154 \newcommand{\myjudd}[3]{#1 \vdash #2 : #3}
155 \newcommand{\myjud}[2]{\myjudd{\myctx}{#1}{#2}}
156 \newcommand{\myabss}[3]{\mydc{$\lambda$} #1 {:} #2 \mathrel{\mydc{$\mapsto$}} #3}
157 \newcommand{\mytt}{\mydc{$\langle\rangle$}}
158 \newcommand{\myunit}{\mytyc{Unit}}
159 \newcommand{\mypair}[2]{\mathopen{\mydc{$\langle$}}#1\mathpunct{\mydc{,}} #2\mathclose{\mydc{$\rangle$}}}
160 \newcommand{\myfst}{\myfld{fst}}
161 \newcommand{\mysnd}{\myfld{snd}}
162 \newcommand{\myconst}{\myse{c}}
163 \newcommand{\myemptyctx}{\varepsilon}
164 \newcommand{\myhole}{\AgdaHole}
165 \newcommand{\myfix}[3]{\mysyn{fix} \myappsp #1 {:} #2 \mapsto #3}
166 \newcommand{\mysum}{\mathbin{\textcolor{AgdaDatatype}{+}}}
167 \newcommand{\myleft}[1]{\mydc{left}_{#1}}
168 \newcommand{\myright}[1]{\mydc{right}_{#1}}
169 \newcommand{\myempty}{\mytyc{Empty}}
170 \newcommand{\mycase}[2]{\mathopen{\myfun{[}}#1\mathpunct{\myfun{,}} #2 \mathclose{\myfun{]}}}
171 \newcommand{\myabsurd}[1]{\myfun{absurd}_{#1}}
172 \newcommand{\myarg}{\_}
173 \newcommand{\myderivsp}{}
174 \newcommand{\myderivspp}{\vspace{0.3cm}}
175 \newcommand{\mytyp}{\mytyc{Type}}
176 \newcommand{\myneg}{\myfun{$\neg$}}
177 \newcommand{\myar}{\,}
178 \newcommand{\mybool}{\mytyc{Bool}}
179 \newcommand{\mytrue}{\mydc{true}}
180 \newcommand{\myfalse}{\mydc{false}}
181 \newcommand{\myitee}[5]{\myfun{if}\,#1 / {#2.#3}\,\myfun{then}\,#4\,\myfun{else}\,#5}
182 \newcommand{\mynat}{\mytyc{$\mathbb{N}$}}
183 \newcommand{\myrat}{\mytyc{$\mathbb{R}$}}
184 \newcommand{\myite}[3]{\myfun{if}\,#1\,\myfun{then}\,#2\,\myfun{else}\,#3}
185 \newcommand{\myfora}[3]{(#1 {:} #2) \myarr #3}
186 \newcommand{\myexi}[3]{(#1 {:} #2) \myprod #3}
187 \newcommand{\mypairr}[4]{\mathopen{\mydc{$\langle$}}#1\mathpunct{\mydc{,}} #4\mathclose{\mydc{$\rangle$}}_{#2{.}#3}}
188 \newcommand{\mylist}{\mytyc{List}}
189 \newcommand{\mynil}[1]{\mydc{[]}_{#1}}
190 \newcommand{\mycons}{\mathbin{\mydc{∷}}}
191 \newcommand{\myfoldr}{\myfun{foldr}}
192 \newcommand{\myw}[3]{\myapp{\myapp{\mytyc{W}}{(#1 {:} #2)}}{#3}}
193 \newcommand{\mynodee}{\mathbin{\mydc{$\lhd$}}}
194 \newcommand{\mynode}[2]{\mynodee_{#1.#2}}
195 \newcommand{\myrec}[4]{\myfun{rec}\,#1 / {#2.#3}\,\myfun{with}\,#4}
196 \newcommand{\mylub}{\sqcup}
197 \newcommand{\mydefeq}{\cong}
198 \newcommand{\myrefl}{\mydc{refl}}
199 \newcommand{\mypeq}{\mytyc{=}}
200 \newcommand{\myjeqq}{\myfun{$=$-elim}}
201 \newcommand{\myjeq}[3]{\myapp{\myapp{\myapp{\myjeqq}{#1}}{#2}}{#3}}
202 \newcommand{\mysubst}{\myfun{subst}}
203 \newcommand{\myprsyn}{\myse{prop}}
204 \newcommand{\myprdec}[1]{\mathopen{\mytyc{$\llbracket$}} #1 \mathclose{\mytyc{$\rrbracket$}}}
205 \newcommand{\myand}{\mathrel{\mytyc{$\wedge$}}}
206 \newcommand{\mybigand}{\mathrel{\mytyc{$\bigwedge$}}}
207 \newcommand{\myprfora}[3]{\forall #1 {:} #2. #3}
208 \newcommand{\myimpl}{\mathrel{\mytyc{$\Rightarrow$}}}
209 \newcommand{\mybot}{\mytyc{$\bot$}}
210 \newcommand{\mytop}{\mytyc{$\top$}}
211 \newcommand{\mycoe}{\myfun{coe}}
212 \newcommand{\mycoee}[4]{\myapp{\myapp{\myapp{\myapp{\mycoe}{#1}}{#2}}{#3}}{#4}}
213 \newcommand{\mycoh}{\myfun{coh}}
214 \newcommand{\mycohh}[4]{\myapp{\myapp{\myapp{\myapp{\mycoh}{#1}}{#2}}{#3}}{#4}}
215 \newcommand{\myjm}[4]{(#1 {:} #2) \mathrel{\mytyc{=}} (#3 {:} #4)}
216 \newcommand{\myeq}{\mathrel{\mytyc{=}}}
217 \newcommand{\myprop}{\mytyc{Prop}}
218 \newcommand{\mytmup}{\mytmsyn\uparrow}
219 \newcommand{\mydefs}{\Delta}
220 \newcommand{\mynf}{\Downarrow}
221 \newcommand{\myinff}[3]{#1 \vdash #2 \Uparrow #3}
222 \newcommand{\myinf}[2]{\myinff{\myctx}{#1}{#2}}
223 \newcommand{\mychkk}[3]{#1 \vdash #2 \Downarrow #3}
224 \newcommand{\mychk}[2]{\mychkk{\myctx}{#1}{#2}}
225 \newcommand{\myann}[2]{#1 : #2}
226 \newcommand{\mydeclsyn}{\myse{decl}}
227 \newcommand{\myval}[3]{#1 : #2 \mapsto #3}
228 \newcommand{\mypost}[2]{\mysyn{abstract}\ #1 : #2}
229 \newcommand{\myadt}[4]{\mysyn{data}\ #1 #2\ \mysyn{where}\ #3\{ #4 \}}
230 \newcommand{\myreco}[4]{\mysyn{record}\ #1 #2\ \mysyn{where}\ \{ #4 \}}
231 \newcommand{\myelabt}{\vdash}
232 \newcommand{\myelabf}{\rhd}
233 \newcommand{\myelab}[2]{\myctx \myelabt #1 \myelabf #2}
234 \newcommand{\mytele}{\Delta}
235 \newcommand{\mytelee}{\delta}
236 \newcommand{\mydcctx}{\Gamma}
237 \newcommand{\mynamesyn}{\myse{name}}
238 \newcommand{\myvec}{\overrightarrow}
239 \newcommand{\mymeta}{\textsc}
240 \newcommand{\myhyps}{\mymeta{hyps}}
241 \newcommand{\mycc}{;}
242 \newcommand{\myemptytele}{\varepsilon}
243 \newcommand{\mymetagoes}{\Longrightarrow}
244 % \newcommand{\mytesctx}{\
245 \newcommand{\mytelesyn}{\myse{telescope}}
246 \newcommand{\myrecs}{\mymeta{recs}}
247 \newcommand{\myle}{\mathrel{\lcfun{$\le$}}}
248 \newcommand{\mylet}{\mysyn{let}}
249 \newcommand{\myhead}{\mymeta{head}}
250 \newcommand{\mytake}{\mymeta{take}}
251 \newcommand{\myix}{\mymeta{ix}}
252 \newcommand{\myapply}{\mymeta{apply}}
253 \newcommand{\mydataty}{\mymeta{datatype}}
254 \newcommand{\myisreco}{\mymeta{record}}
255 \newcommand{\mydcsep}{\ |\ }
256 \newcommand{\mytree}{\mytyc{Tree}}
257 \newcommand{\myproj}[1]{\myfun{$\pi_{#1}$}}
258 \newcommand{\mysigma}{\mytyc{$\Sigma$}}
259 \newcommand{\mynegder}{\vspace{-0.3cm}}
260 \newcommand{\myquot}{\Uparrow}
261 \newcommand{\mynquot}{\, \Downarrow}
262 \newcommand{\mycanquot}{\ensuremath{\textsc{quote}{\Uparrow}}}
263 \newcommand{\myneuquot}{\ensuremath{\textsc{quote}{\Downarrow}}}
264 \newcommand{\mymetaguard}{\ |\ }
265 \newcommand{\mybox}{\Box}
267 \renewcommand{\[}{\begin{equation*}}
268 \renewcommand{\]}{\end{equation*}}
269 \newcommand{\mymacol}[2]{\text{\textcolor{#1}{$#2$}}}
271 \newtheorem*{mydef}{Definition}
272 \newtheoremstyle{named}{}{}{\itshape}{}{\bfseries}{}{.5em}{\textsc{#1}}
275 %% -----------------------------------------------------------------------------
277 \title{\mykant: Implementing Observational Equality}
278 \author{Francesco Mazzoli \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{<fm2209@ic.ac.uk>}}}
292 % Upper part of the page. The '~' is needed because \\
293 % only works if a paragraph has started.
294 \includegraphics[width=0.4\textwidth]{brouwer-cropped.png}~\\[1cm]
296 \textsc{\Large Final year project}\\[0.5cm]
299 { \huge \mykant: Implementing Observational Equality}\\[1.5cm]
301 {\Large Francesco \textsc{Mazzoli} \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{<fm2209@ic.ac.uk>}}}\\[0.8cm]
303 \begin{minipage}{0.4\textwidth}
304 \begin{flushleft} \large
306 Dr. Steffen \textsc{van Bakel}
309 \begin{minipage}{0.4\textwidth}
310 \begin{flushright} \large
311 \emph{Second marker:} \\
312 Dr. Philippa \textsc{Gardner}
324 The marriage between programming and logic has been a very fertile
325 one. In particular, since the definition of the simply typed lambda
326 calculus, a number of type systems have been devised with increasing
329 Among this systems, Inutitionistic Type Theory (ITT) has been a very
330 popular framework for theorem provers and programming languages.
331 However, reasoning about equality has always been a tricky business in
332 ITT and related theories. In this thesis we will explain why this is
333 the case, and present Observational Type Theory (OTT), a solution to
334 some of the problems with equality.
336 To bring OTT closer to the current practice of interactive theorem
337 provers, we describe \mykant, a system featuring OTT in a setting more
338 close to the one found in widely used provers such as Agda and Coq.
339 Nost notably, we feature used defined inductive and record types and a
340 cumulative, implicit type hierarchy. Having implemented part of
341 $\mykant$ as a Haskell program, we describe some of the implementation
347 \renewcommand{\abstractname}{Acknowledgements}
349 I would like to thank Steffen van Bakel, my supervisor, who was brave
350 enough to believe in my project and who provided much advice and
353 I would also like to thank the Haskell and Agda community on
354 \texttt{IRC}, which guided me through the strange world of types; and
355 in particular Andrea Vezzosi and James Deikun, with whom I entertained
356 countless insightful discussions over the past year. Andrea suggested
357 Observational Type Theory as a topic of study: this thesis would not
358 exist without him. Before them, Tony Field introduced me to Haskell,
359 unknowingly filling most of my free time from that time on.
361 Finally, much of the work stems from the research of Conor McBride,
362 who answered many of my doubts through these months. I also owe him
372 \section{Introduction}
374 \section{Simple and not-so-simple types}
377 \subsection{The untyped $\lambda$-calculus}
380 Along with Turing's machines, the earliest attempts to formalise computation
381 lead to the $\lambda$-calculus \citep{Church1936}. This early programming
382 language encodes computation with a minimal syntax and no `data' in the
383 traditional sense, but just functions. Here we give a brief overview of the
384 language, which will give the chance to introduce concepts central to the
385 analysis of all the following calculi. The exposition follows the one found in
386 chapter 5 of \cite{Queinnec2003}.
388 \begin{mydef}[$\lambda$-terms]
389 Syntax of the $\lambda$-calculus: variables, abstractions, and
395 \begin{array}{r@{\ }c@{\ }l}
396 \mytmsyn & ::= & \myb{x} \mysynsep \myabs{\myb{x}}{\mytmsyn} \mysynsep (\myapp{\mytmsyn}{\mytmsyn}) \\
397 x & \in & \text{Some enumerable set of symbols}
402 Parenthesis will be omitted in the usual way, with application being
405 Abstractions roughly corresponds to functions, and their semantics is more
406 formally explained by the $\beta$-reduction rule.
408 \begin{mydef}[$\beta$-reduction]
409 $\beta$-reduction and substitution for the $\lambda$-calculus.
412 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
415 \myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{\myb{x}}{\mytmn}\text{, where} \\
417 \begin{array}{l@{\ }c@{\ }l}
418 \mysub{\myb{x}}{\myb{x}}{\mytmn} & = & \mytmn \\
419 \mysub{\myb{y}}{\myb{x}}{\mytmn} & = & y\text{, with } \myb{x} \neq y \\
420 \mysub{(\myapp{\mytmt}{\mytmm})}{\myb{x}}{\mytmn} & = & (\myapp{\mysub{\mytmt}{\myb{x}}{\mytmn}}{\mysub{\mytmm}{\myb{x}}{\mytmn}}) \\
421 \mysub{(\myabs{\myb{x}}{\mytmm})}{\myb{x}}{\mytmn} & = & \myabs{\myb{x}}{\mytmm} \\
422 \mysub{(\myabs{\myb{y}}{\mytmm})}{\myb{x}}{\mytmn} & = & \myabs{\myb{z}}{\mysub{\mysub{\mytmm}{\myb{y}}{\myb{z}}}{\myb{x}}{\mytmn}}, \\
423 \multicolumn{3}{l}{\myind{2} \text{with $\myb{x} \neq \myb{y}$ and $\myb{z}$ not free in $\myapp{\mytmm}{\mytmn}$}}
429 The care required during substituting variables for terms is required to avoid
430 name capturing. We will use substitution in the future for other name-binding
431 constructs assuming similar precautions.
433 These few elements have a remarkable expressiveness, and are in fact
434 Turing complete. As a corollary, we must be able to devise a term that
435 reduces forever (`loops' in imperative terms):
437 (\myapp{\omega}{\omega}) \myred (\myapp{\omega}{\omega}) \myred \cdots \text{, with $\omega = \myabs{x}{\myapp{x}{x}}$}
440 A \emph{redex} is a term that can be reduced.
442 In the untyped $\lambda$-calculus this will be the case for an
443 application in which the first term is an abstraction, but in general we
444 call aterm reducible if it appears to the left of a reduction rule.
445 \begin{mydef}[normal form]
446 A term that contains no redexes is said to be in \emph{normal form}.
448 \begin{mydef}[normalising terms and systems]
449 Terms that reduce in a finite number of reduction steps to a normal
450 form are \emph{normalising}. A system in which all terms are
451 normalising is said to be have the \emph{normalisation property}, or
454 Given the reduction behaviour of $(\myapp{\omega}{\omega})$, it is clear
455 that the untyped $\lambda$-calculus does not have the normalisation
458 We have not presented reduction in an algorithmic way, but
459 \emph{evaluation strategies} can be employed to reduce term
460 systematically. Common evaluation strategies include \emph{call by
461 value} (or \emph{strict}), where arguments of abstractions are reduced
462 before being applied to the abstraction; and conversely \emph{call by
463 name} (or \emph{lazy}), where we reduce only when we need to do so to
464 proceed---in other words when we have an application where the function
465 is still not a $\lambda$. In both these reduction strategies we never
466 reduce under an abstraction: for this reason a weaker form of
467 normalisation is used, where both abstractions and normal forms are said
468 to be in \emph{weak head normal form}.
470 \subsection{The simply typed $\lambda$-calculus}
472 A convenient way to `discipline' and reason about $\lambda$-terms is to assign
473 \emph{types} to them, and then check that the terms that we are forming make
474 sense given our typing rules \citep{Curry1934}.The first most basic instance
475 of this idea takes the name of \emph{simply typed $\lambda$-calculus} (STLC).
476 \begin{mydef}[Simply typed $\lambda$-calculus]
477 The syntax and typing rules for the STLC are given in Figure \ref{fig:stlc}.
480 Our types contain a set of \emph{type variables} $\Phi$, which might
481 correspond to some `primitive' types; and $\myarr$, the type former for
482 `arrow' types, the types of functions. The language is explicitly
483 typed: when we bring a variable into scope with an abstraction, we
484 declare its type. Reduction is unchanged from the untyped
490 \begin{array}{r@{\ }c@{\ }l}
491 \mytmsyn & ::= & \myb{x} \mysynsep \myabss{\myb{x}}{\mytysyn}{\mytmsyn} \mysynsep
492 (\myapp{\mytmsyn}{\mytmsyn}) \\
493 \mytysyn & ::= & \myse{\phi} \mysynsep \mytysyn \myarr \mytysyn \mysynsep \\
494 \myb{x} & \in & \text{Some enumerable set of symbols} \\
495 \myse{\phi} & \in & \Phi
500 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
502 \AxiomC{$\myctx(x) = A$}
503 \UnaryInfC{$\myjud{\myb{x}}{A}$}
506 \AxiomC{$\myjudd{\myctx;\myb{x} : A}{\mytmt}{\mytyb}$}
507 \UnaryInfC{$\myjud{\myabss{x}{A}{\mytmt}}{\mytyb}$}
510 \AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$}
511 \AxiomC{$\myjud{\mytmn}{\mytya}$}
512 \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mytyb}$}
516 \caption{Syntax and typing rules for the STLC. Reduction is unchanged from
517 the untyped $\lambda$-calculus.}
521 In the typing rules, a context $\myctx$ is used to store the types of bound
522 variables: $\myctx; \myb{x} : \mytya$ adds a variable to the context and
523 $\myctx(x)$ extracts the type of the rightmost occurrence of $x$.
525 This typing system takes the name of `simply typed lambda calculus' (STLC), and
526 enjoys a number of properties. Two of them are expected in most type systems
528 \begin{mydef}[Progress]
529 A well-typed term is not stuck---it is either a variable, or it
530 does not appear on the left of the $\myred$ relation (currently
531 only $\lambda$), or it can take a step according to the evaluation rules.
533 \begin{mydef}[Subject reduction]
534 If a well-typed term takes a step of evaluation, then the
535 resulting term is also well-typed, and preserves the previous type.
538 However, STLC buys us much more: every well-typed term is normalising
539 \citep{Tait1967}. It is easy to see that we cannot fill the blanks if we want to
540 give types to the non-normalising term shown before:
542 \myapp{(\myabss{\myb{x}}{\myhole{?}}{\myapp{\myb{x}}{\myb{x}}})}{(\myabss{\myb{x}}{\myhole{?}}{\myapp{\myb{x}}{\myb{x}}})}
545 This makes the STLC Turing incomplete. We can recover the ability to loop by
546 adding a combinator that recurses:
547 \begin{mydef}[Fixed-point combinator]\end{mydef}
550 \begin{minipage}{0.5\textwidth}
552 $ \mytmsyn ::= \cdots b \mysynsep \myfix{\myb{x}}{\mytysyn}{\mytmsyn} $
556 \begin{minipage}{0.5\textwidth}
557 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}} {
558 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytmt}{\mytya}$}
559 \UnaryInfC{$\myjud{\myfix{\myb{x}}{\mytya}{\mytmt}}{\mytya}$}
564 \mydesc{reduction:}{\myjud{\mytmsyn}{\mytmsyn}}{
565 $ \myfix{\myb{x}}{\mytya}{\mytmt} \myred \mysub{\mytmt}{\myb{x}}{(\myfix{\myb{x}}{\mytya}{\mytmt})}$
568 This will deprive us of normalisation, which is a particularly bad thing if we
569 want to use the STLC as described in the next section.
571 \subsection{The Curry-Howard correspondence}
573 It turns out that the STLC can be seen a natural deduction system for
574 intuitionistic propositional logic. Terms correspond to proofs, and
575 their types correspond to the propositions they prove. This remarkable
576 fact is known as the Curry-Howard correspondence, or isomorphism.
578 The arrow ($\myarr$) type corresponds to implication. If we wish to prove that
579 that $(\mytya \myarr \mytyb) \myarr (\mytyb \myarr \mytycc) \myarr (\mytya
580 \myarr \mytycc)$, all we need to do is to devise a $\lambda$-term that has the
583 \myabss{\myb{f}}{(\mytya \myarr \mytyb)}{\myabss{\myb{g}}{(\mytyb \myarr \mytycc)}{\myabss{\myb{x}}{\mytya}{\myapp{\myb{g}}{(\myapp{\myb{f}}{\myb{x}})}}}}
585 Which is known to functional programmers as function composition. Going
586 beyond arrow types, we can extend our bare lambda calculus with useful
587 types to represent other logical constructs.
588 \begin{mydef}[The extended STLC]
589 Figure \ref{fig:natded} shows syntax, reduction, and typing rules for
590 the \emph{extendend simply typed $\lambda$-calculus}.
596 \begin{array}{r@{\ }c@{\ }l}
597 \mytmsyn & ::= & \cdots \\
598 & | & \mytt \mysynsep \myapp{\myabsurd{\mytysyn}}{\mytmsyn} \\
599 & | & \myapp{\myleft{\mytysyn}}{\mytmsyn} \mysynsep
600 \myapp{\myright{\mytysyn}}{\mytmsyn} \mysynsep
601 \myapp{\mycase{\mytmsyn}{\mytmsyn}}{\mytmsyn} \\
602 & | & \mypair{\mytmsyn}{\mytmsyn} \mysynsep
603 \myapp{\myfst}{\mytmsyn} \mysynsep \myapp{\mysnd}{\mytmsyn} \\
604 \mytysyn & ::= & \cdots \mysynsep \myunit \mysynsep \myempty \mysynsep \mytmsyn \mysum \mytmsyn \mysynsep \mytysyn \myprod \mytysyn
609 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
612 \begin{array}{l@{ }l@{\ }c@{\ }l}
613 \myapp{\mycase{\mytmm}{\mytmn}}{(\myapp{\myleft{\mytya} &}{\mytmt})} & \myred &
614 \myapp{\mytmm}{\mytmt} \\
615 \myapp{\mycase{\mytmm}{\mytmn}}{(\myapp{\myright{\mytya} &}{\mytmt})} & \myred &
616 \myapp{\mytmn}{\mytmt}
621 \begin{array}{l@{ }l@{\ }c@{\ }l}
622 \myapp{\myfst &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmm \\
623 \myapp{\mysnd &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmn
629 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
631 \AxiomC{\phantom{$\myjud{\mytmt}{\myempty}$}}
632 \UnaryInfC{$\myjud{\mytt}{\myunit}$}
635 \AxiomC{$\myjud{\mytmt}{\myempty}$}
636 \UnaryInfC{$\myjud{\myapp{\myabsurd{\mytya}}{\mytmt}}{\mytya}$}
643 \AxiomC{$\myjud{\mytmt}{\mytya}$}
644 \UnaryInfC{$\myjud{\myapp{\myleft{\mytyb}}{\mytmt}}{\mytya \mysum \mytyb}$}
647 \AxiomC{$\myjud{\mytmt}{\mytyb}$}
648 \UnaryInfC{$\myjud{\myapp{\myright{\mytya}}{\mytmt}}{\mytya \mysum \mytyb}$}
656 \AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$}
657 \AxiomC{$\myjud{\mytmn}{\mytya \myarr \mytycc}$}
658 \AxiomC{$\myjud{\mytmt}{\mytya \mysum \mytyb}$}
659 \TrinaryInfC{$\myjud{\myapp{\mycase{\mytmm}{\mytmn}}{\mytmt}}{\mytycc}$}
666 \AxiomC{$\myjud{\mytmm}{\mytya}$}
667 \AxiomC{$\myjud{\mytmn}{\mytyb}$}
668 \BinaryInfC{$\myjud{\mypair{\mytmm}{\mytmn}}{\mytya \myprod \mytyb}$}
671 \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
672 \UnaryInfC{$\myjud{\myapp{\myfst}{\mytmt}}{\mytya}$}
675 \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
676 \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mytyb}$}
680 \caption{Rules for the extendend STLC. Only the new features are shown, all the
681 rules and syntax for the STLC apply here too.}
685 Tagged unions (or sums, or coproducts---$\mysum$ here, \texttt{Either}
686 in Haskell) correspond to disjunctions, and dually tuples (or pairs, or
687 products---$\myprod$ here, tuples in Haskell) correspond to
688 conjunctions. This is apparent looking at the ways to construct and
689 destruct the values inhabiting those types: for $\mysum$ $\myleft{ }$
690 and $\myright{ }$ correspond to $\vee$ introduction, and
691 $\mycase{\myarg}{\myarg}$ to $\vee$ elimination; for $\myprod$
692 $\mypair{\myarg}{\myarg}$ corresponds to $\wedge$ introduction, $\myfst$
693 and $\mysnd$ to $\wedge$ elimination.
695 The trivial type $\myunit$ corresponds to the logical $\top$ (true), and
696 dually $\myempty$ corresponds to the logical $\bot$ (false). $\myunit$
697 has one introduction rule ($\mytt$), and thus one inhabitant; and no
698 eliminators. $\myempty$ has no introduction rules, and thus no
699 inhabitants; and one eliminator ($\myabsurd{ }$), corresponding to the
700 logical \emph{ex falso quodlibet}.
702 With these rules, our STLC now looks remarkably similar in power and use to the
703 natural deduction we already know.
704 \begin{mydef}[Negation]
705 $\myneg \mytya$ can be expressed as $\mytya \myarr \myempty$.
707 However, there is an important omission: there is no term of
708 the type $\mytya \mysum \myneg \mytya$ (excluded middle), or equivalently
709 $\myneg \myneg \mytya \myarr \mytya$ (double negation), or indeed any term with
710 a type equivalent to those.
712 This has a considerable effect on our logic and it is no coincidence, since there
713 is no obvious computational behaviour for laws like the excluded middle.
714 Logics of this kind are called \emph{intuitionistic}, or \emph{constructive},
715 and all the systems analysed will have this characteristic since they build on
716 the foundation of the STLC.\footnote{There is research to give computational
717 behaviour to classical logic, but I will not touch those subjects.}
719 As in logic, if we want to keep our system consistent, we must make sure that no
720 closed terms (in other words terms not under a $\lambda$) inhabit $\myempty$.
721 The variant of STLC presented here is indeed
722 consistent, a result that follows from the fact that it is
724 Going back to our $\mysyn{fix}$ combinator, it is easy to see how it ruins our
725 desire for consistency. The following term works for every type $\mytya$,
727 \[(\myfix{\myb{x}}{\mytya}{\myb{x}}) : \mytya\]
729 \subsection{Inductive data}
732 To make the STLC more useful as a programming language or reasoning tool it is
733 common to include (or let the user define) inductive data types. These comprise
734 of a type former, various constructors, and an eliminator (or destructor) that
735 serves as primitive recursor.
737 \begin{mydef}[Finite lists for the STLC]
738 We add a $\mylist$ type constructor, along with an `empty
739 list' ($\mynil{ }$) and `cons cell' ($\mycons$) constructor. The eliminator for
740 lists will be the usual folding operation ($\myfoldr$). Full rules in Figure
747 \begin{array}{r@{\ }c@{\ }l}
748 \mytmsyn & ::= & \cdots \mysynsep \mynil{\mytysyn} \mysynsep \mytmsyn \mycons \mytmsyn
750 \myapp{\myapp{\myapp{\myfoldr}{\mytmsyn}}{\mytmsyn}}{\mytmsyn} \\
751 \mytysyn & ::= & \cdots \mysynsep \myapp{\mylist}{\mytysyn}
755 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
757 \begin{array}{l@{\ }c@{\ }l}
758 \myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{\mynil{\mytya}} & \myred & \mytmt \\
760 \myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{(\mytmm \mycons \mytmn)} & \myred &
761 \myapp{\myapp{\myse{f}}{\mytmm}}{(\myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{\mytmn})}
765 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
767 \AxiomC{\phantom{$\myjud{\mytmm}{\mytya}$}}
768 \UnaryInfC{$\myjud{\mynil{\mytya}}{\myapp{\mylist}{\mytya}}$}
771 \AxiomC{$\myjud{\mytmm}{\mytya}$}
772 \AxiomC{$\myjud{\mytmn}{\myapp{\mylist}{\mytya}}$}
773 \BinaryInfC{$\myjud{\mytmm \mycons \mytmn}{\myapp{\mylist}{\mytya}}$}
778 \AxiomC{$\myjud{\mysynel{f}}{\mytya \myarr \mytyb \myarr \mytyb}$}
779 \AxiomC{$\myjud{\mytmm}{\mytyb}$}
780 \AxiomC{$\myjud{\mytmn}{\myapp{\mylist}{\mytya}}$}
781 \TrinaryInfC{$\myjud{\myapp{\myapp{\myapp{\myfoldr}{\mysynel{f}}}{\mytmm}}{\mytmn}}{\mytyb}$}
784 \caption{Rules for lists in the STLC.}
788 In Section \ref{sec:well-order} we will see how to give a general account of
791 \section{Intuitionistic Type Theory}
794 \subsection{Extending the STLC}
796 The STLC can be made more expressive in various ways. \cite{Barendregt1991}
797 succinctly expressed geometrically how we can add expressivity:
800 & \lambda\omega \ar@{-}[rr]\ar@{-}'[d][dd]
801 & & \lambda C \ar@{-}[dd]
803 \lambda2 \ar@{-}[ur]\ar@{-}[rr]\ar@{-}[dd]
804 & & \lambda P2 \ar@{-}[ur]\ar@{-}[dd]
806 & \lambda\underline\omega \ar@{-}'[r][rr]
807 & & \lambda P\underline\omega
809 \lambda{\to} \ar@{-}[rr]\ar@{-}[ur]
810 & & \lambda P \ar@{-}[ur]
813 Here $\lambda{\to}$, in the bottom left, is the STLC. From there can move along
816 \item[Terms depending on types (towards $\lambda{2}$)] We can quantify over
817 types in our type signatures. For example, we can define a polymorphic
818 identity function, where $\mytyp$ denotes the `type of types':
820 (\myabss{\myb{A}}{\mytyp}{\myabss{\myb{x}}{\myb{A}}{\myb{x}}}) : (\myb{A} {:} \mytyp) \myarr \myb{A} \myarr \myb{A}
822 The first and most famous instance of this idea has been System F.
823 This form of polymorphism and has been wildly successful, also thanks
824 to a well known inference algorithm for a restricted version of System
825 F known as Hindley-Milner \citep{milner1978theory}. Languages like
826 Haskell and SML are based on this discipline.
827 \item[Types depending on types (towards $\lambda{\underline{\omega}}$)] We have
828 type operators. For example we could define a function that given types $R$
829 and $\mytya$ forms the type that represents a value of type $\mytya$ in
830 continuation passing style:
831 \[\displaystyle(\myabss{\myb{A} \myar \myb{R}}{\mytyp}{(\myb{A}
832 \myarr \myb{R}) \myarr \myb{R}}) : \mytyp \myarr \mytyp \myarr \mytyp
834 \item[Types depending on terms (towards $\lambda{P}$)] Also known as `dependent
835 types', give great expressive power. For example, we can have values of whose
836 type depend on a boolean:
837 \[\displaystyle(\myabss{\myb{x}}{\mybool}{\myite{\myb{x}}{\mynat}{\myrat}}) : \mybool
841 All the systems preserve the properties that make the STLC well behaved. The
842 system we are going to focus on, Intuitionistic Type Theory, has all of the
843 above additions, and thus would sit where $\lambda{C}$ sits in the
844 `$\lambda$-cube'. It will serve as the logical `core' of all the other
845 extensions that we will present and ultimately our implementation of a similar
848 \subsection{A Bit of History}
850 Logic frameworks and programming languages based on type theory have a
851 long history. Per Martin-L\"{o}f described the first version of his
852 theory in 1971, but then revised it since the original version was
853 inconsistent due to its impredicativity.\footnote{In the early version
854 there was only one universe $\mytyp$ and $\mytyp : \mytyp$; see
855 Section \ref{sec:term-types} for an explanation on why this causes
856 problems.} For this reason he later gave a revised and consistent
857 definition \citep{Martin-Lof1984}.
859 A related development is the polymorphic $\lambda$-calculus, and specifically
860 the previously mentioned System F, which was developed independently by Girard
861 and Reynolds. An overview can be found in \citep{Reynolds1994}. The surprising
862 fact is that while System F is impredicative it is still consistent and strongly
863 normalising. \cite{Coquand1986} further extended this line of work with the
864 Calculus of Constructions (CoC).
866 Most widely used interactive theorem provers are based on ITT. Popular ones
867 include Agda \citep{Norell2007, Bove2009}, Coq \citep{Coq}, and Epigram
868 \citep{McBride2004, EpigramTut}.
870 \subsection{A simple type theory}
873 The calculus I present follows the exposition in \citep{Thompson1991},
874 and is quite close to the original formulation of predicative ITT as
875 found in \citep{Martin-Lof1984}.
876 \begin{mydef}[Intuitionistic Type Theory (ITT)]
877 The syntax and reduction rules are shown in Figure \ref{fig:core-tt-syn}.
878 The typing rules are presented piece by piece in the following sections.
880 Agda and \mykant\ renditions of the presented theory and all the
881 examples is reproduced in Appendix \ref{app:itt-code}.
886 \begin{array}{r@{\ }c@{\ }l}
887 \mytmsyn & ::= & \myb{x} \mysynsep
888 \mytyp_{level} \mysynsep
889 \myunit \mysynsep \mytt \mysynsep
890 \myempty \mysynsep \myapp{\myabsurd{\mytmsyn}}{\mytmsyn} \\
891 & | & \mybool \mysynsep \mytrue \mysynsep \myfalse \mysynsep
892 \myitee{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
893 & | & \myfora{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
894 \myabss{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
895 (\myapp{\mytmsyn}{\mytmsyn}) \\
896 & | & \myexi{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
897 \mypairr{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn} \\
898 & | & \myapp{\myfst}{\mytmsyn} \mysynsep \myapp{\mysnd}{\mytmsyn} \\
899 & | & \myw{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
900 \mytmsyn \mynode{\myb{x}}{\mytmsyn} \mytmsyn \\
901 & | & \myrec{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn} \\
902 level & \in & \mathbb{N}
907 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
910 \begin{array}{l@{ }l@{\ }c@{\ }l}
911 \myitee{\mytrue &}{\myb{x}}{\myse{P}}{\mytmm}{\mytmn} & \myred & \mytmm \\
912 \myitee{\myfalse &}{\myb{x}}{\myse{P}}{\mytmm}{\mytmn} & \myred & \mytmn \\
917 \myapp{(\myabss{\myb{x}}{\mytya}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{\myb{x}}{\mytmn}
921 \begin{array}{l@{ }l@{\ }c@{\ }l}
922 \myapp{\myfst &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmm \\
923 \myapp{\mysnd &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmn
931 \myrec{(\myse{s} \mynode{\myb{x}}{\myse{T}} \myse{f})}{\myb{y}}{\myse{P}}{\myse{p}} \myred
932 \myapp{\myapp{\myapp{\myse{p}}{\myse{s}}}{\myse{f}}}{(\myabss{\myb{t}}{\mysub{\myse{T}}{\myb{x}}{\myse{s}}}{
933 \myrec{\myapp{\myse{f}}{\myb{t}}}{\myb{y}}{\myse{P}}{\mytmt}
937 \caption{Syntax and reduction rules for our type theory.}
938 \label{fig:core-tt-syn}
941 \subsubsection{Types are terms, some terms are types}
942 \label{sec:term-types}
944 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
946 \AxiomC{$\myjud{\mytmt}{\mytya}$}
947 \AxiomC{$\mytya \mydefeq \mytyb$}
948 \BinaryInfC{$\myjud{\mytmt}{\mytyb}$}
951 \AxiomC{\phantom{$\myjud{\mytmt}{\mytya}$}}
952 \UnaryInfC{$\myjud{\mytyp_l}{\mytyp_{l + 1}}$}
957 The first thing to notice is that a barrier between values and types that we had
958 in the STLC is gone: values can appear in types, and the two are treated
959 uniformly in the syntax.
961 While the usefulness of doing this will become clear soon, a consequence is
962 that since types can be the result of computation, deciding type equality is
963 not immediate as in the STLC. For this reason we define \emph{definitional
964 equality}, $\mydefeq$, as the congruence relation extending
965 $\myred$---moreover, when comparing types syntactically we do it up to
966 renaming of bound names ($\alpha$-renaming). For example under this
967 discipline we will find that
969 \myabss{\myb{x}}{\mytya}{\myb{x}} \mydefeq \myabss{\myb{y}}{\mytya}{\myb{y}}
971 Types that are definitionally equal can be used interchangeably. Here
972 the `conversion' rule is not syntax directed, but it is possible to
973 employ $\myred$ to decide term equality in a systematic way, by
974 comparing terms by reducing to their normal forms and then comparing
975 them syntactically; so that a separate conversion rule is not needed.
976 Another thing to notice is that considering the need to reduce terms to
977 decide equality it is essential for a dependently typed system to be
978 terminating and confluent for type checking to be decidable, since every
979 type needs to have a \emph{unique} normal form.
981 Moreover, we specify a \emph{type hierarchy} to talk about `large'
982 types: $\mytyp_0$ will be the type of types inhabited by data:
983 $\mybool$, $\mynat$, $\mylist$, etc. $\mytyp_1$ will be the type of
984 $\mytyp_0$, and so on---for example we have $\mytrue : \mybool :
985 \mytyp_0 : \mytyp_1 : \cdots$. Each type `level' is often called a
986 universe in the literature. While it is possible to simplify things by
987 having only one universe $\mytyp$ with $\mytyp : \mytyp$, this plan is
988 inconsistent for much the same reason that impredicative na\"{\i}ve set
989 theory is \citep{Hurkens1995}. However various techniques can be
990 employed to lift the burden of explicitly handling universes, as we will
991 see in Section \ref{sec:term-hierarchy}.
993 \subsubsection{Contexts}
995 \begin{minipage}{0.5\textwidth}
996 \mydesc{context validity:}{\myvalid{\myctx}}{
998 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
999 \UnaryInfC{$\myvalid{\myemptyctx}$}
1002 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
1003 \UnaryInfC{$\myvalid{\myctx ; \myb{x} : \mytya}$}
1008 \begin{minipage}{0.5\textwidth}
1009 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1010 \AxiomC{$\myctx(x) = \mytya$}
1011 \UnaryInfC{$\myjud{\myb{x}}{\mytya}$}
1017 We need to refine the notion context to make sure that every variable appearing
1018 is typed correctly, or that in other words each type appearing in the context is
1019 indeed a type and not a value. In every other rule, if no premises are present,
1020 we assume the context in the conclusion to be valid.
1022 Then we can re-introduce the old rule to get the type of a variable for a
1025 \subsubsection{$\myunit$, $\myempty$}
1027 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1028 \begin{tabular}{ccc}
1029 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
1030 \UnaryInfC{$\myjud{\myunit}{\mytyp_0}$}
1032 \UnaryInfC{$\myjud{\myempty}{\mytyp_0}$}
1035 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
1036 \UnaryInfC{$\myjud{\mytt}{\myunit}$}
1038 \UnaryInfC{\phantom{$\myjud{\myempty}{\mytyp_0}$}}
1041 \AxiomC{$\myjud{\mytmt}{\myempty}$}
1042 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
1043 \BinaryInfC{$\myjud{\myapp{\myabsurd{\mytya}}{\mytmt}}{\mytya}$}
1045 \UnaryInfC{\phantom{$\myjud{\myempty}{\mytyp_0}$}}
1050 Nothing surprising here: $\myunit$ and $\myempty$ are unchanged from the STLC,
1051 with the added rules to type $\myunit$ and $\myempty$ themselves, and to make
1052 sure that we are invoking $\myabsurd{}$ over a type.
1054 \subsubsection{$\mybool$, and dependent $\myfun{if}$}
1056 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1057 \begin{tabular}{ccc}
1059 \UnaryInfC{$\myjud{\mybool}{\mytyp_0}$}
1063 \UnaryInfC{$\myjud{\mytrue}{\mybool}$}
1067 \UnaryInfC{$\myjud{\myfalse}{\mybool}$}
1072 \AxiomC{$\myjud{\mytmt}{\mybool}$}
1073 \AxiomC{$\myjudd{\myctx : \mybool}{\mytya}{\mytyp_l}$}
1075 \BinaryInfC{$\myjud{\mytmm}{\mysub{\mytya}{x}{\mytrue}}$ \hspace{0.7cm} $\myjud{\mytmn}{\mysub{\mytya}{x}{\myfalse}}$}
1076 \UnaryInfC{$\myjud{\myitee{\mytmt}{\myb{x}}{\mytya}{\mytmm}{\mytmn}}{\mysub{\mytya}{\myb{x}}{\mytmt}}$}
1080 With booleans we get the first taste of the `dependent' in `dependent
1081 types'. While the two introduction rules for $\mytrue$ and $\myfalse$
1082 are not surprising, the typing rules for $\myfun{if}$ are. In most
1083 strongly typed languages we expect the branches of an $\myfun{if}$
1084 statements to be of the same type, to preserve subject reduction, since
1085 execution could take both paths. This is a pity, since the type system
1086 does not reflect the fact that in each branch we gain knowledge on the
1087 term we are branching on. Which means that programs along the lines of
1089 if null xs then head xs else 0
1091 are a necessary, well typed, danger.
1093 However, in a more expressive system, we can do better: the branches' type can
1094 depend on the value of the scrutinised boolean. This is what the typing rule
1095 expresses: the user provides a type $\mytya$ ranging over an $\myb{x}$
1096 representing the scrutinised boolean type, and the branches are typechecked with
1097 the updated knowledge on the value of $\myb{x}$.
1099 \subsubsection{$\myarr$, or dependent function}
1101 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1102 \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
1103 \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
1104 \BinaryInfC{$\myjud{\myfora{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
1110 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytmt}{\mytyb}$}
1111 \UnaryInfC{$\myjud{\myabss{\myb{x}}{\mytya}{\mytmt}}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
1114 \AxiomC{$\myjud{\mytmm}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
1115 \AxiomC{$\myjud{\mytmn}{\mytya}$}
1116 \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mysub{\mytyb}{\myb{x}}{\mytmn}}$}
1121 Dependent functions are one of the two key features that perhaps most
1122 characterise dependent types---the other being dependent products. With
1123 dependent functions, the result type can depend on the value of the
1124 argument. This feature, together with the fact that the result type
1125 might be a type itself, brings a lot of interesting possibilities.
1126 Following this intuition, in the introduction rule, the return type is
1127 typechecked in a context with an abstracted variable of lhs' type, and
1128 in the elimination rule the actual argument is substituted in the return
1129 type. Keeping the correspondence with logic alive, dependent functions
1130 are much like universal quantifiers ($\forall$) in logic.
1132 For example, assuming that we have lists and natural numbers in our
1133 language, using dependent functions we are write functions of type:
1136 \myfun{length} : (\myb{A} {:} \mytyp_0) \myarr \myapp{\mylist}{\myb{A}} \myarr \mynat \\
1137 \myarg \myfun{$>$} \myarg : \mynat \myarr \mynat \myarr \mytyp_0 \\
1138 \myfun{head} : (\myb{A} {:} \mytyp_0) \myarr (\myb{l} {:} \myapp{\mylist}{\myb{A}})
1139 \myarr \myapp{\myapp{\myfun{length}}{\myb{A}}}{\myb{l}} \mathrel{\myfun{$>$}} 0 \myarr
1144 \myfun{length} is the usual polymorphic length
1145 function. $\myarg\myfun{$>$}\myarg$ is a function that takes two naturals
1146 and returns a type: if the lhs is greater then the rhs, $\myunit$ is
1147 returned, $\myempty$ otherwise. This way, we can express a
1148 `non-emptyness' condition in $\myfun{head}$, by including a proof that
1149 the length of the list argument is non-zero. This allows us to rule out
1150 the `empty list' case, so that we can safely return the first element.
1152 Again, we need to make sure that the type hierarchy is respected, which
1153 is the reason why a type formed by $\myarr$ will live in the least upper
1154 bound of the levels of argument and return type. If this was not the
1155 case, we would be able to form a `powerset' function along the lines of
1158 \myfun{P} : \mytyp_0 \myarr \mytyp_0 \\
1159 \myfun{P} \myappsp \myb{A} \mapsto \myb{A} \myarr \mytyp_0
1162 Where the type of $\myb{A} \myarr \mytyp_0$ is in $\mytyp_0$ itself.
1163 Using this and similar devices we would be able to derive falsity
1164 \citep{Hurkens1995}. This trend will continue with the other type-level
1165 binders, $\myprod$ and $\mytyc{W}$.
1167 \subsubsection{$\myprod$, or dependent product}
1170 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1171 \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
1172 \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
1173 \BinaryInfC{$\myjud{\myexi{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
1179 \AxiomC{$\myjud{\mytmm}{\mytya}$}
1180 \AxiomC{$\myjud{\mytmn}{\mysub{\mytyb}{\myb{x}}{\mytmm}}$}
1181 \BinaryInfC{$\myjud{\mypairr{\mytmm}{\myb{x}}{\mytyb}{\mytmn}}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
1183 \UnaryInfC{\phantom{$--$}}
1186 \AxiomC{$\myjud{\mytmt}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
1187 \UnaryInfC{$\hspace{0.7cm}\myjud{\myapp{\myfst}{\mytmt}}{\mytya}\hspace{0.7cm}$}
1189 \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mysub{\mytyb}{\myb{x}}{\myapp{\myfst}{\mytmt}}}$}
1194 If dependent functions are a generalisation of $\myarr$ in the STLC,
1195 dependent products are a generalisation of $\myprod$ in the STLC. The
1196 improvement is that the second element's type can depend on the value of
1197 the first element. The corrispondence with logic is through the
1198 existential quantifier: $\exists x \in \mathbb{N}. even(x)$ can be
1199 expressed as $\myexi{\myb{x}}{\mynat}{\myapp{\myfun{even}}{\myb{x}}}$.
1200 The first element will be a number, and the second evidence that the
1201 number is even. This highlights the fact that we are working in a
1202 constructive logic: if we have an existence proof, we can always ask for
1203 a witness. This means, for instance, that $\neg \forall \neg$ is not
1204 equivalent to $\exists$.
1206 Another perhaps more `dependent' application of products, paired with
1207 $\mybool$, is to offer choice between different types. For example we
1208 can easily recover disjunctions:
1211 \myarg\myfun{$\vee$}\myarg : \mytyp_0 \myarr \mytyp_0 \myarr \mytyp_0 \\
1212 \myb{A} \mathrel{\myfun{$\vee$}} \myb{B} \mapsto \myexi{\myb{x}}{\mybool}{\myite{\myb{x}}{\myb{A}}{\myb{B}}} \\ \ \\
1213 \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} \\
1214 \myfun{case} \myappsp \myb{A} \myappsp \myb{B} \myappsp \myb{C} \myappsp \myb{f} \myappsp \myb{g} \myappsp \myb{x} \mapsto \\
1215 \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}})}
1219 \subsubsection{$\mytyc{W}$, or well-order}
1220 \label{sec:well-order}
1222 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1224 \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
1225 \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
1226 \BinaryInfC{$\myjud{\myw{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
1231 \AxiomC{$\myjud{\mytmt}{\mytya}$}
1232 \AxiomC{$\myjud{\mysynel{f}}{\mysub{\mytyb}{\myb{x}}{\mytmt} \myarr \myw{\myb{x}}{\mytya}{\mytyb}}$}
1233 \BinaryInfC{$\myjud{\mytmt \mynode{\myb{x}}{\mytyb} \myse{f}}{\myw{\myb{x}}{\mytya}{\mytyb}}$}
1239 \AxiomC{$\myjud{\myse{u}}{\myw{\myb{x}}{\myse{S}}{\myse{T}}}$}
1240 \AxiomC{$\myjudd{\myctx; \myb{w} : \myw{\myb{x}}{\myse{S}}{\myse{T}}}{\myse{P}}{\mytyp_l}$}
1242 \BinaryInfC{$\myjud{\myse{p}}{
1243 \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}}}}
1245 \UnaryInfC{$\myjud{\myrec{\myse{u}}{\myb{w}}{\myse{P}}{\myse{p}}}{\mysub{\myse{P}}{\myb{w}}{\myse{u}}}$}
1249 Finally, the well-order type, or in short $\mytyc{W}$-type, which will
1250 let us represent inductive data in a general (but clumsy) way. We can
1251 form `nodes' of the shape $\mytmt \mynode{\myb{x}}{\mytyb} \myse{f} :
1252 \myw{\myb{x}}{\mytya}{\mytyb}$ that contain data ($\mytmt$) of type and
1253 one `child' for each member of $\mysub{\mytyb}{\myb{x}}{\mytmt}$. The
1254 $\myfun{rec}\ \myfun{with}$ acts as an induction principle on
1255 $\mytyc{W}$, given a predicate an a function dealing with the inductive
1256 case---we will gain more intuition about inductive data in ITT in
1257 Section \ref{sec:user-type}.
1259 For example, if we want to form natural numbers, we can take
1262 \mytyc{Tr} : \mybool \myarr \mytyp_0 \\
1263 \mytyc{Tr} \myappsp \myb{b} \mapsto \myfun{if}\, \myb{b}\, \myunit\, \myfun{else}\, \myempty \\
1265 \mynat : \mytyp_0 \\
1266 \mynat \mapsto \myw{\myb{b}}{\mybool}{(\mytyc{Tr}\myappsp\myb{b})}
1269 Each node will contain a boolean. If $\mytrue$, the number is non-zero,
1270 and we will have one child representing its predecessor, given that
1271 $\mytyc{Tr}$ will return $\myunit$. If $\myfalse$, the number is zero,
1272 and we will have no predecessors (children), given the $\myempty$:
1275 \mydc{zero} : \mynat \\
1276 \mydc{zero} \mapsto \myfalse \mynodee (\myabs{\myb{z}}{\myabsurd{\mynat} \myappsp \myb{x}}) \\
1278 \mydc{suc} : \mynat \myarr \mynat \\
1279 \mydc{suc}\myappsp \myb{x} \mapsto \mytrue \mynodee (\myabs{\myarg}{\myb{x}})
1282 And with a bit of effort, we can recover addition:
1285 \myfun{plus} : \mynat \myarr \mynat \myarr \mynat \\
1286 \myfun{plus} \myappsp \myb{x} \myappsp \myb{y} \mapsto \\
1287 \myind{2} \myfun{rec}\, \myb{x} / \myb{b}.\mynat \, \\
1288 \myind{2} \myfun{with}\, \myabs{\myb{b}}{\\
1289 \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) \\
1290 \myind{2}\myind{2}\myfun{then}\,(\myabs{\myarg\, \myb{f}}{\mydc{suc}\myappsp (\myapp{\myb{f}}{\mytt})})\, \myfun{else}\, (\myabs{\myarg\, \myarg}{\myb{y}})}
1293 Note how we explicitly have to type the branches to make them
1294 match with the definition of $\mynat$---which gives a taste of the
1295 `clumsiness' of $\mytyc{W}$-types, which while useful as a reasoning
1296 tool are useless to the user modelling data types.
1298 \section{The struggle for equality}
1299 \label{sec:equality}
1301 In the previous section we saw how a type checker (or a human) needs a
1302 notion of \emph{definitional equality}. Beyond this meta-theoretic
1303 notion, in this section we will explore the ways of expressing equality
1304 \emph{inside} the theory, as a reasoning tool available to the user.
1305 This area is the main concern of this thesis, and in general a very
1306 active research topic, since we do not have a fully satisfactory
1307 solution, yet. As in the previous section, everything presented is
1308 formalised in Agda in Appendix \ref{app:agda-itt}.
1310 \subsection{Propositional equality}
1312 \begin{mydef}[Propositional equality] The syntax, reduction, and typing
1313 rules for propositional equality and related constructs is defined as:
1317 \begin{minipage}{0.5\textwidth}
1320 \begin{array}{r@{\ }c@{\ }l}
1321 \mytmsyn & ::= & \cdots \\
1322 & | & \mypeq \myappsp \mytmsyn \myappsp \mytmsyn \myappsp \mytmsyn \mysynsep
1323 \myapp{\myrefl}{\mytmsyn} \\
1324 & | & \myjeq{\mytmsyn}{\mytmsyn}{\mytmsyn}
1329 \begin{minipage}{0.5\textwidth}
1330 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
1332 \myjeq{\myse{P}}{(\myapp{\myrefl}{\mytmm})}{\mytmn} \myred \mytmn
1338 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1339 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
1340 \AxiomC{$\myjud{\mytmm}{\mytya}$}
1341 \AxiomC{$\myjud{\mytmn}{\mytya}$}
1342 \TrinaryInfC{$\myjud{\mypeq \myappsp \mytya \myappsp \mytmm \myappsp \mytmn}{\mytyp_l}$}
1348 \AxiomC{$\begin{array}{c}\ \\\myjud{\mytmm}{\mytya}\hspace{1.1cm}\mytmm \mydefeq \mytmn\end{array}$}
1349 \UnaryInfC{$\myjud{\myapp{\myrefl}{\mytmm}}{\mypeq \myappsp \mytya \myappsp \mytmm \myappsp \mytmn}$}
1354 \myjud{\myse{P}}{\myfora{\myb{x}\ \myb{y}}{\mytya}{\myfora{q}{\mypeq \myappsp \mytya \myappsp \myb{x} \myappsp \myb{y}}{\mytyp_l}}} \\
1355 \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})}}
1358 \UnaryInfC{$\myjud{\myjeq{\myse{P}}{\myse{q}}{\myse{p}}}{\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmn}}{q}}$}
1363 To express equality between two terms inside ITT, the obvious way to do
1364 so is to have equality to be a type. Here we present what has survived
1365 as the dominating form of equality in systems based on ITT up to the
1368 Our type former is $\mypeq$, which given a type (in this case
1369 $\mytya$) relates equal terms of that type. $\mypeq$ has one introduction
1370 rule, $\myrefl$, which introduces an equality relation between definitionally
1373 Finally, we have one eliminator for $\mypeq$, $\myjeqq$. $\myjeq{\myse{P}}{\myse{q}}{\myse{p}}$ takes
1375 \item $\myse{P}$, a predicate working with two terms of a certain type (say
1376 $\mytya$) and a proof of their equality
1377 \item $\myse{q}$, a proof that two terms in $\mytya$ (say $\myse{m}$ and
1378 $\myse{n}$) are equal
1379 \item and $\myse{p}$, an inhabitant of $\myse{P}$ applied to $\myse{m}$
1380 twice, plus the trivial proof by reflexivity showing that $\myse{m}$
1383 Given these ingredients, $\myjeqq$ retuns a member of $\myse{P}$ applied
1384 to $\mytmm$, $\mytmn$, and $\myse{q}$. In other words $\myjeqq$ takes a
1385 witness that $\myse{P}$ works with \emph{definitionally equal} terms,
1386 and returns a witness of $\myse{P}$ working with \emph{propositionally
1387 equal} terms. Invokations of $\myjeqq$ will vanish when the equality
1388 proofs will reduce to invocations to reflexivity, at which point the
1389 arguments must be definitionally equal, and thus the provided
1390 $\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmm}}{(\myapp{\myrefl}{\mytmm})}$
1391 can be returned. This means that $\myjeqq$ will not compute with
1392 hypotetical proofs, which makes sense given that they might be false.
1394 While the $\myjeqq$ rule is slightly convoluted, ve can derive many more
1395 `friendly' rules from it, for example a more obvious `substitution' rule, that
1396 replaces equal for equal in predicates:
1399 \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}}}}} \\
1400 \myfun{subst}\myappsp \myb{A}\myappsp\myb{P}\myappsp\myb{x}\myappsp\myb{y}\myappsp\myb{q}\myappsp\myb{p} \mapsto
1401 \myjeq{(\myabs{\myb{x}\ \myb{y}\ \myb{q}}{\myapp{\myb{P}}{\myb{y}}})}{\myb{p}}{\myb{q}}
1404 Once we have $\myfun{subst}$, we can easily prove more familiar laws regarding
1405 equality, such as symmetry, transitivity, congruence laws, etc.
1407 \subsection{Common extensions}
1409 Our definitional and propositional equalities can be enhanced in various
1410 ways. Obviously if we extend the definitional equality we are also
1411 automatically extend propositional equality, given how $\myrefl$ works.
1413 \subsubsection{$\eta$-expansion}
1414 \label{sec:eta-expand}
1416 A simple extension to our definitional equality is $\eta$-expansion.
1417 Given an abstract variable $\myb{f} : \mytya \myarr \mytyb$ the aim is
1418 to have that $\myb{f} \mydefeq
1419 \myabss{\myb{x}}{\mytya}{\myapp{\myb{f}}{\myb{x}}}$. We can achieve
1420 this by `expanding' terms based on their types, a process also known as
1421 \emph{quotation}---a term borrowed from the practice of
1422 \emph{normalisation by evaluation}, where we embed terms in some host
1423 language with an existing notion of computation, and then reify them
1424 back into terms, which will `smooth out' differences like the one above
1427 The same concept applies to $\myprod$, where we expand each inhabitant
1428 by reconstructing it by getting its projections, so that $\myb{x}
1429 \mydefeq \mypair{\myfst \myappsp \myb{x}}{\mysnd \myappsp \myb{x}}$.
1430 Similarly, all one inhabitants of $\myunit$ and all zero inhabitants of
1431 $\myempty$ can be considered equal. Quotation can be performed in a
1432 type-directed way, as we will witness in Section \ref{sec:kant-irr}.
1434 \begin{mydef}[Congruence and $\eta$-laws]
1435 To justify quotation in our type system we will add a congruence law
1436 for abstractions and a similar law for products, plus the fact that all
1437 elements of $\myunit$ or $\myempty$ are equal.
1440 \mydesc{definitional equality:}{\myjud{\mytmm \mydefeq \mytmn}{\mytmsyn}}{
1442 \AxiomC{$\myjudd{\myctx; \myb{y} : \mytya}{\myapp{\myse{f}}{\myb{x}} \mydefeq \myapp{\myse{g}}{\myb{x}}}{\mysub{\mytyb}{\myb{x}}{\myb{y}}}$}
1443 \UnaryInfC{$\myjud{\myse{f} \mydefeq \myse{g}}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
1446 \AxiomC{$\myjud{\mypair{\myapp{\myfst}{\mytmm}}{\myapp{\mysnd}{\mytmm}} \mydefeq \mypair{\myapp{\myfst}{\mytmn}}{\myapp{\mysnd}{\mytmn}}}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
1447 \UnaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
1454 \AxiomC{$\myjud{\mytmm}{\myunit}$}
1455 \AxiomC{$\myjud{\mytmn}{\myunit}$}
1456 \BinaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\myunit}$}
1459 \AxiomC{$\myjud{\mytmm}{\myempty}$}
1460 \AxiomC{$\myjud{\mytmn}{\myempty}$}
1461 \BinaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\myempty}$}
1466 \subsubsection{Uniqueness of identity proofs}
1468 Another common but controversial addition to propositional equality is
1469 the $\myfun{K}$ axiom, which essentially states that all equality proofs
1472 \begin{mydef}[$\myfun{K}$ axiom]\end{mydef}
1473 \mydesc{typing:}{\myjud{\mytmm \mydefeq \mytmn}{\mytmsyn}}{
1476 \myjud{\myse{P}}{\myfora{\myb{x}}{\mytya}{\myb{x} \mypeq{\mytya} \myb{x} \myarr \mytyp}} \\\
1477 \myjud{\mytmt}{\mytya} \hspace{1cm}
1478 \myjud{\myse{p}}{\myse{P} \myappsp \mytmt \myappsp (\myrefl \myappsp \mytmt)} \hspace{1cm}
1479 \myjud{\myse{q}}{\mytmt \mypeq{\mytya} \mytmt}
1482 \UnaryInfC{$\myjud{\myfun{K} \myappsp \myse{P} \myappsp \myse{t} \myappsp \myse{p} \myappsp \myse{q}}{\myse{P} \myappsp \mytmt \myappsp \myse{q}}$}
1486 \cite{Hofmann1994} showed that $\myfun{K}$ is not derivable from the
1487 $\myjeqq$ axiom that we presented, and \cite{McBride2004} showed that it is
1488 needed to implement `dependent pattern matching', as first proposed by
1489 \cite{Coquand1992}. Thus, $\myfun{K}$ is derivable in the systems that
1490 implement dependent pattern matching, such as Epigram and Agda; but for
1493 $\myfun{K}$ is controversial mainly because it is at odds with
1494 equalities that include computational behaviour, most notably
1495 Voevodsky's `Univalent Foundations', which includes a \emph{univalence}
1496 axiom that identifies isomorphisms between types with propositional
1497 equality. For example we would have two isomorphisms, and thus two
1498 equalities, between $\mybool$ and $\mybool$, corresponding to the two
1499 permutations---one is the identity, and one swaps the elements. Given
1500 this, $\myfun{K}$ and univalence are inconsistent, and thus a form of
1501 dependent pattern matching that does not imply $\myfun{K}$ is subject of
1502 research.\footnote{More information about univalence can be found at
1503 \url{http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations.html}.}
1505 \subsection{Limitations}
1507 \epigraph{\emph{Half of my time spent doing research involves thinking up clever
1508 schemes to avoid needing functional extensionality.}}{@larrytheliquid}
1510 Propositional equality as described is quite restricted when
1511 reasoning about equality beyond the term structure, which is what definitional
1512 equality gives us (extension notwithstanding).
1514 The problem is best exemplified by \emph{function extensionality}. In
1515 mathematics, we would expect to be able to treat functions that give equal
1516 output for equal input as the same. When reasoning in a mechanised framework
1517 we ought to be able to do the same: in the end, without considering the
1518 operational behaviour, all functions equal extensionally are going to be
1519 replaceable with one another.
1521 However this is not the case, or in other words with the tools we have we have
1524 \myfun{ext} : \myfora{\myb{A}\ \myb{B}}{\mytyp}{\myfora{\myb{f}\ \myb{g}}{
1525 \myb{A} \myarr \myb{B}}{
1526 (\myfora{\myb{x}}{\myb{A}}{\myapp{\myb{f}}{\myb{x}} \mypeq{\myb{B}} \myapp{\myb{g}}{\myb{x}}}) \myarr
1527 \myb{f} \mypeq{\myb{A} \myarr \myb{B}} \myb{g}
1531 To see why this is the case, consider the functions
1532 \[\myabs{\myb{x}}{0 \mathrel{\myfun{$+$}} \myb{x}}$ and $\myabs{\myb{x}}{\myb{x} \mathrel{\myfun{$+$}} 0}\]
1533 where $\myfun{$+$}$ is defined by recursion on the first argument,
1534 gradually destructing it to build up successors of the second argument.
1535 The two functions are clearly extensionally equal, and we can in fact
1538 \myfora{\myb{x}}{\mynat}{(0 \mathrel{\myfun{$+$}} \myb{x}) \mypeq{\mynat} (\myb{x} \mathrel{\myfun{$+$}} 0)}
1540 By analysis on the $\myb{x}$. However, the two functions are not
1541 definitionally equal, and thus we won't be able to get rid of the
1544 For the reasons given above, theories that offer a propositional equality
1545 similar to what we presented are called \emph{intensional}, as opposed
1546 to \emph{extensional}. Most systems widely used today (such as Agda,
1547 Coq, and Epigram) are of this kind.
1549 This is quite an annoyance that often makes reasoning awkward to execute. It
1550 also extends to other fields, for example proving bisimulation between
1551 processes specified by coinduction, or in general proving equivalences based
1552 on the behaviour on a term.
1554 \subsection{Equality reflection}
1556 One way to `solve' this problem is by identifying propositional equality with
1557 definitional equality.
1559 \begin{mydef}[Equality reflection]\end{mydef}
1560 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1561 \AxiomC{$\myjud{\myse{q}}{\mytmm \mypeq{\mytya} \mytmn}$}
1562 \UnaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\mytya}$}
1566 The \emph{equality reflection} rule is a very different rule from the
1567 ones we saw up to now: it links a typing judgement internal to the type
1568 theory to a meta-theoretic judgement that the type checker uses to work
1569 with terms. It is easy to see the dangerous consequences that this
1572 \item The rule is not syntax directed, and the type checker is
1573 presumably expected to come up with equality proofs when needed.
1574 \item More worryingly, type checking becomes undecidable also because
1575 computing under false assumptions becomes unsafe, since we derive any
1576 equality proof and then use equality reflection and the conversion
1577 rule to have terms of any type.
1579 For example, assuming that we are in a context that contains
1581 \myb{A} : \mytyp; \myb{q} : \mypeq \myappsp \mytyp
1582 \myappsp (\mytya \myarr \mytya) \myappsp \mytya
1584 we can write a looping term similar to the one we saw in Section
1589 Given these facts theories employing equality reflection, like NuPRL
1590 \citep{NuPRL}, carry the derivations that gave rise to each typing judgement
1591 to keep the systems manageable.
1593 For all its faults, equality reflection does allow us to prove extensionality,
1594 using the extensions we gave above. Assuming that $\myctx$ contains
1595 \[\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}}}\]
1599 \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}$}
1600 \RightLabel{equality reflection}
1601 \UnaryInfC{$\myjudd{\myctx; \myb{x} : \myb{A}}{\myapp{\myb{f}}{\myb{x}} \mydefeq \myapp{\myb{g}}{\myb{x}}}{\myb{B}}$}
1602 \RightLabel{congruence for $\lambda$s}
1603 \UnaryInfC{$\myjud{(\myabs{\myb{x}}{\myapp{\myb{f}}{\myb{x}}}) \mydefeq (\myabs{\myb{x}}{\myapp{\myb{g}}{\myb{x}}})}{\myb{A} \myarr \myb{B}}$}
1604 \RightLabel{$\eta$-law for $\lambda$}
1605 \UnaryInfC{$\hspace{1.45cm}\myjud{\myb{f} \mydefeq \myb{g}}{\myb{A} \myarr \myb{B}}\hspace{1.45cm}$}
1606 \RightLabel{$\myrefl$}
1607 \UnaryInfC{$\myjud{\myapp{\myrefl}{\myb{f}}}{\myb{f} \mypeq{} \myb{g}}$}
1610 Now, the question is: do we need to give up well-behavedness of our theory to
1611 gain extensionality?
1613 \subsection{Some alternatives}
1616 % TODO add `extentional axioms' (Hoffman), setoid models (Thorsten)
1618 \section{The observational approach}
1621 % TODO add \begin{mydef}s
1623 A recent development by \citet{Altenkirch2007}, \emph{Observational Type
1624 Theory} (OTT), promises to keep the well behavedness of ITT while
1625 being able to gain many useful equality proofs,\footnote{It is suspected
1626 that OTT gains \emph{all} the equality proofs of ETT, but no proof
1627 exists yet.} including function extensionality. The main idea is to
1628 give the user the possibility to \emph{coerce} (or transport) values
1629 from a type $\mytya$ to a type $\mytyb$, if the type checker can prove
1630 structurally that $\mytya$ and $\mytyb$ are equal; and providing a
1631 value-level equality based on similar principles. Here we give an
1632 exposition which follows closely the original paper.
1634 \subsection{A simpler theory, a propositional fragment}
1637 $\mytyp_l$ is replaced by $\mytyp$. \\\ \\
1639 \begin{array}{r@{\ }c@{\ }l}
1640 \mytmsyn & ::= & \cdots \mysynsep \myprdec{\myprsyn} \mysynsep
1641 \myITE{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
1642 \myprsyn & ::= & \mybot \mysynsep \mytop \mysynsep \myprsyn \myand \myprsyn
1643 \mysynsep \myprfora{\myb{x}}{\mytmsyn}{\myprsyn}
1650 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
1652 \begin{array}{l@{}l@{\ }c@{\ }l}
1653 \myITE{\mytrue &}{\mytya}{\mytyb} & \myred & \mytya \\
1654 \myITE{\myfalse &}{\mytya}{\mytyb} & \myred & \mytyb
1661 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1663 \AxiomC{$\myjud{\myse{P}}{\myprop}$}
1664 \UnaryInfC{$\myjud{\myprdec{\myse{P}}}{\mytyp}$}
1667 \AxiomC{$\myjud{\mytmt}{\mybool}$}
1668 \AxiomC{$\myjud{\mytya}{\mytyp}$}
1669 \AxiomC{$\myjud{\mytyb}{\mytyp}$}
1670 \TrinaryInfC{$\myjud{\myITE{\mytmt}{\mytya}{\mytyb}}{\mytyp}$}
1677 \mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
1678 \begin{tabular}{ccc}
1679 \AxiomC{\phantom{$\myjud{\myse{P}}{\myprop}$}}
1680 \UnaryInfC{$\myjud{\mytop}{\myprop}$}
1682 \UnaryInfC{$\myjud{\mybot}{\myprop}$}
1685 \AxiomC{$\myjud{\myse{P}}{\myprop}$}
1686 \AxiomC{$\myjud{\myse{Q}}{\myprop}$}
1687 \BinaryInfC{$\myjud{\myse{P} \myand \myse{Q}}{\myprop}$}
1689 \UnaryInfC{\phantom{$\myjud{\mybot}{\myprop}$}}
1692 \AxiomC{$\myjud{\myse{A}}{\mytyp}$}
1693 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\myse{P}}{\myprop}$}
1694 \BinaryInfC{$\myjud{\myprfora{\myb{x}}{\mytya}{\myse{P}}}{\myprop}$}
1696 \UnaryInfC{\phantom{$\myjud{\mybot}{\myprop}$}}
1701 Our foundation will be a type theory like the one of section
1702 \ref{sec:itt}, with only one level: $\mytyp_0$. In this context we will
1703 drop the $0$ and call $\mytyp_0$ $\mytyp$. Moreover, since the old
1704 $\myfun{if}\myarg\myfun{then}\myarg\myfun{else}$ was able to return
1705 types thanks to the hierarchy (which is gone), we need to reintroduce an
1706 ad-hoc conditional for types, where the reduction rule is the obvious
1709 However, we have an addition: a universe of \emph{propositions},
1710 $\myprop$. $\myprop$ isolates a fragment of types at large, and
1711 indeed we can `inject' any $\myprop$ back in $\mytyp$ with $\myprdec{\myarg}$: \\
1712 \mydesc{proposition decoding:}{\myprdec{\mytmsyn} \myred \mytmsyn}{
1715 \begin{array}{l@{\ }c@{\ }l}
1716 \myprdec{\mybot} & \myred & \myempty \\
1717 \myprdec{\mytop} & \myred & \myunit
1722 \begin{array}{r@{ }c@{ }l@{\ }c@{\ }l}
1723 \myprdec{&\myse{P} \myand \myse{Q} &} & \myred & \myprdec{\myse{P}} \myprod \myprdec{\myse{Q}} \\
1724 \myprdec{&\myprfora{\myb{x}}{\mytya}{\myse{P}} &} & \myred &
1725 \myfora{\myb{x}}{\mytya}{\myprdec{\myse{P}}}
1730 Propositions are what we call the types of \emph{proofs}, or types
1731 whose inhabitants contain no `data', much like $\myunit$. The goal of
1732 doing this is twofold: erasing all top-level propositions when
1733 compiling; and to identify all equivalent propositions as the same, as
1736 Why did we choose what we have in $\myprop$? Given the above
1737 criteria, $\mytop$ obviously fits the bill, since it us one element.
1738 A pair of propositions $\myse{P} \myand \myse{Q}$ still won't get us
1739 data, since if they both have one element the only possible pair is
1740 the one formed by said elements. Finally, if $\myse{P}$ is a
1741 proposition and we have $\myprfora{\myb{x}}{\mytya}{\myse{P}}$, the
1742 decoding will be a function which returns propositional content. The
1743 only threat is $\mybot$, by which we can fabricate anything we want:
1744 however if we are consistent there will be nothing of type $\mybot$ at
1745 the top level, which is what we care about regarding proof erasure.
1747 \subsection{Equality proofs}
1751 \begin{array}{r@{\ }c@{\ }l}
1752 \mytmsyn & ::= & \cdots \mysynsep
1753 \mycoee{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \mysynsep
1754 \mycohh{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
1755 \myprsyn & ::= & \cdots \mysynsep \mytmsyn \myeq \mytmsyn \mysynsep
1756 \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn}
1761 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1763 \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
1764 \AxiomC{$\myjud{\mytmt}{\mytya}$}
1765 \BinaryInfC{$\myjud{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}$}
1768 \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
1769 \AxiomC{$\myjud{\mytmt}{\mytya}$}
1770 \BinaryInfC{$\myjud{\mycohh{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\myprdec{\myjm{\mytmt}{\mytya}{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}}}$}
1776 \mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
1781 \myjud{\myse{A}}{\mytyp} \hspace{1cm} \myjud{\myse{B}}{\mytyp}
1784 \UnaryInfC{$\myjud{\mytya \myeq \mytyb}{\myprop}$}
1789 \myjud{\myse{A}}{\mytyp} \hspace{1cm} \myjud{\mytmm}{\myse{A}} \\
1790 \myjud{\myse{B}}{\mytyp} \hspace{1cm} \myjud{\mytmn}{\myse{B}}
1793 \UnaryInfC{$\myjud{\myjm{\mytmm}{\myse{A}}{\mytmn}{\myse{B}}}{\myprop}$}
1800 While isolating a propositional universe as presented can be a useful
1801 exercises on its own, what we are really after is a useful notion of
1802 equality. In OTT we want to maintain the notion that things judged to
1803 be equal are still always repleaceable for one another with no
1804 additional changes. Note that this is not the same as saying that they
1805 are definitionally equal, since as we saw extensionally equal functions,
1806 while satisfying the above requirement, are not definitionally equal.
1808 Towards this goal we introduce two equality constructs in
1809 $\myprop$---the fact that they are in $\myprop$ indicates that they
1810 indeed have no computational content. The first construct, $\myarg
1811 \myeq \myarg$, relates types, the second,
1812 $\myjm{\myarg}{\myarg}{\myarg}{\myarg}$, relates values. The
1813 value-level equality is different from our old propositional equality:
1814 instead of ranging over only one type, we might form equalities between
1815 values of different types---the usefulness of this construct will be
1816 clear soon. In the literature this equality is known as `heterogeneous'
1817 or `John Major', since
1820 John Major's `classless society' widened people's aspirations to
1821 equality, but also the gap between rich and poor. After all, aspiring
1822 to be equal to others than oneself is the politics of envy. In much
1823 the same way, forms equations between members of any type, but they
1824 cannot be treated as equals (ie substituted) unless they are of the
1825 same type. Just as before, each thing is only equal to
1826 itself. \citep{McBride1999}.
1829 Correspondingly, at the term level, $\myfun{coe}$ (`coerce') lets us
1830 transport values between equal types; and $\myfun{coh}$ (`coherence')
1831 guarantees that $\myfun{coe}$ respects the value-level equality, or in
1832 other words that it really has no computational component: if we
1833 transport $\mytmm : \mytya$ to $\mytmn : \mytyb$, $\mytmm$ and $\mytmn$
1834 will still be the same.
1836 Before introducing the core ideas that make OTT work, let us distinguish
1837 between \emph{canonical} and \emph{neutral} types. Canonical types are
1838 those arising from the ground types ($\myempty$, $\myunit$, $\mybool$)
1839 and the three type formers ($\myarr$, $\myprod$, $\mytyc{W}$). Neutral
1840 types are those formed by
1841 $\myfun{If}\myarg\myfun{Then}\myarg\myfun{Else}\myarg$.
1842 Correspondingly, canonical terms are those inhabiting canonical types
1843 ($\mytt$, $\mytrue$, $\myfalse$, $\myabss{\myb{x}}{\mytya}{\mytmt}$,
1844 ...), and neutral terms those formed by eliminators.\footnote{Using the
1845 terminology from Section \ref{sec:types}, we'd say that canonical
1846 terms are in \emph{weak head normal form}.} In the current system
1847 (and hopefully in well-behaved systems), all closed terms reduce to a
1848 canonical term, and all canonical types are inhabited by canonical
1851 \subsubsection{Type equality, and coercions}
1853 The plan is to decompose type-level equalities between canonical types
1854 into decodable propositions containing equalities regarding the
1855 subterms, and to use coerce recursively on the subterms using the
1856 generated equalities. This interplay between type equalities and
1857 \myfun{coe} ensures that invocations of $\myfun{coe}$ will vanish when
1858 we have evidence of the structural equality of the types we are
1859 transporting terms across. If the type is neutral, the equality won't
1860 reduce and thus $\myfun{coe}$ won't reduce either. If we come an
1861 equality between different canonical types, then we reduce the equality
1862 to bottom, making sure that no such proof can exist, and providing an
1863 `escape hatch' in $\myfun{coe}$.
1867 \mydesc{equality reduction:}{\myprsyn \myred \myprsyn}{
1869 \begin{array}{c@{\ }c@{\ }c@{\ }l}
1870 \myempty & \myeq & \myempty & \myred \mytop \\
1871 \myunit & \myeq & \myunit & \myred \mytop \\
1872 \mybool & \myeq & \mybool & \myred \mytop \\
1873 \myexi{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myexi{\myb{x_2}}{\mytya_2}{\mytya_2} & \myred \\
1875 \myind{2} \mytya_1 \myeq \mytyb_1 \myand
1876 \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}]}
1878 \myfora{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myfora{\myb{x_2}}{\mytya_2}{\mytyb_2} & \myred \cdots \\
1879 \myw{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myw{\myb{x_2}}{\mytya_2}{\mytyb_2} & \myred \cdots \\
1880 \mytya & \myeq & \mytyb & \myred \mybot\ \text{if $\mytya$ and $\mytyb$ are canonical.}
1885 \mydesc{reduction}{\mytmsyn \myred \mytmsyn}{
1887 \begin{array}[t]{@{}l@{\ }l@{\ }l@{\ }l@{\ }l@{\ }c@{\ }l@{\ }}
1888 \mycoe & \myempty & \myempty & \myse{Q} & \myse{t} & \myred & \myse{t} \\
1889 \mycoe & \myunit & \myunit & \myse{Q} & \myse{t} & \myred & \mytt \\
1890 \mycoe & \mybool & \mybool & \myse{Q} & \mytrue & \myred & \mytrue \\
1891 \mycoe & \mybool & \mybool & \myse{Q} & \myfalse & \myred & \myfalse \\
1892 \mycoe & (\myexi{\myb{x_1}}{\mytya_1}{\mytyb_1}) &
1893 (\myexi{\myb{x_2}}{\mytya_2}{\mytyb_2}) & \myse{Q} &
1894 \mytmt_1 & \myred & \\
1896 \myind{2}\begin{array}[t]{l@{\ }l@{\ }c@{\ }l}
1897 \mysyn{let} & \myb{\mytmm_1} & \mapsto & \myapp{\myfst}{\mytmt_1} : \mytya_1 \\
1898 & \myb{\mytmn_1} & \mapsto & \myapp{\mysnd}{\mytmt_1} : \mysub{\mytyb_1}{\myb{x_1}}{\myb{\mytmm_1}} \\
1899 & \myb{Q_A} & \mapsto & \myapp{\myfst}{\myse{Q}} : \mytya_1 \myeq \mytya_2 \\
1900 & \myb{\mytmm_2} & \mapsto & \mycoee{\mytya_1}{\mytya_2}{\myb{Q_A}}{\myb{\mytmm_1}} : \mytya_2 \\
1901 & \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}}} \\
1902 & \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}} \\
1903 \mysyn{in} & \multicolumn{3}{@{}l}{\mypair{\myb{\mytmm_2}}{\myb{\mytmn_2}}}
1906 \mycoe & (\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}) &
1907 (\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}) & \myse{Q} &
1911 \mycoe & (\myw{\myb{x_1}}{\mytya_1}{\mytyb_1}) &
1912 (\myw{\myb{x_2}}{\mytya_2}{\mytyb_2}) & \myse{Q} &
1916 \mycoe & \mytya & \mytyb & \myse{Q} & \mytmt & \myred & \myapp{\myabsurd{\mytyb}}{\myse{Q}}\ \text{if $\mytya$ and $\mytyb$ are canonical.}
1920 \caption{Reducing type equalities, and using them when
1921 $\myfun{coe}$rcing.}
1925 Figure \ref{fig:eqred} illustrates this idea in practice. For ground
1926 types, the proof is the trivial element, and \myfun{coe} is the
1927 identity. For $\myunit$, we can do better: we return its only member
1928 without matching on the term. For the three type binders, things are
1929 similar but subtly different---the choices we make in the type equality
1930 are dictated by the desire of writing the $\myfun{coe}$ in a natural
1933 $\myprod$ is the easiest case: we decompose the proof into proofs that
1934 the first element's types are equal ($\mytya_1 \myeq \mytya_2$), and a
1935 proof that given equal values in the first element, the types of the
1936 second elements are equal too
1937 ($\myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{\myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2}}
1938 \myimpl \mytyb_1 \myeq \mytyb_2}$).\footnote{We are using $\myimpl$ to
1939 indicate a $\forall$ where we discard the first value. We write
1940 $\mytyb_1[\myb{x_1}]$ to indicate that the $\myb{x_1}$ in $\mytyb_1$
1941 is re-bound to the $\myb{x_1}$ quantified by the $\forall$, and
1942 similarly for $\myb{x_2}$ and $\mytyb_2$.} This also explains the
1943 need for heterogeneous equality, since in the second proof it would be
1944 awkward to express the fact that $\myb{A_1}$ is the same as $\myb{A_2}$.
1945 In the respective $\myfun{coe}$ case, since the types are canonical, we
1946 know at this point that the proof of equality is a pair of the shape
1947 described above. Thus, we can immediately coerce the first element of
1948 the pair using the first element of the proof, and then instantiate the
1949 second element with the two first elements and a proof by coherence of
1950 their equality, since we know that the types are equal.
1952 The cases for the other binders are omitted for brevity, but they follow
1953 the same principle with some twists to make $\myfun{coe}$ work with the
1954 generated proofs; the reader can refer to the paper for details.
1956 \subsubsection{$\myfun{coe}$, laziness, and $\myfun{coh}$erence}
1958 It is important to notice that in the reduction rules for $\myfun{coe}$
1959 are never obstructed by the proofs: with the exception of comparisons
1960 between different canonical types we never `pattern match' on the proof
1961 pairs, but always look at the projections. This means that, as long as
1962 we are consistent, and thus as long as we don't have $\mybot$-inducing
1963 proofs, we can add propositional axioms for equality and $\myfun{coe}$
1964 will still compute. Thus, we can take $\myfun{coh}$ as axiomatic, and
1965 we can add back familiar useful equality rules:
1967 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1968 \AxiomC{$\myjud{\mytmt}{\mytya}$}
1969 \UnaryInfC{$\myjud{\myapp{\myrefl}{\mytmt}}{\myprdec{\myjm{\mytmt}{\mytya}{\mytmt}{\mytya}}}$}
1974 \AxiomC{$\myjud{\mytya}{\mytyp}$}
1975 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytyb}{\mytyp}$}
1976 \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}}}}}$}
1980 $\myrefl$ is the equivalent of the reflexivity rule in propositional
1981 equality, and $\mytyc{R}$ asserts that if we have a we have a $\mytyp$
1982 abstracting over a value we can substitute equal for equal---this lets
1983 us recover $\myfun{subst}$. Note that while we need to provide ad-hoc
1984 rules in the restricted, non-hierarchical theory that we have, if our
1985 theory supports abstraction over $\mytyp$s we can easily add these
1986 axioms as abstracted variables.
1988 \subsubsection{Value-level equality}
1990 \mydesc{equality reduction:}{\myprsyn \myred \myprsyn}{
1992 \begin{array}{r@{ }c@{\ }c@{\ }c@{}l@{\ }c@{\ }r@{}c@{\ }c@{\ }c@{}l@{\ }l}
1993 (&\mytmt_1 & : & \myempty&) & \myeq & (&\mytmt_2 & : & \myempty &) & \myred \mytop \\
1994 (&\mytmt_1 & : & \myunit&) & \myeq & (&\mytmt_2 & : & \myunit&) & \myred \mytop \\
1995 (&\mytrue & : & \mybool&) & \myeq & (&\mytrue & : & \mybool&) & \myred \mytop \\
1996 (&\myfalse & : & \mybool&) & \myeq & (&\myfalse & : & \mybool&) & \myred \mytop \\
1997 (&\mytrue & : & \mybool&) & \myeq & (&\myfalse & : & \mybool&) & \myred \mybot \\
1998 (&\myfalse & : & \mybool&) & \myeq & (&\mytrue & : & \mybool&) & \myred \mybot \\
1999 (&\mytmt_1 & : & \myexi{\mytya_1}{\myb{x_1}}{\mytyb_1}&) & \myeq & (&\mytmt_2 & : & \myexi{\mytya_2}{\myb{x_2}}{\mytyb_2}&) & \myred \\
2000 & \multicolumn{11}{@{}l}{
2001 \myind{2} \myjm{\myapp{\myfst}{\mytmt_1}}{\mytya_1}{\myapp{\myfst}{\mytmt_2}}{\mytya_2} \myand
2002 \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}}}
2004 (&\myse{f}_1 & : & \myfora{\mytya_1}{\myb{x_1}}{\mytyb_1}&) & \myeq & (&\myse{f}_2 & : & \myfora{\mytya_2}{\myb{x_2}}{\mytyb_2}&) & \myred \\
2005 & \multicolumn{11}{@{}l}{
2006 \myind{2} \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{
2007 \myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2} \myimpl
2008 \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}]}
2011 (&\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 \\
2012 (&\mytmt_1 & : & \mytya_1&) & \myeq & (&\mytmt_2 & : & \mytya_2 &) & \myred \mybot\ \text{if $\mytya_1$ and $\mytya_2$ are canonical.}
2017 As with type-level equality, we want value-level equality to reduce
2018 based on the structure of the compared terms. When matching
2019 propositional data, such as $\myempty$ and $\myunit$, we automatically
2020 return the trivial type, since if a type has zero one members, all
2021 members will be equal. When matching on data-bearing types, such as
2022 $\mybool$, we check that such data matches, and return bottom otherwise.
2024 \subsection{Proof irrelevance and stuck coercions}
2025 \label{sec:ott-quot}
2027 The last effort is required to make sure that proofs (members of
2028 $\myprop$) are \emph{irrelevant}. Since they are devoid of
2029 computational content, we would like to identify all equivalent
2030 propositions as the same, in a similar way as we identified all
2031 $\myempty$ and all $\myunit$ as the same in section
2032 \ref{sec:eta-expand}.
2034 Thus we will have a quotation that will not only perform
2035 $\eta$-expansion, but will also identify and mark proofs that could not
2036 be decoded (that is, equalities on neutral types). Then, when
2037 comparing terms, marked proofs will be considered equal without
2038 analysing their contents, thus gaining irrelevance.
2040 Moreover we can safely advance `stuck' $\myfun{coe}$rcions between
2041 non-canonical but definitionally equal types. Consider for example
2043 \mycoee{(\myITE{\myb{b}}{\mynat}{\mybool})}{(\myITE{\myb{b}}{\mynat}{\mybool})}{\myb{x}}
2045 Where $\myb{b}$ and $\myb{x}$ are abstracted variables. This
2046 $\myfun{coe}$ will not advance, since the types are not canonical.
2047 However they are definitionally equal, and thus we can safely remove the
2048 coerce and return $\myb{x}$ as it is.
2050 \section{\mykant : the theory}
2051 \label{sec:kant-theory}
2053 \mykant\ is an interactive theorem prover developed as part of this thesis.
2054 The plan is to present a core language which would be capable of serving as
2055 the basis for a more featureful system, while still presenting interesting
2056 features and more importantly observational equality.
2058 We will first present the features of the system, and then describe the
2059 implementation we have developed in Section \ref{sec:kant-practice}.
2061 The defining features of \mykant\ are:
2064 \item[Full dependent types] As we would expect, we have dependent a system
2065 which is as expressive as the `best' corner in the lambda cube described in
2066 Section \ref{sec:itt}.
2068 \item[Implicit, cumulative universe hierarchy] The user does not need to
2069 specify universe level explicitly, and universes are \emph{cumulative}.
2071 \item[User defined data types and records] Instead of forcing the user to
2072 choose from a restricted toolbox, we let her define inductive data types,
2073 with associated primitive recursion operators; or records, with associated
2074 projections for each field.
2076 \item[Bidirectional type checking] While no `fancy' inference via
2077 unification is present, we take advantage of a type synthesis system
2078 in the style of \cite{Pierce2000}, extending the concept for user
2081 \item[Observational equality] As described in Section \ref{sec:ott} but
2082 extended to work with the type hierarchy and to admit equality between
2083 arbitrary data types.
2085 \item[Type holes] When building up programs interactively, it is useful
2086 to leave parts unfinished while exploring the current context. This
2087 is what type holes are for. We do not describe holes rigorously, but
2088 provide more information about them from the implementation and usage
2089 perspective in Section \ref{sec:type-holes}.
2093 We will analyse the features one by one, along with motivations and
2094 tradeoffs for the design decisions made.
2096 \subsection{Bidirectional type checking}
2098 We start by describing bidirectional type checking since it calls for
2099 fairly different typing rules that what we have seen up to now. The
2100 idea is to have two kinds of terms: terms for which a type can always be
2101 inferred, and terms that need to be checked against a type. A nice
2102 observation is that this duality runs through the semantics of the
2103 terms: neutral terms (abstracted or defined variables, function
2104 application, record projections, primitive recursors, etc.) \emph{infer}
2105 types, canonical terms (abstractions, record/data types data
2106 constructors, etc.) need to be \emph{checked}.
2108 To introduce the concept and notation, we will revisit the STLC in a
2109 bidirectional style. The presentation follows \cite{Loh2010}. The
2110 syntax for our bidirectional STLC is the same as the untyped
2111 $\lambda$-calculus, but with an extra construct to annotate terms
2112 explicitly---this will be necessary when having top-level canonical
2113 terms. The types are the same as those found in the normal STLC.
2117 \begin{array}{r@{\ }c@{\ }l}
2118 \mytmsyn & ::= & \myb{x} \mysynsep \myabs{\myb{x}}{\mytmsyn} \mysynsep (\myapp{\mytmsyn}{\mytmsyn}) \mysynsep (\mytmsyn : \mytysyn)
2122 We will have two kinds of typing judgements: \emph{inference} and
2123 \emph{checking}. $\myinf{\mytmt}{\mytya}$ indicates that $\mytmt$
2124 infers the type $\mytya$, while $\mychk{\mytmt}{\mytya}$ can be checked
2125 against type $\mytya$. The type of variables in context is inferred,
2126 and so are annotate terms. The type of applications is inferred too,
2127 propagating types down the applied term. Abstractions are checked.
2128 Finally, we have a rule to check the type of an inferrable term.
2130 \mydesc{typing:}{\myctx \vdash \mytmsyn \Updownarrow \mytmsyn}{
2132 \AxiomC{$\myctx(x) = A$}
2133 \UnaryInfC{$\myinf{\myb{x}}{A}$}
2136 \AxiomC{$\myjudd{\myctx;\myb{x} : A}{\mytmt}{\mytyb}$}
2137 \UnaryInfC{$\mychk{\myabs{x}{\mytmt}}{(\myb{x} {:} \mytya) \myarr \mytyb}$}
2143 \begin{tabular}{ccc}
2144 \AxiomC{$\myinf{\mytmm}{\mytya \myarr \mytyb}$}
2145 \AxiomC{$\mychk{\mytmn}{\mytya}$}
2146 \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mytyb}$}
2149 \AxiomC{$\mychk{\mytmt}{\mytya}$}
2150 \UnaryInfC{$\myinf{\myann{\mytmt}{\mytya}}{\mytya}$}
2153 \AxiomC{$\myinf{\mytmt}{\mytya}$}
2154 \UnaryInfC{$\myinf{\mytmt}{\mytya}$}
2159 For example, if we wanted to type function composition (in this case for
2160 naturals), we would have to annotate the term:
2162 \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
2164 But we would not have to annotate functions passed to it, since the type would be propagated to the arguments:
2166 \myfun{comp}\myappsp (\myabs{\myb{x}}{\myb{x} \mathrel{\myfun{$+$}} 3}) \myappsp (\myabs{\myb{x}}{\myb{x} \mathrel{\myfun{$*$}} 4}) \myappsp 42
2169 \subsection{Base terms and types}
2171 Let us begin by describing the primitives available without the user
2172 defining any data types, and without equality. The way we handle
2173 variables and substitution is left unspecified, and explained in section
2174 \ref{sec:term-repr}, along with other implementation issues. We are
2175 also going to give an account of the implicit type hierarchy separately
2176 in Section \ref{sec:term-hierarchy}, so as not to clutter derivation
2177 rules too much, and just treat types as impredicative for the time
2182 \begin{array}{r@{\ }c@{\ }l}
2183 \mytmsyn & ::= & \mynamesyn \mysynsep \mytyp \\
2184 & | & \myfora{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
2185 \myabs{\myb{x}}{\mytmsyn} \mysynsep
2186 (\myapp{\mytmsyn}{\mytmsyn}) \mysynsep
2187 (\myann{\mytmsyn}{\mytmsyn}) \\
2188 \mynamesyn & ::= & \myb{x} \mysynsep \myfun{f}
2193 The syntax for our calculus includes just two basic constructs:
2194 abstractions and $\mytyp$s. Everything else will be provided by
2195 user-definable constructs. Since we let the user define values, we will
2196 need a context capable of carrying the body of variables along with
2199 Bound names and defined names are treated separately in the syntax, and
2200 while both can be associated to a type in the context, only defined
2201 names can be associated with a body:
2203 \mydesc{context validity:}{\myvalid{\myctx}}{
2204 \begin{tabular}{ccc}
2205 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
2206 \UnaryInfC{$\myvalid{\myemptyctx}$}
2209 \AxiomC{$\myjud{\mytya}{\mytyp}$}
2210 \AxiomC{$\mynamesyn \not\in \myctx$}
2211 \BinaryInfC{$\myvalid{\myctx ; \mynamesyn : \mytya}$}
2214 \AxiomC{$\myjud{\mytmt}{\mytya}$}
2215 \AxiomC{$\myfun{f} \not\in \myctx$}
2216 \BinaryInfC{$\myvalid{\myctx ; \myfun{f} \mapsto \mytmt : \mytya}$}
2221 Now we can present the reduction rules, which are unsurprising. We have
2222 the usual function application ($\beta$-reduction), but also a rule to
2223 replace names with their bodies ($\delta$-reduction), and one to discard
2224 type annotations. For this reason reduction is done in-context, as
2225 opposed to what we have seen in the past:
2227 \mydesc{reduction:}{\myctx \vdash \mytmsyn \myred \mytmsyn}{
2228 \begin{tabular}{ccc}
2229 \AxiomC{\phantom{$\myb{x} \mapsto \mytmt : \mytya \in \myctx$}}
2230 \UnaryInfC{$\myctx \vdash \myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn}
2231 \myred \mysub{\mytmm}{\myb{x}}{\mytmn}$}
2234 \AxiomC{$\myfun{f} \mapsto \mytmt : \mytya \in \myctx$}
2235 \UnaryInfC{$\myctx \vdash \myfun{f} \myred \mytmt$}
2238 \AxiomC{\phantom{$\myb{x} \mapsto \mytmt : \mytya \in \myctx$}}
2239 \UnaryInfC{$\myctx \vdash \myann{\mytmm}{\mytya} \myred \mytmm$}
2244 We can now give types to our terms. Although we include the usual
2245 conversion rule, we defer a detailed account of definitional equality to
2246 Section \ref{sec:kant-irr}.
2248 \mydesc{typing:}{\myctx \vdash \mytmsyn \Updownarrow \mytmsyn}{
2249 \begin{tabular}{cccc}
2250 \AxiomC{$\myse{name} : A \in \myctx$}
2251 \UnaryInfC{$\myinf{\myse{name}}{A}$}
2254 \AxiomC{$\myfun{f} \mapsto \mytmt : A \in \myctx$}
2255 \UnaryInfC{$\myinf{\myfun{f}}{A}$}
2258 \AxiomC{$\mychk{\mytmt}{\mytya}$}
2259 \UnaryInfC{$\myinf{\myann{\mytmt}{\mytya}}{\mytya}$}
2262 \AxiomC{$\myinf{\mytmt}{\mytya}$}
2263 \AxiomC{$\myctx \vdash \mytya \mydefeq \mytyb$}
2264 \BinaryInfC{$\mychk{\mytmt}{\mytyb}$}
2272 \AxiomC{\phantom{$\mychkk{\myctx; \myb{x}: \mytya}{\mytmt}{\mytyb}$}}
2273 \UnaryInfC{$\myinf{\mytyp}{\mytyp}$}
2276 \AxiomC{$\myinf{\mytya}{\mytyp}$}
2277 \AxiomC{$\myinff{\myctx; \myb{x} : \mytya}{\mytyb}{\mytyp}$}
2278 \BinaryInfC{$\myinf{(\myb{x} {:} \mytya) \myarr \mytyb}{\mytyp}$}
2287 \AxiomC{$\myinf{\mytmm}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
2288 \AxiomC{$\mychk{\mytmn}{\mytya}$}
2289 \BinaryInfC{$\myinf{\myapp{\mytmm}{\mytmn}}{\mysub{\mytyb}{\myb{x}}{\mytmn}}$}
2294 \AxiomC{$\mychkk{\myctx; \myb{x}: \mytya}{\mytmt}{\mytyb}$}
2295 \UnaryInfC{$\mychk{\myabs{\myb{x}}{\mytmt}}{\myfora{\myb{x}}{\mytyb}{\mytyb}}$}
2301 \subsection{Elaboration}
2303 As we mentioned, $\mykant$\ allows the user to define not only values
2304 but also custom data types and records. \emph{Elaboration} consists of
2305 turning these declarations into workable syntax, types, and reduction
2306 rules. The treatment of custom types in $\mykant$\ is heavily inspired
2307 by McBride's and McKinna's early work on Epigram \citep{McBride2004},
2308 although with some differences.
2310 \subsubsection{Term vectors, telescopes, and assorted notation}
2312 We use a vector notation to refer to a series of term applied to
2313 another, for example $\mytyc{D} \myappsp \vec{A}$ is a shorthand for
2314 $\mytyc{D} \myappsp \mytya_1 \cdots \mytya_n$, for some $n$. $n$ is
2315 consistently used to refer to the length of such vectors, and $i$ to
2316 refer to an index in such vectors. We also often need to `build up'
2317 terms vectors, in which case we use $\myemptyctx$ for an empty vector
2318 and add elements to an existing vector with $\myarg ; \myarg$, similarly
2319 to what we do for contexts.
2321 To present the elaboration and operations on user defined data types, we
2322 frequently make use what de Bruijn called \emph{telescopes}
2323 \citep{Bruijn91}, a construct that will prove useful when dealing with
2324 the types of type and data constructors. A telescope is a series of
2325 nested typed bindings, such as $(\myb{x} {:} \mynat); (\myb{p} {:}
2326 \myapp{\myfun{even}}{\myb{x}})$. Consistent with the notation for
2327 contexts and term vectors, we use $\myemptyctx$ to denote an empty
2328 telescope and $\myarg ; \myarg$ to add a new binding to an existing
2331 We refer to telescopes with $\mytele$, $\mytele'$, $\mytele_i$, etc. If
2332 $\mytele$ refers to a telescope, $\mytelee$ refers to the term vector
2333 made up of all the variables bound by $\mytele$. $\mytele \myarr
2334 \mytya$ refers to the type made by turning the telescope into a series
2335 of $\myarr$. Returning to the examples above, we have that
2337 (\myb{x} {:} \mynat); (\myb{p} : \myapp{\myfun{even}}{\myb{x}}) \myarr \mynat =
2338 (\myb{x} {:} \mynat) \myarr (\myb{p} : \myapp{\myfun{even}}{\myb{x}}) \myarr \mynat
2341 We make use of various operations to manipulate telescopes:
2343 \item $\myhead(\mytele)$ refers to the first type appearing in
2344 $\mytele$: $\myhead((\myb{x} {:} \mynat); (\myb{p} :
2345 \myapp{\myfun{even}}{\myb{x}})) = \mynat$. Similarly,
2346 $\myix_i(\mytele)$ refers to the $i^{th}$ type in a telescope
2348 \item $\mytake_i(\mytele)$ refers to the telescope created by taking the
2349 first $i$ elements of $\mytele$: $\mytake_1((\myb{x} {:} \mynat); (\myb{p} :
2350 \myapp{\myfun{even}}{\myb{x}})) = (\myb{x} {:} \mynat)$.
2351 \item $\mytele \vec{A}$ refers to the telescope made by `applying' the
2352 terms in $\vec{A}$ on $\mytele$: $((\myb{x} {:} \mynat); (\myb{p} :
2353 \myapp{\myfun{even}}{\myb{x}}))42 = (\myb{p} :
2354 \myapp{\myfun{even}}{42})$.
2357 Additionally, when presenting syntax elaboration, I'll use $\mytmsyn^n$
2358 to indicate a term vector composed of $n$ elements, or
2359 $\mytmsyn^{\mytele}$ for one composed by as many elements as the
2362 \subsubsection{Declarations syntax}
2366 \begin{array}{r@{\ }c@{\ }l}
2367 \mydeclsyn & ::= & \myval{\myb{x}}{\mytmsyn}{\mytmsyn} \\
2368 & | & \mypost{\myb{x}}{\mytmsyn} \\
2369 & | & \myadt{\mytyc{D}}{\myappsp \mytelesyn}{}{\mydc{c} : \mytelesyn\ |\ \cdots } \\
2370 & | & \myreco{\mytyc{D}}{\myappsp \mytelesyn}{}{\myfun{f} : \mytmsyn,\ \cdots } \\
2372 \mytelesyn & ::= & \myemptytele \mysynsep \mytelesyn \mycc (\myb{x} {:} \mytmsyn) \\
2373 \mynamesyn & ::= & \cdots \mysynsep \mytyc{D} \mysynsep \mytyc{D}.\mydc{c} \mysynsep \mytyc{D}.\myfun{f}
2378 In \mykant\ we have four kind of declarations:
2381 \item[Defined value] A variable, together with a type and a body.
2382 \item[Abstract variable] An abstract variable, with a type but no body.
2383 \item[Inductive data] A datatype, with a type constructor and various
2384 data constructors, quite similar to what we find in Haskell. A
2385 primitive recursor (or `destructor') will be generated automatically.
2386 \item[Record] A record, which consists of one data constructor and various
2387 fields, with no recursive occurrences.
2390 Elaborating defined variables consists of type checking the body against
2391 the given type, and updating the context to contain the new binding.
2392 Elaborating abstract variables and abstract variables consists of type
2393 checking the type, and updating the context with a new typed variable:
2395 \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
2397 \AxiomC{$\myjud{\mytmt}{\mytya}$}
2398 \AxiomC{$\myfun{f} \not\in \myctx$}
2400 $\myctx \myelabt \myval{\myfun{f}}{\mytya}{\mytmt} \ \ \myelabf\ \ \myctx; \myfun{f} \mapsto \mytmt : \mytya$
2404 \AxiomC{$\myjud{\mytya}{\mytyp}$}
2405 \AxiomC{$\myfun{f} \not\in \myctx$}
2408 \myctx \myelabt \mypost{\myfun{f}}{\mytya}
2409 \ \ \myelabf\ \ \myctx; \myfun{f} : \mytya
2416 \subsubsection{User defined types}
2417 \label{sec:user-type}
2419 Elaborating user defined types is the real effort. First, we will
2420 explain what we can define, with some examples.
2423 \item[Natural numbers] To define natural numbers, we create a data type
2424 with two constructors: one with zero arguments ($\mydc{zero}$) and one
2425 with one recursive argument ($\mydc{suc}$):
2428 \myadt{\mynat}{ }{ }{
2429 \mydc{zero} \mydcsep \mydc{suc} \myappsp \mynat
2433 This is very similar to what we would write in Haskell:
2435 data Nat = Zero | Suc Nat
2437 Once the data type is defined, $\mykant$\ will generate syntactic
2438 constructs for the type and data constructors, so that we will have
2441 \begin{tabular}{ccc}
2442 \AxiomC{\phantom{$\mychk{\mytmt}{\mynat}$}}
2443 \UnaryInfC{$\myinf{\mynat}{\mytyp}$}
2446 \AxiomC{\phantom{$\mychk{\mytmt}{\mynat}$}}
2447 \UnaryInfC{$\myinf{\mytyc{\mynat}.\mydc{zero}}{\mynat}$}
2450 \AxiomC{$\mychk{\mytmt}{\mynat}$}
2451 \UnaryInfC{$\myinf{\mytyc{\mynat}.\mydc{suc} \myappsp \mytmt}{\mynat}$}
2455 While in Haskell (or indeed in Agda or Coq) data constructors are
2456 treated the same way as functions, in $\mykant$\ they are syntax, so
2457 for example using $\mytyc{\mynat}.\mydc{suc}$ on its own will give a
2458 syntax error. This is necessary so that we can easily infer the type
2459 of polymorphic data constructors, as we will see later.
2461 Moreover, each data constructor is prefixed by the type constructor
2462 name, since we need to retrieve the type constructor of a data
2463 constructor when type checking. This measure aids in the presentation
2464 of various features but it is not needed in the implementation, where
2465 we can have a dictionary to lookup the type constructor corresponding
2466 to each data constructor. When using data constructors in examples I
2467 will omit the type constructor prefix for brevity, in this case
2468 writing $\mydc{zero}$ instead of $\mynat.\mydc{suc}$ and $\mydc{suc}$ instead of
2469 $\mynat.\mydc{suc}$.
2471 Along with user defined constructors, $\mykant$\ automatically
2472 generates an \emph{eliminator}, or \emph{destructor}, to compute with
2473 natural numbers: If we have $\mytmt : \mynat$, we can destruct
2474 $\mytmt$ using the generated eliminator `$\mynat.\myfun{elim}$':
2477 \AxiomC{$\mychk{\mytmt}{\mynat}$}
2479 \myinf{\mytyc{\mynat}.\myfun{elim} \myappsp \mytmt}{
2481 \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}}
2485 $\mynat.\myfun{elim}$ corresponds to the induction principle for
2486 natural numbers: if we have a predicate on numbers ($\myb{P}$), and we
2487 know that predicate holds for the base case
2488 ($\myapp{\myb{P}}{\mydc{zero}}$) and for each inductive step
2489 ($\myfora{\myb{x}}{\mynat}{\myapp{\myb{P}}{\myb{x}} \myarr
2490 \myapp{\myb{P}}{(\myapp{\mydc{suc}}{\myb{x}})}}$), then $\myb{P}$
2491 holds for any number. As with the data constructors, we require the
2492 eliminator to be applied to the `destructed' element.
2494 While the induction principle is usually seen as a mean to prove
2495 properties about numbers, in the intuitionistic setting it is also a
2496 mean to compute. In this specific case $\mynat.\myfun{elim}$
2497 returns the base case if the provided number is $\mydc{zero}$, and
2498 recursively applies the inductive step if the number is a
2501 \begin{array}{@{}l@{}l}
2502 \mytyc{\mynat}.\myfun{elim} \myappsp \mydc{zero} & \myappsp \myse{P} \myappsp \myse{pz} \myappsp \myse{ps} \myred \myse{pz} \\
2503 \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})
2506 The Haskell equivalent would be
2508 elim :: Nat -> a -> (Nat -> a -> a) -> a
2509 elim Zero pz ps = pz
2510 elim (Suc n) pz ps = ps n (elim n pz ps)
2512 Which buys us the computational behaviour, but not the reasoning power,
2513 since we cannot express the notion of a predicate depending on $\mynat$,
2514 since the type system is far too weak.
2516 \item[Binary trees] Now for a polymorphic data type: binary trees, since
2517 lists are too similar to natural numbers to be interesting.
2520 \myadt{\mytree}{\myappsp (\myb{A} {:} \mytyp)}{ }{
2521 \mydc{leaf} \mydcsep \mydc{node} \myappsp (\myapp{\mytree}{\myb{A}}) \myappsp \myb{A} \myappsp (\myapp{\mytree}{\myb{A}})
2525 Now the purpose of constructors as syntax can be explained: what would
2526 the type of $\mydc{leaf}$ be? If we were to treat it as a `normal'
2527 term, we would have to specify the type parameter of the tree each
2528 time the constructor is applied:
2530 \begin{array}{@{}l@{\ }l}
2531 \mydc{leaf} & : \myfora{\myb{A}}{\mytyp}{\myapp{\mytree}{\myb{A}}} \\
2532 \mydc{node} & : \myfora{\myb{A}}{\mytyp}{\myapp{\mytree}{\myb{A}} \myarr \myb{A} \myarr \myapp{\mytree}{\myb{A}} \myarr \myapp{\mytree}{\myb{A}}}
2535 The problem with this approach is that creating terms is incredibly
2536 verbose and dull, since we would need to specify the type parameters
2537 each time. For example if we wished to create a $\mytree \myappsp
2538 \mynat$ with two nodes and three leaves, we would have to write
2540 \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)
2542 The redundancy of $\mynat$s is quite irritating. Instead, if we treat
2543 constructors as syntactic elements, we can `extract' the type of the
2544 parameter from the type that the term gets checked against, much like
2545 we get the type of abstraction arguments:
2549 \AxiomC{$\mychk{\mytya}{\mytyp}$}
2550 \UnaryInfC{$\mychk{\mydc{leaf}}{\myapp{\mytree}{\mytya}}$}
2553 \AxiomC{$\mychk{\mytmm}{\mytree \myappsp \mytya}$}
2554 \AxiomC{$\mychk{\mytmt}{\mytya}$}
2555 \AxiomC{$\mychk{\mytmm}{\mytree \myappsp \mytya}$}
2556 \TrinaryInfC{$\mychk{\mydc{node} \myappsp \mytmm \myappsp \mytmt \myappsp \mytmn}{\mytree \myappsp \mytya}$}
2560 Which enables us to write, much more concisely
2562 \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}
2564 We gain an annotation, but we lose the myriad of types applied to the
2565 constructors. Conversely, with the eliminator for $\mytree$, we can
2566 infer the type of the arguments given the type of the destructed:
2569 \AxiomC{$\myinf{\mytmt}{\myapp{\mytree}{\mytya}}$}
2571 \myinf{\mytree.\myfun{elim} \myappsp \mytmt}{
2573 (\myb{P} {:} \myapp{\mytree}{\mytya} \myarr \mytyp) \myarr \\
2574 \myapp{\myb{P}}{\mydc{leaf}} \myarr \\
2575 ((\myb{l} {:} \myapp{\mytree}{\mytya}) (\myb{x} {:} \mytya) (\myb{r} {:} \myapp{\mytree}{\mytya}) \myarr \myapp{\myb{P}}{\myb{l}} \myarr
2576 \myapp{\myb{P}}{\myb{r}} \myarr \myb{P} \myappsp (\mydc{node} \myappsp \myb{l} \myappsp \myb{x} \myappsp \myb{r})) \myarr \\
2577 \myapp{\myb{P}}{\mytmt}
2582 As expected, the eliminator embodies structural induction on trees.
2583 We have a base case for $\myb{P} \myappsp \mydc{leaf}$, and an
2584 inductive step that given two subtrees and the predicate applied to
2585 them we need to return the predicate applied to the tree formed by a
2586 node with the two subtrees as children.
2588 \item[Empty type] We have presented types that have at least one
2589 constructors, but nothing prevents us from defining types with
2590 \emph{no} constructors:
2591 \[\myadt{\mytyc{Empty}}{ }{ }{ }\]
2592 What shall the `induction principle' on $\mytyc{Empty}$ be? Does it
2593 even make sense to talk about induction on $\mytyc{Empty}$?
2594 $\mykant$\ does not care, and generates an eliminator with no `cases',
2595 and thus corresponding to the $\myfun{absurd}$ that we know and love:
2598 \AxiomC{$\myinf{\mytmt}{\mytyc{Empty}}$}
2599 \UnaryInfC{$\myinf{\myempty.\myfun{elim} \myappsp \mytmt}{(\myb{P} {:} \mytmt \myarr \mytyp) \myarr \myapp{\myb{P}}{\mytmt}}$}
2602 \item[Ordered lists] Up to this point, the examples shown are nothing
2603 new to the \{Haskell, SML, OCaml, functional\} programmer. However
2604 dependent types let us express much more than that. A useful example
2605 is the type of ordered lists. There are many ways to define such a
2606 thing, we will define our type to store the bounds of the list, making
2607 sure that $\mydc{cons}$ing respects that.
2609 First, using $\myunit$ and $\myempty$, we define a type expressing the
2610 ordering on natural numbers, $\myfun{le}$---`less or equal'.
2611 $\myfun{le}\myappsp \mytmm \myappsp \mytmn$ will be inhabited only if
2612 $\mytmm \le \mytmn$:
2615 \myfun{le} : \mynat \myarr \mynat \myarr \mytyp \\
2616 \myfun{le} \myappsp \myb{n} \mapsto \\
2617 \myind{2} \mynat.\myfun{elim} \\
2618 \myind{2}\myind{2} \myb{n} \\
2619 \myind{2}\myind{2} (\myabs{\myarg}{\mynat \myarr \mytyp}) \\
2620 \myind{2}\myind{2} (\myabs{\myarg}{\myunit}) \\
2621 \myind{2}\myind{2} (\myabs{\myb{n}\, \myb{f}\, \myb{m}}{
2622 \mynat.\myfun{elim} \myappsp \myb{m} \myappsp (\myabs{\myarg}{\mytyp}) \myappsp \myempty \myappsp (\myabs{\myb{m'}\, \myarg}{\myapp{\myb{f}}{\myb{m'}}})
2626 We return $\myunit$ if the scrutinised is $\mydc{zero}$ (every
2627 number in less or equal than zero), $\myempty$ if the first number is
2628 a $\mydc{suc}$cessor and the second a $\mydc{zero}$, and we recurse if
2629 they are both successors. Since we want the list to have possibly
2630 `open' bounds, for example for empty lists, we create a type for
2631 `lifted' naturals with a bottom (less than everything) and top
2632 (greater than everything) elements, along with an associated comparison
2636 \myadt{\mytyc{Lift}}{ }{ }{\mydc{bot} \mydcsep \mydc{lift} \myappsp \mynat \mydcsep \mydc{top}}\\
2637 \myfun{le'} : \mytyc{Lift} \myarr \mytyc{Lift} \myarr \mytyp\\
2638 \myfun{le'} \myappsp \myb{l_1} \mapsto \\
2639 \myind{2} \mytyc{Lift}.\myfun{elim} \\
2640 \myind{2}\myind{2} \myb{l_1} \\
2641 \myind{2}\myind{2} (\myabs{\myarg}{\mytyc{Lift} \myarr \mytyp}) \\
2642 \myind{2}\myind{2} (\myabs{\myarg}{\myunit}) \\
2643 \myind{2}\myind{2} (\myabs{\myb{n_1}\, \myb{n_2}}{
2644 \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
2646 \myind{2}\myind{2} (\myabs{\myb{n_1}\, \myb{n_2}}{
2647 \mytyc{Lift}.\myfun{elim} \myappsp \myb{l_2} \myappsp (\myabs{\myarg}{\mytyp}) \myappsp \myempty \myappsp (\myabs{\myarg}{\myempty}) \myappsp \myunit
2651 Finally, we can defined a type of ordered lists. The type is
2652 parametrised over two values representing the lower and upper bounds
2653 of the elements, as opposed to the type parameters that we are used
2654 to. Then, an empty list will have to have evidence that the bounds
2655 are ordered, and each time we add an element we require the list to
2656 have a matching lower bound:
2659 \myadt{\mytyc{OList}}{\myappsp (\myb{low}\ \myb{upp} {:} \mytyc{Lift})}{\\ \myind{2}}{
2660 \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})
2664 Note that in the $\mydc{cons}$ constructor we quantify over the first
2665 argument, which will determine the type of the following
2666 arguments---again something we cannot do in systems like Haskell. If
2667 we want we can then employ this structure to write and prove correct
2668 various sorting algorithms.\footnote{See this presentation by Conor
2670 \url{https://personal.cis.strath.ac.uk/conor.mcbride/Pivotal.pdf},
2671 and this blog post by the author:
2672 \url{http://mazzo.li/posts/AgdaSort.html}.}
2674 \item[Dependent products] Apart from $\mysyn{data}$, $\mykant$\ offers
2675 us another way to define types: $\mysyn{record}$. A record is a
2676 datatype with one constructor and `projections' to extract specific
2677 fields of the said constructor.
2679 For example, we can recover dependent products:
2682 \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}}}
2685 Here $\myfst$ and $\mysnd$ are the projections, with their respective
2686 types. Note that each field can refer to the preceding fields. A
2687 constructor will be automatically generated, under the name of
2688 $\mytyc{Prod}.\mydc{constr}$. Dually to data types, we will omit the
2689 type constructor prefix for record projections.
2691 Following the bidirectionality of the system, we have that projections
2692 (the destructors of the record) infer the type, while the constructor
2697 \AxiomC{$\mychk{\mytmm}{\mytya}$}
2698 \AxiomC{$\mychk{\mytmn}{\myapp{\mytyb}{\mytmm}}$}
2699 \BinaryInfC{$\mychk{\mytyc{Prod}.\mydc{constr} \myappsp \mytmm \myappsp \mytmn}{\mytyc{Prod} \myappsp \mytya \myappsp \mytyb}$}
2701 \UnaryInfC{\phantom{$\myinf{\myfun{snd} \myappsp \mytmt}{\mytyb \myappsp (\myfst \myappsp \mytmt)}$}}
2704 \AxiomC{$\myinf{\mytmt}{\mytyc{Prod} \myappsp \mytya \myappsp \mytyb}$}
2705 \UnaryInfC{$\myinf{\myfun{fst} \myappsp \mytmt}{\mytya}$}
2707 \UnaryInfC{$\myinf{\myfun{snd} \myappsp \mytmt}{\mytyb \myappsp (\myfst \myappsp \mytmt)}$}
2711 What we have is equivalent to ITT's dependent products.
2719 \mynamesyn ::= \cdots \mysynsep \mytyc{D} \mysynsep \mytyc{D}.\mydc{c} \mysynsep \mytyc{D}.\myfun{f}
2726 \mydesc{syntax elaboration:}{\mydeclsyn \myelabf \mytmsyn ::= \cdots}{
2729 \begin{array}{r@{\ }l}
2730 & \myadt{\mytyc{D}}{\mytele}{}{\cdots\ |\ \mydc{c}_n : \mytele_n } \\
2733 \begin{array}{r@{\ }c@{\ }l}
2734 \mytmsyn & ::= & \cdots \mysynsep \myapp{\mytyc{D}}{\mytmsyn^{\mytele}} \mysynsep \cdots \mysynsep
2735 \mytyc{D}.\mydc{c}_n \myappsp \mytmsyn^{\mytele_n} \mysynsep \mytyc{D}.\myfun{elim} \myappsp \mytmsyn \\
2743 \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
2748 \myinf{\mytele \myarr \mytyp}{\mytyp}\hspace{0.8cm}
2749 \mytyc{D} \not\in \myctx \\
2750 \myinff{\myctx;\ \mytyc{D} : \mytele \myarr \mytyp}{\mytele \mycc \mytele_i \myarr \myapp{\mytyc{D}}{\mytelee}}{\mytyp}\ \ \ (1 \leq i \leq n) \\
2751 \text{For each $(\myb{x} {:} \mytya)$ in each $\mytele_i$, if $\mytyc{D} \in \mytya$, then $\mytya = \myapp{\mytyc{D}}{\vec{\mytmt}}$.}
2755 \begin{array}{r@{\ }c@{\ }l}
2756 \myctx & \myelabt & \myadt{\mytyc{D}}{\mytele}{}{ \cdots \ |\ \mydc{c}_n : \mytele_n } \\
2757 & & \vspace{-0.2cm} \\
2758 & \myelabf & \myctx;\ \mytyc{D} : \mytele \myarr \mytyp;\ \cdots;\ \mytyc{D}.\mydc{c}_n : \mytele \mycc \mytele_n \myarr \myapp{\mytyc{D}}{\mytelee}; \\
2760 \begin{array}{@{}r@{\ }l l}
2761 \mytyc{D}.\myfun{elim} : & \mytele \myarr (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr & \textbf{target} \\
2762 & (\myb{P} {:} \myapp{\mytyc{D}}{\mytelee} \myarr \mytyp) \myarr & \textbf{motive} \\
2766 (\mytele_n \mycc \myhyps(\myb{P}, \mytele_n) \myarr \myapp{\myb{P}}{(\myapp{\mytyc{D}.\mydc{c}_n}{\mytelee_n})}) \myarr
2767 \end{array} \right \}
2768 & \textbf{methods} \\
2769 & \myapp{\myb{P}}{\myb{x}} &
2773 \DisplayProof \\ \vspace{0.2cm}\ \\
2775 \begin{array}{@{}l l@{\ } l@{} r c l}
2776 \textbf{where} & \myhyps(\myb{P}, & \myemptytele &) & \mymetagoes & \myemptytele \\
2777 & \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) \\
2778 & \myhyps(\myb{P}, & (\myb{x} {:} \mytya) \mycc \mytele & ) & \mymetagoes & \myhyps(\myb{P}, \mytele)
2786 \mydesc{reduction elaboration:}{\mydeclsyn \myelabf \myctx \vdash \mytmsyn \myred \mytmsyn}{
2788 $\myadt{\mytyc{D}}{\mytele}{}{ \cdots \ |\ \mydc{c}_n : \mytele_n } \ \ \myelabf$
2789 \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
2790 \AxiomC{$\mytyc{D}.\mydc{c}_i : \mytele;\mytele_i \myarr \myapp{\mytyc{D}}{\mytelee} \in \myctx$}
2792 \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)}
2794 \DisplayProof \\ \vspace{0.2cm}\ \\
2796 \begin{array}{@{}l l@{\ } l@{} r c l}
2797 \textbf{where} & \myrecs(\myse{P}, \vec{m}, & \myemptytele &) & \mymetagoes & \myemptytele \\
2798 & \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) \\
2799 & \myrecs(\myse{P}, \vec{m}, & (\myb{x} {:} \mytya); \mytele &) & \mymetagoes & \myrecs(\myse{P}, \vec{m}, \mytele)
2806 \mydesc{syntax elaboration:}{\myelab{\mydeclsyn}{\mytmsyn ::= \cdots}}{
2809 \begin{array}{r@{\ }c@{\ }l}
2810 \myctx & \myelabt & \myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \\
2813 \begin{array}{r@{\ }c@{\ }l}
2814 \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 \\
2822 \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
2826 \myinf{\mytele \myarr \mytyp}{\mytyp}\hspace{0.8cm}
2827 \mytyc{D} \not\in \myctx \\
2828 \myinff{\myctx; \mytele; (\myb{f}_j : \myse{F}_j)_{j=1}^{i - 1}}{F_i}{\mytyp} \myind{3} (1 \le i \le n)
2832 \begin{array}{r@{\ }c@{\ }l}
2833 \myctx & \myelabt & \myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \\
2834 & & \vspace{-0.2cm} \\
2835 & \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}; \\
2836 & & \mytyc{D}.\mydc{constr} : \mytele \myarr \myse{F}_1 \myarr \cdots \myarr \myse{F}_n \myarr \myapp{\mytyc{D}}{\mytelee};
2844 \mydesc{reduction elaboration:}{\mydeclsyn \myelabf \myctx \vdash \mytmsyn \myred \mytmsyn}{
2846 $\myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \ \ \myelabf$
2847 \AxiomC{$\mytyc{D} \in \myctx$}
2848 \UnaryInfC{$\myctx \vdash \myapp{\mytyc{D}.\myfun{f}_i}{(\mytyc{D}.\mydc{constr} \myappsp \vec{t})} \myred t_i$}
2852 \caption{Elaboration for data types and records.}
2856 Following the intuition given by the examples, the mechanised
2857 elaboration is presented in Figure \ref{fig:elab}, which is essentially
2858 a modification of Figure 9 of \citep{McBride2004}\footnote{However, our
2859 datatypes do not have indices, we do bidirectional typechecking by
2860 treating constructors/destructors as syntactic constructs, and we have
2863 In data type declarations we allow recursive occurrences as long as
2864 they are \emph{strictly positive}, employing a syntactic check to make
2865 sure that this is the case. See \cite{Dybjer1991} for a more formal
2866 treatment of inductive definitions in ITT.
2868 For what concerns records, recursive occurrences are disallowed. The
2869 reason for this choice is answered by the reason for the choice of
2870 having records at all: we need records to give the user types with
2871 $\eta$-laws for equality, as we saw in Section \ref{sec:eta-expand}
2872 and in the treatment of OTT in Section \ref{sec:ott}. If we tried to
2873 $\eta$-expand recursive data types, we would expand forever.
2875 To implement bidirectional type checking for constructors and
2876 destructors, we store their types in full in the context, and then
2877 instantiate when due:
2879 \mydesc{typing:}{\myctx \vdash \mytmsyn \Leftrightarrow \mytmsyn}{
2882 \mytyc{D} : \mytele \myarr \mytyp \in \myctx \hspace{1cm}
2883 \mytyc{D}.\mydc{c} : \mytele \mycc \mytele' \myarr
2884 \myapp{\mytyc{D}}{\mytelee} \in \myctx \\
2885 \mytele'' = (\mytele;\mytele')\vec{A} \hspace{1cm}
2886 \mychkk{\myctx; \mytake_{i-1}(\mytele'')}{t_i}{\myix_i( \mytele'')}\ \
2887 (1 \le i \le \mytele'')
2890 \UnaryInfC{$\mychk{\myapp{\mytyc{D}.\mydc{c}}{\vec{t}}}{\myapp{\mytyc{D}}{\vec{A}}}$}
2895 \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
2896 \AxiomC{$\mytyc{D}.\myfun{f} : \mytele \mycc (\myb{x} {:}
2897 \myapp{\mytyc{D}}{\mytelee}) \myarr \myse{F}$}
2898 \AxiomC{$\myjud{\mytmt}{\myapp{\mytyc{D}}{\vec{A}}}$}
2899 \TrinaryInfC{$\myinf{\myapp{\mytyc{D}.\myfun{f}}{\mytmt}}{(\mytele
2900 \mycc (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr
2901 \myse{F})(\vec{A};\mytmt)}$}
2905 \subsubsection{Why user defined types? Why eliminators?}
2907 The `hardest' design choice when designing $\mykant$\ was to decide
2908 whether user defined types should be included. In the end, we can
2911 % TODO reference levitated theories, indexed containers
2915 \subsection{Cumulative hierarchy and typical ambiguity}
2916 \label{sec:term-hierarchy}
2918 Having a well founded type hierarchy is crucial if we want to retain
2919 consistency, otherwise we can break our type systems by proving bottom,
2920 as shown in Appendix \ref{sec:hurkens}.
2922 However, hierarchy as presented in section \label{sec:itt} is a
2923 considerable burden on the user, on various levels. Consider for
2924 example how we recovered disjunctions in Section \ref{sec:disju}: we
2925 have a function that takes two $\mytyp_0$ and forms a new $\mytyp_0$.
2926 What if we wanted to form a disjunction containing something a
2927 $\mytyp_1$, or $\mytyp_{42}$? Our definition would fail us, since
2928 $\mytyp_1 : \mytyp_2$.
2933 \mydesc{cumulativity:}{\myctx \vdash \mytmsyn \mycumul \mytmsyn}{
2934 \begin{tabular}{ccc}
2935 \AxiomC{$\myctx \vdash \mytya \mydefeq \mytyb$}
2936 \UnaryInfC{$\myctx \vdash \mytya \mycumul \mytyb$}
2939 \AxiomC{\phantom{$\myctx \vdash \mytya \mydefeq \mytyb$}}
2940 \UnaryInfC{$\myctx \vdash \mytyp_l \mycumul \mytyp_{l+1}$}
2943 \AxiomC{$\myctx \vdash \mytya \mycumul \mytyb$}
2944 \AxiomC{$\myctx \vdash \mytyb \mycumul \myse{C}$}
2945 \BinaryInfC{$\myctx \vdash \mytya \mycumul \myse{C}$}
2951 \begin{tabular}{ccc}
2952 \AxiomC{$\myjud{\mytmt}{\mytya}$}
2953 \AxiomC{$\myctx \vdash \mytya \mycumul \mytyb$}
2954 \BinaryInfC{$\myjud{\mytmt}{\mytyb}$}
2957 \AxiomC{$\myctx \vdash \mytya_1 \mydefeq \mytya_2$}
2958 \AxiomC{$\myctx; \myb{x} : \mytya_1 \vdash \mytyb_1 \mycumul \mytyb_2$}
2959 \BinaryInfC{$\myctx (\myb{x} {:} \mytya_1) \myarr \mytyb_1 \mycumul (\myb{x} {:} \mytya_2) \myarr \mytyb_2$}
2963 \caption{Cumulativity rules for base types in \mykant, plus a
2964 `conversion' rule for cumulative types.}
2965 \label{fig:cumulativity}
2968 One way to solve this issue is a \emph{cumulative} hierarchy, where
2969 $\mytyp_{l_1} : \mytyp_{l_2}$ iff $l_1 < l_2$. This way we retain
2970 consistency, while allowing for `large' definitions that work on small
2971 types too. Figure \ref{fig:cumulativity} gives a formal definition of
2972 cumulativity for types, abstractions, and data constructors.
2974 For example we might define our disjunction to be
2976 \myarg\myfun{$\vee$}\myarg : \mytyp_{100} \myarr \mytyp_{100} \myarr \mytyp_{100}
2978 And hope that $\mytyp_{100}$ will be large enough to fit all the types
2979 that we want to use with our disjunction. However, there are two
2980 problems with this. First, there is the obvious clumsyness of having to
2981 manually specify the size of types. More importantly, if we want to use
2982 $\myfun{$\vee$}$ itself as an argument to other type-formers, we need to
2983 make sure that those allow for types at least as large as
2986 A better option is to employ a mechanised version of what Russell called
2987 \emph{typical ambiguity}: we let the user live under the illusion that
2988 $\mytyp : \mytyp$, but check that the statements about types are
2989 consistent under the hood. $\mykant$\ implements this following the
2990 lines of \cite{Huet1988}. See also \citep{Harper1991} for a published
2991 reference, although describing a more complex system allowing for both
2992 explicit and explicit hierarchy at the same time.
2994 We define a partial ordering on the levels, with both weak ($\le$) and
2995 strong ($<$) constraints---the laws governing them being the same as the
2996 ones governing $<$ and $\le$ for the natural numbers. Each occurrence
2997 of $\mytyp$ is decorated with a unique reference, and we keep a set of
2998 constraints and add new constraints as we type check, generating new
2999 references when needed.
3001 For example, when type checking the type $\mytyp\, r_1$, where $r_1$
3002 denotes the unique reference assigned to that term, we will generate a
3003 new fresh reference $\mytyp\, r_2$, and add the constraint $r_1 < r_2$
3004 to the set. When type checking $\myctx \vdash
3005 \myfora{\myb{x}}{\mytya}{\mytyb}$, if $\myctx \vdash \mytya : \mytyp\,
3006 r_1$ and $\myctx; \myb{x} : \mytyb \vdash \mytyb : \mytyp\,r_2$; we will
3007 generate new reference $r$ and add $r_1 \le r$ and $r_2 \le r$ to the
3010 If at any point the constraint set becomes inconsistent, type checking
3011 fails. Moreover, when comparing two $\mytyp$ terms we equate their
3012 respective references with two $\le$ constraints---the details are
3013 explained in Section \ref{sec:hier-impl}.
3015 Another more flexible but also more verbose alternative is the one
3016 chosen by Agda, where levels can be quantified so that the relationship
3017 between arguments and result in type formers can be explicitly
3020 \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}
3022 Inference algorithms to automatically derive this kind of relationship
3023 are currently subject of research. We chose less flexible but more
3024 concise way, since it is easier to implement and better understood.
3028 % \caption{Constraints generated by the typical ambiguity engine. We
3029 % assume some global set of constraints with the ability of generating
3030 % fresh references.}
3031 % \label{fig:hierarchy}
3034 \subsection{Observational equality, \mykant\ style}
3036 There are two correlated differences between $\mykant$\ and the theory
3037 used to present OTT. The first is that in $\mykant$ we have a type
3038 hierarchy, which lets us, for example, abstract over types. The second
3039 is that we let the user define inductive types.
3041 Reconciling propositions for OTT and a hierarchy had already been
3042 investigated by Conor McBride,\footnote{See
3043 \url{http://www.e-pig.org/epilogue/index.html?p=1098.html}.} and we
3044 follow his broad design plan, although with some modifications. Most of
3045 the work, as an extension of elaboration, is to handle reduction rules
3046 and coercions for data types---both type constructors and data
3049 \subsubsection{The \mykant\ prelude, and $\myprop$ositions}
3051 Before defining $\myprop$, we define some basic types inside $\mykant$,
3052 as the target for the $\myprop$ decoder:
3055 \myadt{\mytyc{Empty}}{}{ }{ } \\
3056 \myfun{absurd} : (\myb{A} {:} \mytyp) \myarr \mytyc{Empty} \myarr \myb{A} \mapsto \\
3057 \myind{2} \myabs{\myb{A\ \myb{bot}}}{\mytyc{Empty}.\myfun{elim} \myappsp \myb{bot} \myappsp (\myabs{\_}{\myb{A}})} \\
3060 \myreco{\mytyc{Unit}}{}{}{ } \\ \ \\
3062 \myreco{\mytyc{Prod}}{\myappsp (\myb{A}\ \myb{B} {:} \mytyp)}{ }{\myfun{fst} : \myb{A}, \myfun{snd} : \myb{B} }
3065 When using $\mytyc{Prod}$, we shall use $\myprod$ to define `nested'
3066 products, and $\myproj{n}$ to project elements from them, so that
3069 \mytya \myprod \mytyb = \mytyc{Prod} \myappsp \mytya \myappsp (\mytyc{Prod} \myappsp \mytyb \myappsp \myunit) \\
3070 \mytya \myprod \mytyb \myprod \myse{C} = \mytyc{Prod} \myappsp \mytya \myappsp (\mytyc{Prod} \myappsp \mytyb \myappsp (\mytyc{Prod} \myappsp \mytyc \myappsp \myunit)) \\
3072 \myproj{1} : \mytyc{Prod} \myappsp \mytya \myappsp \mytyb \myarr \mytya \\
3073 \myproj{2} : \mytyc{Prod} \myappsp \mytya \myappsp (\mytyc{Prod} \myappsp \mytyb \myappsp \myse{C}) \myarr \mytyb \\
3077 And so on, so that $\myproj{n}$ will work with all products with at
3078 least than $n$ elements. Then we can define propositions, and decoding:
3082 \begin{array}{r@{\ }c@{\ }l}
3083 \mytmsyn & ::= & \cdots \mysynsep \myprdec{\myprsyn} \\
3084 \myprsyn & ::= & \mybot \mysynsep \mytop \mysynsep \myprsyn \myand \myprsyn \mysynsep \myprfora{\myb{x}}{\mytmsyn}{\myprsyn}
3089 \mydesc{proposition decoding:}{\myprdec{\mytmsyn} \myred \mytmsyn}{
3092 \begin{array}{l@{\ }c@{\ }l}
3093 \myprdec{\mybot} & \myred & \myempty \\
3094 \myprdec{\mytop} & \myred & \myunit
3099 \begin{array}{r@{ }c@{ }l@{\ }c@{\ }l}
3100 \myprdec{&\myse{P} \myand \myse{Q} &} & \myred & \myprdec{\myse{P}} \myprod \myprdec{\myse{Q}} \\
3101 \myprdec{&\myprfora{\myb{x}}{\mytya}{\myse{P}} &} & \myred &
3102 \myfora{\myb{x}}{\mytya}{\myprdec{\myse{P}}}
3108 Adopting the same convention as with $\mytyp$-level products, we will
3109 nest $\myand$ in the same way.
3111 \subsubsection{Some OTT examples}
3113 Before presenting the direction that $\mykant$\ takes, let us consider
3114 some examples of use-defined data types, and the result we would expect,
3115 given what we already know about OTT, assuming the same propositional
3120 \item[Product types] Let's consider first the already mentioned
3121 dependent product, using the alternate name $\mysigma$\footnote{For
3122 extra confusion, `dependent products' are often called `dependent
3123 sums' in the literature, referring to the interpretation that
3124 identifies the first element as a `tag' deciding the type of the
3125 second element, which lets us recover sum types (disjuctions), as we
3126 saw in Section \ref{sec:user-type}. Thus, $\mysigma$.} to
3127 avoid confusion with the $\mytyc{Prod}$ in the prelude:
3130 \myreco{\mysigma}{\myappsp (\myb{A} {:} \mytyp) \myappsp (\myb{B} {:} \myb{A} \myarr \mytyp)}{\\ \myind{2}}{\myfst : \myb{A}, \mysnd : \myapp{\myb{B}}{\myb{fst}}}
3133 Let's start with type-level equality. The result we want is
3136 \mysigma \myappsp \mytya_1 \myappsp \mytyb_1 \myeq \mysigma \myappsp \mytya_2 \myappsp \mytyb_2 \myred \\
3137 \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}}}
3140 The difference here is that in the original presentation of OTT
3141 the type binders are explicit, while here $\mytyb_1$ and $\mytyb_2$ are
3142 functions returning types. We can do this thanks to the type
3143 hierarchy, and this hints at the fact that heterogeneous equality will
3144 have to allow $\mytyp$ `to the right of the colon', and in fact this
3145 provides the solution to simplify the equality above.
3147 If we take, just like we saw previously in OTT
3150 \myjm{\myse{f}_1}{\myfora{\mytya_1}{\myb{x_1}}{\mytyb_1}}{\myse{f}_2}{\myfora{\mytya_2}{\myb{x_2}}{\mytyb_2}} \myred \\
3151 \myind{2} \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{
3152 \myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2} \myimpl
3153 \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}]}
3157 Then we can simply take
3160 \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}
3163 Which will reduce to precisely what we desire. For what
3164 concerns coercions and quotation, things stay the same (apart from the
3165 fact that we apply to the second argument instead of substituting).
3166 We can recognise records such as $\mysigma$ as such and employ
3167 projections in value equality and coercions; as to not
3168 impede progress if not necessary.
3170 \item[Lists] Now for finite lists, which will give us a taste for data
3174 \myadt{\mylist}{\myappsp (\myb{A} {:} \mytyp)}{ }{\mydc{nil} \mydcsep \mydc{cons} \myappsp \myb{A} \myappsp (\myapp{\mylist}{\myb{A}})}
3177 Type equality is simple---we only need to compare the parameter:
3179 \mylist \myappsp \mytya_1 \myeq \mylist \myappsp \mytya_2 \myred \mytya_1 \myeq \mytya_2
3181 For coercions, we transport based on the constructor, recycling the
3182 proof for the inductive occurrence:
3184 \begin{array}{@{}l@{\ }c@{\ }l}
3185 \mycoe \myappsp (\mylist \myappsp \mytya_1) \myappsp (\mylist \myappsp \mytya_2) \myappsp \myse{Q} \myappsp \mydc{nil} & \myred & \mydc{nil} \\
3186 \mycoe \myappsp (\mylist \myappsp \mytya_1) \myappsp (\mylist \myappsp \mytya_2) \myappsp \myse{Q} \myappsp (\mydc{cons} \myappsp \mytmm \myappsp \mytmn) & \myred & \\
3187 \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)}
3190 Value equality is unsurprising---we match the constructors, and
3191 return bottom for mismatches. However, we also need to equate the
3192 parameter in $\mydc{nil}$:
3194 \begin{array}{r@{ }c@{\ }c@{\ }c@{}l@{\ }c@{\ }r@{}c@{\ }c@{\ }c@{}l@{\ }l}
3195 (& \mydc{nil} & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{nil} & : & \myapp{\mylist}{\mytya_2} &) \myred \mytya_1 \myeq \mytya_2 \\
3196 (& \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 \\
3197 & \multicolumn{11}{@{}l}{ \myind{2}
3198 \myjm{\mytmm_1}{\mytya_1}{\mytmm_2}{\mytya_2} \myand \myjm{\mytmn_1}{\myapp{\mylist}{\mytya_1}}{\mytmn_2}{\myapp{\mylist}{\mytya_2}}
3200 (& \mydc{nil} & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{cons} \myappsp \mytmm_2 \myappsp \mytmn_2 & : & \myapp{\mylist}{\mytya_2} &) \myred \mybot \\
3201 (& \mydc{cons} \myappsp \mytmm_1 \myappsp \mytmn_1 & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{nil} & : & \myapp{\mylist}{\mytya_2} &) \myred \mybot
3207 Now for something useless but complicated.
3211 \subsubsection{Only one equality}
3213 Given the examples above, a more `flexible' heterogeneous emerged, since
3214 of the fact that in $\mykant$ we re-gain the possibility of abstracting
3215 and in general handling sets in a way that was not possible in the
3216 original OTT presentation. Moreover, we found that the rules for value
3217 equality work very well if used with user defined type
3218 abstractions---for example in the case of dependent products we recover
3219 the original definition with explicit binders, in a very simple manner.
3221 In fact, we can drop a separate notion of type-equality, which will
3222 simply be served by $\myjm{\mytya}{\mytyp}{\mytyb}{\mytyp}$, from now on
3223 abbreviated as $\mytya \myeq \mytyb$. We shall still distinguish
3224 equalities relating types for hierarchical purposes. The full rules for
3225 equality reductions, along with the syntax for propositions, are given
3226 in figure \ref{fig:kant-eq-red}. We exploit record to perform
3227 $\eta$-expansion. Moreover, given the nested $\myand$s, values of data
3228 types with zero constructors (such as $\myempty$) and records with zero
3229 destructors (such as $\myunit$) will be automatically always identified
3236 \begin{array}{r@{\ }c@{\ }l}
3237 \myprsyn & ::= & \cdots \mysynsep \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
3242 % \mytmsyn & ::= & \cdots \mysynsep \mycoee{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \mysynsep
3243 % \mycohh{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
3244 % \myprsyn & ::= & \cdots \mysynsep \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
3248 % \mydesc{typing:}{\myctx \vdash \mytmsyn \Leftrightarrow \mytmsyn}{
3250 % \begin{tabular}{cc}
3251 % \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
3252 % \AxiomC{$\myjud{\mytmt}{\mytya}$}
3253 % \BinaryInfC{$\myinf{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}$}
3256 % \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
3257 % \AxiomC{$\myjud{\mytmt}{\mytya}$}
3258 % \BinaryInfC{$\myinf{\mycohh{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\myprdec{\myjm{\mytmt}{\mytya}{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}}}$}
3265 \mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
3268 \AxiomC{\phantom{$\myjud{\myse{P}}{\myprop}$}}
3269 \UnaryInfC{$\myjud{\mytop}{\myprop}$}
3271 \UnaryInfC{$\myjud{\mybot}{\myprop}$}
3274 \AxiomC{$\myjud{\myse{P}}{\myprop}$}
3275 \AxiomC{$\myjud{\myse{Q}}{\myprop}$}
3276 \BinaryInfC{$\myjud{\myse{P} \myand \myse{Q}}{\myprop}$}
3278 \UnaryInfC{\phantom{$\myjud{\mybot}{\myprop}$}}
3287 \phantom{\myjud{\myse{A}}{\mytyp} \hspace{0.8cm} \myjud{\mytmm}{\myse{A}}} \\
3288 \myjud{\myse{A}}{\mytyp}\hspace{0.8cm}
3289 \myjudd{\myctx; \myb{x} : \mytya}{\myse{P}}{\myprop}
3292 \UnaryInfC{$\myjud{\myprfora{\myb{x}}{\mytya}{\myse{P}}}{\myprop}$}
3297 \myjud{\myse{A}}{\mytyp} \hspace{0.8cm} \myjud{\mytmm}{\myse{A}} \\
3298 \myjud{\myse{B}}{\mytyp} \hspace{0.8cm} \myjud{\mytmn}{\myse{B}}
3301 \UnaryInfC{$\myjud{\myjm{\mytmm}{\myse{A}}{\mytmn}{\myse{B}}}{\myprop}$}
3308 \mydesc{equality reduction:}{\myctx \vdash \myprsyn \myred \myprsyn}{
3312 \UnaryInfC{$\myctx \vdash \myjm{\mytyp}{\mytyp}{\mytyp}{\mytyp} \myred \mytop$}
3316 \UnaryInfC{$\myctx \vdash \myjm{\myprdec{\myse{P}}}{\mytyp}{\myprdec{\myse{Q}}}{\mytyp} \myred \mytop$}
3324 \begin{array}{@{}r@{\ }l}
3326 \myjm{\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}}{\mytyp}{\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}}{\mytyp} \myred \\
3327 & \myind{2} \mytya_2 \myeq \mytya_1 \myand \myprfora{\myb{x_2}}{\mytya_2}{\myprfora{\myb{x_1}}{\mytya_1}{
3328 \myjm{\myb{x_2}}{\mytya_2}{\myb{x_1}}{\mytya_1} \myimpl \mytyb_1[\myb{x_1}] \myeq \mytyb_2[\myb{x_2}]
3338 \begin{array}{@{}r@{\ }l}
3340 \myjm{\myse{f}_1}{\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}}{\myse{f}_2}{\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}} \myred \\
3341 & \myind{2} \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{
3342 \myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2} \myimpl
3343 \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}]}
3352 \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
3354 \begin{array}{r@{\ }l}
3356 \myjm{\mytyc{D} \myappsp \vec{A}}{\mytyp}{\mytyc{D} \myappsp \vec{B}}{\mytyp} \myred \\
3357 & \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}))})
3366 \mydataty(\mytyc{D}, \myctx)\hspace{0.8cm}
3367 \mytyc{D}.\mydc{c} : \mytele;\mytele' \myarr \mytyc{D} \myappsp \mytelee \in \myctx \hspace{0.8cm}
3368 \mytele_A = (\mytele;\mytele')\vec{A}\hspace{0.8cm}
3369 \mytele_B = (\mytele;\mytele')\vec{B}
3373 \begin{array}{@{}l@{\ }l}
3374 \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 \\
3375 & \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}))})
3382 \AxiomC{$\mydataty(\mytyc{D}, \myctx)$}
3384 \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
3392 \myisreco(\mytyc{D}, \myctx)\hspace{0.8cm}
3393 \mytyc{D}.\myfun{f}_i : \mytele; (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr \myse{F}_i \in \myctx\\
3397 \begin{array}{@{}l@{\ }l}
3398 \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})})
3405 \UnaryInfC{$\myjm{\mytmm}{\mytya}{\mytmn}{\mytyb} \myred \mybot\ \text{if $\mytya$ and $\mytyb$ are canonical types.}$}
3408 \caption{Propositions and equality reduction in $\mykant$. We assume
3409 the presence of $\mydataty$ and $\myisreco$ as operations on the
3410 context to recognise whether a user defined type is a data type or a
3412 \label{fig:kant-eq-red}
3415 \subsubsection{Coercions}
3418 % \mydesc{reduction}{\mytmsyn \myred \mytmsyn}{
3421 % \caption{Coercions in \mykant.}
3422 % \label{fig:kant-coe}
3427 \subsubsection{$\myprop$ and the hierarchy}
3429 We shall have, at earch universe level, not only a $\mytyp_l$ but also a
3430 $\myprop_l$. Where will propositions placed in the type hierarchy? The
3431 main indicator is the decoding operator, since it converts into things
3432 that already live in the hierarchy. For example, if we have
3434 \myprdec{\mynat \myarr \mybool \myeq \mynat \myarr \mybool} \myred
3435 \mytop \myand ((\myb{x}\, \myb{y} : \mynat) \myarr \mytop \myarr \mytop)
3437 we will better make sure that the `to be decoded' is at the same
3438 level as its reduction as to preserve subject reduction. In the example
3439 above, we'll have that proposition to be at least as large as the type
3440 of $\mynat$, since the reduced proof will abstract over it. Pretending
3441 that we had explicit, non cumulative levels, it would be tempting to have
3444 \AxiomC{$\myjud{\myse{Q}}{\myprop_l}$}
3445 \UnaryInfC{$\myjud{\myprdec{\myse{Q}}}{\mytyp_l}$}
3448 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
3449 \AxiomC{$\myjud{\mytyb}{\mytyp_l}$}
3450 \BinaryInfC{$\myjud{\myjm{\mytya}{\mytyp_{l}}{\mytyb}{\mytyp_{l}}}{\myprop_l}$}
3454 $\mybot$ and $\mytop$ living at any level, $\myand$ and $\forall$
3455 following rules similar to the ones for $\myprod$ and $\myarr$ in
3456 Section \ref{sec:itt}. However, we need to be careful with value
3457 equality since for example we have that
3459 \myprdec{\myjm{\myse{f}_1}{\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}}{\myse{f}_2}{\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}}}
3461 \myfora{\myb{x_1}}{\mytya_1}{\myfora{\myb{x_2}}{\mytya_2}{\cdots}}
3463 where the proposition decodes into something of at least type $\mytyp_l$, where
3464 $\mytya_l : \mytyp_l$ and $\mytyb_l : \mytyp_l$. We can resolve this
3465 tension by making all equalities larger:
3467 \AxiomC{$\myjud{\mytmm}{\mytya}$}
3468 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
3469 \AxiomC{$\myjud{\mytmn}{\mytyb}$}
3470 \AxiomC{$\myjud{\mytyb}{\mytyp_l}$}
3471 \QuaternaryInfC{$\myjud{\myjm{\mytmm}{\mytya}{\mytmm}{\mytya}}{\myprop_l}$}
3473 This is disappointing, since type equalities will be needlessly large:
3474 $\myprdec{\myjm{\mytya}{\mytyp_l}{\mytyb}{\mytyp_l}} : \mytyp_{l + 1}$.
3476 However, considering that our theory is cumulative, we can do better.
3477 Assuming rules for $\myprop$ cumulativity similar to the ones for
3478 $\mytyp$, we will have (with the conversion rule reproduced as a
3482 \AxiomC{$\myctx \vdash \mytya \mycumul \mytyb$}
3483 \AxiomC{$\myjud{\mytmt}{\mytya}$}
3484 \BinaryInfC{$\myjud{\mytmt}{\mytyb}$}
3487 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
3488 \AxiomC{$\myjud{\mytyb}{\mytyp_l}$}
3489 \BinaryInfC{$\myjud{\myjm{\mytya}{\mytyp_{l}}{\mytyb}{\mytyp_{l}}}{\myprop_l}$}
3495 \AxiomC{$\myjud{\mytmm}{\mytya}$}
3496 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
3497 \AxiomC{$\myjud{\mytmn}{\mytyb}$}
3498 \AxiomC{$\myjud{\mytyb}{\mytyp_l}$}
3499 \AxiomC{$\mytya$ and $\mytyb$ are not $\mytyp_{l'}$}
3500 \QuinaryInfC{$\myjud{\myjm{\mytmm}{\mytya}{\mytmm}{\mytya}}{\myprop_l}$}
3504 That is, we are small when we can (type equalities) and large otherwise.
3505 This would not work in a non-cumulative theory because subject reduction
3506 would not hold. Consider for instance
3508 \myjm{\mynat}{\myITE{\mytrue}{\mytyp_0}{\mytyp_0}}{\mybool}{\myITE{\mytrue}{\mytyp_0}{\mytyp_0}}
3512 \[\myjm{\mynat}{\mytyp_0}{\mybool}{\mytyp_0} : \myprop_0 \]
3513 We need $\myprop_0$ to be $\myprop_1$ too, which will be the case with
3514 cumulativity. This is not the most elegant of systems, but it buys us a
3515 cheap type level equality without having to replicate functionality with
3516 a dedicated construct.
3518 \subsubsection{Quotation and definitional equality}
3519 \label{sec:kant-irr}
3521 Now we can give an account of definitional equality, by explaining how
3522 to perform quotation (as defined in Section \ref{sec:eta-expand})
3523 towards the goal described in Section \ref{sec:ott-quot}.
3527 \item Perform $\eta$-expansion on functions and records.
3529 \item As a consequence of the previous point, identify all records with
3530 no projections as equal, since they will have only one element.
3532 \item Identify all members of types with no elements as equal.
3534 \item Identify all equivalent proofs as equal---with `equivalent proof'
3535 we mean those proving the same propositions.
3537 \item Advance coercions working across definitionally equal types.
3539 Towards these goals and following the intuition between bidirectional
3540 type checking we define two mutually recursive functions, one quoting
3541 canonical terms against their types (since we need the type to typecheck
3542 canonical terms), one quoting neutral terms while recovering their
3545 Our quotation will work on normalised terms, so that all defined values
3546 will have been replaced. Moreover, we match on datatype eliminators and
3547 all their arguments, so that $\mynat.\myfun{elim} \myappsp \vec{\mytmt}$
3548 will stand for $\mynat.\myfun{elim}$ applied to the scrutinised
3549 $\mynat$, plus its three arguments. This measure can be easily
3550 implemented by checking the head of applications and `consuming' the
3555 \mydesc{canonical quotation:}{\mycanquot(\myctx, \mytmsyn : \mytmsyn) \mymetagoes \mytmsyn}{
3559 \mycanquot(\myctx, \mytmt : \mytyc{D} \myappsp \vec{A}) \mymetaguard \mymeta{empty}(\myctx, \mytyc{D}) \mymetagoes \boxed{\mytmt} \\
3560 \mycanquot(\myctx, \mytmt : \mytyc{D} \myappsp \vec{A}) \mymetaguard \mymeta{record}(\myctx, \mytyc{D}) \mymetagoes \\ \myind{2} \mytyc{D}.\mydc{constr} \myappsp \cdots \myappsp \mycanquot(\myctx, \mytyc{D}.\myfun{f}_n : (\myctx(\mytyc{D}.\myfun{f}_n))(\vec{A};\mytmt)) \\
3561 \mycanquot(\myctx, \mytyc{D}.\mydc{c} \myappsp \vec{t} : \mytyc{D} \myappsp \vec{A}) \mymetagoes \cdots \\
3562 \mycanquot(\myctx, \myse{f} : \myfora{\myb{x}}{\mytya}{\mytyb}) \mymetagoes \myabs{\myb{x}}{\mycanquot(\myctx; \myb{x} : \mytya, \myapp{\myse{f}}{\myb{x}} : \mytyb)} \\
3563 \mycanquot(\myctx, \myse{p} : \myprdec{\myse{P}}) \mymetagoes \boxed{\myse{p}}
3565 \mycanquot(\myctx, \mytmt : \mytya) \mymetagoes \mytmt'\text{, where}\ \mytmt' : \myarg = \myneuquot(\myctx, \mytmt)
3572 \mydesc{neutral quotation:}{\myneuquot(\myctx, \mytmsyn) \mymetagoes \mytmsyn : \mytmsyn}{
3575 \begin{array}{@{}l@{}l}
3576 \myneuquot(\myctx,\ \myb{x} &) \mymetagoes \myb{x} : \myctx(\myb{x}) \\
3577 \myneuquot(\myctx,\ \mytyp &) \mymetagoes \mytyp : \mytyp \\
3578 \myneuquot(\myctx,\ \myfora{\myb{x}}{\mytya}{\mytyb} & ) \mymetagoes
3579 \myfora{\myb{x}}{\myneuquot(\myctx, \mytya)}{\myneuquot(\myctx; \myb{x} : \mytya, \mytyb)} : \mytyp \\
3580 \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 \\
3581 \myneuquot(\myctx,\ \myprdec{\myjm{\mytmm}{\mytya}{\mytmn}{\mytyb}} &) \mymetagoes \myprdec{\myjm{\mycanquot(\myctx, \mytmm : \mytya)}{\mytya'}{\mycanquot(\myctx, \mytmn : \mytyb)}{\mytyb'}} : \mytyp \\
3582 \multicolumn{2}{@{}l}{\myind{2}\text{where}\ \mytya' : \myarg = \myneuquot(\myctx, \mytya)\text{, and}\ \mytyb' : \myarg = \myneuquot(\myctx, \mytyb)} \\
3583 \myneuquot(\myctx,\ \mytyc{D}.\myfun{f} \myappsp \mytmt &) \mymetaguard \mymeta{record}(\myctx, \mytyc{D}) \mymetagoes \\
3584 \multicolumn{2}{@{}l}{\myind{2} \mytyc{D}.\myfun{f} \myappsp \mytmt' : (\myctx(\mytyc{D}.\myfun{f}))(\vec{A};\mytmt)\text{, where}\ \mytmt' : \mytyc{D} \myappsp \vec{A} = \myneuquot(\myctx, \mytmt)} \\
3585 \myneuquot(\myctx,\ \mytyc{D}.\myfun{elim} \myappsp \mytmt \myappsp \myse{P} &) \mymetaguard \mymeta{empty}(\myctx, \mytyc{D}) \mymetagoes \mytyc{D}.\myfun{elim} \myappsp \boxed{\mytmt} \myappsp \myneuquot(\myctx, \myse{P} \myappsp \mytmt) \\
3586 \myneuquot(\myctx,\ \mytyc{D}.\myfun{elim} \myappsp \mytmm \myappsp \myse{P} \myappsp \vec{\mytmn} &) \mymetagoes \cdots \\
3587 \myneuquot(\myctx,\ \myapp{\myse{f}}{\mytmt} &) \mymetagoes \\
3588 \multicolumn{2}{@{}l}{\myind{2} \myapp{\myse{f'}}{\mycanquot(\myctx, \mytmt : \mytya)} : \mysub{\mytyb}{\myb{x}}{\mytmt}\text{, where}\ \myse{f'} : \myfora{\myb{x}}{\mytya}{\mytyb} = \myneuquot(\myctx, \myse{f})} \\
3589 \myneuquot(\myctx,\ \mycoee{\mytya}{\mytyb}{\myse{Q}}{\mytmt} &) \mymetaguard \myneuquot(\myctx, \mytya) \mydefeq_{\mybox} \myneuquot(\myctx, \mytyb) \mymetagoes \myneuquot(\myctx, \mytmt) \\
3590 \myneuquot(\myctx,\ \mycoee{\mytya}{\mytyb}{\myse{Q}}{\mytmt} &) \mymetagoes
3591 \mycoee{\myneuquot(\myctx, \mytya)}{\myneuquot(\myctx, \mytyb)}{\boxed{\myse{Q}}}{\myneuquot(\myctx, \mytmt)}
3595 \caption{Quotation in \mykant.}
3596 \label{fig:kant-quot}
3601 \subsubsection{Why $\myprop$?}
3603 It is worth to ask if $\myprop$ is needed at all. It is perfectly
3604 possible to have the type checker identify propositional types
3605 automatically, and in fact in some sense we already do during equality
3606 reduction and quotation. However, this has the considerable
3607 disadvantage that we can never identify abstracted
3608 variables\footnote{And in general neutral terms, although we currently
3609 don't have neutral propositions.} of type $\mytyp$ as $\myprop$, thus
3610 forbidding the user to talk about $\myprop$ explicitly.
3612 This is a considerable impediment, for example when implementing
3613 \emph{quotient types}. With quotients, we let the user specify an
3614 equivalence class over a certain type, and then exploit this in various
3615 way---crucially, we need to be sure that the equivalence given is
3616 propositional, a fact which prevented the use of quotients in dependent
3617 type theories \citep{Jacobs1994}.
3621 \section{\mykant : The practice}
3622 \label{sec:kant-practice}
3624 The codebase consists of around 2500 lines of Haskell, as reported by
3625 the \texttt{cloc} utility. The high level design is inspired by the
3626 work on various incarnations of Epigram, and specifically by the first
3627 version as described \citep{McBride2004} and the codebase for the new
3628 version.\footnote{Available intermittently as a \texttt{darcs}
3629 repository at \url{http://sneezy.cs.nott.ac.uk/darcs/Pig09}.} In many
3630 ways \mykant\ is something in between the first and second version of
3633 The author learnt the hard way the implementation challenges for such a
3634 project, and while there is a solid and working base to work on, the
3635 implementation of observational equality is not currently complete.
3636 However, given the detailed plan in the previous section, doing so
3637 should not prove to be too much work.
3639 The interaction happens in a read-eval-print loop (REPL). The REPL is a
3640 available both as a commandline application and in a web interface,
3641 which is available at \url{kant.mazzo.li} and presents itself as in
3642 figure \ref{fig:kant-web}.
3645 {\small\begin{verbatim}B E R T U S
3646 Version 0.0, made in London, year 2013.
3648 <decl> Declare value/data type/record
3651 :p <term> Pretty print
3653 :r <file> Reload file (erases previous environment)
3654 :i <name> Info about an identifier
3656 >>> :l data/samples/good/common.ka
3658 >>> :e plus three two
3659 suc (suc (suc (suc (suc zero))))
3660 >>> :t plus three two
3661 Type: Nat\end{verbatim}
3664 \caption{A sample run of the \mykant\ prompt.}
3665 \label{fig:kant-web}
3668 The interaction with the user takes place in a loop living in and
3669 updating a context of \mykant\ declarations. A REPL cycle starts with
3670 the user inputing a \mykant\ declaration or another REPL command, which
3671 then goes through various stages that can end up in a context update, or
3672 in failures of various kind. The process is described diagrammatically
3673 in figure \ref{fig:kant-process}:
3677 \item[Parse] In this phase the text input gets converted to a sugared
3678 version of the core language. For example, we accept multiple
3679 arguments in arrow types and abstractions, and we represent variables
3680 with names, while as we will see in Section \ref{sec:term-repr} the
3681 final term types uses a \emph{nameless} representation.
3683 \item[Desugar] The sugared declaration is converted to a core term.
3684 Most notably we go from names to nameless.
3686 \item[ConDestr] Short for `Constructors/Destructors', converts
3687 applications of data destructors and constructors to a special form,
3688 to perform bidirectional type checking.
3690 \item[Reference] Occurrences of $\mytyp$ get decorated by a unique reference,
3691 which is necessary to implement the type hierarchy check.
3693 \item[Elaborate] Converts the declaration to some context items, which
3694 might be a value declaration (type and body) or a data type
3695 declaration (constructors and destructors). This phase works in
3696 tandem with \textbf{Type checking}, which in turns needs to
3697 \textbf{Evaluate} terms.
3699 \item[Distill] and report the result. `Distilling' refers to the
3700 process of converting a core term back to a sugared version that the
3701 user can visualise. This can be necessary both to display errors
3702 including terms or to display result of evaluations or type checking
3703 that the user has requested. Among the other things in this stage we
3704 go from nameless back to names by recycling the names that the user
3705 used originally, as to fabricate a term which is as close as possible
3706 to what it originated from.
3708 \item[Pretty print] Format the terms in a nice way, and display the result to
3715 \tikzstyle{block} = [rectangle, draw, text width=5em, text centered, rounded
3716 corners, minimum height=2.5em, node distance=0.7cm]
3718 \tikzstyle{decision} = [diamond, draw, text width=4.5em, text badly
3719 centered, inner sep=0pt, node distance=0.7cm]
3721 \tikzstyle{line} = [draw, -latex']
3723 \tikzstyle{cloud} = [draw, ellipse, minimum height=2em, text width=5em, text
3724 centered, node distance=1.5cm]
3727 \begin{tikzpicture}[auto]
3728 \node [cloud] (user) {User};
3729 \node [block, below left=1cm and 0.1cm of user] (parse) {Parse};
3730 \node [block, below=of parse] (desugar) {Desugar};
3731 \node [block, below=of desugar] (condestr) {ConDestr};
3732 \node [block, below=of condestr] (reference) {Reference};
3733 \node [block, below=of reference] (elaborate) {Elaborate};
3734 \node [block, left=of elaborate] (tycheck) {Typecheck};
3735 \node [block, left=of tycheck] (evaluate) {Evaluate};
3736 \node [decision, right=of elaborate] (error) {Error?};
3737 \node [block, right=of parse] (pretty) {Pretty print};
3738 \node [block, below=of pretty] (distill) {Distill};
3739 \node [block, below=of distill] (update) {Update context};
3741 \path [line] (user) -- (parse);
3742 \path [line] (parse) -- (desugar);
3743 \path [line] (desugar) -- (condestr);
3744 \path [line] (condestr) -- (reference);
3745 \path [line] (reference) -- (elaborate);
3746 \path [line] (elaborate) edge[bend right] (tycheck);
3747 \path [line] (tycheck) edge[bend right] (elaborate);
3748 \path [line] (elaborate) -- (error);
3749 \path [line] (error) edge[out=0,in=0] node [near start] {yes} (distill);
3750 \path [line] (error) -- node [near start] {no} (update);
3751 \path [line] (update) -- (distill);
3752 \path [line] (pretty) -- (user);
3753 \path [line] (distill) -- (pretty);
3754 \path [line] (tycheck) edge[bend right] (evaluate);
3755 \path [line] (evaluate) edge[bend right] (tycheck);
3758 \caption{High level overview of the life of a \mykant\ prompt cycle.}
3759 \label{fig:kant-process}
3762 Here we will review only a sampling of the more interesting
3763 implementation challenges present when implementing an interactive
3766 \subsection{Term and context representation}
3767 \label{sec:term-repr}
3769 \subsubsection{Naming and substituting}
3771 Perhaps surprisingly, one of the most difficult challenges in
3772 implementing a theory of the kind presented is choosing a good data type
3773 for terms, and specifically handling substitutions in a sane way.
3775 There are two broad schools of thought when it comes to naming
3776 variables, and thus substituting:
3778 \item[Nameful] Bound variables are represented by some enumerable data
3779 type, just as we have described up to now, starting from Section
3780 \ref{sec:untyped}. The problem is that avoiding name capturing is a
3781 nightmare, both in the sense that it is not performant---given that we
3782 need to rename rename substitute each time we `enter' a binder---but
3783 most importantly given the fact that in even more slightly complicated
3784 systems it is very hard to get right, even for experts.
3786 One of the sore spots of explicit names is comparing terms up
3787 $\alpha$-renaming, which again generates a huge amounts of
3788 substitutions and requires special care. We can represent the
3789 relationship between variables and their binders, by...
3791 \item[Nameless] ...getting rid of names altogether, and representing
3792 bound variables with an index referring to the `binding' structure, a
3793 notion introduced by \cite{de1972lambda}. Classically $0$ represents
3794 the variable bound by the innermost binding structure, $1$ the
3795 second-innermost, and so on. For instance with simple abstractions we
3799 \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} \\
3800 \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
3804 While this technique is obviously terrible in terms of human
3805 usability,\footnote{With some people going as far as defining it akin
3806 to an inverse Turing test.} it is much more convenient as an
3807 internal representation to deal with terms mechanically---at least in
3808 simple cases. Moreover, $\alpha$ renaming ceases to be an issue, and
3809 term comparison is purely syntactical.
3811 Nonetheless, more complex, constructs such as pattern matching put
3812 some strain on the indices and many systems end up using explicit
3813 names anyway (Agda, Coq, \dots).
3817 In the past decade or so advancements in the Haskell's type system and
3818 in general the spread new programming practices have enabled to make the
3819 second option much more amenable. \mykant\ thus takes the second path
3820 through the use of Edward Kmett's excellent \texttt{bound}
3821 library.\footnote{Available at
3822 \url{http://hackage.haskell.org/package/bound}.} We decribe its
3823 advantages but also pitfalls in the previously relatively unknown
3824 territory of dependent types---\texttt{bound} being created mostly to
3825 handle more simply typed systems.
3827 \texttt{bound} builds on the work of \cite{Bird1999}, who suggest to
3828 parametrising the term type over the type of the variables, and `nest'
3829 the type each time we enter a scope. If we wanted to define a term for
3830 the untyped $\lambda$-calculus, we might have
3832 -- A type with no members.
3835 data Var v = Bound | Free v
3838 = V v -- Bound variable
3839 | App (Tm v) (Tm v) -- Term application
3840 | Lam (Tm (Var v)) -- Abstraction
3842 Closed terms would be of type \texttt{Tm Empty}, so that there would be
3843 no occurrences of \texttt{V}. However, inside an abstraction, we can
3844 have \texttt{V Bound}, representing the bound variable, and inside a
3845 second abstraction we can have \texttt{V Bound} or \texttt{V (Free
3846 Bound)}. Thus the term
3847 \[\myabs{\myb{x}}{\myabs{\myb{y}}{\myb{x}}}\]
3848 can be represented as
3850 -- The top level term is of type `Tm Empty'.
3851 -- The inner term `Lam (Free Bound)' is of type `Tm (Var Empty)'.
3852 -- The second inner term `V (Free Bound)' is of type `Tm (Var (Var
3854 Lam (Lam (V (Free Bound)))
3856 This allows us to reflect the of a type `nestedness' at the type level,
3857 and since we usually work with functions polymorphic on the parameter
3858 \texttt{v} it's very hard to make mistakes by putting terms of the wrong
3859 nestedness where they don't belong.
3861 Even more interestingly, the substitution operation is perfectly
3862 captured by the \verb|>>=| (bind) operator of the \texttt{Monad}
3867 (>>=) :: m a -> (a -> m b) -> m b
3869 instance Monad Tm where
3870 -- `return'ing turns a variable into a `Tm'
3873 -- `t >>= f' takes a term `t' and a mapping from variables to terms
3874 -- `f' and applies `f' to all the variables in `t', replacing them
3875 -- with the mapped terms.
3877 App m n >>= f = App (m >>= f) (n >>= f)
3879 -- `Lam' is the tricky case: we modify the function to work with bound
3880 -- variables, so that if it encounters `Bound' it leaves it untouched
3881 -- (since the mapping refers to the outer scope); if it encounters a
3882 -- free variable it asks `f' for the term and then updates all the
3883 -- variables to make them refer to the outer scope they were meant to
3885 Lam s >>= f = Lam (s >>= bump)
3886 where bump Bound = return Bound
3887 bump (Free v) = f v >>= V . Free
3889 With this in mind, we can define functions which will not only work on
3890 \verb|Tm|, but on any \verb|Monad|!
3892 -- Replaces free variable `v' with `m' in `n'.
3893 subst :: (Eq v, Monad m) => v -> m v -> m v -> m v
3894 subst v m n = n >>= \v' -> if v == v' then m else return v'
3896 -- Replace the variable bound by `s' with term `t'.
3897 inst :: Monad m => m v -> m (Var v) -> m v
3898 inst t s = do v <- s
3901 Free v' -> return v'
3903 The beauty of this technique is that in a few simple function we have
3904 defined all the core operations in a general and `obviously correct'
3905 way, with the extra confidence of having the type checker looking our
3906 back. For what concerns term equality, we can just ask the Haskell
3907 compiler to derive the instance for the \verb|Eq| type class and since
3908 we are nameless that will be enough (modulo fancy quotation).
3910 Moreover, if we take the top level term type to be \verb|Tm String|, we
3911 get for free a representation of terms with top-level, definitions;
3912 where closed terms contain only \verb|String| references to said
3913 definitions---see also \cite{McBride2004b}.
3915 What are then the pitfalls of this seemingly invincible technique? The
3916 most obvious impediment is the need for polymorphic recursion.
3917 Functions traversing terms parametrised by the variable type will have
3920 -- Infer the type of a term, or return an error.
3921 infer :: Tm v -> Either Error (Tm v)
3923 When traversing under a \verb|Scope| the parameter changes from \verb|v|
3924 to \verb|Var v|, and thus if we do not specify the type for our function explicitly
3925 inference will fail---type inference for polymorphic recursion being
3926 undecidable \citep{henglein1993type}. This causes some annoyance,
3927 especially in the presence of many local definitions that we would like
3930 But the real issue is the fact that giving a type parametrised over a
3931 variable---say \verb|m v|---a \verb|Monad| instance means being able to
3932 only substitute variables for values of type \verb|m v|. This is a
3933 considerable inconvenience. Consider for instance the case of
3934 telescopes, which are a central tool to deal with contexts and other
3935 constructs. In Haskell we can give them a faithful representation
3936 with a data type along the lines of
3938 data Tele m v = End (m v) | Bind (m v) (Tele (Var v))
3939 type TeleTm = Tele Tm
3941 The problem here is that what we want to substitute for variables in
3942 \verb|Tele m v| is \verb|m v| (probably \verb|Tm v|), not \verb|Tele m v| itself! What we need is
3944 bindTele :: Monad m => Tele m a -> (a -> m b) -> Tele m b
3945 substTele :: (Eq v, Monad m) => v -> m v -> Tele m v -> Tele m v
3946 instTele :: Monad m => m v -> Tele m (Var v) -> Tele m v
3948 Not what \verb|Monad| gives us. Solving this issue in an elegant way
3949 has been a major sink of time and source of headaches for the author,
3950 who analysed some of the alternatives---most notably the work by
3951 \cite{weirich2011binders}---but found it impossible to give up the
3952 simplicity of the model above.
3954 That said, our term type is still reasonably brief, as shown in full in
3955 Appendix \ref{app:termrep}. The fact that propositions cannot be
3956 factored out in another data type is an instance of the problem
3957 described above. However the real pain is during elaboration, where we
3958 are forced to treat everything as a type while we would much rather have
3959 telescopes. Future work would include writing a library that marries a
3960 nice interface similar to the one of \verb|bound| with a more flexible
3963 We also make use of a `forgetful' data type (as provided by
3964 \verb|bound|) to store user-provided variables names along with the
3965 `nameless' representation, so that the names will not be considered when
3966 compared terms, but will be available when distilling so that we can
3967 recover variable names that are as close as possible to what the user
3970 \subsubsection{Evaluation}
3972 Another source of contention related to term representation is dealing
3973 with evaluation. Here \mykant\ does not make bold moves, and simply
3974 employs substitution. Before
3975 Moreover, when elaborating user defined types,
3978 \subsubsection{Context}
3980 Given the parmetrised type,
3984 \subsection{Turning constraints into graphs}
3985 \label{sec:hier-impl}
3987 As an interlude from all the types, we will explain how to
3988 implement the typical ambiguity we have spoken about in
3989 \ref{sec:term-hierarchy} efficiently. As mentioned, we have to verify a the
3990 consistency of a set of constraints each time we add a new one. The
3991 constraints range over some set of variables whose members we will
3992 denote with $x, y, z, \dots$. and are of two kinds:
3999 Predictably, $\le$ expresses a reflexive order, and $<$ expresses an
4000 irreflexive order, both working with the same notion of equality, where
4001 $x < y$ implies $x \le y$---they behave like $\le$ and $<$ do on natural
4002 numbers (or in our case, levels in a type hierarchy). We also need an
4003 equality constraint ($x = y$), which can be reduced to two constraints
4004 $x \le y$ and $y \le x$.
4006 Given this specification, we have implemented a standalone Haskell
4007 module---that we plan to release as a standalone library---to
4008 efficiently store and check the consistency of constraints. The problem
4009 predictably reduces to a graph algorithm, and for this reason we also
4010 implement a library for labelled graphs, since the existing Haskell
4011 graph libraries fell short in different areas.\footnote{We tried the
4012 \texttt{Data.Graph} module in
4013 \url{http://hackage.haskell.org/package/containers}, and the much more
4014 featureful \texttt{fgl} library
4015 \url{http://hackage.haskell.org/package/fgl}.}. The interfaces for
4016 these modules are shown in Appendix \ref{app:constraint}. The graph
4017 library is implemented as a modification of the code described by
4020 We represent the set by building a graph where vertices are variables,
4021 and edges are constraints between them. The edges are labelled with the
4022 constraint type ($<$ or $\le$). As we add constraints, $\le$
4023 constraints are replaced by $<$ constraints, so that if we started with
4024 an empty set and added
4026 x \le y,\ y < z,\ z \le k,\ k \le j,\ x < y,\ j \le y
4028 it would generate the graph shown in Figure \ref{fig:graph-one}.
4034 \subsection{Type holes}
4035 \label{sec:type-holes}
4037 Type holes are, in the author's opinion, one of the `killer' features of
4038 interactive theorem provers, and one that is begging to be exported to
4039 the word of mainstream programming. The idea is that when we are
4040 developing a proof or a program we can insert a hole to have the
4041 software tell us the type expected at that point. Furthermore, we can
4042 ask for the type of variables in context, to better understand our
4047 \subsection{Web prompt}
4050 \section{Evaluation}
4052 \section{Future work}
4054 \subsection{Coinduction}
4056 \subsection{Quotient types}
4058 \subsection{Partiality}
4060 \subsection{Pattern matching}
4062 \subsection{Pattern unification}
4064 % TODO coinduction (obscoin, gimenez, jacobs), pattern unification (miller,
4065 % gundry), partiality monad (NAD)
4069 \section{Notation and syntax}
4071 Syntax, derivation rules, and reduction rules, are enclosed in frames describing
4072 the type of relation being established and the syntactic elements appearing,
4075 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
4076 Typing derivations here.
4079 In the languages presented and Agda code samples I also highlight the syntax,
4080 following a uniform color and font convention:
4083 \begin{tabular}{c | l}
4084 $\mytyc{Sans}$ & Type constructors. \\
4085 $\mydc{sans}$ & Data constructors. \\
4086 % $\myfld{sans}$ & Field accessors (e.g. \myfld{fst} and \myfld{snd} for products). \\
4087 $\mysyn{roman}$ & Keywords of the language. \\
4088 $\myfun{roman}$ & Defined values and destructors. \\
4089 $\myb{math}$ & Bound variables.
4093 Moreover, I will from time to time give examples in the Haskell programming
4094 language as defined in \citep{Haskell2010}, which I will typeset in
4095 \texttt{teletype} font. I assume that the reader is already familiar with
4096 Haskell, plenty of good introductions are available \citep{LYAH,ProgInHask}.
4098 When presenting grammars, I will use a word in $\mysynel{math}$ font
4099 (e.g. $\mytmsyn$ or $\mytysyn$) to indicate indicate
4100 nonterminals. Additionally, I will use quite flexibly a $\mysynel{math}$
4101 font to indicate a syntactic element in derivations or meta-operations.
4102 More specifically, terms are usually indicated by lowercase letters
4103 (often $\mytmt$, $\mytmm$, or $\mytmn$); and types by an uppercase
4104 letter (often $\mytya$, $\mytyb$, or $\mytycc$).
4106 When presenting type derivations, I will often abbreviate and present multiple
4107 conclusions, each on a separate line:
4109 \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
4110 \UnaryInfC{$\myjud{\myapp{\myfst}{\mytmt}}{\mytya}$}
4112 \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mytyb}$}
4115 I will often present `definitions' in the described calculi and in
4116 $\mykant$\ itself, like so:
4119 \myfun{name} : \mytysyn \\
4120 \myfun{name} \myappsp \myb{arg_1} \myappsp \myb{arg_2} \myappsp \cdots \mapsto \mytmsyn
4123 To define operators, I use a mixfix notation similar
4124 to Agda, where $\myarg$s denote arguments:
4127 \myarg \mathrel{\myfun{$\wedge$}} \myarg : \mybool \myarr \mybool \myarr \mybool \\
4128 \myb{b_1} \mathrel{\myfun{$\wedge$}} \myb{b_2} \mapsto \cdots
4132 In explicitly typed systems, I will also omit type annotations when they
4133 are obvious, e.g. by not annotating the type of parameters of
4134 abstractions or of dependent pairs.
4136 I will introduce multiple arguments in one go in arrow types:
4138 (\myb{x}\, \myb{y} {:} \mytya) \myarr \cdots = (\myb{x} {:} \mytya) \myarr (\myb{y} {:} \mytya) \myarr \cdots
4140 and in abstractions:
4142 \myabs{\myb{x}\myappsp\myb{y}}{\cdots} = \myabs{\myb{x}}{\myabs{\myb{y}}{\cdots}}
4144 I will also omit arrows to abbreviate types:
4146 (\myb{x} {:} \mytya)(\myb{y} {:} \mytyb) \myarr \cdots =
4147 (\myb{x} {:} \mytya) \myarr (\myb{y} {:} \mytyb) \myarr \cdots
4152 \subsection{ITT renditions}
4153 \label{app:itt-code}
4155 \subsubsection{Agda}
4156 \label{app:agda-itt}
4158 Note that in what follows rules for `base' types are
4159 universe-polymorphic, to reflect the exposition. Derived definitions,
4160 on the other hand, mostly work with \mytyc{Set}, reflecting the fact
4161 that in the theory presented we don't have universe polymorphism.
4167 data Empty : Set where
4169 absurd : ∀ {a} {A : Set a} → Empty → A
4172 ¬_ : ∀ {a} → (A : Set a) → Set a
4175 record Unit : Set where
4178 record _×_ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
4185 data Bool : Set where
4188 if_/_then_else_ : ∀ {a} (x : Bool) (P : Bool → Set a) → P true → P false → P x
4189 if true / _ then x else _ = x
4190 if false / _ then _ else x = x
4192 if_then_else_ : ∀ {a} (x : Bool) {P : Bool → Set a} → P true → P false → P x
4193 if_then_else_ x {P} = if_/_then_else_ x P
4195 data W {s p} (S : Set s) (P : S → Set p) : Set (s ⊔ p) where
4196 _◁_ : (s : S) → (P s → W S P) → W S P
4198 rec : ∀ {a b} {S : Set a} {P : S → Set b}
4199 (C : W S P → Set) → -- some conclusion we hope holds
4200 ((s : S) → -- given a shape...
4201 (f : P s → W S P) → -- ...and a bunch of kids...
4202 ((p : P s) → C (f p)) → -- ...and C for each kid in the bunch...
4203 C (s ◁ f)) → -- ...does C hold for the node?
4204 (x : W S P) → -- If so, ...
4205 C x -- ...C always holds.
4206 rec C c (s ◁ f) = c s f (λ p → rec C c (f p))
4208 module Examples-→ where
4215 -- These pragmas are needed so we can use number literals.
4216 {-# BUILTIN NATURAL ℕ #-}
4217 {-# BUILTIN ZERO zero #-}
4218 {-# BUILTIN SUC suc #-}
4220 data List (A : Set) : Set where
4222 _∷_ : A → List A → List A
4224 length : ∀ {A} → List A → ℕ
4226 length (_ ∷ l) = suc (length l)
4231 suc x > suc y = x > y
4233 head : ∀ {A} → (l : List A) → length l > 0 → A
4234 head [] p = absurd p
4237 module Examples-× where
4243 even (suc zero) = Empty
4244 even (suc (suc n)) = even n
4249 5-not-even : ¬ (even 5)
4252 there-is-an-even-number : ℕ × even
4253 there-is-an-even-number = 6 , 6-even
4255 _∨_ : (A B : Set) → Set
4256 A ∨ B = Bool × (λ b → if b then A else B)
4258 left : ∀ {A B} → A → A ∨ B
4261 right : ∀ {A B} → B → A ∨ B
4264 [_,_] : {A B C : Set} → (A → C) → (B → C) → A ∨ B → C
4266 (if (fst x) / (λ b → if b then _ else _ → _) then f else g) (snd x)
4268 module Examples-W where
4273 Tr b = if b then Unit else Empty
4279 zero = false ◁ absurd
4282 suc n = true ◁ (λ _ → n)
4288 if b / (λ b → (Tr b → ℕ) → (Tr b → ℕ) → ℕ)
4289 then (λ _ f → (suc (f tt))) else (λ _ _ → y))
4292 module Equality where
4295 data _≡_ {a} {A : Set a} : A → A → Set a where
4298 ≡-elim : ∀ {a b} {A : Set a}
4299 (P : (x y : A) → x ≡ y → Set b) →
4300 ∀ {x y} → P x x (refl x) → (x≡y : x ≡ y) → P x y x≡y
4301 ≡-elim P p (refl x) = p
4303 subst : ∀ {A : Set} (P : A → Set) → ∀ {x y} → (x≡y : x ≡ y) → P x → P y
4304 subst P x≡y p = ≡-elim (λ _ y _ → P y) p x≡y
4306 sym : ∀ {A : Set} (x y : A) → x ≡ y → y ≡ x
4307 sym x y p = subst (λ y′ → y′ ≡ x) p (refl x)
4309 trans : ∀ {A : Set} (x y z : A) → x ≡ y → y ≡ z → x ≡ z
4310 trans x y z p q = subst (λ z′ → x ≡ z′) q p
4312 cong : ∀ {A B : Set} (x y : A) → x ≡ y → (f : A → B) → f x ≡ f y
4313 cong x y p f = subst (λ z → f x ≡ f z) p (refl (f x))
4316 \subsubsection{\mykant}
4318 The following things are missing: $\mytyc{W}$-types, since our
4319 positivity check is overly strict, and equality, since we haven't
4320 implemented that yet.
4323 \verbatiminput{itt.ka}
4326 \subsection{\mykant\ examples}
4329 \verbatiminput{examples.ka}
4332 \subsection{\mykant' hierachy}
4335 This rendition of the Hurken's paradox does not type check with the
4336 hierachy enabled, type checks and loops without it. Adapted from an
4337 Agda version, available at
4338 \url{http://code.haskell.org/Agda/test/succeed/Hurkens.agda}.
4341 \verbatiminput{hurkens.ka}
4344 \subsection{Term representation}
4347 Data type for terms in \mykant.
4349 {\small\begin{verbatim}-- A top-level name.
4351 -- A data/type constructor name.
4354 -- A term, parametrised over the variable (`v') and over the reference
4355 -- type used in the type hierarchy (`r').
4358 | Ty r -- Type, with a hierarchy reference.
4359 | Lam (TmScope r v) -- Abstraction.
4360 | Arr (Tm r v) (TmScope r v) -- Dependent function.
4361 | App (Tm r v) (Tm r v) -- Application.
4362 | Ann (Tm r v) (Tm r v) -- Annotated term.
4363 -- Data constructor, the first ConId is the type constructor and
4364 -- the second is the data constructor.
4365 | Con ADTRec ConId ConId [Tm r v]
4366 -- Data destrutor, again first ConId being the type constructor
4367 -- and the second the name of the eliminator.
4368 | Destr ADTRec ConId Id (Tm r v)
4370 | Hole HoleId [Tm r v]
4371 -- Decoding of propositions.
4375 | Prop r -- The type of proofs, with hierarchy reference.
4378 | And (Tm r v) (Tm r v)
4379 | Forall (Tm r v) (TmScope r v)
4380 -- Heterogeneous equality.
4381 | Eq (Tm r v) (Tm r v) (Tm r v) (Tm r v)
4383 -- Either a data type, or a record.
4384 data ADTRec = ADT | Rec
4386 -- Either a coercion, or coherence.
4387 data Coeh = Coe | Coh\end{verbatim}
4390 \subsection{Graph and constraints modules}
4391 \label{app:constraint}
4393 The modules are respectively named \texttt{Data.LGraph} (short for
4394 `labelled graph'), and \texttt{Data.Constraint}. The type class
4395 constraints on the type parameters are not shown for clarity, unless
4396 they are meaningful to the function. In practice we use the
4397 \texttt{Hashable} type class on the vertex to implement the graph
4398 efficiently with hash maps.
4400 \subsubsection{\texttt{Data.LGraph}}
4403 \verbatiminput{graph.hs}
4406 \subsubsection{\texttt{Data.Constraint}}
4409 \verbatiminput{constraint.hs}
4414 \bibliographystyle{authordate1}
4415 \bibliography{thesis}