1 \documentclass[report, 11pt]{article}
4 \usepackage[sc,slantedGreek]{mathpazo}
17 % \usepackage{fullpage}
29 \usepackage[fleqn]{amsmath}
30 \usepackage{stmaryrd} %llbracket
33 \usepackage{bussproofs}
45 \usepackage{subcaption}
51 \usetikzlibrary{shapes,arrows,positioning}
52 % \usepackage{tikz-cd}
53 % \usepackage{pgfplots}
56 %% -----------------------------------------------------------------------------
58 \usepackage[english]{babel}
59 \usepackage[conor]{agda}
60 \renewcommand{\AgdaKeywordFontStyle}[1]{\ensuremath{\mathrm{\underline{#1}}}}
61 \renewcommand{\AgdaFunction}[1]{\textbf{\textcolor{AgdaFunction}{#1}}}
62 \renewcommand{\AgdaField}{\AgdaFunction}
63 % \definecolor{AgdaBound} {HTML}{000000}
64 \definecolor{AgdaHole} {HTML} {FFFF33}
66 \DeclareUnicodeCharacter{9665}{\ensuremath{\lhd}}
67 \DeclareUnicodeCharacter{964}{\ensuremath{\tau}}
68 \DeclareUnicodeCharacter{963}{\ensuremath{\sigma}}
69 \DeclareUnicodeCharacter{915}{\ensuremath{\Gamma}}
70 \DeclareUnicodeCharacter{8799}{\ensuremath{\stackrel{?}{=}}}
71 \DeclareUnicodeCharacter{9655}{\ensuremath{\rhd}}
73 \renewenvironment{code}%
74 {\noindent\ignorespaces\advance\leftskip\mathindent\AgdaCodeStyle\pboxed\small}%
75 {\endpboxed\par\noindent%
76 \ignorespacesafterend\small}
79 %% -----------------------------------------------------------------------------
82 \newcommand{\mysmall}{}
83 \newcommand{\mysyn}{\AgdaKeyword}
84 \newcommand{\mytyc}{\AgdaDatatype}
85 \newcommand{\mydc}{\AgdaInductiveConstructor}
86 \newcommand{\myfld}{\AgdaField}
87 \newcommand{\myfun}{\AgdaFunction}
88 \newcommand{\myb}[1]{\AgdaBound{$#1$}}
89 \newcommand{\myfield}{\AgdaField}
90 \newcommand{\myind}{\AgdaIndent}
91 \newcommand{\mykant}{\textsc{Kant}}
92 \newcommand{\mysynel}[1]{#1}
93 \newcommand{\myse}{\mysynel}
94 \newcommand{\mytmsyn}{\mysynel{term}}
95 \newcommand{\mysp}{\ }
96 \newcommand{\myabs}[2]{\mydc{$\lambda$} #1 \mathrel{\mydc{$\mapsto$}} #2}
97 \newcommand{\myappsp}{\hspace{0.07cm}}
98 \newcommand{\myapp}[2]{#1 \myappsp #2}
99 \newcommand{\mysynsep}{\ \ |\ \ }
100 \newcommand{\myITE}[3]{\myfun{If}\, #1\, \myfun{Then}\, #2\, \myfun{Else}\, #3}
101 \newcommand{\mycumul}{\preceq}
104 \newcommand{\mydesc}[3]{
110 \hfill \textbf{#1} $#2$
111 \framebox[\textwidth]{
126 \newcommand{\mytmt}{\mysynel{t}}
127 \newcommand{\mytmm}{\mysynel{m}}
128 \newcommand{\mytmn}{\mysynel{n}}
129 \newcommand{\myred}{\leadsto}
130 \newcommand{\mysub}[3]{#1[#2 / #3]}
131 \newcommand{\mytysyn}{\mysynel{type}}
132 \newcommand{\mybasetys}{K}
133 \newcommand{\mybasety}[1]{B_{#1}}
134 \newcommand{\mytya}{\myse{A}}
135 \newcommand{\mytyb}{\myse{B}}
136 \newcommand{\mytycc}{\myse{C}}
137 \newcommand{\myarr}{\mathrel{\textcolor{AgdaDatatype}{\to}}}
138 \newcommand{\myprod}{\mathrel{\textcolor{AgdaDatatype}{\times}}}
139 \newcommand{\myctx}{\Gamma}
140 \newcommand{\myvalid}[1]{#1 \vdash \underline{\mathrm{valid}}}
141 \newcommand{\myjudd}[3]{#1 \vdash #2 : #3}
142 \newcommand{\myjud}[2]{\myjudd{\myctx}{#1}{#2}}
143 \newcommand{\myabss}[3]{\mydc{$\lambda$} #1 {:} #2 \mathrel{\mydc{$\mapsto$}} #3}
144 \newcommand{\mytt}{\mydc{$\langle\rangle$}}
145 \newcommand{\myunit}{\mytyc{Unit}}
146 \newcommand{\mypair}[2]{\mathopen{\mydc{$\langle$}}#1\mathpunct{\mydc{,}} #2\mathclose{\mydc{$\rangle$}}}
147 \newcommand{\myfst}{\myfld{fst}}
148 \newcommand{\mysnd}{\myfld{snd}}
149 \newcommand{\myconst}{\myse{c}}
150 \newcommand{\myemptyctx}{\cdot}
151 \newcommand{\myhole}{\AgdaHole}
152 \newcommand{\myfix}[3]{\mysyn{fix} \myappsp #1 {:} #2 \mapsto #3}
153 \newcommand{\mysum}{\mathbin{\textcolor{AgdaDatatype}{+}}}
154 \newcommand{\myleft}[1]{\mydc{left}_{#1}}
155 \newcommand{\myright}[1]{\mydc{right}_{#1}}
156 \newcommand{\myempty}{\mytyc{Empty}}
157 \newcommand{\mycase}[2]{\mathopen{\myfun{[}}#1\mathpunct{\myfun{,}} #2 \mathclose{\myfun{]}}}
158 \newcommand{\myabsurd}[1]{\myfun{absurd}_{#1}}
159 \newcommand{\myarg}{\_}
160 \newcommand{\myderivsp}{}
161 \newcommand{\myderivspp}{\vspace{0.3cm}}
162 \newcommand{\mytyp}{\mytyc{Type}}
163 \newcommand{\myneg}{\myfun{$\neg$}}
164 \newcommand{\myar}{\,}
165 \newcommand{\mybool}{\mytyc{Bool}}
166 \newcommand{\mytrue}{\mydc{true}}
167 \newcommand{\myfalse}{\mydc{false}}
168 \newcommand{\myitee}[5]{\myfun{if}\,#1 / {#2.#3}\,\myfun{then}\,#4\,\myfun{else}\,#5}
169 \newcommand{\mynat}{\mytyc{$\mathbb{N}$}}
170 \newcommand{\myrat}{\mytyc{$\mathbb{R}$}}
171 \newcommand{\myite}[3]{\myfun{if}\,#1\,\myfun{then}\,#2\,\myfun{else}\,#3}
172 \newcommand{\myfora}[3]{(#1 {:} #2) \myarr #3}
173 \newcommand{\myexi}[3]{(#1 {:} #2) \myprod #3}
174 \newcommand{\mypairr}[4]{\mathopen{\mydc{$\langle$}}#1\mathpunct{\mydc{,}} #4\mathclose{\mydc{$\rangle$}}_{#2{.}#3}}
175 \newcommand{\mylist}{\mytyc{List}}
176 \newcommand{\mynil}[1]{\mydc{[]}_{#1}}
177 \newcommand{\mycons}{\mathbin{\mydc{∷}}}
178 \newcommand{\myfoldr}{\myfun{foldr}}
179 \newcommand{\myw}[3]{\myapp{\myapp{\mytyc{W}}{(#1 {:} #2)}}{#3}}
180 \newcommand{\mynodee}{\mathbin{\mydc{$\lhd$}}}
181 \newcommand{\mynode}[2]{\mynodee_{#1.#2}}
182 \newcommand{\myrec}[4]{\myfun{rec}\,#1 / {#2.#3}\,\myfun{with}\,#4}
183 \newcommand{\mylub}{\sqcup}
184 \newcommand{\mydefeq}{\cong}
185 \newcommand{\myrefl}{\mydc{refl}}
186 \newcommand{\mypeq}[1]{\mathrel{\mytyc{=}_{#1}}}
187 \newcommand{\myjeqq}{\myfun{$=$-elim}}
188 \newcommand{\myjeq}[3]{\myapp{\myapp{\myapp{\myjeqq}{#1}}{#2}}{#3}}
189 \newcommand{\mysubst}{\myfun{subst}}
190 \newcommand{\myprsyn}{\myse{prop}}
191 \newcommand{\myprdec}[1]{\mathopen{\mytyc{$\llbracket$}} #1 \mathclose{\mytyc{$\rrbracket$}}}
192 \newcommand{\myand}{\mathrel{\mytyc{$\wedge$}}}
193 \newcommand{\mybigand}{\mathrel{\mytyc{$\bigwedge$}}}
194 \newcommand{\myprfora}[3]{\forall #1 {:} #2. #3}
195 \newcommand{\myimpl}{\mathrel{\mytyc{$\Rightarrow$}}}
196 \newcommand{\mybot}{\mytyc{$\bot$}}
197 \newcommand{\mytop}{\mytyc{$\top$}}
198 \newcommand{\mycoe}{\myfun{coe}}
199 \newcommand{\mycoee}[4]{\myapp{\myapp{\myapp{\myapp{\mycoe}{#1}}{#2}}{#3}}{#4}}
200 \newcommand{\mycoh}{\myfun{coh}}
201 \newcommand{\mycohh}[4]{\myapp{\myapp{\myapp{\myapp{\mycoh}{#1}}{#2}}{#3}}{#4}}
202 \newcommand{\myjm}[4]{(#1 {:} #2) \mathrel{\mytyc{=}} (#3 {:} #4)}
203 \newcommand{\myeq}{\mathrel{\mytyc{=}}}
204 \newcommand{\myprop}{\mytyc{Prop}}
205 \newcommand{\mytmup}{\mytmsyn\uparrow}
206 \newcommand{\mydefs}{\Delta}
207 \newcommand{\mynf}{\Downarrow}
208 \newcommand{\myinff}[3]{#1 \vdash #2 \Rightarrow #3}
209 \newcommand{\myinf}[2]{\myinff{\myctx}{#1}{#2}}
210 \newcommand{\mychkk}[3]{#1 \vdash #2 \Leftarrow #3}
211 \newcommand{\mychk}[2]{\mychkk{\myctx}{#1}{#2}}
212 \newcommand{\myann}[2]{#1 : #2}
213 \newcommand{\mydeclsyn}{\myse{decl}}
214 \newcommand{\myval}[3]{#1 : #2 \mapsto #3}
215 \newcommand{\mypost}[2]{\mysyn{abstract}\ #1 : #2}
216 \newcommand{\myadt}[4]{\mysyn{data}\ #1 #2\ \mysyn{where}\ #3\{ #4 \}}
217 \newcommand{\myreco}[4]{\mysyn{record}\ #1 #2\ \mysyn{where}\ \{ #4 \}}
218 \newcommand{\myelabt}{\vdash}
219 \newcommand{\myelabf}{\rhd}
220 \newcommand{\myelab}[2]{\myctx \myelabt #1 \myelabf #2}
221 \newcommand{\mytele}{\Delta}
222 \newcommand{\mytelee}{\delta}
223 \newcommand{\mydcctx}{\Gamma}
224 \newcommand{\mynamesyn}{\myse{name}}
225 \newcommand{\myvec}{\overrightarrow}
226 \newcommand{\mymeta}{\textsc}
227 \newcommand{\myhyps}{\mymeta{hyps}}
228 \newcommand{\mycc}{;}
229 \newcommand{\myemptytele}{\cdot}
230 \newcommand{\mymetagoes}{\Longrightarrow}
231 % \newcommand{\mytesctx}{\
232 \newcommand{\mytelesyn}{\myse{telescope}}
233 \newcommand{\myrecs}{\mymeta{recs}}
234 \newcommand{\myle}{\mathrel{\lcfun{$\le$}}}
235 \newcommand{\mylet}{\mysyn{let}}
236 \newcommand{\myhead}{\mymeta{head}}
237 \newcommand{\mytake}{\mymeta{take}}
238 \newcommand{\myix}{\mymeta{ix}}
239 \newcommand{\myapply}{\mymeta{apply}}
240 \newcommand{\mydataty}{\mymeta{datatype}}
241 \newcommand{\myisreco}{\mymeta{record}}
242 \newcommand{\mydcsep}{\ |\ }
243 \newcommand{\mytree}{\mytyc{Tree}}
244 \newcommand{\myproj}[1]{\myfun{$\pi_{#1}$}}
245 \newcommand{\mysigma}{\mytyc{$\Sigma$}}
246 \newcommand{\mynegder}{\vspace{-0.3cm}}
247 \newcommand{\myquot}{\Downarrow}
250 %% -----------------------------------------------------------------------------
252 \title{\mykant: Implementing Observational Equality}
253 \author{Francesco Mazzoli \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{<fm2209@ic.ac.uk>}}}
268 \thispagestyle{empty}
270 \begin{minipage}{0.4\textwidth}
271 \begin{flushleft} \large
273 Dr. Steffen \textsc{van Backel}
276 \begin{minipage}{0.4\textwidth}
277 \begin{flushright} \large
279 Dr. Philippa \textsc{Gardner}
286 The marriage between programming and logic has been a very fertile one. In
287 particular, since the simply typed lambda calculus (STLC), a number of type
288 systems have been devised with increasing expressive power.
290 Among this systems, Inutitionistic Type Theory (ITT) has been a very
291 popular framework for theorem provers and programming languages.
292 However, equality has always been a tricky business in ITT and related
295 In these thesis we will explain why this is the case, and present
296 Observational Type Theory (OTT), a solution to some of the problems
297 with equality. We then describe $\mykant$, a theorem prover featuring
298 OTT in a setting more close to the one found in current systems.
299 Having implemented part of $\mykant$ as a Haskell program, we describe
300 some of the implementation issues faced.
305 \renewcommand{\abstractname}{Acknowledgements}
307 I would like to thank Steffen van Backel, my supervisor, who was brave
308 enough to believe in my project and who provided much advice and
311 I would also like to thank the Haskell and Agda community on
312 \texttt{IRC}, which guided me through the strange world of types; and
313 in particular Andrea Vezzosi and James Deikun, with whom I entertained
314 countless insightful discussions in the past year. Andrea suggested
315 Observational Type Theory as a topic of study: this thesis would not
316 exist without him. Before them, Tony Fields introduced me to Haskell,
317 unknowingly filling most of my free time from that time on.
319 Finally, much of the work stems from the research of Conor McBride,
320 who answered many of my doubts through these months. I also owe him
330 \section{Simple and not-so-simple types}
333 \subsection{The untyped $\lambda$-calculus}
335 Along with Turing's machines, the earliest attempts to formalise computation
336 lead to the $\lambda$-calculus \citep{Church1936}. This early programming
337 language encodes computation with a minimal syntax and no `data' in the
338 traditional sense, but just functions. Here we give a brief overview of the
339 language, which will give the chance to introduce concepts central to the
340 analysis of all the following calculi. The exposition follows the one found in
341 chapter 5 of \cite{Queinnec2003}.
343 The syntax of $\lambda$-terms consists of three things: variables, abstractions,
348 \begin{array}{r@{\ }c@{\ }l}
349 \mytmsyn & ::= & \myb{x} \mysynsep \myabs{\myb{x}}{\mytmsyn} \mysynsep (\myapp{\mytmsyn}{\mytmsyn}) \\
350 x & \in & \text{Some enumerable set of symbols}
355 Parenthesis will be omitted in the usual way:
356 $\myapp{\myapp{\mytmt}{\mytmm}}{\mytmn} =
357 \myapp{(\myapp{\mytmt}{\mytmm})}{\mytmn}$.
359 Abstractions roughly corresponds to functions, and their semantics is more
360 formally explained by the $\beta$-reduction rule:
362 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
365 \myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{\myb{x}}{\mytmn}\text{, where} \\
367 \begin{array}{l@{\ }c@{\ }l}
368 \mysub{\myb{x}}{\myb{x}}{\mytmn} & = & \mytmn \\
369 \mysub{\myb{y}}{\myb{x}}{\mytmn} & = & y\text{, with } \myb{x} \neq y \\
370 \mysub{(\myapp{\mytmt}{\mytmm})}{\myb{x}}{\mytmn} & = & (\myapp{\mysub{\mytmt}{\myb{x}}{\mytmn}}{\mysub{\mytmm}{\myb{x}}{\mytmn}}) \\
371 \mysub{(\myabs{\myb{x}}{\mytmm})}{\myb{x}}{\mytmn} & = & \myabs{\myb{x}}{\mytmm} \\
372 \mysub{(\myabs{\myb{y}}{\mytmm})}{\myb{x}}{\mytmn} & = & \myabs{\myb{z}}{\mysub{\mysub{\mytmm}{\myb{y}}{\myb{z}}}{\myb{x}}{\mytmn}}, \\
373 \multicolumn{3}{l}{\myind{2} \text{with $\myb{x} \neq \myb{y}$ and $\myb{z}$ not free in $\myapp{\mytmm}{\mytmn}$}}
379 The care required during substituting variables for terms is required to avoid
380 name capturing. We will use substitution in the future for other name-binding
381 constructs assuming similar precautions.
383 These few elements are of remarkable expressiveness, and in fact Turing
384 complete. As a corollary, we must be able to devise a term that reduces forever
385 (`loops' in imperative terms):
388 (\myapp{\omega}{\omega}) \myred (\myapp{\omega}{\omega}) \myred \cdots \text{, with $\omega = \myabs{x}{\myapp{x}{x}}$}
391 A \emph{redex} is a term that can be reduced. In the untyped $\lambda$-calculus
392 this will be the case for an application in which the first term is an
393 abstraction, but in general we call aterm reducible if it appears to the left of
394 a reduction rule. When a term contains no redexes it's said to be in
395 \emph{normal form}. Given the observation above, not all terms reduce to a
396 normal forms: we call the ones that do \emph{normalising}, and the ones that
397 don't \emph{non-normalising}.
399 The reduction rule presented is not syntax directed, but \emph{evaluation
400 strategies} can be employed to reduce term systematically. Common evaluation
401 strategies include \emph{call by value} (or \emph{strict}), where arguments of
402 abstractions are reduced before being applied to the abstraction; and conversely
403 \emph{call by name} (or \emph{lazy}), where we reduce only when we need to do so
404 to proceed---in other words when we have an application where the function is
405 still not a $\lambda$. In both these reduction strategies we never reduce under
406 an abstraction: for this reason a weaker form of normalisation is used, where
407 both abstractions and normal forms are said to be in \emph{weak head normal
410 \subsection{The simply typed $\lambda$-calculus}
412 A convenient way to `discipline' and reason about $\lambda$-terms is to assign
413 \emph{types} to them, and then check that the terms that we are forming make
414 sense given our typing rules \citep{Curry1934}. The first most basic instance
415 of this idea takes the name of \emph{simply typed $\lambda$ calculus}, whose
416 rules are shown in figure \ref{fig:stlc}.
418 Our types contain a set of \emph{type variables} $\Phi$, which might
419 correspond to some `primitive' types; and $\myarr$, the type former for
420 `arrow' types, the types of functions. The language is explicitly
421 typed: when we bring a variable into scope with an abstraction, we
422 declare its type. Reduction is unchanged from the untyped
428 \begin{array}{r@{\ }c@{\ }l}
429 \mytmsyn & ::= & \myb{x} \mysynsep \myabss{\myb{x}}{\mytysyn}{\mytmsyn} \mysynsep
430 (\myapp{\mytmsyn}{\mytmsyn}) \\
431 \mytysyn & ::= & \myse{\phi} \mysynsep \mytysyn \myarr \mytysyn \mysynsep \\
432 \myb{x} & \in & \text{Some enumerable set of symbols} \\
433 \myse{\phi} & \in & \Phi
438 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
440 \AxiomC{$\myctx(x) = A$}
441 \UnaryInfC{$\myjud{\myb{x}}{A}$}
444 \AxiomC{$\myjudd{\myctx;\myb{x} : A}{\mytmt}{\mytyb}$}
445 \UnaryInfC{$\myjud{\myabss{x}{A}{\mytmt}}{\mytyb}$}
448 \AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$}
449 \AxiomC{$\myjud{\mytmn}{\mytya}$}
450 \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mytyb}$}
454 \caption{Syntax and typing rules for the STLC. Reduction is unchanged from
455 the untyped $\lambda$-calculus.}
459 In the typing rules, a context $\myctx$ is used to store the types of bound
460 variables: $\myctx; \myb{x} : \mytya$ adds a variable to the context and
461 $\myctx(x)$ returns the type of the rightmost occurrence of $x$.
463 This typing system takes the name of `simply typed lambda calculus' (STLC), and
464 enjoys a number of properties. Two of them are expected in most type systems
467 \item[Progress] A well-typed term is not stuck---it is either a variable, or its
468 constructor does not appear on the left of the $\myred$ relation (currently
469 only $\lambda$), or it can take a step according to the evaluation rules.
470 \item[Preservation] If a well-typed term takes a step of evaluation, then the
471 resulting term is also well-typed, and preserves the previous type. Also
472 known as \emph{subject reduction}.
475 However, STLC buys us much more: every well-typed term is normalising
476 \citep{Tait1967}. It is easy to see that we can't fill the blanks if we want to
477 give types to the non-normalising term shown before:
479 \myapp{(\myabss{\myb{x}}{\myhole{?}}{\myapp{\myb{x}}{\myb{x}}})}{(\myabss{\myb{x}}{\myhole{?}}{\myapp{\myb{x}}{\myb{x}}})}
482 This makes the STLC Turing incomplete. We can recover the ability to loop by
483 adding a combinator that recurses:
486 \begin{minipage}{0.5\textwidth}
488 $ \mytmsyn ::= \cdots b \mysynsep \myfix{\myb{x}}{\mytysyn}{\mytmsyn} $
492 \begin{minipage}{0.5\textwidth}
493 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}} {
494 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytmt}{\mytya}$}
495 \UnaryInfC{$\myjud{\myfix{\myb{x}}{\mytya}{\mytmt}}{\mytya}$}
500 \mydesc{reduction:}{\myjud{\mytmsyn}{\mytmsyn}}{
501 $ \myfix{\myb{x}}{\mytya}{\mytmt} \myred \mysub{\mytmt}{\myb{x}}{(\myfix{\myb{x}}{\mytya}{\mytmt})}$
504 This will deprive us of normalisation, which is a particularly bad thing if we
505 want to use the STLC as described in the next section.
507 \subsection{The Curry-Howard correspondence}
509 It turns out that the STLC can be seen a natural deduction system for
510 intuitionistic propositional logic. Terms are proofs, and their types are the
511 propositions they prove. This remarkable fact is known as the Curry-Howard
512 correspondence, or isomorphism.
514 The arrow ($\myarr$) type corresponds to implication. If we wish to prove that
515 that $(\mytya \myarr \mytyb) \myarr (\mytyb \myarr \mytycc) \myarr (\mytya
516 \myarr \mytycc)$, all we need to do is to devise a $\lambda$-term that has the
519 \myabss{\myb{f}}{(\mytya \myarr \mytyb)}{\myabss{\myb{g}}{(\mytyb \myarr \mytycc)}{\myabss{\myb{x}}{\mytya}{\myapp{\myb{g}}{(\myapp{\myb{f}}{\myb{x}})}}}}
521 That is, function composition. Going beyond arrow types, we can extend our bare
522 lambda calculus with useful types to represent other logical constructs, as
523 shown in figure \ref{fig:natded}.
528 \begin{array}{r@{\ }c@{\ }l}
529 \mytmsyn & ::= & \cdots \\
530 & | & \mytt \mysynsep \myapp{\myabsurd{\mytysyn}}{\mytmsyn} \\
531 & | & \myapp{\myleft{\mytysyn}}{\mytmsyn} \mysynsep
532 \myapp{\myright{\mytysyn}}{\mytmsyn} \mysynsep
533 \myapp{\mycase{\mytmsyn}{\mytmsyn}}{\mytmsyn} \\
534 & | & \mypair{\mytmsyn}{\mytmsyn} \mysynsep
535 \myapp{\myfst}{\mytmsyn} \mysynsep \myapp{\mysnd}{\mytmsyn} \\
536 \mytysyn & ::= & \cdots \mysynsep \myunit \mysynsep \myempty \mysynsep \mytmsyn \mysum \mytmsyn \mysynsep \mytysyn \myprod \mytysyn
541 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
544 \begin{array}{l@{ }l@{\ }c@{\ }l}
545 \myapp{\mycase{\mytmm}{\mytmn}}{(\myapp{\myleft{\mytya} &}{\mytmt})} & \myred &
546 \myapp{\mytmm}{\mytmt} \\
547 \myapp{\mycase{\mytmm}{\mytmn}}{(\myapp{\myright{\mytya} &}{\mytmt})} & \myred &
548 \myapp{\mytmn}{\mytmt}
553 \begin{array}{l@{ }l@{\ }c@{\ }l}
554 \myapp{\myfst &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmm \\
555 \myapp{\mysnd &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmn
561 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
563 \AxiomC{\phantom{$\myjud{\mytmt}{\myempty}$}}
564 \UnaryInfC{$\myjud{\mytt}{\myunit}$}
567 \AxiomC{$\myjud{\mytmt}{\myempty}$}
568 \UnaryInfC{$\myjud{\myapp{\myabsurd{\mytya}}{\mytmt}}{\mytya}$}
575 \AxiomC{$\myjud{\mytmt}{\mytya}$}
576 \UnaryInfC{$\myjud{\myapp{\myleft{\mytyb}}{\mytmt}}{\mytya \mysum \mytyb}$}
579 \AxiomC{$\myjud{\mytmt}{\mytyb}$}
580 \UnaryInfC{$\myjud{\myapp{\myright{\mytya}}{\mytmt}}{\mytya \mysum \mytyb}$}
588 \AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$}
589 \AxiomC{$\myjud{\mytmn}{\mytya \myarr \mytycc}$}
590 \AxiomC{$\myjud{\mytmt}{\mytya \mysum \mytyb}$}
591 \TrinaryInfC{$\myjud{\myapp{\mycase{\mytmm}{\mytmn}}{\mytmt}}{\mytycc}$}
598 \AxiomC{$\myjud{\mytmm}{\mytya}$}
599 \AxiomC{$\myjud{\mytmn}{\mytyb}$}
600 \BinaryInfC{$\myjud{\mypair{\mytmm}{\mytmn}}{\mytya \myprod \mytyb}$}
603 \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
604 \UnaryInfC{$\myjud{\myapp{\myfst}{\mytmt}}{\mytya}$}
607 \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
608 \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mytyb}$}
612 \caption{Rules for the extendend STLC. Only the new features are shown, all the
613 rules and syntax for the STLC apply here too.}
617 Tagged unions (or sums, or coproducts---$\mysum$ here, \texttt{Either}
618 in Haskell) correspond to disjunctions, and dually tuples (or pairs, or
619 products---$\myprod$ here, tuples in Haskell) correspond to
620 conjunctions. This is apparent looking at the ways to construct and
621 destruct the values inhabiting those types: for $\mysum$ $\myleft{ }$
622 and $\myright{ }$ correspond to $\vee$ introduction, and
623 $\mycase{\myarg}{\myarg}$ to $\vee$ elimination; for $\myprod$
624 $\mypair{\myarg}{\myarg}$ corresponds to $\wedge$ introduction, $\myfst$
625 and $\mysnd$ to $\wedge$ elimination.
627 The trivial type $\myunit$ corresponds to the logical $\top$, and dually
628 $\myempty$ corresponds to the logical $\bot$. $\myunit$ has one introduction
629 rule ($\mytt$), and thus one inhabitant; and no eliminators. $\myempty$ has no
630 introduction rules, and thus no inhabitants; and one eliminator ($\myabsurd{
631 }$), corresponding to the logical \emph{ex falso quodlibet}.
633 With these rules, our STLC now looks remarkably similar in power and use to the
634 natural deduction we already know. $\myneg \mytya$ can be expressed as $\mytya
635 \myarr \myempty$. However, there is an important omission: there is no term of
636 the type $\mytya \mysum \myneg \mytya$ (excluded middle), or equivalently
637 $\myneg \myneg \mytya \myarr \mytya$ (double negation), or indeed any term with
638 a type equivalent to those.
640 This has a considerable effect on our logic and it's no coincidence, since there
641 is no obvious computational behaviour for laws like the excluded middle.
642 Theories of this kind are called \emph{intuitionistic}, or \emph{constructive},
643 and all the systems analysed will have this characteristic since they build on
644 the foundation of the STLC\footnote{There is research to give computational
645 behaviour to classical logic, but I will not touch those subjects.}.
647 As in logic, if we want to keep our system consistent, we must make sure that no
648 closed terms (in other words terms not under a $\lambda$) inhabit $\myempty$.
649 The variant of STLC presented here is indeed
650 consistent, a result that follows from the fact that it is
652 Going back to our $\mysyn{fix}$ combinator, it is easy to see how it ruins our
653 desire for consistency. The following term works for every type $\mytya$,
656 (\myfix{\myb{x}}{\mytya}{\myb{x}}) : \mytya
659 \subsection{Inductive data}
662 To make the STLC more useful as a programming language or reasoning tool it is
663 common to include (or let the user define) inductive data types. These comprise
664 of a type former, various constructors, and an eliminator (or destructor) that
665 serves as primitive recursor.
667 For example, we might add a $\mylist$ type constructor, along with an `empty
668 list' ($\mynil{ }$) and `cons cell' ($\mycons$) constructor. The eliminator for
669 lists will be the usual folding operation ($\myfoldr$). See figure
675 \begin{array}{r@{\ }c@{\ }l}
676 \mytmsyn & ::= & \cdots \mysynsep \mynil{\mytysyn} \mysynsep \mytmsyn \mycons \mytmsyn
678 \myapp{\myapp{\myapp{\myfoldr}{\mytmsyn}}{\mytmsyn}}{\mytmsyn} \\
679 \mytysyn & ::= & \cdots \mysynsep \myapp{\mylist}{\mytysyn}
683 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
685 \begin{array}{l@{\ }c@{\ }l}
686 \myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{\mynil{\mytya}} & \myred & \mytmt \\
688 \myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{(\mytmm \mycons \mytmn)} & \myred &
689 \myapp{\myapp{\myse{f}}{\mytmm}}{(\myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{\mytmn})}
693 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
695 \AxiomC{\phantom{$\myjud{\mytmm}{\mytya}$}}
696 \UnaryInfC{$\myjud{\mynil{\mytya}}{\myapp{\mylist}{\mytya}}$}
699 \AxiomC{$\myjud{\mytmm}{\mytya}$}
700 \AxiomC{$\myjud{\mytmn}{\myapp{\mylist}{\mytya}}$}
701 \BinaryInfC{$\myjud{\mytmm \mycons \mytmn}{\myapp{\mylist}{\mytya}}$}
706 \AxiomC{$\myjud{\mysynel{f}}{\mytya \myarr \mytyb \myarr \mytyb}$}
707 \AxiomC{$\myjud{\mytmm}{\mytyb}$}
708 \AxiomC{$\myjud{\mytmn}{\myapp{\mylist}{\mytya}}$}
709 \TrinaryInfC{$\myjud{\myapp{\myapp{\myapp{\myfoldr}{\mysynel{f}}}{\mytmm}}{\mytmn}}{\mytyb}$}
712 \caption{Rules for lists in the STLC.}
716 In section \ref{sec:well-order} we will see how to give a general account of
719 \section{Intuitionistic Type Theory}
722 \subsection{Extending the STLC}
724 The STLC can be made more expressive in various ways. \cite{Barendregt1991}
725 succinctly expressed geometrically how we can add expressivity:
729 & \lambda\omega \ar@{-}[rr]\ar@{-}'[d][dd]
730 & & \lambda C \ar@{-}[dd]
732 \lambda2 \ar@{-}[ur]\ar@{-}[rr]\ar@{-}[dd]
733 & & \lambda P2 \ar@{-}[ur]\ar@{-}[dd]
735 & \lambda\underline\omega \ar@{-}'[r][rr]
736 & & \lambda P\underline\omega
738 \lambda{\to} \ar@{-}[rr]\ar@{-}[ur]
739 & & \lambda P \ar@{-}[ur]
742 Here $\lambda{\to}$, in the bottom left, is the STLC. From there can move along
745 \item[Terms depending on types (towards $\lambda{2}$)] We can quantify over
746 types in our type signatures. For example, we can define a polymorphic
748 {\mysmall\[\displaystyle
749 (\myabss{\myb{A}}{\mytyp}{\myabss{\myb{x}}{\myb{A}}{\myb{x}}}) : (\myb{A} : \mytyp) \myarr \myb{A} \myarr \myb{A}
751 The first and most famous instance of this idea has been System F. This form
752 of polymorphism and has been wildly successful, also thanks to a well known
753 inference algorithm for a restricted version of System F known as
754 Hindley-Milner. Languages like Haskell and SML are based on this discipline.
755 \item[Types depending on types (towards $\lambda{\underline{\omega}}$)] We have
756 type operators. For example we could define a function that given types $R$
757 and $\mytya$ forms the type that represents a value of type $\mytya$ in
758 continuation passing style: {\mysmall\[\displaystyle(\myabss{\myb{A} \myar \myb{R}}{\mytyp}{(\myb{A}
759 \myarr \myb{R}) \myarr \myb{R}}) : \mytyp \myarr \mytyp \myarr \mytyp\]}
760 \item[Types depending on terms (towards $\lambda{P}$)] Also known as `dependent
761 types', give great expressive power. For example, we can have values of whose
762 type depend on a boolean:
763 {\mysmall\[\displaystyle(\myabss{\myb{x}}{\mybool}{\myite{\myb{x}}{\mynat}{\myrat}}) : \mybool
767 All the systems preserve the properties that make the STLC well behaved. The
768 system we are going to focus on, Intuitionistic Type Theory, has all of the
769 above additions, and thus would sit where $\lambda{C}$ sits in the
770 `$\lambda$-cube'. It will serve as the logical `core' of all the other
771 extensions that we will present and ultimately our implementation of a similar
774 \subsection{A Bit of History}
776 Logic frameworks and programming languages based on type theory have a long
777 history. Per Martin-L\"{o}f described the first version of his theory in 1971,
778 but then revised it since the original version was inconsistent due to its
779 impredicativity\footnote{In the early version there was only one universe
780 $\mytyp$ and $\mytyp : \mytyp$, see section \ref{sec:term-types} for an
781 explanation on why this causes problems.}. For this reason he gave a revised
782 and consistent definition later \citep{Martin-Lof1984}.
784 A related development is the polymorphic $\lambda$-calculus, and specifically
785 the previously mentioned System F, which was developed independently by Girard
786 and Reynolds. An overview can be found in \citep{Reynolds1994}. The surprising
787 fact is that while System F is impredicative it is still consistent and strongly
788 normalising. \cite{Coquand1986} further extended this line of work with the
789 Calculus of Constructions (CoC).
791 Most widely used interactive theorem provers are based on ITT. Popular ones
792 include Agda \citep{Norell2007, Bove2009}, Coq \citep{Coq}, and Epigram
793 \citep{McBride2004, EpigramTut}.
795 \subsection{A simple type theory}
798 The calculus I present follows the exposition in \citep{Thompson1991},
799 and is quite close to the original formulation of predicative ITT as
800 found in \citep{Martin-Lof1984}. The system's syntax and reduction
801 rules are presented in their entirety in figure \ref{fig:core-tt-syn}.
802 The typing rules are presented piece by piece. Agda and \mykant\
803 renditions of the presented theory and all the examples is reproduced in
804 appendix \ref{app:itt-code}.
809 \begin{array}{r@{\ }c@{\ }l}
810 \mytmsyn & ::= & \myb{x} \mysynsep
812 \myunit \mysynsep \mytt \mysynsep
813 \myempty \mysynsep \myapp{\myabsurd{\mytmsyn}}{\mytmsyn} \\
814 & | & \mybool \mysynsep \mytrue \mysynsep \myfalse \mysynsep
815 \myitee{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
816 & | & \myfora{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
817 \myabss{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
818 (\myapp{\mytmsyn}{\mytmsyn}) \\
819 & | & \myexi{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
820 \mypairr{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn} \\
821 & | & \myapp{\myfst}{\mytmsyn} \mysynsep \myapp{\mysnd}{\mytmsyn} \\
822 & | & \myw{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
823 \mytmsyn \mynode{\myb{x}}{\mytmsyn} \mytmsyn \\
824 & | & \myrec{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn} \\
830 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
833 \begin{array}{l@{ }l@{\ }c@{\ }l}
834 \myitee{\mytrue &}{\myb{x}}{\myse{P}}{\mytmm}{\mytmn} & \myred & \mytmm \\
835 \myitee{\myfalse &}{\myb{x}}{\myse{P}}{\mytmm}{\mytmn} & \myred & \mytmn \\
840 \myapp{(\myabss{\myb{x}}{\mytya}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{\myb{x}}{\mytmn}
844 \begin{array}{l@{ }l@{\ }c@{\ }l}
845 \myapp{\myfst &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmm \\
846 \myapp{\mysnd &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmn
854 \myrec{(\myse{s} \mynode{\myb{x}}{\myse{T}} \myse{f})}{\myb{y}}{\myse{P}}{\myse{p}} \myred
855 \myapp{\myapp{\myapp{\myse{p}}{\myse{s}}}{\myse{f}}}{(\myabss{\myb{t}}{\mysub{\myse{T}}{\myb{x}}{\myse{s}}}{
856 \myrec{\myapp{\myse{f}}{\myb{t}}}{\myb{y}}{\myse{P}}{\mytmt}
860 \caption{Syntax and reduction rules for our type theory.}
861 \label{fig:core-tt-syn}
864 \subsubsection{Types are terms, some terms are types}
865 \label{sec:term-types}
867 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
869 \AxiomC{$\myjud{\mytmt}{\mytya}$}
870 \AxiomC{$\mytya \mydefeq \mytyb$}
871 \BinaryInfC{$\myjud{\mytmt}{\mytyb}$}
874 \AxiomC{\phantom{$\myjud{\mytmt}{\mytya}$}}
875 \UnaryInfC{$\myjud{\mytyp_l}{\mytyp_{l + 1}}$}
880 The first thing to notice is that a barrier between values and types that we had
881 in the STLC is gone: values can appear in types, and the two are treated
882 uniformly in the syntax.
884 While the usefulness of doing this will become clear soon, a consequence is
885 that since types can be the result of computation, deciding type equality is
886 not immediate as in the STLC. For this reason we define \emph{definitional
887 equality}, $\mydefeq$, as the congruence relation extending
888 $\myred$---moreover, when comparing types syntactically we do it up to
889 renaming of bound names ($\alpha$-renaming). For example under this
890 discipline we will find that
892 \myabss{\myb{x}}{\mytya}{\myb{x}} \mydefeq \myabss{\myb{y}}{\mytya}{\myb{y}}
894 Types that are definitionally equal can be used interchangeably. Here
895 the `conversion' rule is not syntax directed, but it is possible to
896 employ $\myred$ to decide term equality in a systematic way, by always
897 reducing terms to their normal forms before comparing them, so that a
898 separate conversion rule is not needed.
899 Another thing to notice is that considering the need to reduce terms to
900 decide equality, it is essential for a dependently type system to be
901 terminating and confluent for type checking to be decidable.
903 Moreover, we specify a \emph{type hierarchy} to talk about `large'
904 types: $\mytyp_0$ will be the type of types inhabited by data:
905 $\mybool$, $\mynat$, $\mylist$, etc. $\mytyp_1$ will be the type of
906 $\mytyp_0$, and so on---for example we have $\mytrue : \mybool :
907 \mytyp_0 : \mytyp_1 : \cdots$. Each type `level' is often called a
908 universe in the literature. While it is possible to simplify things by
909 having only one universe $\mytyp$ with $\mytyp : \mytyp$, this plan is
910 inconsistent for much the same reason that impredicative na\"{\i}ve set
911 theory is \citep{Hurkens1995}. However various techniques can be
912 employed to lift the burden of explicitly handling universes, as we will
913 see in section \ref{sec:term-hierarchy}.
915 \subsubsection{Contexts}
917 \begin{minipage}{0.5\textwidth}
918 \mydesc{context validity:}{\myvalid{\myctx}}{
920 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
921 \UnaryInfC{$\myvalid{\myemptyctx}$}
924 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
925 \UnaryInfC{$\myvalid{\myctx ; \myb{x} : \mytya}$}
930 \begin{minipage}{0.5\textwidth}
931 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
932 \AxiomC{$\myctx(x) = \mytya$}
933 \UnaryInfC{$\myjud{\myb{x}}{\mytya}$}
939 We need to refine the notion context to make sure that every variable appearing
940 is typed correctly, or that in other words each type appearing in the context is
941 indeed a type and not a value. In every other rule, if no premises are present,
942 we assume the context in the conclusion to be valid.
944 Then we can re-introduce the old rule to get the type of a variable for a
947 \subsubsection{$\myunit$, $\myempty$}
949 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
951 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
952 \UnaryInfC{$\myjud{\myunit}{\mytyp_0}$}
954 \UnaryInfC{$\myjud{\myempty}{\mytyp_0}$}
957 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
958 \UnaryInfC{$\myjud{\mytt}{\myunit}$}
960 \UnaryInfC{\phantom{$\myjud{\myempty}{\mytyp_0}$}}
963 \AxiomC{$\myjud{\mytmt}{\myempty}$}
964 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
965 \BinaryInfC{$\myjud{\myapp{\myabsurd{\mytya}}{\mytmt}}{\mytya}$}
967 \UnaryInfC{\phantom{$\myjud{\myempty}{\mytyp_0}$}}
972 Nothing surprising here: $\myunit$ and $\myempty$ are unchanged from the STLC,
973 with the added rules to type $\myunit$ and $\myempty$ themselves, and to make
974 sure that we are invoking $\myabsurd{}$ over a type.
976 \subsubsection{$\mybool$, and dependent $\myfun{if}$}
978 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
981 \UnaryInfC{$\myjud{\mybool}{\mytyp_0}$}
985 \UnaryInfC{$\myjud{\mytrue}{\mybool}$}
989 \UnaryInfC{$\myjud{\myfalse}{\mybool}$}
994 \AxiomC{$\myjud{\mytmt}{\mybool}$}
995 \AxiomC{$\myjudd{\myctx : \mybool}{\mytya}{\mytyp_l}$}
997 \BinaryInfC{$\myjud{\mytmm}{\mysub{\mytya}{x}{\mytrue}}$ \hspace{0.7cm} $\myjud{\mytmn}{\mysub{\mytya}{x}{\myfalse}}$}
998 \UnaryInfC{$\myjud{\myitee{\mytmt}{\myb{x}}{\mytya}{\mytmm}{\mytmn}}{\mysub{\mytya}{\myb{x}}{\mytmt}}$}
1002 With booleans we get the first taste of the `dependent' in `dependent
1003 types'. While the two introduction rules ($\mytrue$ and $\myfalse$) are
1004 not surprising, the typing rules for $\myfun{if}$ are. In most strongly
1005 typed languages we expect the branches of an $\myfun{if}$ statements to
1006 be of the same type, to preserve subject reduction, since execution
1007 could take both paths. This is a pity, since the type system does not
1008 reflect the fact that in each branch we gain knowledge on the term we
1009 are branching on. Which means that programs along the lines of
1010 {\mysmall\[\text{\texttt{if null xs then head xs else 0}}\]}
1011 are a necessary, well typed, danger.
1013 However, in a more expressive system, we can do better: the branches' type can
1014 depend on the value of the scrutinised boolean. This is what the typing rule
1015 expresses: the user provides a type $\mytya$ ranging over an $\myb{x}$
1016 representing the scrutinised boolean type, and the branches are typechecked with
1017 the updated knowledge on the value of $\myb{x}$.
1019 \subsubsection{$\myarr$, or dependent function}
1021 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1022 \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
1023 \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
1024 \BinaryInfC{$\myjud{\myfora{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
1030 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytmt}{\mytyb}$}
1031 \UnaryInfC{$\myjud{\myabss{\myb{x}}{\mytya}{\mytmt}}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
1034 \AxiomC{$\myjud{\mytmm}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
1035 \AxiomC{$\myjud{\mytmn}{\mytya}$}
1036 \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mysub{\mytyb}{\myb{x}}{\mytmn}}$}
1041 Dependent functions are one of the two key features that perhaps most
1042 characterise dependent types---the other being dependent products. With
1043 dependent functions, the result type can depend on the value of the
1044 argument. This feature, together with the fact that the result type
1045 might be a type itself, brings a lot of interesting possibilities.
1046 Following this intuition, in the introduction rule, the return type is
1047 typechecked in a context with an abstracted variable of lhs' type, and
1048 in the elimination rule the actual argument is substituted in the return
1049 type. Keeping the correspondence with logic alive, dependent functions
1050 are much like universal quantifiers ($\forall$) in logic.
1052 For example, assuming that we have lists and natural numbers in our
1053 language, using dependent functions we would be able to
1057 \myfun{length} : (\myb{A} {:} \mytyp_0) \myarr \myapp{\mylist}{\myb{A}} \myarr \mynat \\
1058 \myarg \myfun{$>$} \myarg : \mynat \myarr \mynat \myarr \mytyp_0 \\
1059 \myfun{head} : (\myb{A} {:} \mytyp_0) \myarr (\myb{l} {:} \myapp{\mylist}{\myb{A}})
1060 \myarr \myapp{\myapp{\myfun{length}}{\myb{A}}}{\myb{l}} \mathrel{\myfun{$>$}} 0 \myarr
1065 \myfun{length} is the usual polymorphic length
1066 function. $\myarg\myfun{$>$}\myarg$ is a function that takes two naturals
1067 and returns a type: if the lhs is greater then the rhs, $\myunit$ is
1068 returned, $\myempty$ otherwise. This way, we can express a
1069 `non-emptyness' condition in $\myfun{head}$, by including a proof that
1070 the length of the list argument is non-zero. This allows us to rule out
1071 the `empty list' case, so that we can safely return the first element.
1073 Again, we need to make sure that the type hierarchy is respected, which is the
1074 reason why a type formed by $\myarr$ will live in the least upper bound of the
1075 levels of argument and return type. This trend will continue with the other
1076 type-level binders, $\myprod$ and $\mytyc{W}$.
1078 \subsubsection{$\myprod$, or dependent product}
1081 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1082 \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
1083 \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
1084 \BinaryInfC{$\myjud{\myexi{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
1090 \AxiomC{$\myjud{\mytmm}{\mytya}$}
1091 \AxiomC{$\myjud{\mytmn}{\mysub{\mytyb}{\myb{x}}{\mytmm}}$}
1092 \BinaryInfC{$\myjud{\mypairr{\mytmm}{\myb{x}}{\mytyb}{\mytmn}}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
1094 \UnaryInfC{\phantom{$--$}}
1097 \AxiomC{$\myjud{\mytmt}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
1098 \UnaryInfC{$\hspace{0.7cm}\myjud{\myapp{\myfst}{\mytmt}}{\mytya}\hspace{0.7cm}$}
1100 \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mysub{\mytyb}{\myb{x}}{\myapp{\myfst}{\mytmt}}}$}
1105 If dependent functions are a generalisation of $\myarr$ in the STLC,
1106 dependent products are a generalisation of $\myprod$ in the STLC. The
1107 improvement is that the second element's type can depend on the value of
1108 the first element. The corrispondence with logic is through the
1109 existential quantifier: $\exists x \in \mathbb{N}. even(x)$ can be
1110 expressed as $\myexi{\myb{x}}{\mynat}{\myapp{\myfun{even}}{\myb{x}}}$.
1111 The first element will be a number, and the second evidence that the
1112 number is even. This highlights the fact that we are working in a
1113 constructive logic: if we have an existence proof, we can always ask for
1114 a witness. This means, for instance, that $\neg \forall \neg$ is not
1115 equivalent to $\exists$.
1117 Another perhaps more `dependent' application of products, paired with
1118 $\mybool$, is to offer choice between different types. For example we
1119 can easily recover disjunctions:
1122 \myarg\myfun{$\vee$}\myarg : \mytyp_0 \myarr \mytyp_0 \myarr \mytyp_0 \\
1123 \myb{A} \mathrel{\myfun{$\vee$}} \myb{B} \mapsto \myexi{\myb{x}}{\mybool}{\myite{\myb{x}}{\myb{A}}{\myb{B}}} \\ \ \\
1124 \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} \\
1125 \myfun{case} \myappsp \myb{A} \myappsp \myb{B} \myappsp \myb{C} \myappsp \myb{f} \myappsp \myb{g} \myappsp \myb{x} \mapsto \\
1126 \myind{2} \myapp{(\myitee{\myapp{\myfst}{\myb{b}}}{\myb{x}}{(\myite{\myb{b}}{\myb{A}}{\myb{B}})}{\myb{f}}{\myb{g}})}{(\myapp{\mysnd}{\myb{x}})}
1130 \subsubsection{$\mytyc{W}$, or well-order}
1131 \label{sec:well-order}
1133 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1135 \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
1136 \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
1137 \BinaryInfC{$\myjud{\myw{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
1142 \AxiomC{$\myjud{\mytmt}{\mytya}$}
1143 \AxiomC{$\myjud{\mysynel{f}}{\mysub{\mytyb}{\myb{x}}{\mytmt} \myarr \myw{\myb{x}}{\mytya}{\mytyb}}$}
1144 \BinaryInfC{$\myjud{\mytmt \mynode{\myb{x}}{\mytyb} \myse{f}}{\myw{\myb{x}}{\mytya}{\mytyb}}$}
1150 \AxiomC{$\myjud{\myse{u}}{\myw{\myb{x}}{\myse{S}}{\myse{T}}}$}
1151 \AxiomC{$\myjudd{\myctx; \myb{w} : \myw{\myb{x}}{\myse{S}}{\myse{T}}}{\myse{P}}{\mytyp_l}$}
1153 \BinaryInfC{$\myjud{\myse{p}}{
1154 \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}}}}
1156 \UnaryInfC{$\myjud{\myrec{\myse{u}}{\myb{w}}{\myse{P}}{\myse{p}}}{\mysub{\myse{P}}{\myb{w}}{\myse{u}}}$}
1160 Finally, the well-order type, or in short $\mytyc{W}$-type, which will
1161 let us represent inductive data in a general (but clumsy) way. We can
1162 form `nodes' of the shape $\mytmt \mynode{\myb{x}}{\mytyb} \myse{f} :
1163 \myw{\myb{x}}{\mytya}{\mytyb}$ that contain data ($\mytmt$) of type and
1164 one `child' for each member of $\mysub{\mytyb}{\myb{x}}{\mytmt}$. The
1165 $\myfun{rec}\ \myfun{with}$ acts as an induction principle on
1166 $\mytyc{W}$, given a predicate an a function dealing with the inductive
1167 case---we will gain more intuition about inductive data in ITT in
1168 section \ref{sec:user-type}.
1170 For example, if we want to form natural numbers, we can take
1173 \mytyc{Tr} : \mybool \myarr \mytyp_0 \\
1174 \mytyc{Tr} \myappsp \myb{b} \mapsto \myfun{if}\, \myb{b}\, \myunit\, \myfun{else}\, \myempty \\
1176 \mynat : \mytyp_0 \\
1177 \mynat \mapsto \myw{\myb{b}}{\mybool}{(\mytyc{Tr}\myappsp\myb{b})}
1179 \]} Each node will contain a boolean. If $\mytrue$, the number is
1180 non-zero, and we will have one child representing its predecessor, given
1181 that $\mytyc{Tr}$ will return $\myunit$. If $\myfalse$, the number is
1182 zero, and we will have no predecessors (children), given the $\myempty$:
1185 \mydc{zero} : \mynat \\
1186 \mydc{zero} \mapsto \myfalse \mynodee (\myabs{\myb{z}}{\myabsurd{\mynat} \myappsp \myb{x}}) \\
1188 \mydc{suc} : \mynat \myarr \mynat \\
1189 \mydc{suc}\myappsp \myb{x} \mapsto \mytrue \mynodee (\myabs{\myarg}{\myb{x}})
1192 And with a bit of effort, we can recover addition:
1195 \myfun{plus} : \mynat \myarr \mynat \myarr \mynat \\
1196 \myfun{plus} \myappsp \myb{x} \myappsp \myb{y} \mapsto \\
1197 \myind{2} \myfun{rec}\, \myb{x} / \myb{b}.\mynat \, \\
1198 \myind{2} \myfun{with}\, \myabs{\myb{b}}{\\
1199 \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) \\
1200 \myind{2}\myind{2}\myfun{then}\,(\myabs{\myarg\, \myb{f}}{\mydc{suc}\myappsp (\myapp{\myb{f}}{\mytt})})\, \myfun{else}\, (\myabs{\myarg\, \myarg}{\myb{y}})}
1202 \]} Note how we explicitly have to type the branches to make them
1203 match with the definition of $\mynat$---which gives a taste of the
1204 `clumsiness' of $\mytyc{W}$-types, which while useful as a reasoning
1205 tool are useless to the user modelling data types.
1207 \section{The struggle for equality}
1208 \label{sec:equality}
1210 In the previous section we saw how a type checker (or a human) needs a
1211 notion of \emph{definitional equality}. Beyond this meta-theoretic
1212 notion, in this section we will explore the ways of expressing equality
1213 \emph{inside} the theory, as a reasoning tool available to the user.
1214 This area is the main concern of this thesis, and in general a very
1215 active research topic, since we do not have a fully satisfactory
1216 solution, yet. As in the previous section, everything presented is
1217 formalised in Agda in appendix \ref{app:agda-itt}.
1219 \subsection{Propositional equality}
1222 \begin{minipage}{0.5\textwidth}
1225 \begin{array}{r@{\ }c@{\ }l}
1226 \mytmsyn & ::= & \cdots \\
1227 & | & \mytmsyn \mypeq{\mytmsyn} \mytmsyn \mysynsep
1228 \myapp{\myrefl}{\mytmsyn} \\
1229 & | & \myjeq{\mytmsyn}{\mytmsyn}{\mytmsyn}
1234 \begin{minipage}{0.5\textwidth}
1235 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
1237 \myjeq{\myse{P}}{(\myapp{\myrefl}{\mytmm})}{\mytmn} \myred \mytmn
1243 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1244 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
1245 \AxiomC{$\myjud{\mytmm}{\mytya}$}
1246 \AxiomC{$\myjud{\mytmn}{\mytya}$}
1247 \TrinaryInfC{$\myjud{\mytmm \mypeq{\mytya} \mytmn}{\mytyp_l}$}
1253 \AxiomC{$\begin{array}{c}\ \\\myjud{\mytmm}{\mytya}\hspace{1.1cm}\mytmm \mydefeq \mytmn\end{array}$}
1254 \UnaryInfC{$\myjud{\myapp{\myrefl}{\mytmm}}{\mytmm \mypeq{\mytya} \mytmn}$}
1259 \myjud{\myse{P}}{\myfora{\myb{x}\ \myb{y}}{\mytya}{\myfora{q}{\myb{x} \mypeq{\mytya} \myb{y}}{\mytyp_l}}} \\
1260 \myjud{\myse{q}}{\mytmm \mypeq{\mytya} \mytmn}\hspace{1.1cm}\myjud{\myse{p}}{\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmm}}{(\myapp{\myrefl}{\mytmm})}}
1263 \UnaryInfC{$\myjud{\myjeq{\myse{P}}{\myse{q}}{\myse{p}}}{\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmn}}{q}}$}
1268 To express equality between two terms inside ITT, the obvious way to do so is
1269 to have the equality construction to be a type-former. Here we present what
1270 has survived as the dominating form of equality in systems based on ITT up to
1273 Our type former is $\mypeq{\mytya}$, which given a type (in this case
1274 $\mytya$) relates equal terms of that type. $\mypeq{}$ has one introduction
1275 rule, $\myrefl$, which introduces an equality relation between definitionally
1278 Finally, we have one eliminator for $\mypeq{}$, $\myjeqq$. $\myjeq{\myse{P}}{\myse{q}}{\myse{p}}$ takes
1280 \item $\myse{P}$, a predicate working with two terms of a certain type (say
1281 $\mytya$) and a proof of their equality
1282 \item $\myse{q}$, a proof that two terms in $\mytya$ (say $\myse{m}$ and
1283 $\myse{n}$) are equal
1284 \item and $\myse{p}$, an inhabitant of $\myse{P}$ applied to $\myse{m}$
1285 twice, plus the trivial proof by reflexivity showing that $\myse{m}$
1288 Given these ingredients, $\myjeqq$ retuns a member of $\myse{P}$ applied to
1289 $\mytmm$, $\mytmn$, and $\myse{q}$. In other words $\myjeqq$ takes a
1290 witness that $\myse{P}$ works with \emph{definitionally equal} terms, and
1291 returns a witness of $\myse{P}$ working with \emph{propositionally equal}
1292 terms. Invokations of $\myjeqq$ will vanish when the equality proofs will
1293 reduce to invocations to reflexivity, at which point the arguments must be
1294 definitionally equal, and thus the provided
1295 $\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmm}}{(\myapp{\myrefl}{\mytmm})}$
1298 While the $\myjeqq$ rule is slightly convoluted, ve can derive many more
1299 `friendly' rules from it, for example a more obvious `substitution' rule, that
1300 replaces equal for equal in predicates:
1303 \myfun{subst} : \myfora{\myb{A}}{\mytyp}{\myfora{\myb{P}}{\myb{A} \myarr \mytyp}{\myfora{\myb{x}\ \myb{y}}{\myb{A}}{\myb{x} \mypeq{\myb{A}} \myb{y} \myarr \myapp{\myb{P}}{\myb{x}} \myarr \myapp{\myb{P}}{\myb{y}}}}} \\
1304 \myfun{subst}\myappsp \myb{A}\myappsp\myb{P}\myappsp\myb{x}\myappsp\myb{y}\myappsp\myb{q}\myappsp\myb{p} \mapsto
1305 \myjeq{(\myabs{\myb{x}\ \myb{y}\ \myb{q}}{\myapp{\myb{P}}{\myb{y}}})}{\myb{p}}{\myb{q}}
1308 Once we have $\myfun{subst}$, we can easily prove more familiar laws regarding
1309 equality, such as symmetry, transitivity, congruence laws, etc.
1311 \subsection{Common extensions}
1313 Our definitional and propositional equalities can be enhanced in various
1314 ways. Obviously if we extend the definitional equality we are also
1315 automatically extend propositional equality, given how $\myrefl$ works.
1317 \subsubsection{$\eta$-expansion}
1318 \label{sec:eta-expand}
1320 A simple extension to our definitional equality is $\eta$-expansion.
1321 Given an abstract variable $\myb{f} : \mytya \myarr \mytyb$ the aim is
1322 to have that $\myb{f} \mydefeq
1323 \myabss{\myb{x}}{\mytya}{\myapp{\myb{f}}{\myb{x}}}$. We can achieve
1324 this by `expanding' terms based on their types, a process also known as
1325 \emph{quotation}---a term borrowed from the practice of
1326 \emph{normalisation by evaluation}, where we embed terms in some host
1327 language with an existing notion of computation, and then reify them
1328 back into terms, which will `smooth out' differences like the one above
1331 The same concept applies to $\myprod$, where we expand each inhabitant
1332 by reconstructing it by getting its projections, so that $\myb{x}
1333 \mydefeq \mypair{\myfst \myappsp \myb{x}}{\mysnd \myappsp \myb{x}}$.
1334 Similarly, all one inhabitants of $\myunit$ and all zero inhabitants of
1335 $\myempty$ can be considered equal. Quotation can be performed in a
1336 type-directed way, as we will witness in section \ref{sec:kant-irr}.
1338 To justify this process in our type system we will add a congruence law
1339 for abstractions and a similar law for products, plus the fact that all
1340 elements of $\myunit$ or $\myempty$ are equal.
1342 \mydesc{definitional equality:}{\myjud{\mytmm \mydefeq \mytmn}{\mytmsyn}}{
1344 \AxiomC{$\myjudd{\myctx; \myb{y} : \mytya}{\myapp{\myse{f}}{\myb{x}} \mydefeq \myapp{\myse{g}}{\myb{x}}}{\mysub{\mytyb}{\myb{x}}{\myb{y}}}$}
1345 \UnaryInfC{$\myjud{\myse{f} \mydefeq \myse{g}}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
1348 \AxiomC{$\myjud{\mypair{\myapp{\myfst}{\mytmm}}{\myapp{\mysnd}{\mytmm}} \mydefeq \mypair{\myapp{\myfst}{\mytmn}}{\myapp{\mysnd}{\mytmn}}}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
1349 \UnaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
1356 \AxiomC{$\myjud{\mytmm}{\myunit}$}
1357 \AxiomC{$\myjud{\mytmn}{\myunit}$}
1358 \BinaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\myunit}$}
1361 \AxiomC{$\myjud{\mytmm}{\myempty}$}
1362 \AxiomC{$\myjud{\mytmn}{\myempty}$}
1363 \BinaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\myempty}$}
1368 \subsubsection{Uniqueness of identity proofs}
1370 Another common but controversial addition to propositional equality is
1371 the $\myfun{K}$ axiom, which essentially states that all equality proofs
1374 \mydesc{typing:}{\myjud{\mytmm \mydefeq \mytmn}{\mytmsyn}}{
1377 \myjud{\myse{P}}{\myfora{\myb{x}}{\mytya}{\myb{x} \mypeq{\mytya} \myb{x} \myarr \mytyp}} \\\
1378 \myjud{\mytmt}{\mytya} \hspace{1cm}
1379 \myjud{\myse{p}}{\myse{P} \myappsp \mytmt \myappsp (\myrefl \myappsp \mytmt)} \hspace{1cm}
1380 \myjud{\myse{q}}{\mytmt \mypeq{\mytya} \mytmt}
1383 \UnaryInfC{$\myjud{\myfun{K} \myappsp \myse{P} \myappsp \myse{t} \myappsp \myse{p} \myappsp \myse{q}}{\myse{P} \myappsp \mytmt \myappsp \myse{q}}$}
1387 \cite{Hofmann1994} showed that $\myfun{K}$ is not derivable from the
1388 $\myjeqq$ axiom that we presented, and \cite{McBride2004} showed that it is
1389 needed to implement `dependent pattern matching', as first proposed by
1390 \cite{Coquand1992}. Thus, $\myfun{K}$ is derivable in the systems that
1391 implement dependent pattern matching, such as Epigram and Agda; but for
1394 $\myfun{K}$ is controversial mainly because it is at odds with
1395 equalities that include computational behaviour, most notably
1396 Voevodsky's `Univalent Foundations', which includes a \emph{univalence}
1397 axiom that identifies isomorphisms between types with propositional
1398 equality. For example we would have two isomorphisms, and thus two
1399 equalities, between $\mybool$ and $\mybool$, corresponding to the two
1400 permutations---one is the identity, and one swaps the elements. Given
1401 this, $\myfun{K}$ and univalence are inconsistent, and thus a form of
1402 dependent pattern matching that does not imply $\myfun{K}$ is subject of
1403 research\footnote{More information about univalence can be found at
1404 \url{http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations.html}.}.
1406 \subsection{Limitations}
1408 \epigraph{\emph{Half of my time spent doing research involves thinking up clever
1409 schemes to avoid needing functional extensionality.}}{@larrytheliquid}
1411 However, propositional equality as described is quite restricted when
1412 reasoning about equality beyond the term structure, which is what definitional
1413 equality gives us (extension notwithstanding).
1415 The problem is best exemplified by \emph{function extensionality}. In
1416 mathematics, we would expect to be able to treat functions that give equal
1417 output for equal input as the same. When reasoning in a mechanised framework
1418 we ought to be able to do the same: in the end, without considering the
1419 operational behaviour, all functions equal extensionally are going to be
1420 replaceable with one another.
1422 However this is not the case, or in other words with the tools we have we have
1425 \myfun{ext} : \myfora{\myb{A}\ \myb{B}}{\mytyp}{\myfora{\myb{f}\ \myb{g}}{
1426 \myb{A} \myarr \myb{B}}{
1427 (\myfora{\myb{x}}{\myb{A}}{\myapp{\myb{f}}{\myb{x}} \mypeq{\myb{B}} \myapp{\myb{g}}{\myb{x}}}) \myarr
1428 \myb{f} \mypeq{\myb{A} \myarr \myb{B}} \myb{g}
1432 To see why this is the case, consider the functions
1433 {\mysmall\[\myabs{\myb{x}}{0 \mathrel{\myfun{$+$}} \myb{x}}$ and $\myabs{\myb{x}}{\myb{x} \mathrel{\myfun{$+$}} 0}\]}
1434 where $\myfun{$+$}$ is defined by recursion on the first argument,
1435 gradually destructing it to build up successors of the second argument.
1436 The two functions are clearly extensionally equal, and we can in fact
1439 \myfora{\myb{x}}{\mynat}{(0 \mathrel{\myfun{$+$}} \myb{x}) \mypeq{\mynat} (\myb{x} \mathrel{\myfun{$+$}} 0)}
1441 By analysis on the $\myb{x}$. However, the two functions are not
1442 definitionally equal, and thus we won't be able to get rid of the
1445 For the reasons above, theories that offer a propositional equality
1446 similar to what we presented are called \emph{intensional}, as opposed
1447 to \emph{extensional}. Most systems in wide use today (such as Agda,
1448 Coq, and Epigram) are of this kind.
1450 This is quite an annoyance that often makes reasoning awkward to execute. It
1451 also extends to other fields, for example proving bisimulation between
1452 processes specified by coinduction, or in general proving equivalences based
1453 on the behaviour on a term.
1455 \subsection{Equality reflection}
1457 One way to `solve' this problem is by identifying propositional equality with
1458 definitional equality:
1460 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1461 \AxiomC{$\myjud{\myse{q}}{\mytmm \mypeq{\mytya} \mytmn}$}
1462 \UnaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\mytya}$}
1466 This rule takes the name of \emph{equality reflection}, and is a very
1467 different rule from the ones we saw up to now: it links a typing judgement
1468 internal to the type theory to a meta-theoretic judgement that the type
1469 checker uses to work with terms. It is easy to see the dangerous consequences
1472 \item The rule is syntax directed, and the type checker is presumably expected
1473 to come up with equality proofs when needed.
1474 \item More worryingly, type checking becomes undecidable also because
1475 computing under false assumptions becomes unsafe, since we derive any
1476 equality proof and then use equality reflection and the conversion
1477 rule to have terms of any type.
1480 Given these facts theories employing equality reflection, like NuPRL
1481 \citep{NuPRL}, carry the derivations that gave rise to each typing judgement
1482 to keep the systems manageable.
1484 For all its faults, equality reflection does allow us to prove extensionality,
1485 using the extensions we gave above. Assuming that $\myctx$ contains
1486 {\mysmall\[\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}}}\]}
1490 \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}$}
1491 \RightLabel{equality reflection}
1492 \UnaryInfC{$\myjudd{\myctx; \myb{x} : \myb{A}}{\myapp{\myb{f}}{\myb{x}} \mydefeq \myapp{\myb{g}}{\myb{x}}}{\myb{B}}$}
1493 \RightLabel{congruence for $\lambda$s}
1494 \UnaryInfC{$\myjud{(\myabs{\myb{x}}{\myapp{\myb{f}}{\myb{x}}}) \mydefeq (\myabs{\myb{x}}{\myapp{\myb{g}}{\myb{x}}})}{\myb{A} \myarr \myb{B}}$}
1495 \RightLabel{$\eta$-law for $\lambda$}
1496 \UnaryInfC{$\hspace{1.45cm}\myjud{\myb{f} \mydefeq \myb{g}}{\myb{A} \myarr \myb{B}}\hspace{1.45cm}$}
1497 \RightLabel{$\myrefl$}
1498 \UnaryInfC{$\myjud{\myapp{\myrefl}{\myb{f}}}{\myb{f} \mypeq{} \myb{g}}$}
1501 Now, the question is: do we need to give up well-behavedness of our theory to
1502 gain extensionality?
1504 \subsection{Some alternatives}
1507 % TODO add `extentional axioms' (Hoffman), setoid models (Thorsten)
1509 \section{Observational equality}
1512 A recent development by \citet{Altenkirch2007}, \emph{Observational Type
1513 Theory} (OTT), promises to keep the well behavedness of ITT while
1514 being able to gain many useful equality proofs\footnote{It is suspected
1515 that OTT gains \emph{all} the equality proofs of ETT, but no proof
1516 exists yet.}, including function extensionality. The main idea is to
1517 give the user the possibility to \emph{coerce} (or transport) values
1518 from a type $\mytya$ to a type $\mytyb$, if the type checker can prove
1519 structurally that $\mytya$ and $\mytya$ are equal; and providing a
1520 value-level equality based on similar principles. Here we give an
1521 exposition which follows closely the original paper.
1523 \subsection{A simpler theory, a propositional fragment}
1526 $\mytyp_l$ is replaced by $\mytyp$. \\\ \\
1528 \begin{array}{r@{\ }c@{\ }l}
1529 \mytmsyn & ::= & \cdots \mysynsep \myprdec{\myprsyn} \mysynsep
1530 \myITE{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
1531 \myprsyn & ::= & \mybot \mysynsep \mytop \mysynsep \myprsyn \myand \myprsyn
1532 \mysynsep \myprfora{\myb{x}}{\mytmsyn}{\myprsyn}
1537 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1539 \AxiomC{$\myjud{\myse{P}}{\myprop}$}
1540 \UnaryInfC{$\myjud{\myprdec{\myse{P}}}{\mytyp}$}
1543 \AxiomC{$\myjud{\mytmt}{\mybool}$}
1544 \AxiomC{$\myjud{\mytya}{\mytyp}$}
1545 \AxiomC{$\myjud{\mytyb}{\mytyp}$}
1546 \TrinaryInfC{$\myjud{\myITE{\mytmt}{\mytya}{\mytyb}}{\mytyp}$}
1551 \mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
1552 \begin{tabular}{ccc}
1553 \AxiomC{\phantom{$\myjud{\myse{P}}{\myprop}$}}
1554 \UnaryInfC{$\myjud{\mytop}{\myprop}$}
1556 \UnaryInfC{$\myjud{\mybot}{\myprop}$}
1559 \AxiomC{$\myjud{\myse{P}}{\myprop}$}
1560 \AxiomC{$\myjud{\myse{Q}}{\myprop}$}
1561 \BinaryInfC{$\myjud{\myse{P} \myand \myse{Q}}{\myprop}$}
1563 \UnaryInfC{\phantom{$\myjud{\mybot}{\myprop}$}}
1566 \AxiomC{$\myjud{\myse{A}}{\mytyp}$}
1567 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\myse{P}}{\myprop}$}
1568 \BinaryInfC{$\myjud{\myprfora{\myb{x}}{\mytya}{\myse{P}}}{\myprop}$}
1570 \UnaryInfC{\phantom{$\myjud{\mybot}{\myprop}$}}
1575 Our foundation will be a type theory like the one of section
1576 \ref{sec:itt}, with only one level: $\mytyp_0$. In this context we will
1577 drop the $0$ and call $\mytyp_0$ $\mytyp$. Moreover, since the old
1578 $\myfun{if}\myarg\myfun{then}\myarg\myfun{else}$ was able to return
1579 types thanks to the hierarchy (which is gone), we need to reintroduce an
1580 ad-hoc conditional for types, where the reduction rule is the obvious
1583 However, we have an addition: a universe of \emph{propositions},
1584 $\myprop$. $\myprop$ isolates a fragment of types at large, and
1585 indeed we can `inject' any $\myprop$ back in $\mytyp$ with $\myprdec{\myarg}$: \\
1586 \mydesc{proposition decoding:}{\myprdec{\mytmsyn} \myred \mytmsyn}{
1589 \begin{array}{l@{\ }c@{\ }l}
1590 \myprdec{\mybot} & \myred & \myempty \\
1591 \myprdec{\mytop} & \myred & \myunit
1596 \begin{array}{r@{ }c@{ }l@{\ }c@{\ }l}
1597 \myprdec{&\myse{P} \myand \myse{Q} &} & \myred & \myprdec{\myse{P}} \myprod \myprdec{\myse{Q}} \\
1598 \myprdec{&\myprfora{\myb{x}}{\mytya}{\myse{P}} &} & \myred &
1599 \myfora{\myb{x}}{\mytya}{\myprdec{\myse{P}}}
1604 Propositions are what we call the types of \emph{proofs}, or types
1605 whose inhabitants contain no `data', much like $\myunit$. The goal of
1606 doing this is twofold: erasing all top-level propositions when
1607 compiling; and to identify all equivalent propositions as the same, as
1610 Why did we choose what we have in $\myprop$? Given the above
1611 criteria, $\mytop$ obviously fits the bill. A pair of propositions
1612 $\myse{P} \myand \myse{Q}$ still won't get us data. Finally, if
1613 $\myse{P}$ is a proposition and we have
1614 $\myprfora{\myb{x}}{\mytya}{\myse{P}}$ , the decoding will be a
1615 function which returns propositional content. The only threat is
1616 $\mybot$, by which we can fabricate anything we want: however if we
1617 are consistent there will be nothing of type $\mybot$ at the top
1618 level, which is what we care about regarding proof erasure.
1620 \subsection{Equality proofs}
1624 \begin{array}{r@{\ }c@{\ }l}
1625 \mytmsyn & ::= & \cdots \mysynsep
1626 \mycoee{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \mysynsep
1627 \mycohh{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
1628 \myprsyn & ::= & \cdots \mysynsep \mytmsyn \myeq \mytmsyn \mysynsep
1629 \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn}
1634 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1636 \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
1637 \AxiomC{$\myjud{\mytmt}{\mytya}$}
1638 \BinaryInfC{$\myjud{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}$}
1641 \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
1642 \AxiomC{$\myjud{\mytmt}{\mytya}$}
1643 \BinaryInfC{$\myjud{\mycohh{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\myprdec{\myjm{\mytmt}{\mytya}{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}}}$}
1649 \mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
1654 \myjud{\myse{A}}{\mytyp} \hspace{1cm} \myjud{\myse{B}}{\mytyp}
1657 \UnaryInfC{$\myjud{\mytya \myeq \mytyb}{\myprop}$}
1662 \myjud{\myse{A}}{\mytyp} \hspace{1cm} \myjud{\mytmm}{\myse{A}} \\
1663 \myjud{\myse{B}}{\mytyp} \hspace{1cm} \myjud{\mytmn}{\myse{B}}
1666 \UnaryInfC{$\myjud{\myjm{\mytmm}{\myse{A}}{\mytmn}{\myse{B}}}{\myprop}$}
1673 While isolating a propositional universe as presented can be a useful
1674 exercises on its own, what we are really after is a useful notion of
1675 equality. In OTT we want to maintain the notion that things judged to
1676 be equal are still always repleaceable for one another with no
1677 additional changes. Note that this is not the same as saying that they
1678 are definitionally equal, since as we saw extensionally equal functions,
1679 while satisfying the above requirement, are not definitionally equal.
1681 Towards this goal we introduce two equality constructs in
1682 $\myprop$---the fact that they are in $\myprop$ indicates that they
1683 indeed have no computational content. The first construct, $\myarg
1684 \myeq \myarg$, relates types, the second,
1685 $\myjm{\myarg}{\myarg}{\myarg}{\myarg}$, relates values. The
1686 value-level equality is different from our old propositional equality:
1687 instead of ranging over only one type, we might form equalities between
1688 values of different types---the usefulness of this construct will be
1689 clear soon. In the literature this equality is known as `heterogeneous'
1690 or `John Major', since
1693 John Major's `classless society' widened people's aspirations to
1694 equality, but also the gap between rich and poor. After all, aspiring
1695 to be equal to others than oneself is the politics of envy. In much
1696 the same way, forms equations between members of any type, but they
1697 cannot be treated as equals (ie substituted) unless they are of the
1698 same type. Just as before, each thing is only equal to
1699 itself. \citep{McBride1999}.
1702 Correspondingly, at the term level, $\myfun{coe}$ (`coerce') lets us
1703 transport values between equal types; and $\myfun{coh}$ (`coherence')
1704 guarantees that $\myfun{coe}$ respects the value-level equality, or in
1705 other words that it really has no computational component: if we
1706 transport $\mytmm : \mytya$ to $\mytmn : \mytyb$, $\mytmm$ and $\mytmn$
1707 will still be the same.
1709 Before introducing the core ideas that make OTT work, let us distinguish
1710 between \emph{canonical} and \emph{neutral} types. Canonical types are
1711 those arising from the ground types ($\myempty$, $\myunit$, $\mybool$)
1712 and the three type formers ($\myarr$, $\myprod$, $\mytyc{W}$). Neutral
1713 types are those formed by
1714 $\myfun{If}\myarg\myfun{Then}\myarg\myfun{Else}\myarg$.
1715 Correspondingly, canonical terms are those inhabiting canonical types
1716 ($\mytt$, $\mytrue$, $\myfalse$, $\myabss{\myb{x}}{\mytya}{\mytmt}$,
1717 ...), and neutral terms those formed by eliminators\footnote{Using the
1718 terminology from section \ref{sec:types}, we'd say that canonical
1719 terms are in \emph{weak head normal form}.}. In the current system
1720 (and hopefully in well-behaved systems), all closed terms reduce to a
1721 canonical term, and all canonical types are inhabited by canonical
1724 \subsubsection{Type equality, and coercions}
1726 The plan is to decompose type-level equalities between canonical types
1727 into decodable propositions containing equalities regarding the
1728 subterms, and to use coerce recursively on the subterms using the
1729 generated equalities. This interplay between type equalities and
1730 \myfun{coe} ensures that invocations of $\myfun{coe}$ will vanish when
1731 we have evidence of the structural equality of the types we are
1732 transporting terms across. If the type is neutral, the equality won't
1733 reduce and thus $\myfun{coe}$ won't reduce either. If we come an
1734 equality between different canonical types, then we reduce the equality
1735 to bottom, making sure that no such proof can exist, and providing an
1736 `escape hatch' in $\myfun{coe}$.
1740 \mydesc{equality reduction:}{\myprsyn \myred \myprsyn}{
1742 \begin{array}{c@{\ }c@{\ }c@{\ }l}
1743 \myempty & \myeq & \myempty & \myred \mytop \\
1744 \myunit & \myeq & \myunit & \myred \mytop \\
1745 \mybool & \myeq & \mybool & \myred \mytop \\
1746 \myexi{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myexi{\myb{x_2}}{\mytya_2}{\mytya_2} & \myred \\
1748 \myind{2} \mytya_1 \myeq \mytyb_1 \myand
1749 \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}]}
1751 \myfora{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myfora{\myb{x_2}}{\mytya_2}{\mytyb_2} & \myred \cdots \\
1752 \myw{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myw{\myb{x_2}}{\mytya_2}{\mytyb_2} & \myred \cdots \\
1753 \mytya & \myeq & \mytyb & \myred \mybot\ \text{if $\mytya$ and $\mytyb$ are canonical.}
1758 \mydesc{reduction}{\mytmsyn \myred \mytmsyn}{
1760 \begin{array}[t]{@{}l@{\ }l@{\ }l@{\ }l@{\ }l@{\ }c@{\ }l@{\ }}
1761 \mycoe & \myempty & \myempty & \myse{Q} & \myse{t} & \myred & \myse{t} \\
1762 \mycoe & \myunit & \myunit & \myse{Q} & \myse{t} & \myred & \mytt \\
1763 \mycoe & \mybool & \mybool & \myse{Q} & \mytrue & \myred & \mytrue \\
1764 \mycoe & \mybool & \mybool & \myse{Q} & \myfalse & \myred & \myfalse \\
1765 \mycoe & (\myexi{\myb{x_1}}{\mytya_1}{\mytyb_1}) &
1766 (\myexi{\myb{x_2}}{\mytya_2}{\mytyb_2}) & \myse{Q} &
1767 \mytmt_1 & \myred & \\
1769 \myind{2}\begin{array}[t]{l@{\ }l@{\ }c@{\ }l}
1770 \mysyn{let} & \myb{\mytmm_1} & \mapsto & \myapp{\myfst}{\mytmt_1} : \mytya_1 \\
1771 & \myb{\mytmn_1} & \mapsto & \myapp{\mysnd}{\mytmt_1} : \mysub{\mytyb_1}{\myb{x_1}}{\myb{\mytmm_1}} \\
1772 & \myb{Q_A} & \mapsto & \myapp{\myfst}{\myse{Q}} : \mytya_1 \myeq \mytya_2 \\
1773 & \myb{\mytmm_2} & \mapsto & \mycoee{\mytya_1}{\mytya_2}{\myb{Q_A}}{\myb{\mytmm_1}} : \mytya_2 \\
1774 & \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}}} \\
1775 & \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}} \\
1776 \mysyn{in} & \multicolumn{3}{@{}l}{\mypair{\myb{\mytmm_2}}{\myb{\mytmn_2}}}
1779 \mycoe & (\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}) &
1780 (\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}) & \myse{Q} &
1784 \mycoe & (\myw{\myb{x_1}}{\mytya_1}{\mytyb_1}) &
1785 (\myw{\myb{x_2}}{\mytya_2}{\mytyb_2}) & \myse{Q} &
1789 \mycoe & \mytya & \mytyb & \myse{Q} & \mytmt & \myred & \myapp{\myabsurd{\mytyb}}{\myse{Q}}\ \text{if $\mytya$ and $\mytyb$ are canonical.}
1793 \caption{Reducing type equalities, and using them when
1794 $\myfun{coe}$rcing.}
1798 Figure \ref{fig:eqred} illustrates this idea in practice. For ground
1799 types, the proof is the trivial element, and \myfun{coe} is the
1800 identity. For $\myunit$, we can do better: we return its only member
1801 without matching on the term. For the three type binders, things are
1802 similar but subtly different---the choices we make in the type equality
1803 are dictated by the desire of writing the $\myfun{coe}$ in a natural
1806 $\myprod$ is the easiest case: we decompose the proof into proofs that
1807 the first element's types are equal ($\mytya_1 \myeq \mytya_2$), and a
1808 proof that given equal values in the first element, the types of the
1809 second elements are equal too
1810 ($\myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{\myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2}}
1811 \myimpl \mytyb_1 \myeq \mytyb_2}$)\footnote{We are using $\myimpl$ to
1812 indicate a $\forall$ where we discard the first value. We write
1813 $\mytyb_1[\myb{x_1}]$ to indicate that the $\myb{x_1}$ in $\mytyb_1$
1814 is re-bound to the $\myb{x_1}$ quantified by the $\forall$, and
1815 similarly for $\myb{x_2}$ and $\mytyb_2$.}. This also explains the
1816 need for heterogeneous equality, since in the second proof it would be
1817 awkward to express the fact that $\myb{A_1}$ is the same as $\myb{A_2}$.
1818 In the respective $\myfun{coe}$ case, since the types are canonical, we
1819 know at this point that the proof of equality is a pair of the shape
1820 described above. Thus, we can immediately coerce the first element of
1821 the pair using the first element of the proof, and then instantiate the
1822 second element with the two first elements and a proof by coherence of
1823 their equality, since we know that the types are equal.
1825 The cases for the other binders are omitted for brevity, but they follow
1826 the same principle with some twists to make $\myfun{coe}$ work with the
1827 generated proofs; the reader can refer to the paper for details.
1829 \subsubsection{$\myfun{coe}$, laziness, and $\myfun{coh}$erence}
1831 It is important to notice that in the reduction rules for $\myfun{coe}$
1832 are never obstructed by the proofs: with the exception of comparisons
1833 between different canonical types we never `pattern match' on the proof
1834 pairs, but always look at the projections. This means that, as long as
1835 we are consistent, and thus as long as we don't have $\mybot$-inducing
1836 proofs, we can add propositional axioms for equality and $\myfun{coe}$
1837 will still compute. Thus, we can take $\myfun{coh}$ as axiomatic, and
1838 we can add back familiar useful equality rules:
1840 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1841 \AxiomC{$\myjud{\mytmt}{\mytya}$}
1842 \UnaryInfC{$\myjud{\myapp{\myrefl}{\mytmt}}{\myprdec{\myjm{\mytmt}{\mytya}{\mytmt}{\mytya}}}$}
1847 \AxiomC{$\myjud{\mytya}{\mytyp}$}
1848 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytyb}{\mytyp}$}
1849 \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}}}}}$}
1853 $\myrefl$ is the equivalent of the reflexivity rule in propositional
1854 equality, and $\mytyc{R}$ asserts that if we have a we have a $\mytyp$
1855 abstracting over a value we can substitute equal for equal---this lets
1856 us recover $\myfun{subst}$. Note that while we need to provide ad-hoc
1857 rules in the restricted, non-hierarchical theory that we have, if our
1858 theory supports abstraction over $\mytyp$s we can easily add these
1859 axioms as abstracted variables.
1861 \subsubsection{Value-level equality}
1863 \mydesc{equality reduction:}{\myprsyn \myred \myprsyn}{
1865 \begin{array}{r@{ }c@{\ }c@{\ }c@{}l@{\ }c@{\ }r@{}c@{\ }c@{\ }c@{}l@{\ }l}
1866 (&\mytmt_1 & : & \myempty&) & \myeq & (&\mytmt_2 & : & \myempty &) & \myred \mytop \\
1867 (&\mytmt_1 & : & \myunit&) & \myeq & (&\mytmt_2 & : & \myunit&) & \myred \mytop \\
1868 (&\mytrue & : & \mybool&) & \myeq & (&\mytrue & : & \mybool&) & \myred \mytop \\
1869 (&\myfalse & : & \mybool&) & \myeq & (&\myfalse & : & \mybool&) & \myred \mytop \\
1870 (&\mytrue & : & \mybool&) & \myeq & (&\myfalse & : & \mybool&) & \myred \mybot \\
1871 (&\myfalse & : & \mybool&) & \myeq & (&\mytrue & : & \mybool&) & \myred \mybot \\
1872 (&\mytmt_1 & : & \myexi{\mytya_1}{\myb{x_1}}{\mytyb_1}&) & \myeq & (&\mytmt_2 & : & \myexi{\mytya_2}{\myb{x_2}}{\mytyb_2}&) & \myred \\
1873 & \multicolumn{11}{@{}l}{
1874 \myind{2} \myjm{\myapp{\myfst}{\mytmt_1}}{\mytya_1}{\myapp{\myfst}{\mytmt_2}}{\mytya_2} \myand
1875 \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}}}
1877 (&\myse{f}_1 & : & \myfora{\mytya_1}{\myb{x_1}}{\mytyb_1}&) & \myeq & (&\myse{f}_2 & : & \myfora{\mytya_2}{\myb{x_2}}{\mytyb_2}&) & \myred \\
1878 & \multicolumn{11}{@{}l}{
1879 \myind{2} \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{
1880 \myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2} \myimpl
1881 \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}]}
1884 (&\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 \\
1885 (&\mytmt_1 & : & \mytya_1&) & \myeq & (&\mytmt_2 & : & \mytya_2 &) & \myred \mybot\ \text{if $\mytya_1$ and $\mytya_2$ are canonical.}
1890 As with type-level equality, we want value-level equality to reduce
1891 based on the structure of the compared terms. When matching
1892 propositional data, such as $\myempty$ and $\myunit$, we automatically
1893 return the trivial type, since if a type has zero one members, all
1894 members will be equal. When matching on data-bearing types, such as
1895 $\mybool$, we check that such data matches, and return bottom otherwise.
1897 \subsection{Proof irrelevance and stuck coercions}
1899 The last effort is required to make sure that proofs (members of
1900 $\myprop$) are \emph{irrelevant}. Since they are devoid of
1901 computational content, we would like to identify all equivalent
1902 propositions as the same, in a similar way as we identified all
1903 $\myempty$ and all $\myunit$ as the same in section
1904 \ref{sec:eta-expand}.
1906 Thus we will have a quotation that will not only perform
1907 $\eta$-expansion, but will also identify and mark proofs that could not
1908 be decoded (that is, equalities on neutral types). Then, when
1909 comparing terms, marked proofs will be considered equal without
1910 analysing their contents, thus gaining irrelevance.
1912 Moreover we can safely advance `stuck' $\myfun{coe}$rcions between
1913 non-canonical but definitionally equal types. Consider for example
1915 \mycoee{(\myITE{\myb{b}}{\mynat}{\mybool})}{(\myITE{\myb{b}}{\mynat}{\mybool})}{\myb{x}}
1916 \]} Where $\myb{b}$ and $\myb{x}$ are abstracted variables. This
1917 $\myfun{coe}$ will not advance, since the types are not canonical.
1918 However they are definitionally equal, and thus we can safely remove the
1919 coerce and return $\myb{x}$ as it is.
1921 This process of identifying every proof as equivalent and removing
1922 $\myfun{coe}$rcions is known as \emph{quotation}.
1924 \section{\mykant : the theory}
1925 \label{sec:kant-theory}
1927 \mykant\ is an interactive theorem prover developed as part of this thesis.
1928 The plan is to present a core language which would be capable of serving as
1929 the basis for a more featureful system, while still presenting interesting
1930 features and more importantly observational equality.
1932 We will first present the features of the system, and then describe the
1933 implementation we have developed in section \ref{sec:kant-practice}.
1935 The defining features of \mykant\ are:
1938 \item[Full dependent types] As we would expect, we have dependent a system
1939 which is as expressive as the `best' corner in the lambda cube described in
1940 section \ref{sec:itt}.
1942 \item[Implicit, cumulative universe hierarchy] The user does not need to
1943 specify universe level explicitly, and universes are \emph{cumulative}.
1945 \item[User defined data types and records] Instead of forcing the user to
1946 choose from a restricted toolbox, we let her define inductive data types,
1947 with associated primitive recursion operators; or records, with associated
1948 projections for each field.
1950 \item[Bidirectional type checking] While no `fancy' inference via
1951 unification is present, we take advantage of a type synthesis system
1952 in the style of \cite{Pierce2000}, extending the concept for user
1955 \item[Type holes] When building up programs interactively, it is useful to
1956 leave parts unfinished while exploring the current context. This is what
1959 \item[Observational equality] As described in section \ref{sec:ott} but
1960 extended to work with the type hierarchy and to admit equality between
1961 arbitrary data types.
1964 We will analyse the features one by one, along with motivations and
1965 tradeoffs for the design decisions made.
1967 \subsection{Bidirectional type checking}
1969 We start by describing bidirectional type checking since it calls for
1970 fairly different typing rules that what we have seen up to now. The
1971 idea is to have two kinds of terms: terms for which a type can always be
1972 inferred, and terms that need to be checked against a type. A nice
1973 observation is that this duality runs through the semantics of the
1974 terms: neutral terms (abstracted or defined variables, function
1975 application, record projections, primitive recursors, etc.) \emph{infer}
1976 types, canonical terms (abstractions, record/data types data
1977 constructors, etc.) need to be \emph{checked}.
1979 To introduce the concept and notation, we will revisit the STLC in a
1980 bidirectional style. The presentation follows \cite{Loh2010}. The
1981 syntax for our bidirectional STLC is the same as the untyped
1982 $\lambda$-calculus, but with an extra construct to annotate terms
1983 explicitly---this will be necessary when having top-level canonical
1984 terms. The types are the same as those found in the normal STLC.
1988 \begin{array}{r@{\ }c@{\ }l}
1989 \mytmsyn & ::= & \myb{x} \mysynsep \myabs{\myb{x}}{\mytmsyn} \mysynsep (\myapp{\mytmsyn}{\mytmsyn}) \mysynsep (\mytmsyn : \mytysyn)
1991 $ } We will have two kinds of typing judgements: \emph{inference} and
1992 \emph{checking}. $\myinf{\mytmt}{\mytya}$ indicates that $\mytmt$
1993 infers the type $\mytya$, while $\mychk{\mytmt}{\mytya}$ can be checked
1994 against type $\mytya$. The type of variables in context is inferred,
1995 and so are annotate terms. The type of applications is inferred too,
1996 propagating types down the applied term. Abstractions are checked.
1997 Finally, we have a rule to check the type of an inferrable term.
1999 \mydesc{typing:}{\myctx \vdash \mytmsyn \Leftrightarrow \mytmsyn}{
2000 \begin{tabular}{ccc}
2001 \AxiomC{$\myctx(x) = A$}
2002 \UnaryInfC{$\myinf{\myb{x}}{A}$}
2005 \AxiomC{$\myjudd{\myctx;\myb{x} : A}{\mytmt}{\mytyb}$}
2006 \UnaryInfC{$\mychk{\myabs{x}{\mytmt}}{\mytyb}$}
2009 \AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$}
2010 \AxiomC{$\myjud{\mytmn}{\mytya}$}
2011 \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mytyb}$}
2018 \AxiomC{$\mychk{\mytmt}{\mytya}$}
2019 \UnaryInfC{$\myinf{\myann{\mytmt}{\mytya}}{\mytya}$}
2022 \AxiomC{$\myinf{\mytmt}{\mytya}$}
2023 \UnaryInfC{$\mychk{\mytmt}{\mytya}$}
2028 \subsection{Base terms and types}
2030 Let us begin by describing the primitives available without the user
2031 defining any data types, and without equality. The way we handle
2032 variables and substitution is left unspecified, and explained in section
2033 \ref{sec:term-repr}, along with other implementation issues. We are
2034 also going to give an account of the implicit type hierarchy separately
2035 in section \ref{sec:term-hierarchy}, so as not to clutter derivation
2036 rules too much, and just treat types as impredicative for the time
2041 \begin{array}{r@{\ }c@{\ }l}
2042 \mytmsyn & ::= & \mynamesyn \mysynsep \mytyp \\
2043 & | & \myfora{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
2044 \myabs{\myb{x}}{\mytmsyn} \mysynsep
2045 (\myapp{\mytmsyn}{\mytmsyn}) \mysynsep
2046 (\myann{\mytmsyn}{\mytmsyn}) \\
2047 \mynamesyn & ::= & \myb{x} \mysynsep \myfun{f}
2052 The syntax for our calculus includes just two basic constructs:
2053 abstractions and $\mytyp$s. Everything else will be provided by
2054 user-definable constructs. Since we let the user define values, we will
2055 need a context capable of carrying the body of variables along with
2058 Bound names and defined names are treated separately in the syntax, and
2059 while both can be associated to a type in the context, only defined
2060 names can be associated with a body:
2062 \mydesc{context validity:}{\myvalid{\myctx}}{
2063 \begin{tabular}{ccc}
2064 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
2065 \UnaryInfC{$\myvalid{\myemptyctx}$}
2068 \AxiomC{$\myjud{\mytya}{\mytyp}$}
2069 \AxiomC{$\mynamesyn \not\in \myctx$}
2070 \BinaryInfC{$\myvalid{\myctx ; \mynamesyn : \mytya}$}
2073 \AxiomC{$\myjud{\mytmt}{\mytya}$}
2074 \AxiomC{$\myfun{f} \not\in \myctx$}
2075 \BinaryInfC{$\myvalid{\myctx ; \myfun{f} \mapsto \mytmt : \mytya}$}
2080 Now we can present the reduction rules, which are unsurprising. We have
2081 the usual function application ($\beta$-reduction), but also a rule to
2082 replace names with their bodies ($\delta$-reduction), and one to discard
2083 type annotations. For this reason reduction is done in-context, as
2084 opposed to what we have seen in the past:
2086 \mydesc{reduction:}{\myctx \vdash \mytmsyn \myred \mytmsyn}{
2087 \begin{tabular}{ccc}
2088 \AxiomC{\phantom{$\myb{x} \mapsto \mytmt : \mytya \in \myctx$}}
2089 \UnaryInfC{$\myctx \vdash \myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn}
2090 \myred \mysub{\mytmm}{\myb{x}}{\mytmn}$}
2093 \AxiomC{$\myfun{f} \mapsto \mytmt : \mytya \in \myctx$}
2094 \UnaryInfC{$\myctx \vdash \myfun{f} \myred \mytmt$}
2097 \AxiomC{\phantom{$\myb{x} \mapsto \mytmt : \mytya \in \myctx$}}
2098 \UnaryInfC{$\myctx \vdash \myann{\mytmm}{\mytya} \myred \mytmm$}
2103 We can now give types to our terms. We defer the question of term
2104 equality (which is needed for type checking) to section
2107 \mydesc{typing:}{\myctx \vdash \mytmsyn \Leftrightarrow \mytmsyn}{
2108 \begin{tabular}{cccc}
2109 \AxiomC{$\myse{name} : A \in \myctx$}
2110 \UnaryInfC{$\myinf{\myse{name}}{A}$}
2113 \AxiomC{$\myfun{f} \mapsto \mytmt : A \in \myctx$}
2114 \UnaryInfC{$\myinf{\myfun{f}}{A}$}
2117 \AxiomC{$\mychk{\mytmt}{\mytya}$}
2118 \UnaryInfC{$\myinf{\myann{\mytmt}{\mytya}}{\mytya}$}
2121 \AxiomC{$\myinf{\mytmt}{\mytya}$}
2122 \UnaryInfC{$\mychk{\mytmt}{\mytya}$}
2127 \begin{tabular}{ccc}
2128 \AxiomC{$\myinf{\mytmm}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
2129 \AxiomC{$\mychk{\mytmn}{\mytya}$}
2130 \BinaryInfC{$\myinf{\myapp{\mytmm}{\mytmn}}{\mysub{\mytyb}{\myb{x}}{\mytmn}}$}
2135 \AxiomC{$\mychkk{\myctx; \myb{x}: \mytya}{\mytmt}{\mytyb}$}
2136 \UnaryInfC{$\mychk{\myabs{\myb{x}}{\mytmt}}{\myfora{\myb{x}}{\mytyb}{\mytyb}}$}
2141 \subsection{Elaboration}
2143 As we mentioned, $\mykant$\ allows the user to define not only values
2144 but also custom data types and records. \emph{Elaboration} consists of
2145 turning these declarations into workable syntax, types, and reduction
2146 rules. The treatment of custom types in $\mykant$\ is heavily inspired
2147 by McBride and McKinna early work on Epigram \citep{McBride2004},
2148 although with some differences.
2150 \subsubsection{Term vectors, telescopes, and assorted notation}
2152 We use a vector notation to refer to a series of term applied to
2153 another, for example $\mytyc{D} \myappsp \vec{A}$ is a shorthand for
2154 $\mytyc{D} \myappsp \mytya_1 \cdots \mytya_n$, for some $n$. $n$ is
2155 consistently used to refer to the length of such vectors, and $i$ to
2156 refer to an index in such vectors. We also often need to `build up'
2157 terms vectors, in which case we use $\myemptyctx$ for an empty vector
2158 and add elements to an existing vector with $\myarg ; \myarg$, similarly
2159 to what we do for context.
2161 To present the elaboration and operations on user defined data types, we
2162 frequently make use what de Bruijn called \emph{telescopes}
2163 \citep{Bruijn91}, a construct that will prove useful when dealing with
2164 the types of type and data constructors. A telescope is a series of
2165 nested typed bindings, such as $(\myb{x} {:} \mynat); (\myb{p} {:}
2166 \myapp{\myfun{even}}{\myb{x}})$. Consistently with the notation for
2167 contexts and term vectors, we use $\myemptyctx$ to denote an empty
2168 telescope and $\myarg ; \myarg$ to add a new binding to an existing
2171 We refer to telescopes with $\mytele$, $\mytele'$, $\mytele_i$, etc. If
2172 $\mytele$ refers to a telescope, $\mytelee$ refers to the term vector
2173 made up of all the variables bound by $\mytele$. $\mytele \myarr
2174 \mytya$ refers to the type made by turning the telescope into a series
2175 of $\myarr$. Returning to the examples above, we have that
2177 (\myb{x} {:} \mynat); (\myb{p} : \myapp{\myfun{even}}{\myb{x}}) \myarr \mynat =
2178 (\myb{x} {:} \mynat) \myarr (\myb{p} : \myapp{\myfun{even}}{\myb{x}}) \myarr \mynat
2181 We make use of various operations to manipulate telescopes:
2183 \item $\myhead(\mytele)$ refers to the first type appearing in
2184 $\mytele$: $\myhead((\myb{x} {:} \mynat); (\myb{p} :
2185 \myapp{\myfun{even}}{\myb{x}})) = \mynat$. Similarly,
2186 $\myix_i(\mytele)$ refers to the $i^{th}$ type in a telescope
2188 \item $\mytake_i(\mytele)$ refers to the telescope created by taking the
2189 first $i$ elements of $\mytele$: $\mytake_1((\myb{x} {:} \mynat); (\myb{p} :
2190 \myapp{\myfun{even}}{\myb{x}})) = (\myb{x} {:} \mynat)$
2191 \item $\mytele \vec{A}$ refers to the telescope made by `applying' the
2192 terms in $\vec{A}$ on $\mytele$: $((\myb{x} {:} \mynat); (\myb{p} :
2193 \myapp{\myfun{even}}{\myb{x}}))42 = (\myb{p} :
2194 \myapp{\myfun{even}}{42})$.
2197 Additionally, when presenting syntax elaboration, I'll use $\mytmsyn^n$
2198 to indicate a term vector composed of $n$ elements, or
2199 $\mytmsyn^{\mytele}$ for one composed by as many elements as the
2202 \subsubsection{Declarations syntax}
2206 \begin{array}{r@{\ }c@{\ }l}
2207 \mydeclsyn & ::= & \myval{\myb{x}}{\mytmsyn}{\mytmsyn} \\
2208 & | & \mypost{\myb{x}}{\mytmsyn} \\
2209 & | & \myadt{\mytyc{D}}{\myappsp \mytelesyn}{}{\mydc{c} : \mytelesyn\ |\ \cdots } \\
2210 & | & \myreco{\mytyc{D}}{\myappsp \mytelesyn}{}{\myfun{f} : \mytmsyn,\ \cdots } \\
2212 \mytelesyn & ::= & \myemptytele \mysynsep \mytelesyn \mycc (\myb{x} {:} \mytmsyn) \\
2213 \mynamesyn & ::= & \cdots \mysynsep \mytyc{D} \mysynsep \mytyc{D}.\mydc{c} \mysynsep \mytyc{D}.\myfun{f}
2218 In \mykant\ we have four kind of declarations:
2221 \item[Defined value] A variable, together with a type and a body.
2222 \item[Abstract variable] An abstract variable, with a type but no body.
2223 \item[Inductive data] A datatype, with a type constructor and various data
2224 constructors---somewhat similar to what we find in Haskell. A primitive
2225 recursor (or `destructor') will be generated automatically.
2226 \item[Record] A record, which consists of one data constructor and various
2227 fields, with no recursive occurrences.
2230 Elaborating defined variables consists of type checking body against the
2231 given type, and updating the context to contain the new binding.
2232 Elaborating abstract variables and abstract variables consists of type
2233 checking the type, and updating the context with a new typed variable:
2235 \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
2237 \AxiomC{$\myjud{\mytmt}{\mytya}$}
2238 \AxiomC{$\myfun{f} \not\in \myctx$}
2240 $\myctx \myelabt \myval{\myfun{f}}{\mytya}{\mytmt} \ \ \myelabf\ \ \myctx; \myfun{f} \mapsto \mytmt : \mytya$
2244 \AxiomC{$\myjud{\mytya}{\mytyp}$}
2245 \AxiomC{$\myfun{f} \not\in \myctx$}
2248 \myctx \myelabt \mypost{\myfun{f}}{\mytya}
2249 \ \ \myelabf\ \ \myctx; \myfun{f} : \mytya
2256 \subsubsection{User defined types}
2257 \label{sec:user-type}
2259 Elaborating user defined types is the real effort. First, let's explain
2260 what we can defined, with some examples.
2263 \item[Natural numbers] To define natural numbers, we create a data type
2264 with two constructors: one with zero arguments ($\mydc{zero}$) and one
2265 with one recursive argument ($\mydc{suc}$):
2268 \myadt{\mynat}{ }{ }{
2269 \mydc{zero} \mydcsep \mydc{suc} \myappsp \mynat
2273 This is very similar to what we would write in Haskell:
2274 {\mysmall\[\text{\texttt{data Nat = Zero | Suc Nat}}\]}
2275 Once the data type is defined, $\mykant$\ will generate syntactic
2276 constructs for the type and data constructors, so that we will have
2279 \begin{tabular}{ccc}
2280 \AxiomC{\phantom{$\mychk{\mytmt}{\mynat}$}}
2281 \UnaryInfC{$\myinf{\mynat}{\mytyp}$}
2284 \AxiomC{\phantom{$\mychk{\mytmt}{\mynat}$}}
2285 \UnaryInfC{$\myinf{\mytyc{\mynat}.\mydc{zero}}{\mynat}$}
2288 \AxiomC{$\mychk{\mytmt}{\mynat}$}
2289 \UnaryInfC{$\myinf{\mytyc{\mynat}.\mydc{suc} \myappsp \mytmt}{\mynat}$}
2293 While in Haskell (or indeed in Agda or Coq) data constructors are
2294 treated the same way as functions, in $\mykant$\ they are syntax, so
2295 for example using $\mytyc{\mynat}.\mydc{suc}$ on its own will be a
2296 syntax error. This is necessary so that we can easily infer the type
2297 of polymorphic data constructors, as we will see later.
2299 Moreover, each data constructor is prefixed by the type constructor
2300 name, since we need to retrieve the type constructor of a data
2301 constructor when type checking. This measure aids in the presentation
2302 of various features but it is not needed in the implementation, where
2303 we can have a dictionary to lookup the type constructor corresponding
2304 to each data constructor. When using data constructors in examples I
2305 will omit the type constructor prefix for brevity.
2307 Along with user defined constructors, $\mykant$\ automatically
2308 generates an \emph{eliminator}, or \emph{destructor}, to compute with
2309 natural numbers: If we have $\mytmt : \mynat$, we can destruct
2310 $\mytmt$ using the generated eliminator `$\mynat.\myfun{elim}$':
2313 \AxiomC{$\mychk{\mytmt}{\mynat}$}
2315 \myinf{\mytyc{\mynat}.\myfun{elim} \myappsp \mytmt}{
2317 \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}}
2321 $\mynat.\myfun{elim}$ corresponds to the induction principle for
2322 natural numbers: if we have a predicate on numbers ($\myb{P}$), and we
2323 know that predicate holds for the base case
2324 ($\myapp{\myb{P}}{\mydc{zero}}$) and for each inductive step
2325 ($\myfora{\myb{x}}{\mynat}{\myapp{\myb{P}}{\myb{x}} \myarr
2326 \myapp{\myb{P}}{(\myapp{\mydc{suc}}{\myb{x}})}}$), then $\myb{P}$
2327 holds for any number. As with the data constructors, we require the
2328 eliminator to be applied to the `destructed' element.
2330 While the induction principle is usually seen as a mean to prove
2331 properties about numbers, in the intuitionistic setting it is also a
2332 mean to compute. In this specific case we will $\mynat.\myfun{elim}$
2333 will return the base case if the provided number is $\mydc{zero}$, and
2334 recursively apply the inductive step if the number is a
2337 \begin{array}{@{}l@{}l}
2338 \mytyc{\mynat}.\myfun{elim} \myappsp \mydc{zero} & \myappsp \myse{P} \myappsp \myse{pz} \myappsp \myse{ps} \myred \myse{pz} \\
2339 \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})
2342 The Haskell equivalent would be
2345 \text{\texttt{elim :: Nat -> a -> (Nat -> a -> a) -> a}}\\
2346 \text{\texttt{elim Zero pz ps = pz}}\\
2347 \text{\texttt{elim (Suc n) pz ps = ps n (elim n pz ps)}}
2350 Which buys us the computational behaviour, but not the reasoning power.
2352 \item[Binary trees] Now for a polymorphic data type: binary trees, since
2353 lists are too similar to natural numbers to be interesting.
2356 \myadt{\mytree}{\myappsp (\myb{A} {:} \mytyp)}{ }{
2357 \mydc{leaf} \mydcsep \mydc{node} \myappsp (\myapp{\mytree}{\myb{A}}) \myappsp \myb{A} \myappsp (\myapp{\mytree}{\myb{A}})
2361 Now the purpose of constructors as syntax can be explained: what would
2362 the type of $\mydc{leaf}$ be? If we were to treat it as a `normal'
2363 term, we would have to specify the type parameter of the tree each
2364 time the constructor is applied:
2366 \begin{array}{@{}l@{\ }l}
2367 \mydc{leaf} & : \myfora{\myb{A}}{\mytyp}{\myapp{\mytree}{\myb{A}}} \\
2368 \mydc{node} & : \myfora{\myb{A}}{\mytyp}{\myapp{\mytree}{\myb{A}} \myarr \myb{A} \myarr \myapp{\mytree}{\myb{A}} \myarr \myapp{\mytree}{\myb{A}}}
2371 The problem with this approach is that creating terms is incredibly
2372 verbose and dull, since we would need to specify the type parameters
2373 each time. For example if we wished to create a $\mytree \myappsp
2374 \mynat$ with two nodes and three leaves, we would have to write
2376 \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)
2378 The redundancy of $\mynat$s is quite irritating. Instead, if we treat
2379 constructors as syntactic elements, we can `extract' the type of the
2380 parameter from the type that the term gets checked against, much like
2381 we get the type of abstraction arguments:
2385 \AxiomC{$\mychk{\mytya}{\mytyp}$}
2386 \UnaryInfC{$\mychk{\mydc{leaf}}{\myapp{\mytree}{\mytya}}$}
2389 \AxiomC{$\mychk{\mytmm}{\mytree \myappsp \mytya}$}
2390 \AxiomC{$\mychk{\mytmt}{\mytya}$}
2391 \AxiomC{$\mychk{\mytmm}{\mytree \myappsp \mytya}$}
2392 \TrinaryInfC{$\mychk{\mydc{node} \myappsp \mytmm \myappsp \mytmt \myappsp \mytmn}{\mytree \myappsp \mytya}$}
2396 Which enables us to write, much more concisely
2398 \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}
2400 We gain an annotation, but we lose the myriad of types applied to the
2401 constructors. Conversely, with the eliminator for $\mytree$, we can
2402 infer the type of the arguments given the type of the destructed:
2405 \AxiomC{$\myinf{\mytmt}{\myapp{\mytree}{\mytya}}$}
2407 \myinf{\mytree.\myfun{elim} \myappsp \mytmt}{
2409 (\myb{P} {:} \myapp{\mytree}{\mytya} \myarr \mytyp) \myarr \\
2410 \myapp{\myb{P}}{\mydc{leaf}} \myarr \\
2411 ((\myb{l} {:} \myapp{\mytree}{\mytya}) (\myb{x} {:} \mytya) (\myb{r} {:} \myapp{\mytree}{\mytya}) \myarr \myapp{\myb{P}}{\myb{l}} \myarr
2412 \myapp{\myb{P}}{\myb{r}} \myarr \myb{P} \myappsp (\mydc{node} \myappsp \myb{l} \myappsp \myb{x} \myappsp \myb{r})) \myarr \\
2413 \myapp{\myb{P}}{\mytmt}
2418 As expected, the eliminator embodies structural induction on trees.
2420 \item[Empty type] We have presented types that have at least one
2421 constructors, but nothing prevents us from defining types with
2422 \emph{no} constructors:
2424 \myadt{\mytyc{Empty}}{ }{ }{ }
2426 What shall the `induction principle' on $\mytyc{Empty}$ be? Does it
2427 even make sense to talk about induction on $\mytyc{Empty}$?
2428 $\mykant$\ does not care, and generates an eliminator with no `cases',
2429 and thus corresponding to the $\myfun{absurd}$ that we know and love:
2432 \AxiomC{$\myinf{\mytmt}{\mytyc{Empty}}$}
2433 \UnaryInfC{$\myinf{\myempty.\myfun{elim} \myappsp \mytmt}{(\myb{P} {:} \mytmt \myarr \mytyp) \myarr \myapp{\myb{P}}{\mytmt}}$}
2436 \item[Ordered lists] Up to this point, the examples shown are nothing
2437 new to the \{Haskell, SML, OCaml, functional\} programmer. However
2438 dependent types let us express much more than that. A useful example
2439 is the type of ordered lists. There are many ways to define such a
2440 thing, we will define our type to store the bounds of the list, making
2441 sure that $\mydc{cons}$ing respects that.
2443 First, using $\myunit$ and $\myempty$, we define a type expressing the
2444 ordering on natural numbers, $\myfun{le}$---`less or equal'.
2445 $\myfun{le}\myappsp \mytmm \myappsp \mytmn$ will be inhabited only if
2446 $\mytmm \le \mytmn$:
2449 \myfun{le} : \mynat \myarr \mynat \myarr \mytyp \\
2450 \myfun{le} \myappsp \myb{n} \mapsto \\
2451 \myind{2} \mynat.\myfun{elim} \\
2452 \myind{2}\myind{2} \myb{n} \\
2453 \myind{2}\myind{2} (\myabs{\myarg}{\mynat \myarr \mytyp}) \\
2454 \myind{2}\myind{2} (\myabs{\myarg}{\myunit}) \\
2455 \myind{2}\myind{2} (\myabs{\myb{n}\, \myb{f}\, \myb{m}}{
2456 \mynat.\myfun{elim} \myappsp \myb{m} \myappsp (\myabs{\myarg}{\mytyp}) \myappsp \myempty \myappsp (\myabs{\myb{m'}\, \myarg}{\myapp{\myb{f}}{\myb{m'}}})
2459 \]} We return $\myunit$ if the scrutinised is $\mydc{zero}$ (every
2460 number in less or equal than zero), $\myempty$ if the first number is
2461 a $\mydc{suc}$cessor and the second a $\mydc{zero}$, and we recurse if
2462 they are both successors. Since we want the list to have possibly
2463 `open' bounds, for example for empty lists, we create a type for
2464 `lifted' naturals with a bottom (less than everything) and top
2465 (greater than everything) elements, along with an associated comparison
2469 \myadt{\mytyc{Lift}}{ }{ }{\mydc{bot} \mydcsep \mydc{lift} \myappsp \mynat \mydcsep \mydc{top}}\\
2470 \myfun{le'} : \mytyc{Lift} \myarr \mytyc{Lift} \myarr \mytyp\\
2471 \myfun{le'} \myappsp \myb{l_1} \mapsto \\
2472 \myind{2} \mytyc{Lift}.\myfun{elim} \\
2473 \myind{2}\myind{2} \myb{l_1} \\
2474 \myind{2}\myind{2} (\myabs{\myarg}{\mytyc{Lift} \myarr \mytyp}) \\
2475 \myind{2}\myind{2} (\myabs{\myarg}{\myunit}) \\
2476 \myind{2}\myind{2} (\myabs{\myb{n_1}\, \myb{n_2}}{
2477 \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
2479 \myind{2}\myind{2} (\myabs{\myb{n_1}\, \myb{n_2}}{
2480 \mytyc{Lift}.\myfun{elim} \myappsp \myb{l_2} \myappsp (\myabs{\myarg}{\mytyp}) \myappsp \myempty \myappsp (\myabs{\myarg}{\myempty}) \myappsp \myunit
2483 \]} Finally, we can defined a type of ordered lists. The type is
2484 parametrised over two values representing the lower and upper bounds
2485 of the elements, as opposed to the type parameters that we are used
2486 to. Then, an empty list will have to have evidence that the bounds
2487 are ordered, and each time we add an element we require the list to
2488 have a matching lower bound:
2491 \myadt{\mytyc{OList}}{\myappsp (\myb{low}\ \myb{upp} {:} \mytyc{Lift})}{\\ \myind{2}}{
2492 \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})
2495 \]} If we want we can then employ this structure to write and prove
2496 correct various sorting algorithms\footnote{See this presentation by
2498 \url{https://personal.cis.strath.ac.uk/conor.mcbride/Pivotal.pdf},
2499 and this blog post by the author:
2500 \url{http://mazzo.li/posts/AgdaSort.html}.}.
2502 \item[Dependent products] Apart from $\mysyn{data}$, $\mykant$\ offers
2503 us another way to define types: $\mysyn{record}$. A record is a
2504 datatype with one constructor and `projections' to extract specific
2505 fields of the said constructor.
2507 For example, we can recover dependent products:
2510 \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}}}
2513 Here $\myfst$ and $\mysnd$ are the projections, with their respective
2514 types. Note that each field can refer to the preceding fields. A
2515 constructor will be automatically generated, under the name of
2516 $\mytyc{Prod}.\mydc{constr}$. Dually to data types, we will omit the
2517 type constructor prefix for record projections.
2519 Following the bidirectionality of the system, we have that projections
2520 (the destructors of the record) infer the type, while the constructor
2525 \AxiomC{$\mychk{\mytmm}{\mytya}$}
2526 \AxiomC{$\mychk{\mytmn}{\myapp{\mytyb}{\mytmm}}$}
2527 \BinaryInfC{$\mychk{\mytyc{Prod}.\mydc{constr} \myappsp \mytmm \myappsp \mytmn}{\mytyc{Prod} \myappsp \mytya \myappsp \mytyb}$}
2529 \UnaryInfC{\phantom{$\myinf{\myfun{snd} \myappsp \mytmt}{\mytyb \myappsp (\myfst \myappsp \mytmt)}$}}
2532 \AxiomC{$\myinf{\mytmt}{\mytyc{Prod} \myappsp \mytya \myappsp \mytyb}$}
2533 \UnaryInfC{$\myinf{\myfun{fst} \myappsp \mytmt}{\mytya}$}
2535 \UnaryInfC{$\myinf{\myfun{snd} \myappsp \mytmt}{\mytyb \myappsp (\myfst \myappsp \mytmt)}$}
2539 What we have is equivalent to ITT's dependent products.
2547 \mynamesyn ::= \cdots \mysynsep \mytyc{D} \mysynsep \mytyc{D}.\mydc{c} \mysynsep \mytyc{D}.\myfun{f}
2554 \mydesc{syntax elaboration:}{\mydeclsyn \myelabf \mytmsyn ::= \cdots}{
2557 \begin{array}{r@{\ }l}
2558 & \myadt{\mytyc{D}}{\mytele}{}{\cdots\ |\ \mydc{c}_n : \mytele_n } \\
2561 \begin{array}{r@{\ }c@{\ }l}
2562 \mytmsyn & ::= & \cdots \mysynsep \myapp{\mytyc{D}}{\mytmsyn^{\mytele}} \mysynsep \cdots \mysynsep
2563 \mytyc{D}.\mydc{c}_n \myappsp \mytmsyn^{\mytele_n} \mysynsep \mytyc{D}.\myfun{elim} \myappsp \mytmsyn \\
2571 \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
2576 \myinf{\mytele \myarr \mytyp}{\mytyp}\hspace{0.8cm}
2577 \mytyc{D} \not\in \myctx \\
2578 \myinff{\myctx;\ \mytyc{D} : \mytele \myarr \mytyp}{\mytele \mycc \mytele_i \myarr \myapp{\mytyc{D}}{\mytelee}}{\mytyp}\ \ \ (1 \leq i \leq n) \\
2579 \text{For each $(\myb{x} {:} \mytya)$ in each $\mytele_i$, if $\mytyc{D} \in \mytya$, then $\mytya = \myapp{\mytyc{D}}{\vec{\mytmt}}$.}
2583 \begin{array}{r@{\ }c@{\ }l}
2584 \myctx & \myelabt & \myadt{\mytyc{D}}{\mytele}{}{ \cdots \ |\ \mydc{c}_n : \mytele_n } \\
2585 & & \vspace{-0.2cm} \\
2586 & \myelabf & \myctx;\ \mytyc{D} : \mytele \myarr \mytyp;\ \cdots;\ \mytyc{D}.\mydc{c}_n : \mytele \mycc \mytele_n \myarr \myapp{\mytyc{D}}{\mytelee}; \\
2588 \begin{array}{@{}r@{\ }l l}
2589 \mytyc{D}.\myfun{elim} : & \mytele \myarr (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr & \textbf{target} \\
2590 & (\myb{P} {:} \myapp{\mytyc{D}}{\mytelee} \myarr \mytyp) \myarr & \textbf{motive} \\
2594 (\mytele_n \mycc \myhyps(\myb{P}, \mytele_n) \myarr \myapp{\myb{P}}{(\myapp{\mytyc{D}.\mydc{c}_n}{\mytelee_n})}) \myarr
2595 \end{array} \right \}
2596 & \textbf{methods} \\
2597 & \myapp{\myb{P}}{\myb{x}} &
2601 \DisplayProof \\ \vspace{0.2cm}\ \\
2603 \begin{array}{@{}l l@{\ } l@{} r c l}
2604 \textbf{where} & \myhyps(\myb{P}, & \myemptytele &) & \mymetagoes & \myemptytele \\
2605 & \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) \\
2606 & \myhyps(\myb{P}, & (\myb{x} {:} \mytya) \mycc \mytele & ) & \mymetagoes & \myhyps(\myb{P}, \mytele)
2614 \mydesc{reduction elaboration:}{\mydeclsyn \myelabf \myctx \vdash \mytmsyn \myred \mytmsyn}{
2616 $\myadt{\mytyc{D}}{\mytele}{}{ \cdots \ |\ \mydc{c}_n : \mytele_n } \ \ \myelabf$
2617 \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
2618 \AxiomC{$\mytyc{D}.\mydc{c}_i : \mytele;\mytele_i \myarr \myapp{\mytyc{D}}{\mytelee} \in \myctx$}
2620 \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)}
2622 \DisplayProof \\ \vspace{0.2cm}\ \\
2624 \begin{array}{@{}l l@{\ } l@{} r c l}
2625 \textbf{where} & \myrecs(\myse{P}, \vec{m}, & \myemptytele &) & \mymetagoes & \myemptytele \\
2626 & \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) \\
2627 & \myrecs(\myse{P}, \vec{m}, & (\myb{x} {:} \mytya); \mytele &) & \mymetagoes & \myrecs(\myse{P}, \vec{m}, \mytele)
2634 \mydesc{syntax elaboration:}{\myelab{\mydeclsyn}{\mytmsyn ::= \cdots}}{
2637 \begin{array}{r@{\ }c@{\ }l}
2638 \myctx & \myelabt & \myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \\
2641 \begin{array}{r@{\ }c@{\ }l}
2642 \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 \\
2650 \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
2654 \myinf{\mytele \myarr \mytyp}{\mytyp}\hspace{0.8cm}
2655 \mytyc{D} \not\in \myctx \\
2656 \myinff{\myctx; \mytele; (\myb{f}_j : \myse{F}_j)_{j=1}^{i - 1}}{F_i}{\mytyp} \myind{3} (1 \le i \le n)
2660 \begin{array}{r@{\ }c@{\ }l}
2661 \myctx & \myelabt & \myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \\
2662 & & \vspace{-0.2cm} \\
2663 & \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}; \\
2664 & & \mytyc{D}.\mydc{constr} : \mytele \myarr \myse{F}_1 \myarr \cdots \myarr \myse{F}_n \myarr \myapp{\mytyc{D}}{\mytelee};
2672 \mydesc{reduction elaboration:}{\mydeclsyn \myelabf \myctx \vdash \mytmsyn \myred \mytmsyn}{
2674 $\myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \ \ \myelabf$
2675 \AxiomC{$\mytyc{D} \in \myctx$}
2676 \UnaryInfC{$\myctx \vdash \myapp{\mytyc{D}.\myfun{f}_i}{(\mytyc{D}.\mydc{constr} \myappsp \vec{t})} \myred t_i$}
2680 \caption{Elaboration for data types and records.}
2684 Following the intuition given by the examples, the mechanised
2685 elaboration is presented in figure \ref{fig:elab}, which is essentially
2686 a modification of figure 9 of \citep{McBride2004}\footnote{However, our
2687 datatypes do not have indices, we do bidirectional typechecking by
2688 treating constructors/destructors as syntactic constructs, and we have
2691 In data types declarations we allow recursive occurrences as long as
2692 they are \emph{strictly positive}, employing a syntactic check to make
2693 sure that this is the case. See \cite{Dybjer1991} for a more formal
2694 treatment of inductive definitions in ITT.
2696 For what concerns records, recursive occurrences are disallowed. The
2697 reason for this choice is answered by the reason for the choice of
2698 having records at all: we need records to give the user types with
2699 $\eta$-laws for equality, as we saw in section \ref{sec:eta-expand}
2700 and in the treatment of OTT in section \ref{sec:ott}. If we tried to
2701 $\eta$-expand recursive data types, we would expand forever.
2703 To implement bidirectional type checking for constructors and
2704 destructors, we store their types in full in the context, and then
2705 instantiate when due:
2707 \mydesc{typing:}{\myctx \vdash \mytmsyn \Leftrightarrow \mytmsyn}{
2710 \mytyc{D} : \mytele \myarr \mytyp \in \myctx \hspace{1cm}
2711 \mytyc{D}.\mydc{c} : \mytele \mycc \mytele' \myarr
2712 \myapp{\mytyc{D}}{\mytelee} \in \myctx \\
2713 \mytele'' = (\mytele;\mytele')\vec{A} \hspace{1cm}
2714 \mychkk{\myctx; \mytake_{i-1}(\mytele'')}{t_i}{\myix_i( \mytele'')}\ \
2715 (1 \le i \le \mytele'')
2718 \UnaryInfC{$\mychk{\myapp{\mytyc{D}.\mydc{c}}{\vec{t}}}{\myapp{\mytyc{D}}{\vec{A}}}$}
2723 \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
2724 \AxiomC{$\mytyc{D}.\myfun{f} : \mytele \mycc (\myb{x} {:}
2725 \myapp{\mytyc{D}}{\mytelee}) \myarr \myse{F}$}
2726 \AxiomC{$\myjud{\mytmt}{\myapp{\mytyc{D}}{\vec{A}}}$}
2727 \TrinaryInfC{$\myinf{\myapp{\mytyc{D}.\myfun{f}}{\mytmt}}{(\mytele
2728 \mycc (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr
2729 \myse{F})(\vec{A};\mytmt)}$}
2733 \subsubsection{Why user defined types? Why eliminators?}
2735 % TODO reference levitated theories, indexed containers
2739 \subsection{Cumulative hierarchy and typical ambiguity}
2740 \label{sec:term-hierarchy}
2742 A type hierarchy as presented in section \label{sec:itt} is a
2743 considerable burden on the user, on various levels. Consider for
2744 example how we recovered disjunctions in section \ref{sec:disju}: we
2745 have a function that takes two $\mytyp_0$ and forms a new $\mytyp_0$.
2746 What if we wanted to form a disjunction containing something a
2747 $\mytyp_1$, or $\mytyp_{42}$? Our definition would fail us, since
2748 $\mytyp_1 : \mytyp_2$.
2753 \mydesc{cumulativity:}{\myctx \vdash \mytmsyn \mycumul \mytmsyn}{
2754 \begin{tabular}{ccc}
2755 \AxiomC{\phantom{$\myctx \vdash \mytya \mycumul \mytyb$}}
2756 \UnaryInfC{$\myctx \vdash \mytya \mycumul \mytya$}
2759 \AxiomC{\phantom{$\myctx \vdash \mytya \mydefeq \mytyb$}}
2760 \UnaryInfC{$\myctx \vdash \mytyp_l \mycumul \mytyp_{l+1}$}
2763 \AxiomC{$\myctx \vdash \mytya \mycumul \mytyb$}
2764 \AxiomC{$\myctx \vdash \mytyb \mycumul \myse{C}$}
2765 \BinaryInfC{$\myctx \vdash \mytya \mycumul \myse{C}$}
2771 \begin{tabular}{ccc}
2772 \AxiomC{$\myctx \vdash \mytya_1 \ \mytyb$}
2773 \UnaryInfC{$\myctx \vdash \mytya \mycumul \mytyb$}
2776 \AxiomC{\phantom{$\myctx \vdash \mytya \mydefeq \mytyb$}}
2777 \UnaryInfC{$\myctx \vdash \mytyp_l \mycumul \mytyp_{l+1}$}
2780 \AxiomC{$\myctx \vdash \mytya \mycumul \mytyb$}
2781 \AxiomC{$\myctx \vdash \mytyb \mycumul \myse{C}$}
2782 \BinaryInfC{$\myctx \vdash \mytya \mycumul \myse{C}$}
2786 \caption{Cumulativity rules for \mykant, plus a `conversion' rule for
2788 \label{fig:cumulativity}
2791 One way to solve this issue is a \emph{cumulative} hierarchy, where
2792 $\mytyp_{l_1} : \mytyp_{l_2}$ iff $l_1 < l_2$. This way we retain
2793 consistency, while allowing for `large' definitions that work on small
2794 types too. Figure \ref{fig:cumulativity} gives a formal definition of
2795 cumulativity for types, abstractions, and data constructors.
2797 For example we might define our disjunction to be
2799 \myarg\myfun{$\vee$}\myarg : \mytyp_{100} \myarr \mytyp_{100} \myarr \mytyp_{100}
2801 And hope that $\mytyp_{100}$ will be large enough to fit all the types
2802 that we want to use with our disjunction. However, there are two
2803 problems with this. First, there is the obvious clumsyness of having to
2804 manually specify the size of types. More importantly, if we want to use
2805 $\myfun{$\vee$}$ itself as an argument to other type-formers, we need to
2806 make sure that those allow for types at least as large as
2809 A better option is to employ a mechanised version of what Russell called
2810 \emph{typical ambiguity}: we let the user live under the illusion that
2811 $\mytyp : \mytyp$, but check that the statements about types are
2812 consistent behind the hood. $\mykant$\ implements this following the
2813 lines of \cite{Huet1988}. See also \citep{Harper1991} for a published
2814 reference, although describing a more complex system allowing for both
2815 explicit and explicit hierarchy at the same time.
2817 We define a partial ordering on the levels, with both weak ($\le$) and
2818 strong ($<$) constraints---the laws governing them being the same as the
2819 ones governing $<$ and $\le$ for the natural numbers. Each occurrence
2820 of $\mytyp$ is decorated with a unique reference, and we keep a set of
2821 constraints and add new constraints as we type check, generating new
2822 references when needed.
2824 For example, when type checking the type $\mytyp\, r_1$, where $r_1$
2825 denotes the unique reference assigned to that term, we will generate a
2826 new fresh reference $\mytyp\, r_2$, and add the constraint $r_1 < r_2$
2827 to the set. When type checking $\myctx \vdash
2828 \myfora{\myb{x}}{\mytya}{\mytyb}$, if $\myctx \vdash \mytya : \mytyp\,
2829 r_1$ and $\myctx; \myb{x} : \mytyb \vdash \mytyb : \mytyp\,r_2$; we will
2830 generate new reference $r$ and add $r_1 \le r$ and $r_2 \le r$ to the
2833 If at any point the constraint set becomes inconsistent, type checking
2834 fails. Moreover, when comparing two $\mytyp$ terms we equate their
2835 respective references with two $\le$ constraints---the details are
2836 explained in section \ref{sec:hier-impl}.
2838 Another more flexible but also more verbose alternative is the one
2839 chosen by Agda, where levels can be quantified so that the relationship
2840 between arguments and result in type formers can be explicitly
2843 \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}
2845 Inference algorithms to automatically derive this kind of relationship
2846 are currently subject of research. We chose less flexible but more
2847 concise way, since it is easier to implement and better understood.
2851 % \caption{Constraints generated by the typical ambiguity engine. We
2852 % assume some global set of constraints with the ability of generating
2853 % fresh references.}
2854 % \label{fig:hierarchy}
2857 \subsection{Observational equality, \mykant\ style}
2859 There are two correlated differences between $\mykant$\ and the theory
2860 used to present OTT. The first is that in $\mykant$ we have a type
2861 hierarchy, which lets us, for example, abstract over types. The second
2862 is that we let the user define inductive types.
2864 Reconciling propositions for OTT and a hierarchy had already been
2865 investigated by Conor McBride\footnote{See
2866 \url{http://www.e-pig.org/epilogue/index.html?p=1098.html}.}, and we
2867 follow his broad design plan, although with some modifications. Most of
2868 the work, as an extension of elaboration, is to handle reduction rules
2869 and coercions for data types---both type constructors and data
2872 \subsubsection{The \mykant\ prelude, and $\myprop$ositions}
2874 Before defining $\myprop$, we define some basic types inside $\mykant$,
2875 as the target for the $\myprop$ decoder:
2878 \myadt{\mytyc{Empty}}{}{ }{ } \\
2879 \myfun{absurd} : (\myb{A} {:} \mytyp) \myarr \mytyc{Empty} \myarr \myb{A} \mapsto \\
2880 \myind{2} \myabs{\myb{A\ \myb{bot}}}{\mytyc{Empty}.\myfun{elim} \myappsp \myb{bot} \myappsp (\myabs{\_}{\myb{A}})} \\
2883 \myreco{\mytyc{Unit}}{}{}{ } \\ \ \\
2885 \myreco{\mytyc{Prod}}{\myappsp (\myb{A}\ \myb{B} {:} \mytyp)}{ }{\myfun{fst} : \myb{A}, \myfun{snd} : \myb{B} }
2888 When using $\mytyc{Prod}$, we shall use $\myprod$ to define `nested'
2889 products, and $\myproj{n}$ to project elements from them, so that
2893 \mytya \myprod \mytyb = \mytyc{Prod} \myappsp \mytya \myappsp (\mytyc{Prod} \myappsp \mytyb \myappsp \myunit) \\
2894 \mytya \myprod \mytyb \myprod \myse{C} = \mytyc{Prod} \myappsp \mytya \myappsp (\mytyc{Prod} \myappsp \mytyb \myappsp (\mytyc{Prod} \myappsp \mytyc \myappsp \myunit)) \\
2896 \myproj{1} : \mytyc{Prod} \myappsp \mytya \myappsp \mytyb \myarr \mytya \\
2897 \myproj{2} : \mytyc{Prod} \myappsp \mytya \myappsp (\mytyc{Prod} \myappsp \mytyb \myappsp \myse{C}) \myarr \mytyb \\
2902 And so on, so that $\myproj{n}$ will work with all products with at
2903 least than $n$ elements. Then we can define propositions, and decoding:
2907 \begin{array}{r@{\ }c@{\ }l}
2908 \mytmsyn & ::= & \cdots \mysynsep \myprdec{\myprsyn} \\
2909 \myprsyn & ::= & \mybot \mysynsep \mytop \mysynsep \myprsyn \myand \myprsyn \mysynsep \myprfora{\myb{x}}{\mytmsyn}{\myprsyn}
2914 \mydesc{proposition decoding:}{\myprdec{\mytmsyn} \myred \mytmsyn}{
2917 \begin{array}{l@{\ }c@{\ }l}
2918 \myprdec{\mybot} & \myred & \myempty \\
2919 \myprdec{\mytop} & \myred & \myunit
2924 \begin{array}{r@{ }c@{ }l@{\ }c@{\ }l}
2925 \myprdec{&\myse{P} \myand \myse{Q} &} & \myred & \myprdec{\myse{P}} \myprod \myprdec{\myse{Q}} \\
2926 \myprdec{&\myprfora{\myb{x}}{\mytya}{\myse{P}} &} & \myred &
2927 \myfora{\myb{x}}{\mytya}{\myprdec{\myse{P}}}
2933 Adopting the same convention as with $\mytyp$-level products, we will
2934 nest $\myand$ in the same way.
2936 \subsubsection{Some OTT examples}
2938 Before presenting the direction that $\mykant$\ takes, let's consider
2939 some examples of use-defined data types, and the result we would expect,
2940 given what we already know about OTT, assuming the same propositional
2945 \item[Product types] Let's consider first the already mentioned
2946 dependent product, using the alternate name $\mysigma$\footnote{For
2947 extra confusion, `dependent products' are often called `dependent
2948 sums' in the literature, referring to the interpretation that
2949 identifies the first element as a `tag' deciding the type of the
2950 second element, which lets us recover sum types (disjuctions), as we
2951 saw in section \ref{sec:user-type}. Thus, $\mysigma$.} to
2952 avoid confusion with the $\mytyc{Prod}$ in the prelude: {\mysmall\[
2954 \myreco{\mysigma}{\myappsp (\myb{A} {:} \mytyp) \myappsp (\myb{B} {:} \myb{A} \myarr \mytyp)}{\\ \myind{2}}{\myfst : \myb{A}, \mysnd : \myapp{\myb{B}}{\myb{fst}}}
2956 \]} Let's start with type-level equality. The result we want is
2959 \mysigma \myappsp \mytya_1 \myappsp \mytyb_1 \myeq \mysigma \myappsp \mytya_2 \myappsp \mytyb_2 \myred \\
2960 \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}}}
2962 \]} The difference here is that in the original presentation of OTT
2963 the type binders are explicit, while here $\mytyb_1$ and $\mytyb_2$
2964 functions returning types. We can do this thanks to the type
2965 hierarchy, and this hints at the fact that heterogeneous equality will
2966 have to allow $\mytyp$ `to the right of the colon', and in fact this
2967 provides the solution to simplify the equality above.
2969 If we take, just like we saw previously in OTT
2972 \myjm{\myse{f}_1}{\myfora{\mytya_1}{\myb{x_1}}{\mytyb_1}}{\myse{f}_2}{\myfora{\mytya_2}{\myb{x_2}}{\mytyb_2}} \myred \\
2973 \myind{2} \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{
2974 \myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2} \myimpl
2975 \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}]}
2978 \]} Then we can simply take
2981 \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}
2983 \]} Which will reduce to precisely what we desire. For what
2984 concerns coercions and quotation, things stay the same (apart from the
2985 fact that we apply to the second argument instead of substituting).
2986 We can recognise records such as $\mysigma$ as such and employ
2987 projections in value equality, coercions, and quotation; as to not
2988 impede progress if not necessary.
2990 \item[Lists] Now for finite lists, which will give us a taste for data
2994 \myadt{\mylist}{\myappsp (\myb{A} {:} \mytyp)}{ }{\mydc{nil} \mydcsep \mydc{cons} \myappsp \myb{A} \myappsp (\myapp{\mylist}{\myb{A}})}
2997 Type equality is simple---we only need to compare the parameter:
2999 \mylist \myappsp \mytya_1 \myeq \mylist \myappsp \mytya_2 \myred \mytya_1 \myeq \mytya_2
3000 \]} For coercions, we transport based on the constructor, recycling
3001 the proof for the inductive occurrence: {\mysmall\[
3002 \begin{array}{@{}l@{\ }c@{\ }l}
3003 \mycoe \myappsp (\mylist \myappsp \mytya_1) \myappsp (\mylist \myappsp \mytya_2) \myappsp \myse{Q} \myappsp \mydc{nil} & \myred & \mydc{nil} \\
3004 \mycoe \myappsp (\mylist \myappsp \mytya_1) \myappsp (\mylist \myappsp \mytya_2) \myappsp \myse{Q} \myappsp (\mydc{cons} \myappsp \mytmm \myappsp \mytmn) & \myred & \\
3005 \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)}
3007 \]} Value equality is unsurprising---we match the constructors, and
3008 return bottom for mismatches. However, we also need to equate the
3009 parameter in $\mydc{nil}$: {\mysmall\[
3010 \begin{array}{r@{ }c@{\ }c@{\ }c@{}l@{\ }c@{\ }r@{}c@{\ }c@{\ }c@{}l@{\ }l}
3011 (& \mydc{nil} & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{nil} & : & \myapp{\mylist}{\mytya_2} &) \myred \mytya_1 \myeq \mytya_2 \\
3012 (& \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 \\
3013 & \multicolumn{11}{@{}l}{ \myind{2}
3014 \myjm{\mytmm_1}{\mytya_1}{\mytmm_2}{\mytya_2} \myand \myjm{\mytmn_1}{\myapp{\mylist}{\mytya_1}}{\mytmn_2}{\myapp{\mylist}{\mytya_2}}
3016 (& \mydc{nil} & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{cons} \myappsp \mytmm_2 \myappsp \mytmn_2 & : & \myapp{\mylist}{\mytya_2} &) \myred \mybot \\
3017 (& \mydc{cons} \myappsp \mytmm_1 \myappsp \mytmn_1 & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{nil} & : & \myapp{\mylist}{\mytya_2} &) \myred \mybot
3024 Now for something useless but complicated.
3028 \subsubsection{Only one equality}
3030 Given the examples above, a more `flexible' heterogeneous emerged, since
3031 of the fact that in $\mykant$ we re-gain the possibility of abstracting
3032 and in general handling sets in a way that was not possible in the
3033 original OTT presentation. Moreover, we found that the rules for value
3034 equality work very well if used with user defined type
3035 abstractions---for example in the case of dependent products we recover
3036 the original definition with explicit binders, in a very simple manner.
3038 In fact, we can drop a separate notion of type-equality, which will
3039 simply be served by $\myjm{\mytya}{\mytyp}{\mytyb}{\mytyp}$, from now on
3040 abbreviated as $\mytya \myeq \mytyb$. We shall still distinguish
3041 equalities relating types for hierarchical purposes. The full rules for
3042 equality reductions, along with the syntax for propositions, are given
3043 in figure \ref{fig:kant-eq-red}. We exploit record to perform
3044 $\eta$-expansion. Moreover, given the nested $\myand$s, values of data
3045 types with zero constructors (such as $\myempty$) and records with zero
3046 destructors (such as $\myunit$) will be automatically always identified
3053 \begin{array}{r@{\ }c@{\ }l}
3054 \myprsyn & ::= & \cdots \mysynsep \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
3059 % \mytmsyn & ::= & \cdots \mysynsep \mycoee{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \mysynsep
3060 % \mycohh{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
3061 % \myprsyn & ::= & \cdots \mysynsep \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
3065 % \mydesc{typing:}{\myctx \vdash \mytmsyn \Leftrightarrow \mytmsyn}{
3067 % \begin{tabular}{cc}
3068 % \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
3069 % \AxiomC{$\myjud{\mytmt}{\mytya}$}
3070 % \BinaryInfC{$\myinf{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}$}
3073 % \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
3074 % \AxiomC{$\myjud{\mytmt}{\mytya}$}
3075 % \BinaryInfC{$\myinf{\mycohh{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\myprdec{\myjm{\mytmt}{\mytya}{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}}}$}
3082 \mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
3085 \AxiomC{\phantom{$\myjud{\myse{P}}{\myprop}$}}
3086 \UnaryInfC{$\myjud{\mytop}{\myprop}$}
3088 \UnaryInfC{$\myjud{\mybot}{\myprop}$}
3091 \AxiomC{$\myjud{\myse{P}}{\myprop}$}
3092 \AxiomC{$\myjud{\myse{Q}}{\myprop}$}
3093 \BinaryInfC{$\myjud{\myse{P} \myand \myse{Q}}{\myprop}$}
3095 \UnaryInfC{\phantom{$\myjud{\mybot}{\myprop}$}}
3104 \phantom{\myjud{\myse{A}}{\mytyp} \hspace{0.8cm} \myjud{\mytmm}{\myse{A}}} \\
3105 \myjud{\myse{A}}{\mytyp}\hspace{0.8cm}
3106 \myjudd{\myctx; \myb{x} : \mytya}{\myse{P}}{\myprop}
3109 \UnaryInfC{$\myjud{\myprfora{\myb{x}}{\mytya}{\myse{P}}}{\myprop}$}
3114 \myjud{\myse{A}}{\mytyp} \hspace{0.8cm} \myjud{\mytmm}{\myse{A}} \\
3115 \myjud{\myse{B}}{\mytyp} \hspace{0.8cm} \myjud{\mytmn}{\myse{B}}
3118 \UnaryInfC{$\myjud{\myjm{\mytmm}{\myse{A}}{\mytmn}{\myse{B}}}{\myprop}$}
3124 % TODO equality for decodings
3125 \mydesc{equality reduction:}{\myctx \vdash \myprsyn \myred \myprsyn}{
3129 \UnaryInfC{$\myctx \vdash \myjm{\mytyp}{\mytyp}{\mytyp}{\mytyp} \myred \mytop$}
3133 \UnaryInfC{$\myctx \vdash \myjm{\myprdec{\myse{P}}}{\mytyp}{\myprdec{\myse{Q}}}{\mytyp} \myred \mytop$}
3141 \begin{array}{@{}r@{\ }l}
3143 \myjm{\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}}{\mytyp}{\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}}{\mytyp} \myred \\
3144 & \myind{2} \mytya_2 \myeq \mytya_1 \myand \myprfora{\myb{x_2}}{\mytya_2}{\myprfora{\myb{x_1}}{\mytya_1}{
3145 \myjm{\myb{x_2}}{\mytya_2}{\myb{x_1}}{\mytya_1} \myimpl \mytyb_1[\myb{x_1}] \myeq \mytyb_2[\myb{x_2}]
3155 \begin{array}{@{}r@{\ }l}
3157 \myjm{\myse{f}_1}{\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}}{\myse{f}_2}{\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}} \myred \\
3158 & \myind{2} \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{
3159 \myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2} \myimpl
3160 \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}]}
3169 \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
3171 \begin{array}{r@{\ }l}
3173 \myjm{\mytyc{D} \myappsp \vec{A}}{\mytyp}{\mytyc{D} \myappsp \vec{B}}{\mytyp} \myred \\
3174 & \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}))})
3183 \mydataty(\mytyc{D}, \myctx)\hspace{0.8cm}
3184 \mytyc{D}.\mydc{c} : \mytele;\mytele' \myarr \mytyc{D} \myappsp \mytelee \in \myctx \hspace{0.8cm}
3185 \mytele_A = (\mytele;\mytele')\vec{A}\hspace{0.8cm}
3186 \mytele_B = (\mytele;\mytele')\vec{B}
3190 \begin{array}{@{}l@{\ }l}
3191 \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 \\
3192 & \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}))})
3199 \AxiomC{$\mydataty(\mytyc{D}, \myctx)$}
3201 \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
3209 \myisreco(\mytyc{D}, \myctx)\hspace{0.8cm}
3210 \mytyc{D}.\myfun{f}_i : \mytele; (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr \myse{F}_i \in \myctx\\
3214 \begin{array}{@{}l@{\ }l}
3215 \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})})
3222 \UnaryInfC{$\myjm{\mytmm}{\mytya}{\mytmn}{\mytyb} \myred \mybot\ \text{if $\mytya$ and $\mytyb$ are canonical types.}$}
3225 \caption{Propositions and equality reduction in $\mykant$. We assume
3226 the presence of $\mydataty$ and $\myisreco$ as operations on the
3227 context to recognise whether a user defined type is a data type or a
3229 \label{fig:kant-eq-red}
3232 \subsubsection{Coercions}
3235 % \mydesc{reduction}{\mytmsyn \myred \mytmsyn}{
3238 % \caption{Coercions in \mykant.}
3239 % \label{fig:kant-coe}
3244 \subsubsection{$\myprop$ and the hierarchy}
3246 Where is $\myprop$ placed in the type hierarchy? The main indicator
3247 is the decoding operator, since it converts into things that already
3248 live in the hierarchy. For example, if we
3250 \myprdec{\mynat \myarr \mybool \myeq \mynat \myarr \mybool} \myred
3251 \mytop \myand ((\myb{x}\, \myb{y} : \mynat) \myarr \mytop \myarr \mytop)
3252 \]} we will better make sure that the `to be decoded' is at the same
3253 level as its reduction as to preserve subject reduction. In the example
3254 above, we'll have that proposition to be at least as large as the type
3255 of $\mynat$, since the reduced proof will abstract over it. Pretending
3256 that we had explicit, non cumulative levels, it would be tempting to have
3259 \AxiomC{$\myjud{\myse{Q}}{\myprop_l}$}
3260 \UnaryInfC{$\myjud{\myprdec{\myse{Q}}}{\mytyp_l}$}
3263 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
3264 \AxiomC{$\myjud{\mytyb}{\mytyp_l}$}
3265 \BinaryInfC{$\myjud{\myjm{\mytya}{\mytyp_{l}}{\mytyb}{\mytyp_{l}}}{\myprop_l}$}
3269 $\mybot$ and $\mytop$ living at any level, $\myand$ and $\forall$
3270 following rules similar to the ones for $\myprod$ and $\myarr$ in
3271 section \ref{sec:itt}. However, we need to be careful with value
3272 equality since for example we have that {\mysmall\[
3273 \myprdec{\myjm{\myse{f}_1}{\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}}{\myse{f}_2}{\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}}}
3275 \myfora{\myb{x_1}}{\mytya_1}{\myfora{\myb{x_2}}{\mytya_2}{\cdots}}
3276 \]} where the proposition decodes into something of type
3277 $\mytyp_l$, where $\mytya : \mytyp_l$ and $\mytyb : \mytyp_l$. We
3278 can resolve this tension by making all equalities larger:
3280 \AxiomC{$\myjud{\mytmm}{\mytya}$}
3281 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
3282 \AxiomC{$\myjud{\mytmn}{\mytyb}$}
3283 \AxiomC{$\myjud{\mytyb}{\mytyp_l}$}
3284 \QuaternaryInfC{$\myjud{\myjm{\mytmm}{\mytya}{\mytmm}{\mytya}}{\myprop_l}$}
3286 This is disappointing, since type equalities will be needlessly large:
3287 $\myprdec{\myjm{\mytya}{\mytyp_l}{\mytyb}{\mytyp_l}} : \mytyp_{l + 1}$.
3289 However, considering that our theory is cumulative, we can do better.
3290 Assuming rules for $\myprop$ cumulativity similar to the ones for
3291 $\mytyp$, we will have (with the conversion rule reproduced as a
3295 \AxiomC{$\myctx \vdash \mytya \mycumul \mytyb$}
3296 \AxiomC{$\myjud{\mytmt}{\mytya}$}
3297 \BinaryInfC{$\myjud{\mytmt}{\mytyb}$}
3300 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
3301 \AxiomC{$\myjud{\mytyb}{\mytyp_l}$}
3302 \BinaryInfC{$\myjud{\myjm{\mytya}{\mytyp_{l}}{\mytyb}{\mytyp_{l}}}{\myprop_l}$}
3308 \AxiomC{$\myjud{\mytmm}{\mytya}$}
3309 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
3310 \AxiomC{$\myjud{\mytmn}{\mytyb}$}
3311 \AxiomC{$\myjud{\mytyb}{\mytyp_l}$}
3312 \AxiomC{$\mytya$ and $\mytyb$ are not $\mytyp_{l'}$}
3313 \QuinaryInfC{$\myjud{\myjm{\mytmm}{\mytya}{\mytmm}{\mytya}}{\myprop_l}$}
3317 That is, we are small when we can (type equalities) and large otherwise.
3318 This would not work in a non-cumulative theory because subject reduction
3319 would not hold. Consider for instance {\mysmall\[
3320 \myjm{\mynat}{\myITE{\mytrue}{\mytyp_0}{\mytyp_0}}{\mybool}{\myITE{\mytrue}{\mytyp_0}{\mytyp_0}}
3325 \myjm{\mynat}{\mytyp_0}{\mybool}{\mytyp_0} : \myprop_0
3326 \]} We need $\myprop_0$ to be $\myprop_1$ too, which will be the case
3327 with cumulativity. This is not the most elegant of systems, but it buys
3328 us a cheap type level equality without having to replicate functionality
3329 with a dedicated construct.
3331 \subsubsection{Quotation and term equality}
3332 \label{sec:kant-irr}
3335 % \mydesc{reduction}{\mytmsyn \myred \mytmsyn}{
3338 % \caption{Quotation in \mykant.}
3339 % \label{fig:kant-quot}
3344 \subsubsection{Why $\myprop$?}
3346 It is worth to ask if $\myprop$ is needed at all. It is perfectly
3347 possible to have the type checker identify propositional types
3348 automatically, and in fact in some sense we already do during equality
3349 reduction and quotation. However, this has the considerable
3350 disadvantage that we can never identify abstracted
3351 variables\footnote{And in general neutral terms, although we currently
3352 don't have neutral propositions.} of type $\mytyp$ as $\myprop$, thus
3353 forbidding the user to talk about $\myprop$ explicitly.
3355 This is a considerable impediment, for example when implementing
3356 \emph{quotient types}. With quotients, we let the user specify an
3357 equivalence class over a certain type, and then exploit this in various
3358 way---crucially, we need to be sure that the equivalence given is
3359 propositional, a fact which prevented the use of quotients in dependent
3360 type theories \citep{Jacobs1994}.
3364 \subsection{Type holes}
3366 \section{\mykant : The practice}
3367 \label{sec:kant-practice}
3369 The codebase consists of around 2500 lines of Haskell, as reported by
3370 the \texttt{cloc} utility. The high level design is inspired by Conor
3371 McBride's work on various incarnations of Epigram, and specifically by
3372 the first version as described \citep{McBride2004} and the codebase for
3373 the new version \footnote{Available intermittently as a \texttt{darcs}
3374 repository at \url{http://sneezy.cs.nott.ac.uk/darcs/Pig09}.}. In
3375 many ways \mykant\ is something in between the first and second version
3378 The author learnt the hard way the implementations challenges for such a
3379 project, and while there is a solid and working base to work on, the
3380 implementation of observational equality is not currently complete.
3381 However, given the detailed plan in the previous section, doing so would
3382 should not prove to be too much work.
3384 The interaction happens in a read-eval-print loop (REPL). The REPL is a
3385 available both as a commandline application and in a web interface,
3386 which is available at \url{kant.mazzo.li} and presents itself as in
3387 figure \ref{fig:kant-web}.
3391 \includegraphics[scale=1.0]{kant-web.png}
3393 \caption{The \mykant\ web prompt.}
3394 \label{fig:kant-web}
3397 The interaction with the user takes place in a loop living in and updating a
3398 context \mykant\ declarations. The user inputs a new declaration that goes
3399 through various stages starts with the user inputing a \mykant\ declaration or
3400 another REPL command, which then goes through various stages that can end up
3401 in a context update, or in failures of various kind. The process is described
3402 diagrammatically in figure \ref{fig:kant-process}:
3405 \item[Parse] In this phase the text input gets converted to a sugared
3406 version of the core language.
3408 \item[Desugar] The sugared declaration is converted to a core term.
3410 \item[Reference] Occurrences of $\mytyp$ get decorated by a unique reference,
3411 which is necessary to implement the type hierarchy check.
3413 \item[Elaborate] Convert the declaration to some context item, which might be
3414 a value declaration (type and body) or a data type declaration (constructors
3415 and destructors). This phase works in tandem with \textbf{Typechecking},
3416 which in turns needs to \textbf{Evaluate} terms.
3418 \item[Distill] and report the result. `Distilling' refers to the process of
3419 converting a core term back to a sugared version that the user can
3420 visualise. This can be necessary both to display errors including terms or
3421 to display result of evaluations or type checking that the user has
3424 \item[Pretty print] Format the terms in a nice way, and display the result to
3431 \tikzstyle{block} = [rectangle, draw, text width=5em, text centered, rounded
3432 corners, minimum height=2.5em, node distance=0.7cm]
3434 \tikzstyle{decision} = [diamond, draw, text width=4.5em, text badly
3435 centered, inner sep=0pt, node distance=0.7cm]
3437 \tikzstyle{line} = [draw, -latex']
3439 \tikzstyle{cloud} = [draw, ellipse, minimum height=2em, text width=5em, text
3440 centered, node distance=1.5cm]
3443 \begin{tikzpicture}[auto]
3444 \node [cloud] (user) {User};
3445 \node [block, below left=1cm and 0.1cm of user] (parse) {Parse};
3446 \node [block, below=of parse] (desugar) {Desugar};
3447 \node [block, below=of desugar] (reference) {Reference};
3448 \node [block, below=of reference] (elaborate) {Elaborate};
3449 \node [block, left=of elaborate] (tycheck) {Typecheck};
3450 \node [block, left=of tycheck] (evaluate) {Evaluate};
3451 \node [decision, right=of elaborate] (error) {Error?};
3452 \node [block, right=of parse] (distill) {Distill};
3453 \node [block, right=of desugar] (update) {Update context};
3455 \path [line] (user) -- (parse);
3456 \path [line] (parse) -- (desugar);
3457 \path [line] (desugar) -- (reference);
3458 \path [line] (reference) -- (elaborate);
3459 \path [line] (elaborate) edge[bend right] (tycheck);
3460 \path [line] (tycheck) edge[bend right] (elaborate);
3461 \path [line] (elaborate) -- (error);
3462 \path [line] (error) edge[out=0,in=0] node [near start] {yes} (distill);
3463 \path [line] (error) -- node [near start] {no} (update);
3464 \path [line] (update) -- (distill);
3465 \path [line] (distill) -- (user);
3466 \path [line] (tycheck) edge[bend right] (evaluate);
3467 \path [line] (evaluate) edge[bend right] (tycheck);
3470 \caption{High level overview of the life of a \mykant\ prompt cycle.}
3471 \label{fig:kant-process}
3474 \subsection{Parsing and \texttt{Sugar}}
3476 \subsection{Term representation and context}
3477 \label{sec:term-repr}
3479 \subsection{Type checking}
3481 \subsection{Type hierarchy}
3482 \label{sec:hier-impl}
3484 \subsection{Elaboration}
3486 \section{Evaluation}
3488 \section{Future work}
3490 \subsection{Coinduction}
3492 \subsection{Quotient types}
3494 \subsection{Partiality}
3496 \subsection{Pattern matching}
3498 \subsection{Pattern unification}
3500 % TODO coinduction (obscoin, gimenez, jacobs), pattern unification (miller,
3501 % gundry), partiality monad (NAD)
3505 \section{Notation and syntax}
3507 Syntax, derivation rules, and reduction rules, are enclosed in frames describing
3508 the type of relation being established and the syntactic elements appearing,
3511 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
3512 Typing derivations here.
3515 In the languages presented and Agda code samples I also highlight the syntax,
3516 following a uniform color and font convention:
3519 \begin{tabular}{c | l}
3520 $\mytyc{Sans}$ & Type constructors. \\
3521 $\mydc{sans}$ & Data constructors. \\
3522 % $\myfld{sans}$ & Field accessors (e.g. \myfld{fst} and \myfld{snd} for products). \\
3523 $\mysyn{roman}$ & Keywords of the language. \\
3524 $\myfun{roman}$ & Defined values and destructors. \\
3525 $\myb{math}$ & Bound variables.
3529 Moreover, I will from time to time give examples in the Haskell programming
3530 language as defined in \citep{Haskell2010}, which I will typeset in
3531 \texttt{teletype} font. I assume that the reader is already familiar with
3532 Haskell, plenty of good introductions are available \citep{LYAH,ProgInHask}.
3534 When presenting grammars, I will use a word in $\mysynel{math}$ font
3535 (e.g. $\mytmsyn$ or $\mytysyn$) to indicate indicate nonterminals. Additionally,
3536 I will use quite flexibly a $\mysynel{math}$ font to indicate a syntactic
3537 element. More specifically, terms are usually indicated by lowercase letters
3538 (often $\mytmt$, $\mytmm$, or $\mytmn$); and types by an uppercase letter (often
3539 $\mytya$, $\mytyb$, or $\mytycc$).
3541 When presenting type derivations, I will often abbreviate and present multiple
3542 conclusions, each on a separate line:
3544 \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
3545 \UnaryInfC{$\myjud{\myapp{\myfst}{\mytmt}}{\mytya}$}
3547 \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mytyb}$}
3550 I will often present `definition' in the described calculi and in
3551 $\mykant$\ itself, like so:
3554 \myfun{name} : \mytysyn \\
3555 \myfun{name} \myappsp \myb{arg_1} \myappsp \myb{arg_2} \myappsp \cdots \mapsto \mytmsyn
3558 To define operators, I use a mixfix notation similar
3559 to Agda, where $\myarg$s denote arguments, for example
3562 \myarg \mathrel{\myfun{$\wedge$}} \myarg : \mybool \myarr \mybool \myarr \mybool \\
3563 \myb{b_1} \mathrel{\myfun{$\wedge$}} \myb{b_2} \mapsto \cdots
3567 In explicitly typed systems, I will also omit type annotations when they
3568 are obvious, e.g. by not annotating the type of parameters of
3569 abstractions or of dependent pairs.
3573 \subsection{ITT renditions}
3574 \label{app:itt-code}
3576 \subsubsection{Agda}
3577 \label{app:agda-itt}
3579 Note that in what follows rules for `base' types are
3580 universe-polymorphic, to reflect the exposition. Derived definitions,
3581 on the other hand, mostly work with \mytyc{Set}, reflecting the fact
3582 that in the theory presented we don't have universe polymorphism.
3588 data Empty : Set where
3590 absurd : ∀ {a} {A : Set a} → Empty → A
3593 ¬_ : ∀ {a} → (A : Set a) → Set a
3596 record Unit : Set where
3599 record _×_ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
3606 data Bool : Set where
3609 if_/_then_else_ : ∀ {a} (x : Bool) (P : Bool → Set a) → P true → P false → P x
3610 if true / _ then x else _ = x
3611 if false / _ then _ else x = x
3613 if_then_else_ : ∀ {a} (x : Bool) {P : Bool → Set a} → P true → P false → P x
3614 if_then_else_ x {P} = if_/_then_else_ x P
3616 data W {s p} (S : Set s) (P : S → Set p) : Set (s ⊔ p) where
3617 _◁_ : (s : S) → (P s → W S P) → W S P
3619 rec : ∀ {a b} {S : Set a} {P : S → Set b}
3620 (C : W S P → Set) → -- some conclusion we hope holds
3621 ((s : S) → -- given a shape...
3622 (f : P s → W S P) → -- ...and a bunch of kids...
3623 ((p : P s) → C (f p)) → -- ...and C for each kid in the bunch...
3624 C (s ◁ f)) → -- ...does C hold for the node?
3625 (x : W S P) → -- If so, ...
3626 C x -- ...C always holds.
3627 rec C c (s ◁ f) = c s f (λ p → rec C c (f p))
3629 module Examples-→ where
3636 -- These pragmas are needed so we can use number literals.
3637 {-# BUILTIN NATURAL ℕ #-}
3638 {-# BUILTIN ZERO zero #-}
3639 {-# BUILTIN SUC suc #-}
3641 data List (A : Set) : Set where
3643 _∷_ : A → List A → List A
3645 length : ∀ {A} → List A → ℕ
3647 length (_ ∷ l) = suc (length l)
3652 suc x > suc y = x > y
3654 head : ∀ {A} → (l : List A) → length l > 0 → A
3655 head [] p = absurd p
3658 module Examples-× where
3664 even (suc zero) = Empty
3665 even (suc (suc n)) = even n
3670 5-not-even : ¬ (even 5)
3673 there-is-an-even-number : ℕ × even
3674 there-is-an-even-number = 6 , 6-even
3676 _∨_ : (A B : Set) → Set
3677 A ∨ B = Bool × (λ b → if b then A else B)
3679 left : ∀ {A B} → A → A ∨ B
3682 right : ∀ {A B} → B → A ∨ B
3685 [_,_] : {A B C : Set} → (A → C) → (B → C) → A ∨ B → C
3687 (if (fst x) / (λ b → if b then _ else _ → _) then f else g) (snd x)
3689 module Examples-W where
3694 Tr b = if b then Unit else Empty
3700 zero = false ◁ absurd
3703 suc n = true ◁ (λ _ → n)
3709 if b / (λ b → (Tr b → ℕ) → (Tr b → ℕ) → ℕ)
3710 then (λ _ f → (suc (f tt))) else (λ _ _ → y))
3713 List : (A : Set) → Set
3714 List A = W (A ∨ Unit) (λ s → Tr (fst s))
3717 [] = (false , tt) ◁ absurd
3719 _∷_ : ∀ {A} → A → List A → List A
3720 x ∷ l = (true , x) ◁ (λ _ → l)
3722 module Equality where
3725 data _≡_ {a} {A : Set a} : A → A → Set a where
3728 ≡-elim : ∀ {a b} {A : Set a}
3729 (P : (x y : A) → x ≡ y → Set b) →
3730 ∀ {x y} → P x x (refl x) → (x≡y : x ≡ y) → P x y x≡y
3731 ≡-elim P p (refl x) = p
3733 subst : ∀ {A : Set} (P : A → Set) → ∀ {x y} → (x≡y : x ≡ y) → P x → P y
3734 subst P x≡y p = ≡-elim (λ _ y _ → P y) p x≡y
3736 sym : ∀ {A : Set} (x y : A) → x ≡ y → y ≡ x
3737 sym x y p = subst (λ y′ → y′ ≡ x) p (refl x)
3739 trans : ∀ {A : Set} (x y z : A) → x ≡ y → y ≡ z → x ≡ z
3740 trans x y z p q = subst (λ z′ → x ≡ z′) q p
3742 cong : ∀ {A B : Set} (x y : A) → x ≡ y → (f : A → B) → f x ≡ f y
3743 cong x y p f = subst (λ z → f x ≡ f z) p (refl (f x))
3746 \subsubsection{\mykant}
3748 The following things are missing: $\mytyc{W}$-types, since our
3749 positivity check is overly strict, and equality, since we haven't
3750 implemented that yet.
3753 \verbatiminput{itt.ka}
3756 \subsection{\mykant\ examples}
3759 \verbatiminput{examples.ka}
3762 \subsection{\mykant's hierachy}
3764 This rendition of the Hurken's paradox does not type check with the
3765 hierachy enabled, type checks and loops without it. Adapted from an
3766 Agda version, available at
3767 \url{http://code.haskell.org/Agda/test/succeed/Hurkens.agda}.
3770 \verbatiminput{hurkens.ka}
3773 \bibliographystyle{authordate1}
3774 \bibliography{thesis}