2 %% THIS LATEX HURTS YOUR EYES. DO NOT READ.
5 \documentclass[11pt, fleqn]{article}
8 \usepackage[sc,slantedGreek]{mathpazo}
24 % \usepackage{fullpage}
36 \usepackage[fleqn]{amsmath}
37 \usepackage{stmaryrd} %llbracket
40 \usepackage{bussproofs}
52 \usepackage{subcaption}
57 \RecustomVerbatimEnvironment
63 \usetikzlibrary{shapes,arrows,positioning}
64 % \usepackage{tikz-cd}
65 % \usepackage{pgfplots}
68 %% -----------------------------------------------------------------------------
70 \usepackage[english]{babel}
71 \usepackage[conor]{agda}
72 \renewcommand{\AgdaKeywordFontStyle}[1]{\ensuremath{\mathrm{\underline{#1}}}}
73 \renewcommand{\AgdaFunction}[1]{\textbf{\textcolor{AgdaFunction}{#1}}}
74 \renewcommand{\AgdaField}{\AgdaFunction}
75 % \definecolor{AgdaBound} {HTML}{000000}
76 \definecolor{AgdaHole} {HTML} {FFFF33}
78 \DeclareUnicodeCharacter{9665}{\ensuremath{\lhd}}
79 \DeclareUnicodeCharacter{964}{\ensuremath{\tau}}
80 \DeclareUnicodeCharacter{963}{\ensuremath{\sigma}}
81 \DeclareUnicodeCharacter{915}{\ensuremath{\Gamma}}
82 \DeclareUnicodeCharacter{8799}{\ensuremath{\stackrel{?}{=}}}
83 \DeclareUnicodeCharacter{9655}{\ensuremath{\rhd}}
85 \renewenvironment{code}%
86 {\noindent\ignorespaces\advance\leftskip\mathindent\AgdaCodeStyle\pboxed\small}%
87 {\endpboxed\par\noindent%
88 \ignorespacesafterend\small}
91 %% -----------------------------------------------------------------------------
94 \newcommand{\mysmall}{}
95 \newcommand{\mysyn}{\AgdaKeyword}
96 \newcommand{\mytyc}{\AgdaDatatype}
97 \newcommand{\mydc}{\AgdaInductiveConstructor}
98 \newcommand{\myfld}{\AgdaField}
99 \newcommand{\myfun}{\AgdaFunction}
100 \newcommand{\myb}[1]{\AgdaBound{$#1$}}
101 \newcommand{\myfield}{\AgdaField}
102 \newcommand{\myind}{\AgdaIndent}
103 \newcommand{\mykant}{\textsc{Bertus}}
104 \newcommand{\mysynel}[1]{#1}
105 \newcommand{\myse}{\mysynel}
106 \newcommand{\mytmsyn}{\mysynel{term}}
107 \newcommand{\mysp}{\ }
108 \newcommand{\myabs}[2]{\mydc{$\lambda$} #1 \mathrel{\mydc{$\mapsto$}} #2}
109 \newcommand{\myappsp}{\hspace{0.07cm}}
110 \newcommand{\myapp}[2]{#1 \myappsp #2}
111 \newcommand{\mysynsep}{\ \ |\ \ }
112 \newcommand{\myITE}[3]{\myfun{If}\, #1\, \myfun{Then}\, #2\, \myfun{Else}\, #3}
113 \newcommand{\mycumul}{\preceq}
116 \newcommand{\mydesc}[3]{
122 \hfill \textbf{#1} $#2$
123 \framebox[\textwidth]{
138 \newcommand{\mytmt}{\mysynel{t}}
139 \newcommand{\mytmm}{\mysynel{m}}
140 \newcommand{\mytmn}{\mysynel{n}}
141 \newcommand{\myred}{\leadsto}
142 \newcommand{\mysub}[3]{#1[#2 / #3]}
143 \newcommand{\mytysyn}{\mysynel{type}}
144 \newcommand{\mybasetys}{K}
145 \newcommand{\mybasety}[1]{B_{#1}}
146 \newcommand{\mytya}{\myse{A}}
147 \newcommand{\mytyb}{\myse{B}}
148 \newcommand{\mytycc}{\myse{C}}
149 \newcommand{\myarr}{\mathrel{\textcolor{AgdaDatatype}{\to}}}
150 \newcommand{\myprod}{\mathrel{\textcolor{AgdaDatatype}{\times}}}
151 \newcommand{\myctx}{\Gamma}
152 \newcommand{\myvalid}[1]{#1 \vdash \underline{\mathrm{valid}}}
153 \newcommand{\myjudd}[3]{#1 \vdash #2 : #3}
154 \newcommand{\myjud}[2]{\myjudd{\myctx}{#1}{#2}}
155 \newcommand{\myabss}[3]{\mydc{$\lambda$} #1 {:} #2 \mathrel{\mydc{$\mapsto$}} #3}
156 \newcommand{\mytt}{\mydc{$\langle\rangle$}}
157 \newcommand{\myunit}{\mytyc{Unit}}
158 \newcommand{\mypair}[2]{\mathopen{\mydc{$\langle$}}#1\mathpunct{\mydc{,}} #2\mathclose{\mydc{$\rangle$}}}
159 \newcommand{\myfst}{\myfld{fst}}
160 \newcommand{\mysnd}{\myfld{snd}}
161 \newcommand{\myconst}{\myse{c}}
162 \newcommand{\myemptyctx}{\varepsilon}
163 \newcommand{\myhole}{\AgdaHole}
164 \newcommand{\myfix}[3]{\mysyn{fix} \myappsp #1 {:} #2 \mapsto #3}
165 \newcommand{\mysum}{\mathbin{\textcolor{AgdaDatatype}{+}}}
166 \newcommand{\myleft}[1]{\mydc{left}_{#1}}
167 \newcommand{\myright}[1]{\mydc{right}_{#1}}
168 \newcommand{\myempty}{\mytyc{Empty}}
169 \newcommand{\mycase}[2]{\mathopen{\myfun{[}}#1\mathpunct{\myfun{,}} #2 \mathclose{\myfun{]}}}
170 \newcommand{\myabsurd}[1]{\myfun{absurd}_{#1}}
171 \newcommand{\myarg}{\_}
172 \newcommand{\myderivsp}{}
173 \newcommand{\myderivspp}{\vspace{0.3cm}}
174 \newcommand{\mytyp}{\mytyc{Type}}
175 \newcommand{\myneg}{\myfun{$\neg$}}
176 \newcommand{\myar}{\,}
177 \newcommand{\mybool}{\mytyc{Bool}}
178 \newcommand{\mytrue}{\mydc{true}}
179 \newcommand{\myfalse}{\mydc{false}}
180 \newcommand{\myitee}[5]{\myfun{if}\,#1 / {#2.#3}\,\myfun{then}\,#4\,\myfun{else}\,#5}
181 \newcommand{\mynat}{\mytyc{$\mathbb{N}$}}
182 \newcommand{\myrat}{\mytyc{$\mathbb{R}$}}
183 \newcommand{\myite}[3]{\myfun{if}\,#1\,\myfun{then}\,#2\,\myfun{else}\,#3}
184 \newcommand{\myfora}[3]{(#1 {:} #2) \myarr #3}
185 \newcommand{\myexi}[3]{(#1 {:} #2) \myprod #3}
186 \newcommand{\mypairr}[4]{\mathopen{\mydc{$\langle$}}#1\mathpunct{\mydc{,}} #4\mathclose{\mydc{$\rangle$}}_{#2{.}#3}}
187 \newcommand{\mylist}{\mytyc{List}}
188 \newcommand{\mynil}[1]{\mydc{[]}_{#1}}
189 \newcommand{\mycons}{\mathbin{\mydc{∷}}}
190 \newcommand{\myfoldr}{\myfun{foldr}}
191 \newcommand{\myw}[3]{\myapp{\myapp{\mytyc{W}}{(#1 {:} #2)}}{#3}}
192 \newcommand{\mynodee}{\mathbin{\mydc{$\lhd$}}}
193 \newcommand{\mynode}[2]{\mynodee_{#1.#2}}
194 \newcommand{\myrec}[4]{\myfun{rec}\,#1 / {#2.#3}\,\myfun{with}\,#4}
195 \newcommand{\mylub}{\sqcup}
196 \newcommand{\mydefeq}{\cong}
197 \newcommand{\myrefl}{\mydc{refl}}
198 \newcommand{\mypeq}[1]{\mathrel{\mytyc{=}_{#1}}}
199 \newcommand{\myjeqq}{\myfun{$=$-elim}}
200 \newcommand{\myjeq}[3]{\myapp{\myapp{\myapp{\myjeqq}{#1}}{#2}}{#3}}
201 \newcommand{\mysubst}{\myfun{subst}}
202 \newcommand{\myprsyn}{\myse{prop}}
203 \newcommand{\myprdec}[1]{\mathopen{\mytyc{$\llbracket$}} #1 \mathclose{\mytyc{$\rrbracket$}}}
204 \newcommand{\myand}{\mathrel{\mytyc{$\wedge$}}}
205 \newcommand{\mybigand}{\mathrel{\mytyc{$\bigwedge$}}}
206 \newcommand{\myprfora}[3]{\forall #1 {:} #2. #3}
207 \newcommand{\myimpl}{\mathrel{\mytyc{$\Rightarrow$}}}
208 \newcommand{\mybot}{\mytyc{$\bot$}}
209 \newcommand{\mytop}{\mytyc{$\top$}}
210 \newcommand{\mycoe}{\myfun{coe}}
211 \newcommand{\mycoee}[4]{\myapp{\myapp{\myapp{\myapp{\mycoe}{#1}}{#2}}{#3}}{#4}}
212 \newcommand{\mycoh}{\myfun{coh}}
213 \newcommand{\mycohh}[4]{\myapp{\myapp{\myapp{\myapp{\mycoh}{#1}}{#2}}{#3}}{#4}}
214 \newcommand{\myjm}[4]{(#1 {:} #2) \mathrel{\mytyc{=}} (#3 {:} #4)}
215 \newcommand{\myeq}{\mathrel{\mytyc{=}}}
216 \newcommand{\myprop}{\mytyc{Prop}}
217 \newcommand{\mytmup}{\mytmsyn\uparrow}
218 \newcommand{\mydefs}{\Delta}
219 \newcommand{\mynf}{\Downarrow}
220 \newcommand{\myinff}[3]{#1 \vdash #2 \Rightarrow #3}
221 \newcommand{\myinf}[2]{\myinff{\myctx}{#1}{#2}}
222 \newcommand{\mychkk}[3]{#1 \vdash #2 \Leftarrow #3}
223 \newcommand{\mychk}[2]{\mychkk{\myctx}{#1}{#2}}
224 \newcommand{\myann}[2]{#1 : #2}
225 \newcommand{\mydeclsyn}{\myse{decl}}
226 \newcommand{\myval}[3]{#1 : #2 \mapsto #3}
227 \newcommand{\mypost}[2]{\mysyn{abstract}\ #1 : #2}
228 \newcommand{\myadt}[4]{\mysyn{data}\ #1 #2\ \mysyn{where}\ #3\{ #4 \}}
229 \newcommand{\myreco}[4]{\mysyn{record}\ #1 #2\ \mysyn{where}\ \{ #4 \}}
230 \newcommand{\myelabt}{\vdash}
231 \newcommand{\myelabf}{\rhd}
232 \newcommand{\myelab}[2]{\myctx \myelabt #1 \myelabf #2}
233 \newcommand{\mytele}{\Delta}
234 \newcommand{\mytelee}{\delta}
235 \newcommand{\mydcctx}{\Gamma}
236 \newcommand{\mynamesyn}{\myse{name}}
237 \newcommand{\myvec}{\overrightarrow}
238 \newcommand{\mymeta}{\textsc}
239 \newcommand{\myhyps}{\mymeta{hyps}}
240 \newcommand{\mycc}{;}
241 \newcommand{\myemptytele}{\varepsilon}
242 \newcommand{\mymetagoes}{\Longrightarrow}
243 % \newcommand{\mytesctx}{\
244 \newcommand{\mytelesyn}{\myse{telescope}}
245 \newcommand{\myrecs}{\mymeta{recs}}
246 \newcommand{\myle}{\mathrel{\lcfun{$\le$}}}
247 \newcommand{\mylet}{\mysyn{let}}
248 \newcommand{\myhead}{\mymeta{head}}
249 \newcommand{\mytake}{\mymeta{take}}
250 \newcommand{\myix}{\mymeta{ix}}
251 \newcommand{\myapply}{\mymeta{apply}}
252 \newcommand{\mydataty}{\mymeta{datatype}}
253 \newcommand{\myisreco}{\mymeta{record}}
254 \newcommand{\mydcsep}{\ |\ }
255 \newcommand{\mytree}{\mytyc{Tree}}
256 \newcommand{\myproj}[1]{\myfun{$\pi_{#1}$}}
257 \newcommand{\mysigma}{\mytyc{$\Sigma$}}
258 \newcommand{\mynegder}{\vspace{-0.3cm}}
259 \newcommand{\myquot}{\Uparrow}
260 \newcommand{\mynquot}{\, \Downarrow}
262 \renewcommand{\[}{\begin{equation*}}
263 \renewcommand{\]}{\end{equation*}}
264 \newcommand{\mymacol}[2]{\text{\textcolor{#1}{$#2$}}}
266 %% -----------------------------------------------------------------------------
268 \title{\mykant: Implementing Observational Equality}
269 \author{Francesco Mazzoli \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{<fm2209@ic.ac.uk>}}}
284 \thispagestyle{empty}
286 \begin{minipage}{0.4\textwidth}
287 \begin{flushleft} \large
289 Dr. Steffen \textsc{van Bakel}
292 \begin{minipage}{0.4\textwidth}
293 \begin{flushright} \large
295 Dr. Philippa \textsc{Gardner}
302 The marriage between programming and logic has been a very fertile one. In
303 particular, since the simply typed lambda calculus (STLC), a number of type
304 systems have been devised with increasing expressive power.
306 Among this systems, Inutitionistic Type Theory (ITT) has been a very
307 popular framework for theorem provers and programming languages.
308 However, equality has always been a tricky business in ITT and related
311 In these thesis we will explain why this is the case, and present
312 Observational Type Theory (OTT), a solution to some of the problems
313 with equality. We then describe $\mykant$, a theorem prover featuring
314 OTT in a setting more close to the one found in current systems.
315 Having implemented part of $\mykant$ as a Haskell program, we describe
316 some of the implementation issues faced.
321 \renewcommand{\abstractname}{Acknowledgements}
323 I would like to thank Steffen van Backel, my supervisor, who was brave
324 enough to believe in my project and who provided much advice and
327 I would also like to thank the Haskell and Agda community on
328 \texttt{IRC}, which guided me through the strange world of types; and
329 in particular Andrea Vezzosi and James Deikun, with whom I entertained
330 countless insightful discussions in the past year. Andrea suggested
331 Observational Type Theory as a topic of study: this thesis would not
332 exist without him. Before them, Tony Fields introduced me to Haskell,
333 unknowingly filling most of my free time from that time on.
335 Finally, much of the work stems from the research of Conor McBride,
336 who answered many of my doubts through these months. I also owe him
346 \section{Simple and not-so-simple types}
349 \subsection{The untyped $\lambda$-calculus}
352 Along with Turing's machines, the earliest attempts to formalise computation
353 lead to the $\lambda$-calculus \citep{Church1936}. This early programming
354 language encodes computation with a minimal syntax and no `data' in the
355 traditional sense, but just functions. Here we give a brief overview of the
356 language, which will give the chance to introduce concepts central to the
357 analysis of all the following calculi. The exposition follows the one found in
358 chapter 5 of \cite{Queinnec2003}.
360 The syntax of $\lambda$-terms consists of three things: variables, abstractions,
365 \begin{array}{r@{\ }c@{\ }l}
366 \mytmsyn & ::= & \myb{x} \mysynsep \myabs{\myb{x}}{\mytmsyn} \mysynsep (\myapp{\mytmsyn}{\mytmsyn}) \\
367 x & \in & \text{Some enumerable set of symbols}
372 Parenthesis will be omitted in the usual way:
373 $\myapp{\myapp{\mytmt}{\mytmm}}{\mytmn} =
374 \myapp{(\myapp{\mytmt}{\mytmm})}{\mytmn}$.
376 Abstractions roughly corresponds to functions, and their semantics is more
377 formally explained by the $\beta$-reduction rule:
379 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
382 \myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{\myb{x}}{\mytmn}\text{, where} \\
384 \begin{array}{l@{\ }c@{\ }l}
385 \mysub{\myb{x}}{\myb{x}}{\mytmn} & = & \mytmn \\
386 \mysub{\myb{y}}{\myb{x}}{\mytmn} & = & y\text{, with } \myb{x} \neq y \\
387 \mysub{(\myapp{\mytmt}{\mytmm})}{\myb{x}}{\mytmn} & = & (\myapp{\mysub{\mytmt}{\myb{x}}{\mytmn}}{\mysub{\mytmm}{\myb{x}}{\mytmn}}) \\
388 \mysub{(\myabs{\myb{x}}{\mytmm})}{\myb{x}}{\mytmn} & = & \myabs{\myb{x}}{\mytmm} \\
389 \mysub{(\myabs{\myb{y}}{\mytmm})}{\myb{x}}{\mytmn} & = & \myabs{\myb{z}}{\mysub{\mysub{\mytmm}{\myb{y}}{\myb{z}}}{\myb{x}}{\mytmn}}, \\
390 \multicolumn{3}{l}{\myind{2} \text{with $\myb{x} \neq \myb{y}$ and $\myb{z}$ not free in $\myapp{\mytmm}{\mytmn}$}}
396 The care required during substituting variables for terms is required to avoid
397 name capturing. We will use substitution in the future for other name-binding
398 constructs assuming similar precautions.
400 These few elements are of remarkable expressiveness, and in fact Turing
401 complete. As a corollary, we must be able to devise a term that reduces forever
402 (`loops' in imperative terms):
404 (\myapp{\omega}{\omega}) \myred (\myapp{\omega}{\omega}) \myred \cdots \text{, with $\omega = \myabs{x}{\myapp{x}{x}}$}
406 A \emph{redex} is a term that can be reduced. In the untyped $\lambda$-calculus
407 this will be the case for an application in which the first term is an
408 abstraction, but in general we call aterm reducible if it appears to the left of
409 a reduction rule. When a term contains no redexes it's said to be in
410 \emph{normal form}. Given the observation above, not all terms reduce to a
411 normal forms: we call the ones that do \emph{normalising}, and the ones that
412 don't \emph{non-normalising}.
414 The reduction rule presented is not syntax directed, but \emph{evaluation
415 strategies} can be employed to reduce term systematically. Common evaluation
416 strategies include \emph{call by value} (or \emph{strict}), where arguments of
417 abstractions are reduced before being applied to the abstraction; and conversely
418 \emph{call by name} (or \emph{lazy}), where we reduce only when we need to do so
419 to proceed---in other words when we have an application where the function is
420 still not a $\lambda$. In both these reduction strategies we never reduce under
421 an abstraction: for this reason a weaker form of normalisation is used, where
422 both abstractions and normal forms are said to be in \emph{weak head normal
425 \subsection{The simply typed $\lambda$-calculus}
427 A convenient way to `discipline' and reason about $\lambda$-terms is to assign
428 \emph{types} to them, and then check that the terms that we are forming make
429 sense given our typing rules \citep{Curry1934}. The first most basic instance
430 of this idea takes the name of \emph{simply typed $\lambda$ calculus}, whose
431 rules are shown in figure \ref{fig:stlc}.
433 Our types contain a set of \emph{type variables} $\Phi$, which might
434 correspond to some `primitive' types; and $\myarr$, the type former for
435 `arrow' types, the types of functions. The language is explicitly
436 typed: when we bring a variable into scope with an abstraction, we
437 declare its type. Reduction is unchanged from the untyped
443 \begin{array}{r@{\ }c@{\ }l}
444 \mytmsyn & ::= & \myb{x} \mysynsep \myabss{\myb{x}}{\mytysyn}{\mytmsyn} \mysynsep
445 (\myapp{\mytmsyn}{\mytmsyn}) \\
446 \mytysyn & ::= & \myse{\phi} \mysynsep \mytysyn \myarr \mytysyn \mysynsep \\
447 \myb{x} & \in & \text{Some enumerable set of symbols} \\
448 \myse{\phi} & \in & \Phi
453 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
455 \AxiomC{$\myctx(x) = A$}
456 \UnaryInfC{$\myjud{\myb{x}}{A}$}
459 \AxiomC{$\myjudd{\myctx;\myb{x} : A}{\mytmt}{\mytyb}$}
460 \UnaryInfC{$\myjud{\myabss{x}{A}{\mytmt}}{\mytyb}$}
463 \AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$}
464 \AxiomC{$\myjud{\mytmn}{\mytya}$}
465 \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mytyb}$}
469 \caption{Syntax and typing rules for the STLC. Reduction is unchanged from
470 the untyped $\lambda$-calculus.}
474 In the typing rules, a context $\myctx$ is used to store the types of bound
475 variables: $\myctx; \myb{x} : \mytya$ adds a variable to the context and
476 $\myctx(x)$ returns the type of the rightmost occurrence of $x$.
478 This typing system takes the name of `simply typed lambda calculus' (STLC), and
479 enjoys a number of properties. Two of them are expected in most type systems
482 \item[Progress] A well-typed term is not stuck---it is either a variable, or its
483 constructor does not appear on the left of the $\myred$ relation (currently
484 only $\lambda$), or it can take a step according to the evaluation rules.
485 \item[Preservation] If a well-typed term takes a step of evaluation, then the
486 resulting term is also well-typed, and preserves the previous type. Also
487 known as \emph{subject reduction}.
490 However, STLC buys us much more: every well-typed term is normalising
491 \citep{Tait1967}. It is easy to see that we can't fill the blanks if we want to
492 give types to the non-normalising term shown before:
494 \myapp{(\myabss{\myb{x}}{\myhole{?}}{\myapp{\myb{x}}{\myb{x}}})}{(\myabss{\myb{x}}{\myhole{?}}{\myapp{\myb{x}}{\myb{x}}})}
497 This makes the STLC Turing incomplete. We can recover the ability to loop by
498 adding a combinator that recurses:
501 \begin{minipage}{0.5\textwidth}
503 $ \mytmsyn ::= \cdots b \mysynsep \myfix{\myb{x}}{\mytysyn}{\mytmsyn} $
507 \begin{minipage}{0.5\textwidth}
508 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}} {
509 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytmt}{\mytya}$}
510 \UnaryInfC{$\myjud{\myfix{\myb{x}}{\mytya}{\mytmt}}{\mytya}$}
515 \mydesc{reduction:}{\myjud{\mytmsyn}{\mytmsyn}}{
516 $ \myfix{\myb{x}}{\mytya}{\mytmt} \myred \mysub{\mytmt}{\myb{x}}{(\myfix{\myb{x}}{\mytya}{\mytmt})}$
519 This will deprive us of normalisation, which is a particularly bad thing if we
520 want to use the STLC as described in the next section.
522 \subsection{The Curry-Howard correspondence}
524 It turns out that the STLC can be seen a natural deduction system for
525 intuitionistic propositional logic. Terms are proofs, and their types are the
526 propositions they prove. This remarkable fact is known as the Curry-Howard
527 correspondence, or isomorphism.
529 The arrow ($\myarr$) type corresponds to implication. If we wish to prove that
530 that $(\mytya \myarr \mytyb) \myarr (\mytyb \myarr \mytycc) \myarr (\mytya
531 \myarr \mytycc)$, all we need to do is to devise a $\lambda$-term that has the
534 \myabss{\myb{f}}{(\mytya \myarr \mytyb)}{\myabss{\myb{g}}{(\mytyb \myarr \mytycc)}{\myabss{\myb{x}}{\mytya}{\myapp{\myb{g}}{(\myapp{\myb{f}}{\myb{x}})}}}}
536 That is, function composition. Going beyond arrow types, we can extend our bare
537 lambda calculus with useful types to represent other logical constructs, as
538 shown in figure \ref{fig:natded}.
543 \begin{array}{r@{\ }c@{\ }l}
544 \mytmsyn & ::= & \cdots \\
545 & | & \mytt \mysynsep \myapp{\myabsurd{\mytysyn}}{\mytmsyn} \\
546 & | & \myapp{\myleft{\mytysyn}}{\mytmsyn} \mysynsep
547 \myapp{\myright{\mytysyn}}{\mytmsyn} \mysynsep
548 \myapp{\mycase{\mytmsyn}{\mytmsyn}}{\mytmsyn} \\
549 & | & \mypair{\mytmsyn}{\mytmsyn} \mysynsep
550 \myapp{\myfst}{\mytmsyn} \mysynsep \myapp{\mysnd}{\mytmsyn} \\
551 \mytysyn & ::= & \cdots \mysynsep \myunit \mysynsep \myempty \mysynsep \mytmsyn \mysum \mytmsyn \mysynsep \mytysyn \myprod \mytysyn
556 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
559 \begin{array}{l@{ }l@{\ }c@{\ }l}
560 \myapp{\mycase{\mytmm}{\mytmn}}{(\myapp{\myleft{\mytya} &}{\mytmt})} & \myred &
561 \myapp{\mytmm}{\mytmt} \\
562 \myapp{\mycase{\mytmm}{\mytmn}}{(\myapp{\myright{\mytya} &}{\mytmt})} & \myred &
563 \myapp{\mytmn}{\mytmt}
568 \begin{array}{l@{ }l@{\ }c@{\ }l}
569 \myapp{\myfst &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmm \\
570 \myapp{\mysnd &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmn
576 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
578 \AxiomC{\phantom{$\myjud{\mytmt}{\myempty}$}}
579 \UnaryInfC{$\myjud{\mytt}{\myunit}$}
582 \AxiomC{$\myjud{\mytmt}{\myempty}$}
583 \UnaryInfC{$\myjud{\myapp{\myabsurd{\mytya}}{\mytmt}}{\mytya}$}
590 \AxiomC{$\myjud{\mytmt}{\mytya}$}
591 \UnaryInfC{$\myjud{\myapp{\myleft{\mytyb}}{\mytmt}}{\mytya \mysum \mytyb}$}
594 \AxiomC{$\myjud{\mytmt}{\mytyb}$}
595 \UnaryInfC{$\myjud{\myapp{\myright{\mytya}}{\mytmt}}{\mytya \mysum \mytyb}$}
603 \AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$}
604 \AxiomC{$\myjud{\mytmn}{\mytya \myarr \mytycc}$}
605 \AxiomC{$\myjud{\mytmt}{\mytya \mysum \mytyb}$}
606 \TrinaryInfC{$\myjud{\myapp{\mycase{\mytmm}{\mytmn}}{\mytmt}}{\mytycc}$}
613 \AxiomC{$\myjud{\mytmm}{\mytya}$}
614 \AxiomC{$\myjud{\mytmn}{\mytyb}$}
615 \BinaryInfC{$\myjud{\mypair{\mytmm}{\mytmn}}{\mytya \myprod \mytyb}$}
618 \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
619 \UnaryInfC{$\myjud{\myapp{\myfst}{\mytmt}}{\mytya}$}
622 \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
623 \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mytyb}$}
627 \caption{Rules for the extendend STLC. Only the new features are shown, all the
628 rules and syntax for the STLC apply here too.}
632 Tagged unions (or sums, or coproducts---$\mysum$ here, \texttt{Either}
633 in Haskell) correspond to disjunctions, and dually tuples (or pairs, or
634 products---$\myprod$ here, tuples in Haskell) correspond to
635 conjunctions. This is apparent looking at the ways to construct and
636 destruct the values inhabiting those types: for $\mysum$ $\myleft{ }$
637 and $\myright{ }$ correspond to $\vee$ introduction, and
638 $\mycase{\myarg}{\myarg}$ to $\vee$ elimination; for $\myprod$
639 $\mypair{\myarg}{\myarg}$ corresponds to $\wedge$ introduction, $\myfst$
640 and $\mysnd$ to $\wedge$ elimination.
642 The trivial type $\myunit$ corresponds to the logical $\top$, and dually
643 $\myempty$ corresponds to the logical $\bot$. $\myunit$ has one introduction
644 rule ($\mytt$), and thus one inhabitant; and no eliminators. $\myempty$ has no
645 introduction rules, and thus no inhabitants; and one eliminator ($\myabsurd{
646 }$), corresponding to the logical \emph{ex falso quodlibet}.
648 With these rules, our STLC now looks remarkably similar in power and use to the
649 natural deduction we already know. $\myneg \mytya$ can be expressed as $\mytya
650 \myarr \myempty$. However, there is an important omission: there is no term of
651 the type $\mytya \mysum \myneg \mytya$ (excluded middle), or equivalently
652 $\myneg \myneg \mytya \myarr \mytya$ (double negation), or indeed any term with
653 a type equivalent to those.
655 This has a considerable effect on our logic and it's no coincidence, since there
656 is no obvious computational behaviour for laws like the excluded middle.
657 Theories of this kind are called \emph{intuitionistic}, or \emph{constructive},
658 and all the systems analysed will have this characteristic since they build on
659 the foundation of the STLC.\footnote{There is research to give computational
660 behaviour to classical logic, but I will not touch those subjects.}
662 As in logic, if we want to keep our system consistent, we must make sure that no
663 closed terms (in other words terms not under a $\lambda$) inhabit $\myempty$.
664 The variant of STLC presented here is indeed
665 consistent, a result that follows from the fact that it is
667 Going back to our $\mysyn{fix}$ combinator, it is easy to see how it ruins our
668 desire for consistency. The following term works for every type $\mytya$,
670 \[(\myfix{\myb{x}}{\mytya}{\myb{x}}) : \mytya\]
672 \subsection{Inductive data}
675 To make the STLC more useful as a programming language or reasoning tool it is
676 common to include (or let the user define) inductive data types. These comprise
677 of a type former, various constructors, and an eliminator (or destructor) that
678 serves as primitive recursor.
680 For example, we might add a $\mylist$ type constructor, along with an `empty
681 list' ($\mynil{ }$) and `cons cell' ($\mycons$) constructor. The eliminator for
682 lists will be the usual folding operation ($\myfoldr$). See figure
688 \begin{array}{r@{\ }c@{\ }l}
689 \mytmsyn & ::= & \cdots \mysynsep \mynil{\mytysyn} \mysynsep \mytmsyn \mycons \mytmsyn
691 \myapp{\myapp{\myapp{\myfoldr}{\mytmsyn}}{\mytmsyn}}{\mytmsyn} \\
692 \mytysyn & ::= & \cdots \mysynsep \myapp{\mylist}{\mytysyn}
696 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
698 \begin{array}{l@{\ }c@{\ }l}
699 \myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{\mynil{\mytya}} & \myred & \mytmt \\
701 \myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{(\mytmm \mycons \mytmn)} & \myred &
702 \myapp{\myapp{\myse{f}}{\mytmm}}{(\myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{\mytmn})}
706 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
708 \AxiomC{\phantom{$\myjud{\mytmm}{\mytya}$}}
709 \UnaryInfC{$\myjud{\mynil{\mytya}}{\myapp{\mylist}{\mytya}}$}
712 \AxiomC{$\myjud{\mytmm}{\mytya}$}
713 \AxiomC{$\myjud{\mytmn}{\myapp{\mylist}{\mytya}}$}
714 \BinaryInfC{$\myjud{\mytmm \mycons \mytmn}{\myapp{\mylist}{\mytya}}$}
719 \AxiomC{$\myjud{\mysynel{f}}{\mytya \myarr \mytyb \myarr \mytyb}$}
720 \AxiomC{$\myjud{\mytmm}{\mytyb}$}
721 \AxiomC{$\myjud{\mytmn}{\myapp{\mylist}{\mytya}}$}
722 \TrinaryInfC{$\myjud{\myapp{\myapp{\myapp{\myfoldr}{\mysynel{f}}}{\mytmm}}{\mytmn}}{\mytyb}$}
725 \caption{Rules for lists in the STLC.}
729 In Section \ref{sec:well-order} we will see how to give a general account of
732 \section{Intuitionistic Type Theory}
735 \subsection{Extending the STLC}
737 The STLC can be made more expressive in various ways. \cite{Barendregt1991}
738 succinctly expressed geometrically how we can add expressivity:
741 & \lambda\omega \ar@{-}[rr]\ar@{-}'[d][dd]
742 & & \lambda C \ar@{-}[dd]
744 \lambda2 \ar@{-}[ur]\ar@{-}[rr]\ar@{-}[dd]
745 & & \lambda P2 \ar@{-}[ur]\ar@{-}[dd]
747 & \lambda\underline\omega \ar@{-}'[r][rr]
748 & & \lambda P\underline\omega
750 \lambda{\to} \ar@{-}[rr]\ar@{-}[ur]
751 & & \lambda P \ar@{-}[ur]
754 Here $\lambda{\to}$, in the bottom left, is the STLC. From there can move along
757 \item[Terms depending on types (towards $\lambda{2}$)] We can quantify over
758 types in our type signatures. For example, we can define a polymorphic
761 (\myabss{\myb{A}}{\mytyp}{\myabss{\myb{x}}{\myb{A}}{\myb{x}}}) : (\myb{A} : \mytyp) \myarr \myb{A} \myarr \myb{A}
763 The first and most famous instance of this idea has been System F. This form
764 of polymorphism and has been wildly successful, also thanks to a well known
765 inference algorithm for a restricted version of System F known as
766 Hindley-Milner. Languages like Haskell and SML are based on this discipline.
767 \item[Types depending on types (towards $\lambda{\underline{\omega}}$)] We have
768 type operators. For example we could define a function that given types $R$
769 and $\mytya$ forms the type that represents a value of type $\mytya$ in
770 continuation passing style:
771 \[\displaystyle(\myabss{\myb{A} \myar \myb{R}}{\mytyp}{(\myb{A}
772 \myarr \myb{R}) \myarr \myb{R}}) : \mytyp \myarr \mytyp \myarr \mytyp
774 \item[Types depending on terms (towards $\lambda{P}$)] Also known as `dependent
775 types', give great expressive power. For example, we can have values of whose
776 type depend on a boolean:
777 \[\displaystyle(\myabss{\myb{x}}{\mybool}{\myite{\myb{x}}{\mynat}{\myrat}}) : \mybool
781 All the systems preserve the properties that make the STLC well behaved. The
782 system we are going to focus on, Intuitionistic Type Theory, has all of the
783 above additions, and thus would sit where $\lambda{C}$ sits in the
784 `$\lambda$-cube'. It will serve as the logical `core' of all the other
785 extensions that we will present and ultimately our implementation of a similar
788 \subsection{A Bit of History}
790 Logic frameworks and programming languages based on type theory have a long
791 history. Per Martin-L\"{o}f described the first version of his theory in 1971,
792 but then revised it since the original version was inconsistent due to its
793 impredicativity.\footnote{In the early version there was only one universe
794 $\mytyp$ and $\mytyp : \mytyp$, see Section \ref{sec:term-types} for an
795 explanation on why this causes problems.} For this reason he gave a revised
796 and consistent definition later \citep{Martin-Lof1984}.
798 A related development is the polymorphic $\lambda$-calculus, and specifically
799 the previously mentioned System F, which was developed independently by Girard
800 and Reynolds. An overview can be found in \citep{Reynolds1994}. The surprising
801 fact is that while System F is impredicative it is still consistent and strongly
802 normalising. \cite{Coquand1986} further extended this line of work with the
803 Calculus of Constructions (CoC).
805 Most widely used interactive theorem provers are based on ITT. Popular ones
806 include Agda \citep{Norell2007, Bove2009}, Coq \citep{Coq}, and Epigram
807 \citep{McBride2004, EpigramTut}.
809 \subsection{A simple type theory}
812 The calculus I present follows the exposition in \citep{Thompson1991},
813 and is quite close to the original formulation of predicative ITT as
814 found in \citep{Martin-Lof1984}. The system's syntax and reduction
815 rules are presented in their entirety in figure \ref{fig:core-tt-syn}.
816 The typing rules are presented piece by piece. Agda and \mykant\
817 renditions of the presented theory and all the examples is reproduced in
818 appendix \ref{app:itt-code}.
823 \begin{array}{r@{\ }c@{\ }l}
824 \mytmsyn & ::= & \myb{x} \mysynsep
825 \mytyp_{level} \mysynsep
826 \myunit \mysynsep \mytt \mysynsep
827 \myempty \mysynsep \myapp{\myabsurd{\mytmsyn}}{\mytmsyn} \\
828 & | & \mybool \mysynsep \mytrue \mysynsep \myfalse \mysynsep
829 \myitee{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
830 & | & \myfora{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
831 \myabss{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
832 (\myapp{\mytmsyn}{\mytmsyn}) \\
833 & | & \myexi{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
834 \mypairr{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn} \\
835 & | & \myapp{\myfst}{\mytmsyn} \mysynsep \myapp{\mysnd}{\mytmsyn} \\
836 & | & \myw{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
837 \mytmsyn \mynode{\myb{x}}{\mytmsyn} \mytmsyn \\
838 & | & \myrec{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn} \\
839 level & \in & \mathbb{N}
844 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
847 \begin{array}{l@{ }l@{\ }c@{\ }l}
848 \myitee{\mytrue &}{\myb{x}}{\myse{P}}{\mytmm}{\mytmn} & \myred & \mytmm \\
849 \myitee{\myfalse &}{\myb{x}}{\myse{P}}{\mytmm}{\mytmn} & \myred & \mytmn \\
854 \myapp{(\myabss{\myb{x}}{\mytya}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{\myb{x}}{\mytmn}
858 \begin{array}{l@{ }l@{\ }c@{\ }l}
859 \myapp{\myfst &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmm \\
860 \myapp{\mysnd &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmn
868 \myrec{(\myse{s} \mynode{\myb{x}}{\myse{T}} \myse{f})}{\myb{y}}{\myse{P}}{\myse{p}} \myred
869 \myapp{\myapp{\myapp{\myse{p}}{\myse{s}}}{\myse{f}}}{(\myabss{\myb{t}}{\mysub{\myse{T}}{\myb{x}}{\myse{s}}}{
870 \myrec{\myapp{\myse{f}}{\myb{t}}}{\myb{y}}{\myse{P}}{\mytmt}
874 \caption{Syntax and reduction rules for our type theory.}
875 \label{fig:core-tt-syn}
878 \subsubsection{Types are terms, some terms are types}
879 \label{sec:term-types}
881 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
883 \AxiomC{$\myjud{\mytmt}{\mytya}$}
884 \AxiomC{$\mytya \mydefeq \mytyb$}
885 \BinaryInfC{$\myjud{\mytmt}{\mytyb}$}
888 \AxiomC{\phantom{$\myjud{\mytmt}{\mytya}$}}
889 \UnaryInfC{$\myjud{\mytyp_l}{\mytyp_{l + 1}}$}
894 The first thing to notice is that a barrier between values and types that we had
895 in the STLC is gone: values can appear in types, and the two are treated
896 uniformly in the syntax.
898 While the usefulness of doing this will become clear soon, a consequence is
899 that since types can be the result of computation, deciding type equality is
900 not immediate as in the STLC. For this reason we define \emph{definitional
901 equality}, $\mydefeq$, as the congruence relation extending
902 $\myred$---moreover, when comparing types syntactically we do it up to
903 renaming of bound names ($\alpha$-renaming). For example under this
904 discipline we will find that
906 \myabss{\myb{x}}{\mytya}{\myb{x}} \mydefeq \myabss{\myb{y}}{\mytya}{\myb{y}}
908 Types that are definitionally equal can be used interchangeably. Here
909 the `conversion' rule is not syntax directed, but it is possible to
910 employ $\myred$ to decide term equality in a systematic way, by always
911 reducing terms to their normal forms before comparing them, so that a
912 separate conversion rule is not needed.
913 Another thing to notice is that considering the need to reduce terms to
914 decide equality, it is essential for a dependently type system to be
915 terminating and confluent for type checking to be decidable.
917 Moreover, we specify a \emph{type hierarchy} to talk about `large'
918 types: $\mytyp_0$ will be the type of types inhabited by data:
919 $\mybool$, $\mynat$, $\mylist$, etc. $\mytyp_1$ will be the type of
920 $\mytyp_0$, and so on---for example we have $\mytrue : \mybool :
921 \mytyp_0 : \mytyp_1 : \cdots$. Each type `level' is often called a
922 universe in the literature. While it is possible to simplify things by
923 having only one universe $\mytyp$ with $\mytyp : \mytyp$, this plan is
924 inconsistent for much the same reason that impredicative na\"{\i}ve set
925 theory is \citep{Hurkens1995}. However various techniques can be
926 employed to lift the burden of explicitly handling universes, as we will
927 see in Section \ref{sec:term-hierarchy}.
929 \subsubsection{Contexts}
931 \begin{minipage}{0.5\textwidth}
932 \mydesc{context validity:}{\myvalid{\myctx}}{
934 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
935 \UnaryInfC{$\myvalid{\myemptyctx}$}
938 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
939 \UnaryInfC{$\myvalid{\myctx ; \myb{x} : \mytya}$}
944 \begin{minipage}{0.5\textwidth}
945 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
946 \AxiomC{$\myctx(x) = \mytya$}
947 \UnaryInfC{$\myjud{\myb{x}}{\mytya}$}
953 We need to refine the notion context to make sure that every variable appearing
954 is typed correctly, or that in other words each type appearing in the context is
955 indeed a type and not a value. In every other rule, if no premises are present,
956 we assume the context in the conclusion to be valid.
958 Then we can re-introduce the old rule to get the type of a variable for a
961 \subsubsection{$\myunit$, $\myempty$}
963 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
965 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
966 \UnaryInfC{$\myjud{\myunit}{\mytyp_0}$}
968 \UnaryInfC{$\myjud{\myempty}{\mytyp_0}$}
971 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
972 \UnaryInfC{$\myjud{\mytt}{\myunit}$}
974 \UnaryInfC{\phantom{$\myjud{\myempty}{\mytyp_0}$}}
977 \AxiomC{$\myjud{\mytmt}{\myempty}$}
978 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
979 \BinaryInfC{$\myjud{\myapp{\myabsurd{\mytya}}{\mytmt}}{\mytya}$}
981 \UnaryInfC{\phantom{$\myjud{\myempty}{\mytyp_0}$}}
986 Nothing surprising here: $\myunit$ and $\myempty$ are unchanged from the STLC,
987 with the added rules to type $\myunit$ and $\myempty$ themselves, and to make
988 sure that we are invoking $\myabsurd{}$ over a type.
990 \subsubsection{$\mybool$, and dependent $\myfun{if}$}
992 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
995 \UnaryInfC{$\myjud{\mybool}{\mytyp_0}$}
999 \UnaryInfC{$\myjud{\mytrue}{\mybool}$}
1003 \UnaryInfC{$\myjud{\myfalse}{\mybool}$}
1008 \AxiomC{$\myjud{\mytmt}{\mybool}$}
1009 \AxiomC{$\myjudd{\myctx : \mybool}{\mytya}{\mytyp_l}$}
1011 \BinaryInfC{$\myjud{\mytmm}{\mysub{\mytya}{x}{\mytrue}}$ \hspace{0.7cm} $\myjud{\mytmn}{\mysub{\mytya}{x}{\myfalse}}$}
1012 \UnaryInfC{$\myjud{\myitee{\mytmt}{\myb{x}}{\mytya}{\mytmm}{\mytmn}}{\mysub{\mytya}{\myb{x}}{\mytmt}}$}
1016 With booleans we get the first taste of the `dependent' in `dependent
1017 types'. While the two introduction rules ($\mytrue$ and $\myfalse$) are
1018 not surprising, the typing rules for $\myfun{if}$ are. In most strongly
1019 typed languages we expect the branches of an $\myfun{if}$ statements to
1020 be of the same type, to preserve subject reduction, since execution
1021 could take both paths. This is a pity, since the type system does not
1022 reflect the fact that in each branch we gain knowledge on the term we
1023 are branching on. Which means that programs along the lines of
1025 if null xs then head xs else 0
1027 are a necessary, well typed, danger.
1029 However, in a more expressive system, we can do better: the branches' type can
1030 depend on the value of the scrutinised boolean. This is what the typing rule
1031 expresses: the user provides a type $\mytya$ ranging over an $\myb{x}$
1032 representing the scrutinised boolean type, and the branches are typechecked with
1033 the updated knowledge on the value of $\myb{x}$.
1035 \subsubsection{$\myarr$, or dependent function}
1037 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1038 \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
1039 \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
1040 \BinaryInfC{$\myjud{\myfora{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
1046 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytmt}{\mytyb}$}
1047 \UnaryInfC{$\myjud{\myabss{\myb{x}}{\mytya}{\mytmt}}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
1050 \AxiomC{$\myjud{\mytmm}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
1051 \AxiomC{$\myjud{\mytmn}{\mytya}$}
1052 \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mysub{\mytyb}{\myb{x}}{\mytmn}}$}
1057 Dependent functions are one of the two key features that perhaps most
1058 characterise dependent types---the other being dependent products. With
1059 dependent functions, the result type can depend on the value of the
1060 argument. This feature, together with the fact that the result type
1061 might be a type itself, brings a lot of interesting possibilities.
1062 Following this intuition, in the introduction rule, the return type is
1063 typechecked in a context with an abstracted variable of lhs' type, and
1064 in the elimination rule the actual argument is substituted in the return
1065 type. Keeping the correspondence with logic alive, dependent functions
1066 are much like universal quantifiers ($\forall$) in logic.
1068 For example, assuming that we have lists and natural numbers in our
1069 language, using dependent functions we would be able to
1073 \myfun{length} : (\myb{A} {:} \mytyp_0) \myarr \myapp{\mylist}{\myb{A}} \myarr \mynat \\
1074 \myarg \myfun{$>$} \myarg : \mynat \myarr \mynat \myarr \mytyp_0 \\
1075 \myfun{head} : (\myb{A} {:} \mytyp_0) \myarr (\myb{l} {:} \myapp{\mylist}{\myb{A}})
1076 \myarr \myapp{\myapp{\myfun{length}}{\myb{A}}}{\myb{l}} \mathrel{\myfun{$>$}} 0 \myarr
1081 \myfun{length} is the usual polymorphic length
1082 function. $\myarg\myfun{$>$}\myarg$ is a function that takes two naturals
1083 and returns a type: if the lhs is greater then the rhs, $\myunit$ is
1084 returned, $\myempty$ otherwise. This way, we can express a
1085 `non-emptyness' condition in $\myfun{head}$, by including a proof that
1086 the length of the list argument is non-zero. This allows us to rule out
1087 the `empty list' case, so that we can safely return the first element.
1089 Again, we need to make sure that the type hierarchy is respected, which is the
1090 reason why a type formed by $\myarr$ will live in the least upper bound of the
1091 levels of argument and return type. This trend will continue with the other
1092 type-level binders, $\myprod$ and $\mytyc{W}$.
1094 \subsubsection{$\myprod$, or dependent product}
1097 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1098 \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
1099 \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
1100 \BinaryInfC{$\myjud{\myexi{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
1106 \AxiomC{$\myjud{\mytmm}{\mytya}$}
1107 \AxiomC{$\myjud{\mytmn}{\mysub{\mytyb}{\myb{x}}{\mytmm}}$}
1108 \BinaryInfC{$\myjud{\mypairr{\mytmm}{\myb{x}}{\mytyb}{\mytmn}}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
1110 \UnaryInfC{\phantom{$--$}}
1113 \AxiomC{$\myjud{\mytmt}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
1114 \UnaryInfC{$\hspace{0.7cm}\myjud{\myapp{\myfst}{\mytmt}}{\mytya}\hspace{0.7cm}$}
1116 \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mysub{\mytyb}{\myb{x}}{\myapp{\myfst}{\mytmt}}}$}
1121 If dependent functions are a generalisation of $\myarr$ in the STLC,
1122 dependent products are a generalisation of $\myprod$ in the STLC. The
1123 improvement is that the second element's type can depend on the value of
1124 the first element. The corrispondence with logic is through the
1125 existential quantifier: $\exists x \in \mathbb{N}. even(x)$ can be
1126 expressed as $\myexi{\myb{x}}{\mynat}{\myapp{\myfun{even}}{\myb{x}}}$.
1127 The first element will be a number, and the second evidence that the
1128 number is even. This highlights the fact that we are working in a
1129 constructive logic: if we have an existence proof, we can always ask for
1130 a witness. This means, for instance, that $\neg \forall \neg$ is not
1131 equivalent to $\exists$.
1133 Another perhaps more `dependent' application of products, paired with
1134 $\mybool$, is to offer choice between different types. For example we
1135 can easily recover disjunctions:
1138 \myarg\myfun{$\vee$}\myarg : \mytyp_0 \myarr \mytyp_0 \myarr \mytyp_0 \\
1139 \myb{A} \mathrel{\myfun{$\vee$}} \myb{B} \mapsto \myexi{\myb{x}}{\mybool}{\myite{\myb{x}}{\myb{A}}{\myb{B}}} \\ \ \\
1140 \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} \\
1141 \myfun{case} \myappsp \myb{A} \myappsp \myb{B} \myappsp \myb{C} \myappsp \myb{f} \myappsp \myb{g} \myappsp \myb{x} \mapsto \\
1142 \myind{2} \myapp{(\myitee{\myapp{\myfst}{\myb{x}}}{\myb{b}}{(\myite{\myb{b}}{\myb{A}}{\myb{B}})}{\myb{f}}{\myb{g}})}{(\myapp{\mysnd}{\myb{x}})}
1146 \subsubsection{$\mytyc{W}$, or well-order}
1147 \label{sec:well-order}
1149 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1151 \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
1152 \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
1153 \BinaryInfC{$\myjud{\myw{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
1158 \AxiomC{$\myjud{\mytmt}{\mytya}$}
1159 \AxiomC{$\myjud{\mysynel{f}}{\mysub{\mytyb}{\myb{x}}{\mytmt} \myarr \myw{\myb{x}}{\mytya}{\mytyb}}$}
1160 \BinaryInfC{$\myjud{\mytmt \mynode{\myb{x}}{\mytyb} \myse{f}}{\myw{\myb{x}}{\mytya}{\mytyb}}$}
1166 \AxiomC{$\myjud{\myse{u}}{\myw{\myb{x}}{\myse{S}}{\myse{T}}}$}
1167 \AxiomC{$\myjudd{\myctx; \myb{w} : \myw{\myb{x}}{\myse{S}}{\myse{T}}}{\myse{P}}{\mytyp_l}$}
1169 \BinaryInfC{$\myjud{\myse{p}}{
1170 \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}}}}
1172 \UnaryInfC{$\myjud{\myrec{\myse{u}}{\myb{w}}{\myse{P}}{\myse{p}}}{\mysub{\myse{P}}{\myb{w}}{\myse{u}}}$}
1176 Finally, the well-order type, or in short $\mytyc{W}$-type, which will
1177 let us represent inductive data in a general (but clumsy) way. We can
1178 form `nodes' of the shape $\mytmt \mynode{\myb{x}}{\mytyb} \myse{f} :
1179 \myw{\myb{x}}{\mytya}{\mytyb}$ that contain data ($\mytmt$) of type and
1180 one `child' for each member of $\mysub{\mytyb}{\myb{x}}{\mytmt}$. The
1181 $\myfun{rec}\ \myfun{with}$ acts as an induction principle on
1182 $\mytyc{W}$, given a predicate an a function dealing with the inductive
1183 case---we will gain more intuition about inductive data in ITT in
1184 Section \ref{sec:user-type}.
1186 For example, if we want to form natural numbers, we can take
1189 \mytyc{Tr} : \mybool \myarr \mytyp_0 \\
1190 \mytyc{Tr} \myappsp \myb{b} \mapsto \myfun{if}\, \myb{b}\, \myunit\, \myfun{else}\, \myempty \\
1192 \mynat : \mytyp_0 \\
1193 \mynat \mapsto \myw{\myb{b}}{\mybool}{(\mytyc{Tr}\myappsp\myb{b})}
1196 Each node will contain a boolean. If $\mytrue$, the number is non-zero,
1197 and we will have one child representing its predecessor, given that
1198 $\mytyc{Tr}$ will return $\myunit$. If $\myfalse$, the number is zero,
1199 and we will have no predecessors (children), given the $\myempty$:
1202 \mydc{zero} : \mynat \\
1203 \mydc{zero} \mapsto \myfalse \mynodee (\myabs{\myb{z}}{\myabsurd{\mynat} \myappsp \myb{x}}) \\
1205 \mydc{suc} : \mynat \myarr \mynat \\
1206 \mydc{suc}\myappsp \myb{x} \mapsto \mytrue \mynodee (\myabs{\myarg}{\myb{x}})
1209 And with a bit of effort, we can recover addition:
1212 \myfun{plus} : \mynat \myarr \mynat \myarr \mynat \\
1213 \myfun{plus} \myappsp \myb{x} \myappsp \myb{y} \mapsto \\
1214 \myind{2} \myfun{rec}\, \myb{x} / \myb{b}.\mynat \, \\
1215 \myind{2} \myfun{with}\, \myabs{\myb{b}}{\\
1216 \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) \\
1217 \myind{2}\myind{2}\myfun{then}\,(\myabs{\myarg\, \myb{f}}{\mydc{suc}\myappsp (\myapp{\myb{f}}{\mytt})})\, \myfun{else}\, (\myabs{\myarg\, \myarg}{\myb{y}})}
1220 Note how we explicitly have to type the branches to make them
1221 match with the definition of $\mynat$---which gives a taste of the
1222 `clumsiness' of $\mytyc{W}$-types, which while useful as a reasoning
1223 tool are useless to the user modelling data types.
1225 \section{The struggle for equality}
1226 \label{sec:equality}
1228 In the previous section we saw how a type checker (or a human) needs a
1229 notion of \emph{definitional equality}. Beyond this meta-theoretic
1230 notion, in this section we will explore the ways of expressing equality
1231 \emph{inside} the theory, as a reasoning tool available to the user.
1232 This area is the main concern of this thesis, and in general a very
1233 active research topic, since we do not have a fully satisfactory
1234 solution, yet. As in the previous section, everything presented is
1235 formalised in Agda in appendix \ref{app:agda-itt}.
1237 \subsection{Propositional equality}
1240 \begin{minipage}{0.5\textwidth}
1243 \begin{array}{r@{\ }c@{\ }l}
1244 \mytmsyn & ::= & \cdots \\
1245 & | & \mytmsyn \mypeq{\mytmsyn} \mytmsyn \mysynsep
1246 \myapp{\myrefl}{\mytmsyn} \\
1247 & | & \myjeq{\mytmsyn}{\mytmsyn}{\mytmsyn}
1252 \begin{minipage}{0.5\textwidth}
1253 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
1255 \myjeq{\myse{P}}{(\myapp{\myrefl}{\mytmm})}{\mytmn} \myred \mytmn
1261 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1262 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
1263 \AxiomC{$\myjud{\mytmm}{\mytya}$}
1264 \AxiomC{$\myjud{\mytmn}{\mytya}$}
1265 \TrinaryInfC{$\myjud{\mytmm \mypeq{\mytya} \mytmn}{\mytyp_l}$}
1271 \AxiomC{$\begin{array}{c}\ \\\myjud{\mytmm}{\mytya}\hspace{1.1cm}\mytmm \mydefeq \mytmn\end{array}$}
1272 \UnaryInfC{$\myjud{\myapp{\myrefl}{\mytmm}}{\mytmm \mypeq{\mytya} \mytmn}$}
1277 \myjud{\myse{P}}{\myfora{\myb{x}\ \myb{y}}{\mytya}{\myfora{q}{\myb{x} \mypeq{\mytya} \myb{y}}{\mytyp_l}}} \\
1278 \myjud{\myse{q}}{\mytmm \mypeq{\mytya} \mytmn}\hspace{1.1cm}\myjud{\myse{p}}{\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmm}}{(\myapp{\myrefl}{\mytmm})}}
1281 \UnaryInfC{$\myjud{\myjeq{\myse{P}}{\myse{q}}{\myse{p}}}{\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmn}}{q}}$}
1286 To express equality between two terms inside ITT, the obvious way to do so is
1287 to have the equality construction to be a type-former. Here we present what
1288 has survived as the dominating form of equality in systems based on ITT up to
1291 Our type former is $\mypeq{\mytya}$, which given a type (in this case
1292 $\mytya$) relates equal terms of that type. $\mypeq{}$ has one introduction
1293 rule, $\myrefl$, which introduces an equality relation between definitionally
1296 Finally, we have one eliminator for $\mypeq{}$, $\myjeqq$. $\myjeq{\myse{P}}{\myse{q}}{\myse{p}}$ takes
1298 \item $\myse{P}$, a predicate working with two terms of a certain type (say
1299 $\mytya$) and a proof of their equality
1300 \item $\myse{q}$, a proof that two terms in $\mytya$ (say $\myse{m}$ and
1301 $\myse{n}$) are equal
1302 \item and $\myse{p}$, an inhabitant of $\myse{P}$ applied to $\myse{m}$
1303 twice, plus the trivial proof by reflexivity showing that $\myse{m}$
1306 Given these ingredients, $\myjeqq$ retuns a member of $\myse{P}$ applied to
1307 $\mytmm$, $\mytmn$, and $\myse{q}$. In other words $\myjeqq$ takes a
1308 witness that $\myse{P}$ works with \emph{definitionally equal} terms, and
1309 returns a witness of $\myse{P}$ working with \emph{propositionally equal}
1310 terms. Invokations of $\myjeqq$ will vanish when the equality proofs will
1311 reduce to invocations to reflexivity, at which point the arguments must be
1312 definitionally equal, and thus the provided
1313 $\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmm}}{(\myapp{\myrefl}{\mytmm})}$
1316 While the $\myjeqq$ rule is slightly convoluted, ve can derive many more
1317 `friendly' rules from it, for example a more obvious `substitution' rule, that
1318 replaces equal for equal in predicates:
1321 \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}}}}} \\
1322 \myfun{subst}\myappsp \myb{A}\myappsp\myb{P}\myappsp\myb{x}\myappsp\myb{y}\myappsp\myb{q}\myappsp\myb{p} \mapsto
1323 \myjeq{(\myabs{\myb{x}\ \myb{y}\ \myb{q}}{\myapp{\myb{P}}{\myb{y}}})}{\myb{p}}{\myb{q}}
1326 Once we have $\myfun{subst}$, we can easily prove more familiar laws regarding
1327 equality, such as symmetry, transitivity, congruence laws, etc.
1329 \subsection{Common extensions}
1331 Our definitional and propositional equalities can be enhanced in various
1332 ways. Obviously if we extend the definitional equality we are also
1333 automatically extend propositional equality, given how $\myrefl$ works.
1335 \subsubsection{$\eta$-expansion}
1336 \label{sec:eta-expand}
1338 A simple extension to our definitional equality is $\eta$-expansion.
1339 Given an abstract variable $\myb{f} : \mytya \myarr \mytyb$ the aim is
1340 to have that $\myb{f} \mydefeq
1341 \myabss{\myb{x}}{\mytya}{\myapp{\myb{f}}{\myb{x}}}$. We can achieve
1342 this by `expanding' terms based on their types, a process also known as
1343 \emph{quotation}---a term borrowed from the practice of
1344 \emph{normalisation by evaluation}, where we embed terms in some host
1345 language with an existing notion of computation, and then reify them
1346 back into terms, which will `smooth out' differences like the one above
1349 The same concept applies to $\myprod$, where we expand each inhabitant
1350 by reconstructing it by getting its projections, so that $\myb{x}
1351 \mydefeq \mypair{\myfst \myappsp \myb{x}}{\mysnd \myappsp \myb{x}}$.
1352 Similarly, all one inhabitants of $\myunit$ and all zero inhabitants of
1353 $\myempty$ can be considered equal. Quotation can be performed in a
1354 type-directed way, as we will witness in Section \ref{sec:kant-irr}.
1356 To justify this process in our type system we will add a congruence law
1357 for abstractions and a similar law for products, plus the fact that all
1358 elements of $\myunit$ or $\myempty$ are equal.
1360 \mydesc{definitional equality:}{\myjud{\mytmm \mydefeq \mytmn}{\mytmsyn}}{
1362 \AxiomC{$\myjudd{\myctx; \myb{y} : \mytya}{\myapp{\myse{f}}{\myb{x}} \mydefeq \myapp{\myse{g}}{\myb{x}}}{\mysub{\mytyb}{\myb{x}}{\myb{y}}}$}
1363 \UnaryInfC{$\myjud{\myse{f} \mydefeq \myse{g}}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
1366 \AxiomC{$\myjud{\mypair{\myapp{\myfst}{\mytmm}}{\myapp{\mysnd}{\mytmm}} \mydefeq \mypair{\myapp{\myfst}{\mytmn}}{\myapp{\mysnd}{\mytmn}}}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
1367 \UnaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
1374 \AxiomC{$\myjud{\mytmm}{\myunit}$}
1375 \AxiomC{$\myjud{\mytmn}{\myunit}$}
1376 \BinaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\myunit}$}
1379 \AxiomC{$\myjud{\mytmm}{\myempty}$}
1380 \AxiomC{$\myjud{\mytmn}{\myempty}$}
1381 \BinaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\myempty}$}
1386 \subsubsection{Uniqueness of identity proofs}
1388 Another common but controversial addition to propositional equality is
1389 the $\myfun{K}$ axiom, which essentially states that all equality proofs
1392 \mydesc{typing:}{\myjud{\mytmm \mydefeq \mytmn}{\mytmsyn}}{
1395 \myjud{\myse{P}}{\myfora{\myb{x}}{\mytya}{\myb{x} \mypeq{\mytya} \myb{x} \myarr \mytyp}} \\\
1396 \myjud{\mytmt}{\mytya} \hspace{1cm}
1397 \myjud{\myse{p}}{\myse{P} \myappsp \mytmt \myappsp (\myrefl \myappsp \mytmt)} \hspace{1cm}
1398 \myjud{\myse{q}}{\mytmt \mypeq{\mytya} \mytmt}
1401 \UnaryInfC{$\myjud{\myfun{K} \myappsp \myse{P} \myappsp \myse{t} \myappsp \myse{p} \myappsp \myse{q}}{\myse{P} \myappsp \mytmt \myappsp \myse{q}}$}
1405 \cite{Hofmann1994} showed that $\myfun{K}$ is not derivable from the
1406 $\myjeqq$ axiom that we presented, and \cite{McBride2004} showed that it is
1407 needed to implement `dependent pattern matching', as first proposed by
1408 \cite{Coquand1992}. Thus, $\myfun{K}$ is derivable in the systems that
1409 implement dependent pattern matching, such as Epigram and Agda; but for
1412 $\myfun{K}$ is controversial mainly because it is at odds with
1413 equalities that include computational behaviour, most notably
1414 Voevodsky's `Univalent Foundations', which includes a \emph{univalence}
1415 axiom that identifies isomorphisms between types with propositional
1416 equality. For example we would have two isomorphisms, and thus two
1417 equalities, between $\mybool$ and $\mybool$, corresponding to the two
1418 permutations---one is the identity, and one swaps the elements. Given
1419 this, $\myfun{K}$ and univalence are inconsistent, and thus a form of
1420 dependent pattern matching that does not imply $\myfun{K}$ is subject of
1421 research.\footnote{More information about univalence can be found at
1422 \url{http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations.html}.}
1424 \subsection{Limitations}
1426 \epigraph{\emph{Half of my time spent doing research involves thinking up clever
1427 schemes to avoid needing functional extensionality.}}{@larrytheliquid}
1429 However, propositional equality as described is quite restricted when
1430 reasoning about equality beyond the term structure, which is what definitional
1431 equality gives us (extension notwithstanding).
1433 The problem is best exemplified by \emph{function extensionality}. In
1434 mathematics, we would expect to be able to treat functions that give equal
1435 output for equal input as the same. When reasoning in a mechanised framework
1436 we ought to be able to do the same: in the end, without considering the
1437 operational behaviour, all functions equal extensionally are going to be
1438 replaceable with one another.
1440 However this is not the case, or in other words with the tools we have we have
1443 \myfun{ext} : \myfora{\myb{A}\ \myb{B}}{\mytyp}{\myfora{\myb{f}\ \myb{g}}{
1444 \myb{A} \myarr \myb{B}}{
1445 (\myfora{\myb{x}}{\myb{A}}{\myapp{\myb{f}}{\myb{x}} \mypeq{\myb{B}} \myapp{\myb{g}}{\myb{x}}}) \myarr
1446 \myb{f} \mypeq{\myb{A} \myarr \myb{B}} \myb{g}
1450 To see why this is the case, consider the functions
1451 \[\myabs{\myb{x}}{0 \mathrel{\myfun{$+$}} \myb{x}}$ and $\myabs{\myb{x}}{\myb{x} \mathrel{\myfun{$+$}} 0}\]
1452 where $\myfun{$+$}$ is defined by recursion on the first argument,
1453 gradually destructing it to build up successors of the second argument.
1454 The two functions are clearly extensionally equal, and we can in fact
1457 \myfora{\myb{x}}{\mynat}{(0 \mathrel{\myfun{$+$}} \myb{x}) \mypeq{\mynat} (\myb{x} \mathrel{\myfun{$+$}} 0)}
1459 By analysis on the $\myb{x}$. However, the two functions are not
1460 definitionally equal, and thus we won't be able to get rid of the
1463 For the reasons above, theories that offer a propositional equality
1464 similar to what we presented are called \emph{intensional}, as opposed
1465 to \emph{extensional}. Most systems in wide use today (such as Agda,
1466 Coq, and Epigram) are of this kind.
1468 This is quite an annoyance that often makes reasoning awkward to execute. It
1469 also extends to other fields, for example proving bisimulation between
1470 processes specified by coinduction, or in general proving equivalences based
1471 on the behaviour on a term.
1473 \subsection{Equality reflection}
1475 One way to `solve' this problem is by identifying propositional equality with
1476 definitional equality:
1478 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1479 \AxiomC{$\myjud{\myse{q}}{\mytmm \mypeq{\mytya} \mytmn}$}
1480 \UnaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\mytya}$}
1484 This rule takes the name of \emph{equality reflection}, and is a very
1485 different rule from the ones we saw up to now: it links a typing judgement
1486 internal to the type theory to a meta-theoretic judgement that the type
1487 checker uses to work with terms. It is easy to see the dangerous consequences
1490 \item The rule is syntax directed, and the type checker is presumably expected
1491 to come up with equality proofs when needed.
1492 \item More worryingly, type checking becomes undecidable also because
1493 computing under false assumptions becomes unsafe, since we derive any
1494 equality proof and then use equality reflection and the conversion
1495 rule to have terms of any type.
1498 Given these facts theories employing equality reflection, like NuPRL
1499 \citep{NuPRL}, carry the derivations that gave rise to each typing judgement
1500 to keep the systems manageable.
1502 For all its faults, equality reflection does allow us to prove extensionality,
1503 using the extensions we gave above. Assuming that $\myctx$ contains
1504 \[\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}}}\]
1508 \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}$}
1509 \RightLabel{equality reflection}
1510 \UnaryInfC{$\myjudd{\myctx; \myb{x} : \myb{A}}{\myapp{\myb{f}}{\myb{x}} \mydefeq \myapp{\myb{g}}{\myb{x}}}{\myb{B}}$}
1511 \RightLabel{congruence for $\lambda$s}
1512 \UnaryInfC{$\myjud{(\myabs{\myb{x}}{\myapp{\myb{f}}{\myb{x}}}) \mydefeq (\myabs{\myb{x}}{\myapp{\myb{g}}{\myb{x}}})}{\myb{A} \myarr \myb{B}}$}
1513 \RightLabel{$\eta$-law for $\lambda$}
1514 \UnaryInfC{$\hspace{1.45cm}\myjud{\myb{f} \mydefeq \myb{g}}{\myb{A} \myarr \myb{B}}\hspace{1.45cm}$}
1515 \RightLabel{$\myrefl$}
1516 \UnaryInfC{$\myjud{\myapp{\myrefl}{\myb{f}}}{\myb{f} \mypeq{} \myb{g}}$}
1519 Now, the question is: do we need to give up well-behavedness of our theory to
1520 gain extensionality?
1522 \subsection{Some alternatives}
1525 % TODO add `extentional axioms' (Hoffman), setoid models (Thorsten)
1527 \section{Observational equality}
1530 A recent development by \citet{Altenkirch2007}, \emph{Observational Type
1531 Theory} (OTT), promises to keep the well behavedness of ITT while
1532 being able to gain many useful equality proofs,\footnote{It is suspected
1533 that OTT gains \emph{all} the equality proofs of ETT, but no proof
1534 exists yet.} including function extensionality. The main idea is to
1535 give the user the possibility to \emph{coerce} (or transport) values
1536 from a type $\mytya$ to a type $\mytyb$, if the type checker can prove
1537 structurally that $\mytya$ and $\mytya$ are equal; and providing a
1538 value-level equality based on similar principles. Here we give an
1539 exposition which follows closely the original paper.
1541 \subsection{A simpler theory, a propositional fragment}
1544 $\mytyp_l$ is replaced by $\mytyp$. \\\ \\
1546 \begin{array}{r@{\ }c@{\ }l}
1547 \mytmsyn & ::= & \cdots \mysynsep \myprdec{\myprsyn} \mysynsep
1548 \myITE{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
1549 \myprsyn & ::= & \mybot \mysynsep \mytop \mysynsep \myprsyn \myand \myprsyn
1550 \mysynsep \myprfora{\myb{x}}{\mytmsyn}{\myprsyn}
1555 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1557 \AxiomC{$\myjud{\myse{P}}{\myprop}$}
1558 \UnaryInfC{$\myjud{\myprdec{\myse{P}}}{\mytyp}$}
1561 \AxiomC{$\myjud{\mytmt}{\mybool}$}
1562 \AxiomC{$\myjud{\mytya}{\mytyp}$}
1563 \AxiomC{$\myjud{\mytyb}{\mytyp}$}
1564 \TrinaryInfC{$\myjud{\myITE{\mytmt}{\mytya}{\mytyb}}{\mytyp}$}
1569 \mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
1570 \begin{tabular}{ccc}
1571 \AxiomC{\phantom{$\myjud{\myse{P}}{\myprop}$}}
1572 \UnaryInfC{$\myjud{\mytop}{\myprop}$}
1574 \UnaryInfC{$\myjud{\mybot}{\myprop}$}
1577 \AxiomC{$\myjud{\myse{P}}{\myprop}$}
1578 \AxiomC{$\myjud{\myse{Q}}{\myprop}$}
1579 \BinaryInfC{$\myjud{\myse{P} \myand \myse{Q}}{\myprop}$}
1581 \UnaryInfC{\phantom{$\myjud{\mybot}{\myprop}$}}
1584 \AxiomC{$\myjud{\myse{A}}{\mytyp}$}
1585 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\myse{P}}{\myprop}$}
1586 \BinaryInfC{$\myjud{\myprfora{\myb{x}}{\mytya}{\myse{P}}}{\myprop}$}
1588 \UnaryInfC{\phantom{$\myjud{\mybot}{\myprop}$}}
1593 Our foundation will be a type theory like the one of section
1594 \ref{sec:itt}, with only one level: $\mytyp_0$. In this context we will
1595 drop the $0$ and call $\mytyp_0$ $\mytyp$. Moreover, since the old
1596 $\myfun{if}\myarg\myfun{then}\myarg\myfun{else}$ was able to return
1597 types thanks to the hierarchy (which is gone), we need to reintroduce an
1598 ad-hoc conditional for types, where the reduction rule is the obvious
1601 However, we have an addition: a universe of \emph{propositions},
1602 $\myprop$. $\myprop$ isolates a fragment of types at large, and
1603 indeed we can `inject' any $\myprop$ back in $\mytyp$ with $\myprdec{\myarg}$: \\
1604 \mydesc{proposition decoding:}{\myprdec{\mytmsyn} \myred \mytmsyn}{
1607 \begin{array}{l@{\ }c@{\ }l}
1608 \myprdec{\mybot} & \myred & \myempty \\
1609 \myprdec{\mytop} & \myred & \myunit
1614 \begin{array}{r@{ }c@{ }l@{\ }c@{\ }l}
1615 \myprdec{&\myse{P} \myand \myse{Q} &} & \myred & \myprdec{\myse{P}} \myprod \myprdec{\myse{Q}} \\
1616 \myprdec{&\myprfora{\myb{x}}{\mytya}{\myse{P}} &} & \myred &
1617 \myfora{\myb{x}}{\mytya}{\myprdec{\myse{P}}}
1622 Propositions are what we call the types of \emph{proofs}, or types
1623 whose inhabitants contain no `data', much like $\myunit$. The goal of
1624 doing this is twofold: erasing all top-level propositions when
1625 compiling; and to identify all equivalent propositions as the same, as
1628 Why did we choose what we have in $\myprop$? Given the above
1629 criteria, $\mytop$ obviously fits the bill. A pair of propositions
1630 $\myse{P} \myand \myse{Q}$ still won't get us data. Finally, if
1631 $\myse{P}$ is a proposition and we have
1632 $\myprfora{\myb{x}}{\mytya}{\myse{P}}$ , the decoding will be a
1633 function which returns propositional content. The only threat is
1634 $\mybot$, by which we can fabricate anything we want: however if we
1635 are consistent there will be nothing of type $\mybot$ at the top
1636 level, which is what we care about regarding proof erasure.
1638 \subsection{Equality proofs}
1642 \begin{array}{r@{\ }c@{\ }l}
1643 \mytmsyn & ::= & \cdots \mysynsep
1644 \mycoee{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \mysynsep
1645 \mycohh{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
1646 \myprsyn & ::= & \cdots \mysynsep \mytmsyn \myeq \mytmsyn \mysynsep
1647 \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn}
1652 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1654 \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
1655 \AxiomC{$\myjud{\mytmt}{\mytya}$}
1656 \BinaryInfC{$\myjud{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}$}
1659 \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
1660 \AxiomC{$\myjud{\mytmt}{\mytya}$}
1661 \BinaryInfC{$\myjud{\mycohh{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\myprdec{\myjm{\mytmt}{\mytya}{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}}}$}
1667 \mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
1672 \myjud{\myse{A}}{\mytyp} \hspace{1cm} \myjud{\myse{B}}{\mytyp}
1675 \UnaryInfC{$\myjud{\mytya \myeq \mytyb}{\myprop}$}
1680 \myjud{\myse{A}}{\mytyp} \hspace{1cm} \myjud{\mytmm}{\myse{A}} \\
1681 \myjud{\myse{B}}{\mytyp} \hspace{1cm} \myjud{\mytmn}{\myse{B}}
1684 \UnaryInfC{$\myjud{\myjm{\mytmm}{\myse{A}}{\mytmn}{\myse{B}}}{\myprop}$}
1691 While isolating a propositional universe as presented can be a useful
1692 exercises on its own, what we are really after is a useful notion of
1693 equality. In OTT we want to maintain the notion that things judged to
1694 be equal are still always repleaceable for one another with no
1695 additional changes. Note that this is not the same as saying that they
1696 are definitionally equal, since as we saw extensionally equal functions,
1697 while satisfying the above requirement, are not definitionally equal.
1699 Towards this goal we introduce two equality constructs in
1700 $\myprop$---the fact that they are in $\myprop$ indicates that they
1701 indeed have no computational content. The first construct, $\myarg
1702 \myeq \myarg$, relates types, the second,
1703 $\myjm{\myarg}{\myarg}{\myarg}{\myarg}$, relates values. The
1704 value-level equality is different from our old propositional equality:
1705 instead of ranging over only one type, we might form equalities between
1706 values of different types---the usefulness of this construct will be
1707 clear soon. In the literature this equality is known as `heterogeneous'
1708 or `John Major', since
1711 John Major's `classless society' widened people's aspirations to
1712 equality, but also the gap between rich and poor. After all, aspiring
1713 to be equal to others than oneself is the politics of envy. In much
1714 the same way, forms equations between members of any type, but they
1715 cannot be treated as equals (ie substituted) unless they are of the
1716 same type. Just as before, each thing is only equal to
1717 itself. \citep{McBride1999}.
1720 Correspondingly, at the term level, $\myfun{coe}$ (`coerce') lets us
1721 transport values between equal types; and $\myfun{coh}$ (`coherence')
1722 guarantees that $\myfun{coe}$ respects the value-level equality, or in
1723 other words that it really has no computational component: if we
1724 transport $\mytmm : \mytya$ to $\mytmn : \mytyb$, $\mytmm$ and $\mytmn$
1725 will still be the same.
1727 Before introducing the core ideas that make OTT work, let us distinguish
1728 between \emph{canonical} and \emph{neutral} types. Canonical types are
1729 those arising from the ground types ($\myempty$, $\myunit$, $\mybool$)
1730 and the three type formers ($\myarr$, $\myprod$, $\mytyc{W}$). Neutral
1731 types are those formed by
1732 $\myfun{If}\myarg\myfun{Then}\myarg\myfun{Else}\myarg$.
1733 Correspondingly, canonical terms are those inhabiting canonical types
1734 ($\mytt$, $\mytrue$, $\myfalse$, $\myabss{\myb{x}}{\mytya}{\mytmt}$,
1735 ...), and neutral terms those formed by eliminators.\footnote{Using the
1736 terminology from Section \ref{sec:types}, we'd say that canonical
1737 terms are in \emph{weak head normal form}.} In the current system
1738 (and hopefully in well-behaved systems), all closed terms reduce to a
1739 canonical term, and all canonical types are inhabited by canonical
1742 \subsubsection{Type equality, and coercions}
1744 The plan is to decompose type-level equalities between canonical types
1745 into decodable propositions containing equalities regarding the
1746 subterms, and to use coerce recursively on the subterms using the
1747 generated equalities. This interplay between type equalities and
1748 \myfun{coe} ensures that invocations of $\myfun{coe}$ will vanish when
1749 we have evidence of the structural equality of the types we are
1750 transporting terms across. If the type is neutral, the equality won't
1751 reduce and thus $\myfun{coe}$ won't reduce either. If we come an
1752 equality between different canonical types, then we reduce the equality
1753 to bottom, making sure that no such proof can exist, and providing an
1754 `escape hatch' in $\myfun{coe}$.
1758 \mydesc{equality reduction:}{\myprsyn \myred \myprsyn}{
1760 \begin{array}{c@{\ }c@{\ }c@{\ }l}
1761 \myempty & \myeq & \myempty & \myred \mytop \\
1762 \myunit & \myeq & \myunit & \myred \mytop \\
1763 \mybool & \myeq & \mybool & \myred \mytop \\
1764 \myexi{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myexi{\myb{x_2}}{\mytya_2}{\mytya_2} & \myred \\
1766 \myind{2} \mytya_1 \myeq \mytyb_1 \myand
1767 \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}]}
1769 \myfora{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myfora{\myb{x_2}}{\mytya_2}{\mytyb_2} & \myred \cdots \\
1770 \myw{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myw{\myb{x_2}}{\mytya_2}{\mytyb_2} & \myred \cdots \\
1771 \mytya & \myeq & \mytyb & \myred \mybot\ \text{if $\mytya$ and $\mytyb$ are canonical.}
1776 \mydesc{reduction}{\mytmsyn \myred \mytmsyn}{
1778 \begin{array}[t]{@{}l@{\ }l@{\ }l@{\ }l@{\ }l@{\ }c@{\ }l@{\ }}
1779 \mycoe & \myempty & \myempty & \myse{Q} & \myse{t} & \myred & \myse{t} \\
1780 \mycoe & \myunit & \myunit & \myse{Q} & \myse{t} & \myred & \mytt \\
1781 \mycoe & \mybool & \mybool & \myse{Q} & \mytrue & \myred & \mytrue \\
1782 \mycoe & \mybool & \mybool & \myse{Q} & \myfalse & \myred & \myfalse \\
1783 \mycoe & (\myexi{\myb{x_1}}{\mytya_1}{\mytyb_1}) &
1784 (\myexi{\myb{x_2}}{\mytya_2}{\mytyb_2}) & \myse{Q} &
1785 \mytmt_1 & \myred & \\
1787 \myind{2}\begin{array}[t]{l@{\ }l@{\ }c@{\ }l}
1788 \mysyn{let} & \myb{\mytmm_1} & \mapsto & \myapp{\myfst}{\mytmt_1} : \mytya_1 \\
1789 & \myb{\mytmn_1} & \mapsto & \myapp{\mysnd}{\mytmt_1} : \mysub{\mytyb_1}{\myb{x_1}}{\myb{\mytmm_1}} \\
1790 & \myb{Q_A} & \mapsto & \myapp{\myfst}{\myse{Q}} : \mytya_1 \myeq \mytya_2 \\
1791 & \myb{\mytmm_2} & \mapsto & \mycoee{\mytya_1}{\mytya_2}{\myb{Q_A}}{\myb{\mytmm_1}} : \mytya_2 \\
1792 & \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}}} \\
1793 & \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}} \\
1794 \mysyn{in} & \multicolumn{3}{@{}l}{\mypair{\myb{\mytmm_2}}{\myb{\mytmn_2}}}
1797 \mycoe & (\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}) &
1798 (\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}) & \myse{Q} &
1802 \mycoe & (\myw{\myb{x_1}}{\mytya_1}{\mytyb_1}) &
1803 (\myw{\myb{x_2}}{\mytya_2}{\mytyb_2}) & \myse{Q} &
1807 \mycoe & \mytya & \mytyb & \myse{Q} & \mytmt & \myred & \myapp{\myabsurd{\mytyb}}{\myse{Q}}\ \text{if $\mytya$ and $\mytyb$ are canonical.}
1811 \caption{Reducing type equalities, and using them when
1812 $\myfun{coe}$rcing.}
1816 Figure \ref{fig:eqred} illustrates this idea in practice. For ground
1817 types, the proof is the trivial element, and \myfun{coe} is the
1818 identity. For $\myunit$, we can do better: we return its only member
1819 without matching on the term. For the three type binders, things are
1820 similar but subtly different---the choices we make in the type equality
1821 are dictated by the desire of writing the $\myfun{coe}$ in a natural
1824 $\myprod$ is the easiest case: we decompose the proof into proofs that
1825 the first element's types are equal ($\mytya_1 \myeq \mytya_2$), and a
1826 proof that given equal values in the first element, the types of the
1827 second elements are equal too
1828 ($\myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{\myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2}}
1829 \myimpl \mytyb_1 \myeq \mytyb_2}$).\footnote{We are using $\myimpl$ to
1830 indicate a $\forall$ where we discard the first value. We write
1831 $\mytyb_1[\myb{x_1}]$ to indicate that the $\myb{x_1}$ in $\mytyb_1$
1832 is re-bound to the $\myb{x_1}$ quantified by the $\forall$, and
1833 similarly for $\myb{x_2}$ and $\mytyb_2$.} This also explains the
1834 need for heterogeneous equality, since in the second proof it would be
1835 awkward to express the fact that $\myb{A_1}$ is the same as $\myb{A_2}$.
1836 In the respective $\myfun{coe}$ case, since the types are canonical, we
1837 know at this point that the proof of equality is a pair of the shape
1838 described above. Thus, we can immediately coerce the first element of
1839 the pair using the first element of the proof, and then instantiate the
1840 second element with the two first elements and a proof by coherence of
1841 their equality, since we know that the types are equal.
1843 The cases for the other binders are omitted for brevity, but they follow
1844 the same principle with some twists to make $\myfun{coe}$ work with the
1845 generated proofs; the reader can refer to the paper for details.
1847 \subsubsection{$\myfun{coe}$, laziness, and $\myfun{coh}$erence}
1849 It is important to notice that in the reduction rules for $\myfun{coe}$
1850 are never obstructed by the proofs: with the exception of comparisons
1851 between different canonical types we never `pattern match' on the proof
1852 pairs, but always look at the projections. This means that, as long as
1853 we are consistent, and thus as long as we don't have $\mybot$-inducing
1854 proofs, we can add propositional axioms for equality and $\myfun{coe}$
1855 will still compute. Thus, we can take $\myfun{coh}$ as axiomatic, and
1856 we can add back familiar useful equality rules:
1858 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1859 \AxiomC{$\myjud{\mytmt}{\mytya}$}
1860 \UnaryInfC{$\myjud{\myapp{\myrefl}{\mytmt}}{\myprdec{\myjm{\mytmt}{\mytya}{\mytmt}{\mytya}}}$}
1865 \AxiomC{$\myjud{\mytya}{\mytyp}$}
1866 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytyb}{\mytyp}$}
1867 \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}}}}}$}
1871 $\myrefl$ is the equivalent of the reflexivity rule in propositional
1872 equality, and $\mytyc{R}$ asserts that if we have a we have a $\mytyp$
1873 abstracting over a value we can substitute equal for equal---this lets
1874 us recover $\myfun{subst}$. Note that while we need to provide ad-hoc
1875 rules in the restricted, non-hierarchical theory that we have, if our
1876 theory supports abstraction over $\mytyp$s we can easily add these
1877 axioms as abstracted variables.
1879 \subsubsection{Value-level equality}
1881 \mydesc{equality reduction:}{\myprsyn \myred \myprsyn}{
1883 \begin{array}{r@{ }c@{\ }c@{\ }c@{}l@{\ }c@{\ }r@{}c@{\ }c@{\ }c@{}l@{\ }l}
1884 (&\mytmt_1 & : & \myempty&) & \myeq & (&\mytmt_2 & : & \myempty &) & \myred \mytop \\
1885 (&\mytmt_1 & : & \myunit&) & \myeq & (&\mytmt_2 & : & \myunit&) & \myred \mytop \\
1886 (&\mytrue & : & \mybool&) & \myeq & (&\mytrue & : & \mybool&) & \myred \mytop \\
1887 (&\myfalse & : & \mybool&) & \myeq & (&\myfalse & : & \mybool&) & \myred \mytop \\
1888 (&\mytrue & : & \mybool&) & \myeq & (&\myfalse & : & \mybool&) & \myred \mybot \\
1889 (&\myfalse & : & \mybool&) & \myeq & (&\mytrue & : & \mybool&) & \myred \mybot \\
1890 (&\mytmt_1 & : & \myexi{\mytya_1}{\myb{x_1}}{\mytyb_1}&) & \myeq & (&\mytmt_2 & : & \myexi{\mytya_2}{\myb{x_2}}{\mytyb_2}&) & \myred \\
1891 & \multicolumn{11}{@{}l}{
1892 \myind{2} \myjm{\myapp{\myfst}{\mytmt_1}}{\mytya_1}{\myapp{\myfst}{\mytmt_2}}{\mytya_2} \myand
1893 \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}}}
1895 (&\myse{f}_1 & : & \myfora{\mytya_1}{\myb{x_1}}{\mytyb_1}&) & \myeq & (&\myse{f}_2 & : & \myfora{\mytya_2}{\myb{x_2}}{\mytyb_2}&) & \myred \\
1896 & \multicolumn{11}{@{}l}{
1897 \myind{2} \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{
1898 \myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2} \myimpl
1899 \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}]}
1902 (&\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 \\
1903 (&\mytmt_1 & : & \mytya_1&) & \myeq & (&\mytmt_2 & : & \mytya_2 &) & \myred \mybot\ \text{if $\mytya_1$ and $\mytya_2$ are canonical.}
1908 As with type-level equality, we want value-level equality to reduce
1909 based on the structure of the compared terms. When matching
1910 propositional data, such as $\myempty$ and $\myunit$, we automatically
1911 return the trivial type, since if a type has zero one members, all
1912 members will be equal. When matching on data-bearing types, such as
1913 $\mybool$, we check that such data matches, and return bottom otherwise.
1915 \subsection{Proof irrelevance and stuck coercions}
1916 \label{sec:ott-quot}
1918 The last effort is required to make sure that proofs (members of
1919 $\myprop$) are \emph{irrelevant}. Since they are devoid of
1920 computational content, we would like to identify all equivalent
1921 propositions as the same, in a similar way as we identified all
1922 $\myempty$ and all $\myunit$ as the same in section
1923 \ref{sec:eta-expand}.
1925 Thus we will have a quotation that will not only perform
1926 $\eta$-expansion, but will also identify and mark proofs that could not
1927 be decoded (that is, equalities on neutral types). Then, when
1928 comparing terms, marked proofs will be considered equal without
1929 analysing their contents, thus gaining irrelevance.
1931 Moreover we can safely advance `stuck' $\myfun{coe}$rcions between
1932 non-canonical but definitionally equal types. Consider for example
1934 \mycoee{(\myITE{\myb{b}}{\mynat}{\mybool})}{(\myITE{\myb{b}}{\mynat}{\mybool})}{\myb{x}}
1936 Where $\myb{b}$ and $\myb{x}$ are abstracted variables. This
1937 $\myfun{coe}$ will not advance, since the types are not canonical.
1938 However they are definitionally equal, and thus we can safely remove the
1939 coerce and return $\myb{x}$ as it is.
1941 This process of identifying every proof as equivalent and removing
1942 $\myfun{coe}$rcions is known as \emph{quotation}.
1944 \section{\mykant : the theory}
1945 \label{sec:kant-theory}
1947 \mykant\ is an interactive theorem prover developed as part of this thesis.
1948 The plan is to present a core language which would be capable of serving as
1949 the basis for a more featureful system, while still presenting interesting
1950 features and more importantly observational equality.
1952 We will first present the features of the system, and then describe the
1953 implementation we have developed in Section \ref{sec:kant-practice}.
1955 The defining features of \mykant\ are:
1958 \item[Full dependent types] As we would expect, we have dependent a system
1959 which is as expressive as the `best' corner in the lambda cube described in
1960 Section \ref{sec:itt}.
1962 \item[Implicit, cumulative universe hierarchy] The user does not need to
1963 specify universe level explicitly, and universes are \emph{cumulative}.
1965 \item[User defined data types and records] Instead of forcing the user to
1966 choose from a restricted toolbox, we let her define inductive data types,
1967 with associated primitive recursion operators; or records, with associated
1968 projections for each field.
1970 \item[Bidirectional type checking] While no `fancy' inference via
1971 unification is present, we take advantage of a type synthesis system
1972 in the style of \cite{Pierce2000}, extending the concept for user
1975 \item[Observational equality] As described in Section \ref{sec:ott} but
1976 extended to work with the type hierarchy and to admit equality between
1977 arbitrary data types.
1980 We will analyse the features one by one, along with motivations and
1981 tradeoffs for the design decisions made.
1983 \subsection{Bidirectional type checking}
1985 We start by describing bidirectional type checking since it calls for
1986 fairly different typing rules that what we have seen up to now. The
1987 idea is to have two kinds of terms: terms for which a type can always be
1988 inferred, and terms that need to be checked against a type. A nice
1989 observation is that this duality runs through the semantics of the
1990 terms: neutral terms (abstracted or defined variables, function
1991 application, record projections, primitive recursors, etc.) \emph{infer}
1992 types, canonical terms (abstractions, record/data types data
1993 constructors, etc.) need to be \emph{checked}.
1995 To introduce the concept and notation, we will revisit the STLC in a
1996 bidirectional style. The presentation follows \cite{Loh2010}. The
1997 syntax for our bidirectional STLC is the same as the untyped
1998 $\lambda$-calculus, but with an extra construct to annotate terms
1999 explicitly---this will be necessary when having top-level canonical
2000 terms. The types are the same as those found in the normal STLC.
2004 \begin{array}{r@{\ }c@{\ }l}
2005 \mytmsyn & ::= & \myb{x} \mysynsep \myabs{\myb{x}}{\mytmsyn} \mysynsep (\myapp{\mytmsyn}{\mytmsyn}) \mysynsep (\mytmsyn : \mytysyn)
2009 We will have two kinds of typing judgements: \emph{inference} and
2010 \emph{checking}. $\myinf{\mytmt}{\mytya}$ indicates that $\mytmt$
2011 infers the type $\mytya$, while $\mychk{\mytmt}{\mytya}$ can be checked
2012 against type $\mytya$. The type of variables in context is inferred,
2013 and so are annotate terms. The type of applications is inferred too,
2014 propagating types down the applied term. Abstractions are checked.
2015 Finally, we have a rule to check the type of an inferrable term.
2017 \mydesc{typing:}{\myctx \vdash \mytmsyn \Leftrightarrow \mytmsyn}{
2018 \begin{tabular}{ccc}
2019 \AxiomC{$\myctx(x) = A$}
2020 \UnaryInfC{$\myinf{\myb{x}}{A}$}
2023 \AxiomC{$\myjudd{\myctx;\myb{x} : A}{\mytmt}{\mytyb}$}
2024 \UnaryInfC{$\mychk{\myabs{x}{\mytmt}}{\mytyb}$}
2027 \AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$}
2028 \AxiomC{$\myjud{\mytmn}{\mytya}$}
2029 \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mytyb}$}
2036 \AxiomC{$\mychk{\mytmt}{\mytya}$}
2037 \UnaryInfC{$\myinf{\myann{\mytmt}{\mytya}}{\mytya}$}
2040 \AxiomC{$\myinf{\mytmt}{\mytya}$}
2041 \UnaryInfC{$\mychk{\mytmt}{\mytya}$}
2046 For example, if we wanted to type function composition (in this case for
2047 naturals), we would have to annotate the term:
2049 \myfun{comp} \mapsto (\myabs{\myb{f}\, \myb{g}\, \myb{x}}{\myb{f}\myappsp(\myb{g}\myappsp\myb{x})}) : (\mynat \myarr \mynat) \myarr (\mynat \myarr \mynat) \myarr \mynat \myarr \mynat
2051 But we would not have to annotate functions passed to it, since the type would be propagated to the arguments:
2053 \myfun{comp}\myappsp (\myabs{\myb{x}}{\myb{x} \mathrel{\myfun{$+$}} 3}) \myappsp (\myabs{\myb{x}}{\myb{x} \mathrel{\myfun{$*$}} 4}) \myappsp 42
2056 \subsection{Base terms and types}
2058 Let us begin by describing the primitives available without the user
2059 defining any data types, and without equality. The way we handle
2060 variables and substitution is left unspecified, and explained in section
2061 \ref{sec:term-repr}, along with other implementation issues. We are
2062 also going to give an account of the implicit type hierarchy separately
2063 in Section \ref{sec:term-hierarchy}, so as not to clutter derivation
2064 rules too much, and just treat types as impredicative for the time
2069 \begin{array}{r@{\ }c@{\ }l}
2070 \mytmsyn & ::= & \mynamesyn \mysynsep \mytyp \\
2071 & | & \myfora{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
2072 \myabs{\myb{x}}{\mytmsyn} \mysynsep
2073 (\myapp{\mytmsyn}{\mytmsyn}) \mysynsep
2074 (\myann{\mytmsyn}{\mytmsyn}) \\
2075 \mynamesyn & ::= & \myb{x} \mysynsep \myfun{f}
2080 The syntax for our calculus includes just two basic constructs:
2081 abstractions and $\mytyp$s. Everything else will be provided by
2082 user-definable constructs. Since we let the user define values, we will
2083 need a context capable of carrying the body of variables along with
2086 Bound names and defined names are treated separately in the syntax, and
2087 while both can be associated to a type in the context, only defined
2088 names can be associated with a body:
2090 \mydesc{context validity:}{\myvalid{\myctx}}{
2091 \begin{tabular}{ccc}
2092 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
2093 \UnaryInfC{$\myvalid{\myemptyctx}$}
2096 \AxiomC{$\myjud{\mytya}{\mytyp}$}
2097 \AxiomC{$\mynamesyn \not\in \myctx$}
2098 \BinaryInfC{$\myvalid{\myctx ; \mynamesyn : \mytya}$}
2101 \AxiomC{$\myjud{\mytmt}{\mytya}$}
2102 \AxiomC{$\myfun{f} \not\in \myctx$}
2103 \BinaryInfC{$\myvalid{\myctx ; \myfun{f} \mapsto \mytmt : \mytya}$}
2108 Now we can present the reduction rules, which are unsurprising. We have
2109 the usual function application ($\beta$-reduction), but also a rule to
2110 replace names with their bodies ($\delta$-reduction), and one to discard
2111 type annotations. For this reason reduction is done in-context, as
2112 opposed to what we have seen in the past:
2114 \mydesc{reduction:}{\myctx \vdash \mytmsyn \myred \mytmsyn}{
2115 \begin{tabular}{ccc}
2116 \AxiomC{\phantom{$\myb{x} \mapsto \mytmt : \mytya \in \myctx$}}
2117 \UnaryInfC{$\myctx \vdash \myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn}
2118 \myred \mysub{\mytmm}{\myb{x}}{\mytmn}$}
2121 \AxiomC{$\myfun{f} \mapsto \mytmt : \mytya \in \myctx$}
2122 \UnaryInfC{$\myctx \vdash \myfun{f} \myred \mytmt$}
2125 \AxiomC{\phantom{$\myb{x} \mapsto \mytmt : \mytya \in \myctx$}}
2126 \UnaryInfC{$\myctx \vdash \myann{\mytmm}{\mytya} \myred \mytmm$}
2131 We can now give types to our terms. Although we include the usual
2132 conversion rule, we defer a detailed account of definitional equality to
2133 Section \ref{sec:kant-irr}.
2135 \mydesc{typing:}{\myctx \vdash \mytmsyn \Leftrightarrow \mytmsyn}{
2136 \begin{tabular}{cccc}
2137 \AxiomC{$\myse{name} : A \in \myctx$}
2138 \UnaryInfC{$\myinf{\myse{name}}{A}$}
2141 \AxiomC{$\myfun{f} \mapsto \mytmt : A \in \myctx$}
2142 \UnaryInfC{$\myinf{\myfun{f}}{A}$}
2145 \AxiomC{$\mychk{\mytmt}{\mytya}$}
2146 \UnaryInfC{$\myinf{\myann{\mytmt}{\mytya}}{\mytya}$}
2149 \AxiomC{$\myinf{\mytmt}{\mytya}$}
2150 \AxiomC{$\myctx \vdash \mytya \mydefeq \mytyb$}
2151 \BinaryInfC{$\mychk{\mytmt}{\mytyb}$}
2156 \begin{tabular}{ccc}
2157 \AxiomC{$\myinf{\mytmm}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
2158 \AxiomC{$\mychk{\mytmn}{\mytya}$}
2159 \BinaryInfC{$\myinf{\myapp{\mytmm}{\mytmn}}{\mysub{\mytyb}{\myb{x}}{\mytmn}}$}
2164 \AxiomC{$\mychkk{\myctx; \myb{x}: \mytya}{\mytmt}{\mytyb}$}
2165 \UnaryInfC{$\mychk{\myabs{\myb{x}}{\mytmt}}{\myfora{\myb{x}}{\mytyb}{\mytyb}}$}
2170 \subsection{Elaboration}
2172 As we mentioned, $\mykant$\ allows the user to define not only values
2173 but also custom data types and records. \emph{Elaboration} consists of
2174 turning these declarations into workable syntax, types, and reduction
2175 rules. The treatment of custom types in $\mykant$\ is heavily inspired
2176 by McBride and McKinna early work on Epigram \citep{McBride2004},
2177 although with some differences.
2179 \subsubsection{Term vectors, telescopes, and assorted notation}
2181 We use a vector notation to refer to a series of term applied to
2182 another, for example $\mytyc{D} \myappsp \vec{A}$ is a shorthand for
2183 $\mytyc{D} \myappsp \mytya_1 \cdots \mytya_n$, for some $n$. $n$ is
2184 consistently used to refer to the length of such vectors, and $i$ to
2185 refer to an index in such vectors. We also often need to `build up'
2186 terms vectors, in which case we use $\myemptyctx$ for an empty vector
2187 and add elements to an existing vector with $\myarg ; \myarg$, similarly
2188 to what we do for context.
2190 To present the elaboration and operations on user defined data types, we
2191 frequently make use what de Bruijn called \emph{telescopes}
2192 \citep{Bruijn91}, a construct that will prove useful when dealing with
2193 the types of type and data constructors. A telescope is a series of
2194 nested typed bindings, such as $(\myb{x} {:} \mynat); (\myb{p} {:}
2195 \myapp{\myfun{even}}{\myb{x}})$. Consistently with the notation for
2196 contexts and term vectors, we use $\myemptyctx$ to denote an empty
2197 telescope and $\myarg ; \myarg$ to add a new binding to an existing
2200 We refer to telescopes with $\mytele$, $\mytele'$, $\mytele_i$, etc. If
2201 $\mytele$ refers to a telescope, $\mytelee$ refers to the term vector
2202 made up of all the variables bound by $\mytele$. $\mytele \myarr
2203 \mytya$ refers to the type made by turning the telescope into a series
2204 of $\myarr$. Returning to the examples above, we have that
2206 (\myb{x} {:} \mynat); (\myb{p} : \myapp{\myfun{even}}{\myb{x}}) \myarr \mynat =
2207 (\myb{x} {:} \mynat) \myarr (\myb{p} : \myapp{\myfun{even}}{\myb{x}}) \myarr \mynat
2210 We make use of various operations to manipulate telescopes:
2212 \item $\myhead(\mytele)$ refers to the first type appearing in
2213 $\mytele$: $\myhead((\myb{x} {:} \mynat); (\myb{p} :
2214 \myapp{\myfun{even}}{\myb{x}})) = \mynat$. Similarly,
2215 $\myix_i(\mytele)$ refers to the $i^{th}$ type in a telescope
2217 \item $\mytake_i(\mytele)$ refers to the telescope created by taking the
2218 first $i$ elements of $\mytele$: $\mytake_1((\myb{x} {:} \mynat); (\myb{p} :
2219 \myapp{\myfun{even}}{\myb{x}})) = (\myb{x} {:} \mynat)$.
2220 \item $\mytele \vec{A}$ refers to the telescope made by `applying' the
2221 terms in $\vec{A}$ on $\mytele$: $((\myb{x} {:} \mynat); (\myb{p} :
2222 \myapp{\myfun{even}}{\myb{x}}))42 = (\myb{p} :
2223 \myapp{\myfun{even}}{42})$.
2226 Additionally, when presenting syntax elaboration, I'll use $\mytmsyn^n$
2227 to indicate a term vector composed of $n$ elements, or
2228 $\mytmsyn^{\mytele}$ for one composed by as many elements as the
2231 \subsubsection{Declarations syntax}
2235 \begin{array}{r@{\ }c@{\ }l}
2236 \mydeclsyn & ::= & \myval{\myb{x}}{\mytmsyn}{\mytmsyn} \\
2237 & | & \mypost{\myb{x}}{\mytmsyn} \\
2238 & | & \myadt{\mytyc{D}}{\myappsp \mytelesyn}{}{\mydc{c} : \mytelesyn\ |\ \cdots } \\
2239 & | & \myreco{\mytyc{D}}{\myappsp \mytelesyn}{}{\myfun{f} : \mytmsyn,\ \cdots } \\
2241 \mytelesyn & ::= & \myemptytele \mysynsep \mytelesyn \mycc (\myb{x} {:} \mytmsyn) \\
2242 \mynamesyn & ::= & \cdots \mysynsep \mytyc{D} \mysynsep \mytyc{D}.\mydc{c} \mysynsep \mytyc{D}.\myfun{f}
2247 In \mykant\ we have four kind of declarations:
2250 \item[Defined value] A variable, together with a type and a body.
2251 \item[Abstract variable] An abstract variable, with a type but no body.
2252 \item[Inductive data] A datatype, with a type constructor and various data
2253 constructors---somewhat similar to what we find in Haskell. A primitive
2254 recursor (or `destructor') will be generated automatically.
2255 \item[Record] A record, which consists of one data constructor and various
2256 fields, with no recursive occurrences.
2259 Elaborating defined variables consists of type checking body against the
2260 given type, and updating the context to contain the new binding.
2261 Elaborating abstract variables and abstract variables consists of type
2262 checking the type, and updating the context with a new typed variable:
2264 \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
2266 \AxiomC{$\myjud{\mytmt}{\mytya}$}
2267 \AxiomC{$\myfun{f} \not\in \myctx$}
2269 $\myctx \myelabt \myval{\myfun{f}}{\mytya}{\mytmt} \ \ \myelabf\ \ \myctx; \myfun{f} \mapsto \mytmt : \mytya$
2273 \AxiomC{$\myjud{\mytya}{\mytyp}$}
2274 \AxiomC{$\myfun{f} \not\in \myctx$}
2277 \myctx \myelabt \mypost{\myfun{f}}{\mytya}
2278 \ \ \myelabf\ \ \myctx; \myfun{f} : \mytya
2285 \subsubsection{User defined types}
2286 \label{sec:user-type}
2288 Elaborating user defined types is the real effort. First, let's explain
2289 what we can defined, with some examples.
2292 \item[Natural numbers] To define natural numbers, we create a data type
2293 with two constructors: one with zero arguments ($\mydc{zero}$) and one
2294 with one recursive argument ($\mydc{suc}$):
2297 \myadt{\mynat}{ }{ }{
2298 \mydc{zero} \mydcsep \mydc{suc} \myappsp \mynat
2302 This is very similar to what we would write in Haskell:
2304 data Nat = Zero | Suc Nat
2306 Once the data type is defined, $\mykant$\ will generate syntactic
2307 constructs for the type and data constructors, so that we will have
2310 \begin{tabular}{ccc}
2311 \AxiomC{\phantom{$\mychk{\mytmt}{\mynat}$}}
2312 \UnaryInfC{$\myinf{\mynat}{\mytyp}$}
2315 \AxiomC{\phantom{$\mychk{\mytmt}{\mynat}$}}
2316 \UnaryInfC{$\myinf{\mytyc{\mynat}.\mydc{zero}}{\mynat}$}
2319 \AxiomC{$\mychk{\mytmt}{\mynat}$}
2320 \UnaryInfC{$\myinf{\mytyc{\mynat}.\mydc{suc} \myappsp \mytmt}{\mynat}$}
2324 While in Haskell (or indeed in Agda or Coq) data constructors are
2325 treated the same way as functions, in $\mykant$\ they are syntax, so
2326 for example using $\mytyc{\mynat}.\mydc{suc}$ on its own will be a
2327 syntax error. This is necessary so that we can easily infer the type
2328 of polymorphic data constructors, as we will see later.
2330 Moreover, each data constructor is prefixed by the type constructor
2331 name, since we need to retrieve the type constructor of a data
2332 constructor when type checking. This measure aids in the presentation
2333 of various features but it is not needed in the implementation, where
2334 we can have a dictionary to lookup the type constructor corresponding
2335 to each data constructor. When using data constructors in examples I
2336 will omit the type constructor prefix for brevity.
2338 Along with user defined constructors, $\mykant$\ automatically
2339 generates an \emph{eliminator}, or \emph{destructor}, to compute with
2340 natural numbers: If we have $\mytmt : \mynat$, we can destruct
2341 $\mytmt$ using the generated eliminator `$\mynat.\myfun{elim}$':
2344 \AxiomC{$\mychk{\mytmt}{\mynat}$}
2346 \myinf{\mytyc{\mynat}.\myfun{elim} \myappsp \mytmt}{
2348 \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}}
2352 $\mynat.\myfun{elim}$ corresponds to the induction principle for
2353 natural numbers: if we have a predicate on numbers ($\myb{P}$), and we
2354 know that predicate holds for the base case
2355 ($\myapp{\myb{P}}{\mydc{zero}}$) and for each inductive step
2356 ($\myfora{\myb{x}}{\mynat}{\myapp{\myb{P}}{\myb{x}} \myarr
2357 \myapp{\myb{P}}{(\myapp{\mydc{suc}}{\myb{x}})}}$), then $\myb{P}$
2358 holds for any number. As with the data constructors, we require the
2359 eliminator to be applied to the `destructed' element.
2361 While the induction principle is usually seen as a mean to prove
2362 properties about numbers, in the intuitionistic setting it is also a
2363 mean to compute. In this specific case we will $\mynat.\myfun{elim}$
2364 will return the base case if the provided number is $\mydc{zero}$, and
2365 recursively apply the inductive step if the number is a
2368 \begin{array}{@{}l@{}l}
2369 \mytyc{\mynat}.\myfun{elim} \myappsp \mydc{zero} & \myappsp \myse{P} \myappsp \myse{pz} \myappsp \myse{ps} \myred \myse{pz} \\
2370 \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})
2373 The Haskell equivalent would be
2375 elim :: Nat -> a -> (Nat -> a -> a) -> a
2376 elim Zero pz ps = pz
2377 elim (Suc n) pz ps = ps n (elim n pz ps)
2379 Which buys us the computational behaviour, but not the reasoning power.
2381 \item[Binary trees] Now for a polymorphic data type: binary trees, since
2382 lists are too similar to natural numbers to be interesting.
2385 \myadt{\mytree}{\myappsp (\myb{A} {:} \mytyp)}{ }{
2386 \mydc{leaf} \mydcsep \mydc{node} \myappsp (\myapp{\mytree}{\myb{A}}) \myappsp \myb{A} \myappsp (\myapp{\mytree}{\myb{A}})
2390 Now the purpose of constructors as syntax can be explained: what would
2391 the type of $\mydc{leaf}$ be? If we were to treat it as a `normal'
2392 term, we would have to specify the type parameter of the tree each
2393 time the constructor is applied:
2395 \begin{array}{@{}l@{\ }l}
2396 \mydc{leaf} & : \myfora{\myb{A}}{\mytyp}{\myapp{\mytree}{\myb{A}}} \\
2397 \mydc{node} & : \myfora{\myb{A}}{\mytyp}{\myapp{\mytree}{\myb{A}} \myarr \myb{A} \myarr \myapp{\mytree}{\myb{A}} \myarr \myapp{\mytree}{\myb{A}}}
2400 The problem with this approach is that creating terms is incredibly
2401 verbose and dull, since we would need to specify the type parameters
2402 each time. For example if we wished to create a $\mytree \myappsp
2403 \mynat$ with two nodes and three leaves, we would have to write
2405 \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)
2407 The redundancy of $\mynat$s is quite irritating. Instead, if we treat
2408 constructors as syntactic elements, we can `extract' the type of the
2409 parameter from the type that the term gets checked against, much like
2410 we get the type of abstraction arguments:
2414 \AxiomC{$\mychk{\mytya}{\mytyp}$}
2415 \UnaryInfC{$\mychk{\mydc{leaf}}{\myapp{\mytree}{\mytya}}$}
2418 \AxiomC{$\mychk{\mytmm}{\mytree \myappsp \mytya}$}
2419 \AxiomC{$\mychk{\mytmt}{\mytya}$}
2420 \AxiomC{$\mychk{\mytmm}{\mytree \myappsp \mytya}$}
2421 \TrinaryInfC{$\mychk{\mydc{node} \myappsp \mytmm \myappsp \mytmt \myappsp \mytmn}{\mytree \myappsp \mytya}$}
2425 Which enables us to write, much more concisely
2427 \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}
2429 We gain an annotation, but we lose the myriad of types applied to the
2430 constructors. Conversely, with the eliminator for $\mytree$, we can
2431 infer the type of the arguments given the type of the destructed:
2434 \AxiomC{$\myinf{\mytmt}{\myapp{\mytree}{\mytya}}$}
2436 \myinf{\mytree.\myfun{elim} \myappsp \mytmt}{
2438 (\myb{P} {:} \myapp{\mytree}{\mytya} \myarr \mytyp) \myarr \\
2439 \myapp{\myb{P}}{\mydc{leaf}} \myarr \\
2440 ((\myb{l} {:} \myapp{\mytree}{\mytya}) (\myb{x} {:} \mytya) (\myb{r} {:} \myapp{\mytree}{\mytya}) \myarr \myapp{\myb{P}}{\myb{l}} \myarr
2441 \myapp{\myb{P}}{\myb{r}} \myarr \myb{P} \myappsp (\mydc{node} \myappsp \myb{l} \myappsp \myb{x} \myappsp \myb{r})) \myarr \\
2442 \myapp{\myb{P}}{\mytmt}
2447 As expected, the eliminator embodies structural induction on trees.
2449 \item[Empty type] We have presented types that have at least one
2450 constructors, but nothing prevents us from defining types with
2451 \emph{no} constructors:
2452 \[\myadt{\mytyc{Empty}}{ }{ }{ }\]
2453 What shall the `induction principle' on $\mytyc{Empty}$ be? Does it
2454 even make sense to talk about induction on $\mytyc{Empty}$?
2455 $\mykant$\ does not care, and generates an eliminator with no `cases',
2456 and thus corresponding to the $\myfun{absurd}$ that we know and love:
2459 \AxiomC{$\myinf{\mytmt}{\mytyc{Empty}}$}
2460 \UnaryInfC{$\myinf{\myempty.\myfun{elim} \myappsp \mytmt}{(\myb{P} {:} \mytmt \myarr \mytyp) \myarr \myapp{\myb{P}}{\mytmt}}$}
2463 \item[Ordered lists] Up to this point, the examples shown are nothing
2464 new to the \{Haskell, SML, OCaml, functional\} programmer. However
2465 dependent types let us express much more than that. A useful example
2466 is the type of ordered lists. There are many ways to define such a
2467 thing, we will define our type to store the bounds of the list, making
2468 sure that $\mydc{cons}$ing respects that.
2470 First, using $\myunit$ and $\myempty$, we define a type expressing the
2471 ordering on natural numbers, $\myfun{le}$---`less or equal'.
2472 $\myfun{le}\myappsp \mytmm \myappsp \mytmn$ will be inhabited only if
2473 $\mytmm \le \mytmn$:
2476 \myfun{le} : \mynat \myarr \mynat \myarr \mytyp \\
2477 \myfun{le} \myappsp \myb{n} \mapsto \\
2478 \myind{2} \mynat.\myfun{elim} \\
2479 \myind{2}\myind{2} \myb{n} \\
2480 \myind{2}\myind{2} (\myabs{\myarg}{\mynat \myarr \mytyp}) \\
2481 \myind{2}\myind{2} (\myabs{\myarg}{\myunit}) \\
2482 \myind{2}\myind{2} (\myabs{\myb{n}\, \myb{f}\, \myb{m}}{
2483 \mynat.\myfun{elim} \myappsp \myb{m} \myappsp (\myabs{\myarg}{\mytyp}) \myappsp \myempty \myappsp (\myabs{\myb{m'}\, \myarg}{\myapp{\myb{f}}{\myb{m'}}})
2487 We return $\myunit$ if the scrutinised is $\mydc{zero}$ (every
2488 number in less or equal than zero), $\myempty$ if the first number is
2489 a $\mydc{suc}$cessor and the second a $\mydc{zero}$, and we recurse if
2490 they are both successors. Since we want the list to have possibly
2491 `open' bounds, for example for empty lists, we create a type for
2492 `lifted' naturals with a bottom (less than everything) and top
2493 (greater than everything) elements, along with an associated comparison
2497 \myadt{\mytyc{Lift}}{ }{ }{\mydc{bot} \mydcsep \mydc{lift} \myappsp \mynat \mydcsep \mydc{top}}\\
2498 \myfun{le'} : \mytyc{Lift} \myarr \mytyc{Lift} \myarr \mytyp\\
2499 \myfun{le'} \myappsp \myb{l_1} \mapsto \\
2500 \myind{2} \mytyc{Lift}.\myfun{elim} \\
2501 \myind{2}\myind{2} \myb{l_1} \\
2502 \myind{2}\myind{2} (\myabs{\myarg}{\mytyc{Lift} \myarr \mytyp}) \\
2503 \myind{2}\myind{2} (\myabs{\myarg}{\myunit}) \\
2504 \myind{2}\myind{2} (\myabs{\myb{n_1}\, \myb{n_2}}{
2505 \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
2507 \myind{2}\myind{2} (\myabs{\myb{n_1}\, \myb{n_2}}{
2508 \mytyc{Lift}.\myfun{elim} \myappsp \myb{l_2} \myappsp (\myabs{\myarg}{\mytyp}) \myappsp \myempty \myappsp (\myabs{\myarg}{\myempty}) \myappsp \myunit
2512 Finally, we can defined a type of ordered lists. The type is
2513 parametrised over two values representing the lower and upper bounds
2514 of the elements, as opposed to the type parameters that we are used
2515 to. Then, an empty list will have to have evidence that the bounds
2516 are ordered, and each time we add an element we require the list to
2517 have a matching lower bound:
2520 \myadt{\mytyc{OList}}{\myappsp (\myb{low}\ \myb{upp} {:} \mytyc{Lift})}{\\ \myind{2}}{
2521 \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})
2525 If we want we can then employ this structure to write and prove
2526 correct various sorting algorithms.\footnote{See this presentation by
2528 \url{https://personal.cis.strath.ac.uk/conor.mcbride/Pivotal.pdf},
2529 and this blog post by the author:
2530 \url{http://mazzo.li/posts/AgdaSort.html}.}
2532 \item[Dependent products] Apart from $\mysyn{data}$, $\mykant$\ offers
2533 us another way to define types: $\mysyn{record}$. A record is a
2534 datatype with one constructor and `projections' to extract specific
2535 fields of the said constructor.
2537 For example, we can recover dependent products:
2540 \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}}}
2543 Here $\myfst$ and $\mysnd$ are the projections, with their respective
2544 types. Note that each field can refer to the preceding fields. A
2545 constructor will be automatically generated, under the name of
2546 $\mytyc{Prod}.\mydc{constr}$. Dually to data types, we will omit the
2547 type constructor prefix for record projections.
2549 Following the bidirectionality of the system, we have that projections
2550 (the destructors of the record) infer the type, while the constructor
2555 \AxiomC{$\mychk{\mytmm}{\mytya}$}
2556 \AxiomC{$\mychk{\mytmn}{\myapp{\mytyb}{\mytmm}}$}
2557 \BinaryInfC{$\mychk{\mytyc{Prod}.\mydc{constr} \myappsp \mytmm \myappsp \mytmn}{\mytyc{Prod} \myappsp \mytya \myappsp \mytyb}$}
2559 \UnaryInfC{\phantom{$\myinf{\myfun{snd} \myappsp \mytmt}{\mytyb \myappsp (\myfst \myappsp \mytmt)}$}}
2562 \AxiomC{$\myinf{\mytmt}{\mytyc{Prod} \myappsp \mytya \myappsp \mytyb}$}
2563 \UnaryInfC{$\myinf{\myfun{fst} \myappsp \mytmt}{\mytya}$}
2565 \UnaryInfC{$\myinf{\myfun{snd} \myappsp \mytmt}{\mytyb \myappsp (\myfst \myappsp \mytmt)}$}
2569 What we have is equivalent to ITT's dependent products.
2577 \mynamesyn ::= \cdots \mysynsep \mytyc{D} \mysynsep \mytyc{D}.\mydc{c} \mysynsep \mytyc{D}.\myfun{f}
2584 \mydesc{syntax elaboration:}{\mydeclsyn \myelabf \mytmsyn ::= \cdots}{
2587 \begin{array}{r@{\ }l}
2588 & \myadt{\mytyc{D}}{\mytele}{}{\cdots\ |\ \mydc{c}_n : \mytele_n } \\
2591 \begin{array}{r@{\ }c@{\ }l}
2592 \mytmsyn & ::= & \cdots \mysynsep \myapp{\mytyc{D}}{\mytmsyn^{\mytele}} \mysynsep \cdots \mysynsep
2593 \mytyc{D}.\mydc{c}_n \myappsp \mytmsyn^{\mytele_n} \mysynsep \mytyc{D}.\myfun{elim} \myappsp \mytmsyn \\
2601 \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
2606 \myinf{\mytele \myarr \mytyp}{\mytyp}\hspace{0.8cm}
2607 \mytyc{D} \not\in \myctx \\
2608 \myinff{\myctx;\ \mytyc{D} : \mytele \myarr \mytyp}{\mytele \mycc \mytele_i \myarr \myapp{\mytyc{D}}{\mytelee}}{\mytyp}\ \ \ (1 \leq i \leq n) \\
2609 \text{For each $(\myb{x} {:} \mytya)$ in each $\mytele_i$, if $\mytyc{D} \in \mytya$, then $\mytya = \myapp{\mytyc{D}}{\vec{\mytmt}}$.}
2613 \begin{array}{r@{\ }c@{\ }l}
2614 \myctx & \myelabt & \myadt{\mytyc{D}}{\mytele}{}{ \cdots \ |\ \mydc{c}_n : \mytele_n } \\
2615 & & \vspace{-0.2cm} \\
2616 & \myelabf & \myctx;\ \mytyc{D} : \mytele \myarr \mytyp;\ \cdots;\ \mytyc{D}.\mydc{c}_n : \mytele \mycc \mytele_n \myarr \myapp{\mytyc{D}}{\mytelee}; \\
2618 \begin{array}{@{}r@{\ }l l}
2619 \mytyc{D}.\myfun{elim} : & \mytele \myarr (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr & \textbf{target} \\
2620 & (\myb{P} {:} \myapp{\mytyc{D}}{\mytelee} \myarr \mytyp) \myarr & \textbf{motive} \\
2624 (\mytele_n \mycc \myhyps(\myb{P}, \mytele_n) \myarr \myapp{\myb{P}}{(\myapp{\mytyc{D}.\mydc{c}_n}{\mytelee_n})}) \myarr
2625 \end{array} \right \}
2626 & \textbf{methods} \\
2627 & \myapp{\myb{P}}{\myb{x}} &
2631 \DisplayProof \\ \vspace{0.2cm}\ \\
2633 \begin{array}{@{}l l@{\ } l@{} r c l}
2634 \textbf{where} & \myhyps(\myb{P}, & \myemptytele &) & \mymetagoes & \myemptytele \\
2635 & \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) \\
2636 & \myhyps(\myb{P}, & (\myb{x} {:} \mytya) \mycc \mytele & ) & \mymetagoes & \myhyps(\myb{P}, \mytele)
2644 \mydesc{reduction elaboration:}{\mydeclsyn \myelabf \myctx \vdash \mytmsyn \myred \mytmsyn}{
2646 $\myadt{\mytyc{D}}{\mytele}{}{ \cdots \ |\ \mydc{c}_n : \mytele_n } \ \ \myelabf$
2647 \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
2648 \AxiomC{$\mytyc{D}.\mydc{c}_i : \mytele;\mytele_i \myarr \myapp{\mytyc{D}}{\mytelee} \in \myctx$}
2650 \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)}
2652 \DisplayProof \\ \vspace{0.2cm}\ \\
2654 \begin{array}{@{}l l@{\ } l@{} r c l}
2655 \textbf{where} & \myrecs(\myse{P}, \vec{m}, & \myemptytele &) & \mymetagoes & \myemptytele \\
2656 & \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) \\
2657 & \myrecs(\myse{P}, \vec{m}, & (\myb{x} {:} \mytya); \mytele &) & \mymetagoes & \myrecs(\myse{P}, \vec{m}, \mytele)
2664 \mydesc{syntax elaboration:}{\myelab{\mydeclsyn}{\mytmsyn ::= \cdots}}{
2667 \begin{array}{r@{\ }c@{\ }l}
2668 \myctx & \myelabt & \myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \\
2671 \begin{array}{r@{\ }c@{\ }l}
2672 \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 \\
2680 \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
2684 \myinf{\mytele \myarr \mytyp}{\mytyp}\hspace{0.8cm}
2685 \mytyc{D} \not\in \myctx \\
2686 \myinff{\myctx; \mytele; (\myb{f}_j : \myse{F}_j)_{j=1}^{i - 1}}{F_i}{\mytyp} \myind{3} (1 \le i \le n)
2690 \begin{array}{r@{\ }c@{\ }l}
2691 \myctx & \myelabt & \myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \\
2692 & & \vspace{-0.2cm} \\
2693 & \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}; \\
2694 & & \mytyc{D}.\mydc{constr} : \mytele \myarr \myse{F}_1 \myarr \cdots \myarr \myse{F}_n \myarr \myapp{\mytyc{D}}{\mytelee};
2702 \mydesc{reduction elaboration:}{\mydeclsyn \myelabf \myctx \vdash \mytmsyn \myred \mytmsyn}{
2704 $\myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \ \ \myelabf$
2705 \AxiomC{$\mytyc{D} \in \myctx$}
2706 \UnaryInfC{$\myctx \vdash \myapp{\mytyc{D}.\myfun{f}_i}{(\mytyc{D}.\mydc{constr} \myappsp \vec{t})} \myred t_i$}
2710 \caption{Elaboration for data types and records.}
2714 Following the intuition given by the examples, the mechanised
2715 elaboration is presented in figure \ref{fig:elab}, which is essentially
2716 a modification of figure 9 of \citep{McBride2004}\footnote{However, our
2717 datatypes do not have indices, we do bidirectional typechecking by
2718 treating constructors/destructors as syntactic constructs, and we have
2721 In data types declarations we allow recursive occurrences as long as
2722 they are \emph{strictly positive}, employing a syntactic check to make
2723 sure that this is the case. See \cite{Dybjer1991} for a more formal
2724 treatment of inductive definitions in ITT.
2726 For what concerns records, recursive occurrences are disallowed. The
2727 reason for this choice is answered by the reason for the choice of
2728 having records at all: we need records to give the user types with
2729 $\eta$-laws for equality, as we saw in Section \ref{sec:eta-expand}
2730 and in the treatment of OTT in Section \ref{sec:ott}. If we tried to
2731 $\eta$-expand recursive data types, we would expand forever.
2733 To implement bidirectional type checking for constructors and
2734 destructors, we store their types in full in the context, and then
2735 instantiate when due:
2737 \mydesc{typing:}{\myctx \vdash \mytmsyn \Leftrightarrow \mytmsyn}{
2740 \mytyc{D} : \mytele \myarr \mytyp \in \myctx \hspace{1cm}
2741 \mytyc{D}.\mydc{c} : \mytele \mycc \mytele' \myarr
2742 \myapp{\mytyc{D}}{\mytelee} \in \myctx \\
2743 \mytele'' = (\mytele;\mytele')\vec{A} \hspace{1cm}
2744 \mychkk{\myctx; \mytake_{i-1}(\mytele'')}{t_i}{\myix_i( \mytele'')}\ \
2745 (1 \le i \le \mytele'')
2748 \UnaryInfC{$\mychk{\myapp{\mytyc{D}.\mydc{c}}{\vec{t}}}{\myapp{\mytyc{D}}{\vec{A}}}$}
2753 \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
2754 \AxiomC{$\mytyc{D}.\myfun{f} : \mytele \mycc (\myb{x} {:}
2755 \myapp{\mytyc{D}}{\mytelee}) \myarr \myse{F}$}
2756 \AxiomC{$\myjud{\mytmt}{\myapp{\mytyc{D}}{\vec{A}}}$}
2757 \TrinaryInfC{$\myinf{\myapp{\mytyc{D}.\myfun{f}}{\mytmt}}{(\mytele
2758 \mycc (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr
2759 \myse{F})(\vec{A};\mytmt)}$}
2763 \subsubsection{Why user defined types? Why eliminators?}
2765 The `hardest' design choice when designing $\mykant$\ was to decide
2766 whether user defined types should be included. In the end, we can
2769 % TODO reference levitated theories, indexed containers
2773 \subsection{Cumulative hierarchy and typical ambiguity}
2774 \label{sec:term-hierarchy}
2776 Having a well founded type hierarchy is crucial if we want to retain
2777 consistency, otherwise we can break our type systems by proving bottom,
2778 as shown in Appendix \ref{sec:hurkens}.
2780 However, hierarchy as presented in section \label{sec:itt} is a
2781 considerable burden on the user, on various levels. Consider for
2782 example how we recovered disjunctions in Section \ref{sec:disju}: we
2783 have a function that takes two $\mytyp_0$ and forms a new $\mytyp_0$.
2784 What if we wanted to form a disjunction containing something a
2785 $\mytyp_1$, or $\mytyp_{42}$? Our definition would fail us, since
2786 $\mytyp_1 : \mytyp_2$.
2791 \mydesc{cumulativity:}{\myctx \vdash \mytmsyn \mycumul \mytmsyn}{
2792 \begin{tabular}{ccc}
2793 \AxiomC{$\myctx \vdash \mytya \mydefeq \mytyb$}
2794 \UnaryInfC{$\myctx \vdash \mytya \mycumul \mytyb$}
2797 \AxiomC{\phantom{$\myctx \vdash \mytya \mydefeq \mytyb$}}
2798 \UnaryInfC{$\myctx \vdash \mytyp_l \mycumul \mytyp_{l+1}$}
2801 \AxiomC{$\myctx \vdash \mytya \mycumul \mytyb$}
2802 \AxiomC{$\myctx \vdash \mytyb \mycumul \myse{C}$}
2803 \BinaryInfC{$\myctx \vdash \mytya \mycumul \myse{C}$}
2809 \begin{tabular}{ccc}
2810 \AxiomC{$\myjud{\mytmt}{\mytya}$}
2811 \AxiomC{$\myctx \vdash \mytya \mycumul \mytyb$}
2812 \BinaryInfC{$\myjud{\mytmt}{\mytyb}$}
2815 \AxiomC{$\myctx \vdash \mytya_1 \mydefeq \mytya_2$}
2816 \AxiomC{$\myctx; \myb{x} : \mytya_1 \vdash \mytyb_1 \mycumul \mytyb_2$}
2817 \BinaryInfC{$\myctx (\myb{x} {:} \mytya_1) \myarr \mytyb_1 \mycumul (\myb{x} {:} \mytya_2) \myarr \mytyb_2$}
2821 \caption{Cumulativity rules for base types in \mykant, plus a
2822 `conversion' rule for cumulative types.}
2823 \label{fig:cumulativity}
2826 One way to solve this issue is a \emph{cumulative} hierarchy, where
2827 $\mytyp_{l_1} : \mytyp_{l_2}$ iff $l_1 < l_2$. This way we retain
2828 consistency, while allowing for `large' definitions that work on small
2829 types too. Figure \ref{fig:cumulativity} gives a formal definition of
2830 cumulativity for types, abstractions, and data constructors.
2832 For example we might define our disjunction to be
2834 \myarg\myfun{$\vee$}\myarg : \mytyp_{100} \myarr \mytyp_{100} \myarr \mytyp_{100}
2836 And hope that $\mytyp_{100}$ will be large enough to fit all the types
2837 that we want to use with our disjunction. However, there are two
2838 problems with this. First, there is the obvious clumsyness of having to
2839 manually specify the size of types. More importantly, if we want to use
2840 $\myfun{$\vee$}$ itself as an argument to other type-formers, we need to
2841 make sure that those allow for types at least as large as
2844 A better option is to employ a mechanised version of what Russell called
2845 \emph{typical ambiguity}: we let the user live under the illusion that
2846 $\mytyp : \mytyp$, but check that the statements about types are
2847 consistent behind the hood. $\mykant$\ implements this following the
2848 lines of \cite{Huet1988}. See also \citep{Harper1991} for a published
2849 reference, although describing a more complex system allowing for both
2850 explicit and explicit hierarchy at the same time.
2852 We define a partial ordering on the levels, with both weak ($\le$) and
2853 strong ($<$) constraints---the laws governing them being the same as the
2854 ones governing $<$ and $\le$ for the natural numbers. Each occurrence
2855 of $\mytyp$ is decorated with a unique reference, and we keep a set of
2856 constraints and add new constraints as we type check, generating new
2857 references when needed.
2859 For example, when type checking the type $\mytyp\, r_1$, where $r_1$
2860 denotes the unique reference assigned to that term, we will generate a
2861 new fresh reference $\mytyp\, r_2$, and add the constraint $r_1 < r_2$
2862 to the set. When type checking $\myctx \vdash
2863 \myfora{\myb{x}}{\mytya}{\mytyb}$, if $\myctx \vdash \mytya : \mytyp\,
2864 r_1$ and $\myctx; \myb{x} : \mytyb \vdash \mytyb : \mytyp\,r_2$; we will
2865 generate new reference $r$ and add $r_1 \le r$ and $r_2 \le r$ to the
2868 If at any point the constraint set becomes inconsistent, type checking
2869 fails. Moreover, when comparing two $\mytyp$ terms we equate their
2870 respective references with two $\le$ constraints---the details are
2871 explained in Section \ref{sec:hier-impl}.
2873 Another more flexible but also more verbose alternative is the one
2874 chosen by Agda, where levels can be quantified so that the relationship
2875 between arguments and result in type formers can be explicitly
2878 \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}
2880 Inference algorithms to automatically derive this kind of relationship
2881 are currently subject of research. We chose less flexible but more
2882 concise way, since it is easier to implement and better understood.
2886 % \caption{Constraints generated by the typical ambiguity engine. We
2887 % assume some global set of constraints with the ability of generating
2888 % fresh references.}
2889 % \label{fig:hierarchy}
2892 \subsection{Observational equality, \mykant\ style}
2894 There are two correlated differences between $\mykant$\ and the theory
2895 used to present OTT. The first is that in $\mykant$ we have a type
2896 hierarchy, which lets us, for example, abstract over types. The second
2897 is that we let the user define inductive types.
2899 Reconciling propositions for OTT and a hierarchy had already been
2900 investigated by Conor McBride,\footnote{See
2901 \url{http://www.e-pig.org/epilogue/index.html?p=1098.html}.} and we
2902 follow his broad design plan, although with some modifications. Most of
2903 the work, as an extension of elaboration, is to handle reduction rules
2904 and coercions for data types---both type constructors and data
2907 \subsubsection{The \mykant\ prelude, and $\myprop$ositions}
2909 Before defining $\myprop$, we define some basic types inside $\mykant$,
2910 as the target for the $\myprop$ decoder:
2913 \myadt{\mytyc{Empty}}{}{ }{ } \\
2914 \myfun{absurd} : (\myb{A} {:} \mytyp) \myarr \mytyc{Empty} \myarr \myb{A} \mapsto \\
2915 \myind{2} \myabs{\myb{A\ \myb{bot}}}{\mytyc{Empty}.\myfun{elim} \myappsp \myb{bot} \myappsp (\myabs{\_}{\myb{A}})} \\
2918 \myreco{\mytyc{Unit}}{}{}{ } \\ \ \\
2920 \myreco{\mytyc{Prod}}{\myappsp (\myb{A}\ \myb{B} {:} \mytyp)}{ }{\myfun{fst} : \myb{A}, \myfun{snd} : \myb{B} }
2923 When using $\mytyc{Prod}$, we shall use $\myprod$ to define `nested'
2924 products, and $\myproj{n}$ to project elements from them, so that
2927 \mytya \myprod \mytyb = \mytyc{Prod} \myappsp \mytya \myappsp (\mytyc{Prod} \myappsp \mytyb \myappsp \myunit) \\
2928 \mytya \myprod \mytyb \myprod \myse{C} = \mytyc{Prod} \myappsp \mytya \myappsp (\mytyc{Prod} \myappsp \mytyb \myappsp (\mytyc{Prod} \myappsp \mytyc \myappsp \myunit)) \\
2930 \myproj{1} : \mytyc{Prod} \myappsp \mytya \myappsp \mytyb \myarr \mytya \\
2931 \myproj{2} : \mytyc{Prod} \myappsp \mytya \myappsp (\mytyc{Prod} \myappsp \mytyb \myappsp \myse{C}) \myarr \mytyb \\
2935 And so on, so that $\myproj{n}$ will work with all products with at
2936 least than $n$ elements. Then we can define propositions, and decoding:
2940 \begin{array}{r@{\ }c@{\ }l}
2941 \mytmsyn & ::= & \cdots \mysynsep \myprdec{\myprsyn} \\
2942 \myprsyn & ::= & \mybot \mysynsep \mytop \mysynsep \myprsyn \myand \myprsyn \mysynsep \myprfora{\myb{x}}{\mytmsyn}{\myprsyn}
2947 \mydesc{proposition decoding:}{\myprdec{\mytmsyn} \myred \mytmsyn}{
2950 \begin{array}{l@{\ }c@{\ }l}
2951 \myprdec{\mybot} & \myred & \myempty \\
2952 \myprdec{\mytop} & \myred & \myunit
2957 \begin{array}{r@{ }c@{ }l@{\ }c@{\ }l}
2958 \myprdec{&\myse{P} \myand \myse{Q} &} & \myred & \myprdec{\myse{P}} \myprod \myprdec{\myse{Q}} \\
2959 \myprdec{&\myprfora{\myb{x}}{\mytya}{\myse{P}} &} & \myred &
2960 \myfora{\myb{x}}{\mytya}{\myprdec{\myse{P}}}
2966 Adopting the same convention as with $\mytyp$-level products, we will
2967 nest $\myand$ in the same way.
2969 \subsubsection{Some OTT examples}
2971 Before presenting the direction that $\mykant$\ takes, let's consider
2972 some examples of use-defined data types, and the result we would expect,
2973 given what we already know about OTT, assuming the same propositional
2978 \item[Product types] Let's consider first the already mentioned
2979 dependent product, using the alternate name $\mysigma$\footnote{For
2980 extra confusion, `dependent products' are often called `dependent
2981 sums' in the literature, referring to the interpretation that
2982 identifies the first element as a `tag' deciding the type of the
2983 second element, which lets us recover sum types (disjuctions), as we
2984 saw in Section \ref{sec:user-type}. Thus, $\mysigma$.} to
2985 avoid confusion with the $\mytyc{Prod}$ in the prelude:
2988 \myreco{\mysigma}{\myappsp (\myb{A} {:} \mytyp) \myappsp (\myb{B} {:} \myb{A} \myarr \mytyp)}{\\ \myind{2}}{\myfst : \myb{A}, \mysnd : \myapp{\myb{B}}{\myb{fst}}}
2991 Let's start with type-level equality. The result we want is
2994 \mysigma \myappsp \mytya_1 \myappsp \mytyb_1 \myeq \mysigma \myappsp \mytya_2 \myappsp \mytyb_2 \myred \\
2995 \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}}}
2998 The difference here is that in the original presentation of OTT
2999 the type binders are explicit, while here $\mytyb_1$ and $\mytyb_2$
3000 functions returning types. We can do this thanks to the type
3001 hierarchy, and this hints at the fact that heterogeneous equality will
3002 have to allow $\mytyp$ `to the right of the colon', and in fact this
3003 provides the solution to simplify the equality above.
3005 If we take, just like we saw previously in OTT
3008 \myjm{\myse{f}_1}{\myfora{\mytya_1}{\myb{x_1}}{\mytyb_1}}{\myse{f}_2}{\myfora{\mytya_2}{\myb{x_2}}{\mytyb_2}} \myred \\
3009 \myind{2} \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{
3010 \myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2} \myimpl
3011 \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}]}
3015 Then we can simply take
3018 \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}
3021 Which will reduce to precisely what we desire. For what
3022 concerns coercions and quotation, things stay the same (apart from the
3023 fact that we apply to the second argument instead of substituting).
3024 We can recognise records such as $\mysigma$ as such and employ
3025 projections in value equality and coercions; as to not
3026 impede progress if not necessary.
3028 \item[Lists] Now for finite lists, which will give us a taste for data
3032 \myadt{\mylist}{\myappsp (\myb{A} {:} \mytyp)}{ }{\mydc{nil} \mydcsep \mydc{cons} \myappsp \myb{A} \myappsp (\myapp{\mylist}{\myb{A}})}
3035 Type equality is simple---we only need to compare the parameter:
3037 \mylist \myappsp \mytya_1 \myeq \mylist \myappsp \mytya_2 \myred \mytya_1 \myeq \mytya_2
3039 For coercions, we transport based on the constructor, recycling the
3040 proof for the inductive occurrence:
3042 \begin{array}{@{}l@{\ }c@{\ }l}
3043 \mycoe \myappsp (\mylist \myappsp \mytya_1) \myappsp (\mylist \myappsp \mytya_2) \myappsp \myse{Q} \myappsp \mydc{nil} & \myred & \mydc{nil} \\
3044 \mycoe \myappsp (\mylist \myappsp \mytya_1) \myappsp (\mylist \myappsp \mytya_2) \myappsp \myse{Q} \myappsp (\mydc{cons} \myappsp \mytmm \myappsp \mytmn) & \myred & \\
3045 \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)}
3048 Value equality is unsurprising---we match the constructors, and
3049 return bottom for mismatches. However, we also need to equate the
3050 parameter in $\mydc{nil}$:
3052 \begin{array}{r@{ }c@{\ }c@{\ }c@{}l@{\ }c@{\ }r@{}c@{\ }c@{\ }c@{}l@{\ }l}
3053 (& \mydc{nil} & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{nil} & : & \myapp{\mylist}{\mytya_2} &) \myred \mytya_1 \myeq \mytya_2 \\
3054 (& \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 \\
3055 & \multicolumn{11}{@{}l}{ \myind{2}
3056 \myjm{\mytmm_1}{\mytya_1}{\mytmm_2}{\mytya_2} \myand \myjm{\mytmn_1}{\myapp{\mylist}{\mytya_1}}{\mytmn_2}{\myapp{\mylist}{\mytya_2}}
3058 (& \mydc{nil} & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{cons} \myappsp \mytmm_2 \myappsp \mytmn_2 & : & \myapp{\mylist}{\mytya_2} &) \myred \mybot \\
3059 (& \mydc{cons} \myappsp \mytmm_1 \myappsp \mytmn_1 & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{nil} & : & \myapp{\mylist}{\mytya_2} &) \myred \mybot
3065 Now for something useless but complicated.
3069 \subsubsection{Only one equality}
3071 Given the examples above, a more `flexible' heterogeneous emerged, since
3072 of the fact that in $\mykant$ we re-gain the possibility of abstracting
3073 and in general handling sets in a way that was not possible in the
3074 original OTT presentation. Moreover, we found that the rules for value
3075 equality work very well if used with user defined type
3076 abstractions---for example in the case of dependent products we recover
3077 the original definition with explicit binders, in a very simple manner.
3079 In fact, we can drop a separate notion of type-equality, which will
3080 simply be served by $\myjm{\mytya}{\mytyp}{\mytyb}{\mytyp}$, from now on
3081 abbreviated as $\mytya \myeq \mytyb$. We shall still distinguish
3082 equalities relating types for hierarchical purposes. The full rules for
3083 equality reductions, along with the syntax for propositions, are given
3084 in figure \ref{fig:kant-eq-red}. We exploit record to perform
3085 $\eta$-expansion. Moreover, given the nested $\myand$s, values of data
3086 types with zero constructors (such as $\myempty$) and records with zero
3087 destructors (such as $\myunit$) will be automatically always identified
3094 \begin{array}{r@{\ }c@{\ }l}
3095 \myprsyn & ::= & \cdots \mysynsep \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
3100 % \mytmsyn & ::= & \cdots \mysynsep \mycoee{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \mysynsep
3101 % \mycohh{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
3102 % \myprsyn & ::= & \cdots \mysynsep \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
3106 % \mydesc{typing:}{\myctx \vdash \mytmsyn \Leftrightarrow \mytmsyn}{
3108 % \begin{tabular}{cc}
3109 % \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
3110 % \AxiomC{$\myjud{\mytmt}{\mytya}$}
3111 % \BinaryInfC{$\myinf{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}$}
3114 % \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
3115 % \AxiomC{$\myjud{\mytmt}{\mytya}$}
3116 % \BinaryInfC{$\myinf{\mycohh{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\myprdec{\myjm{\mytmt}{\mytya}{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}}}$}
3123 \mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
3126 \AxiomC{\phantom{$\myjud{\myse{P}}{\myprop}$}}
3127 \UnaryInfC{$\myjud{\mytop}{\myprop}$}
3129 \UnaryInfC{$\myjud{\mybot}{\myprop}$}
3132 \AxiomC{$\myjud{\myse{P}}{\myprop}$}
3133 \AxiomC{$\myjud{\myse{Q}}{\myprop}$}
3134 \BinaryInfC{$\myjud{\myse{P} \myand \myse{Q}}{\myprop}$}
3136 \UnaryInfC{\phantom{$\myjud{\mybot}{\myprop}$}}
3145 \phantom{\myjud{\myse{A}}{\mytyp} \hspace{0.8cm} \myjud{\mytmm}{\myse{A}}} \\
3146 \myjud{\myse{A}}{\mytyp}\hspace{0.8cm}
3147 \myjudd{\myctx; \myb{x} : \mytya}{\myse{P}}{\myprop}
3150 \UnaryInfC{$\myjud{\myprfora{\myb{x}}{\mytya}{\myse{P}}}{\myprop}$}
3155 \myjud{\myse{A}}{\mytyp} \hspace{0.8cm} \myjud{\mytmm}{\myse{A}} \\
3156 \myjud{\myse{B}}{\mytyp} \hspace{0.8cm} \myjud{\mytmn}{\myse{B}}
3159 \UnaryInfC{$\myjud{\myjm{\mytmm}{\myse{A}}{\mytmn}{\myse{B}}}{\myprop}$}
3165 % TODO equality for decodings
3166 \mydesc{equality reduction:}{\myctx \vdash \myprsyn \myred \myprsyn}{
3170 \UnaryInfC{$\myctx \vdash \myjm{\mytyp}{\mytyp}{\mytyp}{\mytyp} \myred \mytop$}
3174 \UnaryInfC{$\myctx \vdash \myjm{\myprdec{\myse{P}}}{\mytyp}{\myprdec{\myse{Q}}}{\mytyp} \myred \mytop$}
3182 \begin{array}{@{}r@{\ }l}
3184 \myjm{\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}}{\mytyp}{\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}}{\mytyp} \myred \\
3185 & \myind{2} \mytya_2 \myeq \mytya_1 \myand \myprfora{\myb{x_2}}{\mytya_2}{\myprfora{\myb{x_1}}{\mytya_1}{
3186 \myjm{\myb{x_2}}{\mytya_2}{\myb{x_1}}{\mytya_1} \myimpl \mytyb_1[\myb{x_1}] \myeq \mytyb_2[\myb{x_2}]
3196 \begin{array}{@{}r@{\ }l}
3198 \myjm{\myse{f}_1}{\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}}{\myse{f}_2}{\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}} \myred \\
3199 & \myind{2} \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{
3200 \myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2} \myimpl
3201 \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}]}
3210 \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
3212 \begin{array}{r@{\ }l}
3214 \myjm{\mytyc{D} \myappsp \vec{A}}{\mytyp}{\mytyc{D} \myappsp \vec{B}}{\mytyp} \myred \\
3215 & \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}))})
3224 \mydataty(\mytyc{D}, \myctx)\hspace{0.8cm}
3225 \mytyc{D}.\mydc{c} : \mytele;\mytele' \myarr \mytyc{D} \myappsp \mytelee \in \myctx \hspace{0.8cm}
3226 \mytele_A = (\mytele;\mytele')\vec{A}\hspace{0.8cm}
3227 \mytele_B = (\mytele;\mytele')\vec{B}
3231 \begin{array}{@{}l@{\ }l}
3232 \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 \\
3233 & \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}))})
3240 \AxiomC{$\mydataty(\mytyc{D}, \myctx)$}
3242 \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
3250 \myisreco(\mytyc{D}, \myctx)\hspace{0.8cm}
3251 \mytyc{D}.\myfun{f}_i : \mytele; (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr \myse{F}_i \in \myctx\\
3255 \begin{array}{@{}l@{\ }l}
3256 \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})})
3263 \UnaryInfC{$\myjm{\mytmm}{\mytya}{\mytmn}{\mytyb} \myred \mybot\ \text{if $\mytya$ and $\mytyb$ are canonical types.}$}
3266 \caption{Propositions and equality reduction in $\mykant$. We assume
3267 the presence of $\mydataty$ and $\myisreco$ as operations on the
3268 context to recognise whether a user defined type is a data type or a
3270 \label{fig:kant-eq-red}
3273 \subsubsection{Coercions}
3276 % \mydesc{reduction}{\mytmsyn \myred \mytmsyn}{
3279 % \caption{Coercions in \mykant.}
3280 % \label{fig:kant-coe}
3285 \subsubsection{$\myprop$ and the hierarchy}
3287 Where is $\myprop$ placed in the type hierarchy? The main indicator
3288 is the decoding operator, since it converts into things that already
3289 live in the hierarchy. For example, if we
3292 \myprdec{\mynat \myarr \mybool \myeq \mynat \myarr \mybool} \myred
3293 \mytop \myand ((\myb{x}\, \myb{y} : \mynat) \myarr \mytop \myarr \mytop)
3295 we will better make sure that the `to be decoded' is at the same
3296 level as its reduction as to preserve subject reduction. In the example
3297 above, we'll have that proposition to be at least as large as the type
3298 of $\mynat$, since the reduced proof will abstract over it. Pretending
3299 that we had explicit, non cumulative levels, it would be tempting to have
3302 \AxiomC{$\myjud{\myse{Q}}{\myprop_l}$}
3303 \UnaryInfC{$\myjud{\myprdec{\myse{Q}}}{\mytyp_l}$}
3306 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
3307 \AxiomC{$\myjud{\mytyb}{\mytyp_l}$}
3308 \BinaryInfC{$\myjud{\myjm{\mytya}{\mytyp_{l}}{\mytyb}{\mytyp_{l}}}{\myprop_l}$}
3312 $\mybot$ and $\mytop$ living at any level, $\myand$ and $\forall$
3313 following rules similar to the ones for $\myprod$ and $\myarr$ in
3314 Section \ref{sec:itt}. However, we need to be careful with value
3315 equality since for example we have that
3317 \myprdec{\myjm{\myse{f}_1}{\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}}{\myse{f}_2}{\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}}}
3319 \myfora{\myb{x_1}}{\mytya_1}{\myfora{\myb{x_2}}{\mytya_2}{\cdots}}
3321 where the proposition decodes into something of type $\mytyp_l$, where
3322 $\mytya : \mytyp_l$ and $\mytyb : \mytyp_l$. We can resolve this
3323 tension by making all equalities larger:
3325 \AxiomC{$\myjud{\mytmm}{\mytya}$}
3326 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
3327 \AxiomC{$\myjud{\mytmn}{\mytyb}$}
3328 \AxiomC{$\myjud{\mytyb}{\mytyp_l}$}
3329 \QuaternaryInfC{$\myjud{\myjm{\mytmm}{\mytya}{\mytmm}{\mytya}}{\myprop_l}$}
3331 This is disappointing, since type equalities will be needlessly large:
3332 $\myprdec{\myjm{\mytya}{\mytyp_l}{\mytyb}{\mytyp_l}} : \mytyp_{l + 1}$.
3334 However, considering that our theory is cumulative, we can do better.
3335 Assuming rules for $\myprop$ cumulativity similar to the ones for
3336 $\mytyp$, we will have (with the conversion rule reproduced as a
3340 \AxiomC{$\myctx \vdash \mytya \mycumul \mytyb$}
3341 \AxiomC{$\myjud{\mytmt}{\mytya}$}
3342 \BinaryInfC{$\myjud{\mytmt}{\mytyb}$}
3345 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
3346 \AxiomC{$\myjud{\mytyb}{\mytyp_l}$}
3347 \BinaryInfC{$\myjud{\myjm{\mytya}{\mytyp_{l}}{\mytyb}{\mytyp_{l}}}{\myprop_l}$}
3353 \AxiomC{$\myjud{\mytmm}{\mytya}$}
3354 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
3355 \AxiomC{$\myjud{\mytmn}{\mytyb}$}
3356 \AxiomC{$\myjud{\mytyb}{\mytyp_l}$}
3357 \AxiomC{$\mytya$ and $\mytyb$ are not $\mytyp_{l'}$}
3358 \QuinaryInfC{$\myjud{\myjm{\mytmm}{\mytya}{\mytmm}{\mytya}}{\myprop_l}$}
3362 That is, we are small when we can (type equalities) and large otherwise.
3363 This would not work in a non-cumulative theory because subject reduction
3364 would not hold. Consider for instance
3366 \myjm{\mynat}{\myITE{\mytrue}{\mytyp_0}{\mytyp_0}}{\mybool}{\myITE{\mytrue}{\mytyp_0}{\mytyp_0}}
3370 \[\myjm{\mynat}{\mytyp_0}{\mybool}{\mytyp_0} : \myprop_0 \]
3371 We need $\myprop_0$ to be $\myprop_1$ too, which will be the case with
3372 cumulativity. This is not the most elegant of systems, but it buys us a
3373 cheap type level equality without having to replicate functionality with
3374 a dedicated construct.
3376 \subsubsection{Quotation and definitional equality}
3377 \label{sec:kant-irr}
3379 Now we can give an account of definitional equality, by explaining how
3380 to perform quotation (as defined in Section \ref{sec:eta-expand})
3381 towards the goal described in Section \ref{sec:ott-quot}.
3385 \item Perform $\eta$-expansion on functions and records.
3387 \item As a consequence of the previous point, identify all records with
3388 no projections as equal, since they will have only one element.
3390 \item Identify all members of types with no elements as equal.
3392 \item Identify all equivalent proofs as equal---with `equivalent proof'
3393 we mean those proving the same propositions.
3395 \item Advance coercions working across definitionally equal types.
3397 Towards these goals and following the intuition between bidirectional
3398 type checking we define two mutually recursive functions, one quoting
3399 canonical terms against their types (since we need the type to typecheck
3400 canonical terms), one quoting neutral terms while recovering their
3403 Our quotation will work on normalised terms, so that all defined values
3404 will have been replaced. Moreover, we match on datatype eliminators and
3405 all their arguments, so that $\mynat.\myfun{elim} \myappsp \vec{\mytmt}$
3406 will stand for $\mynat.\myfun{elim}$ applied to the scrutinised
3407 $\mynat$, plus its three arguments. This measure can be easily
3408 implemented by checking the head of applications and `consuming' the
3413 \mydesc{canonical quotation}{\myctx \vdash \mytmsyn \myquot \mytmsyn \mapsto \mytmsyn}{
3419 \mydesc{neutral quotation}{\myctx \vdash \mynquot \mytmsyn \mapsto \mytmsyn : \mytmsyn}{
3422 \caption{Quotation in \mykant.}
3423 \label{fig:kant-quot}
3428 \subsubsection{Why $\myprop$?}
3430 It is worth to ask if $\myprop$ is needed at all. It is perfectly
3431 possible to have the type checker identify propositional types
3432 automatically, and in fact in some sense we already do during equality
3433 reduction and quotation. However, this has the considerable
3434 disadvantage that we can never identify abstracted
3435 variables\footnote{And in general neutral terms, although we currently
3436 don't have neutral propositions.} of type $\mytyp$ as $\myprop$, thus
3437 forbidding the user to talk about $\myprop$ explicitly.
3439 This is a considerable impediment, for example when implementing
3440 \emph{quotient types}. With quotients, we let the user specify an
3441 equivalence class over a certain type, and then exploit this in various
3442 way---crucially, we need to be sure that the equivalence given is
3443 propositional, a fact which prevented the use of quotients in dependent
3444 type theories \citep{Jacobs1994}.
3448 \section{\mykant : The practice}
3449 \label{sec:kant-practice}
3451 The codebase consists of around 2500 lines of Haskell, as reported by
3452 the \texttt{cloc} utility. The high level design is inspired by the
3453 work on various incarnations of Epigram, and specifically by the first
3454 version as described \citep{McBride2004} and the codebase for the new
3455 version.\footnote{Available intermittently as a \texttt{darcs}
3456 repository at \url{http://sneezy.cs.nott.ac.uk/darcs/Pig09}.} In many
3457 ways \mykant\ is something in between the first and second version of
3460 The author learnt the hard way the implementations challenges for such a
3461 project, and while there is a solid and working base to work on, the
3462 implementation of observational equality is not currently complete.
3463 However, given the detailed plan in the previous section, doing so
3464 should not prove to be too much work.
3466 The interaction happens in a read-eval-print loop (REPL). The REPL is a
3467 available both as a commandline application and in a web interface,
3468 which is available at \url{kant.mazzo.li} and presents itself as in
3469 figure \ref{fig:kant-web}.
3472 {\small\begin{verbatim}B E R T U S
3473 Version 0.0, made in London, year 2013.
3475 <decl> Declare value/data type/record
3478 :p <term> Pretty print
3480 :r <file> Reload file (erases previous environment)
3481 :i <name> Info about an identifier
3483 >>> :l data/samples/good/common.ka
3485 >>> :e plus three two
3486 suc (suc (suc (suc (suc zero))))
3487 >>> :t plus three two
3488 Type: Nat\end{verbatim}
3491 \caption{A sample run of the \mykant\ prompt.}
3492 \label{fig:kant-web}
3495 The interaction with the user takes place in a loop living in and updating a
3496 context \mykant\ declarations. The user inputs a new declaration that goes
3497 through various stages starts with the user inputing a \mykant\ declaration or
3498 another REPL command, which then goes through various stages that can end up
3499 in a context update, or in failures of various kind. The process is described
3500 diagrammatically in figure \ref{fig:kant-process}:
3503 \item[Parse] In this phase the text input gets converted to a sugared
3504 version of the core language.
3506 \item[Desugar] The sugared declaration is converted to a core term.
3508 \item[Reference] Occurrences of $\mytyp$ get decorated by a unique reference,
3509 which is necessary to implement the type hierarchy check.
3511 \item[Elaborate] Converts the declaration to some context items, which
3512 might be a value declaration (type and body) or a data type
3513 declaration (constructors and destructors). This phase works in
3514 tandem with \textbf{Type checking}, which in turns needs to
3515 \textbf{Evaluate} terms.
3517 \item[Distill] and report the result. `Distilling' refers to the process of
3518 converting a core term back to a sugared version that the user can
3519 visualise. This can be necessary both to display errors including terms or
3520 to display result of evaluations or type checking that the user has
3523 \item[Pretty print] Format the terms in a nice way, and display the result to
3530 \tikzstyle{block} = [rectangle, draw, text width=5em, text centered, rounded
3531 corners, minimum height=2.5em, node distance=0.7cm]
3533 \tikzstyle{decision} = [diamond, draw, text width=4.5em, text badly
3534 centered, inner sep=0pt, node distance=0.7cm]
3536 \tikzstyle{line} = [draw, -latex']
3538 \tikzstyle{cloud} = [draw, ellipse, minimum height=2em, text width=5em, text
3539 centered, node distance=1.5cm]
3542 \begin{tikzpicture}[auto]
3543 \node [cloud] (user) {User};
3544 \node [block, below left=1cm and 0.1cm of user] (parse) {Parse};
3545 \node [block, below=of parse] (desugar) {Desugar};
3546 \node [block, below=of desugar] (reference) {Reference};
3547 \node [block, below=of reference] (elaborate) {Elaborate};
3548 \node [block, left=of elaborate] (tycheck) {Typecheck};
3549 \node [block, left=of tycheck] (evaluate) {Evaluate};
3550 \node [decision, right=of elaborate] (error) {Error?};
3551 \node [block, right=of parse] (distill) {Distill};
3552 \node [block, right=of desugar] (update) {Update context};
3554 \path [line] (user) -- (parse);
3555 \path [line] (parse) -- (desugar);
3556 \path [line] (desugar) -- (reference);
3557 \path [line] (reference) -- (elaborate);
3558 \path [line] (elaborate) edge[bend right] (tycheck);
3559 \path [line] (tycheck) edge[bend right] (elaborate);
3560 \path [line] (elaborate) -- (error);
3561 \path [line] (error) edge[out=0,in=0] node [near start] {yes} (distill);
3562 \path [line] (error) -- node [near start] {no} (update);
3563 \path [line] (update) -- (distill);
3564 \path [line] (distill) -- (user);
3565 \path [line] (tycheck) edge[bend right] (evaluate);
3566 \path [line] (evaluate) edge[bend right] (tycheck);
3569 \caption{High level overview of the life of a \mykant\ prompt cycle.}
3570 \label{fig:kant-process}
3573 Here we will review only a sampling of the more interesting
3574 implementation challenges present when implementing an interactive
3577 \subsection{Term and context representation}
3578 \label{sec:term-repr}
3580 \subsubsection{Naming and substituting}
3582 Perhaps surprisingly, one of the most fundamental challenges in
3583 implementing a theory of the kind presented is choosing a good data type
3584 for terms, and specifically handling substitutions in a sane way.
3586 There are two broad schools of thought when it comes to naming
3587 variables, and thus substituting:
3589 \item[Nameful] Bound variables are represented by some enumerable data
3590 type, just as we have described up to now, starting from Section
3591 \ref{sec:untyped}. The problem is that avoiding name capturing is a
3592 nightmare, both in the sense that it is not performant---given that we
3593 need to rename rename substitute each time we `enter' a binder---but
3594 most importantly given the fact that in even more slightly complicated
3595 systems it is very hard to get right, even for experts.
3597 One of the sore spots of explicit names is comparing terms up
3598 $\alpha$-renaming, which again generates a huge amounts of
3599 substitutions and requires special care. We can represent the
3600 relationship between variables and their binders, by...
3602 \item[Nameless] ...getting rid of names altogether, and representing
3603 bound variables with an index referring to the `binding' structure, a
3604 notion introduced by \cite{de1972lambda}. Classically $0$ represents
3605 the variable bound by the innermost binding structure, $1$ the
3606 second-innermost, and so on. For instance with simple abstractions we
3608 \[\mymacol{red}{\lambda}\, (\mymacol{blue}{\lambda}\, \mymacol{blue}{0}\, (\mymacol{AgdaInductiveConstructor}{\lambda\, 0}))\, (\mymacol{AgdaFunction}{\lambda}\, \mymacol{red}{1}\, \mymacol{AgdaFunction}{0}) : ((\mytya \myarr \mytya) \myarr \mytyb) \myarr \mytyb \]
3610 While this technique is obviously terrible in terms of human
3611 usability,\footnote{With some people going as far as defining it akin
3612 to an inverse Turing test.} it is much more convenient as an
3613 internal representation to deal with terms mechanically---at least in
3614 simple cases. Moreover, $\alpha$ renaming ceases to be an issue, and
3615 term comparison is purely syntactical.
3617 Nonetheless, more complex, more complex constructs such as pattern
3618 matching put some strain on the indices and many systems end up using
3619 explicit names anyway (Agda, Coq, \dots).
3623 In the past decade or so advancements in the Haskell's type system and
3624 in general the spread new programming practices have enabled to make the
3625 second option much more amenable. \mykant\ thus takes the second path
3626 through the use of Edward Kmett's excellent \texttt{bound}
3627 library.\footnote{Available at
3628 \url{http://hackage.haskell.org/package/bound}.} We decribe its
3629 advantages but also pitfalls in the previously relatively unknown
3630 territory of dependent types---\texttt{bound} being created mostly to
3631 handle more simply typed systems.
3633 \texttt{bound} builds on two core ideas. The first is the suggestion by
3634 \cite{Bird1999} consists of parametrising the term type over the type of
3635 the variables, and `nest' the type each time we enter a scope. If we
3636 wanted to define a term for the untyped $\lambda$-calculus, we might
3641 data Var v = Bound | Free v
3644 = V v -- Bound variable
3645 | App (Tm v) (Tm v) -- Term application
3646 | Lam (Tm (Var v)) -- Abstraction
3648 Closed terms would be of type \texttt{Tm Void}, so that there would be
3649 no occurrences of \texttt{V}. However, inside an abstraction, we can
3650 have \texttt{V Bound}, representing the bound variable, and inside a
3651 second abstraction we can have \texttt{V Bound} or \texttt{V (Free
3652 Bound)}. Thus the term $\myabs{\myb{x}}{\myabs{\myb{y}}{\myb{x}}}$ could be represented as
3654 Lam (Lam (Free Bound))
3656 This allows us to reflect at the type level the `nestedness' of a type,
3657 and since we usually work with functions polymorphic on the parameter
3658 \texttt{v} it's very hard to make mistakes by putting terms of the wrong
3659 nestedness where they don't belong.
3661 Even more interestingly, the substitution operation is perfectly
3662 captured by the \verb|>>=| (bind) operator of the \texttt{Monad}
3667 (>>=) :: m a -> (a -> m b) -> m b
3669 instance Monad Tm where
3670 -- `return'ing turns a variable into a `Tm'
3673 -- `t >>= f' takes a term `t' and a mapping from variables to terms
3674 -- `f' and applies `f' to all the variables in `t', replacing them
3675 -- with the mapped terms.
3677 App m n >>= f = App (m >>= f) (n >>= f)
3679 -- `Lam' is the tricky case: we modify the function to work with bound
3680 -- variables, so that if it encounters `Bound' it leaves it untouched
3681 -- (since the mapping referred to the outer scope); if it encounters a
3682 -- free variable it asks `f' for the term and then updates all the
3683 -- variables to make them refer to the outer scope they were meant to
3685 Lam s >>= f = Lam (s >>= bump)
3686 where bump Bound = return Bound
3687 bump (Free v) = f v >>= V . Free
3689 With this in mind, we can define functions which will not only work on
3690 \verb|Tm|, but on any \verb|Monad|!
3692 -- Replaces free variable `v' with `m' in `n'.
3693 subst :: (Eq v, Monad m) => v -> m v -> m v -> m v
3694 subst v m n = n >>= \v' -> if v == v' then m else return v'
3696 -- Replace the variable bound by `s' with term `t'.
3697 inst :: Monad m => m v -> m (Var v) -> m v
3698 inst t s = do v <- s
3701 Free v' -> return v'
3703 The beauty of this technique is that in a few simple function we have
3704 defined all the core operations in a general and `obviously correct'
3705 way, with the extra confidence of having the type checker looking our
3708 Moreover, if we take the top level term type to be \verb|Tm String|, we
3709 get for free a representation of terms with top-level, definitions;
3710 where closed terms contain only \verb|String| references to said
3711 definitions---see also \cite{McBride2004b}.
3713 What are then the pitfalls of this seemingly invincible technique? The
3714 most obvious impediment is the need for polymorphic recursion.
3715 Functions traversing terms parametrised by the variable type will have
3718 -- Infer the type of a term, or return an error.
3719 infer :: Tm v -> Either Error (Tm v)
3721 When traversing under a \verb|Scope| the parameter changes from \verb|v|
3722 to \verb|Var v|, and thus if we do not specify the type for our function explicitly
3723 inference will fail---type inference for polymorphic recursion being
3724 undecidable \citep{henglein1993type}. This causes some annoyance,
3725 especially in the presence of many local definitions that we would like
3728 But the real issue is the fact that giving a type parametrised over a
3729 variable---say \verb|m v|---a \verb|Monad| instance means being able to
3730 only substitute variables for values of type \verb|m v|. This is a
3731 considerable inconvenience. Consider for instance the case of
3732 telescopes, which are a central tool to deal with contexts and other
3735 data Tele m v = End (m v) | Bind (m v) (Tele (Var v))
3736 type TeleTm = Tele Tm
3738 The problem here is that what we want to substitute for variables in
3739 \verb|Tele m v| is \verb|m v| (probably \verb|Tm v|), not \verb|Tele m v| itself! What we need is
3741 bindTele :: Monad m => Tele m a -> (a -> m b) -> Tele m b
3742 substTele :: (Eq v, Monad m) => v -> m v -> Tele m v -> Tele m v
3743 instTele :: Monad m => m v -> Tele m (Var v) -> Tele m v
3745 Not what \verb|Monad| gives us. Solving this issue in an elegant way
3746 has been a major sink of time and source of headaches for the author,
3747 who analysed some of the alternatives---most notably the work by
3748 \cite{weirich2011binders}---but found it impossible to give up the
3749 simplicity of the model above.
3751 That said, our term type is still reasonably brief, as shown in full in
3752 Figure \ref{fig:term}. The fact that propositions cannot be factored
3753 out in another data type is a consequence of the problems described
3754 above. However the real pain is during elaboration, where we are forced
3755 to treat everything as a type while we would much rather have
3756 telescopes. Future work would include writing a library that marries a
3757 nice interface similar to the one of \verb|bound| with a more flexible
3761 {\small\begin{verbatim}-- A top-level name.
3763 -- A data/type constructor name.
3766 -- A term, parametrised over the variable (`v') and over the reference
3767 -- type used in the type hierarchy (`r').
3770 | Ty r -- Type, with a hierarchy reference.
3771 | Lam (TmScope r v) -- Abstraction.
3772 | Arr (Tm r v) (TmScope r v) -- Dependent function.
3773 | App (Tm r v) (Tm r v) -- Application.
3774 | Ann (Tm r v) (Tm r v) -- Annotated term.
3775 -- Data constructor, the first ConId is the type constructor and
3776 -- the second is the data constructor.
3777 | Con ADTRec ConId ConId [Tm r v]
3778 -- Data destrutor, again first ConId being the type constructor
3779 -- and the second the name of the eliminator.
3780 | Destr ADTRec ConId Id (Tm r v)
3782 | Hole HoleId [Tm r v]
3783 -- Decoding of propositions.
3787 | Prop r -- The type of proofs, with hierarchy reference.
3790 | And (Tm r v) (Tm r v)
3791 | Forall (Tm r v) (TmScope r v)
3792 -- Heterogeneous equality.
3793 | Eq (Tm r v) (Tm r v) (Tm r v) (Tm r v)
3795 -- Either a data type, or a record.
3796 data ADTRec = ADT | Rec
3798 -- Either a coercion, or coherence.
3799 data Coeh = Coe | Coh\end{verbatim}
3801 \caption{Data type for terms in \mykant.}
3805 We also make use of a `forgetful' data type (as provided by
3806 \verb|bound|) to store user-provided variables names along with the
3807 `nameless' representation, so that the names will not be considered when
3808 compared terms, but will be available when distilling so that we can
3809 recover variable names that are as close as possible to what the user
3812 \subsubsection{Context}
3816 \subsection{Type hierarchy}
3817 \label{sec:hier-impl}
3819 As a breath of air amongst the type gas, we will explain how to
3820 implement the typical ambiguity we have spoken about in
3821 \ref{sec:term-hierarchy}. As mentioned, we have to verify a the
3822 consistency of a set of constraints each time we add a new one. The
3823 constraints range over some set of variables whose members we will
3824 denote with $x, y, z, \dots$. and are of two kinds:
3831 Predictably, $\le$ expresses a reflexive order, and $<$ expresses an
3832 irreflexive order, both working with the same notion of equality, where
3833 $x < y$ implies $x \le y$---they behave like $\le$ and $<$ do on natural
3834 numbers (or in our case, levels in a type hierarchy). We also need an
3835 equality constraint ($x = y$), which can be reduced to two constraints
3836 $x \le y$ and $y \le x$.
3838 Given this specification, we have implemented a standalone Haskell
3839 module---that we plan to release as a library---to efficiently store and
3840 check the consistency of constraints. Its interface is shown in Figure
3841 \ref{fig:constraint}. The problem unpredictably reduces to a graph
3845 {\small\begin{verbatim}module Data.Constraint where
3847 -- | Data type holding the set of constraints, parametrised over the
3848 -- type of the variables.
3851 -- | A representation of the constraints that we can add.
3852 data Constr a = a :<=: a | a :<: a | a :==: a
3854 -- | An empty set of constraints.
3855 empty :: Ord a => Constrs a
3857 -- | Adds one constraint to the set, returns the new set of constraints
3859 addConstr :: Ord a => Constr a -> Constrs a -> Maybe (Constrs a)\end{verbatim}
3862 \caption{Interface for the module handling the constraints.}
3863 \label{fig:constraint}
3867 \subsection{Type holes}
3869 When building up programs interactively, it is useful to leave parts
3870 unfinished while exploring the current context. This is what type holes
3873 \section{Evaluation}
3875 \section{Future work}
3877 \subsection{Coinduction}
3879 \subsection{Quotient types}
3881 \subsection{Partiality}
3883 \subsection{Pattern matching}
3885 \subsection{Pattern unification}
3887 % TODO coinduction (obscoin, gimenez, jacobs), pattern unification (miller,
3888 % gundry), partiality monad (NAD)
3892 \section{Notation and syntax}
3894 Syntax, derivation rules, and reduction rules, are enclosed in frames describing
3895 the type of relation being established and the syntactic elements appearing,
3898 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
3899 Typing derivations here.
3902 In the languages presented and Agda code samples I also highlight the syntax,
3903 following a uniform color and font convention:
3906 \begin{tabular}{c | l}
3907 $\mytyc{Sans}$ & Type constructors. \\
3908 $\mydc{sans}$ & Data constructors. \\
3909 % $\myfld{sans}$ & Field accessors (e.g. \myfld{fst} and \myfld{snd} for products). \\
3910 $\mysyn{roman}$ & Keywords of the language. \\
3911 $\myfun{roman}$ & Defined values and destructors. \\
3912 $\myb{math}$ & Bound variables.
3916 Moreover, I will from time to time give examples in the Haskell programming
3917 language as defined in \citep{Haskell2010}, which I will typeset in
3918 \texttt{teletype} font. I assume that the reader is already familiar with
3919 Haskell, plenty of good introductions are available \citep{LYAH,ProgInHask}.
3921 When presenting grammars, I will use a word in $\mysynel{math}$ font
3922 (e.g. $\mytmsyn$ or $\mytysyn$) to indicate indicate nonterminals. Additionally,
3923 I will use quite flexibly a $\mysynel{math}$ font to indicate a syntactic
3924 element. More specifically, terms are usually indicated by lowercase letters
3925 (often $\mytmt$, $\mytmm$, or $\mytmn$); and types by an uppercase letter (often
3926 $\mytya$, $\mytyb$, or $\mytycc$).
3928 When presenting type derivations, I will often abbreviate and present multiple
3929 conclusions, each on a separate line:
3931 \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
3932 \UnaryInfC{$\myjud{\myapp{\myfst}{\mytmt}}{\mytya}$}
3934 \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mytyb}$}
3937 I will often present `definitions' in the described calculi and in
3938 $\mykant$\ itself, like so:
3941 \myfun{name} : \mytysyn \\
3942 \myfun{name} \myappsp \myb{arg_1} \myappsp \myb{arg_2} \myappsp \cdots \mapsto \mytmsyn
3945 To define operators, I use a mixfix notation similar
3946 to Agda, where $\myarg$s denote arguments:
3949 \myarg \mathrel{\myfun{$\wedge$}} \myarg : \mybool \myarr \mybool \myarr \mybool \\
3950 \myb{b_1} \mathrel{\myfun{$\wedge$}} \myb{b_2} \mapsto \cdots
3954 In explicitly typed systems, I will also omit type annotations when they
3955 are obvious, e.g. by not annotating the type of parameters of
3956 abstractions or of dependent pairs.
3958 I will also introduce multiple arguments in one go in arrow types:
3960 (\myb{x}\, \myb{y} {:} \mytya) \myarr \cdots = (\myb{x} {:} \mytya) \myarr (\myb{y} {:} \mytya) \myarr \cdots
3962 and in abstractions:
3964 \myabs{\myb{x}\myappsp\myb{y}}{\cdots} = \myabs{\myb{x}}{\myabs{\myb{y}}{\cdots}}
3969 \subsection{ITT renditions}
3970 \label{app:itt-code}
3972 \subsubsection{Agda}
3973 \label{app:agda-itt}
3975 Note that in what follows rules for `base' types are
3976 universe-polymorphic, to reflect the exposition. Derived definitions,
3977 on the other hand, mostly work with \mytyc{Set}, reflecting the fact
3978 that in the theory presented we don't have universe polymorphism.
3984 data Empty : Set where
3986 absurd : ∀ {a} {A : Set a} → Empty → A
3989 ¬_ : ∀ {a} → (A : Set a) → Set a
3992 record Unit : Set where
3995 record _×_ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
4002 data Bool : Set where
4005 if_/_then_else_ : ∀ {a} (x : Bool) (P : Bool → Set a) → P true → P false → P x
4006 if true / _ then x else _ = x
4007 if false / _ then _ else x = x
4009 if_then_else_ : ∀ {a} (x : Bool) {P : Bool → Set a} → P true → P false → P x
4010 if_then_else_ x {P} = if_/_then_else_ x P
4012 data W {s p} (S : Set s) (P : S → Set p) : Set (s ⊔ p) where
4013 _◁_ : (s : S) → (P s → W S P) → W S P
4015 rec : ∀ {a b} {S : Set a} {P : S → Set b}
4016 (C : W S P → Set) → -- some conclusion we hope holds
4017 ((s : S) → -- given a shape...
4018 (f : P s → W S P) → -- ...and a bunch of kids...
4019 ((p : P s) → C (f p)) → -- ...and C for each kid in the bunch...
4020 C (s ◁ f)) → -- ...does C hold for the node?
4021 (x : W S P) → -- If so, ...
4022 C x -- ...C always holds.
4023 rec C c (s ◁ f) = c s f (λ p → rec C c (f p))
4025 module Examples-→ where
4032 -- These pragmas are needed so we can use number literals.
4033 {-# BUILTIN NATURAL ℕ #-}
4034 {-# BUILTIN ZERO zero #-}
4035 {-# BUILTIN SUC suc #-}
4037 data List (A : Set) : Set where
4039 _∷_ : A → List A → List A
4041 length : ∀ {A} → List A → ℕ
4043 length (_ ∷ l) = suc (length l)
4048 suc x > suc y = x > y
4050 head : ∀ {A} → (l : List A) → length l > 0 → A
4051 head [] p = absurd p
4054 module Examples-× where
4060 even (suc zero) = Empty
4061 even (suc (suc n)) = even n
4066 5-not-even : ¬ (even 5)
4069 there-is-an-even-number : ℕ × even
4070 there-is-an-even-number = 6 , 6-even
4072 _∨_ : (A B : Set) → Set
4073 A ∨ B = Bool × (λ b → if b then A else B)
4075 left : ∀ {A B} → A → A ∨ B
4078 right : ∀ {A B} → B → A ∨ B
4081 [_,_] : {A B C : Set} → (A → C) → (B → C) → A ∨ B → C
4083 (if (fst x) / (λ b → if b then _ else _ → _) then f else g) (snd x)
4085 module Examples-W where
4090 Tr b = if b then Unit else Empty
4096 zero = false ◁ absurd
4099 suc n = true ◁ (λ _ → n)
4105 if b / (λ b → (Tr b → ℕ) → (Tr b → ℕ) → ℕ)
4106 then (λ _ f → (suc (f tt))) else (λ _ _ → y))
4109 module Equality where
4112 data _≡_ {a} {A : Set a} : A → A → Set a where
4115 ≡-elim : ∀ {a b} {A : Set a}
4116 (P : (x y : A) → x ≡ y → Set b) →
4117 ∀ {x y} → P x x (refl x) → (x≡y : x ≡ y) → P x y x≡y
4118 ≡-elim P p (refl x) = p
4120 subst : ∀ {A : Set} (P : A → Set) → ∀ {x y} → (x≡y : x ≡ y) → P x → P y
4121 subst P x≡y p = ≡-elim (λ _ y _ → P y) p x≡y
4123 sym : ∀ {A : Set} (x y : A) → x ≡ y → y ≡ x
4124 sym x y p = subst (λ y′ → y′ ≡ x) p (refl x)
4126 trans : ∀ {A : Set} (x y z : A) → x ≡ y → y ≡ z → x ≡ z
4127 trans x y z p q = subst (λ z′ → x ≡ z′) q p
4129 cong : ∀ {A B : Set} (x y : A) → x ≡ y → (f : A → B) → f x ≡ f y
4130 cong x y p f = subst (λ z → f x ≡ f z) p (refl (f x))
4133 \subsubsection{\mykant}
4135 The following things are missing: $\mytyc{W}$-types, since our
4136 positivity check is overly strict, and equality, since we haven't
4137 implemented that yet.
4140 \verbatiminput{itt.ka}
4143 \subsection{\mykant\ examples}
4146 \verbatiminput{examples.ka}
4149 \subsection{\mykant's hierachy}
4152 This rendition of the Hurken's paradox does not type check with the
4153 hierachy enabled, type checks and loops without it. Adapted from an
4154 Agda version, available at
4155 \url{http://code.haskell.org/Agda/test/succeed/Hurkens.agda}.
4158 \verbatiminput{hurkens.ka}
4161 \bibliographystyle{authordate1}
4162 \bibliography{thesis}