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}{\Downarrow}}}
263 \newcommand{\myneuquot}{\ensuremath{\textsc{quote}{\Uparrow}}}
264 \newcommand{\mymetaguard}{\ |\ }
265 \newcommand{\mybox}{\Box}
266 \newcommand{\mytermi}[1]{\text{\texttt{#1}}}
267 \newcommand{\mysee}[1]{\langle\myse{#1}\rangle}
269 \renewcommand{\[}{\begin{equation*}}
270 \renewcommand{\]}{\end{equation*}}
271 \newcommand{\mymacol}[2]{\text{\textcolor{#1}{$#2$}}}
273 \newtheorem*{mydef}{Definition}
274 \newtheoremstyle{named}{}{}{\itshape}{}{\bfseries}{}{.5em}{\textsc{#1}}
277 %% -----------------------------------------------------------------------------
279 \title{\mykant: Implementing Observational Equality}
280 \author{Francesco Mazzoli \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{<fm2209@ic.ac.uk>}}}
294 % Upper part of the page. The '~' is needed because \\
295 % only works if a paragraph has started.
296 \includegraphics[width=0.4\textwidth]{brouwer-cropped.png}~\\[1cm]
298 \textsc{\Large Final year project}\\[0.5cm]
301 { \huge \mykant: Implementing Observational Equality}\\[1.5cm]
303 {\Large Francesco \textsc{Mazzoli} \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{<fm2209@ic.ac.uk>}}}\\[0.8cm]
305 \begin{minipage}{0.4\textwidth}
306 \begin{flushleft} \large
308 Dr. Steffen \textsc{van Bakel}
311 \begin{minipage}{0.4\textwidth}
312 \begin{flushright} \large
313 \emph{Second marker:} \\
314 Dr. Philippa \textsc{Gardner}
326 The marriage between programming and logic has been a very fertile
327 one. In particular, since the definition of the simply typed lambda
328 calculus, a number of type systems have been devised with increasing
331 Among this systems, Inutitionistic Type Theory (ITT) has been a very
332 popular framework for theorem provers and programming languages.
333 However, reasoning about equality has always been a tricky business in
334 ITT and related theories. In this thesis we will explain why this is
335 the case, and present Observational Type Theory (OTT), a solution to
336 some of the problems with equality.
338 To bring OTT closer to the current practice of interactive theorem
339 provers, we describe \mykant, a system featuring OTT in a setting more
340 close to the one found in widely used provers such as Agda and Coq.
341 Nost notably, we feature used defined inductive and record types and a
342 cumulative, implicit type hierarchy. Having implemented part of
343 $\mykant$ as a Haskell program, we describe some of the implementation
349 \renewcommand{\abstractname}{Acknowledgements}
351 I would like to thank Steffen van Bakel, my supervisor, who was brave
352 enough to believe in my project and who provided much advice and
355 I would also like to thank the Haskell and Agda community on
356 \texttt{IRC}, which guided me through the strange world of types; and
357 in particular Andrea Vezzosi and James Deikun, with whom I entertained
358 countless insightful discussions over the past year. Andrea suggested
359 Observational Type Theory as a topic of study: this thesis would not
360 exist without him. Before them, Tony Field introduced me to Haskell,
361 unknowingly filling most of my free time from that time on.
363 Finally, much of the work stems from the research of Conor McBride,
364 who answered many of my doubts through these months. I also owe him
374 \section{Introduction}
378 \section{Simple and not-so-simple types}
381 \subsection{The untyped $\lambda$-calculus}
384 Along with Turing's machines, the earliest attempts to formalise
385 computation lead to the definition of the $\lambda$-calculus
386 \citep{Church1936}. This early programming language encodes computation
387 with a minimal syntax and no `data' in the traditional sense, but just
388 functions. Here we give a brief overview of the language, which will
389 give the chance to introduce concepts central to the analysis of all the
390 following calculi. The exposition follows the one found in chapter 5 of
393 \begin{mydef}[$\lambda$-terms]
394 Syntax of the $\lambda$-calculus: variables, abstractions, and
400 \begin{array}{r@{\ }c@{\ }l}
401 \mytmsyn & ::= & \myb{x} \mysynsep \myabs{\myb{x}}{\mytmsyn} \mysynsep (\myapp{\mytmsyn}{\mytmsyn}) \\
402 x & \in & \text{Some enumerable set of symbols}
407 Parenthesis will be omitted in the usual way, with application being
410 Abstractions roughly corresponds to functions, and their semantics is more
411 formally explained by the $\beta$-reduction rule.
413 \begin{mydef}[$\beta$-reduction]
414 $\beta$-reduction and substitution for the $\lambda$-calculus.
417 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
420 \myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{\myb{x}}{\mytmn}\text{, where} \\
422 \begin{array}{l@{\ }c@{\ }l}
423 \mysub{\myb{x}}{\myb{x}}{\mytmn} & = & \mytmn \\
424 \mysub{\myb{y}}{\myb{x}}{\mytmn} & = & y\text{, with } \myb{x} \neq y \\
425 \mysub{(\myapp{\mytmt}{\mytmm})}{\myb{x}}{\mytmn} & = & (\myapp{\mysub{\mytmt}{\myb{x}}{\mytmn}}{\mysub{\mytmm}{\myb{x}}{\mytmn}}) \\
426 \mysub{(\myabs{\myb{x}}{\mytmm})}{\myb{x}}{\mytmn} & = & \myabs{\myb{x}}{\mytmm} \\
427 \mysub{(\myabs{\myb{y}}{\mytmm})}{\myb{x}}{\mytmn} & = & \myabs{\myb{z}}{\mysub{\mysub{\mytmm}{\myb{y}}{\myb{z}}}{\myb{x}}{\mytmn}}, \\
428 \multicolumn{3}{l}{\myind{2} \text{with $\myb{x} \neq \myb{y}$ and $\myb{z}$ not free in $\myapp{\mytmm}{\mytmn}$}}
434 The care required during substituting variables for terms is required to avoid
435 name capturing. We will use substitution in the future for other name-binding
436 constructs assuming similar precautions.
438 These few elements have a remarkable expressiveness, and are in fact
439 Turing complete. As a corollary, we must be able to devise a term that
440 reduces forever (`loops' in imperative terms):
442 (\myapp{\omega}{\omega}) \myred (\myapp{\omega}{\omega}) \myred \cdots \text{, with $\omega = \myabs{x}{\myapp{x}{x}}$}
445 A \emph{redex} is a term that can be reduced.
447 In the untyped $\lambda$-calculus this will be the case for an
448 application in which the first term is an abstraction, but in general we
449 call aterm reducible if it appears to the left of a reduction rule.
450 \begin{mydef}[normal form]
451 A term that contains no redexes is said to be in \emph{normal form}.
453 \begin{mydef}[normalising terms and systems]
454 Terms that reduce in a finite number of reduction steps to a normal
455 form are \emph{normalising}. A system in which all terms are
456 normalising is said to be have the \emph{normalisation property}, or
459 Given the reduction behaviour of $(\myapp{\omega}{\omega})$, it is clear
460 that the untyped $\lambda$-calculus does not have the normalisation
463 We have not presented reduction in an algorithmic way, but
464 \emph{evaluation strategies} can be employed to reduce term
465 systematically. Common evaluation strategies include \emph{call by
466 value} (or \emph{strict}), where arguments of abstractions are reduced
467 before being applied to the abstraction; and conversely \emph{call by
468 name} (or \emph{lazy}), where we reduce only when we need to do so to
469 proceed---in other words when we have an application where the function
470 is still not a $\lambda$. In both these reduction strategies we never
471 reduce under an abstraction: for this reason a weaker form of
472 normalisation is used, where both abstractions and normal forms are said
473 to be in \emph{weak head normal form}.
475 \subsection{The simply typed $\lambda$-calculus}
477 A convenient way to `discipline' and reason about $\lambda$-terms is to assign
478 \emph{types} to them, and then check that the terms that we are forming make
479 sense given our typing rules \citep{Curry1934}.The first most basic instance
480 of this idea takes the name of \emph{simply typed $\lambda$-calculus} (STLC).
481 \begin{mydef}[Simply typed $\lambda$-calculus]
482 The syntax and typing rules for the STLC are given in Figure \ref{fig:stlc}.
485 Our types contain a set of \emph{type variables} $\Phi$, which might
486 correspond to some `primitive' types; and $\myarr$, the type former for
487 `arrow' types, the types of functions. The language is explicitly
488 typed: when we bring a variable into scope with an abstraction, we
489 declare its type. Reduction is unchanged from the untyped
495 \begin{array}{r@{\ }c@{\ }l}
496 \mytmsyn & ::= & \myb{x} \mysynsep \myabss{\myb{x}}{\mytysyn}{\mytmsyn} \mysynsep
497 (\myapp{\mytmsyn}{\mytmsyn}) \\
498 \mytysyn & ::= & \myse{\phi} \mysynsep \mytysyn \myarr \mytysyn \mysynsep \\
499 \myb{x} & \in & \text{Some enumerable set of symbols} \\
500 \myse{\phi} & \in & \Phi
505 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
507 \AxiomC{$\myctx(x) = A$}
508 \UnaryInfC{$\myjud{\myb{x}}{A}$}
511 \AxiomC{$\myjudd{\myctx;\myb{x} : A}{\mytmt}{\mytyb}$}
512 \UnaryInfC{$\myjud{\myabss{x}{A}{\mytmt}}{\mytyb}$}
515 \AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$}
516 \AxiomC{$\myjud{\mytmn}{\mytya}$}
517 \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mytyb}$}
521 \caption{Syntax and typing rules for the STLC. Reduction is unchanged from
522 the untyped $\lambda$-calculus.}
526 In the typing rules, a context $\myctx$ is used to store the types of bound
527 variables: $\myctx; \myb{x} : \mytya$ adds a variable to the context and
528 $\myctx(x)$ extracts the type of the rightmost occurrence of $x$.
530 This typing system takes the name of `simply typed lambda calculus' (STLC), and
531 enjoys a number of properties. Two of them are expected in most type systems
533 \begin{mydef}[Progress]
534 A well-typed term is not stuck---it is either a variable, or it
535 does not appear on the left of the $\myred$ relation (currently
536 only $\lambda$), or it can take a step according to the evaluation rules.
538 \begin{mydef}[Subject reduction]
539 If a well-typed term takes a step of evaluation, then the
540 resulting term is also well-typed, and preserves the previous type.
543 However, STLC buys us much more: every well-typed term is normalising
544 \citep{Tait1967}. It is easy to see that we cannot fill the blanks if we want to
545 give types to the non-normalising term shown before:
547 \myapp{(\myabss{\myb{x}}{\myhole{?}}{\myapp{\myb{x}}{\myb{x}}})}{(\myabss{\myb{x}}{\myhole{?}}{\myapp{\myb{x}}{\myb{x}}})}
550 This makes the STLC Turing incomplete. We can recover the ability to loop by
551 adding a combinator that recurses:
552 \begin{mydef}[Fixed-point combinator]\end{mydef}
555 \begin{minipage}{0.5\textwidth}
557 $ \mytmsyn ::= \cdots b \mysynsep \myfix{\myb{x}}{\mytysyn}{\mytmsyn} $
561 \begin{minipage}{0.5\textwidth}
562 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}} {
563 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytmt}{\mytya}$}
564 \UnaryInfC{$\myjud{\myfix{\myb{x}}{\mytya}{\mytmt}}{\mytya}$}
569 \mydesc{reduction:}{\myjud{\mytmsyn}{\mytmsyn}}{
570 $ \myfix{\myb{x}}{\mytya}{\mytmt} \myred \mysub{\mytmt}{\myb{x}}{(\myfix{\myb{x}}{\mytya}{\mytmt})}$
573 This will deprive us of normalisation, which is a particularly bad thing if we
574 want to use the STLC as described in the next section.
576 \subsection{The Curry-Howard correspondence}
578 It turns out that the STLC can be seen a natural deduction system for
579 intuitionistic propositional logic. Terms correspond to proofs, and
580 their types correspond to the propositions they prove. This remarkable
581 fact is known as the Curry-Howard correspondence, or isomorphism.
583 The arrow ($\myarr$) type corresponds to implication. If we wish to prove that
584 that $(\mytya \myarr \mytyb) \myarr (\mytyb \myarr \mytycc) \myarr (\mytya
585 \myarr \mytycc)$, all we need to do is to devise a $\lambda$-term that has the
588 \myabss{\myb{f}}{(\mytya \myarr \mytyb)}{\myabss{\myb{g}}{(\mytyb \myarr \mytycc)}{\myabss{\myb{x}}{\mytya}{\myapp{\myb{g}}{(\myapp{\myb{f}}{\myb{x}})}}}}
590 Which is known to functional programmers as function composition. Going
591 beyond arrow types, we can extend our bare lambda calculus with useful
592 types to represent other logical constructs.
593 \begin{mydef}[The extended STLC]
594 Figure \ref{fig:natded} shows syntax, reduction, and typing rules for
595 the \emph{extendend simply typed $\lambda$-calculus}.
601 \begin{array}{r@{\ }c@{\ }l}
602 \mytmsyn & ::= & \cdots \\
603 & | & \mytt \mysynsep \myapp{\myabsurd{\mytysyn}}{\mytmsyn} \\
604 & | & \myapp{\myleft{\mytysyn}}{\mytmsyn} \mysynsep
605 \myapp{\myright{\mytysyn}}{\mytmsyn} \mysynsep
606 \myapp{\mycase{\mytmsyn}{\mytmsyn}}{\mytmsyn} \\
607 & | & \mypair{\mytmsyn}{\mytmsyn} \mysynsep
608 \myapp{\myfst}{\mytmsyn} \mysynsep \myapp{\mysnd}{\mytmsyn} \\
609 \mytysyn & ::= & \cdots \mysynsep \myunit \mysynsep \myempty \mysynsep \mytmsyn \mysum \mytmsyn \mysynsep \mytysyn \myprod \mytysyn
614 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
617 \begin{array}{l@{ }l@{\ }c@{\ }l}
618 \myapp{\mycase{\mytmm}{\mytmn}}{(\myapp{\myleft{\mytya} &}{\mytmt})} & \myred &
619 \myapp{\mytmm}{\mytmt} \\
620 \myapp{\mycase{\mytmm}{\mytmn}}{(\myapp{\myright{\mytya} &}{\mytmt})} & \myred &
621 \myapp{\mytmn}{\mytmt}
626 \begin{array}{l@{ }l@{\ }c@{\ }l}
627 \myapp{\myfst &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmm \\
628 \myapp{\mysnd &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmn
634 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
636 \AxiomC{\phantom{$\myjud{\mytmt}{\myempty}$}}
637 \UnaryInfC{$\myjud{\mytt}{\myunit}$}
640 \AxiomC{$\myjud{\mytmt}{\myempty}$}
641 \UnaryInfC{$\myjud{\myapp{\myabsurd{\mytya}}{\mytmt}}{\mytya}$}
648 \AxiomC{$\myjud{\mytmt}{\mytya}$}
649 \UnaryInfC{$\myjud{\myapp{\myleft{\mytyb}}{\mytmt}}{\mytya \mysum \mytyb}$}
652 \AxiomC{$\myjud{\mytmt}{\mytyb}$}
653 \UnaryInfC{$\myjud{\myapp{\myright{\mytya}}{\mytmt}}{\mytya \mysum \mytyb}$}
661 \AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$}
662 \AxiomC{$\myjud{\mytmn}{\mytya \myarr \mytycc}$}
663 \AxiomC{$\myjud{\mytmt}{\mytya \mysum \mytyb}$}
664 \TrinaryInfC{$\myjud{\myapp{\mycase{\mytmm}{\mytmn}}{\mytmt}}{\mytycc}$}
671 \AxiomC{$\myjud{\mytmm}{\mytya}$}
672 \AxiomC{$\myjud{\mytmn}{\mytyb}$}
673 \BinaryInfC{$\myjud{\mypair{\mytmm}{\mytmn}}{\mytya \myprod \mytyb}$}
676 \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
677 \UnaryInfC{$\myjud{\myapp{\myfst}{\mytmt}}{\mytya}$}
680 \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
681 \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mytyb}$}
685 \caption{Rules for the extendend STLC. Only the new features are shown, all the
686 rules and syntax for the STLC apply here too.}
690 Tagged unions (or sums, or coproducts---$\mysum$ here, \texttt{Either}
691 in Haskell) correspond to disjunctions, and dually tuples (or pairs, or
692 products---$\myprod$ here, tuples in Haskell) correspond to
693 conjunctions. This is apparent looking at the ways to construct and
694 destruct the values inhabiting those types: for $\mysum$ $\myleft{ }$
695 and $\myright{ }$ correspond to $\vee$ introduction, and
696 $\mycase{\myarg}{\myarg}$ to $\vee$ elimination; for $\myprod$
697 $\mypair{\myarg}{\myarg}$ corresponds to $\wedge$ introduction, $\myfst$
698 and $\mysnd$ to $\wedge$ elimination.
700 The trivial type $\myunit$ corresponds to the logical $\top$ (true), and
701 dually $\myempty$ corresponds to the logical $\bot$ (false). $\myunit$
702 has one introduction rule ($\mytt$), and thus one inhabitant; and no
703 eliminators. $\myempty$ has no introduction rules, and thus no
704 inhabitants; and one eliminator ($\myabsurd{ }$), corresponding to the
705 logical \emph{ex falso quodlibet}.
707 With these rules, our STLC now looks remarkably similar in power and use to the
708 natural deduction we already know.
709 \begin{mydef}[Negation]
710 $\myneg \mytya$ can be expressed as $\mytya \myarr \myempty$.
712 However, there is an important omission: there is no term of
713 the type $\mytya \mysum \myneg \mytya$ (excluded middle), or equivalently
714 $\myneg \myneg \mytya \myarr \mytya$ (double negation), or indeed any term with
715 a type equivalent to those.
717 This has a considerable effect on our logic and it is no coincidence, since there
718 is no obvious computational behaviour for laws like the excluded middle.
719 Logics of this kind are called \emph{intuitionistic}, or \emph{constructive},
720 and all the systems analysed will have this characteristic since they build on
721 the foundation of the STLC.\footnote{There is research to give computational
722 behaviour to classical logic, but I will not touch those subjects.}
724 As in logic, if we want to keep our system consistent, we must make sure that no
725 closed terms (in other words terms not under a $\lambda$) inhabit $\myempty$.
726 The variant of STLC presented here is indeed
727 consistent, a result that follows from the fact that it is
729 Going back to our $\mysyn{fix}$ combinator, it is easy to see how it ruins our
730 desire for consistency. The following term works for every type $\mytya$,
732 \[(\myfix{\myb{x}}{\mytya}{\myb{x}}) : \mytya\]
734 \subsection{Inductive data}
737 To make the STLC more useful as a programming language or reasoning tool it is
738 common to include (or let the user define) inductive data types. These comprise
739 of a type former, various constructors, and an eliminator (or destructor) that
740 serves as primitive recursor.
742 \begin{mydef}[Finite lists for the STLC]
743 We add a $\mylist$ type constructor, along with an `empty
744 list' ($\mynil{ }$) and `cons cell' ($\mycons$) constructor. The eliminator for
745 lists will be the usual folding operation ($\myfoldr$). Full rules in Figure
752 \begin{array}{r@{\ }c@{\ }l}
753 \mytmsyn & ::= & \cdots \mysynsep \mynil{\mytysyn} \mysynsep \mytmsyn \mycons \mytmsyn
755 \myapp{\myapp{\myapp{\myfoldr}{\mytmsyn}}{\mytmsyn}}{\mytmsyn} \\
756 \mytysyn & ::= & \cdots \mysynsep \myapp{\mylist}{\mytysyn}
760 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
762 \begin{array}{l@{\ }c@{\ }l}
763 \myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{\mynil{\mytya}} & \myred & \mytmt \\
765 \myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{(\mytmm \mycons \mytmn)} & \myred &
766 \myapp{\myapp{\myse{f}}{\mytmm}}{(\myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{\mytmn})}
770 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
772 \AxiomC{\phantom{$\myjud{\mytmm}{\mytya}$}}
773 \UnaryInfC{$\myjud{\mynil{\mytya}}{\myapp{\mylist}{\mytya}}$}
776 \AxiomC{$\myjud{\mytmm}{\mytya}$}
777 \AxiomC{$\myjud{\mytmn}{\myapp{\mylist}{\mytya}}$}
778 \BinaryInfC{$\myjud{\mytmm \mycons \mytmn}{\myapp{\mylist}{\mytya}}$}
783 \AxiomC{$\myjud{\mysynel{f}}{\mytya \myarr \mytyb \myarr \mytyb}$}
784 \AxiomC{$\myjud{\mytmm}{\mytyb}$}
785 \AxiomC{$\myjud{\mytmn}{\myapp{\mylist}{\mytya}}$}
786 \TrinaryInfC{$\myjud{\myapp{\myapp{\myapp{\myfoldr}{\mysynel{f}}}{\mytmm}}{\mytmn}}{\mytyb}$}
789 \caption{Rules for lists in the STLC.}
793 In Section \ref{sec:well-order} we will see how to give a general account of
796 \section{Intuitionistic Type Theory}
799 \subsection{Extending the STLC}
801 The STLC can be made more expressive in various ways. \cite{Barendregt1991}
802 succinctly expressed geometrically how we can add expressivity:
805 & \lambda\omega \ar@{-}[rr]\ar@{-}'[d][dd]
806 & & \lambda C \ar@{-}[dd]
808 \lambda2 \ar@{-}[ur]\ar@{-}[rr]\ar@{-}[dd]
809 & & \lambda P2 \ar@{-}[ur]\ar@{-}[dd]
811 & \lambda\underline\omega \ar@{-}'[r][rr]
812 & & \lambda P\underline\omega
814 \lambda{\to} \ar@{-}[rr]\ar@{-}[ur]
815 & & \lambda P \ar@{-}[ur]
818 Here $\lambda{\to}$, in the bottom left, is the STLC. From there can move along
821 \item[Terms depending on types (towards $\lambda{2}$)] We can quantify over
822 types in our type signatures. For example, we can define a polymorphic
823 identity function, where $\mytyp$ denotes the `type of types':
825 (\myabss{\myb{A}}{\mytyp}{\myabss{\myb{x}}{\myb{A}}{\myb{x}}}) : (\myb{A} {:} \mytyp) \myarr \myb{A} \myarr \myb{A}
827 The first and most famous instance of this idea has been System F.
828 This form of polymorphism and has been wildly successful, also thanks
829 to a well known inference algorithm for a restricted version of System
830 F known as Hindley-Milner \citep{milner1978theory}. Languages like
831 Haskell and SML are based on this discipline.
832 \item[Types depending on types (towards $\lambda{\underline{\omega}}$)] We have
833 type operators. For example we could define a function that given types $R$
834 and $\mytya$ forms the type that represents a value of type $\mytya$ in
835 continuation passing style:
836 \[\displaystyle(\myabss{\myb{A} \myar \myb{R}}{\mytyp}{(\myb{A}
837 \myarr \myb{R}) \myarr \myb{R}}) : \mytyp \myarr \mytyp \myarr \mytyp
839 \item[Types depending on terms (towards $\lambda{P}$)] Also known as `dependent
840 types', give great expressive power. For example, we can have values of whose
841 type depend on a boolean:
842 \[\displaystyle(\myabss{\myb{x}}{\mybool}{\myite{\myb{x}}{\mynat}{\myrat}}) : \mybool
846 All the systems preserve the properties that make the STLC well behaved. The
847 system we are going to focus on, Intuitionistic Type Theory, has all of the
848 above additions, and thus would sit where $\lambda{C}$ sits in the
849 `$\lambda$-cube'. It will serve as the logical `core' of all the other
850 extensions that we will present and ultimately our implementation of a similar
853 \subsection{A Bit of History}
855 Logic frameworks and programming languages based on type theory have a
856 long history. Per Martin-L\"{o}f described the first version of his
857 theory in 1971, but then revised it since the original version was
858 inconsistent due to its impredicativity.\footnote{In the early version
859 there was only one universe $\mytyp$ and $\mytyp : \mytyp$; see
860 Section \ref{sec:term-types} for an explanation on why this causes
861 problems.} For this reason he later gave a revised and consistent
862 definition \citep{Martin-Lof1984}.
864 A related development is the polymorphic $\lambda$-calculus, and specifically
865 the previously mentioned System F, which was developed independently by Girard
866 and Reynolds. An overview can be found in \citep{Reynolds1994}. The surprising
867 fact is that while System F is impredicative it is still consistent and strongly
868 normalising. \cite{Coquand1986} further extended this line of work with the
869 Calculus of Constructions (CoC).
871 Most widely used interactive theorem provers are based on ITT. Popular ones
872 include Agda \citep{Norell2007, Bove2009}, Coq \citep{Coq}, and Epigram
873 \citep{McBride2004, EpigramTut}.
875 \subsection{A simple type theory}
878 The calculus I present follows the exposition in \citep{Thompson1991},
879 and is quite close to the original formulation of predicative ITT as
880 found in \citep{Martin-Lof1984}.
881 \begin{mydef}[Intuitionistic Type Theory (ITT)]
882 The syntax and reduction rules are shown in Figure \ref{fig:core-tt-syn}.
883 The typing rules are presented piece by piece in the following sections.
885 Agda and \mykant\ renditions of the presented theory and all the
886 examples is reproduced in Appendix \ref{app:itt-code}.
891 \begin{array}{r@{\ }c@{\ }l}
892 \mytmsyn & ::= & \myb{x} \mysynsep
893 \mytyp_{level} \mysynsep
894 \myunit \mysynsep \mytt \mysynsep
895 \myempty \mysynsep \myapp{\myabsurd{\mytmsyn}}{\mytmsyn} \\
896 & | & \mybool \mysynsep \mytrue \mysynsep \myfalse \mysynsep
897 \myitee{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
898 & | & \myfora{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
899 \myabss{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
900 (\myapp{\mytmsyn}{\mytmsyn}) \\
901 & | & \myexi{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
902 \mypairr{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn} \\
903 & | & \myapp{\myfst}{\mytmsyn} \mysynsep \myapp{\mysnd}{\mytmsyn} \\
904 & | & \myw{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
905 \mytmsyn \mynode{\myb{x}}{\mytmsyn} \mytmsyn \\
906 & | & \myrec{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn} \\
907 level & \in & \mathbb{N}
912 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
915 \begin{array}{l@{ }l@{\ }c@{\ }l}
916 \myitee{\mytrue &}{\myb{x}}{\myse{P}}{\mytmm}{\mytmn} & \myred & \mytmm \\
917 \myitee{\myfalse &}{\myb{x}}{\myse{P}}{\mytmm}{\mytmn} & \myred & \mytmn \\
922 \myapp{(\myabss{\myb{x}}{\mytya}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{\myb{x}}{\mytmn}
926 \begin{array}{l@{ }l@{\ }c@{\ }l}
927 \myapp{\myfst &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmm \\
928 \myapp{\mysnd &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmn
936 \myrec{(\myse{s} \mynode{\myb{x}}{\myse{T}} \myse{f})}{\myb{y}}{\myse{P}}{\myse{p}} \myred
937 \myapp{\myapp{\myapp{\myse{p}}{\myse{s}}}{\myse{f}}}{(\myabss{\myb{t}}{\mysub{\myse{T}}{\myb{x}}{\myse{s}}}{
938 \myrec{\myapp{\myse{f}}{\myb{t}}}{\myb{y}}{\myse{P}}{\mytmt}
942 \caption{Syntax and reduction rules for our type theory.}
943 \label{fig:core-tt-syn}
946 \subsubsection{Types are terms, some terms are types}
947 \label{sec:term-types}
949 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
951 \AxiomC{$\myjud{\mytmt}{\mytya}$}
952 \AxiomC{$\mytya \mydefeq \mytyb$}
953 \BinaryInfC{$\myjud{\mytmt}{\mytyb}$}
956 \AxiomC{\phantom{$\myjud{\mytmt}{\mytya}$}}
957 \UnaryInfC{$\myjud{\mytyp_l}{\mytyp_{l + 1}}$}
962 The first thing to notice is that a barrier between values and types that we had
963 in the STLC is gone: values can appear in types, and the two are treated
964 uniformly in the syntax.
966 While the usefulness of doing this will become clear soon, a consequence is
967 that since types can be the result of computation, deciding type equality is
968 not immediate as in the STLC. For this reason we define \emph{definitional
969 equality}, $\mydefeq$, as the congruence relation extending
970 $\myred$---moreover, when comparing types syntactically we do it up to
971 renaming of bound names ($\alpha$-renaming). For example under this
972 discipline we will find that
974 \myabss{\myb{x}}{\mytya}{\myb{x}} \mydefeq \myabss{\myb{y}}{\mytya}{\myb{y}}
976 Types that are definitionally equal can be used interchangeably. Here
977 the `conversion' rule is not syntax directed, but it is possible to
978 employ $\myred$ to decide term equality in a systematic way, by
979 comparing terms by reducing to their normal forms and then comparing
980 them syntactically; so that a separate conversion rule is not needed.
981 Another thing to notice is that considering the need to reduce terms to
982 decide equality it is essential for a dependently typed system to be
983 terminating and confluent for type checking to be decidable, since every
984 type needs to have a \emph{unique} normal form.
986 Moreover, we specify a \emph{type hierarchy} to talk about `large'
987 types: $\mytyp_0$ will be the type of types inhabited by data:
988 $\mybool$, $\mynat$, $\mylist$, etc. $\mytyp_1$ will be the type of
989 $\mytyp_0$, and so on---for example we have $\mytrue : \mybool :
990 \mytyp_0 : \mytyp_1 : \cdots$. Each type `level' is often called a
991 universe in the literature. While it is possible to simplify things by
992 having only one universe $\mytyp$ with $\mytyp : \mytyp$, this plan is
993 inconsistent for much the same reason that impredicative na\"{\i}ve set
994 theory is \citep{Hurkens1995}. However various techniques can be
995 employed to lift the burden of explicitly handling universes, as we will
996 see in Section \ref{sec:term-hierarchy}.
998 \subsubsection{Contexts}
1000 \begin{minipage}{0.5\textwidth}
1001 \mydesc{context validity:}{\myvalid{\myctx}}{
1003 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
1004 \UnaryInfC{$\myvalid{\myemptyctx}$}
1007 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
1008 \UnaryInfC{$\myvalid{\myctx ; \myb{x} : \mytya}$}
1013 \begin{minipage}{0.5\textwidth}
1014 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1015 \AxiomC{$\myctx(x) = \mytya$}
1016 \UnaryInfC{$\myjud{\myb{x}}{\mytya}$}
1022 We need to refine the notion context to make sure that every variable appearing
1023 is typed correctly, or that in other words each type appearing in the context is
1024 indeed a type and not a value. In every other rule, if no premises are present,
1025 we assume the context in the conclusion to be valid.
1027 Then we can re-introduce the old rule to get the type of a variable for a
1030 \subsubsection{$\myunit$, $\myempty$}
1032 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1033 \begin{tabular}{ccc}
1034 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
1035 \UnaryInfC{$\myjud{\myunit}{\mytyp_0}$}
1037 \UnaryInfC{$\myjud{\myempty}{\mytyp_0}$}
1040 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
1041 \UnaryInfC{$\myjud{\mytt}{\myunit}$}
1043 \UnaryInfC{\phantom{$\myjud{\myempty}{\mytyp_0}$}}
1046 \AxiomC{$\myjud{\mytmt}{\myempty}$}
1047 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
1048 \BinaryInfC{$\myjud{\myapp{\myabsurd{\mytya}}{\mytmt}}{\mytya}$}
1050 \UnaryInfC{\phantom{$\myjud{\myempty}{\mytyp_0}$}}
1055 Nothing surprising here: $\myunit$ and $\myempty$ are unchanged from the STLC,
1056 with the added rules to type $\myunit$ and $\myempty$ themselves, and to make
1057 sure that we are invoking $\myabsurd{}$ over a type.
1059 \subsubsection{$\mybool$, and dependent $\myfun{if}$}
1061 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1062 \begin{tabular}{ccc}
1064 \UnaryInfC{$\myjud{\mybool}{\mytyp_0}$}
1068 \UnaryInfC{$\myjud{\mytrue}{\mybool}$}
1072 \UnaryInfC{$\myjud{\myfalse}{\mybool}$}
1077 \AxiomC{$\myjud{\mytmt}{\mybool}$}
1078 \AxiomC{$\myjudd{\myctx : \mybool}{\mytya}{\mytyp_l}$}
1080 \BinaryInfC{$\myjud{\mytmm}{\mysub{\mytya}{x}{\mytrue}}$ \hspace{0.7cm} $\myjud{\mytmn}{\mysub{\mytya}{x}{\myfalse}}$}
1081 \UnaryInfC{$\myjud{\myitee{\mytmt}{\myb{x}}{\mytya}{\mytmm}{\mytmn}}{\mysub{\mytya}{\myb{x}}{\mytmt}}$}
1085 With booleans we get the first taste of the `dependent' in `dependent
1086 types'. While the two introduction rules for $\mytrue$ and $\myfalse$
1087 are not surprising, the typing rules for $\myfun{if}$ are. In most
1088 strongly typed languages we expect the branches of an $\myfun{if}$
1089 statements to be of the same type, to preserve subject reduction, since
1090 execution could take both paths. This is a pity, since the type system
1091 does not reflect the fact that in each branch we gain knowledge on the
1092 term we are branching on. Which means that programs along the lines of
1094 if null xs then head xs else 0
1096 are a necessary, well typed, danger.
1098 However, in a more expressive system, we can do better: the branches' type can
1099 depend on the value of the scrutinised boolean. This is what the typing rule
1100 expresses: the user provides a type $\mytya$ ranging over an $\myb{x}$
1101 representing the scrutinised boolean type, and the branches are typechecked with
1102 the updated knowledge on the value of $\myb{x}$.
1104 \subsubsection{$\myarr$, or dependent function}
1107 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1108 \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
1109 \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
1110 \BinaryInfC{$\myjud{\myfora{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
1116 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytmt}{\mytyb}$}
1117 \UnaryInfC{$\myjud{\myabss{\myb{x}}{\mytya}{\mytmt}}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
1120 \AxiomC{$\myjud{\mytmm}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
1121 \AxiomC{$\myjud{\mytmn}{\mytya}$}
1122 \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mysub{\mytyb}{\myb{x}}{\mytmn}}$}
1127 Dependent functions are one of the two key features that perhaps most
1128 characterise dependent types---the other being dependent products. With
1129 dependent functions, the result type can depend on the value of the
1130 argument. This feature, together with the fact that the result type
1131 might be a type itself, brings a lot of interesting possibilities.
1132 Following this intuition, in the introduction rule, the return type is
1133 typechecked in a context with an abstracted variable of lhs' type, and
1134 in the elimination rule the actual argument is substituted in the return
1135 type. Keeping the correspondence with logic alive, dependent functions
1136 are much like universal quantifiers ($\forall$) in logic.
1138 For example, assuming that we have lists and natural numbers in our
1139 language, using dependent functions we are write functions of type:
1142 \myfun{length} : (\myb{A} {:} \mytyp_0) \myarr \myapp{\mylist}{\myb{A}} \myarr \mynat \\
1143 \myarg \myfun{$>$} \myarg : \mynat \myarr \mynat \myarr \mytyp_0 \\
1144 \myfun{head} : (\myb{A} {:} \mytyp_0) \myarr (\myb{l} {:} \myapp{\mylist}{\myb{A}})
1145 \myarr \myapp{\myapp{\myfun{length}}{\myb{A}}}{\myb{l}} \mathrel{\myfun{$>$}} 0 \myarr
1150 \myfun{length} is the usual polymorphic length
1151 function. $\myarg\myfun{$>$}\myarg$ is a function that takes two naturals
1152 and returns a type: if the lhs is greater then the rhs, $\myunit$ is
1153 returned, $\myempty$ otherwise. This way, we can express a
1154 `non-emptyness' condition in $\myfun{head}$, by including a proof that
1155 the length of the list argument is non-zero. This allows us to rule out
1156 the `empty list' case, so that we can safely return the first element.
1158 Again, we need to make sure that the type hierarchy is respected, which
1159 is the reason why a type formed by $\myarr$ will live in the least upper
1160 bound of the levels of argument and return type. If this was not the
1161 case, we would be able to form a `powerset' function along the lines of
1164 \myfun{P} : \mytyp_0 \myarr \mytyp_0 \\
1165 \myfun{P} \myappsp \myb{A} \mapsto \myb{A} \myarr \mytyp_0
1168 Where the type of $\myb{A} \myarr \mytyp_0$ is in $\mytyp_0$ itself.
1169 Using this and similar devices we would be able to derive falsity
1170 \citep{Hurkens1995}. This trend will continue with the other type-level
1171 binders, $\myprod$ and $\mytyc{W}$.
1173 \subsubsection{$\myprod$, or dependent product}
1176 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1177 \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
1178 \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
1179 \BinaryInfC{$\myjud{\myexi{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
1185 \AxiomC{$\myjud{\mytmm}{\mytya}$}
1186 \AxiomC{$\myjud{\mytmn}{\mysub{\mytyb}{\myb{x}}{\mytmm}}$}
1187 \BinaryInfC{$\myjud{\mypairr{\mytmm}{\myb{x}}{\mytyb}{\mytmn}}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
1189 \UnaryInfC{\phantom{$--$}}
1192 \AxiomC{$\myjud{\mytmt}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
1193 \UnaryInfC{$\hspace{0.7cm}\myjud{\myapp{\myfst}{\mytmt}}{\mytya}\hspace{0.7cm}$}
1195 \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mysub{\mytyb}{\myb{x}}{\myapp{\myfst}{\mytmt}}}$}
1200 If dependent functions are a generalisation of $\myarr$ in the STLC,
1201 dependent products are a generalisation of $\myprod$ in the STLC. The
1202 improvement is that the second element's type can depend on the value of
1203 the first element. The corrispondence with logic is through the
1204 existential quantifier: $\exists x \in \mathbb{N}. even(x)$ can be
1205 expressed as $\myexi{\myb{x}}{\mynat}{\myapp{\myfun{even}}{\myb{x}}}$.
1206 The first element will be a number, and the second evidence that the
1207 number is even. This highlights the fact that we are working in a
1208 constructive logic: if we have an existence proof, we can always ask for
1209 a witness. This means, for instance, that $\neg \forall \neg$ is not
1210 equivalent to $\exists$.
1212 Another perhaps more `dependent' application of products, paired with
1213 $\mybool$, is to offer choice between different types. For example we
1214 can easily recover disjunctions:
1217 \myarg\myfun{$\vee$}\myarg : \mytyp_0 \myarr \mytyp_0 \myarr \mytyp_0 \\
1218 \myb{A} \mathrel{\myfun{$\vee$}} \myb{B} \mapsto \myexi{\myb{x}}{\mybool}{\myite{\myb{x}}{\myb{A}}{\myb{B}}} \\ \ \\
1219 \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} \\
1220 \myfun{case} \myappsp \myb{A} \myappsp \myb{B} \myappsp \myb{C} \myappsp \myb{f} \myappsp \myb{g} \myappsp \myb{x} \mapsto \\
1221 \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}})}
1225 \subsubsection{$\mytyc{W}$, or well-order}
1226 \label{sec:well-order}
1228 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1230 \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
1231 \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
1232 \BinaryInfC{$\myjud{\myw{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
1237 \AxiomC{$\myjud{\mytmt}{\mytya}$}
1238 \AxiomC{$\myjud{\mysynel{f}}{\mysub{\mytyb}{\myb{x}}{\mytmt} \myarr \myw{\myb{x}}{\mytya}{\mytyb}}$}
1239 \BinaryInfC{$\myjud{\mytmt \mynode{\myb{x}}{\mytyb} \myse{f}}{\myw{\myb{x}}{\mytya}{\mytyb}}$}
1245 \AxiomC{$\myjud{\myse{u}}{\myw{\myb{x}}{\myse{S}}{\myse{T}}}$}
1246 \AxiomC{$\myjudd{\myctx; \myb{w} : \myw{\myb{x}}{\myse{S}}{\myse{T}}}{\myse{P}}{\mytyp_l}$}
1248 \BinaryInfC{$\myjud{\myse{p}}{
1249 \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}}}}
1251 \UnaryInfC{$\myjud{\myrec{\myse{u}}{\myb{w}}{\myse{P}}{\myse{p}}}{\mysub{\myse{P}}{\myb{w}}{\myse{u}}}$}
1255 Finally, the well-order type, or in short $\mytyc{W}$-type, which will
1256 let us represent inductive data in a general (but clumsy) way. We can
1257 form `nodes' of the shape $\mytmt \mynode{\myb{x}}{\mytyb} \myse{f} :
1258 \myw{\myb{x}}{\mytya}{\mytyb}$ that contain data ($\mytmt$) of type and
1259 one `child' for each member of $\mysub{\mytyb}{\myb{x}}{\mytmt}$. The
1260 $\myfun{rec}\ \myfun{with}$ acts as an induction principle on
1261 $\mytyc{W}$, given a predicate an a function dealing with the inductive
1262 case---we will gain more intuition about inductive data in ITT in
1263 Section \ref{sec:user-type}.
1265 For example, if we want to form natural numbers, we can take
1268 \mytyc{Tr} : \mybool \myarr \mytyp_0 \\
1269 \mytyc{Tr} \myappsp \myb{b} \mapsto \myfun{if}\, \myb{b}\, \myunit\, \myfun{else}\, \myempty \\
1271 \mynat : \mytyp_0 \\
1272 \mynat \mapsto \myw{\myb{b}}{\mybool}{(\mytyc{Tr}\myappsp\myb{b})}
1275 Each node will contain a boolean. If $\mytrue$, the number is non-zero,
1276 and we will have one child representing its predecessor, given that
1277 $\mytyc{Tr}$ will return $\myunit$. If $\myfalse$, the number is zero,
1278 and we will have no predecessors (children), given the $\myempty$:
1281 \mydc{zero} : \mynat \\
1282 \mydc{zero} \mapsto \myfalse \mynodee (\myabs{\myb{z}}{\myabsurd{\mynat} \myappsp \myb{x}}) \\
1284 \mydc{suc} : \mynat \myarr \mynat \\
1285 \mydc{suc}\myappsp \myb{x} \mapsto \mytrue \mynodee (\myabs{\myarg}{\myb{x}})
1288 And with a bit of effort, we can recover addition:
1291 \myfun{plus} : \mynat \myarr \mynat \myarr \mynat \\
1292 \myfun{plus} \myappsp \myb{x} \myappsp \myb{y} \mapsto \\
1293 \myind{2} \myfun{rec}\, \myb{x} / \myb{b}.\mynat \, \\
1294 \myind{2} \myfun{with}\, \myabs{\myb{b}}{\\
1295 \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) \\
1296 \myind{2}\myind{2}\myfun{then}\,(\myabs{\myarg\, \myb{f}}{\mydc{suc}\myappsp (\myapp{\myb{f}}{\mytt})})\, \myfun{else}\, (\myabs{\myarg\, \myarg}{\myb{y}})}
1299 Note how we explicitly have to type the branches to make them
1300 match with the definition of $\mynat$---which gives a taste of the
1301 `clumsiness' of $\mytyc{W}$-types, which while useful as a reasoning
1302 tool are useless to the user modelling data types.
1304 \section{The struggle for equality}
1305 \label{sec:equality}
1307 In the previous section we saw how a type checker (or a human) needs a
1308 notion of \emph{definitional equality}. Beyond this meta-theoretic
1309 notion, in this section we will explore the ways of expressing equality
1310 \emph{inside} the theory, as a reasoning tool available to the user.
1311 This area is the main concern of this thesis, and in general a very
1312 active research topic, since we do not have a fully satisfactory
1313 solution, yet. As in the previous section, everything presented is
1314 formalised in Agda in Appendix \ref{app:agda-itt}.
1316 \subsection{Propositional equality}
1318 \begin{mydef}[Propositional equality] The syntax, reduction, and typing
1319 rules for propositional equality and related constructs is defined as:
1323 \begin{minipage}{0.5\textwidth}
1326 \begin{array}{r@{\ }c@{\ }l}
1327 \mytmsyn & ::= & \cdots \\
1328 & | & \mypeq \myappsp \mytmsyn \myappsp \mytmsyn \myappsp \mytmsyn \mysynsep
1329 \myapp{\myrefl}{\mytmsyn} \\
1330 & | & \myjeq{\mytmsyn}{\mytmsyn}{\mytmsyn}
1335 \begin{minipage}{0.5\textwidth}
1336 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
1338 \myjeq{\myse{P}}{(\myapp{\myrefl}{\mytmm})}{\mytmn} \myred \mytmn
1344 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1345 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
1346 \AxiomC{$\myjud{\mytmm}{\mytya}$}
1347 \AxiomC{$\myjud{\mytmn}{\mytya}$}
1348 \TrinaryInfC{$\myjud{\mypeq \myappsp \mytya \myappsp \mytmm \myappsp \mytmn}{\mytyp_l}$}
1354 \AxiomC{$\begin{array}{c}\ \\\myjud{\mytmm}{\mytya}\hspace{1.1cm}\mytmm \mydefeq \mytmn\end{array}$}
1355 \UnaryInfC{$\myjud{\myapp{\myrefl}{\mytmm}}{\mypeq \myappsp \mytya \myappsp \mytmm \myappsp \mytmn}$}
1360 \myjud{\myse{P}}{\myfora{\myb{x}\ \myb{y}}{\mytya}{\myfora{q}{\mypeq \myappsp \mytya \myappsp \myb{x} \myappsp \myb{y}}{\mytyp_l}}} \\
1361 \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})}}
1364 \UnaryInfC{$\myjud{\myjeq{\myse{P}}{\myse{q}}{\myse{p}}}{\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmn}}{q}}$}
1369 To express equality between two terms inside ITT, the obvious way to do
1370 so is to have equality to be a type. Here we present what has survived
1371 as the dominating form of equality in systems based on ITT up to the
1374 Our type former is $\mypeq$, which given a type (in this case
1375 $\mytya$) relates equal terms of that type. $\mypeq$ has one introduction
1376 rule, $\myrefl$, which introduces an equality relation between definitionally
1379 Finally, we have one eliminator for $\mypeq$, $\myjeqq$. $\myjeq{\myse{P}}{\myse{q}}{\myse{p}}$ takes
1381 \item $\myse{P}$, a predicate working with two terms of a certain type (say
1382 $\mytya$) and a proof of their equality
1383 \item $\myse{q}$, a proof that two terms in $\mytya$ (say $\myse{m}$ and
1384 $\myse{n}$) are equal
1385 \item and $\myse{p}$, an inhabitant of $\myse{P}$ applied to $\myse{m}$
1386 twice, plus the trivial proof by reflexivity showing that $\myse{m}$
1389 Given these ingredients, $\myjeqq$ retuns a member of $\myse{P}$ applied
1390 to $\mytmm$, $\mytmn$, and $\myse{q}$. In other words $\myjeqq$ takes a
1391 witness that $\myse{P}$ works with \emph{definitionally equal} terms,
1392 and returns a witness of $\myse{P}$ working with \emph{propositionally
1393 equal} terms. Invokations of $\myjeqq$ will vanish when the equality
1394 proofs will reduce to invocations to reflexivity, at which point the
1395 arguments must be definitionally equal, and thus the provided
1396 $\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmm}}{(\myapp{\myrefl}{\mytmm})}$
1397 can be returned. This means that $\myjeqq$ will not compute with
1398 hypotetical proofs, which makes sense given that they might be false.
1400 While the $\myjeqq$ rule is slightly convoluted, ve can derive many more
1401 `friendly' rules from it, for example a more obvious `substitution' rule, that
1402 replaces equal for equal in predicates:
1405 \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}}}}} \\
1406 \myfun{subst}\myappsp \myb{A}\myappsp\myb{P}\myappsp\myb{x}\myappsp\myb{y}\myappsp\myb{q}\myappsp\myb{p} \mapsto
1407 \myjeq{(\myabs{\myb{x}\ \myb{y}\ \myb{q}}{\myapp{\myb{P}}{\myb{y}}})}{\myb{p}}{\myb{q}}
1410 Once we have $\myfun{subst}$, we can easily prove more familiar laws regarding
1411 equality, such as symmetry, transitivity, congruence laws, etc.
1413 \subsection{Common extensions}
1415 Our definitional and propositional equalities can be enhanced in various
1416 ways. Obviously if we extend the definitional equality we are also
1417 automatically extend propositional equality, given how $\myrefl$ works.
1419 \subsubsection{$\eta$-expansion}
1420 \label{sec:eta-expand}
1422 A simple extension to our definitional equality is $\eta$-expansion.
1423 Given an abstract variable $\myb{f} : \mytya \myarr \mytyb$ the aim is
1424 to have that $\myb{f} \mydefeq
1425 \myabss{\myb{x}}{\mytya}{\myapp{\myb{f}}{\myb{x}}}$. We can achieve
1426 this by `expanding' terms based on their types, a process also known as
1427 \emph{quotation}---a term borrowed from the practice of
1428 \emph{normalisation by evaluation}, where we embed terms in some host
1429 language with an existing notion of computation, and then reify them
1430 back into terms, which will `smooth out' differences like the one above
1433 The same concept applies to $\myprod$, where we expand each inhabitant
1434 by reconstructing it by getting its projections, so that $\myb{x}
1435 \mydefeq \mypair{\myfst \myappsp \myb{x}}{\mysnd \myappsp \myb{x}}$.
1436 Similarly, all one inhabitants of $\myunit$ and all zero inhabitants of
1437 $\myempty$ can be considered equal. Quotation can be performed in a
1438 type-directed way, as we will witness in Section \ref{sec:kant-irr}.
1440 \begin{mydef}[Congruence and $\eta$-laws]
1441 To justify quotation in our type system we will add a congruence law
1442 for abstractions and a similar law for products, plus the fact that all
1443 elements of $\myunit$ or $\myempty$ are equal.
1446 \mydesc{definitional equality:}{\myjud{\mytmm \mydefeq \mytmn}{\mytmsyn}}{
1448 \AxiomC{$\myjudd{\myctx; \myb{y} : \mytya}{\myapp{\myse{f}}{\myb{x}} \mydefeq \myapp{\myse{g}}{\myb{x}}}{\mysub{\mytyb}{\myb{x}}{\myb{y}}}$}
1449 \UnaryInfC{$\myjud{\myse{f} \mydefeq \myse{g}}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
1452 \AxiomC{$\myjud{\mypair{\myapp{\myfst}{\mytmm}}{\myapp{\mysnd}{\mytmm}} \mydefeq \mypair{\myapp{\myfst}{\mytmn}}{\myapp{\mysnd}{\mytmn}}}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
1453 \UnaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
1460 \AxiomC{$\myjud{\mytmm}{\myunit}$}
1461 \AxiomC{$\myjud{\mytmn}{\myunit}$}
1462 \BinaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\myunit}$}
1465 \AxiomC{$\myjud{\mytmm}{\myempty}$}
1466 \AxiomC{$\myjud{\mytmn}{\myempty}$}
1467 \BinaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\myempty}$}
1472 \subsubsection{Uniqueness of identity proofs}
1474 Another common but controversial addition to propositional equality is
1475 the $\myfun{K}$ axiom, which essentially states that all equality proofs
1478 \begin{mydef}[$\myfun{K}$ axiom]\end{mydef}
1479 \mydesc{typing:}{\myjud{\mytmm \mydefeq \mytmn}{\mytmsyn}}{
1482 \myjud{\myse{P}}{\myfora{\myb{x}}{\mytya}{\myb{x} \mypeq{\mytya} \myb{x} \myarr \mytyp}} \\\
1483 \myjud{\mytmt}{\mytya} \hspace{1cm}
1484 \myjud{\myse{p}}{\myse{P} \myappsp \mytmt \myappsp (\myrefl \myappsp \mytmt)} \hspace{1cm}
1485 \myjud{\myse{q}}{\mytmt \mypeq{\mytya} \mytmt}
1488 \UnaryInfC{$\myjud{\myfun{K} \myappsp \myse{P} \myappsp \myse{t} \myappsp \myse{p} \myappsp \myse{q}}{\myse{P} \myappsp \mytmt \myappsp \myse{q}}$}
1492 \cite{Hofmann1994} showed that $\myfun{K}$ is not derivable from the
1493 $\myjeqq$ axiom that we presented, and \cite{McBride2004} showed that it is
1494 needed to implement `dependent pattern matching', as first proposed by
1495 \cite{Coquand1992}. Thus, $\myfun{K}$ is derivable in the systems that
1496 implement dependent pattern matching, such as Epigram and Agda; but for
1499 $\myfun{K}$ is controversial mainly because it is at odds with
1500 equalities that include computational behaviour, most notably
1501 Voevodsky's `Univalent Foundations', which includes a \emph{univalence}
1502 axiom that identifies isomorphisms between types with propositional
1503 equality. For example we would have two isomorphisms, and thus two
1504 equalities, between $\mybool$ and $\mybool$, corresponding to the two
1505 permutations---one is the identity, and one swaps the elements. Given
1506 this, $\myfun{K}$ and univalence are inconsistent, and thus a form of
1507 dependent pattern matching that does not imply $\myfun{K}$ is subject of
1508 research.\footnote{More information about univalence can be found at
1509 \url{http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations.html}.}
1511 \subsection{Limitations}
1513 \epigraph{\emph{Half of my time spent doing research involves thinking up clever
1514 schemes to avoid needing functional extensionality.}}{@larrytheliquid}
1516 Propositional equality as described is quite restricted when
1517 reasoning about equality beyond the term structure, which is what definitional
1518 equality gives us (extension notwithstanding).
1520 The problem is best exemplified by \emph{function extensionality}. In
1521 mathematics, we would expect to be able to treat functions that give equal
1522 output for equal input as the same. When reasoning in a mechanised framework
1523 we ought to be able to do the same: in the end, without considering the
1524 operational behaviour, all functions equal extensionally are going to be
1525 replaceable with one another.
1527 However this is not the case, or in other words with the tools we have we have
1530 \myfun{ext} : \myfora{\myb{A}\ \myb{B}}{\mytyp}{\myfora{\myb{f}\ \myb{g}}{
1531 \myb{A} \myarr \myb{B}}{
1532 (\myfora{\myb{x}}{\myb{A}}{\myapp{\myb{f}}{\myb{x}} \mypeq{\myb{B}} \myapp{\myb{g}}{\myb{x}}}) \myarr
1533 \myb{f} \mypeq{\myb{A} \myarr \myb{B}} \myb{g}
1537 To see why this is the case, consider the functions
1538 \[\myabs{\myb{x}}{0 \mathrel{\myfun{$+$}} \myb{x}}$ and $\myabs{\myb{x}}{\myb{x} \mathrel{\myfun{$+$}} 0}\]
1539 where $\myfun{$+$}$ is defined by recursion on the first argument,
1540 gradually destructing it to build up successors of the second argument.
1541 The two functions are clearly extensionally equal, and we can in fact
1544 \myfora{\myb{x}}{\mynat}{(0 \mathrel{\myfun{$+$}} \myb{x}) \mypeq{\mynat} (\myb{x} \mathrel{\myfun{$+$}} 0)}
1546 By analysis on the $\myb{x}$. However, the two functions are not
1547 definitionally equal, and thus we won't be able to get rid of the
1550 For the reasons given above, theories that offer a propositional equality
1551 similar to what we presented are called \emph{intensional}, as opposed
1552 to \emph{extensional}. Most systems widely used today (such as Agda,
1553 Coq, and Epigram) are of this kind.
1555 This is quite an annoyance that often makes reasoning awkward to execute. It
1556 also extends to other fields, for example proving bisimulation between
1557 processes specified by coinduction, or in general proving equivalences based
1558 on the behaviour on a term.
1560 \subsection{Equality reflection}
1562 One way to `solve' this problem is by identifying propositional equality with
1563 definitional equality.
1565 \begin{mydef}[Equality reflection]\end{mydef}
1566 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1567 \AxiomC{$\myjud{\myse{q}}{\mytmm \mypeq{\mytya} \mytmn}$}
1568 \UnaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\mytya}$}
1572 The \emph{equality reflection} rule is a very different rule from the
1573 ones we saw up to now: it links a typing judgement internal to the type
1574 theory to a meta-theoretic judgement that the type checker uses to work
1575 with terms. It is easy to see the dangerous consequences that this
1578 \item The rule is not syntax directed, and the type checker is
1579 presumably expected to come up with equality proofs when needed.
1580 \item More worryingly, type checking becomes undecidable also because
1581 computing under false assumptions becomes unsafe, since we derive any
1582 equality proof and then use equality reflection and the conversion
1583 rule to have terms of any type.
1585 For example, assuming that we are in a context that contains
1587 \myb{A} : \mytyp; \myb{q} : \mypeq \myappsp \mytyp
1588 \myappsp (\mytya \myarr \mytya) \myappsp \mytya
1590 we can write a looping term similar to the one we saw in Section
1595 Given these facts theories employing equality reflection, like NuPRL
1596 \citep{NuPRL}, carry the derivations that gave rise to each typing judgement
1597 to keep the systems manageable.
1599 For all its faults, equality reflection does allow us to prove extensionality,
1600 using the extensions we gave above. Assuming that $\myctx$ contains
1601 \[\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}}}\]
1605 \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}$}
1606 \RightLabel{equality reflection}
1607 \UnaryInfC{$\myjudd{\myctx; \myb{x} : \myb{A}}{\myapp{\myb{f}}{\myb{x}} \mydefeq \myapp{\myb{g}}{\myb{x}}}{\myb{B}}$}
1608 \RightLabel{congruence for $\lambda$s}
1609 \UnaryInfC{$\myjud{(\myabs{\myb{x}}{\myapp{\myb{f}}{\myb{x}}}) \mydefeq (\myabs{\myb{x}}{\myapp{\myb{g}}{\myb{x}}})}{\myb{A} \myarr \myb{B}}$}
1610 \RightLabel{$\eta$-law for $\lambda$}
1611 \UnaryInfC{$\hspace{1.45cm}\myjud{\myb{f} \mydefeq \myb{g}}{\myb{A} \myarr \myb{B}}\hspace{1.45cm}$}
1612 \RightLabel{$\myrefl$}
1613 \UnaryInfC{$\myjud{\myapp{\myrefl}{\myb{f}}}{\myb{f} \mypeq{} \myb{g}}$}
1616 Now, the question is: do we need to give up well-behavedness of our theory to
1617 gain extensionality?
1619 \section{The observational approach}
1622 % TODO add \begin{mydef}s
1624 A recent development by \citet{Altenkirch2007}, \emph{Observational Type
1625 Theory} (OTT), promises to keep the well behavedness of ITT while
1626 being able to gain many useful equality proofs,\footnote{It is suspected
1627 that OTT gains \emph{all} the equality proofs of ETT, but no proof
1628 exists yet.} including function extensionality. The main idea is to
1629 give the user the possibility to \emph{coerce} (or transport) values
1630 from a type $\mytya$ to a type $\mytyb$, if the type checker can prove
1631 structurally that $\mytya$ and $\mytyb$ are equal; and providing a
1632 value-level equality based on similar principles. Here we give an
1633 exposition which follows closely the original paper.
1635 \subsection{A simpler theory, a propositional fragment}
1638 $\mytyp_l$ is replaced by $\mytyp$. \\\ \\
1640 \begin{array}{r@{\ }c@{\ }l}
1641 \mytmsyn & ::= & \cdots \mysynsep \myprdec{\myprsyn} \mysynsep
1642 \myITE{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
1643 \myprsyn & ::= & \mybot \mysynsep \mytop \mysynsep \myprsyn \myand \myprsyn
1644 \mysynsep \myprfora{\myb{x}}{\mytmsyn}{\myprsyn}
1651 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
1653 \begin{array}{l@{}l@{\ }c@{\ }l}
1654 \myITE{\mytrue &}{\mytya}{\mytyb} & \myred & \mytya \\
1655 \myITE{\myfalse &}{\mytya}{\mytyb} & \myred & \mytyb
1662 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1664 \AxiomC{$\myjud{\myse{P}}{\myprop}$}
1665 \UnaryInfC{$\myjud{\myprdec{\myse{P}}}{\mytyp}$}
1668 \AxiomC{$\myjud{\mytmt}{\mybool}$}
1669 \AxiomC{$\myjud{\mytya}{\mytyp}$}
1670 \AxiomC{$\myjud{\mytyb}{\mytyp}$}
1671 \TrinaryInfC{$\myjud{\myITE{\mytmt}{\mytya}{\mytyb}}{\mytyp}$}
1678 \mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
1679 \begin{tabular}{ccc}
1680 \AxiomC{\phantom{$\myjud{\myse{P}}{\myprop}$}}
1681 \UnaryInfC{$\myjud{\mytop}{\myprop}$}
1683 \UnaryInfC{$\myjud{\mybot}{\myprop}$}
1686 \AxiomC{$\myjud{\myse{P}}{\myprop}$}
1687 \AxiomC{$\myjud{\myse{Q}}{\myprop}$}
1688 \BinaryInfC{$\myjud{\myse{P} \myand \myse{Q}}{\myprop}$}
1690 \UnaryInfC{\phantom{$\myjud{\mybot}{\myprop}$}}
1693 \AxiomC{$\myjud{\myse{A}}{\mytyp}$}
1694 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\myse{P}}{\myprop}$}
1695 \BinaryInfC{$\myjud{\myprfora{\myb{x}}{\mytya}{\myse{P}}}{\myprop}$}
1697 \UnaryInfC{\phantom{$\myjud{\mybot}{\myprop}$}}
1702 Our foundation will be a type theory like the one of section
1703 \ref{sec:itt}, with only one level: $\mytyp_0$. In this context we will
1704 drop the $0$ and call $\mytyp_0$ $\mytyp$. Moreover, since the old
1705 $\myfun{if}\myarg\myfun{then}\myarg\myfun{else}$ was able to return
1706 types thanks to the hierarchy (which is gone), we need to reintroduce an
1707 ad-hoc conditional for types, where the reduction rule is the obvious
1710 However, we have an addition: a universe of \emph{propositions},
1711 $\myprop$. $\myprop$ isolates a fragment of types at large, and
1712 indeed we can `inject' any $\myprop$ back in $\mytyp$ with $\myprdec{\myarg}$: \\
1713 \mydesc{proposition decoding:}{\myprdec{\mytmsyn} \myred \mytmsyn}{
1716 \begin{array}{l@{\ }c@{\ }l}
1717 \myprdec{\mybot} & \myred & \myempty \\
1718 \myprdec{\mytop} & \myred & \myunit
1723 \begin{array}{r@{ }c@{ }l@{\ }c@{\ }l}
1724 \myprdec{&\myse{P} \myand \myse{Q} &} & \myred & \myprdec{\myse{P}} \myprod \myprdec{\myse{Q}} \\
1725 \myprdec{&\myprfora{\myb{x}}{\mytya}{\myse{P}} &} & \myred &
1726 \myfora{\myb{x}}{\mytya}{\myprdec{\myse{P}}}
1731 Propositions are what we call the types of \emph{proofs}, or types
1732 whose inhabitants contain no `data', much like $\myunit$. The goal of
1733 doing this is twofold: erasing all top-level propositions when
1734 compiling; and to identify all equivalent propositions as the same, as
1737 Why did we choose what we have in $\myprop$? Given the above
1738 criteria, $\mytop$ obviously fits the bill, since it us one element.
1739 A pair of propositions $\myse{P} \myand \myse{Q}$ still won't get us
1740 data, since if they both have one element the only possible pair is
1741 the one formed by said elements. Finally, if $\myse{P}$ is a
1742 proposition and we have $\myprfora{\myb{x}}{\mytya}{\myse{P}}$, the
1743 decoding will be a function which returns propositional content. The
1744 only threat is $\mybot$, by which we can fabricate anything we want:
1745 however if we are consistent there will be nothing of type $\mybot$ at
1746 the top level, which is what we care about regarding proof erasure.
1748 \subsection{Equality proofs}
1752 \begin{array}{r@{\ }c@{\ }l}
1753 \mytmsyn & ::= & \cdots \mysynsep
1754 \mycoee{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \mysynsep
1755 \mycohh{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
1756 \myprsyn & ::= & \cdots \mysynsep \mytmsyn \myeq \mytmsyn \mysynsep
1757 \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn}
1762 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1764 \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
1765 \AxiomC{$\myjud{\mytmt}{\mytya}$}
1766 \BinaryInfC{$\myjud{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}$}
1769 \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
1770 \AxiomC{$\myjud{\mytmt}{\mytya}$}
1771 \BinaryInfC{$\myjud{\mycohh{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\myprdec{\myjm{\mytmt}{\mytya}{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}}}$}
1777 \mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
1782 \myjud{\myse{A}}{\mytyp} \hspace{1cm} \myjud{\myse{B}}{\mytyp}
1785 \UnaryInfC{$\myjud{\mytya \myeq \mytyb}{\myprop}$}
1790 \myjud{\myse{A}}{\mytyp} \hspace{1cm} \myjud{\mytmm}{\myse{A}} \\
1791 \myjud{\myse{B}}{\mytyp} \hspace{1cm} \myjud{\mytmn}{\myse{B}}
1794 \UnaryInfC{$\myjud{\myjm{\mytmm}{\myse{A}}{\mytmn}{\myse{B}}}{\myprop}$}
1801 While isolating a propositional universe as presented can be a useful
1802 exercises on its own, what we are really after is a useful notion of
1803 equality. In OTT we want to maintain the notion that things judged to
1804 be equal are still always repleaceable for one another with no
1805 additional changes. Note that this is not the same as saying that they
1806 are definitionally equal, since as we saw extensionally equal functions,
1807 while satisfying the above requirement, are not definitionally equal.
1809 Towards this goal we introduce two equality constructs in
1810 $\myprop$---the fact that they are in $\myprop$ indicates that they
1811 indeed have no computational content. The first construct, $\myarg
1812 \myeq \myarg$, relates types, the second,
1813 $\myjm{\myarg}{\myarg}{\myarg}{\myarg}$, relates values. The
1814 value-level equality is different from our old propositional equality:
1815 instead of ranging over only one type, we might form equalities between
1816 values of different types---the usefulness of this construct will be
1817 clear soon. In the literature this equality is known as `heterogeneous'
1818 or `John Major', since
1821 John Major's `classless society' widened people's aspirations to
1822 equality, but also the gap between rich and poor. After all, aspiring
1823 to be equal to others than oneself is the politics of envy. In much
1824 the same way, forms equations between members of any type, but they
1825 cannot be treated as equals (ie substituted) unless they are of the
1826 same type. Just as before, each thing is only equal to
1827 itself. \citep{McBride1999}.
1830 Correspondingly, at the term level, $\myfun{coe}$ (`coerce') lets us
1831 transport values between equal types; and $\myfun{coh}$ (`coherence')
1832 guarantees that $\myfun{coe}$ respects the value-level equality, or in
1833 other words that it really has no computational component: if we
1834 transport $\mytmm : \mytya$ to $\mytmn : \mytyb$, $\mytmm$ and $\mytmn$
1835 will still be the same.
1837 Before introducing the core ideas that make OTT work, let us distinguish
1838 between \emph{canonical} and \emph{neutral} types. Canonical types are
1839 those arising from the ground types ($\myempty$, $\myunit$, $\mybool$)
1840 and the three type formers ($\myarr$, $\myprod$, $\mytyc{W}$). Neutral
1841 types are those formed by
1842 $\myfun{If}\myarg\myfun{Then}\myarg\myfun{Else}\myarg$.
1843 Correspondingly, canonical terms are those inhabiting canonical types
1844 ($\mytt$, $\mytrue$, $\myfalse$, $\myabss{\myb{x}}{\mytya}{\mytmt}$,
1845 ...), and neutral terms those formed by eliminators.\footnote{Using the
1846 terminology from Section \ref{sec:types}, we'd say that canonical
1847 terms are in \emph{weak head normal form}.} In the current system
1848 (and hopefully in well-behaved systems), all closed terms reduce to a
1849 canonical term, and all canonical types are inhabited by canonical
1852 \subsubsection{Type equality, and coercions}
1854 The plan is to decompose type-level equalities between canonical types
1855 into decodable propositions containing equalities regarding the
1856 subterms, and to use coerce recursively on the subterms using the
1857 generated equalities. This interplay between type equalities and
1858 \myfun{coe} ensures that invocations of $\myfun{coe}$ will vanish when
1859 we have evidence of the structural equality of the types we are
1860 transporting terms across. If the type is neutral, the equality won't
1861 reduce and thus $\myfun{coe}$ won't reduce either. If we come an
1862 equality between different canonical types, then we reduce the equality
1863 to bottom, making sure that no such proof can exist, and providing an
1864 `escape hatch' in $\myfun{coe}$.
1868 \mydesc{equality reduction:}{\myprsyn \myred \myprsyn}{
1870 \begin{array}{c@{\ }c@{\ }c@{\ }l}
1871 \myempty & \myeq & \myempty & \myred \mytop \\
1872 \myunit & \myeq & \myunit & \myred \mytop \\
1873 \mybool & \myeq & \mybool & \myred \mytop \\
1874 \myexi{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myexi{\myb{x_2}}{\mytya_2}{\mytya_2} & \myred \\
1876 \myind{2} \mytya_1 \myeq \mytyb_1 \myand
1877 \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}]}
1879 \myfora{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myfora{\myb{x_2}}{\mytya_2}{\mytyb_2} & \myred \cdots \\
1880 \myw{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myw{\myb{x_2}}{\mytya_2}{\mytyb_2} & \myred \cdots \\
1881 \mytya & \myeq & \mytyb & \myred \mybot\ \text{if $\mytya$ and $\mytyb$ are canonical.}
1886 \mydesc{reduction}{\mytmsyn \myred \mytmsyn}{
1888 \begin{array}[t]{@{}l@{\ }l@{\ }l@{\ }l@{\ }l@{\ }c@{\ }l@{\ }}
1889 \mycoe & \myempty & \myempty & \myse{Q} & \myse{t} & \myred & \myse{t} \\
1890 \mycoe & \myunit & \myunit & \myse{Q} & \myse{t} & \myred & \mytt \\
1891 \mycoe & \mybool & \mybool & \myse{Q} & \mytrue & \myred & \mytrue \\
1892 \mycoe & \mybool & \mybool & \myse{Q} & \myfalse & \myred & \myfalse \\
1893 \mycoe & (\myexi{\myb{x_1}}{\mytya_1}{\mytyb_1}) &
1894 (\myexi{\myb{x_2}}{\mytya_2}{\mytyb_2}) & \myse{Q} &
1895 \mytmt_1 & \myred & \\
1897 \myind{2}\begin{array}[t]{l@{\ }l@{\ }c@{\ }l}
1898 \mysyn{let} & \myb{\mytmm_1} & \mapsto & \myapp{\myfst}{\mytmt_1} : \mytya_1 \\
1899 & \myb{\mytmn_1} & \mapsto & \myapp{\mysnd}{\mytmt_1} : \mysub{\mytyb_1}{\myb{x_1}}{\myb{\mytmm_1}} \\
1900 & \myb{Q_A} & \mapsto & \myapp{\myfst}{\myse{Q}} : \mytya_1 \myeq \mytya_2 \\
1901 & \myb{\mytmm_2} & \mapsto & \mycoee{\mytya_1}{\mytya_2}{\myb{Q_A}}{\myb{\mytmm_1}} : \mytya_2 \\
1902 & \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}}} \\
1903 & \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}} \\
1904 \mysyn{in} & \multicolumn{3}{@{}l}{\mypair{\myb{\mytmm_2}}{\myb{\mytmn_2}}}
1907 \mycoe & (\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}) &
1908 (\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}) & \myse{Q} &
1912 \mycoe & (\myw{\myb{x_1}}{\mytya_1}{\mytyb_1}) &
1913 (\myw{\myb{x_2}}{\mytya_2}{\mytyb_2}) & \myse{Q} &
1917 \mycoe & \mytya & \mytyb & \myse{Q} & \mytmt & \myred & \myapp{\myabsurd{\mytyb}}{\myse{Q}}\ \text{if $\mytya$ and $\mytyb$ are canonical.}
1921 \caption{Reducing type equalities, and using them when
1922 $\myfun{coe}$rcing.}
1926 Figure \ref{fig:eqred} illustrates this idea in practice. For ground
1927 types, the proof is the trivial element, and \myfun{coe} is the
1928 identity. For $\myunit$, we can do better: we return its only member
1929 without matching on the term. For the three type binders, things are
1930 similar but subtly different---the choices we make in the type equality
1931 are dictated by the desire of writing the $\myfun{coe}$ in a natural
1934 $\myprod$ is the easiest case: we decompose the proof into proofs that
1935 the first element's types are equal ($\mytya_1 \myeq \mytya_2$), and a
1936 proof that given equal values in the first element, the types of the
1937 second elements are equal too
1938 ($\myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{\myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2}}
1939 \myimpl \mytyb_1 \myeq \mytyb_2}$).\footnote{We are using $\myimpl$ to
1940 indicate a $\forall$ where we discard the first value. We write
1941 $\mytyb_1[\myb{x_1}]$ to indicate that the $\myb{x_1}$ in $\mytyb_1$
1942 is re-bound to the $\myb{x_1}$ quantified by the $\forall$, and
1943 similarly for $\myb{x_2}$ and $\mytyb_2$.} This also explains the
1944 need for heterogeneous equality, since in the second proof it would be
1945 awkward to express the fact that $\myb{A_1}$ is the same as $\myb{A_2}$.
1946 In the respective $\myfun{coe}$ case, since the types are canonical, we
1947 know at this point that the proof of equality is a pair of the shape
1948 described above. Thus, we can immediately coerce the first element of
1949 the pair using the first element of the proof, and then instantiate the
1950 second element with the two first elements and a proof by coherence of
1951 their equality, since we know that the types are equal.
1953 The cases for the other binders are omitted for brevity, but they follow
1954 the same principle with some twists to make $\myfun{coe}$ work with the
1955 generated proofs; the reader can refer to the paper for details.
1957 \subsubsection{$\myfun{coe}$, laziness, and $\myfun{coh}$erence}
1959 It is important to notice that in the reduction rules for $\myfun{coe}$
1960 are never obstructed by the proofs: with the exception of comparisons
1961 between different canonical types we never `pattern match' on the proof
1962 pairs, but always look at the projections. This means that, as long as
1963 we are consistent, and thus as long as we don't have $\mybot$-inducing
1964 proofs, we can add propositional axioms for equality and $\myfun{coe}$
1965 will still compute. Thus, we can take $\myfun{coh}$ as axiomatic, and
1966 we can add back familiar useful equality rules:
1968 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1969 \AxiomC{$\myjud{\mytmt}{\mytya}$}
1970 \UnaryInfC{$\myjud{\myapp{\myrefl}{\mytmt}}{\myprdec{\myjm{\mytmt}{\mytya}{\mytmt}{\mytya}}}$}
1975 \AxiomC{$\myjud{\mytya}{\mytyp}$}
1976 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytyb}{\mytyp}$}
1977 \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}}}}}$}
1981 $\myrefl$ is the equivalent of the reflexivity rule in propositional
1982 equality, and $\mytyc{R}$ asserts that if we have a we have a $\mytyp$
1983 abstracting over a value we can substitute equal for equal---this lets
1984 us recover $\myfun{subst}$. Note that while we need to provide ad-hoc
1985 rules in the restricted, non-hierarchical theory that we have, if our
1986 theory supports abstraction over $\mytyp$s we can easily add these
1987 axioms as abstracted variables.
1989 \subsubsection{Value-level equality}
1991 \mydesc{equality reduction:}{\myprsyn \myred \myprsyn}{
1993 \begin{array}{r@{ }c@{\ }c@{\ }c@{}l@{\ }c@{\ }r@{}c@{\ }c@{\ }c@{}l@{\ }l}
1994 (&\mytmt_1 & : & \myempty&) & \myeq & (&\mytmt_2 & : & \myempty &) & \myred \mytop \\
1995 (&\mytmt_1 & : & \myunit&) & \myeq & (&\mytmt_2 & : & \myunit&) & \myred \mytop \\
1996 (&\mytrue & : & \mybool&) & \myeq & (&\mytrue & : & \mybool&) & \myred \mytop \\
1997 (&\myfalse & : & \mybool&) & \myeq & (&\myfalse & : & \mybool&) & \myred \mytop \\
1998 (&\mytrue & : & \mybool&) & \myeq & (&\myfalse & : & \mybool&) & \myred \mybot \\
1999 (&\myfalse & : & \mybool&) & \myeq & (&\mytrue & : & \mybool&) & \myred \mybot \\
2000 (&\mytmt_1 & : & \myexi{\mytya_1}{\myb{x_1}}{\mytyb_1}&) & \myeq & (&\mytmt_2 & : & \myexi{\mytya_2}{\myb{x_2}}{\mytyb_2}&) & \myred \\
2001 & \multicolumn{11}{@{}l}{
2002 \myind{2} \myjm{\myapp{\myfst}{\mytmt_1}}{\mytya_1}{\myapp{\myfst}{\mytmt_2}}{\mytya_2} \myand
2003 \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}}}
2005 (&\myse{f}_1 & : & \myfora{\mytya_1}{\myb{x_1}}{\mytyb_1}&) & \myeq & (&\myse{f}_2 & : & \myfora{\mytya_2}{\myb{x_2}}{\mytyb_2}&) & \myred \\
2006 & \multicolumn{11}{@{}l}{
2007 \myind{2} \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{
2008 \myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2} \myimpl
2009 \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}]}
2012 (&\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 \\
2013 (&\mytmt_1 & : & \mytya_1&) & \myeq & (&\mytmt_2 & : & \mytya_2 &) & \myred \mybot\ \text{if $\mytya_1$ and $\mytya_2$ are canonical.}
2018 As with type-level equality, we want value-level equality to reduce
2019 based on the structure of the compared terms. When matching
2020 propositional data, such as $\myempty$ and $\myunit$, we automatically
2021 return the trivial type, since if a type has zero one members, all
2022 members will be equal. When matching on data-bearing types, such as
2023 $\mybool$, we check that such data matches, and return bottom otherwise.
2025 \subsection{Proof irrelevance and stuck coercions}
2026 \label{sec:ott-quot}
2028 The last effort is required to make sure that proofs (members of
2029 $\myprop$) are \emph{irrelevant}. Since they are devoid of
2030 computational content, we would like to identify all equivalent
2031 propositions as the same, in a similar way as we identified all
2032 $\myempty$ and all $\myunit$ as the same in section
2033 \ref{sec:eta-expand}.
2035 Thus we will have a quotation that will not only perform
2036 $\eta$-expansion, but will also identify and mark proofs that could not
2037 be decoded (that is, equalities on neutral types). Then, when
2038 comparing terms, marked proofs will be considered equal without
2039 analysing their contents, thus gaining irrelevance.
2041 Moreover we can safely advance `stuck' $\myfun{coe}$rcions between
2042 non-canonical but definitionally equal types. Consider for example
2044 \mycoee{(\myITE{\myb{b}}{\mynat}{\mybool})}{(\myITE{\myb{b}}{\mynat}{\mybool})}{\myb{x}}
2046 Where $\myb{b}$ and $\myb{x}$ are abstracted variables. This
2047 $\myfun{coe}$ will not advance, since the types are not canonical.
2048 However they are definitionally equal, and thus we can safely remove the
2049 coerce and return $\myb{x}$ as it is.
2051 \section{\mykant : the theory}
2052 \label{sec:kant-theory}
2054 \mykant\ is an interactive theorem prover developed as part of this thesis.
2055 The plan is to present a core language which would be capable of serving as
2056 the basis for a more featureful system, while still presenting interesting
2057 features and more importantly observational equality.
2059 We will first present the features of the system, and then describe the
2060 implementation we have developed in Section \ref{sec:kant-practice}.
2062 The defining features of \mykant\ are:
2065 \item[Full dependent types] As we would expect, we have dependent a system
2066 which is as expressive as the `best' corner in the lambda cube described in
2067 Section \ref{sec:itt}.
2069 \item[Implicit, cumulative universe hierarchy] The user does not need to
2070 specify universe level explicitly, and universes are \emph{cumulative}.
2072 \item[User defined data types and records] Instead of forcing the user to
2073 choose from a restricted toolbox, we let her define inductive data types,
2074 with associated primitive recursion operators; or records, with associated
2075 projections for each field.
2077 \item[Bidirectional type checking] While no `fancy' inference via
2078 unification is present, we take advantage of a type synthesis system
2079 in the style of \cite{Pierce2000}, extending the concept for user
2082 \item[Observational equality] As described in Section \ref{sec:ott} but
2083 extended to work with the type hierarchy and to admit equality between
2084 arbitrary data types.
2086 \item[Type holes] When building up programs interactively, it is useful
2087 to leave parts unfinished while exploring the current context. This
2088 is what type holes are for. We do not describe holes rigorously, but
2089 provide more information about them from the implementation and usage
2090 perspective in Section \ref{sec:type-holes}.
2094 We will analyse the features one by one, along with motivations and
2095 tradeoffs for the design decisions made.
2097 \subsection{Bidirectional type checking}
2099 We start by describing bidirectional type checking since it calls for
2100 fairly different typing rules that what we have seen up to now. The
2101 idea is to have two kinds of terms: terms for which a type can always be
2102 inferred, and terms that need to be checked against a type. A nice
2103 observation is that this duality runs through the semantics of the
2104 terms: neutral terms (abstracted or defined variables, function
2105 application, record projections, primitive recursors, etc.) \emph{infer}
2106 types, canonical terms (abstractions, record/data types data
2107 constructors, etc.) need to be \emph{checked}.
2109 To introduce the concept and notation, we will revisit the STLC in a
2110 bidirectional style. The presentation follows \cite{Loh2010}. The
2111 syntax for our bidirectional STLC is the same as the untyped
2112 $\lambda$-calculus, but with an extra construct to annotate terms
2113 explicitly---this will be necessary when having top-level canonical
2114 terms. The types are the same as those found in the normal STLC.
2118 \begin{array}{r@{\ }c@{\ }l}
2119 \mytmsyn & ::= & \myb{x} \mysynsep \myabs{\myb{x}}{\mytmsyn} \mysynsep (\myapp{\mytmsyn}{\mytmsyn}) \mysynsep (\mytmsyn : \mytysyn)
2123 We will have two kinds of typing judgements: \emph{inference} and
2124 \emph{checking}. $\myinf{\mytmt}{\mytya}$ indicates that $\mytmt$
2125 infers the type $\mytya$, while $\mychk{\mytmt}{\mytya}$ can be checked
2126 against type $\mytya$. The type of variables in context is inferred,
2127 and so are annotate terms. The type of applications is inferred too,
2128 propagating types down the applied term. Abstractions are checked.
2129 Finally, we have a rule to check the type of an inferrable term.
2131 \mydesc{typing:}{\myctx \vdash \mytmsyn \Updownarrow \mytmsyn}{
2133 \AxiomC{$\myctx(x) = A$}
2134 \UnaryInfC{$\myinf{\myb{x}}{A}$}
2137 \AxiomC{$\myjudd{\myctx;\myb{x} : A}{\mytmt}{\mytyb}$}
2138 \UnaryInfC{$\mychk{\myabs{x}{\mytmt}}{(\myb{x} {:} \mytya) \myarr \mytyb}$}
2144 \begin{tabular}{ccc}
2145 \AxiomC{$\myinf{\mytmm}{\mytya \myarr \mytyb}$}
2146 \AxiomC{$\mychk{\mytmn}{\mytya}$}
2147 \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mytyb}$}
2150 \AxiomC{$\mychk{\mytmt}{\mytya}$}
2151 \UnaryInfC{$\myinf{\myann{\mytmt}{\mytya}}{\mytya}$}
2154 \AxiomC{$\myinf{\mytmt}{\mytya}$}
2155 \UnaryInfC{$\myinf{\mytmt}{\mytya}$}
2160 For example, if we wanted to type function composition (in this case for
2161 naturals), we would have to annotate the term:
2163 \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
2165 But we would not have to annotate functions passed to it, since the type would be propagated to the arguments:
2167 \myfun{comp}\myappsp (\myabs{\myb{x}}{\myb{x} \mathrel{\myfun{$+$}} 3}) \myappsp (\myabs{\myb{x}}{\myb{x} \mathrel{\myfun{$*$}} 4}) \myappsp 42
2170 \subsection{Base terms and types}
2172 Let us begin by describing the primitives available without the user
2173 defining any data types, and without equality. The way we handle
2174 variables and substitution is left unspecified, and explained in section
2175 \ref{sec:term-repr}, along with other implementation issues. We are
2176 also going to give an account of the implicit type hierarchy separately
2177 in Section \ref{sec:term-hierarchy}, so as not to clutter derivation
2178 rules too much, and just treat types as impredicative for the time
2183 \begin{array}{r@{\ }c@{\ }l}
2184 \mytmsyn & ::= & \mynamesyn \mysynsep \mytyp \\
2185 & | & \myfora{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
2186 \myabs{\myb{x}}{\mytmsyn} \mysynsep
2187 (\myapp{\mytmsyn}{\mytmsyn}) \mysynsep
2188 (\myann{\mytmsyn}{\mytmsyn}) \\
2189 \mynamesyn & ::= & \myb{x} \mysynsep \myfun{f}
2194 The syntax for our calculus includes just two basic constructs:
2195 abstractions and $\mytyp$s. Everything else will be provided by
2196 user-definable constructs. Since we let the user define values, we will
2197 need a context capable of carrying the body of variables along with
2200 Bound names and defined names are treated separately in the syntax, and
2201 while both can be associated to a type in the context, only defined
2202 names can be associated with a body:
2204 \mydesc{context validity:}{\myvalid{\myctx}}{
2205 \begin{tabular}{ccc}
2206 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
2207 \UnaryInfC{$\myvalid{\myemptyctx}$}
2210 \AxiomC{$\myjud{\mytya}{\mytyp}$}
2211 \AxiomC{$\mynamesyn \not\in \myctx$}
2212 \BinaryInfC{$\myvalid{\myctx ; \mynamesyn : \mytya}$}
2215 \AxiomC{$\myjud{\mytmt}{\mytya}$}
2216 \AxiomC{$\myfun{f} \not\in \myctx$}
2217 \BinaryInfC{$\myvalid{\myctx ; \myfun{f} \mapsto \mytmt : \mytya}$}
2222 Now we can present the reduction rules, which are unsurprising. We have
2223 the usual function application ($\beta$-reduction), but also a rule to
2224 replace names with their bodies ($\delta$-reduction), and one to discard
2225 type annotations. For this reason reduction is done in-context, as
2226 opposed to what we have seen in the past:
2228 \mydesc{reduction:}{\myctx \vdash \mytmsyn \myred \mytmsyn}{
2229 \begin{tabular}{ccc}
2230 \AxiomC{\phantom{$\myb{x} \mapsto \mytmt : \mytya \in \myctx$}}
2231 \UnaryInfC{$\myctx \vdash \myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn}
2232 \myred \mysub{\mytmm}{\myb{x}}{\mytmn}$}
2235 \AxiomC{$\myfun{f} \mapsto \mytmt : \mytya \in \myctx$}
2236 \UnaryInfC{$\myctx \vdash \myfun{f} \myred \mytmt$}
2239 \AxiomC{\phantom{$\myb{x} \mapsto \mytmt : \mytya \in \myctx$}}
2240 \UnaryInfC{$\myctx \vdash \myann{\mytmm}{\mytya} \myred \mytmm$}
2245 We can now give types to our terms. Although we include the usual
2246 conversion rule, we defer a detailed account of definitional equality to
2247 Section \ref{sec:kant-irr}.
2249 \mydesc{typing:}{\myctx \vdash \mytmsyn \Updownarrow \mytmsyn}{
2250 \begin{tabular}{cccc}
2251 \AxiomC{$\myse{name} : A \in \myctx$}
2252 \UnaryInfC{$\myinf{\myse{name}}{A}$}
2255 \AxiomC{$\myfun{f} \mapsto \mytmt : A \in \myctx$}
2256 \UnaryInfC{$\myinf{\myfun{f}}{A}$}
2259 \AxiomC{$\mychk{\mytmt}{\mytya}$}
2260 \UnaryInfC{$\myinf{\myann{\mytmt}{\mytya}}{\mytya}$}
2263 \AxiomC{$\myinf{\mytmt}{\mytya}$}
2264 \AxiomC{$\myctx \vdash \mytya \mydefeq \mytyb$}
2265 \BinaryInfC{$\mychk{\mytmt}{\mytyb}$}
2273 \AxiomC{\phantom{$\mychkk{\myctx; \myb{x}: \mytya}{\mytmt}{\mytyb}$}}
2274 \UnaryInfC{$\myinf{\mytyp}{\mytyp}$}
2277 \AxiomC{$\myinf{\mytya}{\mytyp}$}
2278 \AxiomC{$\myinff{\myctx; \myb{x} : \mytya}{\mytyb}{\mytyp}$}
2279 \BinaryInfC{$\myinf{(\myb{x} {:} \mytya) \myarr \mytyb}{\mytyp}$}
2288 \AxiomC{$\myinf{\mytmm}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
2289 \AxiomC{$\mychk{\mytmn}{\mytya}$}
2290 \BinaryInfC{$\myinf{\myapp{\mytmm}{\mytmn}}{\mysub{\mytyb}{\myb{x}}{\mytmn}}$}
2295 \AxiomC{$\mychkk{\myctx; \myb{x}: \mytya}{\mytmt}{\mytyb}$}
2296 \UnaryInfC{$\mychk{\myabs{\myb{x}}{\mytmt}}{\myfora{\myb{x}}{\mytyb}{\mytyb}}$}
2302 \subsection{Elaboration}
2304 As we mentioned, $\mykant$\ allows the user to define not only values
2305 but also custom data types and records. \emph{Elaboration} consists of
2306 turning these declarations into workable syntax, types, and reduction
2307 rules. The treatment of custom types in $\mykant$\ is heavily inspired
2308 by McBride's and McKinna's early work on Epigram \citep{McBride2004},
2309 although with some differences.
2311 \subsubsection{Term vectors, telescopes, and assorted notation}
2313 We use a vector notation to refer to a series of term applied to
2314 another, for example $\mytyc{D} \myappsp \vec{A}$ is a shorthand for
2315 $\mytyc{D} \myappsp \mytya_1 \cdots \mytya_n$, for some $n$. $n$ is
2316 consistently used to refer to the length of such vectors, and $i$ to
2317 refer to an index in such vectors. We also often need to `build up'
2318 terms vectors, in which case we use $\myemptyctx$ for an empty vector
2319 and add elements to an existing vector with $\myarg ; \myarg$, similarly
2320 to what we do for contexts.
2322 To present the elaboration and operations on user defined data types, we
2323 frequently make use what de Bruijn called \emph{telescopes}
2324 \citep{Bruijn91}, a construct that will prove useful when dealing with
2325 the types of type and data constructors. A telescope is a series of
2326 nested typed bindings, such as $(\myb{x} {:} \mynat); (\myb{p} {:}
2327 \myapp{\myfun{even}}{\myb{x}})$. Consistent with the notation for
2328 contexts and term vectors, we use $\myemptyctx$ to denote an empty
2329 telescope and $\myarg ; \myarg$ to add a new binding to an existing
2332 We refer to telescopes with $\mytele$, $\mytele'$, $\mytele_i$, etc. If
2333 $\mytele$ refers to a telescope, $\mytelee$ refers to the term vector
2334 made up of all the variables bound by $\mytele$. $\mytele \myarr
2335 \mytya$ refers to the type made by turning the telescope into a series
2336 of $\myarr$. Returning to the examples above, we have that
2338 (\myb{x} {:} \mynat); (\myb{p} : \myapp{\myfun{even}}{\myb{x}}) \myarr \mynat =
2339 (\myb{x} {:} \mynat) \myarr (\myb{p} : \myapp{\myfun{even}}{\myb{x}}) \myarr \mynat
2342 We make use of various operations to manipulate telescopes:
2344 \item $\myhead(\mytele)$ refers to the first type appearing in
2345 $\mytele$: $\myhead((\myb{x} {:} \mynat); (\myb{p} :
2346 \myapp{\myfun{even}}{\myb{x}})) = \mynat$. Similarly,
2347 $\myix_i(\mytele)$ refers to the $i^{th}$ type in a telescope
2349 \item $\mytake_i(\mytele)$ refers to the telescope created by taking the
2350 first $i$ elements of $\mytele$: $\mytake_1((\myb{x} {:} \mynat); (\myb{p} :
2351 \myapp{\myfun{even}}{\myb{x}})) = (\myb{x} {:} \mynat)$.
2352 \item $\mytele \vec{A}$ refers to the telescope made by `applying' the
2353 terms in $\vec{A}$ on $\mytele$: $((\myb{x} {:} \mynat); (\myb{p} :
2354 \myapp{\myfun{even}}{\myb{x}}))42 = (\myb{p} :
2355 \myapp{\myfun{even}}{42})$.
2358 Additionally, when presenting syntax elaboration, I'll use $\mytmsyn^n$
2359 to indicate a term vector composed of $n$ elements, or
2360 $\mytmsyn^{\mytele}$ for one composed by as many elements as the
2363 \subsubsection{Declarations syntax}
2367 \begin{array}{r@{\ }c@{\ }l}
2368 \mydeclsyn & ::= & \myval{\myb{x}}{\mytmsyn}{\mytmsyn} \\
2369 & | & \mypost{\myb{x}}{\mytmsyn} \\
2370 & | & \myadt{\mytyc{D}}{\myappsp \mytelesyn}{}{\mydc{c} : \mytelesyn\ |\ \cdots } \\
2371 & | & \myreco{\mytyc{D}}{\myappsp \mytelesyn}{}{\myfun{f} : \mytmsyn,\ \cdots } \\
2373 \mytelesyn & ::= & \myemptytele \mysynsep \mytelesyn \mycc (\myb{x} {:} \mytmsyn) \\
2374 \mynamesyn & ::= & \cdots \mysynsep \mytyc{D} \mysynsep \mytyc{D}.\mydc{c} \mysynsep \mytyc{D}.\myfun{f}
2379 In \mykant\ we have four kind of declarations:
2382 \item[Defined value] A variable, together with a type and a body.
2383 \item[Abstract variable] An abstract variable, with a type but no body.
2384 \item[Inductive data] A datatype, with a type constructor and various
2385 data constructors, quite similar to what we find in Haskell. A
2386 primitive recursor (or `destructor') will be generated automatically.
2387 \item[Record] A record, which consists of one data constructor and various
2388 fields, with no recursive occurrences.
2391 Elaborating defined variables consists of type checking the body against
2392 the given type, and updating the context to contain the new binding.
2393 Elaborating abstract variables and abstract variables consists of type
2394 checking the type, and updating the context with a new typed variable:
2396 \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
2398 \AxiomC{$\mychk{\mytmt}{\mytya}$}
2399 \AxiomC{$\myfun{f} \not\in \myctx$}
2401 $\myctx \myelabt \myval{\myfun{f}}{\mytya}{\mytmt} \ \ \myelabf\ \ \myctx; \myfun{f} \mapsto \mytmt : \mytya$
2405 \AxiomC{$\mychk{\mytya}{\mytyp}$}
2406 \AxiomC{$\myfun{f} \not\in \myctx$}
2409 \myctx \myelabt \mypost{\myfun{f}}{\mytya}
2410 \ \ \myelabf\ \ \myctx; \myfun{f} : \mytya
2417 \subsubsection{User defined types}
2418 \label{sec:user-type}
2420 Elaborating user defined types is the real effort. First, we will
2421 explain what we can define, with some examples.
2424 \item[Natural numbers] To define natural numbers, we create a data type
2425 with two constructors: one with zero arguments ($\mydc{zero}$) and one
2426 with one recursive argument ($\mydc{suc}$):
2429 \myadt{\mynat}{ }{ }{
2430 \mydc{zero} \mydcsep \mydc{suc} \myappsp \mynat
2434 This is very similar to what we would write in Haskell:
2436 data Nat = Zero | Suc Nat
2438 Once the data type is defined, $\mykant$\ will generate syntactic
2439 constructs for the type and data constructors, so that we will have
2442 \begin{tabular}{ccc}
2443 \AxiomC{\phantom{$\mychk{\mytmt}{\mynat}$}}
2444 \UnaryInfC{$\myinf{\mynat}{\mytyp}$}
2447 \AxiomC{\phantom{$\mychk{\mytmt}{\mynat}$}}
2448 \UnaryInfC{$\myinf{\mytyc{\mynat}.\mydc{zero}}{\mynat}$}
2451 \AxiomC{$\mychk{\mytmt}{\mynat}$}
2452 \UnaryInfC{$\myinf{\mytyc{\mynat}.\mydc{suc} \myappsp \mytmt}{\mynat}$}
2456 While in Haskell (or indeed in Agda or Coq) data constructors are
2457 treated the same way as functions, in $\mykant$\ they are syntax, so
2458 for example using $\mytyc{\mynat}.\mydc{suc}$ on its own will give a
2459 syntax error. This is necessary so that we can easily infer the type
2460 of polymorphic data constructors, as we will see later.
2462 Moreover, each data constructor is prefixed by the type constructor
2463 name, since we need to retrieve the type constructor of a data
2464 constructor when type checking. This measure aids in the presentation
2465 of various features but it is not needed in the implementation, where
2466 we can have a dictionary to lookup the type constructor corresponding
2467 to each data constructor. When using data constructors in examples I
2468 will omit the type constructor prefix for brevity, in this case
2469 writing $\mydc{zero}$ instead of $\mynat.\mydc{suc}$ and $\mydc{suc}$ instead of
2470 $\mynat.\mydc{suc}$.
2472 Along with user defined constructors, $\mykant$\ automatically
2473 generates an \emph{eliminator}, or \emph{destructor}, to compute with
2474 natural numbers: If we have $\mytmt : \mynat$, we can destruct
2475 $\mytmt$ using the generated eliminator `$\mynat.\myfun{elim}$':
2478 \AxiomC{$\mychk{\mytmt}{\mynat}$}
2480 \myinf{\mytyc{\mynat}.\myfun{elim} \myappsp \mytmt}{
2482 \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}}
2486 $\mynat.\myfun{elim}$ corresponds to the induction principle for
2487 natural numbers: if we have a predicate on numbers ($\myb{P}$), and we
2488 know that predicate holds for the base case
2489 ($\myapp{\myb{P}}{\mydc{zero}}$) and for each inductive step
2490 ($\myfora{\myb{x}}{\mynat}{\myapp{\myb{P}}{\myb{x}} \myarr
2491 \myapp{\myb{P}}{(\myapp{\mydc{suc}}{\myb{x}})}}$), then $\myb{P}$
2492 holds for any number. As with the data constructors, we require the
2493 eliminator to be applied to the `destructed' element.
2495 While the induction principle is usually seen as a mean to prove
2496 properties about numbers, in the intuitionistic setting it is also a
2497 mean to compute. In this specific case $\mynat.\myfun{elim}$
2498 returns the base case if the provided number is $\mydc{zero}$, and
2499 recursively applies the inductive step if the number is a
2502 \begin{array}{@{}l@{}l}
2503 \mytyc{\mynat}.\myfun{elim} \myappsp \mydc{zero} & \myappsp \myse{P} \myappsp \myse{pz} \myappsp \myse{ps} \myred \myse{pz} \\
2504 \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})
2507 The Haskell equivalent would be
2509 elim :: Nat -> a -> (Nat -> a -> a) -> a
2510 elim Zero pz ps = pz
2511 elim (Suc n) pz ps = ps n (elim n pz ps)
2513 Which buys us the computational behaviour, but not the reasoning power,
2514 since we cannot express the notion of a predicate depending on $\mynat$,
2515 since the type system is far too weak.
2517 \item[Binary trees] Now for a polymorphic data type: binary trees, since
2518 lists are too similar to natural numbers to be interesting.
2521 \myadt{\mytree}{\myappsp (\myb{A} {:} \mytyp)}{ }{
2522 \mydc{leaf} \mydcsep \mydc{node} \myappsp (\myapp{\mytree}{\myb{A}}) \myappsp \myb{A} \myappsp (\myapp{\mytree}{\myb{A}})
2526 Now the purpose of constructors as syntax can be explained: what would
2527 the type of $\mydc{leaf}$ be? If we were to treat it as a `normal'
2528 term, we would have to specify the type parameter of the tree each
2529 time the constructor is applied:
2531 \begin{array}{@{}l@{\ }l}
2532 \mydc{leaf} & : \myfora{\myb{A}}{\mytyp}{\myapp{\mytree}{\myb{A}}} \\
2533 \mydc{node} & : \myfora{\myb{A}}{\mytyp}{\myapp{\mytree}{\myb{A}} \myarr \myb{A} \myarr \myapp{\mytree}{\myb{A}} \myarr \myapp{\mytree}{\myb{A}}}
2536 The problem with this approach is that creating terms is incredibly
2537 verbose and dull, since we would need to specify the type parameters
2538 each time. For example if we wished to create a $\mytree \myappsp
2539 \mynat$ with two nodes and three leaves, we would have to write
2541 \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)
2543 The redundancy of $\mynat$s is quite irritating. Instead, if we treat
2544 constructors as syntactic elements, we can `extract' the type of the
2545 parameter from the type that the term gets checked against, much like
2546 we get the type of abstraction arguments:
2550 \AxiomC{$\mychk{\mytya}{\mytyp}$}
2551 \UnaryInfC{$\mychk{\mydc{leaf}}{\myapp{\mytree}{\mytya}}$}
2554 \AxiomC{$\mychk{\mytmm}{\mytree \myappsp \mytya}$}
2555 \AxiomC{$\mychk{\mytmt}{\mytya}$}
2556 \AxiomC{$\mychk{\mytmm}{\mytree \myappsp \mytya}$}
2557 \TrinaryInfC{$\mychk{\mydc{node} \myappsp \mytmm \myappsp \mytmt \myappsp \mytmn}{\mytree \myappsp \mytya}$}
2561 Which enables us to write, much more concisely
2563 \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}
2565 We gain an annotation, but we lose the myriad of types applied to the
2566 constructors. Conversely, with the eliminator for $\mytree$, we can
2567 infer the type of the arguments given the type of the destructed:
2570 \AxiomC{$\myinf{\mytmt}{\myapp{\mytree}{\mytya}}$}
2572 \myinf{\mytree.\myfun{elim} \myappsp \mytmt}{
2574 (\myb{P} {:} \myapp{\mytree}{\mytya} \myarr \mytyp) \myarr \\
2575 \myapp{\myb{P}}{\mydc{leaf}} \myarr \\
2576 ((\myb{l} {:} \myapp{\mytree}{\mytya}) (\myb{x} {:} \mytya) (\myb{r} {:} \myapp{\mytree}{\mytya}) \myarr \myapp{\myb{P}}{\myb{l}} \myarr
2577 \myapp{\myb{P}}{\myb{r}} \myarr \myb{P} \myappsp (\mydc{node} \myappsp \myb{l} \myappsp \myb{x} \myappsp \myb{r})) \myarr \\
2578 \myapp{\myb{P}}{\mytmt}
2583 As expected, the eliminator embodies structural induction on trees.
2584 We have a base case for $\myb{P} \myappsp \mydc{leaf}$, and an
2585 inductive step that given two subtrees and the predicate applied to
2586 them we need to return the predicate applied to the tree formed by a
2587 node with the two subtrees as children.
2589 \item[Empty type] We have presented types that have at least one
2590 constructors, but nothing prevents us from defining types with
2591 \emph{no} constructors:
2592 \[\myadt{\mytyc{Empty}}{ }{ }{ }\]
2593 What shall the `induction principle' on $\mytyc{Empty}$ be? Does it
2594 even make sense to talk about induction on $\mytyc{Empty}$?
2595 $\mykant$\ does not care, and generates an eliminator with no `cases',
2596 and thus corresponding to the $\myfun{absurd}$ that we know and love:
2599 \AxiomC{$\myinf{\mytmt}{\mytyc{Empty}}$}
2600 \UnaryInfC{$\myinf{\myempty.\myfun{elim} \myappsp \mytmt}{(\myb{P} {:} \mytmt \myarr \mytyp) \myarr \myapp{\myb{P}}{\mytmt}}$}
2603 \item[Ordered lists] Up to this point, the examples shown are nothing
2604 new to the \{Haskell, SML, OCaml, functional\} programmer. However
2605 dependent types let us express much more than that. A useful example
2606 is the type of ordered lists. There are many ways to define such a
2607 thing, we will define our type to store the bounds of the list, making
2608 sure that $\mydc{cons}$ing respects that.
2610 First, using $\myunit$ and $\myempty$, we define a type expressing the
2611 ordering on natural numbers, $\myfun{le}$---`less or equal'.
2612 $\myfun{le}\myappsp \mytmm \myappsp \mytmn$ will be inhabited only if
2613 $\mytmm \le \mytmn$:
2616 \myfun{le} : \mynat \myarr \mynat \myarr \mytyp \\
2617 \myfun{le} \myappsp \myb{n} \mapsto \\
2618 \myind{2} \mynat.\myfun{elim} \\
2619 \myind{2}\myind{2} \myb{n} \\
2620 \myind{2}\myind{2} (\myabs{\myarg}{\mynat \myarr \mytyp}) \\
2621 \myind{2}\myind{2} (\myabs{\myarg}{\myunit}) \\
2622 \myind{2}\myind{2} (\myabs{\myb{n}\, \myb{f}\, \myb{m}}{
2623 \mynat.\myfun{elim} \myappsp \myb{m} \myappsp (\myabs{\myarg}{\mytyp}) \myappsp \myempty \myappsp (\myabs{\myb{m'}\, \myarg}{\myapp{\myb{f}}{\myb{m'}}})
2627 We return $\myunit$ if the scrutinised is $\mydc{zero}$ (every
2628 number in less or equal than zero), $\myempty$ if the first number is
2629 a $\mydc{suc}$cessor and the second a $\mydc{zero}$, and we recurse if
2630 they are both successors. Since we want the list to have possibly
2631 `open' bounds, for example for empty lists, we create a type for
2632 `lifted' naturals with a bottom (less than everything) and top
2633 (greater than everything) elements, along with an associated comparison
2637 \myadt{\mytyc{Lift}}{ }{ }{\mydc{bot} \mydcsep \mydc{lift} \myappsp \mynat \mydcsep \mydc{top}}\\
2638 \myfun{le'} : \mytyc{Lift} \myarr \mytyc{Lift} \myarr \mytyp\\
2639 \myfun{le'} \myappsp \myb{l_1} \mapsto \\
2640 \myind{2} \mytyc{Lift}.\myfun{elim} \\
2641 \myind{2}\myind{2} \myb{l_1} \\
2642 \myind{2}\myind{2} (\myabs{\myarg}{\mytyc{Lift} \myarr \mytyp}) \\
2643 \myind{2}\myind{2} (\myabs{\myarg}{\myunit}) \\
2644 \myind{2}\myind{2} (\myabs{\myb{n_1}\, \myb{n_2}}{
2645 \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
2647 \myind{2}\myind{2} (\myabs{\myb{n_1}\, \myb{n_2}}{
2648 \mytyc{Lift}.\myfun{elim} \myappsp \myb{l_2} \myappsp (\myabs{\myarg}{\mytyp}) \myappsp \myempty \myappsp (\myabs{\myarg}{\myempty}) \myappsp \myunit
2652 Finally, we can defined a type of ordered lists. The type is
2653 parametrised over two values representing the lower and upper bounds
2654 of the elements, as opposed to the type parameters that we are used
2655 to. Then, an empty list will have to have evidence that the bounds
2656 are ordered, and each time we add an element we require the list to
2657 have a matching lower bound:
2660 \myadt{\mytyc{OList}}{\myappsp (\myb{low}\ \myb{upp} {:} \mytyc{Lift})}{\\ \myind{2}}{
2661 \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})
2665 Note that in the $\mydc{cons}$ constructor we quantify over the first
2666 argument, which will determine the type of the following
2667 arguments---again something we cannot do in systems like Haskell. If
2668 we want we can then employ this structure to write and prove correct
2669 various sorting algorithms.\footnote{See this presentation by Conor
2671 \url{https://personal.cis.strath.ac.uk/conor.mcbride/Pivotal.pdf},
2672 and this blog post by the author:
2673 \url{http://mazzo.li/posts/AgdaSort.html}.}
2675 \item[Dependent products] Apart from $\mysyn{data}$, $\mykant$\ offers
2676 us another way to define types: $\mysyn{record}$. A record is a
2677 datatype with one constructor and `projections' to extract specific
2678 fields of the said constructor.
2680 For example, we can recover dependent products:
2683 \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}}}
2686 Here $\myfst$ and $\mysnd$ are the projections, with their respective
2687 types. Note that each field can refer to the preceding fields. A
2688 constructor will be automatically generated, under the name of
2689 $\mytyc{Prod}.\mydc{constr}$. Dually to data types, we will omit the
2690 type constructor prefix for record projections.
2692 Following the bidirectionality of the system, we have that projections
2693 (the destructors of the record) infer the type, while the constructor
2698 \AxiomC{$\mychk{\mytmm}{\mytya}$}
2699 \AxiomC{$\mychk{\mytmn}{\myapp{\mytyb}{\mytmm}}$}
2700 \BinaryInfC{$\mychk{\mytyc{Prod}.\mydc{constr} \myappsp \mytmm \myappsp \mytmn}{\mytyc{Prod} \myappsp \mytya \myappsp \mytyb}$}
2702 \UnaryInfC{\phantom{$\myinf{\myfun{snd} \myappsp \mytmt}{\mytyb \myappsp (\myfst \myappsp \mytmt)}$}}
2705 \AxiomC{$\myinf{\mytmt}{\mytyc{Prod} \myappsp \mytya \myappsp \mytyb}$}
2706 \UnaryInfC{$\myinf{\myfun{fst} \myappsp \mytmt}{\mytya}$}
2708 \UnaryInfC{$\myinf{\myfun{snd} \myappsp \mytmt}{\mytyb \myappsp (\myfst \myappsp \mytmt)}$}
2712 What we have is equivalent to ITT's dependent products.
2720 \mynamesyn ::= \cdots \mysynsep \mytyc{D} \mysynsep \mytyc{D}.\mydc{c} \mysynsep \mytyc{D}.\myfun{f}
2727 \mydesc{syntax elaboration:}{\mydeclsyn \myelabf \mytmsyn ::= \cdots}{
2730 \begin{array}{r@{\ }l}
2731 & \myadt{\mytyc{D}}{\mytele}{}{\cdots\ |\ \mydc{c}_n : \mytele_n } \\
2734 \begin{array}{r@{\ }c@{\ }l}
2735 \mytmsyn & ::= & \cdots \mysynsep \myapp{\mytyc{D}}{\mytmsyn^{\mytele}} \mysynsep \cdots \mysynsep
2736 \mytyc{D}.\mydc{c}_n \myappsp \mytmsyn^{\mytele_n} \mysynsep \mytyc{D}.\myfun{elim} \myappsp \mytmsyn \\
2744 \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
2749 \myinf{\mytele \myarr \mytyp}{\mytyp}\hspace{0.8cm}
2750 \mytyc{D} \not\in \myctx \\
2751 \myinff{\myctx;\ \mytyc{D} : \mytele \myarr \mytyp}{\mytele \mycc \mytele_i \myarr \myapp{\mytyc{D}}{\mytelee}}{\mytyp}\ \ \ (1 \leq i \leq n) \\
2752 \text{For each $(\myb{x} {:} \mytya)$ in each $\mytele_i$, if $\mytyc{D} \in \mytya$, then $\mytya = \myapp{\mytyc{D}}{\vec{\mytmt}}$.}
2756 \begin{array}{r@{\ }c@{\ }l}
2757 \myctx & \myelabt & \myadt{\mytyc{D}}{\mytele}{}{ \cdots \ |\ \mydc{c}_n : \mytele_n } \\
2758 & & \vspace{-0.2cm} \\
2759 & \myelabf & \myctx;\ \mytyc{D} : \mytele \myarr \mytyp;\ \cdots;\ \mytyc{D}.\mydc{c}_n : \mytele \mycc \mytele_n \myarr \myapp{\mytyc{D}}{\mytelee}; \\
2761 \begin{array}{@{}r@{\ }l l}
2762 \mytyc{D}.\myfun{elim} : & \mytele \myarr (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr & \textbf{target} \\
2763 & (\myb{P} {:} \myapp{\mytyc{D}}{\mytelee} \myarr \mytyp) \myarr & \textbf{motive} \\
2767 (\mytele_n \mycc \myhyps(\myb{P}, \mytele_n) \myarr \myapp{\myb{P}}{(\myapp{\mytyc{D}.\mydc{c}_n}{\mytelee_n})}) \myarr
2768 \end{array} \right \}
2769 & \textbf{methods} \\
2770 & \myapp{\myb{P}}{\myb{x}} &
2774 \DisplayProof \\ \vspace{0.2cm}\ \\
2776 \begin{array}{@{}l l@{\ } l@{} r c l}
2777 \textbf{where} & \myhyps(\myb{P}, & \myemptytele &) & \mymetagoes & \myemptytele \\
2778 & \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) \\
2779 & \myhyps(\myb{P}, & (\myb{x} {:} \mytya) \mycc \mytele & ) & \mymetagoes & \myhyps(\myb{P}, \mytele)
2787 \mydesc{reduction elaboration:}{\mydeclsyn \myelabf \myctx \vdash \mytmsyn \myred \mytmsyn}{
2789 $\myadt{\mytyc{D}}{\mytele}{}{ \cdots \ |\ \mydc{c}_n : \mytele_n } \ \ \myelabf$
2790 \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
2791 \AxiomC{$\mytyc{D}.\mydc{c}_i : \mytele;\mytele_i \myarr \myapp{\mytyc{D}}{\mytelee} \in \myctx$}
2793 \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)}
2795 \DisplayProof \\ \vspace{0.2cm}\ \\
2797 \begin{array}{@{}l l@{\ } l@{} r c l}
2798 \textbf{where} & \myrecs(\myse{P}, \vec{m}, & \myemptytele &) & \mymetagoes & \myemptytele \\
2799 & \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) \\
2800 & \myrecs(\myse{P}, \vec{m}, & (\myb{x} {:} \mytya); \mytele &) & \mymetagoes & \myrecs(\myse{P}, \vec{m}, \mytele)
2807 \mydesc{syntax elaboration:}{\myelab{\mydeclsyn}{\mytmsyn ::= \cdots}}{
2810 \begin{array}{r@{\ }c@{\ }l}
2811 \myctx & \myelabt & \myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \\
2814 \begin{array}{r@{\ }c@{\ }l}
2815 \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 \\
2823 \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
2827 \myinf{\mytele \myarr \mytyp}{\mytyp}\hspace{0.8cm}
2828 \mytyc{D} \not\in \myctx \\
2829 \myinff{\myctx; \mytele; (\myb{f}_j : \myse{F}_j)_{j=1}^{i - 1}}{F_i}{\mytyp} \myind{3} (1 \le i \le n)
2833 \begin{array}{r@{\ }c@{\ }l}
2834 \myctx & \myelabt & \myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \\
2835 & & \vspace{-0.2cm} \\
2836 & \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}; \\
2837 & & \mytyc{D}.\mydc{constr} : \mytele \myarr \myse{F}_1 \myarr \cdots \myarr \myse{F}_n \myarr \myapp{\mytyc{D}}{\mytelee};
2845 \mydesc{reduction elaboration:}{\mydeclsyn \myelabf \myctx \vdash \mytmsyn \myred \mytmsyn}{
2847 $\myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \ \ \myelabf$
2848 \AxiomC{$\mytyc{D} \in \myctx$}
2849 \UnaryInfC{$\myctx \vdash \myapp{\mytyc{D}.\myfun{f}_i}{(\mytyc{D}.\mydc{constr} \myappsp \vec{t})} \myred t_i$}
2853 \caption{Elaboration for data types and records.}
2857 Following the intuition given by the examples, the mechanised
2858 elaboration is presented in Figure \ref{fig:elab}, which is essentially
2859 a modification of Figure 9 of \citep{McBride2004}\footnote{However, our
2860 datatypes do not have indices, we do bidirectional typechecking by
2861 treating constructors/destructors as syntactic constructs, and we have
2864 In data type declarations we allow recursive occurrences as long as
2865 they are \emph{strictly positive}, employing a syntactic check to make
2866 sure that this is the case. See \cite{Dybjer1991} for a more formal
2867 treatment of inductive definitions in ITT.
2869 For what concerns records, recursive occurrences are disallowed. The
2870 reason for this choice is answered by the reason for the choice of
2871 having records at all: we need records to give the user types with
2872 $\eta$-laws for equality, as we saw in Section \ref{sec:eta-expand}
2873 and in the treatment of OTT in Section \ref{sec:ott}. If we tried to
2874 $\eta$-expand recursive data types, we would expand forever.
2876 To implement bidirectional type checking for constructors and
2877 destructors, we store their types in full in the context, and then
2878 instantiate when due:
2880 \mydesc{typing:}{\myctx \vdash \mytmsyn \Leftrightarrow \mytmsyn}{
2883 \mytyc{D} : \mytele \myarr \mytyp \in \myctx \hspace{1cm}
2884 \mytyc{D}.\mydc{c} : \mytele \mycc \mytele' \myarr
2885 \myapp{\mytyc{D}}{\mytelee} \in \myctx \\
2886 \mytele'' = (\mytele;\mytele')\vec{A} \hspace{1cm}
2887 \mychkk{\myctx; \mytake_{i-1}(\mytele'')}{t_i}{\myix_i( \mytele'')}\ \
2888 (1 \le i \le \mytele'')
2891 \UnaryInfC{$\mychk{\myapp{\mytyc{D}.\mydc{c}}{\vec{t}}}{\myapp{\mytyc{D}}{\vec{A}}}$}
2896 \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
2897 \AxiomC{$\mytyc{D}.\myfun{f} : \mytele \mycc (\myb{x} {:}
2898 \myapp{\mytyc{D}}{\mytelee}) \myarr \myse{F}$}
2899 \AxiomC{$\myjud{\mytmt}{\myapp{\mytyc{D}}{\vec{A}}}$}
2900 \TrinaryInfC{$\myinf{\myapp{\mytyc{D}.\myfun{f}}{\mytmt}}{(\mytele
2901 \mycc (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr
2902 \myse{F})(\vec{A};\mytmt)}$}
2906 \subsubsection{Why user defined types? Why eliminators? Why no inductive families?}
2908 The hardest design choice when designing $\mykant$\ was to decide
2909 whether user defined types should be included, and how to handle them.
2910 In the end, as we saw, we can devise general structures like $\mytyc{W}$
2911 that can express all inductive structures. However, using those tools
2912 beyond very simple examples is near-impossible for a human user. Thus
2913 all theorem provers in use provide some mean for the user to define
2914 structures tailored to specific uses.
2916 Even if we take user defined data types for granted, there are two broad
2917 schools of thought regarding how to manipulate them:
2919 \item[Fixed points and pattern matching] The road chose by Agda and Coq.
2920 Functions are written like in Haskell---matching on the input and with
2921 explicit recursion. An external check on the recursive arguments
2922 ensures that they are decreasing, and thus that all functions
2923 terminate. This approach is the best in terms of user usability, but
2924 it is tricky to implement correctly.
2926 \item[Elaboration into eliminators] The road chose by \mykant, and
2927 pioneered by the Epigram line of work. The advantage is that we can
2928 reduce every data type to simple definitions which guarantee
2929 termination and are simple to reduce and type. It is however more
2930 cumbersome to use than pattern maching, although \cite{McBride2004}
2931 has shown how to implement a pattern matching interface on top of a
2932 larger set of combinators of those provided by \mykant.
2935 We chose the safer and easier to implement path, given the time
2936 constraints and the higher confidence of correctnes.
2938 Beyond normal inductive data types, \mykant\ also does not venture in
2939 more sophisticated notions. A popular improvements on basic data types
2940 are such as inductive families, where the parameters for the type
2941 constructors change based on the data constructors. This choice was
2942 motivated by the fact that inductive families can be represented by
2943 adding equalities concerning the parameters as arguments to the data
2944 constructor, in much the same way that GADTs are handled in Haskell
2945 \citep{Sulzmann2007}.
2947 Another popular extension introduced by \cite{dybjer2000general} is
2948 induction-recursion, where we define a data type in tandem with a
2949 function on that type. This technique has proven extremely useful to
2950 define embeddings of other calculi in an host language, by defining the
2951 representation of the embedded language as a data type and at the same
2952 time a function decoding from the representation to a type in the host
2955 It is also worth mentionning that in recent times there has been work by
2956 \cite{dagand2012elaborating, chapman2010gentle} to show how to define a
2957 set of primitives that data types can be elaborated into, with the
2958 additional advantage of having the possibility of having a very powerful
2959 notion of generic programming by writing functions working on the
2960 `primitive' types as to be workable by all `compatible' user-defined
2961 data types. This has been a considerable problem in the dependently
2962 type world, where we often define types which are more `strongly typed'
2963 version of similar structures,\footnote{For example the $\mytyc{OList}$
2964 presented in Section \ref{sec:user-type} being a `more typed' version
2965 of an ordinary list.} and then find ourselves forced to redefine
2966 identical operations on both types.
2968 \subsection{Cumulative hierarchy and typical ambiguity}
2969 \label{sec:term-hierarchy}
2971 Having a well founded type hierarchy is crucial if we want to retain
2972 consistency, otherwise we can break our type systems by proving bottom,
2973 as shown in Appendix \ref{app:hurkens}.
2975 However, hierarchy as presented in section \label{sec:itt} is a
2976 considerable burden on the user, on various levels. Consider for
2977 example how we recovered disjunctions in Section \ref{sec:disju}: we
2978 have a function that takes two $\mytyp_0$ and forms a new $\mytyp_0$.
2979 What if we wanted to form a disjunction containing something a
2980 $\mytyp_1$, or $\mytyp_{42}$? Our definition would fail us, since
2981 $\mytyp_1 : \mytyp_2$.
2985 \mydesc{cumulativity:}{\myctx \vdash \mytmsyn \mycumul \mytmsyn}{
2986 \begin{tabular}{ccc}
2987 \AxiomC{$\myctx \vdash \mytya \mydefeq \mytyb$}
2988 \UnaryInfC{$\myctx \vdash \mytya \mycumul \mytyb$}
2991 \AxiomC{\phantom{$\myctx \vdash \mytya \mydefeq \mytyb$}}
2992 \UnaryInfC{$\myctx \vdash \mytyp_l \mycumul \mytyp_{l+1}$}
2995 \AxiomC{$\myctx \vdash \mytya \mycumul \mytyb$}
2996 \AxiomC{$\myctx \vdash \mytyb \mycumul \myse{C}$}
2997 \BinaryInfC{$\myctx \vdash \mytya \mycumul \myse{C}$}
3003 \begin{tabular}{ccc}
3004 \AxiomC{$\myjud{\mytmt}{\mytya}$}
3005 \AxiomC{$\myctx \vdash \mytya \mycumul \mytyb$}
3006 \BinaryInfC{$\myjud{\mytmt}{\mytyb}$}
3009 \AxiomC{$\myctx \vdash \mytya_1 \mydefeq \mytya_2$}
3010 \AxiomC{$\myctx; \myb{x} : \mytya_1 \vdash \mytyb_1 \mycumul \mytyb_2$}
3011 \BinaryInfC{$\myctx (\myb{x} {:} \mytya_1) \myarr \mytyb_1 \mycumul (\myb{x} {:} \mytya_2) \myarr \mytyb_2$}
3015 \caption{Cumulativity rules for base types in \mykant, plus a
3016 `conversion' rule for cumulative types.}
3017 \label{fig:cumulativity}
3020 One way to solve this issue is a \emph{cumulative} hierarchy, where
3021 $\mytyp_{l_1} : \mytyp_{l_2}$ iff $l_1 < l_2$. This way we retain
3022 consistency, while allowing for `large' definitions that work on small
3023 types too. Figure \ref{fig:cumulativity} gives a formal definition of
3024 cumulativity for types, abstractions, and data constructors.
3026 For example we might define our disjunction to be
3028 \myarg\myfun{$\vee$}\myarg : \mytyp_{100} \myarr \mytyp_{100} \myarr \mytyp_{100}
3030 And hope that $\mytyp_{100}$ will be large enough to fit all the types
3031 that we want to use with our disjunction. However, there are two
3032 problems with this. First, there is the obvious clumsyness of having to
3033 manually specify the size of types. More importantly, if we want to use
3034 $\myfun{$\vee$}$ itself as an argument to other type-formers, we need to
3035 make sure that those allow for types at least as large as
3038 A better option is to employ a mechanised version of what Russell called
3039 \emph{typical ambiguity}: we let the user live under the illusion that
3040 $\mytyp : \mytyp$, but check that the statements about types are
3041 consistent under the hood. $\mykant$\ implements this following the
3042 lines of \cite{Huet1988}. See also \citep{Harper1991} for a published
3043 reference, although describing a more complex system allowing for both
3044 explicit and explicit hierarchy at the same time.
3046 We define a partial ordering on the levels, with both weak ($\le$) and
3047 strong ($<$) constraints---the laws governing them being the same as the
3048 ones governing $<$ and $\le$ for the natural numbers. Each occurrence
3049 of $\mytyp$ is decorated with a unique reference, and we keep a set of
3050 constraints and add new constraints as we type check, generating new
3051 references when needed.
3053 For example, when type checking the type $\mytyp\, r_1$, where $r_1$
3054 denotes the unique reference assigned to that term, we will generate a
3055 new fresh reference $\mytyp\, r_2$, and add the constraint $r_1 < r_2$
3056 to the set. When type checking $\myctx \vdash
3057 \myfora{\myb{x}}{\mytya}{\mytyb}$, if $\myctx \vdash \mytya : \mytyp\,
3058 r_1$ and $\myctx; \myb{x} : \mytyb \vdash \mytyb : \mytyp\,r_2$; we will
3059 generate new reference $r$ and add $r_1 \le r$ and $r_2 \le r$ to the
3062 If at any point the constraint set becomes inconsistent, type checking
3063 fails. Moreover, when comparing two $\mytyp$ terms we equate their
3064 respective references with two $\le$ constraints---the details are
3065 explained in Section \ref{sec:hier-impl}.
3067 Another more flexible but also more verbose alternative is the one
3068 chosen by Agda, where levels can be quantified so that the relationship
3069 between arguments and result in type formers can be explicitly
3072 \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}
3074 Inference algorithms to automatically derive this kind of relationship
3075 are currently subject of research. We chose less flexible but more
3076 concise way, since it is easier to implement and better understood.
3078 \subsection{Observational equality, \mykant\ style}
3080 There are two correlated differences between $\mykant$\ and the theory
3081 used to present OTT. The first is that in $\mykant$ we have a type
3082 hierarchy, which lets us, for example, abstract over types. The second
3083 is that we let the user define inductive types.
3085 Reconciling propositions for OTT and a hierarchy had already been
3086 investigated by Conor McBride,\footnote{See
3087 \url{http://www.e-pig.org/epilogue/index.html?p=1098.html}.} and we
3088 follow his broad design plan, although with some modifications. Most of
3089 the work, as an extension of elaboration, is to handle reduction rules
3090 and coercions for data types---both type constructors and data
3093 \subsubsection{The \mykant\ prelude, and $\myprop$ositions}
3095 Before defining $\myprop$, we define some basic types inside $\mykant$,
3096 as the target for the $\myprop$ decoder:
3099 \myadt{\mytyc{Empty}}{}{ }{ } \\
3100 \myfun{absurd} : (\myb{A} {:} \mytyp) \myarr \mytyc{Empty} \myarr \myb{A} \mapsto \\
3101 \myind{2} \myabs{\myb{A\ \myb{bot}}}{\mytyc{Empty}.\myfun{elim} \myappsp \myb{bot} \myappsp (\myabs{\_}{\myb{A}})} \\
3104 \myreco{\mytyc{Unit}}{}{}{ } \\ \ \\
3106 \myreco{\mytyc{Prod}}{\myappsp (\myb{A}\ \myb{B} {:} \mytyp)}{ }{\myfun{fst} : \myb{A}, \myfun{snd} : \myb{B} }
3109 When using $\mytyc{Prod}$, we shall use $\myprod$ to define `nested'
3110 products, and $\myproj{n}$ to project elements from them, so that
3113 \mytya \myprod \mytyb = \mytyc{Prod} \myappsp \mytya \myappsp (\mytyc{Prod} \myappsp \mytyb \myappsp \myunit) \\
3114 \mytya \myprod \mytyb \myprod \myse{C} = \mytyc{Prod} \myappsp \mytya \myappsp (\mytyc{Prod} \myappsp \mytyb \myappsp (\mytyc{Prod} \myappsp \mytyc \myappsp \myunit)) \\
3116 \myproj{1} : \mytyc{Prod} \myappsp \mytya \myappsp \mytyb \myarr \mytya \\
3117 \myproj{2} : \mytyc{Prod} \myappsp \mytya \myappsp (\mytyc{Prod} \myappsp \mytyb \myappsp \myse{C}) \myarr \mytyb \\
3121 And so on, so that $\myproj{n}$ will work with all products with at
3122 least than $n$ elements. Then we can define propositions, and decoding:
3126 \begin{array}{r@{\ }c@{\ }l}
3127 \mytmsyn & ::= & \cdots \mysynsep \myprdec{\myprsyn} \\
3128 \myprsyn & ::= & \mybot \mysynsep \mytop \mysynsep \myprsyn \myand \myprsyn \mysynsep \myprfora{\myb{x}}{\mytmsyn}{\myprsyn}
3133 \mydesc{proposition decoding:}{\myprdec{\mytmsyn} \myred \mytmsyn}{
3136 \begin{array}{l@{\ }c@{\ }l}
3137 \myprdec{\mybot} & \myred & \myempty \\
3138 \myprdec{\mytop} & \myred & \myunit
3143 \begin{array}{r@{ }c@{ }l@{\ }c@{\ }l}
3144 \myprdec{&\myse{P} \myand \myse{Q} &} & \myred & \myprdec{\myse{P}} \myprod \myprdec{\myse{Q}} \\
3145 \myprdec{&\myprfora{\myb{x}}{\mytya}{\myse{P}} &} & \myred &
3146 \myfora{\myb{x}}{\mytya}{\myprdec{\myse{P}}}
3152 Adopting the same convention as with $\mytyp$-level products, we will
3153 nest $\myand$ in the same way.
3155 \subsubsection{Some OTT examples}
3157 Before presenting the direction that $\mykant$\ takes, let us consider
3158 some examples of use-defined data types, and the result we would expect,
3159 given what we already know about OTT, assuming the same propositional
3164 \item[Product types] Let's consider first the already mentioned
3165 dependent product, using the alternate name $\mysigma$\footnote{For
3166 extra confusion, `dependent products' are often called `dependent
3167 sums' in the literature, referring to the interpretation that
3168 identifies the first element as a `tag' deciding the type of the
3169 second element, which lets us recover sum types (disjuctions), as we
3170 saw in Section \ref{sec:depprod}. Thus, $\mysigma$.} to
3171 avoid confusion with the $\mytyc{Prod}$ in the prelude:
3174 \myreco{\mysigma}{\myappsp (\myb{A} {:} \mytyp) \myappsp (\myb{B} {:} \myb{A} \myarr \mytyp)}{\\ \myind{2}}{\myfst : \myb{A}, \mysnd : \myapp{\myb{B}}{\myb{fst}}}
3177 Let's start with type-level equality. The result we want is
3180 \mysigma \myappsp \mytya_1 \myappsp \mytyb_1 \myeq \mysigma \myappsp \mytya_2 \myappsp \mytyb_2 \myred \\
3181 \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}}}
3184 The difference here is that in the original presentation of OTT
3185 the type binders are explicit, while here $\mytyb_1$ and $\mytyb_2$ are
3186 functions returning types. We can do this thanks to the type
3187 hierarchy, and this hints at the fact that heterogeneous equality will
3188 have to allow $\mytyp$ `to the right of the colon', and in fact this
3189 provides the solution to simplify the equality above.
3191 If we take, just like we saw previously in OTT
3194 \myjm{\myse{f}_1}{\myfora{\mytya_1}{\myb{x_1}}{\mytyb_1}}{\myse{f}_2}{\myfora{\mytya_2}{\myb{x_2}}{\mytyb_2}} \myred \\
3195 \myind{2} \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{
3196 \myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2} \myimpl
3197 \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}]}
3201 Then we can simply take
3204 \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}
3207 Which will reduce to precisely what we desire. For what
3208 concerns coercions and quotation, things stay the same (apart from the
3209 fact that we apply to the second argument instead of substituting).
3210 We can recognise records such as $\mysigma$ as such and employ
3211 projections in value equality and coercions; as to not
3212 impede progress if not necessary.
3214 \item[Lists] Now for finite lists, which will give us a taste for data
3218 \myadt{\mylist}{\myappsp (\myb{A} {:} \mytyp)}{ }{\mydc{nil} \mydcsep \mydc{cons} \myappsp \myb{A} \myappsp (\myapp{\mylist}{\myb{A}})}
3221 Type equality is simple---we only need to compare the parameter:
3223 \mylist \myappsp \mytya_1 \myeq \mylist \myappsp \mytya_2 \myred \mytya_1 \myeq \mytya_2
3225 For coercions, we transport based on the constructor, recycling the
3226 proof for the inductive occurrence:
3228 \begin{array}{@{}l@{\ }c@{\ }l}
3229 \mycoe \myappsp (\mylist \myappsp \mytya_1) \myappsp (\mylist \myappsp \mytya_2) \myappsp \myse{Q} \myappsp \mydc{nil} & \myred & \mydc{nil} \\
3230 \mycoe \myappsp (\mylist \myappsp \mytya_1) \myappsp (\mylist \myappsp \mytya_2) \myappsp \myse{Q} \myappsp (\mydc{cons} \myappsp \mytmm \myappsp \mytmn) & \myred & \\
3231 \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)}
3234 Value equality is unsurprising---we match the constructors, and
3235 return bottom for mismatches. However, we also need to equate the
3236 parameter in $\mydc{nil}$:
3238 \begin{array}{r@{ }c@{\ }c@{\ }c@{}l@{\ }c@{\ }r@{}c@{\ }c@{\ }c@{}l@{\ }l}
3239 (& \mydc{nil} & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{nil} & : & \myapp{\mylist}{\mytya_2} &) \myred \mytya_1 \myeq \mytya_2 \\
3240 (& \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 \\
3241 & \multicolumn{11}{@{}l}{ \myind{2}
3242 \myjm{\mytmm_1}{\mytya_1}{\mytmm_2}{\mytya_2} \myand \myjm{\mytmn_1}{\myapp{\mylist}{\mytya_1}}{\mytmn_2}{\myapp{\mylist}{\mytya_2}}
3244 (& \mydc{nil} & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{cons} \myappsp \mytmm_2 \myappsp \mytmn_2 & : & \myapp{\mylist}{\mytya_2} &) \myred \mybot \\
3245 (& \mydc{cons} \myappsp \mytmm_1 \myappsp \mytmn_1 & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{nil} & : & \myapp{\mylist}{\mytya_2} &) \myred \mybot
3251 Now for something useless but complicated.
3255 \subsubsection{Only one equality}
3257 Given the examples above, a more `flexible' heterogeneous emerged, since
3258 of the fact that in $\mykant$ we re-gain the possibility of abstracting
3259 and in general handling sets in a way that was not possible in the
3260 original OTT presentation. Moreover, we found that the rules for value
3261 equality work very well if used with user defined type
3262 abstractions---for example in the case of dependent products we recover
3263 the original definition with explicit binders, in a very simple manner.
3265 In fact, we can drop a separate notion of type-equality, which will
3266 simply be served by $\myjm{\mytya}{\mytyp}{\mytyb}{\mytyp}$, from now on
3267 abbreviated as $\mytya \myeq \mytyb$. We shall still distinguish
3268 equalities relating types for hierarchical purposes. The full rules for
3269 equality reductions, along with the syntax for propositions, are given
3270 in figure \ref{fig:kant-eq-red}. We exploit record to perform
3271 $\eta$-expansion. Moreover, given the nested $\myand$s, values of data
3272 types with zero constructors (such as $\myempty$) and records with zero
3273 destructors (such as $\myunit$) will be automatically always identified
3280 \begin{array}{r@{\ }c@{\ }l}
3281 \myprsyn & ::= & \cdots \mysynsep \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
3286 % \mytmsyn & ::= & \cdots \mysynsep \mycoee{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \mysynsep
3287 % \mycohh{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
3288 % \myprsyn & ::= & \cdots \mysynsep \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
3292 % \mydesc{typing:}{\myctx \vdash \mytmsyn \Leftrightarrow \mytmsyn}{
3294 % \begin{tabular}{cc}
3295 % \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
3296 % \AxiomC{$\myjud{\mytmt}{\mytya}$}
3297 % \BinaryInfC{$\myinf{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}$}
3300 % \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
3301 % \AxiomC{$\myjud{\mytmt}{\mytya}$}
3302 % \BinaryInfC{$\myinf{\mycohh{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\myprdec{\myjm{\mytmt}{\mytya}{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}}}$}
3309 \mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
3312 \AxiomC{\phantom{$\myjud{\myse{P}}{\myprop}$}}
3313 \UnaryInfC{$\myjud{\mytop}{\myprop}$}
3315 \UnaryInfC{$\myjud{\mybot}{\myprop}$}
3318 \AxiomC{$\myjud{\myse{P}}{\myprop}$}
3319 \AxiomC{$\myjud{\myse{Q}}{\myprop}$}
3320 \BinaryInfC{$\myjud{\myse{P} \myand \myse{Q}}{\myprop}$}
3322 \UnaryInfC{\phantom{$\myjud{\mybot}{\myprop}$}}
3331 \phantom{\myjud{\myse{A}}{\mytyp} \hspace{0.8cm} \myjud{\mytmm}{\myse{A}}} \\
3332 \myjud{\myse{A}}{\mytyp}\hspace{0.8cm}
3333 \myjudd{\myctx; \myb{x} : \mytya}{\myse{P}}{\myprop}
3336 \UnaryInfC{$\myjud{\myprfora{\myb{x}}{\mytya}{\myse{P}}}{\myprop}$}
3341 \myjud{\myse{A}}{\mytyp} \hspace{0.8cm} \myjud{\mytmm}{\myse{A}} \\
3342 \myjud{\myse{B}}{\mytyp} \hspace{0.8cm} \myjud{\mytmn}{\myse{B}}
3345 \UnaryInfC{$\myjud{\myjm{\mytmm}{\myse{A}}{\mytmn}{\myse{B}}}{\myprop}$}
3352 \mydesc{equality reduction:}{\myctx \vdash \myprsyn \myred \myprsyn}{
3356 \UnaryInfC{$\myctx \vdash \myjm{\mytyp}{\mytyp}{\mytyp}{\mytyp} \myred \mytop$}
3360 \UnaryInfC{$\myctx \vdash \myjm{\myprdec{\myse{P}}}{\mytyp}{\myprdec{\myse{Q}}}{\mytyp} \myred \mytop$}
3368 \begin{array}{@{}r@{\ }l}
3370 \myjm{\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}}{\mytyp}{\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}}{\mytyp} \myred \\
3371 & \myind{2} \mytya_2 \myeq \mytya_1 \myand \myprfora{\myb{x_2}}{\mytya_2}{\myprfora{\myb{x_1}}{\mytya_1}{
3372 \myjm{\myb{x_2}}{\mytya_2}{\myb{x_1}}{\mytya_1} \myimpl \mytyb_1[\myb{x_1}] \myeq \mytyb_2[\myb{x_2}]
3382 \begin{array}{@{}r@{\ }l}
3384 \myjm{\myse{f}_1}{\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}}{\myse{f}_2}{\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}} \myred \\
3385 & \myind{2} \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{
3386 \myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2} \myimpl
3387 \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}]}
3396 \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
3398 \begin{array}{r@{\ }l}
3400 \myjm{\mytyc{D} \myappsp \vec{A}}{\mytyp}{\mytyc{D} \myappsp \vec{B}}{\mytyp} \myred \\
3401 & \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}))})
3410 \mydataty(\mytyc{D}, \myctx)\hspace{0.8cm}
3411 \mytyc{D}.\mydc{c} : \mytele;\mytele' \myarr \mytyc{D} \myappsp \mytelee \in \myctx \hspace{0.8cm}
3412 \mytele_A = (\mytele;\mytele')\vec{A}\hspace{0.8cm}
3413 \mytele_B = (\mytele;\mytele')\vec{B}
3417 \begin{array}{@{}l@{\ }l}
3418 \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 \\
3419 & \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}))})
3426 \AxiomC{$\mydataty(\mytyc{D}, \myctx)$}
3428 \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
3436 \myisreco(\mytyc{D}, \myctx)\hspace{0.8cm}
3437 \mytyc{D}.\myfun{f}_i : \mytele; (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr \myse{F}_i \in \myctx\\
3441 \begin{array}{@{}l@{\ }l}
3442 \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})})
3449 \UnaryInfC{$\myjm{\mytmm}{\mytya}{\mytmn}{\mytyb} \myred \mybot\ \text{if $\mytya$ and $\mytyb$ are canonical types.}$}
3452 \caption{Propositions and equality reduction in $\mykant$. We assume
3453 the presence of $\mydataty$ and $\myisreco$ as operations on the
3454 context to recognise whether a user defined type is a data type or a
3456 \label{fig:kant-eq-red}
3459 \subsubsection{Coercions}
3463 \subsubsection{$\myprop$ and the hierarchy}
3465 We shall have, at earch universe level, not only a $\mytyp_l$ but also a
3466 $\myprop_l$. Where will propositions placed in the type hierarchy? The
3467 main indicator is the decoding operator, since it converts into things
3468 that already live in the hierarchy. For example, if we have
3470 \myprdec{\mynat \myarr \mybool \myeq \mynat \myarr \mybool} \myred
3471 \mytop \myand ((\myb{x}\, \myb{y} : \mynat) \myarr \mytop \myarr \mytop)
3473 we will better make sure that the `to be decoded' is at the same
3474 level as its reduction as to preserve subject reduction. In the example
3475 above, we'll have that proposition to be at least as large as the type
3476 of $\mynat$, since the reduced proof will abstract over it. Pretending
3477 that we had explicit, non cumulative levels, it would be tempting to have
3480 \AxiomC{$\myjud{\myse{Q}}{\myprop_l}$}
3481 \UnaryInfC{$\myjud{\myprdec{\myse{Q}}}{\mytyp_l}$}
3484 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
3485 \AxiomC{$\myjud{\mytyb}{\mytyp_l}$}
3486 \BinaryInfC{$\myjud{\myjm{\mytya}{\mytyp_{l}}{\mytyb}{\mytyp_{l}}}{\myprop_l}$}
3490 $\mybot$ and $\mytop$ living at any level, $\myand$ and $\forall$
3491 following rules similar to the ones for $\myprod$ and $\myarr$ in
3492 Section \ref{sec:itt}. However, we need to be careful with value
3493 equality since for example we have that
3495 \myprdec{\myjm{\myse{f}_1}{\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}}{\myse{f}_2}{\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}}}
3497 \myfora{\myb{x_1}}{\mytya_1}{\myfora{\myb{x_2}}{\mytya_2}{\cdots}}
3499 where the proposition decodes into something of at least type $\mytyp_l$, where
3500 $\mytya_l : \mytyp_l$ and $\mytyb_l : \mytyp_l$. We can resolve this
3501 tension by making all equalities larger:
3503 \AxiomC{$\myjud{\mytmm}{\mytya}$}
3504 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
3505 \AxiomC{$\myjud{\mytmn}{\mytyb}$}
3506 \AxiomC{$\myjud{\mytyb}{\mytyp_l}$}
3507 \QuaternaryInfC{$\myjud{\myjm{\mytmm}{\mytya}{\mytmm}{\mytya}}{\myprop_l}$}
3509 This is disappointing, since type equalities will be needlessly large:
3510 $\myprdec{\myjm{\mytya}{\mytyp_l}{\mytyb}{\mytyp_l}} : \mytyp_{l + 1}$.
3512 However, considering that our theory is cumulative, we can do better.
3513 Assuming rules for $\myprop$ cumulativity similar to the ones for
3514 $\mytyp$, we will have (with the conversion rule reproduced as a
3518 \AxiomC{$\myctx \vdash \mytya \mycumul \mytyb$}
3519 \AxiomC{$\myjud{\mytmt}{\mytya}$}
3520 \BinaryInfC{$\myjud{\mytmt}{\mytyb}$}
3523 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
3524 \AxiomC{$\myjud{\mytyb}{\mytyp_l}$}
3525 \BinaryInfC{$\myjud{\myjm{\mytya}{\mytyp_{l}}{\mytyb}{\mytyp_{l}}}{\myprop_l}$}
3531 \AxiomC{$\myjud{\mytmm}{\mytya}$}
3532 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
3533 \AxiomC{$\myjud{\mytmn}{\mytyb}$}
3534 \AxiomC{$\myjud{\mytyb}{\mytyp_l}$}
3535 \AxiomC{$\mytya$ and $\mytyb$ are not $\mytyp_{l'}$}
3536 \QuinaryInfC{$\myjud{\myjm{\mytmm}{\mytya}{\mytmm}{\mytya}}{\myprop_l}$}
3540 That is, we are small when we can (type equalities) and large otherwise.
3541 This would not work in a non-cumulative theory because subject reduction
3542 would not hold. Consider for instance
3544 \myjm{\mynat}{\myITE{\mytrue}{\mytyp_0}{\mytyp_0}}{\mybool}{\myITE{\mytrue}{\mytyp_0}{\mytyp_0}}
3548 \[\myjm{\mynat}{\mytyp_0}{\mybool}{\mytyp_0} : \myprop_0 \]
3549 We need $\myprop_0$ to be $\myprop_1$ too, which will be the case with
3550 cumulativity. This is not the most elegant of systems, but it buys us a
3551 cheap type level equality without having to replicate functionality with
3552 a dedicated construct.
3554 \subsubsection{Quotation and definitional equality}
3555 \label{sec:kant-irr}
3557 Now we can give an account of definitional equality, by explaining how
3558 to perform quotation (as defined in Section \ref{sec:eta-expand})
3559 towards the goal described in Section \ref{sec:ott-quot}.
3563 \item Perform $\eta$-expansion on functions and records.
3565 \item As a consequence of the previous point, identify all records with
3566 no projections as equal, since they will have only one element.
3568 \item Identify all members of types with no elements as equal.
3570 \item Identify all equivalent proofs as equal---with `equivalent proof'
3571 we mean those proving the same propositions.
3573 \item Advance coercions working across definitionally equal types.
3575 Towards these goals and following the intuition between bidirectional
3576 type checking we define two mutually recursive functions, one quoting
3577 canonical terms against their types (since we need the type to typecheck
3578 canonical terms), one quoting neutral terms while recovering their
3579 types. The full procedure for quotation is shown in Figure
3580 \ref{fig:kant-quot}. We $\boxed{\text{box}}$ the neutral proofs and
3581 neutral members of empty types, following the notation in
3582 \cite{Altenkirch2007}, and we make use of $\mydefeq_{\mybox}$ which
3583 compares terms syntactically up to $\alpha$-renaming, but also up to
3584 equivalent proofs: we consider all boxed content as equal.
3586 Our quotation will work on normalised terms, so that all defined values
3587 will have been replaced. Moreover, we match on datatype eliminators and
3588 all their arguments, so that $\mynat.\myfun{elim} \myappsp \mytmm
3589 \myappsp \myse{P} \myappsp \vec{\mytmn}$ will stand for
3590 $\mynat.\myfun{elim}$ applied to the scrutinised $\mynat$, the
3591 predicate, and the two cases. This measure can be easily implemented by
3592 checking the head of applications and `consuming' the needed terms.
3595 \mydesc{canonical quotation:}{\mycanquot(\myctx, \mytmsyn : \mytmsyn) \mymetagoes \mytmsyn}{
3598 \begin{array}{@{}l@{}l}
3599 \mycanquot(\myctx,\ \mytmt : \mytyc{D} \myappsp \vec{A} &) \mymetaguard \mymeta{empty}(\myctx, \mytyc{D}) \mymetagoes \boxed{\mytmt} \\
3600 \mycanquot(\myctx,\ \mytmt : \mytyc{D} \myappsp \vec{A} &) \mymetaguard \mymeta{record}(\myctx, \mytyc{D}) \mymetagoes \mytyc{D}.\mydc{constr} \myappsp \cdots \myappsp \mycanquot(\myctx, \mytyc{D}.\myfun{f}_n : (\myctx(\mytyc{D}.\myfun{f}_n))(\vec{A};\mytmt)) \\
3601 \mycanquot(\myctx,\ \mytyc{D}.\mydc{c} \myappsp \vec{t} : \mytyc{D} \myappsp \vec{A} &) \mymetagoes \cdots \\
3602 \mycanquot(\myctx,\ \myse{f} : \myfora{\myb{x}}{\mytya}{\mytyb} &) \mymetagoes \myabs{\myb{x}}{\mycanquot(\myctx; \myb{x} : \mytya, \myapp{\myse{f}}{\myb{x}} : \mytyb)} \\
3603 \mycanquot(\myctx,\ \myse{p} : \myprdec{\myse{P}} &) \mymetagoes \boxed{\myse{p}}
3605 \mycanquot(\myctx,\ \mytmt : \mytya &) \mymetagoes \mytmt'\ \text{\textbf{where}}\ \mytmt' : \myarg = \myneuquot(\myctx, \mytmt)
3612 \mydesc{neutral quotation:}{\myneuquot(\myctx, \mytmsyn) \mymetagoes \mytmsyn : \mytmsyn}{
3615 \begin{array}{@{}l@{}l}
3616 \myneuquot(\myctx,\ \myb{x} &) \mymetagoes \myb{x} : \myctx(\myb{x}) \\
3617 \myneuquot(\myctx,\ \mytyp &) \mymetagoes \mytyp : \mytyp \\
3618 \myneuquot(\myctx,\ \myfora{\myb{x}}{\mytya}{\mytyb} & ) \mymetagoes
3619 \myfora{\myb{x}}{\myneuquot(\myctx, \mytya)}{\myneuquot(\myctx; \myb{x} : \mytya, \mytyb)} : \mytyp \\
3620 \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 \\
3621 \myneuquot(\myctx,\ \myprdec{\myjm{\mytmm}{\mytya}{\mytmn}{\mytyb}} &) \mymetagoes \myprdec{\myjm{\mycanquot(\myctx, \mytmm : \mytya)}{\mytya'}{\mycanquot(\myctx, \mytmn : \mytyb)}{\mytyb'}} : \mytyp \\
3622 \multicolumn{2}{@{}l}{\myind{2}\text{\textbf{where}}\ \mytya' : \myarg = \myneuquot(\myctx, \mytya)} \\
3623 \multicolumn{2}{@{}l}{\myind{2}\phantom{\text{\textbf{where}}}\ \mytyb' : \myarg = \myneuquot(\myctx, \mytyb)} \\
3624 \myneuquot(\myctx,\ \mytyc{D}.\myfun{f} \myappsp \mytmt &) \mymetaguard \mymeta{record}(\myctx, \mytyc{D}) \mymetagoes \mytyc{D}.\myfun{f} \myappsp \mytmt' : (\myctx(\mytyc{D}.\myfun{f}))(\vec{A};\mytmt) \\
3625 \multicolumn{2}{@{}l}{\myind{2}\text{\textbf{where}}\ \mytmt' : \mytyc{D} \myappsp \vec{A} = \myneuquot(\myctx, \mytmt)} \\
3626 \myneuquot(\myctx,\ \mytyc{D}.\myfun{elim} \myappsp \mytmt \myappsp \myse{P} &) \mymetaguard \mymeta{empty}(\myctx, \mytyc{D}) \mymetagoes \mytyc{D}.\myfun{elim} \myappsp \boxed{\mytmt} \myappsp \myneuquot(\myctx, \myse{P}) : \myse{P} \myappsp \mytmt \\
3627 \myneuquot(\myctx,\ \mytyc{D}.\myfun{elim} \myappsp \mytmm \myappsp \myse{P} \myappsp \vec{\mytmn} &) \mymetagoes \mytyc{D}.\myfun{elim} \myappsp \mytmm' \myappsp \myneuquot(\myctx, \myse{P}) \cdots : \myse{P} \myappsp \mytmm\\
3628 \multicolumn{2}{@{}l}{\myind{2}\text{\textbf{where}}\ \mytmm' : \mytyc{D} \myappsp \vec{A} = \myneuquot(\myctx, \mytmm)} \\
3629 \myneuquot(\myctx,\ \myapp{\myse{f}}{\mytmt} &) \mymetagoes \myapp{\myse{f'}}{\mycanquot(\myctx, \mytmt : \mytya)} : \mysub{\mytyb}{\myb{x}}{\mytmt} \\
3630 \multicolumn{2}{@{}l}{\myind{2}\text{\textbf{where}}\ \myse{f'} : \myfora{\myb{x}}{\mytya}{\mytyb} = \myneuquot(\myctx, \myse{f})} \\
3631 \myneuquot(\myctx,\ \mycoee{\mytya}{\mytyb}{\myse{Q}}{\mytmt} &) \mymetaguard \myneuquot(\myctx, \mytya) \mydefeq_{\mybox} \myneuquot(\myctx, \mytyb) \mymetagoes \myneuquot(\myctx, \mytmt) \\
3632 \myneuquot(\myctx,\ \mycoee{\mytya}{\mytyb}{\myse{Q}}{\mytmt} &) \mymetagoes
3633 \mycoee{\myneuquot(\myctx, \mytya)}{\myneuquot(\myctx, \mytyb)}{\boxed{\myse{Q}}}{\myneuquot(\myctx, \mytmt)}
3637 \caption{Quotation in \mykant. Along the already used
3638 $\mymeta{record}$ meta-operation on the context we make use of
3639 $\mymeta{empty}$, which checks if a certain type constructor has
3640 zero data constructor. The `data constructor' cases for non-record,
3641 non-empty, data types are omitted for brevity.}
3642 \label{fig:kant-quot}
3645 \subsubsection{Why $\myprop$?}
3647 It is worth to ask if $\myprop$ is needed at all. It is perfectly
3648 possible to have the type checker identify propositional types
3649 automatically, and in fact in some sense we already do during equality
3650 reduction and quotation. However, this has the considerable
3651 disadvantage that we can never identify abstracted
3652 variables\footnote{And in general neutral terms, although we currently
3653 don't have neutral propositions.} of type $\mytyp$ as $\myprop$, thus
3654 forbidding the user to talk about $\myprop$ explicitly.
3656 This is a considerable impediment, for example when implementing
3657 \emph{quotient types}. With quotients, we let the user specify an
3658 equivalence class over a certain type, and then exploit this in various
3659 way---crucially, we need to be sure that the equivalence given is
3660 propositional, a fact which prevented the use of quotients in dependent
3661 type theories \citep{Jacobs1994}.
3663 \section{\mykant : The practice}
3664 \label{sec:kant-practice}
3666 The codebase consists of around 2500 lines of Haskell, as reported by
3667 the \texttt{cloc} utility. The high level design is inspired by the
3668 work on various incarnations of Epigram, and specifically by the first
3669 version as described \citep{McBride2004} and the codebase for the new
3670 version.\footnote{Available intermittently as a \texttt{darcs}
3671 repository at \url{http://sneezy.cs.nott.ac.uk/darcs/Pig09}.} In many
3672 ways \mykant\ is something in between the first and second version of
3675 The author learnt the hard way the implementation challenges for such a
3676 project, and while there is a solid and working base to work on, the
3677 implementation of observational equality is not currently complete.
3678 However, given the detailed plan in the previous section, doing so
3679 should not prove to be too much work.
3681 The interaction happens in a read-eval-print loop (REPL), which presents
3682 itself as in Fiure \ref{fig:kant-web}. The REPL is a available both as
3683 a commandline application and in a web interface, which is available at
3684 \url{bertus.mazzo.li}.
3687 {\small\begin{verbatim}B E R T U S
3688 Version 0.0, made in London, year 2013.
3690 <decl> Declare value/data type/record
3693 :p <term> Pretty print
3695 :r <file> Reload file (erases previous environment)
3696 :i <name> Info about an identifier
3698 >>> :l data/samples/good/common.ka
3700 >>> :e plus three two
3701 suc (suc (suc (suc (suc zero))))
3702 >>> :t plus three two
3703 Type: Nat\end{verbatim}
3706 \caption{A sample run of the \mykant\ prompt.}
3707 \label{fig:kant-web}
3710 The interaction with the user takes place in a loop living in and
3711 updating a context of \mykant\ declarations. A REPL cycle starts with
3712 the user inputing a \mykant\ declaration or another REPL command, which
3713 then goes through various stages that can end up in a context update, or
3714 in failures of various kind. The process is described diagrammatically
3715 in figure \ref{fig:kant-process}:
3719 \item[Parse] In this phase the text input gets converted to a sugared
3720 version of the core language. For example, we accept multiple
3721 arguments in arrow types and abstractions, and we represent variables
3722 with names, while as we will see in Section \ref{sec:term-repr} the
3723 final term types uses a \emph{nameless} representation.
3725 \item[Desugar] The sugared declaration is converted to a core term.
3726 Most notably we go from names to nameless.
3728 \item[ConDestr] Short for `Constructors/Destructors', converts
3729 applications of data destructors and constructors to a special form,
3730 to perform bidirectional type checking.
3732 \item[Reference] Occurrences of $\mytyp$ get decorated by a unique reference,
3733 which is necessary to implement the type hierarchy check.
3735 \item[Elaborate] Converts the declaration to some context items, which
3736 might be a value declaration (type and body) or a data type
3737 declaration (constructors and destructors). This phase works in
3738 tandem with \textbf{Type checking}, which in turns needs to
3739 \textbf{Evaluate} terms.
3741 \item[Distill] and report the result. `Distilling' refers to the
3742 process of converting a core term back to a sugared version that the
3743 user can visualise. This can be necessary both to display errors
3744 including terms or to display result of evaluations or type checking
3745 that the user has requested. Among the other things in this stage we
3746 go from nameless back to names by recycling the names that the user
3747 used originally, as to fabricate a term which is as close as possible
3748 to what it originated from.
3750 \item[Pretty print] Format the terms in a nice way, and display the result to
3757 \tikzstyle{block} = [rectangle, draw, text width=5em, text centered, rounded
3758 corners, minimum height=2.5em, node distance=0.7cm]
3760 \tikzstyle{decision} = [diamond, draw, text width=4.5em, text badly
3761 centered, inner sep=0pt, node distance=0.7cm]
3763 \tikzstyle{line} = [draw, -latex']
3765 \tikzstyle{cloud} = [draw, ellipse, minimum height=2em, text width=5em, text
3766 centered, node distance=1.5cm]
3769 \begin{tikzpicture}[auto]
3770 \node [cloud] (user) {User};
3771 \node [block, below left=1cm and 0.1cm of user] (parse) {Parse};
3772 \node [block, below=of parse] (desugar) {Desugar};
3773 \node [block, below=of desugar] (condestr) {ConDestr};
3774 \node [block, below=of condestr] (reference) {Reference};
3775 \node [block, below=of reference] (elaborate) {Elaborate};
3776 \node [block, left=of elaborate] (tycheck) {Typecheck};
3777 \node [block, left=of tycheck] (evaluate) {Evaluate};
3778 \node [decision, right=of elaborate] (error) {Error?};
3779 \node [block, right=of parse] (pretty) {Pretty print};
3780 \node [block, below=of pretty] (distill) {Distill};
3781 \node [block, below=of distill] (update) {Update context};
3783 \path [line] (user) -- (parse);
3784 \path [line] (parse) -- (desugar);
3785 \path [line] (desugar) -- (condestr);
3786 \path [line] (condestr) -- (reference);
3787 \path [line] (reference) -- (elaborate);
3788 \path [line] (elaborate) edge[bend right] (tycheck);
3789 \path [line] (tycheck) edge[bend right] (elaborate);
3790 \path [line] (elaborate) -- (error);
3791 \path [line] (error) edge[out=0,in=0] node [near start] {yes} (distill);
3792 \path [line] (error) -- node [near start] {no} (update);
3793 \path [line] (update) -- (distill);
3794 \path [line] (pretty) -- (user);
3795 \path [line] (distill) -- (pretty);
3796 \path [line] (tycheck) edge[bend right] (evaluate);
3797 \path [line] (evaluate) edge[bend right] (tycheck);
3800 \caption{High level overview of the life of a \mykant\ prompt cycle.}
3801 \label{fig:kant-process}
3804 Here we will review only a sampling of the more interesting
3805 implementation challenges present when implementing an interactive
3808 \subsection{What is done, what is missing}
3810 Sadly the author ran out of time while implementing observational
3811 equality, and while the constructs and typing rules are present, the
3812 machinery to make it happen (equality reduction, coercions, quotation,
3813 etc.) is not present yet. Everything else presented is implemented and
3814 working reasonably well.
3820 \begin{array}{@{\ \ }l@{\ }c@{\ }l}
3821 \multicolumn{3}{@{}l}{\text{A name, in regexp notation.}} \\
3822 \mysee{name} & ::= & \texttt{[a-zA-Z] [a-zA-Z0-9'\_-]*} \\
3823 \multicolumn{3}{@{}l}{\text{A binder might or might not (\texttt{\_}) bind.}} \\
3824 \mysee{binder} & ::= & \mytermi{\_} \mysynsep \mysee{name} \\
3825 \multicolumn{3}{@{}l}{\text{A series of typed bindings.}} \\
3826 \mysee{telescope}\, \ \ \ & ::= & (\mytermi{[}\ \mysee{binder}\ \mytermi{:}\ \mysee{term}\ \mytermi{]}){*} \\
3827 \multicolumn{3}{@{}l}{\text{Terms, including propositions.}} \\
3828 \multicolumn{3}{@{}l}{
3829 \begin{array}{@{\ \ }l@{\ }c@{\ }l@{\ \ \ \ \ }l}
3830 \mysee{term} & ::= & \mysee{name} & \text{A variable.} \\
3831 & | & \mytermi{*} & \text{\mytyc{Type}.} \\
3832 & | & \mytermi{\{|}\ \mysee{term}{*}\ \mytermi{|\}} & \text{Type holes.} \\
3833 & | & \mytermi{Prop} & \text{\mytyc{Prop}.} \\
3834 & | & \mytermi{Top} \mysynsep \mytermi{Bot} & \text{$\mytop$ and $\mybot$.} \\
3835 & | & \mysee{term}\ \mytermi{/\textbackslash}\ \mysee{term} & \text{Conjuctions.} \\
3836 & | & \mytermi{[|}\ \mysee{term}\ \mytermi{|]} & \text{Proposition decoding.} \\
3837 & | & \mytermi{coe}\ \mysee{term}\ \mysee{term}\ \mysee{term}\ \mysee{term} & \text{Coercion.} \\
3838 & | & \mytermi{coh}\ \mysee{term}\ \mysee{term}\ \mysee{term}\ \mysee{term} & \text{Coherence.} \\
3839 & | & \mytermi{(}\ \mysee{term}\ \mytermi{:}\ \mysee{term}\ \mytermi{)}\ \mytermi{=}\ \mytermi{(}\ \mysee{term}\ \mytermi{:}\ \mysee{term}\ \mytermi{)} & \text{Heterogeneous equality.} \\
3840 & | & \mytermi{(}\ \mysee{compound}\ \mytermi{)} & \text{Parenthesised term.} \\
3841 \mysee{compound} & ::= & \mytermi{\textbackslash}\ \mysee{binder}{*}\ \mytermi{=>}\ \mysee{term} & \text{Untyped abstraction.} \\
3842 & | & \mytermi{\textbackslash}\ \mysee{telescope}\ \mytermi{:}\ \mysee{term}\ \mytermi{=>}\ \mysee{term} & \text{Typed abstraction.} \\
3843 & | & \mytermi{forall}\ \mysee{telescope}\ \mysee{term} & \text{Universal quantification.} \\
3844 & | & \mysee{arr} \\
3845 \mysee{arr} & ::= & \mysee{telescope}\ \mytermi{->}\ \mysee{arr} & \text{Dependent function.} \\
3846 & | & \mysee{term}\ \mytermi{->}\ \mysee{arr} & \text{Non-dependent function.} \\
3847 & | & \mysee{term}{+} & \text {Application.}
3850 \multicolumn{3}{@{}l}{\text{Typed names.}} \\
3851 \mysee{typed} & ::= & \mysee{name}\ \mytermi{:}\ \mysee{term} \\
3852 \multicolumn{3}{@{}l}{\text{Declarations.}} \\
3853 \mysee{decl}& ::= & \mysee{value} \mysynsep \mysee{abstract} \mysynsep \mysee{data} \mysynsep \mysee{record} \\
3854 \multicolumn{3}{@{}l}{\text{Defined values. The telescope specifies named arguments.}} \\
3855 \mysee{value} & ::= & \mysee{name}\ \mysee{telescope}\ \mytermi{:}\ \mysee{term}\ \mytermi{=>}\ \mysee{term} \\
3856 \multicolumn{3}{@{}l}{\text{Abstracted variables.}} \\
3857 \mysee{abstract} & ::= & \mytermi{postulate}\ \mysee{typed} \\
3858 \multicolumn{3}{@{}l}{\text{Data types, and their constructors.}} \\
3859 \mysee{data} & ::= & \mytermi{data}\ \mysee{name}\ \mysee{telescope}\ \mytermi{->}\ \mytermi{*}\ \mytermi{=>}\ \mytermi{\{}\ \mysee{constrs}\ \mytermi{\}} \\
3860 \mysee{constrs} & ::= & \mysee{typed} \\
3861 & | & \mysee{typed}\ \mytermi{|}\ \mysee{constrs} \\
3862 \multicolumn{3}{@{}l}{\text{Records, and their projections. The $\mysee{name}$ before the projections is the constructor name.}} \\
3863 \mysee{record} & ::= & \mytermi{record}\ \mysee{name}\ \mysee{telescope}\ \mytermi{->}\ \mytermi{*}\ \mytermi{=>}\ \mysee{name}\ \mytermi{\{}\ \mysee{projs}\ \mytermi{\}} \\
3864 \mysee{projs} & ::= & \mysee{typed} \\
3865 & | & \mysee{typed}\ \mytermi{,}\ \mysee{projs}
3869 \caption{\mykant' syntax. The non-terminals are marked with
3870 $\langle\text{angle brackets}\rangle$ for greater clarity. The
3871 syntax in the implementation is actually more liberal, for example
3872 giving the possibility of using arrow types directly in
3873 constructor/projection declarations.}
3877 The syntax of \mykant\ is presented in Figure \ref{fig:syntax}.
3878 Examples showing the usage of most of the constructs are present in
3879 Appendices \ref{app:kant-itt}, \ref{app:kant-examples}, and
3882 \subsection{Term and context representation}
3883 \label{sec:term-repr}
3885 \subsubsection{Naming and substituting}
3887 Perhaps surprisingly, one of the most difficult challenges in
3888 implementing a theory of the kind presented is choosing a good data type
3889 for terms, and specifically handling substitutions in a sane way.
3891 There are two broad schools of thought when it comes to naming
3892 variables, and thus substituting:
3894 \item[Nameful] Bound variables are represented by some enumerable data
3895 type, just as we have described up to now, starting from Section
3896 \ref{sec:untyped}. The problem is that avoiding name capturing is a
3897 nightmare, both in the sense that it is not performant---given that we
3898 need to rename rename substitute each time we `enter' a binder---but
3899 most importantly given the fact that in even more slightly complicated
3900 systems it is very hard to get right, even for experts.
3902 One of the sore spots of explicit names is comparing terms up
3903 $\alpha$-renaming, which again generates a huge amounts of
3904 substitutions and requires special care. We can represent the
3905 relationship between variables and their binders, by...
3907 \item[Nameless] ...getting rid of names altogether, and representing
3908 bound variables with an index referring to the `binding' structure, a
3909 notion introduced by \cite{de1972lambda}. Classically $0$ represents
3910 the variable bound by the innermost binding structure, $1$ the
3911 second-innermost, and so on. For instance with simple abstractions we
3915 \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} \\
3916 \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
3920 While this technique is obviously terrible in terms of human
3921 usability,\footnote{With some people going as far as defining it akin
3922 to an inverse Turing test.} it is much more convenient as an
3923 internal representation to deal with terms mechanically---at least in
3924 simple cases. Moreover, $\alpha$ renaming ceases to be an issue, and
3925 term comparison is purely syntactical.
3927 Nonetheless, more complex, constructs such as pattern matching put
3928 some strain on the indices and many systems end up using explicit
3929 names anyway (Agda, Coq, \dots).
3933 In the past decade or so advancements in the Haskell's type system and
3934 in general the spread new programming practices have enabled to make the
3935 second option much more amenable. \mykant\ thus takes the second path
3936 through the use of Edward Kmett's excellent \texttt{bound}
3937 library.\footnote{Available at
3938 \url{http://hackage.haskell.org/package/bound}.} We decribe its
3939 advantages but also pitfalls in the previously relatively unknown
3940 territory of dependent types---\texttt{bound} being created mostly to
3941 handle more simply typed systems.
3943 \texttt{bound} builds on the work of \cite{Bird1999}, who suggest to
3944 parametrising the term type over the type of the variables, and `nest'
3945 the type each time we enter a scope. If we wanted to define a term for
3946 the untyped $\lambda$-calculus, we might have
3948 -- A type with no members.
3951 data Var v = Bound | Free v
3954 = V v -- Bound variable
3955 | App (Tm v) (Tm v) -- Term application
3956 | Lam (Tm (Var v)) -- Abstraction
3958 Closed terms would be of type \texttt{Tm Empty}, so that there would be
3959 no occurrences of \texttt{V}. However, inside an abstraction, we can
3960 have \texttt{V Bound}, representing the bound variable, and inside a
3961 second abstraction we can have \texttt{V Bound} or \texttt{V (Free
3962 Bound)}. Thus the term
3963 \[\myabs{\myb{x}}{\myabs{\myb{y}}{\myb{x}}}\]
3964 can be represented as
3966 -- The top level term is of type `Tm Empty'.
3967 -- The inner term `Lam (Free Bound)' is of type `Tm (Var Empty)'.
3968 -- The second inner term `V (Free Bound)' is of type `Tm (Var (Var
3970 Lam (Lam (V (Free Bound)))
3972 This allows us to reflect the of a type `nestedness' at the type level,
3973 and since we usually work with functions polymorphic on the parameter
3974 \texttt{v} it's very hard to make mistakes by putting terms of the wrong
3975 nestedness where they don't belong.
3977 Even more interestingly, the substitution operation is perfectly
3978 captured by the \verb|>>=| (bind) operator of the \texttt{Monad}
3983 (>>=) :: m a -> (a -> m b) -> m b
3985 instance Monad Tm where
3986 -- `return'ing turns a variable into a `Tm'
3989 -- `t >>= f' takes a term `t' and a mapping from variables to terms
3990 -- `f' and applies `f' to all the variables in `t', replacing them
3991 -- with the mapped terms.
3993 App m n >>= f = App (m >>= f) (n >>= f)
3995 -- `Lam' is the tricky case: we modify the function to work with bound
3996 -- variables, so that if it encounters `Bound' it leaves it untouched
3997 -- (since the mapping refers to the outer scope); if it encounters a
3998 -- free variable it asks `f' for the term and then updates all the
3999 -- variables to make them refer to the outer scope they were meant to
4001 Lam s >>= f = Lam (s >>= bump)
4002 where bump Bound = return Bound
4003 bump (Free v) = f v >>= V . Free
4005 With this in mind, we can define functions which will not only work on
4006 \verb|Tm|, but on any \verb|Monad|!
4008 -- Replaces free variable `v' with `m' in `n'.
4009 subst :: (Eq v, Monad m) => v -> m v -> m v -> m v
4010 subst v m n = n >>= \v' -> if v == v' then m else return v'
4012 -- Replace the variable bound by `s' with term `t'.
4013 inst :: Monad m => m v -> m (Var v) -> m v
4014 inst t s = do v <- s
4017 Free v' -> return v'
4019 The beauty of this technique is that in a few simple function we have
4020 defined all the core operations in a general and `obviously correct'
4021 way, with the extra confidence of having the type checker looking our
4022 back. For what concerns term equality, we can just ask the Haskell
4023 compiler to derive the instance for the \verb|Eq| type class and since
4024 we are nameless that will be enough (modulo fancy quotation).
4026 Moreover, if we take the top level term type to be \verb|Tm String|, we
4027 get for free a representation of terms with top-level, definitions;
4028 where closed terms contain only \verb|String| references to said
4029 definitions---see also \cite{McBride2004b}.
4031 What are then the pitfalls of this seemingly invincible technique? The
4032 most obvious impediment is the need for polymorphic recursion.
4033 Functions traversing terms parametrised by the variable type will have
4036 -- Infer the type of a term, or return an error.
4037 infer :: Tm v -> Either Error (Tm v)
4039 When traversing under a \verb|Scope| the parameter changes from \verb|v|
4040 to \verb|Var v|, and thus if we do not specify the type for our function explicitly
4041 inference will fail---type inference for polymorphic recursion being
4042 undecidable \citep{henglein1993type}. This causes some annoyance,
4043 especially in the presence of many local definitions that we would like
4046 But the real issue is the fact that giving a type parametrised over a
4047 variable---say \verb|m v|---a \verb|Monad| instance means being able to
4048 only substitute variables for values of type \verb|m v|. This is a
4049 considerable inconvenience. Consider for instance the case of
4050 telescopes, which are a central tool to deal with contexts and other
4051 constructs. In Haskell we can give them a faithful representation
4052 with a data type along the lines of
4054 data Tele m v = End (m v) | Bind (m v) (Tele (Var v))
4055 type TeleTm = Tele Tm
4057 The problem here is that what we want to substitute for variables in
4058 \verb|Tele m v| is \verb|m v| (probably \verb|Tm v|), not \verb|Tele m v| itself! What we need is
4060 bindTele :: Monad m => Tele m a -> (a -> m b) -> Tele m b
4061 substTele :: (Eq v, Monad m) => v -> m v -> Tele m v -> Tele m v
4062 instTele :: Monad m => m v -> Tele m (Var v) -> Tele m v
4064 Not what \verb|Monad| gives us. Solving this issue in an elegant way
4065 has been a major sink of time and source of headaches for the author,
4066 who analysed some of the alternatives---most notably the work by
4067 \cite{weirich2011binders}---but found it impossible to give up the
4068 simplicity of the model above.
4070 That said, our term type is still reasonably brief, as shown in full in
4071 Appendix \ref{app:termrep}. The fact that propositions cannot be
4072 factored out in another data type is an instance of the problem
4073 described above. However the real pain is during elaboration, where we
4074 are forced to treat everything as a type while we would much rather have
4075 telescopes. Future work would include writing a library that marries a
4076 nice interface similar to the one of \verb|bound| with a more flexible
4079 We also make use of a `forgetful' data type (as provided by
4080 \verb|bound|) to store user-provided variables names along with the
4081 `nameless' representation, so that the names will not be considered when
4082 compared terms, but will be available when distilling so that we can
4083 recover variable names that are as close as possible to what the user
4086 \subsubsection{Evaluation}
4088 Another source of contention related to term representation is dealing
4089 with evaluation. Here \mykant\ does not make bold moves, and simply
4090 employs substitution. When type checking we match types by reducing
4091 them to their wheak head normal form, as to avoid unnecessary evaluation.
4093 We treat data types eliminators and record projections in an uniform
4094 way, by elaborating declarations in a series of \emph{rewriting rules}:
4098 TmRef v -> -- Term to which the destructor is applied
4099 [TmRef v] -> -- List of other arguments
4100 -- The result of the rewriting, if the eliminator reduces.
4103 A rewriting rule is polymorphic in the variable type, guaranteeing that
4104 it just pattern matches on terms structure and rearranges them in some
4105 way, and making it possible to apply it at any level in the term. When
4106 reducing a series of applications we match the first term and check if
4107 it is a destructor, and if that's the case we apply the reduction rule
4108 and reduce further if it yields a new list of terms.
4110 This has the advantage of being very simple, but has the disadvantage of
4111 being quite poor in terms of performance and that we need to do
4112 quotation manually. An alternative that solves both of these is the
4113 already mentioned \emph{normalization by evaluation}, where we would
4114 compute by turning terms into Haskell values, and then reify back to
4115 terms to compare them---a useful tutorial on this technique is given by
4118 \subsubsection{Context}
4120 Given the parmetrised type,
4124 \subsection{Turning constraints into graphs}
4125 \label{sec:hier-impl}
4127 As an interlude from all the types, we will explain how to
4128 implement the typical ambiguity we have spoken about in
4129 \ref{sec:term-hierarchy} efficiently. As mentioned, we have to verify a the
4130 consistency of a set of constraints each time we add a new one. The
4131 constraints range over some set of variables whose members we will
4132 denote with $x, y, z, \dots$. and are of two kinds:
4139 Predictably, $\le$ expresses a reflexive order, and $<$ expresses an
4140 irreflexive order, both working with the same notion of equality, where
4141 $x < y$ implies $x \le y$---they behave like $\le$ and $<$ do on natural
4142 numbers (or in our case, levels in a type hierarchy). We also need an
4143 equality constraint ($x = y$), which can be reduced to two constraints
4144 $x \le y$ and $y \le x$.
4146 Given this specification, we have implemented a standalone Haskell
4147 module---that we plan to release as a standalone library---to
4148 efficiently store and check the consistency of constraints. The problem
4149 predictably reduces to a graph algorithm, and for this reason we also
4150 implement a library for labelled graphs, since the existing Haskell
4151 graph libraries fell short in different areas.\footnote{We tried the
4152 \texttt{Data.Graph} module in
4153 \url{http://hackage.haskell.org/package/containers}, and the much more
4154 featureful \texttt{fgl} library
4155 \url{http://hackage.haskell.org/package/fgl}.}. The interfaces for
4156 these modules are shown in Appendix \ref{app:constraint}. The graph
4157 library is implemented as a modification of the code described by
4160 We represent the set by building a graph where vertices are variables,
4161 and edges are constraints between them. The edges are labelled with the
4162 constraint type ($<$ or $\le$). As we add constraints, $\le$
4163 constraints are replaced by $<$ constraints, so that if we started with
4164 an empty set and added
4166 x \le y,\ y < z,\ z \le k,\ k \le j,\ x < y,\ j \le y
4168 it would generate the graph shown in Figure \ref{fig:graph-one}.
4174 \subsection{Type holes}
4175 \label{sec:type-holes}
4177 Type holes are, in the author's opinion, one of the `killer' features of
4178 interactive theorem provers, and one that is begging to be exported to
4179 the word of mainstream programming. The idea is that when we are
4180 developing a proof or a program we can insert a hole to have the
4181 software tell us the type expected at that point. Furthermore, we can
4182 ask for the type of variables in context, to better understand our
4187 \subsection{Web prompt}
4190 \section{Evaluation}
4192 \section{Future work}
4194 \subsection{Coinduction}
4196 \subsection{Quotient types}
4198 \subsection{Partiality}
4200 \subsection{Pattern matching}
4202 \subsection{Pattern unification}
4204 % TODO coinduction (obscoin, gimenez, jacobs), pattern unification (miller,
4205 % gundry), partiality monad (NAD)
4209 \section{Notation and syntax}
4211 Syntax, derivation rules, and reduction rules, are enclosed in frames describing
4212 the type of relation being established and the syntactic elements appearing,
4215 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
4216 Typing derivations here.
4219 In the languages presented and Agda code samples I also highlight the syntax,
4220 following a uniform color and font convention:
4223 \begin{tabular}{c | l}
4224 $\mytyc{Sans}$ & Type constructors. \\
4225 $\mydc{sans}$ & Data constructors. \\
4226 % $\myfld{sans}$ & Field accessors (e.g. \myfld{fst} and \myfld{snd} for products). \\
4227 $\mysyn{roman}$ & Keywords of the language. \\
4228 $\myfun{roman}$ & Defined values and destructors. \\
4229 $\myb{math}$ & Bound variables.
4233 Moreover, I will from time to time give examples in the Haskell programming
4234 language as defined in \citep{Haskell2010}, which I will typeset in
4235 \texttt{teletype} font. I assume that the reader is already familiar with
4236 Haskell, plenty of good introductions are available \citep{LYAH,ProgInHask}.
4238 When presenting grammars, I will use a word in $\mysynel{math}$ font
4239 (e.g. $\mytmsyn$ or $\mytysyn$) to indicate indicate
4240 nonterminals. Additionally, I will use quite flexibly a $\mysynel{math}$
4241 font to indicate a syntactic element in derivations or meta-operations.
4242 More specifically, terms are usually indicated by lowercase letters
4243 (often $\mytmt$, $\mytmm$, or $\mytmn$); and types by an uppercase
4244 letter (often $\mytya$, $\mytyb$, or $\mytycc$).
4246 When presenting type derivations, I will often abbreviate and present multiple
4247 conclusions, each on a separate line:
4249 \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
4250 \UnaryInfC{$\myjud{\myapp{\myfst}{\mytmt}}{\mytya}$}
4252 \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mytyb}$}
4255 I will often present `definitions' in the described calculi and in
4256 $\mykant$\ itself, like so:
4259 \myfun{name} : \mytysyn \\
4260 \myfun{name} \myappsp \myb{arg_1} \myappsp \myb{arg_2} \myappsp \cdots \mapsto \mytmsyn
4263 To define operators, I use a mixfix notation similar
4264 to Agda, where $\myarg$s denote arguments:
4267 \myarg \mathrel{\myfun{$\wedge$}} \myarg : \mybool \myarr \mybool \myarr \mybool \\
4268 \myb{b_1} \mathrel{\myfun{$\wedge$}} \myb{b_2} \mapsto \cdots
4272 In explicitly typed systems, I will also omit type annotations when they
4273 are obvious, e.g. by not annotating the type of parameters of
4274 abstractions or of dependent pairs.
4276 I will introduce multiple arguments in one go in arrow types:
4278 (\myb{x}\, \myb{y} {:} \mytya) \myarr \cdots = (\myb{x} {:} \mytya) \myarr (\myb{y} {:} \mytya) \myarr \cdots
4280 and in abstractions:
4282 \myabs{\myb{x}\myappsp\myb{y}}{\cdots} = \myabs{\myb{x}}{\myabs{\myb{y}}{\cdots}}
4284 I will also omit arrows to abbreviate types:
4286 (\myb{x} {:} \mytya)(\myb{y} {:} \mytyb) \myarr \cdots =
4287 (\myb{x} {:} \mytya) \myarr (\myb{y} {:} \mytyb) \myarr \cdots
4289 Meta operations names will be displayed in $\mymeta{smallcaps}$ and
4290 written in a pattern matching style, also making use of boolean guards.
4291 For example, a meta operation operating on a context and terms might
4295 \mymeta{quux}(\myctx, \myb{x}) \mymetaguard \myb{x} \in \myctx \mymetagoes \myctx(\myb{x}) \\
4296 \mymeta{quux}(\myctx, \myb{x}) \mymetagoes \mymeta{outofbounds} \\
4303 \subsection{ITT renditions}
4304 \label{app:itt-code}
4306 \subsubsection{Agda}
4307 \label{app:agda-itt}
4309 Note that in what follows rules for `base' types are
4310 universe-polymorphic, to reflect the exposition. Derived definitions,
4311 on the other hand, mostly work with \mytyc{Set}, reflecting the fact
4312 that in the theory presented we don't have universe polymorphism.
4318 data Empty : Set where
4320 absurd : ∀ {a} {A : Set a} → Empty → A
4323 ¬_ : ∀ {a} → (A : Set a) → Set a
4326 record Unit : Set where
4329 record _×_ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
4336 data Bool : Set where
4339 if_/_then_else_ : ∀ {a} (x : Bool) (P : Bool → Set a) → P true → P false → P x
4340 if true / _ then x else _ = x
4341 if false / _ then _ else x = x
4343 if_then_else_ : ∀ {a} (x : Bool) {P : Bool → Set a} → P true → P false → P x
4344 if_then_else_ x {P} = if_/_then_else_ x P
4346 data W {s p} (S : Set s) (P : S → Set p) : Set (s ⊔ p) where
4347 _◁_ : (s : S) → (P s → W S P) → W S P
4349 rec : ∀ {a b} {S : Set a} {P : S → Set b}
4350 (C : W S P → Set) → -- some conclusion we hope holds
4351 ((s : S) → -- given a shape...
4352 (f : P s → W S P) → -- ...and a bunch of kids...
4353 ((p : P s) → C (f p)) → -- ...and C for each kid in the bunch...
4354 C (s ◁ f)) → -- ...does C hold for the node?
4355 (x : W S P) → -- If so, ...
4356 C x -- ...C always holds.
4357 rec C c (s ◁ f) = c s f (λ p → rec C c (f p))
4359 module Examples-→ where
4366 -- These pragmas are needed so we can use number literals.
4367 {-# BUILTIN NATURAL ℕ #-}
4368 {-# BUILTIN ZERO zero #-}
4369 {-# BUILTIN SUC suc #-}
4371 data List (A : Set) : Set where
4373 _∷_ : A → List A → List A
4375 length : ∀ {A} → List A → ℕ
4377 length (_ ∷ l) = suc (length l)
4382 suc x > suc y = x > y
4384 head : ∀ {A} → (l : List A) → length l > 0 → A
4385 head [] p = absurd p
4388 module Examples-× where
4394 even (suc zero) = Empty
4395 even (suc (suc n)) = even n
4400 5-not-even : ¬ (even 5)
4403 there-is-an-even-number : ℕ × even
4404 there-is-an-even-number = 6 , 6-even
4406 _∨_ : (A B : Set) → Set
4407 A ∨ B = Bool × (λ b → if b then A else B)
4409 left : ∀ {A B} → A → A ∨ B
4412 right : ∀ {A B} → B → A ∨ B
4415 [_,_] : {A B C : Set} → (A → C) → (B → C) → A ∨ B → C
4417 (if (fst x) / (λ b → if b then _ else _ → _) then f else g) (snd x)
4419 module Examples-W where
4424 Tr b = if b then Unit else Empty
4430 zero = false ◁ absurd
4433 suc n = true ◁ (λ _ → n)
4439 if b / (λ b → (Tr b → ℕ) → (Tr b → ℕ) → ℕ)
4440 then (λ _ f → (suc (f tt))) else (λ _ _ → y))
4443 module Equality where
4446 data _≡_ {a} {A : Set a} : A → A → Set a where
4449 ≡-elim : ∀ {a b} {A : Set a}
4450 (P : (x y : A) → x ≡ y → Set b) →
4451 ∀ {x y} → P x x (refl x) → (x≡y : x ≡ y) → P x y x≡y
4452 ≡-elim P p (refl x) = p
4454 subst : ∀ {A : Set} (P : A → Set) → ∀ {x y} → (x≡y : x ≡ y) → P x → P y
4455 subst P x≡y p = ≡-elim (λ _ y _ → P y) p x≡y
4457 sym : ∀ {A : Set} (x y : A) → x ≡ y → y ≡ x
4458 sym x y p = subst (λ y′ → y′ ≡ x) p (refl x)
4460 trans : ∀ {A : Set} (x y z : A) → x ≡ y → y ≡ z → x ≡ z
4461 trans x y z p q = subst (λ z′ → x ≡ z′) q p
4463 cong : ∀ {A B : Set} (x y : A) → x ≡ y → (f : A → B) → f x ≡ f y
4464 cong x y p f = subst (λ z → f x ≡ f z) p (refl (f x))
4467 \subsubsection{\mykant}
4468 \label{app:kant-itt}
4470 The following things are missing: $\mytyc{W}$-types, since our
4471 positivity check is overly strict, and equality, since we haven't
4472 implemented that yet.
4475 \verbatiminput{itt.ka}
4478 \subsection{\mykant\ examples}
4479 \label{app:kant-examples}
4482 \verbatiminput{examples.ka}
4485 \subsection{\mykant' hierachy}
4488 This rendition of the Hurken's paradox does not type check with the
4489 hierachy enabled, type checks and loops without it. Adapted from an
4490 Agda version, available at
4491 \url{http://code.haskell.org/Agda/test/succeed/Hurkens.agda}.
4494 \verbatiminput{hurkens.ka}
4497 \subsection{Term representation}
4500 Data type for terms in \mykant.
4502 {\small\begin{verbatim}-- A top-level name.
4504 -- A data/type constructor name.
4507 -- A term, parametrised over the variable (`v') and over the reference
4508 -- type used in the type hierarchy (`r').
4511 | Ty r -- Type, with a hierarchy reference.
4512 | Lam (TmScope r v) -- Abstraction.
4513 | Arr (Tm r v) (TmScope r v) -- Dependent function.
4514 | App (Tm r v) (Tm r v) -- Application.
4515 | Ann (Tm r v) (Tm r v) -- Annotated term.
4516 -- Data constructor, the first ConId is the type constructor and
4517 -- the second is the data constructor.
4518 | Con ADTRec ConId ConId [Tm r v]
4519 -- Data destrutor, again first ConId being the type constructor
4520 -- and the second the name of the eliminator.
4521 | Destr ADTRec ConId Id (Tm r v)
4523 | Hole HoleId [Tm r v]
4524 -- Decoding of propositions.
4528 | Prop r -- The type of proofs, with hierarchy reference.
4531 | And (Tm r v) (Tm r v)
4532 | Forall (Tm r v) (TmScope r v)
4533 -- Heterogeneous equality.
4534 | Eq (Tm r v) (Tm r v) (Tm r v) (Tm r v)
4536 -- Either a data type, or a record.
4537 data ADTRec = ADT | Rec
4539 -- Either a coercion, or coherence.
4540 data Coeh = Coe | Coh\end{verbatim}
4543 \subsection{Graph and constraints modules}
4544 \label{app:constraint}
4546 The modules are respectively named \texttt{Data.LGraph} (short for
4547 `labelled graph'), and \texttt{Data.Constraint}. The type class
4548 constraints on the type parameters are not shown for clarity, unless
4549 they are meaningful to the function. In practice we use the
4550 \texttt{Hashable} type class on the vertex to implement the graph
4551 efficiently with hash maps.
4553 \subsubsection{\texttt{Data.LGraph}}
4556 \verbatiminput{graph.hs}
4559 \subsubsection{\texttt{Data.Constraint}}
4562 \verbatiminput{constraint.hs}
4567 \bibliographystyle{authordate1}
4568 \bibliography{thesis}