1 \documentclass[report, 11pt]{article}
4 \usepackage[sc,slantedGreek]{mathpazo}
17 % \usepackage{fullpage}
29 \usepackage[fleqn]{amsmath}
30 \usepackage{stmaryrd} %llbracket
33 \usepackage{bussproofs}
45 \usepackage{subcaption}
51 \usetikzlibrary{shapes,arrows,positioning}
52 % \usepackage{tikz-cd}
53 % \usepackage{pgfplots}
56 %% -----------------------------------------------------------------------------
58 \usepackage[english]{babel}
59 \usepackage[conor]{agda}
60 \renewcommand{\AgdaKeywordFontStyle}[1]{\ensuremath{\mathrm{\underline{#1}}}}
61 \renewcommand{\AgdaFunction}[1]{\textbf{\textcolor{AgdaFunction}{#1}}}
62 \renewcommand{\AgdaField}{\AgdaFunction}
63 % \definecolor{AgdaBound} {HTML}{000000}
64 \definecolor{AgdaHole} {HTML} {FFFF33}
66 \DeclareUnicodeCharacter{9665}{\ensuremath{\lhd}}
67 \DeclareUnicodeCharacter{964}{\ensuremath{\tau}}
68 \DeclareUnicodeCharacter{963}{\ensuremath{\sigma}}
69 \DeclareUnicodeCharacter{915}{\ensuremath{\Gamma}}
70 \DeclareUnicodeCharacter{8799}{\ensuremath{\stackrel{?}{=}}}
71 \DeclareUnicodeCharacter{9655}{\ensuremath{\rhd}}
73 \renewenvironment{code}%
74 {\noindent\ignorespaces\advance\leftskip\mathindent\AgdaCodeStyle\pboxed\small}%
75 {\endpboxed\par\noindent%
76 \ignorespacesafterend\small}
79 %% -----------------------------------------------------------------------------
82 \newcommand{\mysyn}{\AgdaKeyword}
83 \newcommand{\mytyc}{\AgdaDatatype}
84 \newcommand{\mydc}{\AgdaInductiveConstructor}
85 \newcommand{\myfld}{\AgdaField}
86 \newcommand{\myfun}{\AgdaFunction}
87 \newcommand{\myb}[1]{\AgdaBound{$#1$}}
88 \newcommand{\myfield}{\AgdaField}
89 \newcommand{\myind}{\AgdaIndent}
90 \newcommand{\mykant}{\textsc{Kant}}
91 \newcommand{\mysynel}[1]{#1}
92 \newcommand{\myse}{\mysynel}
93 \newcommand{\mytmsyn}{\mysynel{term}}
94 \newcommand{\mysp}{\ }
95 \newcommand{\myabs}[2]{\mydc{$\lambda$} #1 \mathrel{\mydc{$\mapsto$}} #2}
96 \newcommand{\myappsp}{\hspace{0.07cm}}
97 \newcommand{\myapp}[2]{#1 \myappsp #2}
98 \newcommand{\mysynsep}{\ \ |\ \ }
99 \newcommand{\myITE}[3]{\myfun{If}\, #1\, \myfun{Then}\, #2\, \myfun{Else}\, #3}
102 \newcommand{\mydesc}[3]{
108 \hfill \textbf{#1} $#2$
109 \framebox[\textwidth]{
123 \newcommand{\mytmt}{\mysynel{t}}
124 \newcommand{\mytmm}{\mysynel{m}}
125 \newcommand{\mytmn}{\mysynel{n}}
126 \newcommand{\myred}{\leadsto}
127 \newcommand{\mysub}[3]{#1[#2 / #3]}
128 \newcommand{\mytysyn}{\mysynel{type}}
129 \newcommand{\mybasetys}{K}
130 \newcommand{\mybasety}[1]{B_{#1}}
131 \newcommand{\mytya}{\myse{A}}
132 \newcommand{\mytyb}{\myse{B}}
133 \newcommand{\mytycc}{\myse{C}}
134 \newcommand{\myarr}{\mathrel{\textcolor{AgdaDatatype}{\to}}}
135 \newcommand{\myprod}{\mathrel{\textcolor{AgdaDatatype}{\times}}}
136 \newcommand{\myctx}{\Gamma}
137 \newcommand{\myvalid}[1]{#1 \vdash \underline{\mathrm{valid}}}
138 \newcommand{\myjudd}[3]{#1 \vdash #2 : #3}
139 \newcommand{\myjud}[2]{\myjudd{\myctx}{#1}{#2}}
140 \newcommand{\myabss}[3]{\mydc{$\lambda$} #1 {:} #2 \mathrel{\mydc{$\mapsto$}} #3}
141 \newcommand{\mytt}{\mydc{$\langle\rangle$}}
142 \newcommand{\myunit}{\mytyc{Unit}}
143 \newcommand{\mypair}[2]{\mathopen{\mydc{$\langle$}}#1\mathpunct{\mydc{,}} #2\mathclose{\mydc{$\rangle$}}}
144 \newcommand{\myfst}{\myfld{fst}}
145 \newcommand{\mysnd}{\myfld{snd}}
146 \newcommand{\myconst}{\myse{c}}
147 \newcommand{\myemptyctx}{\cdot}
148 \newcommand{\myhole}{\AgdaHole}
149 \newcommand{\myfix}[3]{\mysyn{fix} \myappsp #1 {:} #2 \mapsto #3}
150 \newcommand{\mysum}{\mathbin{\textcolor{AgdaDatatype}{+}}}
151 \newcommand{\myleft}[1]{\mydc{left}_{#1}}
152 \newcommand{\myright}[1]{\mydc{right}_{#1}}
153 \newcommand{\myempty}{\mytyc{Empty}}
154 \newcommand{\mycase}[2]{\mathopen{\myfun{[}}#1\mathpunct{\myfun{,}} #2 \mathclose{\myfun{]}}}
155 \newcommand{\myabsurd}[1]{\myfun{absurd}_{#1}}
156 \newcommand{\myarg}{\_}
157 \newcommand{\myderivsp}{\vspace{0.3cm}}
158 \newcommand{\mytyp}{\mytyc{Type}}
159 \newcommand{\myneg}{\myfun{$\neg$}}
160 \newcommand{\myar}{\,}
161 \newcommand{\mybool}{\mytyc{Bool}}
162 \newcommand{\mytrue}{\mydc{true}}
163 \newcommand{\myfalse}{\mydc{false}}
164 \newcommand{\myitee}[5]{\myfun{if}\,#1 / {#2.#3}\,\myfun{then}\,#4\,\myfun{else}\,#5}
165 \newcommand{\mynat}{\mytyc{$\mathbb{N}$}}
166 \newcommand{\myrat}{\mytyc{$\mathbb{R}$}}
167 \newcommand{\myite}[3]{\myfun{if}\,#1\,\myfun{then}\,#2\,\myfun{else}\,#3}
168 \newcommand{\myfora}[3]{(#1 {:} #2) \myarr #3}
169 \newcommand{\myexi}[3]{(#1 {:} #2) \myprod #3}
170 \newcommand{\mypairr}[4]{\mathopen{\mydc{$\langle$}}#1\mathpunct{\mydc{,}} #4\mathclose{\mydc{$\rangle$}}_{#2{.}#3}}
171 \newcommand{\mylist}{\mytyc{List}}
172 \newcommand{\mynil}[1]{\mydc{[]}_{#1}}
173 \newcommand{\mycons}{\mathbin{\mydc{∷}}}
174 \newcommand{\myfoldr}{\myfun{foldr}}
175 \newcommand{\myw}[3]{\myapp{\myapp{\mytyc{W}}{(#1 {:} #2)}}{#3}}
176 \newcommand{\mynodee}{\mathbin{\mydc{$\lhd$}}}
177 \newcommand{\mynode}[2]{\mynodee_{#1.#2}}
178 \newcommand{\myrec}[4]{\myfun{rec}\,#1 / {#2.#3}\,\myfun{with}\,#4}
179 \newcommand{\mylub}{\sqcup}
180 \newcommand{\mydefeq}{\cong}
181 \newcommand{\myrefl}{\mydc{refl}}
182 \newcommand{\mypeq}[1]{\mathrel{\mytyc{=}_{#1}}}
183 \newcommand{\myjeqq}{\myfun{=-elim}}
184 \newcommand{\myjeq}[3]{\myapp{\myapp{\myapp{\myjeqq}{#1}}{#2}}{#3}}
185 \newcommand{\mysubst}{\myfun{subst}}
186 \newcommand{\myprsyn}{\myse{prop}}
187 \newcommand{\myprdec}[1]{\mathopen{\mytyc{$\llbracket$}} #1 \mathopen{\mytyc{$\rrbracket$}}}
188 \newcommand{\myand}{\mathrel{\mytyc{$\wedge$}}}
189 \newcommand{\mybigand}{\mathrel{\mytyc{$\bigwedge$}}}
190 \newcommand{\myprfora}[3]{\forall #1 {:} #2. #3}
191 \newcommand{\myimpl}{\mathrel{\mytyc{$\Rightarrow$}}}
192 \newcommand{\mybot}{\mytyc{$\bot$}}
193 \newcommand{\mytop}{\mytyc{$\top$}}
194 \newcommand{\mycoe}{\myfun{coe}}
195 \newcommand{\mycoee}[4]{\myapp{\myapp{\myapp{\myapp{\mycoe}{#1}}{#2}}{#3}}{#4}}
196 \newcommand{\mycoh}{\myfun{coh}}
197 \newcommand{\mycohh}[4]{\myapp{\myapp{\myapp{\myapp{\mycoh}{#1}}{#2}}{#3}}{#4}}
198 \newcommand{\myjm}[4]{(#1 {:} #2) \mathrel{\mytyc{=}} (#3 {:} #4)}
199 \newcommand{\myeq}{\mathrel{\mytyc{=}}}
200 \newcommand{\myprop}{\mytyc{Prop}}
201 \newcommand{\mytmup}{\mytmsyn\uparrow}
202 \newcommand{\mydefs}{\Delta}
203 \newcommand{\mynf}{\Downarrow}
204 \newcommand{\myinff}[3]{#1 \vdash #2 \Rightarrow #3}
205 \newcommand{\myinf}[2]{\myinff{\myctx}{#1}{#2}}
206 \newcommand{\mychkk}[3]{#1 \vdash #2 \Leftarrow #3}
207 \newcommand{\mychk}[2]{\mychkk{\myctx}{#1}{#2}}
208 \newcommand{\myann}[2]{#1 : #2}
209 \newcommand{\mydeclsyn}{\myse{decl}}
210 \newcommand{\myval}[3]{#1 : #2 \mapsto #3}
211 \newcommand{\mypost}[2]{\mysyn{abstract}\ #1 : #2}
212 \newcommand{\myadt}[4]{\mysyn{data}\ #1 #2\ \mysyn{where}\ #3\{ #4 \}}
213 \newcommand{\myreco}[4]{\mysyn{record}\ #1 #2\ \mysyn{where}\ \{ #4 \}}
214 \newcommand{\myelabt}{\vdash}
215 \newcommand{\myelabf}{\rhd}
216 \newcommand{\myelab}[2]{\myctx \myelabt #1 \myelabf #2}
217 \newcommand{\mytele}{\Delta}
218 \newcommand{\mytelee}{\delta}
219 \newcommand{\mydcctx}{\Gamma}
220 \newcommand{\mynamesyn}{\myse{name}}
221 \newcommand{\myvec}{\overrightarrow}
222 \newcommand{\mymeta}{\textsc}
223 \newcommand{\myhyps}{\mymeta{hyps}}
224 \newcommand{\mycc}{;}
225 \newcommand{\myemptytele}{\cdot}
226 \newcommand{\mymetagoes}{\Longrightarrow}
227 % \newcommand{\mytesctx}{\
228 \newcommand{\mytelesyn}{\myse{telescope}}
229 \newcommand{\myrecs}{\mymeta{recs}}
230 \newcommand{\myle}{\mathrel{\lcfun{$\le$}}}
231 \newcommand{\mylet}{\mysyn{let}}
232 \newcommand{\myhead}{\mymeta{head}}
233 \newcommand{\mytake}{\mymeta{take}}
234 \newcommand{\myix}{\mymeta{ix}}
235 \newcommand{\myapply}{\mymeta{apply}}
236 \newcommand{\mydataty}{\mymeta{datatype}}
237 \newcommand{\myisreco}{\mymeta{record}}
238 \newcommand{\mydcsep}{\ |\ }
239 \newcommand{\mytree}{\mytyc{Tree}}
240 \newcommand{\myproj}[1]{\myfun{$\pi_{#1}$}}
241 \newcommand{\mysigma}{\mytyc{$\Sigma$}}
244 %% -----------------------------------------------------------------------------
246 \title{\mykant: Implementing Observational Equality}
247 \author{Francesco Mazzoli \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{<fm2209@ic.ac.uk>}}}
262 \thispagestyle{empty}
264 \begin{minipage}{0.4\textwidth}
265 \begin{flushleft} \large
267 Dr. Steffen \textsc{van Backel}
270 \begin{minipage}{0.4\textwidth}
271 \begin{flushright} \large
273 Dr. Philippa \textsc{Gardner}
280 The marriage between programming and logic has been a very fertile one. In
281 particular, since the simply typed lambda calculus (STLC), a number of type
282 systems have been devised with increasing expressive power.
284 Among this systems, Inutitionistic Type Theory (ITT) has been a very
285 popular framework for theorem provers and programming languages.
286 However, equality has always been a tricky business in ITT and related
289 In these thesis we will explain why this is the case, and present
290 Observational Type Theory (OTT), a solution to some of the problems
291 with equality. We then describe $\mykant$, a theorem prover featuring
292 OTT in a setting more close to the one found in current systems.
293 Having implemented part of $\mykant$ as a Haskell program, we describe
294 some of the implementation issues faced.
299 \renewcommand{\abstractname}{Acknowledgements}
301 I would like to thank Steffen van Backel, my supervisor, who was brave
302 enough to believe in my project and who provided much advice and
305 I would also like to thank the Haskell and Agda community on
306 \texttt{IRC}, which guided me through the strange world of types; and
307 in particular Andrea Vezzosi and James Deikun, with whom I entertained
308 countless insightful discussions in the past year. Andrea suggested
309 Observational Type Theory as a topic of study: this thesis would not
310 exist without him. Before them, Tony Fields introduced me to Haskell,
311 unknowingly filling most of my free time from that time on.
313 Finally, much of the work stems from the research of Conor McBride,
314 who answered many of my doubts through these months. I also owe him
324 \section{Simple and not-so-simple types}
327 \subsection{The untyped $\lambda$-calculus}
329 Along with Turing's machines, the earliest attempts to formalise computation
330 lead to the $\lambda$-calculus \citep{Church1936}. This early programming
331 language encodes computation with a minimal syntax and no `data' in the
332 traditional sense, but just functions. Here we give a brief overview of the
333 language, which will give the chance to introduce concepts central to the
334 analysis of all the following calculi. The exposition follows the one found in
335 chapter 5 of \cite{Queinnec2003}.
337 The syntax of $\lambda$-terms consists of three things: variables, abstractions,
342 \begin{array}{r@{\ }c@{\ }l}
343 \mytmsyn & ::= & \myb{x} \mysynsep \myabs{\myb{x}}{\mytmsyn} \mysynsep (\myapp{\mytmsyn}{\mytmsyn}) \\
344 x & \in & \text{Some enumerable set of symbols}
349 Parenthesis will be omitted in the usual way:
350 $\myapp{\myapp{\mytmt}{\mytmm}}{\mytmn} =
351 \myapp{(\myapp{\mytmt}{\mytmm})}{\mytmn}$.
353 Abstractions roughly corresponds to functions, and their semantics is more
354 formally explained by the $\beta$-reduction rule:
356 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
359 \myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{\myb{x}}{\mytmn}\text{, where} \\
361 \begin{array}{l@{\ }c@{\ }l}
362 \mysub{\myb{x}}{\myb{x}}{\mytmn} & = & \mytmn \\
363 \mysub{\myb{y}}{\myb{x}}{\mytmn} & = & y\text{, with } \myb{x} \neq y \\
364 \mysub{(\myapp{\mytmt}{\mytmm})}{\myb{x}}{\mytmn} & = & (\myapp{\mysub{\mytmt}{\myb{x}}{\mytmn}}{\mysub{\mytmm}{\myb{x}}{\mytmn}}) \\
365 \mysub{(\myabs{\myb{x}}{\mytmm})}{\myb{x}}{\mytmn} & = & \myabs{\myb{x}}{\mytmm} \\
366 \mysub{(\myabs{\myb{y}}{\mytmm})}{\myb{x}}{\mytmn} & = & \myabs{\myb{z}}{\mysub{\mysub{\mytmm}{\myb{y}}{\myb{z}}}{\myb{x}}{\mytmn}}, \\
367 \multicolumn{3}{l}{\myind{2} \text{with $\myb{x} \neq \myb{y}$ and $\myb{z}$ not free in $\myapp{\mytmm}{\mytmn}$}}
373 The care required during substituting variables for terms is required to avoid
374 name capturing. We will use substitution in the future for other name-binding
375 constructs assuming similar precautions.
377 These few elements are of remarkable expressiveness, and in fact Turing
378 complete. As a corollary, we must be able to devise a term that reduces forever
379 (`loops' in imperative terms):
382 (\myapp{\omega}{\omega}) \myred (\myapp{\omega}{\omega}) \myred \cdots \text{, with $\omega = \myabs{x}{\myapp{x}{x}}$}
385 A \emph{redex} is a term that can be reduced. In the untyped $\lambda$-calculus
386 this will be the case for an application in which the first term is an
387 abstraction, but in general we call aterm reducible if it appears to the left of
388 a reduction rule. When a term contains no redexes it's said to be in
389 \emph{normal form}. Given the observation above, not all terms reduce to a
390 normal forms: we call the ones that do \emph{normalising}, and the ones that
391 don't \emph{non-normalising}.
393 The reduction rule presented is not syntax directed, but \emph{evaluation
394 strategies} can be employed to reduce term systematically. Common evaluation
395 strategies include \emph{call by value} (or \emph{strict}), where arguments of
396 abstractions are reduced before being applied to the abstraction; and conversely
397 \emph{call by name} (or \emph{lazy}), where we reduce only when we need to do so
398 to proceed---in other words when we have an application where the function is
399 still not a $\lambda$. In both these reduction strategies we never reduce under
400 an abstraction: for this reason a weaker form of normalisation is used, where
401 both abstractions and normal forms are said to be in \emph{weak head normal
404 \subsection{The simply typed $\lambda$-calculus}
406 A convenient way to `discipline' and reason about $\lambda$-terms is to assign
407 \emph{types} to them, and then check that the terms that we are forming make
408 sense given our typing rules \citep{Curry1934}. The first most basic instance
409 of this idea takes the name of \emph{simply typed $\lambda$ calculus}, whose
410 rules are shown in figure \ref{fig:stlc}.
412 Our types contain a set of \emph{type variables} $\Phi$, which might
413 correspond to some `primitive' types; and $\myarr$, the type former for
414 `arrow' types, the types of functions. The language is explicitly
415 typed: when we bring a variable into scope with an abstraction, we
416 declare its type. Reduction is unchanged from the untyped
422 \begin{array}{r@{\ }c@{\ }l}
423 \mytmsyn & ::= & \myb{x} \mysynsep \myabss{\myb{x}}{\mytysyn}{\mytmsyn} \mysynsep
424 (\myapp{\mytmsyn}{\mytmsyn}) \\
425 \mytysyn & ::= & \myse{\phi} \mysynsep \mytysyn \myarr \mytysyn \mysynsep \\
426 \myb{x} & \in & \text{Some enumerable set of symbols} \\
427 \myse{\phi} & \in & \Phi
432 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
434 \AxiomC{$\myctx(x) = A$}
435 \UnaryInfC{$\myjud{\myb{x}}{A}$}
438 \AxiomC{$\myjudd{\myctx;\myb{x} : A}{\mytmt}{\mytyb}$}
439 \UnaryInfC{$\myjud{\myabss{x}{A}{\mytmt}}{\mytyb}$}
442 \AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$}
443 \AxiomC{$\myjud{\mytmn}{\mytya}$}
444 \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mytyb}$}
448 \caption{Syntax and typing rules for the STLC. Reduction is unchanged from
449 the untyped $\lambda$-calculus.}
453 In the typing rules, a context $\myctx$ is used to store the types of bound
454 variables: $\myctx; \myb{x} : \mytya$ adds a variable to the context and
455 $\myctx(x)$ returns the type of the rightmost occurrence of $x$.
457 This typing system takes the name of `simply typed lambda calculus' (STLC), and
458 enjoys a number of properties. Two of them are expected in most type systems
461 \item[Progress] A well-typed term is not stuck---it is either a variable, or its
462 constructor does not appear on the left of the $\myred$ relation (currently
463 only $\lambda$), or it can take a step according to the evaluation rules.
464 \item[Preservation] If a well-typed term takes a step of evaluation, then the
465 resulting term is also well-typed, and preserves the previous type. Also
466 known as \emph{subject reduction}.
469 However, STLC buys us much more: every well-typed term is normalising
470 \citep{Tait1967}. It is easy to see that we can't fill the blanks if we want to
471 give types to the non-normalising term shown before:
473 \myapp{(\myabss{\myb{x}}{\myhole{?}}{\myapp{\myb{x}}{\myb{x}}})}{(\myabss{\myb{x}}{\myhole{?}}{\myapp{\myb{x}}{\myb{x}}})}
476 This makes the STLC Turing incomplete. We can recover the ability to loop by
477 adding a combinator that recurses:
480 \begin{minipage}{0.5\textwidth}
482 $ \mytmsyn ::= \cdots b \mysynsep \myfix{\myb{x}}{\mytysyn}{\mytmsyn} $
486 \begin{minipage}{0.5\textwidth}
487 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}} {
488 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytmt}{\mytya}$}
489 \UnaryInfC{$\myjud{\myfix{\myb{x}}{\mytya}{\mytmt}}{\mytya}$}
494 \mydesc{reduction:}{\myjud{\mytmsyn}{\mytmsyn}}{
495 $ \myfix{\myb{x}}{\mytya}{\mytmt} \myred \mysub{\mytmt}{\myb{x}}{(\myfix{\myb{x}}{\mytya}{\mytmt})}$
498 This will deprive us of normalisation, which is a particularly bad thing if we
499 want to use the STLC as described in the next section.
501 \subsection{The Curry-Howard correspondence}
503 It turns out that the STLC can be seen a natural deduction system for
504 intuitionistic propositional logic. Terms are proofs, and their types are the
505 propositions they prove. This remarkable fact is known as the Curry-Howard
506 correspondence, or isomorphism.
508 The arrow ($\myarr$) type corresponds to implication. If we wish to prove that
509 that $(\mytya \myarr \mytyb) \myarr (\mytyb \myarr \mytycc) \myarr (\mytya
510 \myarr \mytycc)$, all we need to do is to devise a $\lambda$-term that has the
513 \myabss{\myb{f}}{(\mytya \myarr \mytyb)}{\myabss{\myb{g}}{(\mytyb \myarr \mytycc)}{\myabss{\myb{x}}{\mytya}{\myapp{\myb{g}}{(\myapp{\myb{f}}{\myb{x}})}}}}
515 That is, function composition. Going beyond arrow types, we can extend our bare
516 lambda calculus with useful types to represent other logical constructs, as
517 shown in figure \ref{fig:natded}.
522 \begin{array}{r@{\ }c@{\ }l}
523 \mytmsyn & ::= & \cdots \\
524 & | & \mytt \mysynsep \myapp{\myabsurd{\mytysyn}}{\mytmsyn} \\
525 & | & \myapp{\myleft{\mytysyn}}{\mytmsyn} \mysynsep
526 \myapp{\myright{\mytysyn}}{\mytmsyn} \mysynsep
527 \myapp{\mycase{\mytmsyn}{\mytmsyn}}{\mytmsyn} \\
528 & | & \mypair{\mytmsyn}{\mytmsyn} \mysynsep
529 \myapp{\myfst}{\mytmsyn} \mysynsep \myapp{\mysnd}{\mytmsyn} \\
530 \mytysyn & ::= & \cdots \mysynsep \myunit \mysynsep \myempty \mysynsep \mytmsyn \mysum \mytmsyn \mysynsep \mytysyn \myprod \mytysyn
535 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
538 \begin{array}{l@{ }l@{\ }c@{\ }l}
539 \myapp{\mycase{\mytmm}{\mytmn}}{(\myapp{\myleft{\mytya} &}{\mytmt})} & \myred &
540 \myapp{\mytmm}{\mytmt} \\
541 \myapp{\mycase{\mytmm}{\mytmn}}{(\myapp{\myright{\mytya} &}{\mytmt})} & \myred &
542 \myapp{\mytmn}{\mytmt}
547 \begin{array}{l@{ }l@{\ }c@{\ }l}
548 \myapp{\myfst &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmm \\
549 \myapp{\mysnd &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmn
555 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
557 \AxiomC{\phantom{$\myjud{\mytmt}{\myempty}$}}
558 \UnaryInfC{$\myjud{\mytt}{\myunit}$}
561 \AxiomC{$\myjud{\mytmt}{\myempty}$}
562 \UnaryInfC{$\myjud{\myapp{\myabsurd{\mytya}}{\mytmt}}{\mytya}$}
569 \AxiomC{$\myjud{\mytmt}{\mytya}$}
570 \UnaryInfC{$\myjud{\myapp{\myleft{\mytyb}}{\mytmt}}{\mytya \mysum \mytyb}$}
573 \AxiomC{$\myjud{\mytmt}{\mytyb}$}
574 \UnaryInfC{$\myjud{\myapp{\myright{\mytya}}{\mytmt}}{\mytya \mysum \mytyb}$}
582 \AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$}
583 \AxiomC{$\myjud{\mytmn}{\mytya \myarr \mytycc}$}
584 \AxiomC{$\myjud{\mytmt}{\mytya \mysum \mytyb}$}
585 \TrinaryInfC{$\myjud{\myapp{\mycase{\mytmm}{\mytmn}}{\mytmt}}{\mytycc}$}
592 \AxiomC{$\myjud{\mytmm}{\mytya}$}
593 \AxiomC{$\myjud{\mytmn}{\mytyb}$}
594 \BinaryInfC{$\myjud{\mypair{\mytmm}{\mytmn}}{\mytya \myprod \mytyb}$}
597 \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
598 \UnaryInfC{$\myjud{\myapp{\myfst}{\mytmt}}{\mytya}$}
601 \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
602 \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mytyb}$}
606 \caption{Rules for the extendend STLC. Only the new features are shown, all the
607 rules and syntax for the STLC apply here too.}
611 Tagged unions (or sums, or coproducts---$\mysum$ here, \texttt{Either}
612 in Haskell) correspond to disjunctions, and dually tuples (or pairs, or
613 products---$\myprod$ here, tuples in Haskell) correspond to
614 conjunctions. This is apparent looking at the ways to construct and
615 destruct the values inhabiting those types: for $\mysum$ $\myleft{ }$
616 and $\myright{ }$ correspond to $\vee$ introduction, and
617 $\mycase{\myarg}{\myarg}$ to $\vee$ elimination; for $\myprod$
618 $\mypair{\myarg}{\myarg}$ corresponds to $\wedge$ introduction, $\myfst$
619 and $\mysnd$ to $\wedge$ elimination.
621 The trivial type $\myunit$ corresponds to the logical $\top$, and dually
622 $\myempty$ corresponds to the logical $\bot$. $\myunit$ has one introduction
623 rule ($\mytt$), and thus one inhabitant; and no eliminators. $\myempty$ has no
624 introduction rules, and thus no inhabitants; and one eliminator ($\myabsurd{
625 }$), corresponding to the logical \emph{ex falso quodlibet}.
627 With these rules, our STLC now looks remarkably similar in power and use to the
628 natural deduction we already know. $\myneg \mytya$ can be expressed as $\mytya
629 \myarr \myempty$. However, there is an important omission: there is no term of
630 the type $\mytya \mysum \myneg \mytya$ (excluded middle), or equivalently
631 $\myneg \myneg \mytya \myarr \mytya$ (double negation), or indeed any term with
632 a type equivalent to those.
634 This has a considerable effect on our logic and it's no coincidence, since there
635 is no obvious computational behaviour for laws like the excluded middle.
636 Theories of this kind are called \emph{intuitionistic}, or \emph{constructive},
637 and all the systems analysed will have this characteristic since they build on
638 the foundation of the STLC\footnote{There is research to give computational
639 behaviour to classical logic, but I will not touch those subjects.}.
641 As in logic, if we want to keep our system consistent, we must make sure that no
642 closed terms (in other words terms not under a $\lambda$) inhabit $\myempty$.
643 The variant of STLC presented here is indeed
644 consistent, a result that follows from the fact that it is
645 normalising. % TODO explain
646 Going back to our $\mysyn{fix}$ combinator, it is easy to see how it ruins our
647 desire for consistency. The following term works for every type $\mytya$,
650 (\myfix{\myb{x}}{\mytya}{\myb{x}}) : \mytya
653 \subsection{Inductive data}
656 To make the STLC more useful as a programming language or reasoning tool it is
657 common to include (or let the user define) inductive data types. These comprise
658 of a type former, various constructors, and an eliminator (or destructor) that
659 serves as primitive recursor.
661 For example, we might add a $\mylist$ type constructor, along with an `empty
662 list' ($\mynil{ }$) and `cons cell' ($\mycons$) constructor. The eliminator for
663 lists will be the usual folding operation ($\myfoldr$). See figure
669 \begin{array}{r@{\ }c@{\ }l}
670 \mytmsyn & ::= & \cdots \mysynsep \mynil{\mytysyn} \mysynsep \mytmsyn \mycons \mytmsyn
672 \myapp{\myapp{\myapp{\myfoldr}{\mytmsyn}}{\mytmsyn}}{\mytmsyn} \\
673 \mytysyn & ::= & \cdots \mysynsep \myapp{\mylist}{\mytysyn}
677 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
679 \begin{array}{l@{\ }c@{\ }l}
680 \myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{\mynil{\mytya}} & \myred & \mytmt \\
682 \myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{(\mytmm \mycons \mytmn)} & \myred &
683 \myapp{\myapp{\myse{f}}{\mytmm}}{(\myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{\mytmn})}
687 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
689 \AxiomC{\phantom{$\myjud{\mytmm}{\mytya}$}}
690 \UnaryInfC{$\myjud{\mynil{\mytya}}{\myapp{\mylist}{\mytya}}$}
693 \AxiomC{$\myjud{\mytmm}{\mytya}$}
694 \AxiomC{$\myjud{\mytmn}{\myapp{\mylist}{\mytya}}$}
695 \BinaryInfC{$\myjud{\mytmm \mycons \mytmn}{\myapp{\mylist}{\mytya}}$}
700 \AxiomC{$\myjud{\mysynel{f}}{\mytya \myarr \mytyb \myarr \mytyb}$}
701 \AxiomC{$\myjud{\mytmm}{\mytyb}$}
702 \AxiomC{$\myjud{\mytmn}{\myapp{\mylist}{\mytya}}$}
703 \TrinaryInfC{$\myjud{\myapp{\myapp{\myapp{\myfoldr}{\mysynel{f}}}{\mytmm}}{\mytmn}}{\mytyb}$}
706 \caption{Rules for lists in the STLC.}
710 In section \ref{sec:well-order} we will see how to give a general account of
711 inductive data. %TODO does this make sense to have here?
713 \section{Intuitionistic Type Theory}
716 \subsection{Extending the STLC}
718 The STLC can be made more expressive in various ways. \cite{Barendregt1991}
719 succinctly expressed geometrically how we can add expressivity:
723 & \lambda\omega \ar@{-}[rr]\ar@{-}'[d][dd]
724 & & \lambda C \ar@{-}[dd]
726 \lambda2 \ar@{-}[ur]\ar@{-}[rr]\ar@{-}[dd]
727 & & \lambda P2 \ar@{-}[ur]\ar@{-}[dd]
729 & \lambda\underline\omega \ar@{-}'[r][rr]
730 & & \lambda P\underline\omega
732 \lambda{\to} \ar@{-}[rr]\ar@{-}[ur]
733 & & \lambda P \ar@{-}[ur]
736 Here $\lambda{\to}$, in the bottom left, is the STLC. From there can move along
739 \item[Terms depending on types (towards $\lambda{2}$)] We can quantify over
740 types in our type signatures. For example, we can define a polymorphic
742 {\small\[\displaystyle
743 (\myabss{\myb{A}}{\mytyp}{\myabss{\myb{x}}{\myb{A}}{\myb{x}}}) : (\myb{A} : \mytyp) \myarr \myb{A} \myarr \myb{A}
745 The first and most famous instance of this idea has been System F. This form
746 of polymorphism and has been wildly successful, also thanks to a well known
747 inference algorithm for a restricted version of System F known as
748 Hindley-Milner. Languages like Haskell and SML are based on this discipline.
749 \item[Types depending on types (towards $\lambda{\underline{\omega}}$)] We have
750 type operators. For example we could define a function that given types $R$
751 and $\mytya$ forms the type that represents a value of type $\mytya$ in
752 continuation passing style: {\small\[\displaystyle(\myabss{\myb{A} \myar \myb{R}}{\mytyp}{(\myb{A}
753 \myarr \myb{R}) \myarr \myb{R}}) : \mytyp \myarr \mytyp \myarr \mytyp\]}
754 \item[Types depending on terms (towards $\lambda{P}$)] Also known as `dependent
755 types', give great expressive power. For example, we can have values of whose
756 type depend on a boolean:
757 {\small\[\displaystyle(\myabss{\myb{x}}{\mybool}{\myite{\myb{x}}{\mynat}{\myrat}}) : \mybool
761 All the systems preserve the properties that make the STLC well behaved. The
762 system we are going to focus on, Intuitionistic Type Theory, has all of the
763 above additions, and thus would sit where $\lambda{C}$ sits in the
764 `$\lambda$-cube'. It will serve as the logical `core' of all the other
765 extensions that we will present and ultimately our implementation of a similar
768 \subsection{A Bit of History}
770 Logic frameworks and programming languages based on type theory have a long
771 history. Per Martin-L\"{o}f described the first version of his theory in 1971,
772 but then revised it since the original version was inconsistent due to its
773 impredicativity\footnote{In the early version there was only one universe
774 $\mytyp$ and $\mytyp : \mytyp$, see section \ref{sec:term-types} for an
775 explanation on why this causes problems.}. For this reason he gave a revised
776 and consistent definition later \citep{Martin-Lof1984}.
778 A related development is the polymorphic $\lambda$-calculus, and specifically
779 the previously mentioned System F, which was developed independently by Girard
780 and Reynolds. An overview can be found in \citep{Reynolds1994}. The surprising
781 fact is that while System F is impredicative it is still consistent and strongly
782 normalising. \cite{Coquand1986} further extended this line of work with the
783 Calculus of Constructions (CoC).
785 Most widely used interactive theorem provers are based on ITT. Popular ones
786 include Agda \citep{Norell2007, Bove2009}, Coq \citep{Coq}, and Epigram
787 \citep{McBride2004, EpigramTut}.
789 \subsection{A note on inference}
791 % TODO do this, adding links to the sections about bidi type checking and
792 % implicit universes.
793 In the following text I will often omit explicit typing for abstractions or
795 Moreover, I will use $\mytyp$ without bothering to specify a
796 universe, with the silent assumption that the definition is consistent
797 regarding to the hierarchy.
799 \subsection{A simple type theory}
802 The calculus I present follows the exposition in \citep{Thompson1991},
803 and is quite close to the original formulation of predicative ITT as
804 found in \citep{Martin-Lof1984}. The system's syntax and reduction
805 rules are presented in their entirety in figure \ref{fig:core-tt-syn}.
806 The typing rules are presented piece by piece. Agda and \mykant\
807 renditions of the presented theory and all the examples is reproduced in
808 appendix \ref{app:itt-code}.
813 \begin{array}{r@{\ }c@{\ }l}
814 \mytmsyn & ::= & \myb{x} \mysynsep
816 \myunit \mysynsep \mytt \mysynsep
817 \myempty \mysynsep \myapp{\myabsurd{\mytmsyn}}{\mytmsyn} \\
818 & | & \mybool \mysynsep \mytrue \mysynsep \myfalse \mysynsep
819 \myitee{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
820 & | & \myfora{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
821 \myabss{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
822 (\myapp{\mytmsyn}{\mytmsyn}) \\
823 & | & \myexi{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
824 \mypairr{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn} \\
825 & | & \myapp{\myfst}{\mytmsyn} \mysynsep \myapp{\mysnd}{\mytmsyn} \\
826 & | & \myw{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
827 \mytmsyn \mynode{\myb{x}}{\mytmsyn} \mytmsyn \\
828 & | & \myrec{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn} \\
834 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
837 \begin{array}{l@{ }l@{\ }c@{\ }l}
838 \myitee{\mytrue &}{\myb{x}}{\myse{P}}{\mytmm}{\mytmn} & \myred & \mytmm \\
839 \myitee{\myfalse &}{\myb{x}}{\myse{P}}{\mytmm}{\mytmn} & \myred & \mytmn \\
844 \myapp{(\myabss{\myb{x}}{\mytya}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{\myb{x}}{\mytmn}
848 \begin{array}{l@{ }l@{\ }c@{\ }l}
849 \myapp{\myfst &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmm \\
850 \myapp{\mysnd &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmn
858 \myrec{(\myse{s} \mynode{\myb{x}}{\myse{T}} \myse{f})}{\myb{y}}{\myse{P}}{\myse{p}} \myred
859 \myapp{\myapp{\myapp{\myse{p}}{\myse{s}}}{\myse{f}}}{(\myabss{\myb{t}}{\mysub{\myse{T}}{\myb{x}}{\myse{s}}}{
860 \myrec{\myapp{\myse{f}}{\myb{t}}}{\myb{y}}{\myse{P}}{\mytmt}
864 \caption{Syntax and reduction rules for our type theory.}
865 \label{fig:core-tt-syn}
868 \subsubsection{Types are terms, some terms are types}
869 \label{sec:term-types}
871 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
873 \AxiomC{$\myjud{\mytmt}{\mytya}$}
874 \AxiomC{$\mytya \mydefeq \mytyb$}
875 \BinaryInfC{$\myjud{\mytmt}{\mytyb}$}
878 \AxiomC{\phantom{$\myjud{\mytmt}{\mytya}$}}
879 \UnaryInfC{$\myjud{\mytyp_l}{\mytyp_{l + 1}}$}
884 The first thing to notice is that a barrier between values and types that we had
885 in the STLC is gone: values can appear in types, and the two are treated
886 uniformly in the syntax.
888 While the usefulness of doing this will become clear soon, a consequence is
889 that since types can be the result of computation, deciding type equality is
890 not immediate as in the STLC. For this reason we define \emph{definitional
891 equality}, $\mydefeq$, as the congruence relation extending
892 $\myred$---moreover, when comparing types syntactically we do it up to
893 renaming of bound names ($\alpha$-renaming). For example under this
894 discipline we will find that
896 \myabss{\myb{x}}{\mytya}{\myb{x}} \mydefeq \myabss{\myb{y}}{\mytya}{\myb{y}}
898 Types that are definitionally equal can be used interchangeably. Here
899 the `conversion' rule is not syntax directed, but it is possible to
900 employ $\myred$ to decide term equality in a systematic way, by always
901 reducing terms to their normal forms before comparing them, so that a
902 separate conversion rule is not needed. % TODO add section
903 Another thing to notice is that considering the need to reduce terms to
904 decide equality, it is essential for a dependently type system to be
905 terminating and confluent for type checking to be decidable.
907 Moreover, we specify a \emph{type hierarchy} to talk about `large'
908 types: $\mytyp_0$ will be the type of types inhabited by data:
909 $\mybool$, $\mynat$, $\mylist$, etc. $\mytyp_1$ will be the type of
910 $\mytyp_0$, and so on---for example we have $\mytrue : \mybool :
911 \mytyp_0 : \mytyp_1 : \cdots$. Each type `level' is often called a
912 universe in the literature. While it is possible to simplify things by
913 having only one universe $\mytyp$ with $\mytyp : \mytyp$, this plan is
914 inconsistent for much the same reason that impredicative na\"{\i}ve set
915 theory is \citep{Hurkens1995}. However various techniques can be
916 employed to lift the burden of explicitly handling universes, as we will
917 see in section \ref{sec:term-hierarchy}.
919 \subsubsection{Contexts}
921 \begin{minipage}{0.5\textwidth}
922 \mydesc{context validity:}{\myvalid{\myctx}}{
924 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
925 \UnaryInfC{$\myvalid{\myemptyctx}$}
928 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
929 \UnaryInfC{$\myvalid{\myctx ; \myb{x} : \mytya}$}
934 \begin{minipage}{0.5\textwidth}
935 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
936 \AxiomC{$\myctx(x) = \mytya$}
937 \UnaryInfC{$\myjud{\myb{x}}{\mytya}$}
943 We need to refine the notion context to make sure that every variable appearing
944 is typed correctly, or that in other words each type appearing in the context is
945 indeed a type and not a value. In every other rule, if no premises are present,
946 we assume the context in the conclusion to be valid.
948 Then we can re-introduce the old rule to get the type of a variable for a
951 \subsubsection{$\myunit$, $\myempty$}
953 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
955 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
956 \UnaryInfC{$\myjud{\myunit}{\mytyp_0}$}
958 \UnaryInfC{$\myjud{\myempty}{\mytyp_0}$}
961 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
962 \UnaryInfC{$\myjud{\mytt}{\myunit}$}
964 \UnaryInfC{\phantom{$\myjud{\myempty}{\mytyp_0}$}}
967 \AxiomC{$\myjud{\mytmt}{\myempty}$}
968 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
969 \BinaryInfC{$\myjud{\myapp{\myabsurd{\mytya}}{\mytmt}}{\mytya}$}
971 \UnaryInfC{\phantom{$\myjud{\myempty}{\mytyp_0}$}}
976 Nothing surprising here: $\myunit$ and $\myempty$ are unchanged from the STLC,
977 with the added rules to type $\myunit$ and $\myempty$ themselves, and to make
978 sure that we are invoking $\myabsurd{}$ over a type.
980 \subsubsection{$\mybool$, and dependent $\myfun{if}$}
982 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
985 \UnaryInfC{$\myjud{\mybool}{\mytyp_0}$}
989 \UnaryInfC{$\myjud{\mytrue}{\mybool}$}
993 \UnaryInfC{$\myjud{\myfalse}{\mybool}$}
998 \AxiomC{$\myjud{\mytmt}{\mybool}$}
999 \AxiomC{$\myjudd{\myctx : \mybool}{\mytya}{\mytyp_l}$}
1001 \BinaryInfC{$\myjud{\mytmm}{\mysub{\mytya}{x}{\mytrue}}$ \hspace{0.7cm} $\myjud{\mytmn}{\mysub{\mytya}{x}{\myfalse}}$}
1002 \UnaryInfC{$\myjud{\myitee{\mytmt}{\myb{x}}{\mytya}{\mytmm}{\mytmn}}{\mysub{\mytya}{\myb{x}}{\mytmt}}$}
1006 With booleans we get the first taste of the `dependent' in `dependent
1007 types'. While the two introduction rules ($\mytrue$ and $\myfalse$) are
1008 not surprising, the typing rules for $\myfun{if}$ are. In most strongly
1009 typed languages we expect the branches of an $\myfun{if}$ statements to
1010 be of the same type, to preserve subject reduction, since execution
1011 could take both paths. This is a pity, since the type system does not
1012 reflect the fact that in each branch we gain knowledge on the term we
1013 are branching on. Which means that programs along the lines of
1014 {\small\[\text{\texttt{if null xs then head xs else 0}}\]}
1015 are a necessary, well typed, danger.
1017 However, in a more expressive system, we can do better: the branches' type can
1018 depend on the value of the scrutinised boolean. This is what the typing rule
1019 expresses: the user provides a type $\mytya$ ranging over an $\myb{x}$
1020 representing the scrutinised boolean type, and the branches are typechecked with
1021 the updated knowledge on the value of $\myb{x}$.
1023 \subsubsection{$\myarr$, or dependent function}
1025 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1026 \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
1027 \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
1028 \BinaryInfC{$\myjud{\myfora{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
1034 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytmt}{\mytyb}$}
1035 \UnaryInfC{$\myjud{\myabss{\myb{x}}{\mytya}{\mytmt}}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
1038 \AxiomC{$\myjud{\mytmm}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
1039 \AxiomC{$\myjud{\mytmn}{\mytya}$}
1040 \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mysub{\mytyb}{\myb{x}}{\mytmn}}$}
1045 Dependent functions are one of the two key features that perhaps most
1046 characterise dependent types---the other being dependent products. With
1047 dependent functions, the result type can depend on the value of the
1048 argument. This feature, together with the fact that the result type
1049 might be a type itself, brings a lot of interesting possibilities.
1050 Following this intuition, in the introduction rule, the return type is
1051 typechecked in a context with an abstracted variable of lhs' type, and
1052 in the elimination rule the actual argument is substituted in the return
1053 type. Keeping the correspondence with logic alive, dependent functions
1054 are much like universal quantifiers ($\forall$) in logic.
1056 For example, assuming that we have lists and natural numbers in our
1057 language, using dependent functions we would be able to
1061 \myfun{length} : (\myb{A} {:} \mytyp_0) \myarr \myapp{\mylist}{\myb{A}} \myarr \mynat \\
1062 \myarg \myfun{$>$} \myarg : \mynat \myarr \mynat \myarr \mytyp_0 \\
1063 \myfun{head} : (\myb{A} {:} \mytyp_0) \myarr (\myb{l} {:} \myapp{\mylist}{\myb{A}})
1064 \myarr \myapp{\myapp{\myfun{length}}{\myb{A}}}{\myb{l}} \mathrel{\myfun{>}} 0 \myarr
1069 \myfun{length} is the usual polymorphic length function. $\myfun{>}$ is
1070 a function that takes two naturals and returns a type: if the lhs is
1071 greater then the rhs, $\myunit$ is returned, $\myempty$ otherwise. This
1072 way, we can express a `non-emptyness' condition in $\myfun{head}$, by
1073 including a proof that the length of the list argument is non-zero.
1074 This allows us to rule out the `empty list' case, so that we can safely
1075 return the first element.
1077 Again, we need to make sure that the type hierarchy is respected, which is the
1078 reason why a type formed by $\myarr$ will live in the least upper bound of the
1079 levels of argument and return type. This trend will continue with the other
1080 type-level binders, $\myprod$ and $\mytyc{W}$.
1082 \subsubsection{$\myprod$, or dependent product}
1085 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1086 \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
1087 \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
1088 \BinaryInfC{$\myjud{\myexi{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
1094 \AxiomC{$\myjud{\mytmm}{\mytya}$}
1095 \AxiomC{$\myjud{\mytmn}{\mysub{\mytyb}{\myb{x}}{\mytmm}}$}
1096 \BinaryInfC{$\myjud{\mypairr{\mytmm}{\myb{x}}{\mytyb}{\mytmn}}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
1098 \UnaryInfC{\phantom{$--$}}
1101 \AxiomC{$\myjud{\mytmt}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
1102 \UnaryInfC{$\hspace{0.7cm}\myjud{\myapp{\myfst}{\mytmt}}{\mytya}\hspace{0.7cm}$}
1104 \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mysub{\mytyb}{\myb{x}}{\myapp{\myfst}{\mytmt}}}$}
1109 If dependent functions are a generalisation of $\myarr$ in the STLC,
1110 dependent products are a generalisation of $\myprod$ in the STLC. The
1111 improvement is that the second element's type can depend on the value of
1112 the first element. The corrispondence with logic is through the
1113 existential quantifier: $\exists x \in \mathbb{N}. even(x)$ can be
1114 expressed as $\myexi{\myb{x}}{\mynat}{\myapp{\myfun{even}}{\myb{x}}}$.
1115 The first element will be a number, and the second evidence that the
1116 number is even. This highlights the fact that we are working in a
1117 constructive logic: if we have an existence proof, we can always ask for
1118 a witness. This means, for instance, that $\neg \forall \neg$ is not
1119 equivalent to $\exists$.
1121 Another perhaps more `dependent' application of products, paired with
1122 $\mybool$, is to offer choice between different types. For example we
1123 can easily recover disjunctions:
1126 \myarg\myfun{$\vee$}\myarg : \mytyp_0 \myarr \mytyp_0 \myarr \mytyp_0 \\
1127 \myb{A} \mathrel{\myfun{$\vee$}} \myb{B} \mapsto \myexi{\myb{x}}{\mybool}{\myite{\myb{x}}{\myb{A}}{\myb{B}}} \\ \ \\
1128 \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} \\
1129 \myfun{case} \myappsp \myb{A} \myappsp \myb{B} \myappsp \myb{C} \myappsp \myb{f} \myappsp \myb{g} \myappsp \myb{x} \mapsto \\
1130 \myind{2} \myapp{(\myitee{\myapp{\myfst}{\myb{b}}}{\myb{x}}{(\myite{\myb{b}}{\myb{A}}{\myb{B}})}{\myb{f}}{\myb{g}})}{(\myapp{\mysnd}{\myb{x}})}
1134 \subsubsection{$\mytyc{W}$, or well-order}
1135 \label{sec:well-order}
1137 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1138 \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
1139 \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
1140 \BinaryInfC{$\myjud{\myw{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
1145 \AxiomC{$\myjud{\mytmt}{\mytya}$}
1146 \AxiomC{$\myjud{\mysynel{f}}{\mysub{\mytyb}{\myb{x}}{\mytmt} \myarr \myw{\myb{x}}{\mytya}{\mytyb}}$}
1147 \BinaryInfC{$\myjud{\mytmt \mynode{\myb{x}}{\mytyb} \myse{f}}{\myw{\myb{x}}{\mytya}{\mytyb}}$}
1152 \AxiomC{$\myjud{\myse{u}}{\myw{\myb{x}}{\myse{S}}{\myse{T}}}$}
1153 \AxiomC{$\myjudd{\myctx; \myb{w} : \myw{\myb{x}}{\myse{S}}{\myse{T}}}{\myse{P}}{\mytyp_l}$}
1155 \BinaryInfC{$\myjud{\myse{p}}{
1156 \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}}}}
1158 \UnaryInfC{$\myjud{\myrec{\myse{u}}{\myb{w}}{\myse{P}}{\myse{p}}}{\mysub{\myse{P}}{\myb{w}}{\myse{u}}}$}
1162 Finally, the well-order type, or in short $\mytyc{W}$-type, which will
1163 let us represent inductive data in a general (but clumsy) way. The core
1169 \section{The struggle for equality}
1170 \label{sec:equality}
1172 In the previous section we saw how a type checker (or a human) needs a
1173 notion of \emph{definitional equality}. Beyond this meta-theoretic
1174 notion, in this section we will explore the ways of expressing equality
1175 \emph{inside} the theory, as a reasoning tool available to the user.
1176 This area is the main concern of this thesis, and in general a very
1177 active research topic, since we do not have a fully satisfactory
1178 solution, yet. As in the previous section, everything presented is
1179 formalised in Agda in appendix \ref{app:agda-itt}.
1181 \subsection{Propositional equality}
1184 \begin{minipage}{0.5\textwidth}
1187 \begin{array}{r@{\ }c@{\ }l}
1188 \mytmsyn & ::= & \cdots \\
1189 & | & \mytmsyn \mypeq{\mytmsyn} \mytmsyn \mysynsep
1190 \myapp{\myrefl}{\mytmsyn} \\
1191 & | & \myjeq{\mytmsyn}{\mytmsyn}{\mytmsyn}
1196 \begin{minipage}{0.5\textwidth}
1197 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
1199 \myjeq{\myse{P}}{(\myapp{\myrefl}{\mytmm})}{\mytmn} \myred \mytmn
1205 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1206 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
1207 \AxiomC{$\myjud{\mytmm}{\mytya}$}
1208 \AxiomC{$\myjud{\mytmn}{\mytya}$}
1209 \TrinaryInfC{$\myjud{\mytmm \mypeq{\mytya} \mytmn}{\mytyp_l}$}
1215 \AxiomC{$\begin{array}{c}\ \\\myjud{\mytmm}{\mytya}\hspace{1.1cm}\mytmm \mydefeq \mytmn\end{array}$}
1216 \UnaryInfC{$\myjud{\myapp{\myrefl}{\mytmm}}{\mytmm \mypeq{\mytya} \mytmn}$}
1221 \myjud{\myse{P}}{\myfora{\myb{x}\ \myb{y}}{\mytya}{\myfora{q}{\myb{x} \mypeq{\mytya} \myb{y}}{\mytyp_l}}} \\
1222 \myjud{\myse{q}}{\mytmm \mypeq{\mytya} \mytmn}\hspace{1.1cm}\myjud{\myse{p}}{\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmm}}{(\myapp{\myrefl}{\mytmm})}}
1225 \UnaryInfC{$\myjud{\myjeq{\myse{P}}{\myse{q}}{\myse{p}}}{\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmn}}{q}}$}
1230 To express equality between two terms inside ITT, the obvious way to do so is
1231 to have the equality construction to be a type-former. Here we present what
1232 has survived as the dominating form of equality in systems based on ITT up to
1235 Our type former is $\mypeq{\mytya}$, which given a type (in this case
1236 $\mytya$) relates equal terms of that type. $\mypeq{}$ has one introduction
1237 rule, $\myrefl$, which introduces an equality relation between definitionally
1240 Finally, we have one eliminator for $\mypeq{}$, $\myjeqq$. $\myjeq{\myse{P}}{\myse{q}}{\myse{p}}$ takes
1242 \item $\myse{P}$, a predicate working with two terms of a certain type (say
1243 $\mytya$) and a proof of their equality
1244 \item $\myse{q}$, a proof that two terms in $\mytya$ (say $\myse{m}$ and
1245 $\myse{n}$) are equal
1246 \item and $\myse{p}$, an inhabitant of $\myse{P}$ applied to $\myse{m}$, plus
1247 the trivial proof by reflexivity showing that $\myse{m}$ is equal to itself
1249 Given these ingredients, $\myjeqq$ retuns a member of $\myse{P}$ applied to
1250 $\mytmm$, $\mytmn$, and $\myse{q}$. In other words $\myjeqq$ takes a
1251 witness that $\myse{P}$ works with \emph{definitionally equal} terms, and
1252 returns a witness of $\myse{P}$ working with \emph{propositionally equal}
1253 terms. Invokations of $\myjeqq$ will vanish when the equality proofs will
1254 reduce to invocations to reflexivity, at which point the arguments must be
1255 definitionally equal, and thus the provided
1256 $\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmm}}{(\myapp{\myrefl}{\mytmm})}$
1259 While the $\myjeqq$ rule is slightly convoluted, ve can derive many more
1260 `friendly' rules from it, for example a more obvious `substitution' rule, that
1261 replaces equal for equal in predicates:
1264 \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}}}}} \\
1265 \myfun{subst}\myappsp \myb{A}\myappsp\myb{P}\myappsp\myb{x}\myappsp\myb{y}\myappsp\myb{q}\myappsp\myb{p} \mapsto
1266 \myjeq{(\myabs{\myb{x}\ \myb{y}\ \myb{q}}{\myapp{\myb{P}}{\myb{y}}})}{\myb{p}}{\myb{q}}
1269 Once we have $\myfun{subst}$, we can easily prove more familiar laws regarding
1270 equality, such as symmetry, transitivity, and a congruence law.
1274 \subsection{Common extensions}
1276 Our definitional equality can be made larger in various ways, here we
1277 review some common extensions.
1279 \subsubsection{Congruence laws and $\eta$-expansion}
1281 A simple type-directed check that we can do on functions and records is
1282 $\eta$-expansion. We can then have
1284 \mydesc{definitional equality:}{\myjud{\mytmm \mydefeq \mytmn}{\mytmsyn}}{
1286 \AxiomC{$\myjud{f \mydefeq (\myabss{\myb{x}}{\mytya}{\myapp{\myse{g}}{\myb{x}}})}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
1287 \UnaryInfC{$\myjud{\myse{f} \mydefeq \myse{g}}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
1290 \AxiomC{$\myjud{\mytmm \mydefeq \mypair{\myapp{\myfst}{\mytmn}}{\myapp{\mysnd}{\mytmn}}}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
1291 \UnaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
1297 \AxiomC{$\myjud{\mytmm}{\myunit}$}
1298 \AxiomC{$\myjud{\mytmn}{\myunit}$}
1299 \BinaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\myunit}$}
1305 \subsubsection{Uniqueness of identity proofs}
1308 % TODO reference the fact that J does not imply J
1309 % TODO mention univalence
1312 \mydesc{definitional equality:}{\myjud{\mytmm \mydefeq \mytmn}{\mytmsyn}}{
1315 \myjud{\myse{P}}{\myfora{\myb{x}}{\mytya}{\myb{x} \mypeq{\mytya} \myb{x} \myarr \mytyp}} \\\
1316 \myjud{\myse{p}}{\myfora{\myb{x}}{\mytya}{\myse{P} \myappsp \myb{x} \myappsp \myb{x} \myappsp (\myrefl \myapp \myb{x})}} \hspace{1cm}
1317 \myjud{\mytmt}{\mytya} \hspace{1cm}
1318 \myjud{\myse{q}}{\mytmt \mypeq{\mytya} \mytmt}
1321 \UnaryInfC{$\myjud{\myfun{K} \myappsp \myse{P} \myappsp \myse{p} \myappsp \myse{t} \myappsp \myse{q}}{\myse{P} \myappsp \mytmt \myappsp \myse{q}}$}
1325 \subsection{Limitations}
1327 \epigraph{\emph{Half of my time spent doing research involves thinking up clever
1328 schemes to avoid needing functional extensionality.}}{@larrytheliquid}
1330 However, propositional equality as described is quite restricted when
1331 reasoning about equality beyond the term structure, which is what definitional
1332 equality gives us (extension notwithstanding).
1334 The problem is best exemplified by \emph{function extensionality}. In
1335 mathematics, we would expect to be able to treat functions that give equal
1336 output for equal input as the same. When reasoning in a mechanised framework
1337 we ought to be able to do the same: in the end, without considering the
1338 operational behaviour, all functions equal extensionally are going to be
1339 replaceable with one another.
1341 However this is not the case, or in other words with the tools we have we have
1344 \myfun{ext} : \myfora{\myb{A}\ \myb{B}}{\mytyp}{\myfora{\myb{f}\ \myb{g}}{
1345 \myb{A} \myarr \myb{B}}{
1346 (\myfora{\myb{x}}{\myb{A}}{\myapp{\myb{f}}{\myb{x}} \mypeq{\myb{B}} \myapp{\myb{g}}{\myb{x}}}) \myarr
1347 \myb{f} \mypeq{\myb{A} \myarr \myb{B}} \myb{g}
1351 To see why this is the case, consider the functions
1352 {\small\[\myabs{\myb{x}}{0 \mathrel{\myfun{+}} \myb{x}}$ and $\myabs{\myb{x}}{\myb{x} \mathrel{\myfun{+}} 0}\]}
1353 where $\myfun{+}$ is defined by recursion on the first argument,
1354 gradually destructing it to build up successors of the second argument.
1355 The two functions are clearly extensionally equal, and we can in fact
1358 \myfora{\myb{x}}{\mynat}{(0 \mathrel{\myfun{+}} \myb{x}) \mypeq{\mynat} (\myb{x} \mathrel{\myfun{+}} 0)}
1360 By analysis on the $\myb{x}$. However, the two functions are not
1361 definitionally equal, and thus we won't be able to get rid of the
1364 For the reasons above, theories that offer a propositional equality
1365 similar to what we presented are called \emph{intensional}, as opposed
1366 to \emph{extensional}. Most systems in wide use today (such as Agda,
1367 Coq, and Epigram) are of this kind.
1369 This is quite an annoyance that often makes reasoning awkward to execute. It
1370 also extends to other fields, for example proving bisimulation between
1371 processes specified by coinduction, or in general proving equivalences based
1372 on the behaviour on a term.
1374 \subsection{Equality reflection}
1376 One way to `solve' this problem is by identifying propositional equality with
1377 definitional equality:
1379 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1380 \AxiomC{$\myjud{\myse{q}}{\mytmm \mypeq{\mytya} \mytmn}$}
1381 \UnaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\mytya}$}
1385 This rule takes the name of \emph{equality reflection}, and is a very
1386 different rule from the ones we saw up to now: it links a typing judgement
1387 internal to the type theory to a meta-theoretic judgement that the type
1388 checker uses to work with terms. It is easy to see the dangerous consequences
1391 \item The rule is syntax directed, and the type checker is presumably expected
1392 to come up with equality proofs when needed.
1393 \item More worryingly, type checking becomes undecidable also because
1394 computing under false assumptions becomes unsafe, since we can use
1395 equality reflection and the conversion rule to have terms of any
1397 Consider for example {\small\[ \myabss{\myb{q}}{\mytya
1398 \mypeq{\mytyp} (\mytya \myarr \mytya)}{\myhole{?}}
1400 Using the assumed proof in tandem with equality reflection we
1401 could easily write a classic Y combinator, sending the compiler into a
1402 loop. In general, we using the conversion rule
1403 % TODO check that this makes sense
1406 Given these facts theories employing equality reflection, like NuPRL
1407 \citep{NuPRL}, carry the derivations that gave rise to each typing judgement
1408 to keep the systems manageable. % TODO more info, problems with that.
1410 For all its faults, equality reflection does allow us to prove extensionality,
1411 using the extensions we gave above. Assuming that $\myctx$ contains
1412 {\small\[\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}}}\]}
1416 \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}$}
1417 \RightLabel{equality reflection}
1418 \UnaryInfC{$\myjudd{\myctx; \myb{x} : \myb{A}}{\myapp{\myb{f}}{\myb{x}} \mydefeq \myapp{\myb{g}}{\myb{x}}}{\myb{B}}$}
1419 \RightLabel{congruence for $\lambda$s}
1420 \UnaryInfC{$\myjud{(\myabs{\myb{x}}{\myapp{\myb{f}}{\myb{x}}}) \mydefeq (\myabs{\myb{x}}{\myapp{\myb{g}}{\myb{x}}})}{\myb{A} \myarr \myb{B}}$}
1421 \RightLabel{$\eta$-law for $\lambda$}
1422 \UnaryInfC{$\hspace{1.45cm}\myjud{\myb{f} \mydefeq \myb{g}}{\myb{A} \myarr \myb{B}}\hspace{1.45cm}$}
1423 \RightLabel{$\myrefl$}
1424 \UnaryInfC{$\myjud{\myapp{\myrefl}{\myb{f}}}{\myb{f} \mypeq{} \myb{g}}$}
1427 Now, the question is: do we need to give up well-behavedness of our theory to
1428 gain extensionality?
1430 \subsection{Some alternatives}
1433 % TODO add `extentional axioms' (Hoffman), setoid models (Thorsten)
1435 \section{Observational equality}
1438 A recent development by \citet{Altenkirch2007}, \emph{Observational Type
1439 Theory} (OTT), promises to keep the well behavedness of ITT while
1440 being able to gain many useful equality proofs\footnote{It is suspected
1441 that OTT gains \emph{all} the equality proofs of ETT, but no proof
1442 exists yet.}, including function extensionality. The main idea is to
1443 give the user the possibility to \emph{coerce} (or transport) values
1444 from a type $\mytya$ to a type $\mytyb$, if the type checker can prove
1445 structurally that $\mytya$ and $\mytya$ are equal; and providing a
1446 value-level equality based on similar principles. Here we give an
1447 exposition which follows closely the original paper.
1449 \subsection{A simpler theory, a propositional fragment}
1452 $\mytyp_l$ is replaced by $\mytyp$. \\\ \\
1454 \begin{array}{r@{\ }c@{\ }l}
1455 \mytmsyn & ::= & \cdots \mysynsep \myprdec{\myprsyn} \mysynsep
1456 \myITE{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
1457 \myprsyn & ::= & \mybot \mysynsep \mytop \mysynsep \myprsyn \myand \myprsyn
1458 \mysynsep \myprfora{\myb{x}}{\mytmsyn}{\myprsyn}
1463 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1465 \AxiomC{$\myjud{\myse{P}}{\myprop}$}
1466 \UnaryInfC{$\myjud{\myprdec{\myse{P}}}{\mytyp}$}
1469 \AxiomC{$\myjud{\mytmt}{\mybool}$}
1470 \AxiomC{$\myjud{\mytya}{\mytyp}$}
1471 \AxiomC{$\myjud{\mytyb}{\mytyp}$}
1472 \TrinaryInfC{$\myjud{\myITE{\mytmt}{\mytya}{\mytyb}}{\mytyp}$}
1477 \mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
1478 \begin{tabular}{ccc}
1479 \AxiomC{\phantom{$\myjud{\myse{P}}{\myprop}$}}
1480 \UnaryInfC{$\myjud{\mytop}{\myprop}$}
1482 \UnaryInfC{$\myjud{\mybot}{\myprop}$}
1485 \AxiomC{$\myjud{\myse{P}}{\myprop}$}
1486 \AxiomC{$\myjud{\myse{Q}}{\myprop}$}
1487 \BinaryInfC{$\myjud{\myse{P} \myand \myse{Q}}{\myprop}$}
1489 \UnaryInfC{\phantom{$\myjud{\mybot}{\myprop}$}}
1492 \AxiomC{$\myjud{\myse{A}}{\mytyp}$}
1493 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\myse{P}}{\myprop}$}
1494 \BinaryInfC{$\myjud{\myprfora{\myb{x}}{\mytya}{\myse{P}}}{\myprop}$}
1496 \UnaryInfC{\phantom{$\myjud{\mybot}{\myprop}$}}
1501 Our foundation will be a type theory like the one of section
1502 \ref{sec:itt}, with only one level: $\mytyp_0$. In this context we will
1503 drop the $0$ and call $\mytyp_0$ $\mytyp$. Moreover, since the old
1504 $\myfun{if}\myarg\myfun{then}\myarg\myfun{else}$ was able to return
1505 types thanks to the hierarchy (which is gone), we need to reintroduce an
1506 ad-hoc conditional for types, where the reduction rule is the obvious
1509 However, we have an addition: a universe of \emph{propositions},
1510 $\myprop$. $\myprop$ isolates a fragment of types at large, and
1511 indeed we can `inject' any $\myprop$ back in $\mytyp$ with $\myprdec{\myarg}$: \\
1512 \mydesc{proposition decoding:}{\myprdec{\mytmsyn} \myred \mytmsyn}{
1515 \begin{array}{l@{\ }c@{\ }l}
1516 \myprdec{\mybot} & \myred & \myempty \\
1517 \myprdec{\mytop} & \myred & \myunit
1522 \begin{array}{r@{ }c@{ }l@{\ }c@{\ }l}
1523 \myprdec{&\myse{P} \myand \myse{Q} &} & \myred & \myprdec{\myse{P}} \myprod \myprdec{\myse{Q}} \\
1524 \myprdec{&\myprfora{\myb{x}}{\mytya}{\myse{P}} &} & \myred &
1525 \myfora{\myb{x}}{\mytya}{\myprdec{\myse{P}}}
1530 Propositions are what we call the types of \emph{proofs}, or types
1531 whose inhabitants contain no `data', much like $\myunit$. The goal of
1532 doing this is twofold: erasing all top-level propositions when
1533 compiling; and to identify all equivalent propositions as the same, as
1536 Why did we choose what we have in $\myprop$? Given the above
1537 criteria, $\mytop$ obviously fits the bill. A pair of propositions
1538 $\myse{P} \myand \myse{Q}$ still won't get us data. Finally, if
1539 $\myse{P}$ is a proposition and we have
1540 $\myprfora{\myb{x}}{\mytya}{\myse{P}}$ , the decoding will be a
1541 function which returns propositional content. The only threat is
1542 $\mybot$, by which we can fabricate anything we want: however if we
1543 are consistent there will be nothing of type $\mybot$ at the top
1544 level, which is what we care about regarding proof erasure.
1546 \subsection{Equality proofs}
1550 \begin{array}{r@{\ }c@{\ }l}
1551 \mytmsyn & ::= & \cdots \mysynsep
1552 \mycoee{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \mysynsep
1553 \mycohh{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
1554 \myprsyn & ::= & \cdots \mysynsep \mytmsyn \myeq \mytmsyn \mysynsep
1555 \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn}
1560 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1562 \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
1563 \AxiomC{$\myjud{\mytmt}{\mytya}$}
1564 \BinaryInfC{$\myjud{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}$}
1567 \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
1568 \AxiomC{$\myjud{\mytmt}{\mytya}$}
1569 \BinaryInfC{$\myjud{\mycohh{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\myprdec{\myjm{\mytmt}{\mytya}{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}}}$}
1575 \mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
1580 \myjud{\myse{A}}{\mytyp} \hspace{1cm} \myjud{\myse{B}}{\mytyp}
1583 \UnaryInfC{$\myjud{\mytya \myeq \mytyb}{\myprop}$}
1588 \myjud{\myse{A}}{\mytyp} \hspace{1cm} \myjud{\mytmm}{\myse{A}} \\
1589 \myjud{\myse{B}}{\mytyp} \hspace{1cm} \myjud{\mytmn}{\myse{B}}
1592 \UnaryInfC{$\myjud{\myjm{\mytmm}{\myse{A}}{\mytmn}{\myse{B}}}{\myprop}$}
1599 While isolating a propositional universe as presented can be a useful
1600 exercises on its own, what we are really after is a useful notion of
1601 equality. In OTT we want to maintain the notion that things judged to
1602 be equal are still always repleaceable for one another with no
1603 additional changes. Note that this is not the same as saying that they
1604 are definitionally equal, since as we saw extensionally equal functions,
1605 while satisfying the above requirement, are not definitionally equal.
1607 Towards this goal we introduce two equality constructs in
1608 $\myprop$---the fact that they are in $\myprop$ indicates that they
1609 indeed have no computational content. The first construct, $\myarg
1610 \myeq \myarg$, relates types, the second,
1611 $\myjm{\myarg}{\myarg}{\myarg}{\myarg}$, relates values. The
1612 value-level equality is different from our old propositional equality:
1613 instead of ranging over only one type, we might form equalities between
1614 values of different types---the usefulness of this construct will be
1615 clear soon. In the literature this equality is known as `heterogeneous'
1616 or `John Major', since
1619 John Major's `classless society' widened people's aspirations to
1620 equality, but also the gap between rich and poor. After all, aspiring
1621 to be equal to others than oneself is the politics of envy. In much
1622 the same way, forms equations between members of any type, but they
1623 cannot be treated as equals (ie substituted) unless they are of the
1624 same type. Just as before, each thing is only equal to
1625 itself. \citep{McBride1999}.
1628 Correspondingly, at the term level, $\myfun{coe}$ (`coerce') lets us
1629 transport values between equal types; and $\myfun{coh}$ (`coherence')
1630 guarantees that $\myfun{coe}$ respects the value-level equality, or in
1631 other words that it really has no computational component: if we
1632 transport $\mytmm : \mytya$ to $\mytmn : \mytyb$, $\mytmm$ and $\mytmn$
1633 will still be the same.
1635 Before introducing the core ideas that make OTT work, let us distinguish
1636 between \emph{canonical} and \emph{neutral} types. Canonical types are
1637 those arising from the ground types ($\myempty$, $\myunit$, $\mybool$)
1638 and the three type formers ($\myarr$, $\myprod$, $\mytyc{W}$). Neutral
1639 types are those formed by
1640 $\myfun{If}\myarg\myfun{Then}\myarg\myfun{Else}\myarg$.
1641 Correspondingly, canonical terms are those inhabiting canonical types
1642 ($\mytt$, $\mytrue$, $\myfalse$, $\myabss{\myb{x}}{\mytya}{\mytmt}$,
1643 ...), and neutral terms those formed by eliminators\footnote{Using the
1644 terminology from section \ref{sec:types}, we'd say that canonical
1645 terms are in \emph{weak head normal form}.}. In the current system
1646 (and hopefully in well-behaved systems), all closed terms reduce to a
1647 canonical term, and all canonical types are inhabited by canonical
1650 \subsubsection{Type equality, and coercions}
1652 The plan is to decompose type-level equalities between canonical types
1653 into decodable propositions containing equalities regarding the
1654 subterms, and to use coerce recursively on the subterms using the
1655 generated equalities. This interplay between type equalities and
1656 \myfun{coe} ensures that invocations of $\myfun{coe}$ will vanish when
1657 we have evidence of the structural equality of the types we are
1658 transporting terms across. If the type is neutral, the equality won't
1659 reduce and thus $\myfun{coe}$ won't reduce either. If we come an
1660 equality between different canonical types, then we reduce the equality
1661 to bottom, making sure that no such proof can exist, and providing an
1662 `escape hatch' in $\myfun{coe}$.
1666 \mydesc{equality reduction:}{\myprsyn \myred \myprsyn}{
1668 \begin{array}{c@{\ }c@{\ }c@{\ }l}
1669 \myempty & \myeq & \myempty & \myred \mytop \\
1670 \myunit & \myeq & \myunit & \myred \mytop \\
1671 \mybool & \myeq & \mybool & \myred \mytop \\
1672 \myexi{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myexi{\myb{x_2}}{\mytya_2}{\mytya_2} & \myred \\
1674 \myind{2} \mytya_1 \myeq \mytyb_1 \myand
1675 \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}]}
1677 \myfora{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myfora{\myb{x_2}}{\mytya_2}{\mytyb_2} & \myred \cdots \\
1678 \myw{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myw{\myb{x_2}}{\mytya_2}{\mytyb_2} & \myred \cdots \\
1679 \mytya & \myeq & \mytyb & \myred \mybot\ \text{if $\mytya$ and $\mytyb$ are canonical.}
1684 \mydesc{reduction}{\mytmsyn \myred \mytmsyn}{
1686 \begin{array}[t]{@{}l@{\ }l@{\ }l@{\ }l@{\ }l@{\ }c@{\ }l@{\ }}
1687 \mycoe & \myempty & \myempty & \myse{Q} & \myse{t} & \myred & \myse{t} \\
1688 \mycoe & \myunit & \myunit & \myse{Q} & \mytt & \myred & \mytt \\
1689 \mycoe & \mybool & \mybool & \myse{Q} & \mytrue & \myred & \mytrue \\
1690 \mycoe & \mybool & \mybool & \myse{Q} & \myfalse & \myred & \myfalse \\
1691 \mycoe & (\myexi{\myb{x_1}}{\mytya_1}{\mytyb_1}) &
1692 (\myexi{\myb{x_2}}{\mytya_2}{\mytyb_2}) & \myse{Q} &
1693 \mytmt_1 & \myred & \\
1695 \myind{2}\begin{array}[t]{l@{\ }l@{\ }c@{\ }l}
1696 \mysyn{let} & \myb{\mytmm_1} & \mapsto & \myapp{\myfst}{\mytmt_1} : \mytya_1 \\
1697 & \myb{\mytmn_1} & \mapsto & \myapp{\mysnd}{\mytmt_1} : \mysub{\mytyb_1}{\myb{x_1}}{\myb{\mytmm_1}} \\
1698 & \myb{Q_A} & \mapsto & \myapp{\myfst}{\myse{Q}} : \mytya_1 \myeq \mytya_2 \\
1699 & \myb{\mytmm_2} & \mapsto & \mycoee{\mytya_1}{\mytya_2}{\myb{Q_A}}{\myb{\mytmm_1}} : \mytya_2 \\
1700 & \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}}} \\
1701 & \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}} \\
1702 \mysyn{in} & \multicolumn{3}{@{}l}{\mypair{\myb{\mytmm_2}}{\myb{\mytmn_2}}}
1705 \mycoe & (\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}) &
1706 (\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}) & \myse{Q} &
1710 \mycoe & (\myw{\myb{x_1}}{\mytya_1}{\mytyb_1}) &
1711 (\myw{\myb{x_2}}{\mytya_2}{\mytyb_2}) & \myse{Q} &
1715 \mycoe & \mytya & \mytyb & \myse{Q} & \mytmt & \myred & \\
1717 \myind{2}\myapp{\myabsurd{\mytyb}}{\myse{Q}}\ \text{if $\mytya$ and $\mytyb$ are canonical.}
1722 \caption{Reducing type equalities, and using them when
1723 $\myfun{coe}$rcing.}
1727 Figure \ref{fig:eqred} illustrates this idea in practice. For ground
1728 types, the proof is the trivial element, and \myfun{coe} is the
1729 identity. For the three type binders, things are similar but subtly
1730 different---the choices we make in the type equality are dictated by
1731 the desire of writing the $\myfun{coe}$ in a natural way.
1733 $\myprod$ is the easiest case: we decompose the proof into proofs that
1734 the first element's types are equal ($\mytya_1 \myeq \mytya_2$), and a
1735 proof that given equal values in the first element, the types of the
1736 second elements are equal too
1737 ($\myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{\myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2}}
1738 \myimpl \mytyb_1 \myeq \mytyb_2}$)\footnote{We are using $\myimpl$ to
1739 indicate a $\forall$ where we discard the first value. We write
1740 $\mytyb_1[\myb{x_1}]$ to indicate that the $\myb{x_1}$ in $\mytyb_1$
1741 is re-bound to the $\myb{x_1}$ quantified by the $\forall$, and
1742 similarly for $\myb{x_2}$ and $\mytyb_2$.}. This also explains the
1743 need for heterogeneous equality, since in the second proof it would be
1744 awkward to express the fact that $\myb{A_1}$ is the same as $\myb{A_2}$.
1745 In the respective $\myfun{coe}$ case, since the types are canonical, we
1746 know at this point that the proof of equality is a pair of the shape
1747 described above. Thus, we can immediately coerce the first element of
1748 the pair using the first element of the proof, and then instantiate the
1749 second element with the two first elements and a proof by coherence of
1750 their equality, since we know that the types are equal. The cases for
1751 the other binders are omitted for brevity, but they follow the same
1754 \subsubsection{$\myfun{coe}$, laziness, and $\myfun{coh}$erence}
1756 It is important to notice that in the reduction rules for $\myfun{coe}$
1757 are never obstructed by the proofs: with the exception of comparisons
1758 between different canonical types we never pattern match on the pairs,
1759 but always look at the projections. This means that, as long as we are
1760 consistent, and thus as long as we don't have $\mybot$-inducing proofs,
1761 we can add propositional axioms for equality and $\myfun{coe}$ will
1762 still compute. Thus, we can take $\myfun{coh}$ as axiomatic, and we can
1763 add back familiar useful equality rules:
1765 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1767 \AxiomC{$\myjud{\mytmt}{\mytya}$}
1768 \UnaryInfC{$\myjud{\myapp{\myrefl}{\mytmt}}{\myprdec{\myjm{\myb{x}}{\myb{\mytya}}{\myb{x}}{\myb{\mytya}}}}$}
1771 \AxiomC{$\myjud{\mytya}{\mytyp}$}
1772 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytyb}{\mytyp}$}
1773 \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}}}}}$}
1778 $\myrefl$ is the equivalent of the reflexivity rule in propositional
1779 equality, and $\mytyc{R}$ asserts that if we have a we have a $\mytyp$
1780 abstracting over a value we can substitute equal for equal---this lets
1781 us recover $\myfun{subst}$. Note that while we need to provide ad-hoc
1782 rules in the restricted, non-hierarchical theory that we have, if our
1783 theory supports abstraction over $\mytyp$s we can easily add these
1784 axioms as abstracted variables.
1786 \subsubsection{Value-level equality}
1788 \mydesc{equality reduction:}{\myprsyn \myred \myprsyn}{
1790 \begin{array}{r@{ }c@{\ }c@{\ }c@{}l@{\ }c@{\ }r@{}c@{\ }c@{\ }c@{}l@{\ }l}
1791 (&\mytmt_1 & : & \myempty&) & \myeq & (&\mytmt_2 & : & \myempty &) & \myred \mytop \\
1792 (&\mytmt_1 & : & \myempty&) & \myeq & (&\mytmt_2 & : & \myempty&) & \myred \mytop \\
1793 (&\mytrue & : & \mybool&) & \myeq & (&\mytrue & : & \mybool&) & \myred \mytop \\
1794 (&\myfalse & : & \mybool&) & \myeq & (&\myfalse & : & \mybool&) & \myred \mytop \\
1795 (&\mytmt_1 & : & \mybool&) & \myeq & (&\mytmt_1 & : & \mybool&) & \myred \mybot \\
1796 (&\mytmt_1 & : & \myexi{\mytya_1}{\myb{x_1}}{\mytyb_1}&) & \myeq & (&\mytmt_2 & : & \myexi{\mytya_2}{\myb{x_2}}{\mytyb_2}&) & \myred \\
1797 & \multicolumn{11}{@{}l}{
1798 \myind{2} \myjm{\myapp{\myfst}{\mytmt_1}}{\mytya_1}{\myapp{\myfst}{\mytmt_2}}{\mytya_2} \myand
1799 \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}}}
1801 (&\myse{f}_1 & : & \myfora{\mytya_1}{\myb{x_1}}{\mytyb_1}&) & \myeq & (&\myse{f}_2 & : & \myfora{\mytya_2}{\myb{x_2}}{\mytyb_2}&) & \myred \\
1802 & \multicolumn{11}{@{}l}{
1803 \myind{2} \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{
1804 \myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2} \myimpl
1805 \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}]}
1808 (&\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 \\
1809 (&\mytmt_1 & : & \mytya_1&) & \myeq & (&\mytmt_2 & : & \mytya_2 &) & \myred \\
1810 & \multicolumn{11}{@{}l}{
1811 \myind{2} \mybot\ \text{if $\mytya_1$ and $\mytya_2$ are canonical.}
1817 As with type-level equality, we want value-level equality to reduce
1818 based on the structure of the compared terms.
1820 \subsection{Proof irrelevance}
1822 % \section{Augmenting ITT}
1823 % \label{sec:practical}
1825 % \subsection{A more liberal hierarchy}
1827 % \subsection{Type inference}
1829 % \subsubsection{Bidirectional type checking}
1831 % \subsubsection{Pattern unification}
1833 % \subsection{Pattern matching and explicit fixpoints}
1835 % \subsection{Induction-recursion}
1837 % \subsection{Coinduction}
1839 % \subsection{Dealing with partiality}
1841 % \subsection{Type holes}
1843 \section{\mykant : the theory}
1844 \label{sec:kant-theory}
1846 \mykant\ is an interactive theorem prover developed as part of this thesis.
1847 The plan is to present a core language which would be capable of serving as
1848 the basis for a more featureful system, while still presenting interesting
1849 features and more importantly observational equality.
1851 The author learnt the hard way the implementations challenges for such a
1852 project, and while there is a solid and working base to work on, observational
1853 equality is not currently implemented. However, a detailed plan on how to add
1854 it this functionality is provided, and should not prove to be too much work.
1856 The features currently implemented in \mykant\ are:
1859 \item[Full dependent types] As we would expect, we have dependent a system
1860 which is as expressive as the `best' corner in the lambda cube described in
1861 section \ref{sec:itt}.
1863 \item[Implicit, cumulative universe hierarchy] The user does not need to
1864 specify universe level explicitly, and universes are \emph{cumulative}.
1866 \item[User defined data types and records] Instead of forcing the user to
1867 choose from a restricted toolbox, we let her define inductive data types,
1868 with associated primitive recursion operators; or records, with associated
1869 projections for each field.
1871 \item[Bidirectional type checking] While no `fancy' inference via unification
1872 is present, we take advantage of an type synthesis system in the style of
1873 \cite{Pierce2000}, extending the concept for user defined data types.
1875 \item[Type holes] When building up programs interactively, it is useful to
1876 leave parts unfinished while exploring the current context. This is what
1880 The planned features are:
1883 \item[Observational equality] As described in section \ref{sec:ott} but
1884 extended to work with the type hierarchy and to admit equality between
1885 arbitrary data types.
1887 \item[Coinductive data] ...
1890 We will analyse the features one by one, along with motivations and tradeoffs
1891 for the design decisions made.
1893 \subsection{Bidirectional type checking}
1895 We start by describing bidirectional type checking since it calls for fairly
1896 different typing rules that what we have seen up to now. The idea is to have
1897 two kind of terms: terms for which a type can always be inferred, and terms
1898 that need to be checked against a type. A nice observation is that this
1899 duality runs through the semantics of the terms: data destructors (function
1900 application, record projections, primitive re cursors) \emph{infer} types,
1901 while data constructors (abstractions, record/data types data constructors)
1902 need to be checked. In the literature these terms are respectively known as
1904 To introduce the concept and notation, we will revisit the STLC in a
1905 bidirectional style. The presentation follows \cite{Loh2010}.
1907 % TODO do this --- is it even necessary
1911 \subsection{Base terms and types}
1913 Let us begin by describing the primitives available without the user
1914 defining any data types, and without equality. The way we handle
1915 variables and substitution is left unspecified, and explained in section
1916 \ref{sec:term-repr}, along with other implementation issues. We are
1917 also going to give an account of the implicit type hierarchy separately
1918 in section \ref{sec:term-hierarchy}, so as not to clutter derivation
1919 rules too much, and just treat types as impredicative for the time
1924 \begin{array}{r@{\ }c@{\ }l}
1925 \mytmsyn & ::= & \mynamesyn \mysynsep \mytyp \\
1926 & | & \myfora{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
1927 \myabs{\myb{x}}{\mytmsyn} \mysynsep
1928 (\myapp{\mytmsyn}{\mytmsyn}) \mysynsep
1929 (\myann{\mytmsyn}{\mytmsyn}) \\
1930 \mynamesyn & ::= & \myb{x} \mysynsep \myfun{f}
1935 The syntax for our calculus includes just two basic constructs:
1936 abstractions and $\mytyp$s. Everything else will be provided by
1937 user-definable constructs. Since we let the user define values, we will
1938 need a context capable of carrying the body of variables along with
1939 their type. Bound names and defined names are treated separately in the
1940 syntax, and while both can be associated to a type in the context, only
1941 defined names can be associated with a body:
1943 \mydesc{context validity:}{\myvalid{\myctx}}{
1944 \begin{tabular}{ccc}
1945 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
1946 \UnaryInfC{$\myvalid{\myemptyctx}$}
1949 \AxiomC{$\myjud{\mytya}{\mytyp}$}
1950 \AxiomC{$\mynamesyn \not\in \myctx$}
1951 \BinaryInfC{$\myvalid{\myctx ; \mynamesyn : \mytya}$}
1954 \AxiomC{$\myjud{\mytmt}{\mytya}$}
1955 \AxiomC{$\myfun{f} \not\in \myctx$}
1956 \BinaryInfC{$\myvalid{\myctx ; \myfun{f} \mapsto \mytmt : \mytya}$}
1961 Now we can present the reduction rules, which are unsurprising. We have
1962 the usual function application ($\beta$-reduction), but also a rule to
1963 replace names with their bodies ($\delta$-reduction), and one to discard
1964 type annotations. For this reason reduction is done in-context, as
1965 opposed to what we have seen in the past:
1967 \mydesc{reduction:}{\myctx \vdash \mytmsyn \myred \mytmsyn}{
1968 \begin{tabular}{ccc}
1969 \AxiomC{\phantom{$\myb{x} \mapsto \mytmt : \mytya \in \myctx$}}
1970 \UnaryInfC{$\myctx \vdash \myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn}
1971 \myred \mysub{\mytmm}{\myb{x}}{\mytmn}$}
1974 \AxiomC{$\myfun{f} \mapsto \mytmt : \mytya \in \myctx$}
1975 \UnaryInfC{$\myctx \vdash \myfun{f} \myred \mytmt$}
1978 \AxiomC{\phantom{$\myb{x} \mapsto \mytmt : \mytya \in \myctx$}}
1979 \UnaryInfC{$\myctx \vdash \myann{\mytmm}{\mytya} \myred \mytmm$}
1984 We can now give types to our terms. The type of names, both defined and
1985 abstract, is inferred. The type of applications is inferred too,
1986 propagating types down the applied term. Abstractions are checked.
1987 Finally, we have a rule to check the type of an inferrable term. We
1988 defer the question of term equality (which is needed for type checking)
1989 to section \label{sec:kant-irr}.
1991 \mydesc{typing:}{\myctx \vdash \mytmsyn \Leftrightarrow \mytmsyn}{
1992 \begin{tabular}{ccc}
1993 \AxiomC{$\myse{name} : A \in \myctx$}
1994 \UnaryInfC{$\myinf{\myse{name}}{A}$}
1997 \AxiomC{$\myfun{f} \mapsto \mytmt : A \in \myctx$}
1998 \UnaryInfC{$\myinf{\myfun{f}}{A}$}
2001 \AxiomC{$\myinf{\mytmt}{\mytya}$}
2002 \UnaryInfC{$\mychk{\myann{\mytmt}{\mytya}}{\mytya}$}
2007 \begin{tabular}{ccc}
2008 \AxiomC{$\myinf{\mytmm}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
2009 \AxiomC{$\mychk{\mytmn}{\mytya}$}
2010 \BinaryInfC{$\myinf{\myapp{\mytmm}{\mytmn}}{\mysub{\mytyb}{\myb{x}}{\mytmn}}$}
2015 \AxiomC{$\mychkk{\myctx; \myb{x}: \mytya}{\mytmt}{\mytyb}$}
2016 \UnaryInfC{$\mychk{\myabs{\myb{x}}{\mytmt}}{\myfora{\myb{x}}{\mytyb}{\mytyb}}$}
2021 \subsection{Elaboration}
2023 As we mentioned, $\mykant$\ allows the user to define not only values
2024 but also custom data types and records. \emph{Elaboration} consists of
2025 turning these declarations into workable syntax, types, and reduction
2026 rules. The treatment of custom types in $\mykant$\ is heavily inspired
2027 by McBride and McKinna early work on Epigram \citep{McBride2004},
2028 although with some differences.
2030 \subsubsection{Term vectors, telescopes, and assorted notation}
2032 We use a vector notation to refer to a series of term applied to
2033 another, for example $\mytyc{D} \myappsp \vec{A}$ is a shorthand for
2034 $\mytyc{D} \myappsp \mytya_1 \cdots \mytya_n$, for some $n$. $n$ is
2035 consistently used to refer to the length of such vectors, and $i$ to
2036 refer to an index in such vectors. We also often need to `build up'
2037 terms vectors, in which case we use $\myemptyctx$ for an empty vector
2038 and add elements to an existing vector with $\myarg ; \myarg$, similarly
2039 to what we do for context.
2041 To present the elaboration and operations on user defined data types, we
2042 frequently make use what de Bruijn called \emph{telescopes}
2043 \citep{Bruijn91}, a construct that will prove useful when dealing with
2044 the types of type and data constructors. A telescope is a series of
2045 nested typed bindings, such as $(\myb{x} {:} \mynat); (\myb{p} {:}
2046 \myapp{\myfun{even}}{\myb{x}})$. Consistently with the notation for
2047 contexts and term vectors, we use $\myemptyctx$ to denote an empty
2048 telescope and $\myarg ; \myarg$ to add a new binding to an existing
2051 We refer to telescopes with $\mytele$, $\mytele'$, $\mytele_i$, etc. If
2052 $\mytele$ refers to a telescope, $\mytelee$ refers to the term vector
2053 made up of all the variables bound by $\mytele$. $\mytele \myarr
2054 \mytya$ refers to the type made by turning the telescope into a series
2055 of $\myarr$. Returning to the examples above, we have that
2057 (\myb{x} {:} \mynat); (\myb{p} : \myapp{\myfun{even}}{\myb{x}}) \myarr \mynat =
2058 (\myb{x} {:} \mynat) \myarr (\myb{p} : \myapp{\myfun{even}}{\myb{x}}) \myarr \mynat
2061 We make use of various operations to manipulate telescopes:
2063 \item $\myhead(\mytele)$ refers to the first type appearing in
2064 $\mytele$: $\myhead((\myb{x} {:} \mynat); (\myb{p} :
2065 \myapp{\myfun{even}}{\myb{x}})) = \mynat$. Similarly,
2066 $\myix_i(\mytele)$ refers to the $i^{th}$ type in a telescope
2068 \item $\mytake_i(\mytele)$ refers to the telescope created by taking the
2069 first $i$ elements of $\mytele$: $\mytake_1((\myb{x} {:} \mynat); (\myb{p} :
2070 \myapp{\myfun{even}}{\myb{x}})) = (\myb{x} {:} \mynat)$
2071 \item $\mytele \vec{A}$ refers to the telescope made by `applying' the
2072 terms in $\vec{A}$ on $\mytele$: $((\myb{x} {:} \mynat); (\myb{p} :
2073 \myapp{\myfun{even}}{\myb{x}}))42 = (\myb{p} :
2074 \myapp{\myfun{even}}{42})$.
2077 \subsubsection{Declarations syntax}
2081 \begin{array}{r@{\ }c@{\ }l}
2082 \mydeclsyn & ::= & \myval{\myb{x}}{\mytmsyn}{\mytmsyn} \\
2083 & | & \mypost{\myb{x}}{\mytmsyn} \\
2084 & | & \myadt{\mytyc{D}}{\mytelesyn}{}{\mydc{c} : \mytelesyn\ |\ \cdots } \\
2085 & | & \myreco{\mytyc{D}}{\mytelesyn}{}{\myfun{f} : \mytmsyn,\ \cdots } \\
2087 \mytelesyn & ::= & \myemptytele \mysynsep \mytelesyn \mycc (\myb{x} {:} \mytmsyn) \\
2088 \mynamesyn & ::= & \cdots \mysynsep \mytyc{D} \mysynsep \mytyc{D}.\mydc{c} \mysynsep \mytyc{D}.\myfun{f}
2093 In \mykant\ we have four kind of declarations:
2096 \item[Defined value] A variable, together with a type and a body.
2097 \item[Abstract variable] An abstract variable, with a type but no body.
2098 \item[Inductive data] A datatype, with a type constructor and various data
2099 constructors---somewhat similar to what we find in Haskell. A primitive
2100 recursor (or `destructor') will be generated automatically.
2101 \item[Record] A record, which consists of one data constructor and various
2102 fields, with no recursive occurrences.
2105 Elaborating defined variables consists of type checking body against the
2106 given type, and updating the context to contain the new binding.
2107 Elaborating abstract variables and abstract variables consists of type
2108 checking the type, and updating the context with a new typed variable:
2110 \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
2112 \AxiomC{$\myjud{\mytmt}{\mytya}$}
2113 \AxiomC{$\myfun{f} \not\in \myctx$}
2115 $\myctx \myelabt \myval{\myfun{f}}{\mytya}{\mytmt} \ \ \myelabf\ \ \myctx; \myfun{f} \mapsto \mytmt : \mytya$
2119 \AxiomC{$\myjud{\mytya}{\mytyp}$}
2120 \AxiomC{$\myfun{f} \not\in \myctx$}
2123 \myctx \myelabt \mypost{\myfun{f}}{\mytya}
2124 \ \ \myelabf\ \ \myctx; \myfun{f} : \mytya
2131 \subsubsection{User defined types}
2132 \label{sec:user-type}
2134 Elaborating user defined types is the real effort. First, let's explain
2135 what we can defined, with some examples.
2138 \item[Natural numbers] To define natural numbers, we create a data type
2139 with two constructors: one with zero arguments ($\mydc{zero}$) and one
2140 with one recursive argument ($\mydc{suc}$):
2143 \myadt{\mynat}{ }{ }{
2144 \mydc{zero} \mydcsep \mydc{suc} \myappsp \mynat
2148 This is very similar to what we would write in Haskell:
2149 {\small\[\text{\texttt{data Nat = Zero | Suc Nat}}\]}
2150 Once the data type is defined, $\mykant$\ will generate syntactic
2151 constructs for the type and data constructors, so that we will have
2154 \begin{tabular}{ccc}
2155 \AxiomC{\phantom{$\mychk{\mytmt}{\mynat}$}}
2156 \UnaryInfC{$\myinf{\mynat}{\mytyp}$}
2159 \AxiomC{\phantom{$\mychk{\mytmt}{\mynat}$}}
2160 \UnaryInfC{$\myinf{\mytyc{\mynat}.\mydc{zero}}{\mynat}$}
2163 \AxiomC{$\mychk{\mytmt}{\mynat}$}
2164 \UnaryInfC{$\myinf{\mytyc{\mynat}.\mydc{suc} \myappsp \mytmt}{\mynat}$}
2168 While in Haskell (or indeed in Agda or Coq) data constructors are
2169 treated the same way as functions, in $\mykant$\ they are syntax, so
2170 for example using $\mytyc{\mynat}.\mydc{suc}$ on its own will be a
2171 syntax error. This is necessary so that we can easily infer the type
2172 of polymorphic data constructors, as we will see later.
2174 Moreover, each data constructor is prefixed by the type constructor
2175 name, since we need to retrieve the type constructor of a data
2176 constructor when type checking. This measure aids in the presentation
2177 of various features but it is not needed in the implementation, where
2178 we can have a dictionary to lookup the type constructor corresponding
2179 to each data constructor. When using data constructors in examples I
2180 will omit the type constructor prefix for brevity.
2182 Along with user defined constructors, $\mykant$\ automatically
2183 generates an \emph{eliminator}, or \emph{destructor}, to compute with
2184 natural numbers: If we have $\mytmt : \mynat$, we can destruct
2185 $\mytmt$ using the generated eliminator `$\mynat.\myfun{elim}$':
2188 \AxiomC{$\mychk{\mytmt}{\mynat}$}
2190 \myinf{\mytyc{\mynat}.\myfun{elim} \myappsp \mytmt}{
2192 \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}}
2196 $\mynat.\myfun{elim}$ corresponds to the induction principle for
2197 natural numbers: if we have a predicate on numbers ($\myb{P}$), and we
2198 know that predicate holds for the base case
2199 ($\myapp{\myb{P}}{\mydc{zero}}$) and for each inductive step
2200 ($\myfora{\myb{x}}{\mynat}{\myapp{\myb{P}}{\myb{x}} \myarr
2201 \myapp{\myb{P}}{(\myapp{\mydc{suc}}{\myb{x}})}}$), then $\myb{P}$
2202 holds for any number. As with the data constructors, we require the
2203 eliminator to be applied to the `destructed' element.
2205 While the induction principle is usually seen as a mean to prove
2206 properties about numbers, in the intuitionistic setting it is also a
2207 mean to compute. In this specific case we will $\mynat.\myfun{elim}$
2208 will return the base case if the provided number is $\mydc{zero}$, and
2209 recursively apply the inductive step if the number is a
2212 \begin{array}{@{}l@{}l}
2213 \mytyc{\mynat}.\myfun{elim} \myappsp \mydc{zero} & \myappsp \myse{P} \myappsp \myse{pz} \myappsp \myse{ps} \myred \myse{pz} \\
2214 \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})
2217 The Haskell equivalent would be
2220 \text{\texttt{elim :: Nat -> a -> (Nat -> a -> a) -> a}}\\
2221 \text{\texttt{elim Zero pz ps = pz}}\\
2222 \text{\texttt{elim (Suc n) pz ps = ps n (elim n pz ps)}}
2225 Which buys us the computational behaviour, but not the reasoning power.
2226 % TODO maybe more examples, e.g. Haskell eliminator and fibonacci
2228 \item[Binary trees] Now for a polymorphic data type: binary trees, since
2229 lists are too similar to natural numbers to be interesting.
2232 \myadt{\mytree}{\myappsp (\myb{A} {:} \mytyp)}{ }{
2233 \mydc{leaf} \mydcsep \mydc{node} \myappsp (\myapp{\mytree}{\myb{A}}) \myappsp \myb{A} \myappsp (\myapp{\mytree}{\myb{A}})
2237 Now the purpose of constructors as syntax can be explained: what would
2238 the type of $\mydc{leaf}$ be? If we were to treat it as a `normal'
2239 term, we would have to specify the type parameter of the tree each
2240 time the constructor is applied:
2242 \begin{array}{@{}l@{\ }l}
2243 \mydc{leaf} & : \myfora{\myb{A}}{\mytyp}{\myapp{\mytree}{\myb{A}}} \\
2244 \mydc{node} & : \myfora{\myb{A}}{\mytyp}{\myapp{\mytree}{\myb{A}} \myarr \myb{A} \myarr \myapp{\mytree}{\myb{A}} \myarr \myapp{\mytree}{\myb{A}}}
2247 The problem with this approach is that creating terms is incredibly
2248 verbose and dull, since we would need to specify the type parameters
2249 each time. For example if we wished to create a $\mytree \myappsp
2250 \mynat$ with two nodes and three leaves, we would have to write
2252 \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)
2254 The redundancy of $\mynat$s is quite irritating. Instead, if we treat
2255 constructors as syntactic elements, we can `extract' the type of the
2256 parameter from the type that the term gets checked against, much like
2257 we get the type of abstraction arguments:
2261 \AxiomC{$\mychk{\mytya}{\mytyp}$}
2262 \UnaryInfC{$\mychk{\mydc{leaf}}{\myapp{\mytree}{\mytya}}$}
2265 \AxiomC{$\mychk{\mytmm}{\mytree \myappsp \mytya}$}
2266 \AxiomC{$\mychk{\mytmt}{\mytya}$}
2267 \AxiomC{$\mychk{\mytmm}{\mytree \myappsp \mytya}$}
2268 \TrinaryInfC{$\mychk{\mydc{node} \myappsp \mytmm \myappsp \mytmt \myappsp \mytmn}{\mytree \myappsp \mytya}$}
2272 Which enables us to write, much more concisely
2274 \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}
2276 We gain an annotation, but we lose the myriad of types applied to the
2277 constructors. Conversely, with the eliminator for $\mytree$, we can
2278 infer the type of the arguments given the type of the destructed:
2281 \AxiomC{$\myinf{\mytmt}{\myapp{\mytree}{\mytya}}$}
2283 \myinf{\mytree.\myfun{elim} \myappsp \mytmt}{
2285 (\myb{P} {:} \myapp{\mytree}{\mytya} \myarr \mytyp) \myarr \\
2286 \myapp{\myb{P}}{\mydc{leaf}} \myarr \\
2287 ((\myb{l} {:} \myapp{\mytree}{\mytya}) (\myb{x} {:} \mytya) (\myb{r} {:} \myapp{\mytree}{\mytya}) \myarr \myapp{\myb{P}}{\myb{l}} \myarr
2288 \myapp{\myb{P}}{\myb{r}} \myarr \myb{P} \myappsp (\mydc{node} \myappsp \myb{l} \myappsp \myb{x} \myappsp \myb{r})) \myarr \\
2289 \myapp{\myb{P}}{\mytmt}
2294 As expected, the eliminator embodies structural induction on trees.
2296 \item[Empty type] We have presented types that have at least one
2297 constructors, but nothing prevents us from defining types with
2298 \emph{no} constructors:
2300 \myadt{\mytyc{Empty}}{ }{ }{ }
2302 What shall the `induction principle' on $\mytyc{Empty}$ be? Does it
2303 even make sense to talk about induction on $\mytyc{Empty}$?
2304 $\mykant$\ does not care, and generates an eliminator with no `cases',
2305 and thus corresponding to the $\myfun{absurd}$ that we know and love:
2308 \AxiomC{$\myinf{\mytmt}{\mytyc{Empty}}$}
2309 \UnaryInfC{$\myinf{\myempty.\myfun{elim} \myappsp \mytmt}{(\myb{P} {:} \mytmt \myarr \mytyp) \myarr \myapp{\myb{P}}{\mytmt}}$}
2312 \item[Ordered lists] Up to this point, the examples shown are nothing
2313 new to the \{Haskell, SML, OCaml, functional\} programmer. However
2314 dependent types let us express much more than that. A useful example
2315 is the type of ordered lists. There are many ways to define such a
2316 thing, we will define our type to store the bounds of the list, making
2317 sure that $\mydc{cons}$ing respects that.
2319 First, using $\myunit$ and $\myempty$, we define a type expressing the
2320 ordering on natural numbers, $\myfun{le}$---`less or equal'.
2321 $\myfun{le}\myappsp \mytmm \myappsp \mytmn$ will be inhabited only if
2322 $\mytmm \le \mytmn$:
2325 \myfun{le} : \mynat \myarr \mynat \myarr \mytyp \mapsto \\
2326 \myind{2} \myabs{\myb{n}}{\\
2327 \myind{2}\myind{2} \mynat.\myfun{elim} \\
2328 \myind{2}\myind{2}\myind{2} \myb{n} \\
2329 \myind{2}\myind{2}\myind{2} (\myabs{\myarg}{\mynat \myarr \mytyp}) \\
2330 \myind{2}\myind{2}\myind{2} (\myabs{\myarg}{\myunit}) \\
2331 \myind{2}\myind{2}\myind{2} (\myabs{\myb{n}\, \myb{f}\, \myb{m}}{
2332 \mynat.\myfun{elim} \myappsp \myb{m} \myappsp (\myabs{\myarg}{\mytyp}) \myappsp \myempty \myappsp (\myabs{\myb{m'}\, \myarg}{\myapp{\myb{f}}{\myb{m'}}})
2336 \]} We return $\myunit$ if the scrutinised is $\mydc{zero}$ (every
2337 number in less or equal than zero), $\myempty$ if the first number is
2338 a $\mydc{suc}$cessor and the second a $\mydc{zero}$, and we recurse if
2339 they are both successors. Since we want the list to have possibly
2340 `open' bounds, for example for empty lists, we create a type for
2341 `lifted' naturals with a bottom (less than everything) and top
2342 (greater than everything) elements, along with an associated comparison
2346 \myadt{\mytyc{Lift}}{ }{ }{\mydc{bot} \mydcsep \mydc{lift} \myappsp \mynat \mydcsep \mydc{top}}\\
2347 \myfun{le'} : \mytyc{Lift} \myarr \mytyc{Lift} \myarr \mytyp \mapsto \cdots \\
2349 \]} Finally, we can defined a type of ordered lists. The type is
2350 parametrised over two values representing the lower and upper bounds
2351 of the elements, as opposed to the type parameters that we are used
2352 to. Then, an empty list will have to have evidence that the bounds
2353 are ordered, and each time we add an element we require the list to
2354 have a matching lower bound:
2357 \myadt{\mytyc{OList}}{\myappsp (\myb{low}\ \myb{upp} {:} \mytyc{Lift})}{\\ \myind{2}}{
2358 \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 (\myfun{le'} \myappsp \myb{low} \myappsp (\myfun{lift} \myappsp \myb{n})
2361 \]} If we want we can then employ this structure to write and prove
2362 correct various sorting algorithms\footnote{See this presentation by
2364 \url{https://personal.cis.strath.ac.uk/conor.mcbride/Pivotal.pdf},
2365 and this blog post by the author:
2366 \url{http://mazzo.li/posts/AgdaSort.html}.}.
2370 \item[Dependent products] Apart from $\mysyn{data}$, $\mykant$\ offers
2371 us another way to define types: $\mysyn{record}$. A record is a
2372 datatype with one constructor and `projections' to extract specific
2373 fields of the said constructor.
2375 For example, we can recover dependent products:
2378 \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}}}
2381 Here $\myfst$ and $\mysnd$ are the projections, with their respective
2382 types. Note that each field can refer to the preceding fields. A
2383 constructor will be automatically generated, under the name of
2384 $\mytyc{Prod}.\mydc{constr}$. Dually to data types, we will omit the
2385 type constructor prefix for record projections.
2387 Following the bidirectionality of the system, we have that projections
2388 (the destructors of the record) infer the type, while the constructor
2393 \AxiomC{$\mychk{\mytmm}{\mytya}$}
2394 \AxiomC{$\mychk{\mytmn}{\myapp{\mytyb}{\mytmm}}$}
2395 \BinaryInfC{$\mychk{\mytyc{Prod}.\mydc{constr} \myappsp \mytmm \myappsp \mytmn}{\mytyc{Prod} \myappsp \mytya \myappsp \mytyb}$}
2397 \UnaryInfC{\phantom{$\myinf{\myfun{snd} \myappsp \mytmt}{\mytyb \myappsp (\myfst \myappsp \mytmt)}$}}
2400 \AxiomC{$\myinf{\mytmt}{\mytyc{Prod} \myappsp \mytya \myappsp \mytyb}$}
2401 \UnaryInfC{$\myinf{\myfun{fst} \myappsp \mytmt}{\mytya}$}
2403 \UnaryInfC{$\myinf{\myfun{snd} \myappsp \mytmt}{\mytyb \myappsp (\myfst \myappsp \mytmt)}$}
2407 What we have is equivalent to ITT's dependent products.
2411 \begin{subfigure}[b]{\textwidth}
2417 \mynamesyn ::= \cdots \mysynsep \mytyc{D} \mysynsep \mytyc{D}.\mydc{c} \mysynsep \mytyc{D}.\myfun{f}
2422 \mydesc{syntax elaboration:}{\mydeclsyn \myelabf \mytmsyn ::= \cdots}{
2425 \begin{array}{r@{\ }l}
2426 & \myadt{\mytyc{D}}{\mytele}{}{\cdots\ |\ \mydc{c}_n : \mytele_n } \\
2429 \begin{array}{r@{\ }c@{\ }l}
2430 \mytmsyn & ::= & \cdots \mysynsep \myapp{\mytyc{D}}{\mytmsyn^{\mytele}} \mysynsep \cdots \mysynsep
2431 \mytyc{D}.\mydc{c}_n \myappsp \mytmsyn^{\mytele_n} \mysynsep \mytyc{D}.\myfun{elim} \myappsp \mytmsyn \\
2437 \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
2442 \myinf{\mytele \myarr \mytyp}{\mytyp}\hspace{0.8cm}
2443 \mytyc{D} \not\in \myctx \\
2444 \myinff{\myctx;\ \mytyc{D} : \mytele \myarr \mytyp}{\mytele \mycc \mytele_i \myarr \myapp{\mytyc{D}}{\mytelee}}{\mytyp}\ \ \ (1 \leq i \leq n) \\
2445 \text{For each $(\myb{x} {:} \mytya)$ in each $\mytele_i$, if $\mytyc{D} \in \mytya$, then $\mytya = \myapp{\mytyc{D}}{\vec{\mytmt}}$.}
2449 \begin{array}{r@{\ }c@{\ }l}
2450 \myctx & \myelabt & \myadt{\mytyc{D}}{\mytele}{}{ \cdots \ |\ \mydc{c}_n : \mytele_n } \\
2451 & & \vspace{-0.2cm} \\
2452 & \myelabf & \myctx;\ \mytyc{D} : \mytele \myarr \mytyp;\ \cdots;\ \mytyc{D}.\mydc{c}_n : \mytele \mycc \mytele_n \myarr \myapp{\mytyc{D}}{\mytelee}; \\
2454 \begin{array}{@{}r@{\ }l l}
2455 \mytyc{D}.\myfun{elim} : & \mytele \myarr (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr & \textbf{target} \\
2456 & (\myb{P} {:} \myapp{\mytyc{D}}{\mytelee} \myarr \mytyp) \myarr & \textbf{motive} \\
2460 (\mytele_n \mycc \myhyps(\myb{P}, \mytele_n) \myarr \myapp{\myb{P}}{(\myapp{\mytyc{D}.\mydc{c}_n}{\mytelee_n})}) \myarr
2461 \end{array} \right \}
2462 & \textbf{methods} \\
2463 & \myapp{\myb{P}}{\myb{x}} &
2467 \DisplayProof \\ \vspace{0.2cm}\ \\
2469 \begin{array}{@{}l l@{\ } l@{} r c l}
2470 \textbf{where} & \myhyps(\myb{P}, & \myemptytele &) & \mymetagoes & \myemptytele \\
2471 & \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) \\
2472 & \myhyps(\myb{P}, & (\myb{x} {:} \mytya) \mycc \mytele & ) & \mymetagoes & \myhyps(\myb{P}, \mytele)
2478 \mydesc{reduction elaboration:}{\mydeclsyn \myelabf \myctx \vdash \mytmsyn \myred \mytmsyn}{
2480 $\myadt{\mytyc{D}}{\mytele}{}{ \cdots \ |\ \mydc{c}_n : \mytele_n } \ \ \myelabf$
2481 \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
2482 \AxiomC{$\mytyc{D}.\mydc{c}_i : \mytele;\mytele_i \myarr \myapp{\mytyc{D}}{\mytelee} \in \myctx$}
2484 \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)}
2486 \DisplayProof \\ \vspace{0.2cm}\ \\
2488 \begin{array}{@{}l l@{\ } l@{} r c l}
2489 \textbf{where} & \myrecs(\myse{P}, \vec{m}, & \myemptytele &) & \mymetagoes & \myemptytele \\
2490 & \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) \\
2491 & \myrecs(\myse{P}, \vec{m}, & (\myb{x} {:} \mytya); \mytele &) & \mymetagoes & \myrecs(\myse{P}, \vec{m}, \mytele)
2497 \begin{subfigure}[b]{\textwidth}
2498 \mydesc{syntax elaboration:}{\myelab{\mydeclsyn}{\mytmsyn ::= \cdots}}{
2501 \begin{array}{r@{\ }c@{\ }l}
2502 \myctx & \myelabt & \myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \\
2505 \begin{array}{r@{\ }c@{\ }l}
2506 \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 \\
2513 \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
2517 \myinf{\mytele \myarr \mytyp}{\mytyp}\hspace{0.8cm}
2518 \mytyc{D} \not\in \myctx \\
2519 \myinff{\myctx; \mytele; (\myb{f}_j : \myse{F}_j)_{j=1}^{i - 1}}{F_i}{\mytyp} \myind{3} (1 \le i \le n)
2523 \begin{array}{r@{\ }c@{\ }l}
2524 \myctx & \myelabt & \myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \\
2525 & & \vspace{-0.2cm} \\
2526 & \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}; \\
2527 & & \mytyc{D}.\mydc{constr} : \mytele \myarr \myse{F}_1 \myarr \cdots \myarr \myse{F}_n \myarr \myapp{\mytyc{D}}{\mytelee};
2533 \mydesc{reduction elaboration:}{\mydeclsyn \myelabf \myctx \vdash \mytmsyn \myred \mytmsyn}{
2535 $\myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \ \ \myelabf$
2536 \AxiomC{$\mytyc{D} \in \myctx$}
2537 \UnaryInfC{$\myctx \vdash \myapp{\mytyc{D}.\myfun{f}_i}{(\mytyc{D}.\mydc{constr} \myappsp \vec{t})} \myred t_i$}
2542 \caption{Elaboration for data types and records.}
2546 Following the intuition given by the examples, the mechanised
2547 elaboration is presented in figure \ref{fig:elab}, which is essentially
2548 a modification of figure 9 of \citep{McBride2004}\footnote{However, our
2549 datatypes do not have indices, we do bidirectional typechecking by
2550 treating constructors/destructors as syntactic constructs, and we have
2553 In data types declarations we allow recursive occurrences as long as
2554 they are \emph{strictly positive}, employing a syntactic check to make
2555 sure that this is the case. See \cite{Dybjer1991} for a more formal
2556 treatment of inductive definitions in ITT.
2558 For what concerns records, recursive occurrences are disallowed. The
2559 reason for this choice is answered by the reason for the choice of
2560 having records at all: we need records to give the user types with
2561 $\eta$-laws for equality, as we saw in section % TODO add section
2562 and in the treatment of OTT in section \ref{sec:ott}. If we tried to
2563 $\eta$-expand recursive data types, we would expand forever.
2565 To implement bidirectional type checking for constructors and
2566 destructors, we store their types in full in the context, and then
2567 instantiate when due:
2569 \mydesc{typing:}{ }{
2572 \mytyc{D} : \mytele \myarr \mytyp \in \myctx \hspace{1cm}
2573 \mytyc{D}.\mydc{c} : \mytele \mycc \mytele' \myarr
2574 \myapp{\mytyc{D}}{\mytelee} \in \myctx \\
2575 \mytele'' = (\mytele;\mytele')\vec{A} \hspace{1cm}
2576 \mychkk{\myctx; \mytake_{i-1}(\mytele'')}{t_i}{\myix_i( \mytele'')}\ \
2577 (1 \le i \le \mytele'')
2580 \UnaryInfC{$\mychk{\myapp{\mytyc{D}.\mydc{c}}{\vec{t}}}{\myapp{\mytyc{D}}{\vec{A}}}$}
2585 \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
2586 \AxiomC{$\mytyc{D}.\myfun{f} : \mytele \mycc (\myb{x} {:}
2587 \myapp{\mytyc{D}}{\mytelee}) \myarr \myse{F}$}
2588 \AxiomC{$\myjud{\mytmt}{\myapp{\mytyc{D}}{\vec{A}}}$}
2589 \TrinaryInfC{$\myinf{\myapp{\mytyc{D}.\myfun{f}}{\mytmt}}{(\mytele
2590 \mycc (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr
2591 \myse{F})(\vec{A};\mytmt)}$}
2595 \subsubsection{Why user defined types? Why eliminators?}
2597 % TODO reference levitated theories, indexed containers
2601 \subsection{Cumulative hierarchy and typical ambiguity}
2602 \label{sec:term-hierarchy}
2604 A type hierarchy as presented in section \label{sec:itt} is a
2605 considerable burden on the user, on various levels. Consider for
2606 example how we recovered disjunctions in section \ref{sec:disju}: we
2607 have a function that takes two $\mytyp_0$ and forms a new $\mytyp_0$.
2608 What if we wanted to form a disjunction containing two $\mytyp_0$, or
2609 $\mytyp_{42}$? Our definition would fail us, since $\mytyp_0 :
2612 One way to solve this issue is a \emph{cumulative} hierarchy, where
2613 $\mytyp_{l_1} : \mytyp_{l_2}$ iff $l_1 < l_2$. This way we retain
2614 consistency, while allowing for `large' definitions that work on small
2615 types too. For example we might define our disjunction to be
2617 \myarg\myfun{$\vee$}\myarg : \mytyp_{100} \myarr \mytyp_{100} \myarr \mytyp_{100}
2619 And hope that $\mytyp_{100}$ will be large enough to fit all the types
2620 that we want to use with our disjunction. However, there are two
2621 problems with this. First, there is the obvious clumsyness of having to
2622 manually specify the size of types. More importantly, if we want to use
2623 $\myfun{$\vee$}$ itself as an argument to other type-formers, we need to
2624 make sure that those allow for types at least as large as
2627 A better option is to employ a mechanised version of what Russell called
2628 \emph{typical ambiguity}: we let the user live under the illusion that
2629 $\mytyp : \mytyp$, but check that the statements about types are
2630 consistent behind the hood. $\mykant$\ implements this following the
2631 lines of \cite{Huet1988}. See also \citep{Harper1991} for a published
2632 reference, although describing a more complex system allowing for both
2633 explicit and explicit hierarchy at the same time.
2635 We define a partial ordering on the levels, with both weak ($\le$) and
2636 strong ($<$) constraints---the laws governing them being the same as the
2637 ones governing $<$ and $\le$ for the natural numbers. Each occurrence
2638 of $\mytyp$ is decorated with a unique reference, and we keep a set of
2639 constraints and add new constraints as we type check, generating new
2640 references when needed.
2642 For example, when type checking the type $\mytyp\, r_1$, where $r_1$
2643 denotes the unique reference assigned to that term, we will generate a
2644 new fresh reference $\mytyp\, r_2$, and add the constraint $r_1 < r_2$
2645 to the set. When type checking $\myctx \vdash
2646 \myfora{\myb{x}}{\mytya}{\mytyb}$, if $\myctx \vdash \mytya : \mytyp\,
2647 r_1$ and $\myctx; \myb{x} : \mytyb \vdash \mytyb : \mytyp\,r_2$; we will
2648 generate new reference $r$ and add $r_1 \le r$ and $r_2 \le r$ to the
2651 If at any point the constraint set becomes inconsistent, type checking
2652 fails. Moreover, when comparing two $\mytyp$ terms we equate their
2653 respective references with two $\le$ constraints---the details are
2654 explained in section \ref{sec:hier-impl}.
2656 Another more flexible but also more verbose alternative is the one
2657 chosen by Agda, where levels can be quantified so that the relationship
2658 between arguments and result in type formers can be explicitly
2661 \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}
2663 Inference algorithms to automatically derive this kind of relationship
2664 are currently subject of research. We chose less flexible but more
2665 concise way, since it is easier to implement and better understood.
2667 \subsection{Observational equality, \mykant\ style}
2669 There are two correlated differences between $\mykant$\ and the theory
2670 used to present OTT. The first is that in $\mykant$ we have a type
2671 hierarchy, which lets us, for example, abstract over types. The second
2672 is that we let the user define inductive types.
2674 Reconciling propositions for OTT and a hierarchy had already been
2675 investigated by Conor McBride\footnote{See
2676 \url{http://www.e-pig.org/epilogue/index.html?p=1098.html}.}, and we
2677 follow his footsteps. Most of the work, as an extension of elaboration,
2678 is to generate reduction rules and coercions.
2680 \subsubsection{The \mykant\ prelude, and $\myprop$ositions}
2682 Before defining $\myprop$, we define some basic types inside $\mykant$,
2683 as the target for the $\myprop$ decoder:
2688 \myadt{\mytyc{Empty}}{}{ }{ } \\
2689 \myfun{absurd} : (\myb{A} {:} \mytyp) \myarr \mytyc{Empty} \myarr \myb{A} \mapsto \\
2690 \myind{2} \myabs{\myb{A\ \myb{bot}}}{\mytyc{Empty}.\myfun{elim} \myappsp \myb{bot} \myappsp (\myabs{\_}{\myb{A}})} \\
2693 \myreco{\mytyc{Unit}}{}{}{ } \\ \ \\
2695 \myreco{\mytyc{Prod}}{\myappsp (\myb{A}\ \myb{B} {:} \mytyp)}{ }{\myfun{fst} : \myb{A}, \myfun{snd} : \myb{B} }
2699 When using $\mytyc{Prod}$, we shall use $\myprod$ to define `nested'
2700 products, and $\myproj{n}$ to project elements from them, so that
2704 \mytya \myprod \mytyb = \mytyc{Prod} \myappsp \mytya \myappsp (\mytyc{Prod} \myappsp \mytyb \myappsp \myunit) \\
2705 \mytya \myprod \mytyb \myprod \myse{C} = \mytyc{Prod} \myappsp \mytya \myappsp (\mytyc{Prod} \myappsp \mytyb \myappsp (\mytyc{Prod} \myappsp \mytyc \myappsp \myunit)) \\
2707 \myproj{1} : \mytyc{Prod} \myappsp \mytya \myappsp \mytyb \myarr \mytya \\
2708 \myproj{2} : \mytyc{Prod} \myappsp \mytya \myappsp (\mytyc{Prod} \myappsp \mytyb \myappsp \myse{C}) \myarr \mytyb \\
2713 And so on, so that $\myproj{n}$ will work with all products with at
2714 least than $n$ elements. Then we can define propositions, and decoding:
2718 \begin{array}{r@{\ }c@{\ }l}
2719 \mytmsyn & ::= & \cdots \mysynsep \myprdec{\myprsyn} \\
2720 \myprsyn & ::= & \mybot \mysynsep \mytop \mysynsep \myprsyn \myand \myprsyn \mysynsep \myprfora{\myb{x}}{\mytmsyn}{\myprsyn}
2725 \mydesc{proposition decoding:}{\myprdec{\mytmsyn} \myred \mytmsyn}{
2728 \begin{array}{l@{\ }c@{\ }l}
2729 \myprdec{\mybot} & \myred & \myempty \\
2730 \myprdec{\mytop} & \myred & \myunit
2735 \begin{array}{r@{ }c@{ }l@{\ }c@{\ }l}
2736 \myprdec{&\myse{P} \myand \myse{Q} &} & \myred & \myprdec{\myse{P}} \myprod \myprdec{\myse{Q}} \\
2737 \myprdec{&\myprfora{\myb{x}}{\mytya}{\myse{P}} &} & \myred &
2738 \myfora{\myb{x}}{\mytya}{\myprdec{\myse{P}}}
2744 \subsubsection{Why $\myprop$?}
2746 It is worth to ask if $\myprop$ is needed at all. It is perfectly
2747 possible to have the type checker identify propositional types
2748 automatically, and in fact that is what The author initially planned to
2749 identify the propositional fragment internally \cite{Jacobs1994}.
2753 \subsubsection{OTT constructs}
2755 Before presenting the direction that $\mykant$\ takes, let's consider
2756 some examples of use-defined data types, and the result we would expect,
2757 given what we already know about OTT, assuming the same propositional
2762 \item[Product types] Let's consider first the already mentioned
2763 dependent product, using the alternate name $\mysigma$\footnote{For
2764 extra confusion, `dependent products' are often called `dependent
2765 sums' in the literature, referring to the interpretation that
2766 identifies the first element as a `tag' deciding the type of the
2767 second element, which lets us recover sum types (disjuctions), as we
2768 saw in section \ref{sec:user-type}. Thus, $\mysigma$.} to
2769 avoid confusion with the $\mytyc{Prod}$ in the prelude: {\small\[
2771 \myreco{\mysigma}{\myappsp (\myb{A} {:} \mytyp) \myappsp (\myb{B} {:} \myb{A} \myarr \mytyp)}{\\ \myind{2}}{\myfst : \myb{A}, \mysnd : \myapp{\myb{B}}{\myb{fst}}}
2773 \]} Let's start with type-level equality. The result we want is
2776 \mysigma \myappsp \mytya_1 \myappsp \mytyb_1 \myeq \mysigma \myappsp \mytya_2 \myappsp \mytyb_2 \myred \\
2777 \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}}}
2779 \]} The difference here is that in the original presentation of OTT
2780 the type binders are explicit, while here $\mytyb_1$ and $\mytyb_2$
2781 functions returning types. We can do this thanks to the type
2782 hierarchy, and this hints at the fact that heterogeneous equality will
2783 have to allow $\mytyp$ `to the right of the colon', and in fact this
2784 provides the solution to simplify the equality above.
2786 If we take, just like we saw previously in OTT
2789 \myjm{\myse{f}_1}{\myfora{\mytya_1}{\myb{x_1}}{\mytyb_1}}{\myse{f}_2}{\myfora{\mytya_2}{\myb{x_2}}{\mytyb_2}} \myred \\
2790 \myind{2} \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{
2791 \myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2} \myimpl
2792 \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}]}
2795 \]} Then we can simply take
2798 \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}
2800 \]} Which will reduce to precisely what we desire. For what
2801 concerns coercions and quotation, things stay the same (apart from the
2802 fact that we apply to the second argument instead of substituting).
2803 We can recognise records such as $\mysigma$ as such and employ
2804 projections in value equality, coercions, and quotation; as to not
2805 impede progress if not necessary.
2807 \item[Lists] Now for finite lists, which will give us a taste for data
2811 \myadt{\mylist}{\myappsp (\myb{A} {:} \mytyp)}{ }{\mydc{nil} \mydcsep \mydc{cons} \myappsp \myb{A} \myappsp (\myapp{\mylist}{\myb{A}})}
2814 Type equality is simple---we only need to compare the parameter:
2816 \mylist \myappsp \mytya_1 \myeq \mylist \myappsp \mytya_2 \myred \mytya_1 \myeq \mytya_2
2817 \]} For coercions, we transport based on the constructor, recycling
2818 the proof for the inductive occurrence: {\small\[
2819 \begin{array}{@{}l@{\ }c@{\ }l}
2820 \mycoe \myappsp (\mylist \myappsp \mytya_1) \myappsp (\mylist \myappsp \mytya_2) \myappsp \myse{Q} \myappsp \mydc{nil} & \myred & \mydc{nil} \\
2821 \mycoe \myappsp (\mylist \myappsp \mytya_1) \myappsp (\mylist \myappsp \mytya_2) \myappsp \myse{Q} \myappsp (\mydc{cons} \myappsp \mytmm \myappsp \mytmn) & \myred & \\
2822 \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)}
2824 \]} Value equality is unsurprising---we match the constructors, and
2825 return bottom for mismatches. However, we also need to equate the
2826 parameter in $\mydc{nil}$: {\small\[
2827 \begin{array}{r@{ }c@{\ }c@{\ }c@{}l@{\ }c@{\ }r@{}c@{\ }c@{\ }c@{}l@{\ }l}
2828 (& \mydc{nil} & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{nil} & : & \myapp{\mylist}{\mytya_2} &) \myred \mytya_1 \myeq \mytya_2 \\
2829 (& \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 \\
2830 & \multicolumn{11}{@{}l}{ \myind{2}
2831 \myjm{\mytmm_1}{\mytya_1}{\mytmm_2}{\mytya_2} \myand \myjm{\mytmn_1}{\myapp{\mylist}{\mytya_1}}{\mytmn_2}{\myapp{\mylist}{\mytya_2}}
2833 (& \mydc{nil} & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{cons} \myappsp \mytmm_2 \myappsp \mytmn_2 & : & \myapp{\mylist}{\mytya_2} &) \myred \mybot \\
2834 (& \mydc{cons} \myappsp \mytmm_1 \myappsp \mytmn_1 & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{nil} & : & \myapp{\mylist}{\mytya_2} &) \myred \mybot
2848 \begin{array}{r@{\ }c@{\ }l}
2849 \mytmsyn & ::= & \cdots \mysynsep \mycoee{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \mysynsep
2850 \mycohh{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
2851 \myprsyn & ::= & \cdots \mysynsep \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
2857 \mydesc{typing:}{\myctx \vdash \myprsyn \myred \myprsyn}{
2860 \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
2861 \AxiomC{$\myjud{\mytmt}{\mytya}$}
2862 \BinaryInfC{$\myjud{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}$}
2865 \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
2866 \AxiomC{$\myjud{\mytmt}{\mytya}$}
2867 \BinaryInfC{$\myjud{\mycohh{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\myprdec{\myjm{\mytmt}{\mytya}{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}}}$}
2871 \mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
2874 \AxiomC{\phantom{$\myjud{\myse{P}}{\myprop}$}}
2875 \UnaryInfC{$\myjud{\mytop}{\myprop}$}
2877 \UnaryInfC{$\myjud{\mybot}{\myprop}$}
2880 \AxiomC{$\myjud{\myse{P}}{\myprop}$}
2881 \AxiomC{$\myjud{\myse{Q}}{\myprop}$}
2882 \BinaryInfC{$\myjud{\myse{P} \myand \myse{Q}}{\myprop}$}
2884 \UnaryInfC{\phantom{$\myjud{\mybot}{\myprop}$}}
2893 \phantom{\myjud{\myse{A}}{\mytyp} \hspace{0.8cm} \myjud{\mytmm}{\myse{A}}} \\
2894 \myjud{\myse{A}}{\mytyp}\hspace{0.8cm}
2895 \myjudd{\myctx; \myb{x} : \mytya}{\myse{P}}{\myprop}
2898 \UnaryInfC{$\myjud{\myprfora{\myb{x}}{\mytya}{\myse{P}}}{\myprop}$}
2903 \myjud{\myse{A}}{\mytyp} \hspace{0.8cm} \myjud{\mytmm}{\myse{A}} \\
2904 \myjud{\myse{B}}{\mytyp} \hspace{0.8cm} \myjud{\mytmn}{\myse{B}}
2907 \UnaryInfC{$\myjud{\myjm{\mytmm}{\myse{A}}{\mytmn}{\myse{B}}}{\myprop}$}
2911 % TODO equality for decodings
2912 \mydesc{equality reduction:}{\myctx \vdash \myprsyn \myred \myprsyn}{
2915 \UnaryInfC{$\myctx \vdash \myjm{\mytyp}{\mytyp}{\mytyp}{\mytyp} \myred \mytop$}
2922 \begin{array}{@{}r@{\ }l}
2924 \myjm{\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}}{\mytyp}{\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}}{\mytyp} \myred \\
2925 & \myind{2} \mytya_2 \myeq \mytya_1 \myand \myprfora{\myb{x_2}}{\mytya_2}{\myprfora{\myb{x_1}}{\mytya_1}{
2926 \myjm{\myb{x_2}}{\mytya_2}{\myb{x_1}}{\mytya_1} \myimpl \mytyb_1 \myeq \mytyb_2
2936 \begin{array}{@{}r@{\ }l}
2938 \myjm{\myse{f}_1}{\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}}{\myse{f}_2}{\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}} \myred \\
2939 & \myind{2} \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{
2940 \myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2} \myimpl
2941 \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}]}
2950 \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
2952 \begin{array}{r@{\ }l}
2954 \myjm{\mytyc{D} \myappsp \vec{A}}{\mytyp}{\mytyc{D} \myappsp \vec{B}}{\mytyp} \myred \\
2955 & \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}))})
2964 \mydataty(\mytyc{D}, \myctx)\hspace{0.8cm}
2965 \mytyc{D}.\mydc{c} : \mytele;\mytele' \myarr \mytyc{D} \myappsp \mytelee \in \myctx \\
2966 \mytele_A = (\mytele;\mytele')\vec{A}\hspace{0.8cm}
2967 \mytele_B = (\mytele;\mytele')\vec{B}
2971 \begin{array}{@{}l@{\ }l}
2972 \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 \\
2973 & \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}))})
2980 \AxiomC{$\mydataty(\mytyc{D}, \myctx)$}
2982 \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
2990 \myisreco(\mytyc{D}, \myctx)\hspace{0.8cm}
2991 \mytyc{D}.\myfun{f}_i : \mytele; (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr \myse{F}_i \in \myctx\\
2995 \begin{array}{@{}l@{\ }l}
2996 \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})})
3003 \UnaryInfC{$\myjm{\mytmm}{\mytya}{\mytmn}{\mytyb} \myred \mybot\ \text{if $\mytya$ and $\mytyb$ are canonical types.}$}
3006 \caption{Equality reduction for $\mykant$.}
3007 \label{fig:kant-eq-red}
3010 \subsubsection{$\myprop$ and the hierarchy}
3012 Where is $\myprop$ placed in the $\mytyp$ hierarchy? At each universe
3013 level, we will have that
3015 \subsubsection{Quotation and irrelevance}
3020 \section{\mykant : The practice}
3021 \label{sec:kant-practice}
3023 The codebase consists of around 2500 lines of Haskell, as reported by
3024 the \texttt{cloc} utility. The high level design is inspired by Conor
3025 McBride's work on various incarnations of Epigram, and specifically by
3026 the first version as described \citep{McBride2004} and the codebase for
3027 the new version \footnote{Available intermittently as a \texttt{darcs}
3028 repository at \url{http://sneezy.cs.nott.ac.uk/darcs/Pig09}.}. In
3029 many ways \mykant\ is something in between the first and second version
3032 The interaction happens in a read-eval-print loop (REPL). The REPL is a
3033 available both as a commandline application and in a web interface,
3034 which is available at \url{kant.mazzo.li} and presents itself as in
3035 figure \ref{fig:kant-web}.
3039 \includegraphics[scale=1.0]{kant-web.png}
3041 \caption{The \mykant\ web prompt.}
3042 \label{fig:kant-web}
3045 The interaction with the user takes place in a loop living in and updating a
3046 context \mykant\ declarations. The user inputs a new declaration that goes
3047 through various stages starts with the user inputing a \mykant\ declaration or
3048 another REPL command, which then goes through various stages that can end up
3049 in a context update, or in failures of various kind. The process is described
3050 diagrammatically in figure \ref{fig:kant-process}:
3053 \item[Parse] In this phase the text input gets converted to a sugared
3054 version of the core language.
3056 \item[Desugar] The sugared declaration is converted to a core term.
3058 \item[Reference] Occurrences of $\mytyp$ get decorated by a unique reference,
3059 which is necessary to implement the type hierarchy check.
3061 \item[Elaborate] Convert the declaration to some context item, which might be
3062 a value declaration (type and body) or a data type declaration (constructors
3063 and destructors). This phase works in tandem with \textbf{Typechecking},
3064 which in turns needs to \textbf{Evaluate} terms.
3066 \item[Distill] and report the result. `Distilling' refers to the process of
3067 converting a core term back to a sugared version that the user can
3068 visualise. This can be necessary both to display errors including terms or
3069 to display result of evaluations or type checking that the user has
3072 \item[Pretty print] Format the terms in a nice way, and display the result to
3079 \tikzstyle{block} = [rectangle, draw, text width=5em, text centered, rounded
3080 corners, minimum height=2.5em, node distance=0.7cm]
3082 \tikzstyle{decision} = [diamond, draw, text width=4.5em, text badly
3083 centered, inner sep=0pt, node distance=0.7cm]
3085 \tikzstyle{line} = [draw, -latex']
3087 \tikzstyle{cloud} = [draw, ellipse, minimum height=2em, text width=5em, text
3088 centered, node distance=1.5cm]
3091 \begin{tikzpicture}[auto]
3092 \node [cloud] (user) {User};
3093 \node [block, below left=1cm and 0.1cm of user] (parse) {Parse};
3094 \node [block, below=of parse] (desugar) {Desugar};
3095 \node [block, below=of desugar] (reference) {Reference};
3096 \node [block, below=of reference] (elaborate) {Elaborate};
3097 \node [block, left=of elaborate] (tycheck) {Typecheck};
3098 \node [block, left=of tycheck] (evaluate) {Evaluate};
3099 \node [decision, right=of elaborate] (error) {Error?};
3100 \node [block, right=of parse] (distill) {Distill};
3101 \node [block, right=of desugar] (update) {Update context};
3103 \path [line] (user) -- (parse);
3104 \path [line] (parse) -- (desugar);
3105 \path [line] (desugar) -- (reference);
3106 \path [line] (reference) -- (elaborate);
3107 \path [line] (elaborate) edge[bend right] (tycheck);
3108 \path [line] (tycheck) edge[bend right] (elaborate);
3109 \path [line] (elaborate) -- (error);
3110 \path [line] (error) edge[out=0,in=0] node [near start] {yes} (distill);
3111 \path [line] (error) -- node [near start] {no} (update);
3112 \path [line] (update) -- (distill);
3113 \path [line] (distill) -- (user);
3114 \path [line] (tycheck) edge[bend right] (evaluate);
3115 \path [line] (evaluate) edge[bend right] (tycheck);
3118 \caption{High level overview of the life of a \mykant\ prompt cycle.}
3119 \label{fig:kant-process}
3122 \subsection{Parsing and \texttt{Sugar}}
3124 \subsection{Term representation and context}
3125 \label{sec:term-repr}
3127 \subsection{Type checking}
3129 \subsection{Type hierarchy}
3130 \label{sec:hier-impl}
3132 \subsection{Elaboration}
3134 \section{Evaluation}
3136 \section{Future work}
3138 \subsection{Coinduction}
3140 \subsection{Quotient types}
3142 \subsection{Partiality}
3144 \subsection{Pattern matching}
3146 \subsection{Pattern unification}
3148 % TODO coinduction (obscoin, gimenez), pattern unification (miller,
3149 % gundry), partiality monad (NAD)
3153 \section{Notation and syntax}
3155 Syntax, derivation rules, and reduction rules, are enclosed in frames describing
3156 the type of relation being established and the syntactic elements appearing,
3159 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
3160 Typing derivations here.
3163 In the languages presented and Agda code samples I also highlight the syntax,
3164 following a uniform color and font convention:
3167 \begin{tabular}{c | l}
3168 $\mytyc{Sans}$ & Type constructors. \\
3169 $\mydc{sans}$ & Data constructors. \\
3170 % $\myfld{sans}$ & Field accessors (e.g. \myfld{fst} and \myfld{snd} for products). \\
3171 $\mysyn{roman}$ & Keywords of the language. \\
3172 $\myfun{roman}$ & Defined values and destructors. \\
3173 $\myb{math}$ & Bound variables.
3177 Moreover, I will from time to time give examples in the Haskell programming
3178 language as defined in \citep{Haskell2010}, which I will typeset in
3179 \texttt{teletype} font. I assume that the reader is already familiar with
3180 Haskell, plenty of good introductions are available \citep{LYAH,ProgInHask}.
3182 When presenting grammars, I will use a word in $\mysynel{math}$ font
3183 (e.g. $\mytmsyn$ or $\mytysyn$) to indicate indicate nonterminals. Additionally,
3184 I will use quite flexibly a $\mysynel{math}$ font to indicate a syntactic
3185 element. More specifically, terms are usually indicated by lowercase letters
3186 (often $\mytmt$, $\mytmm$, or $\mytmn$); and types by an uppercase letter (often
3187 $\mytya$, $\mytyb$, or $\mytycc$).
3189 When presenting type derivations, I will often abbreviate and present multiple
3190 conclusions, each on a separate line:
3192 \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
3193 \UnaryInfC{$\myjud{\myapp{\myfst}{\mytmt}}{\mytya}$}
3195 \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mytyb}$}
3198 I will often present `definition' in the described calculi and in
3199 $\mykant$\ itself, like so:
3202 \myfun{name} : \mytysyn \\
3203 \myfun{name} \myappsp \myb{arg_1} \myappsp \myb{arg_2} \myappsp \cdots \mapsto \mytmsyn
3206 To define operators, I use a mixfix notation similar
3207 to Agda, where $\myarg$s denote arguments, for example
3210 \myarg \mathrel{\myfun{$\wedge$}} \myarg : \mybool \myarr \mybool \myarr \mybool \\
3211 \myb{b_1} \mathrel{\myfun{$\wedge$}} \myb{b_2} \mapsto \cdots
3217 \subsection{ITT renditions}
3218 \label{app:itt-code}
3220 \subsubsection{Agda}
3221 \label{app:agda-itt}
3223 Note that in what follows rules for `base' types are
3224 universe-polymorphic, to reflect the exposition. Derived definitions,
3225 on the other hand, mostly work with \mytyc{Set}, reflecting the fact
3226 that in the theory presented we don't have universe polymorphism.
3232 data Empty : Set where
3234 absurd : ∀ {a} {A : Set a} → Empty → A
3237 ¬_ : ∀ {a} → (A : Set a) → Set a
3240 record Unit : Set where
3243 record _×_ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
3250 data Bool : Set where
3253 if_/_then_else_ : ∀ {a} (x : Bool) (P : Bool → Set a) → P true → P false → P x
3254 if true / _ then x else _ = x
3255 if false / _ then _ else x = x
3257 if_then_else_ : ∀ {a} (x : Bool) {P : Bool → Set a} → P true → P false → P x
3258 if_then_else_ x {P} = if_/_then_else_ x P
3260 data W {s p} (S : Set s) (P : S → Set p) : Set (s ⊔ p) where
3261 _◁_ : (s : S) → (P s → W S P) → W S P
3263 rec : ∀ {a b} {S : Set a} {P : S → Set b}
3264 (C : W S P → Set) → -- some conclusion we hope holds
3265 ((s : S) → -- given a shape...
3266 (f : P s → W S P) → -- ...and a bunch of kids...
3267 ((p : P s) → C (f p)) → -- ...and C for each kid in the bunch...
3268 C (s ◁ f)) → -- ...does C hold for the node?
3269 (x : W S P) → -- If so, ...
3270 C x -- ...C always holds.
3271 rec C c (s ◁ f) = c s f (λ p → rec C c (f p))
3273 module Examples-→ where
3280 -- These pragmas are needed so we can use number literals.
3281 {-# BUILTIN NATURAL ℕ #-}
3282 {-# BUILTIN ZERO zero #-}
3283 {-# BUILTIN SUC suc #-}
3285 data List (A : Set) : Set where
3287 _∷_ : A → List A → List A
3289 length : ∀ {A} → List A → ℕ
3291 length (_ ∷ l) = suc (length l)
3296 suc x > suc y = x > y
3298 head : ∀ {A} → (l : List A) → length l > 0 → A
3299 head [] p = absurd p
3302 module Examples-× where
3308 even (suc zero) = Empty
3309 even (suc (suc n)) = even n
3314 5-not-even : ¬ (even 5)
3317 there-is-an-even-number : ℕ × even
3318 there-is-an-even-number = 6 , 6-even
3320 _∨_ : (A B : Set) → Set
3321 A ∨ B = Bool × (λ b → if b then A else B)
3323 left : ∀ {A B} → A → A ∨ B
3326 right : ∀ {A B} → B → A ∨ B
3329 [_,_] : {A B C : Set} → (A → C) → (B → C) → A ∨ B → C
3331 (if (fst x) / (λ b → if b then _ else _ → _) then f else g) (snd x)
3333 module Examples-W where
3338 Tr b = if b then Unit else Empty
3344 zero = false ◁ absurd
3347 suc n = true ◁ (λ _ → n)
3353 if b / (λ b → (Tr b → ℕ) → (Tr b → ℕ) → ℕ)
3354 then (λ _ f → (suc (f tt))) else (λ _ _ → y))
3357 List : (A : Set) → Set
3358 List A = W (A ∨ Unit) (λ s → Tr (fst s))
3361 [] = (false , tt) ◁ absurd
3363 _∷_ : ∀ {A} → A → List A → List A
3364 x ∷ l = (true , x) ◁ (λ _ → l)
3366 _++_ : ∀ {A} → List A → List A → List A
3368 (λ _ → List _ → List _)
3372 module Equality where
3375 data _≡_ {a} {A : Set a} : A → A → Set a where
3378 ≡-elim : ∀ {a b} {A : Set a}
3379 (P : (x y : A) → x ≡ y → Set b) →
3380 ∀ {x y} → P x x (refl x) → (x≡y : x ≡ y) → P x y x≡y
3381 ≡-elim P p (refl x) = p
3383 subst : ∀ {A : Set} (P : A → Set) → ∀ {x y} → (x≡y : x ≡ y) → P x → P y
3384 subst P x≡y p = ≡-elim (λ _ y _ → P y) p x≡y
3386 sym : ∀ {A : Set} (x y : A) → x ≡ y → y ≡ x
3387 sym x y p = subst (λ y′ → y′ ≡ x) p (refl x)
3389 trans : ∀ {A : Set} (x y z : A) → x ≡ y → y ≡ z → x ≡ z
3390 trans x y z p q = subst (λ z′ → x ≡ z′) q p
3392 cong : ∀ {A B : Set} (x y : A) → x ≡ y → (f : A → B) → f x ≡ f y
3393 cong x y p f = subst (λ z → f x ≡ f z) p (refl (f x))
3396 \subsubsection{\mykant}
3398 The following things are missing: $\mytyc{W}$-types, since our
3399 positivity check is overly strict, and equality, since we haven't
3400 implemented that yet.
3403 \verbatiminput{itt.ka}
3406 \subsection{\mykant\ examples}
3409 \verbatiminput{examples.ka}
3412 \subsection{\mykant's hierachy}
3414 This rendition of the Hurken's paradox does not type check with the
3415 hierachy enabled, type checks and loops without it. Adapted from an
3416 Agda version, available at
3417 \url{http://code.haskell.org/Agda/test/succeed/Hurkens.agda}.
3420 \verbatiminput{hurkens.ka}
3423 \bibliographystyle{authordate1}
3424 \bibliography{thesis}