1 \documentclass[report]{article}
5 % \usepackage{fullpage}
17 \usepackage[fleqn]{amsmath}
18 \usepackage{stmaryrd} %llbracket
21 \usepackage{bussproofs}
33 \usepackage{subcaption}
39 \usetikzlibrary{shapes,arrows,positioning}
40 % \usepackage{tikz-cd}
41 % \usepackage{pgfplots}
44 %% -----------------------------------------------------------------------------
46 \usepackage[english]{babel}
47 \usepackage[conor]{agda}
48 \renewcommand{\AgdaKeywordFontStyle}[1]{\ensuremath{\mathrm{\underline{#1}}}}
49 \renewcommand{\AgdaFunction}[1]{\textbf{\textcolor{AgdaFunction}{#1}}}
50 \renewcommand{\AgdaField}{\AgdaFunction}
51 % \definecolor{AgdaBound} {HTML}{000000}
52 \definecolor{AgdaHole} {HTML} {FFFF33}
54 \DeclareUnicodeCharacter{9665}{\ensuremath{\lhd}}
55 \DeclareUnicodeCharacter{964}{\ensuremath{\tau}}
56 \DeclareUnicodeCharacter{963}{\ensuremath{\sigma}}
57 \DeclareUnicodeCharacter{915}{\ensuremath{\Gamma}}
58 \DeclareUnicodeCharacter{8799}{\ensuremath{\stackrel{?}{=}}}
59 \DeclareUnicodeCharacter{9655}{\ensuremath{\rhd}}
61 \renewenvironment{code}%
62 {\noindent\ignorespaces\advance\leftskip\mathindent\AgdaCodeStyle\pboxed}%
63 {\endpboxed\par\noindent%
64 \ignorespacesafterend\small}
67 %% -----------------------------------------------------------------------------
70 \newcommand{\mysyn}{\AgdaKeyword}
71 \newcommand{\mytyc}{\AgdaDatatype}
72 \newcommand{\mydc}{\AgdaInductiveConstructor}
73 \newcommand{\myfld}{\AgdaField}
74 \newcommand{\myfun}{\AgdaFunction}
75 \newcommand{\myb}[1]{\AgdaBound{$#1$}}
76 \newcommand{\myfield}{\AgdaField}
77 \newcommand{\myind}{\AgdaIndent}
78 \newcommand{\mykant}{\textsc{Kant}}
79 \newcommand{\mysynel}[1]{#1}
80 \newcommand{\myse}{\mysynel}
81 \newcommand{\mytmsyn}{\mysynel{term}}
82 \newcommand{\mysp}{\ }
83 \newcommand{\myabs}[2]{\mydc{$\lambda$} #1 \mathrel{\mydc{$\mapsto$}} #2}
84 \newcommand{\myappsp}{\hspace{0.07cm}}
85 \newcommand{\myapp}[2]{#1 \myappsp #2}
86 \newcommand{\mysynsep}{\ \ |\ \ }
87 \newcommand{\myITE}[3]{\myfun{If}\, #1\, \myfun{Then}\, #2\, \myfun{Else}\, #3}
90 \newcommand{\mydesc}[3]{
96 \hfill \textbf{#1} $#2$
97 \framebox[\textwidth]{
111 \newcommand{\mytmt}{\mysynel{t}}
112 \newcommand{\mytmm}{\mysynel{m}}
113 \newcommand{\mytmn}{\mysynel{n}}
114 \newcommand{\myred}{\leadsto}
115 \newcommand{\mysub}[3]{#1[#2 / #3]}
116 \newcommand{\mytysyn}{\mysynel{type}}
117 \newcommand{\mybasetys}{K}
118 \newcommand{\mybasety}[1]{B_{#1}}
119 \newcommand{\mytya}{\myse{A}}
120 \newcommand{\mytyb}{\myse{B}}
121 \newcommand{\mytycc}{\myse{C}}
122 \newcommand{\myarr}{\mathrel{\textcolor{AgdaDatatype}{\to}}}
123 \newcommand{\myprod}{\mathrel{\textcolor{AgdaDatatype}{\times}}}
124 \newcommand{\myctx}{\Gamma}
125 \newcommand{\myvalid}[1]{#1 \vdash \underline{\mathrm{valid}}}
126 \newcommand{\myjudd}[3]{#1 \vdash #2 : #3}
127 \newcommand{\myjud}[2]{\myjudd{\myctx}{#1}{#2}}
128 \newcommand{\myabss}[3]{\mydc{$\lambda$} #1 {:} #2 \mathrel{\mydc{$\mapsto$}} #3}
129 \newcommand{\mytt}{\mydc{$\langle\rangle$}}
130 \newcommand{\myunit}{\mytyc{Unit}}
131 \newcommand{\mypair}[2]{\mathopen{\mydc{$\langle$}}#1\mathpunct{\mydc{,}} #2\mathclose{\mydc{$\rangle$}}}
132 \newcommand{\myfst}{\myfld{fst}}
133 \newcommand{\mysnd}{\myfld{snd}}
134 \newcommand{\myconst}{\myse{c}}
135 \newcommand{\myemptyctx}{\cdot}
136 \newcommand{\myhole}{\AgdaHole}
137 \newcommand{\myfix}[3]{\mysyn{fix} \myappsp #1 {:} #2 \mapsto #3}
138 \newcommand{\mysum}{\mathbin{\textcolor{AgdaDatatype}{+}}}
139 \newcommand{\myleft}[1]{\mydc{left}_{#1}}
140 \newcommand{\myright}[1]{\mydc{right}_{#1}}
141 \newcommand{\myempty}{\mytyc{Empty}}
142 \newcommand{\mycase}[2]{\mathopen{\myfun{[}}#1\mathpunct{\myfun{,}} #2 \mathclose{\myfun{]}}}
143 \newcommand{\myabsurd}[1]{\myfun{absurd}_{#1}}
144 \newcommand{\myarg}{\_}
145 \newcommand{\myderivsp}{\vspace{0.3cm}}
146 \newcommand{\mytyp}{\mytyc{Type}}
147 \newcommand{\myneg}{\myfun{$\neg$}}
148 \newcommand{\myar}{\,}
149 \newcommand{\mybool}{\mytyc{Bool}}
150 \newcommand{\mytrue}{\mydc{true}}
151 \newcommand{\myfalse}{\mydc{false}}
152 \newcommand{\myitee}[5]{\myfun{if}\,#1 / {#2.#3}\,\myfun{then}\,#4\,\myfun{else}\,#5}
153 \newcommand{\mynat}{\mytyc{$\mathbb{N}$}}
154 \newcommand{\myrat}{\mytyc{$\mathbb{R}$}}
155 \newcommand{\myite}[3]{\myfun{if}\,#1\,\myfun{then}\,#2\,\myfun{else}\,#3}
156 \newcommand{\myfora}[3]{(#1 {:} #2) \myarr #3}
157 \newcommand{\myexi}[3]{(#1 {:} #2) \myprod #3}
158 \newcommand{\mypairr}[4]{\mathopen{\mydc{$\langle$}}#1\mathpunct{\mydc{,}} #4\mathclose{\mydc{$\rangle$}}_{#2{.}#3}}
159 \newcommand{\mylist}{\mytyc{List}}
160 \newcommand{\mynil}[1]{\mydc{[]}_{#1}}
161 \newcommand{\mycons}{\mathbin{\mydc{∷}}}
162 \newcommand{\myfoldr}{\myfun{foldr}}
163 \newcommand{\myw}[3]{\myapp{\myapp{\mytyc{W}}{(#1 {:} #2)}}{#3}}
164 \newcommand{\mynodee}{\mathbin{\mydc{$\lhd$}}}
165 \newcommand{\mynode}[2]{\mynodee_{#1.#2}}
166 \newcommand{\myrec}[4]{\myfun{rec}\,#1 / {#2.#3}\,\myfun{with}\,#4}
167 \newcommand{\mylub}{\sqcup}
168 \newcommand{\mydefeq}{\cong}
169 \newcommand{\myrefl}{\mydc{refl}}
170 \newcommand{\mypeq}[1]{\mathrel{\mytyc{=}_{#1}}}
171 \newcommand{\myjeqq}{\myfun{=-elim}}
172 \newcommand{\myjeq}[3]{\myapp{\myapp{\myapp{\myjeqq}{#1}}{#2}}{#3}}
173 \newcommand{\mysubst}{\myfun{subst}}
174 \newcommand{\myprsyn}{\myse{prop}}
175 \newcommand{\myprdec}[1]{\mathopen{\mytyc{$\llbracket$}} #1 \mathopen{\mytyc{$\rrbracket$}}}
176 \newcommand{\myand}{\mathrel{\mytyc{$\wedge$}}}
177 \newcommand{\myprfora}[3]{\forall #1 {:} #2. #3}
178 \newcommand{\myimpl}{\mathrel{\mytyc{$\Rightarrow$}}}
179 \newcommand{\mybot}{\mytyc{$\bot$}}
180 \newcommand{\mytop}{\mytyc{$\top$}}
181 \newcommand{\mycoe}{\myfun{coe}}
182 \newcommand{\mycoee}[4]{\myapp{\myapp{\myapp{\myapp{\mycoe}{#1}}{#2}}{#3}}{#4}}
183 \newcommand{\mycoh}{\myfun{coh}}
184 \newcommand{\mycohh}[4]{\myapp{\myapp{\myapp{\myapp{\mycoh}{#1}}{#2}}{#3}}{#4}}
185 \newcommand{\myjm}[4]{(#1 {:} #2) \mathrel{\mytyc{=}} (#3 {:} #4)}
186 \newcommand{\myeq}{\mathrel{\mytyc{=}}}
187 \newcommand{\myprop}{\mytyc{Prop}}
188 \newcommand{\mytmup}{\mytmsyn\uparrow}
189 \newcommand{\mydefs}{\Delta}
190 \newcommand{\mynf}{\Downarrow}
191 \newcommand{\myinff}[3]{#1 \vdash #2 \Rightarrow #3}
192 \newcommand{\myinf}[2]{\myinff{\myctx}{#1}{#2}}
193 \newcommand{\mychkk}[3]{#1 \vdash #2 \Leftarrow #3}
194 \newcommand{\mychk}[2]{\mychkk{\myctx}{#1}{#2}}
195 \newcommand{\myann}[2]{#1 : #2}
196 \newcommand{\mydeclsyn}{\myse{decl}}
197 \newcommand{\myval}[3]{#1 : #2 \mapsto #3}
198 \newcommand{\mypost}[2]{\mysyn{abstract}\ #1 : #2}
199 \newcommand{\myadt}[4]{\mysyn{data}\ #1 #2\ \mysyn{where}\ #3\{ #4 \}}
200 \newcommand{\myreco}[4]{\mysyn{record}\ #1 #2\ \mysyn{where}\ #3\ \{ #4 \}}
201 \newcommand{\myelabt}{\vdash}
202 \newcommand{\myelabf}{\rhd}
203 \newcommand{\myelab}[2]{\myctx \myelabt #1 \myelabf #2}
204 \newcommand{\mytele}{\Delta}
205 \newcommand{\mytelee}{\delta}
206 \newcommand{\mydcctx}{\Gamma}
207 \newcommand{\mynamesyn}{\myse{name}}
208 \newcommand{\myvec}{\overrightarrow}
209 \newcommand{\mymeta}{\textsc}
210 \newcommand{\myhyps}{\mymeta{hyps}}
211 \newcommand{\mycc}{;}
212 \newcommand{\myemptytele}{\cdot}
213 \newcommand{\mymetagoes}{\Longrightarrow}
214 % \newcommand{\mytesctx}{\
215 \newcommand{\mytelesyn}{\myse{telescope}}
216 \newcommand{\myrecs}{\mymeta{recs}}
217 \newcommand{\myle}{\mathrel{\lcfun{$\le$}}}
218 \newcommand{\mylet}{\mysyn{let}}
219 \newcommand{\myhead}{\mymeta{head}}
220 \newcommand{\mytake}{\mymeta{take}}
221 \newcommand{\myix}{\mymeta{ix}}
222 \newcommand{\myapply}{\mymeta{apply}}
223 \newcommand{\mydataty}{\mymeta{datatype}}
224 \newcommand{\myisreco}{\mymeta{record}}
225 \newcommand{\mydcsep}{\ |\ }
226 \newcommand{\mytree}{\mytyc{Tree}}
227 \newcommand{\myproj}[1]{\myfun{$\pi_{#1}$}}
230 %% -----------------------------------------------------------------------------
232 \title{\mykant: Implementing Observational Equality}
233 \author{Francesco Mazzoli \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{<fm2209@ic.ac.uk>}}}
246 \begin{minipage}{0.5\textwidth}
247 \begin{flushleft} \large
249 Dr. Steffen \textsc{van Backel}
252 \begin{minipage}{0.5\textwidth}
253 \begin{flushright} \large
255 Dr. Philippa \textsc{Gardner}
262 The marriage between programming and logic has been a very fertile one. In
263 particular, since the simply typed lambda calculus (STLC), a number of type
264 systems have been devised with increasing expressive power.
266 Among this systems, Inutitionistic Type Theory (ITT) has been a very
267 popular framework for theorem provers and programming languages.
268 However, equality has always been a tricky business in ITT and related
271 In these thesis we will explain why this is the case, and present
272 Observational Type Theory (OTT), a solution to some of the problems
273 with equality. We then describe $\mykant$, a theorem prover featuring
274 OTT in a setting more close to the one found in current systems.
275 Having implemented part of $\mykant$ as a Haskell program, we describe
276 some of the implementation issues faced.
281 \renewcommand{\abstractname}{Acknowledgements}
283 I would like to thank Steffen van Backel, my supervisor, who was brave
284 enough to believe in my project and who provided much advice and
287 I would also like to thank the Haskell and Agda community on
288 \texttt{IRC}, which guided me through the strange world of types; and
289 in particular Andrea Vezzosi and James Deikun, with whom I entertained
290 countless insightful discussions in the past year. Andrea suggested
291 Observational Type Theory as a topic of study: this thesis would not
294 Finally, much of the work stems from the research of Conor McBride,
295 who answered many of my doubts through these months. I also owe him
305 \section{Simple and not-so-simple types}
308 \subsection{The untyped $\lambda$-calculus}
310 Along with Turing's machines, the earliest attempts to formalise computation
311 lead to the $\lambda$-calculus \citep{Church1936}. This early programming
312 language encodes computation with a minimal syntax and no `data' in the
313 traditional sense, but just functions. Here we give a brief overview of the
314 language, which will give the chance to introduce concepts central to the
315 analysis of all the following calculi. The exposition follows the one found in
316 chapter 5 of \cite{Queinnec2003}.
318 The syntax of $\lambda$-terms consists of three things: variables, abstractions,
323 \begin{array}{r@{\ }c@{\ }l}
324 \mytmsyn & ::= & \myb{x} \mysynsep \myabs{\myb{x}}{\mytmsyn} \mysynsep (\myapp{\mytmsyn}{\mytmsyn}) \\
325 x & \in & \text{Some enumerable set of symbols}
330 Parenthesis will be omitted in the usual way:
331 $\myapp{\myapp{\mytmt}{\mytmm}}{\mytmn} =
332 \myapp{(\myapp{\mytmt}{\mytmm})}{\mytmn}$.
334 Abstractions roughly corresponds to functions, and their semantics is more
335 formally explained by the $\beta$-reduction rule:
337 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
340 \myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{\myb{x}}{\mytmn}\text{, where} \\
342 \begin{array}{l@{\ }c@{\ }l}
343 \mysub{\myb{x}}{\myb{x}}{\mytmn} & = & \mytmn \\
344 \mysub{\myb{y}}{\myb{x}}{\mytmn} & = & y\text{, with } \myb{x} \neq y \\
345 \mysub{(\myapp{\mytmt}{\mytmm})}{\myb{x}}{\mytmn} & = & (\myapp{\mysub{\mytmt}{\myb{x}}{\mytmn}}{\mysub{\mytmm}{\myb{x}}{\mytmn}}) \\
346 \mysub{(\myabs{\myb{x}}{\mytmm})}{\myb{x}}{\mytmn} & = & \myabs{\myb{x}}{\mytmm} \\
347 \mysub{(\myabs{\myb{y}}{\mytmm})}{\myb{x}}{\mytmn} & = & \myabs{\myb{z}}{\mysub{\mysub{\mytmm}{\myb{y}}{\myb{z}}}{\myb{x}}{\mytmn}}, \\
348 \multicolumn{3}{l}{\myind{1} \text{with $\myb{x} \neq \myb{y}$ and $\myb{z}$ not free in $\myapp{\mytmm}{\mytmn}$}}
354 The care required during substituting variables for terms is required to avoid
355 name capturing. We will use substitution in the future for other name-binding
356 constructs assuming similar precautions.
358 These few elements are of remarkable expressiveness, and in fact Turing
359 complete. As a corollary, we must be able to devise a term that reduces forever
360 (`loops' in imperative terms):
363 (\myapp{\omega}{\omega}) \myred (\myapp{\omega}{\omega}) \myred \cdots \text{, with $\omega = \myabs{x}{\myapp{x}{x}}$}
367 A \emph{redex} is a term that can be reduced. In the untyped $\lambda$-calculus
368 this will be the case for an application in which the first term is an
369 abstraction, but in general we call aterm reducible if it appears to the left of
370 a reduction rule. When a term contains no redexes it's said to be in
371 \emph{normal form}. Given the observation above, not all terms reduce to a
372 normal forms: we call the ones that do \emph{normalising}, and the ones that
373 don't \emph{non-normalising}.
375 The reduction rule presented is not syntax directed, but \emph{evaluation
376 strategies} can be employed to reduce term systematically. Common evaluation
377 strategies include \emph{call by value} (or \emph{strict}), where arguments of
378 abstractions are reduced before being applied to the abstraction; and conversely
379 \emph{call by name} (or \emph{lazy}), where we reduce only when we need to do so
380 to proceed---in other words when we have an application where the function is
381 still not a $\lambda$. In both these reduction strategies we never reduce under
382 an abstraction: for this reason a weaker form of normalisation is used, where
383 both abstractions and normal forms are said to be in \emph{weak head normal
386 \subsection{The simply typed $\lambda$-calculus}
388 A convenient way to `discipline' and reason about $\lambda$-terms is to assign
389 \emph{types} to them, and then check that the terms that we are forming make
390 sense given our typing rules \citep{Curry1934}. The first most basic instance
391 of this idea takes the name of \emph{simply typed $\lambda$ calculus}, whose
392 rules are shown in figure \ref{fig:stlc}.
394 Our types contain a set of \emph{type variables} $\Phi$, which might
395 correspond to some `primitive' types; and $\myarr$, the type former for
396 `arrow' types, the types of functions. The language is explicitly
397 typed: when we bring a variable into scope with an abstraction, we
398 declare its type. Reduction is unchanged from the untyped
404 \begin{array}{r@{\ }c@{\ }l}
405 \mytmsyn & ::= & \myb{x} \mysynsep \myabss{\myb{x}}{\mytysyn}{\mytmsyn} \mysynsep
406 (\myapp{\mytmsyn}{\mytmsyn}) \\
407 \mytysyn & ::= & \myse{\phi} \mysynsep \mytysyn \myarr \mytysyn \mysynsep \\
408 \myb{x} & \in & \text{Some enumerable set of symbols} \\
409 \myse{\phi} & \in & \Phi
414 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
416 \AxiomC{$\myctx(x) = A$}
417 \UnaryInfC{$\myjud{\myb{x}}{A}$}
420 \AxiomC{$\myjudd{\myctx;\myb{x} : A}{\mytmt}{\mytyb}$}
421 \UnaryInfC{$\myjud{\myabss{x}{A}{\mytmt}}{\mytyb}$}
424 \AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$}
425 \AxiomC{$\myjud{\mytmn}{\mytya}$}
426 \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mytyb}$}
430 \caption{Syntax and typing rules for the STLC. Reduction is unchanged from
431 the untyped $\lambda$-calculus.}
435 In the typing rules, a context $\myctx$ is used to store the types of bound
436 variables: $\myctx; \myb{x} : \mytya$ adds a variable to the context and
437 $\myctx(x)$ returns the type of the rightmost occurrence of $x$.
439 This typing system takes the name of `simply typed lambda calculus' (STLC), and
440 enjoys a number of properties. Two of them are expected in most type systems
443 \item[Progress] A well-typed term is not stuck---it is either a variable, or its
444 constructor does not appear on the left of the $\myred$ relation (currently
445 only $\lambda$), or it can take a step according to the evaluation rules.
446 \item[Preservation] If a well-typed term takes a step of evaluation, then the
447 resulting term is also well-typed, and preserves the previous type. Also
448 known as \emph{subject reduction}.
451 However, STLC buys us much more: every well-typed term is normalising
452 \citep{Tait1967}. It is easy to see that we can't fill the blanks if we want to
453 give types to the non-normalising term shown before:
455 \myapp{(\myabss{\myb{x}}{\myhole{?}}{\myapp{\myb{x}}{\myb{x}}})}{(\myabss{\myb{x}}{\myhole{?}}{\myapp{\myb{x}}{\myb{x}}})}
458 This makes the STLC Turing incomplete. We can recover the ability to loop by
459 adding a combinator that recurses:
462 \begin{minipage}{0.5\textwidth}
464 $ \mytmsyn ::= \cdots b \mysynsep \myfix{\myb{x}}{\mytysyn}{\mytmsyn} $
468 \begin{minipage}{0.5\textwidth}
469 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}} {
470 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytmt}{\mytya}$}
471 \UnaryInfC{$\myjud{\myfix{\myb{x}}{\mytya}{\mytmt}}{\mytya}$}
476 \mydesc{reduction:}{\myjud{\mytmsyn}{\mytmsyn}}{
477 $ \myfix{\myb{x}}{\mytya}{\mytmt} \myred \mysub{\mytmt}{\myb{x}}{(\myfix{\myb{x}}{\mytya}{\mytmt})}$
480 This will deprive us of normalisation, which is a particularly bad thing if we
481 want to use the STLC as described in the next section.
483 \subsection{The Curry-Howard correspondence}
485 It turns out that the STLC can be seen a natural deduction system for
486 intuitionistic propositional logic. Terms are proofs, and their types are the
487 propositions they prove. This remarkable fact is known as the Curry-Howard
488 correspondence, or isomorphism.
490 The arrow ($\myarr$) type corresponds to implication. If we wish to prove that
491 that $(\mytya \myarr \mytyb) \myarr (\mytyb \myarr \mytycc) \myarr (\mytya
492 \myarr \mytycc)$, all we need to do is to devise a $\lambda$-term that has the
495 \myabss{\myb{f}}{(\mytya \myarr \mytyb)}{\myabss{\myb{g}}{(\mytyb \myarr \mytycc)}{\myabss{\myb{x}}{\mytya}{\myapp{\myb{g}}{(\myapp{\myb{f}}{\myb{x}})}}}}
497 That is, function composition. Going beyond arrow types, we can extend our bare
498 lambda calculus with useful types to represent other logical constructs, as
499 shown in figure \ref{fig:natded}.
504 \begin{array}{r@{\ }c@{\ }l}
505 \mytmsyn & ::= & \cdots \\
506 & | & \mytt \mysynsep \myapp{\myabsurd{\mytysyn}}{\mytmsyn} \\
507 & | & \myapp{\myleft{\mytysyn}}{\mytmsyn} \mysynsep
508 \myapp{\myright{\mytysyn}}{\mytmsyn} \mysynsep
509 \myapp{\mycase{\mytmsyn}{\mytmsyn}}{\mytmsyn} \\
510 & | & \mypair{\mytmsyn}{\mytmsyn} \mysynsep
511 \myapp{\myfst}{\mytmsyn} \mysynsep \myapp{\mysnd}{\mytmsyn} \\
512 \mytysyn & ::= & \cdots \mysynsep \myunit \mysynsep \myempty \mysynsep \mytmsyn \mysum \mytmsyn \mysynsep \mytysyn \myprod \mytysyn
517 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
520 \begin{array}{l@{ }l@{\ }c@{\ }l}
521 \myapp{\mycase{\mytmm}{\mytmn}}{(\myapp{\myleft{\mytya} &}{\mytmt})} & \myred &
522 \myapp{\mytmm}{\mytmt} \\
523 \myapp{\mycase{\mytmm}{\mytmn}}{(\myapp{\myright{\mytya} &}{\mytmt})} & \myred &
524 \myapp{\mytmn}{\mytmt}
529 \begin{array}{l@{ }l@{\ }c@{\ }l}
530 \myapp{\myfst &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmm \\
531 \myapp{\mysnd &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmn
537 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
539 \AxiomC{\phantom{$\myjud{\mytmt}{\myempty}$}}
540 \UnaryInfC{$\myjud{\mytt}{\myunit}$}
543 \AxiomC{$\myjud{\mytmt}{\myempty}$}
544 \UnaryInfC{$\myjud{\myapp{\myabsurd{\mytya}}{\mytmt}}{\mytya}$}
551 \AxiomC{$\myjud{\mytmt}{\mytya}$}
552 \UnaryInfC{$\myjud{\myapp{\myleft{\mytyb}}{\mytmt}}{\mytya \mysum \mytyb}$}
555 \AxiomC{$\myjud{\mytmt}{\mytyb}$}
556 \UnaryInfC{$\myjud{\myapp{\myright{\mytya}}{\mytmt}}{\mytya \mysum \mytyb}$}
564 \AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$}
565 \AxiomC{$\myjud{\mytmn}{\mytya \myarr \mytycc}$}
566 \AxiomC{$\myjud{\mytmt}{\mytya \mysum \mytyb}$}
567 \TrinaryInfC{$\myjud{\myapp{\mycase{\mytmm}{\mytmn}}{\mytmt}}{\mytycc}$}
574 \AxiomC{$\myjud{\mytmm}{\mytya}$}
575 \AxiomC{$\myjud{\mytmn}{\mytyb}$}
576 \BinaryInfC{$\myjud{\mypair{\mytmm}{\mytmn}}{\mytya \myprod \mytyb}$}
579 \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
580 \UnaryInfC{$\myjud{\myapp{\myfst}{\mytmt}}{\mytya}$}
583 \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
584 \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mytyb}$}
588 \caption{Rules for the extendend STLC. Only the new features are shown, all the
589 rules and syntax for the STLC apply here too.}
593 Tagged unions (or sums, or coproducts---$\mysum$ here, \texttt{Either}
594 in Haskell) correspond to disjunctions, and dually tuples (or pairs, or
595 products---$\myprod$ here, tuples in Haskell) correspond to
596 conjunctions. This is apparent looking at the ways to construct and
597 destruct the values inhabiting those types: for $\mysum$ $\myleft{ }$
598 and $\myright{ }$ correspond to $\vee$ introduction, and
599 $\mycase{\myarg}{\myarg}$ to $\vee$ elimination; for $\myprod$
600 $\mypair{\myarg}{\myarg}$ corresponds to $\wedge$ introduction, $\myfst$
601 and $\mysnd$ to $\wedge$ elimination.
603 The trivial type $\myunit$ corresponds to the logical $\top$, and dually
604 $\myempty$ corresponds to the logical $\bot$. $\myunit$ has one introduction
605 rule ($\mytt$), and thus one inhabitant; and no eliminators. $\myempty$ has no
606 introduction rules, and thus no inhabitants; and one eliminator ($\myabsurd{
607 }$), corresponding to the logical \emph{ex falso quodlibet}.
609 With these rules, our STLC now looks remarkably similar in power and use to the
610 natural deduction we already know. $\myneg \mytya$ can be expressed as $\mytya
611 \myarr \myempty$. However, there is an important omission: there is no term of
612 the type $\mytya \mysum \myneg \mytya$ (excluded middle), or equivalently
613 $\myneg \myneg \mytya \myarr \mytya$ (double negation), or indeed any term with
614 a type equivalent to those.
616 This has a considerable effect on our logic and it's no coincidence, since there
617 is no obvious computational behaviour for laws like the excluded middle.
618 Theories of this kind are called \emph{intuitionistic}, or \emph{constructive},
619 and all the systems analysed will have this characteristic since they build on
620 the foundation of the STLC\footnote{There is research to give computational
621 behaviour to classical logic, but I will not touch those subjects.}.
623 As in logic, if we want to keep our system consistent, we must make sure that no
624 closed terms (in other words terms not under a $\lambda$) inhabit $\myempty$.
625 The variant of STLC presented here is indeed
626 consistent, a result that follows from the fact that it is
627 normalising. % TODO explain
628 Going back to our $\mysyn{fix}$ combinator, it is easy to see how it ruins our
629 desire for consistency. The following term works for every type $\mytya$,
632 (\myfix{\myb{x}}{\mytya}{\myb{x}}) : \mytya
635 \subsection{Inductive data}
638 To make the STLC more useful as a programming language or reasoning tool it is
639 common to include (or let the user define) inductive data types. These comprise
640 of a type former, various constructors, and an eliminator (or destructor) that
641 serves as primitive recursor.
643 For example, we might add a $\mylist$ type constructor, along with an `empty
644 list' ($\mynil{ }$) and `cons cell' ($\mycons$) constructor. The eliminator for
645 lists will be the usual folding operation ($\myfoldr$). See figure
651 \begin{array}{r@{\ }c@{\ }l}
652 \mytmsyn & ::= & \cdots \mysynsep \mynil{\mytysyn} \mysynsep \mytmsyn \mycons \mytmsyn
654 \myapp{\myapp{\myapp{\myfoldr}{\mytmsyn}}{\mytmsyn}}{\mytmsyn} \\
655 \mytysyn & ::= & \cdots \mysynsep \myapp{\mylist}{\mytysyn}
659 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
661 \begin{array}{l@{\ }c@{\ }l}
662 \myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{\mynil{\mytya}} & \myred & \mytmt \\
664 \myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{(\mytmm \mycons \mytmn)} & \myred &
665 \myapp{\myapp{\myse{f}}{\mytmm}}{(\myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{\mytmn})}
669 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
671 \AxiomC{\phantom{$\myjud{\mytmm}{\mytya}$}}
672 \UnaryInfC{$\myjud{\mynil{\mytya}}{\myapp{\mylist}{\mytya}}$}
675 \AxiomC{$\myjud{\mytmm}{\mytya}$}
676 \AxiomC{$\myjud{\mytmn}{\myapp{\mylist}{\mytya}}$}
677 \BinaryInfC{$\myjud{\mytmm \mycons \mytmn}{\myapp{\mylist}{\mytya}}$}
682 \AxiomC{$\myjud{\mysynel{f}}{\mytya \myarr \mytyb \myarr \mytyb}$}
683 \AxiomC{$\myjud{\mytmm}{\mytyb}$}
684 \AxiomC{$\myjud{\mytmn}{\myapp{\mylist}{\mytya}}$}
685 \TrinaryInfC{$\myjud{\myapp{\myapp{\myapp{\myfoldr}{\mysynel{f}}}{\mytmm}}{\mytmn}}{\mytyb}$}
688 \caption{Rules for lists in the STLC.}
692 In section \ref{sec:well-order} we will see how to give a general account of
693 inductive data. %TODO does this make sense to have here?
695 \section{Intuitionistic Type Theory}
698 \subsection{Extending the STLC}
700 The STLC can be made more expressive in various ways. \cite{Barendregt1991}
701 succinctly expressed geometrically how we can add expressivity:
705 & \lambda\omega \ar@{-}[rr]\ar@{-}'[d][dd]
706 & & \lambda C \ar@{-}[dd]
708 \lambda2 \ar@{-}[ur]\ar@{-}[rr]\ar@{-}[dd]
709 & & \lambda P2 \ar@{-}[ur]\ar@{-}[dd]
711 & \lambda\underline\omega \ar@{-}'[r][rr]
712 & & \lambda P\underline\omega
714 \lambda{\to} \ar@{-}[rr]\ar@{-}[ur]
715 & & \lambda P \ar@{-}[ur]
718 Here $\lambda{\to}$, in the bottom left, is the STLC. From there can move along
721 \item[Terms depending on types (towards $\lambda{2}$)] We can quantify over
722 types in our type signatures. For example, we can define a polymorphic
724 {\small\[\displaystyle
725 (\myabss{\myb{A}}{\mytyp}{\myabss{\myb{x}}{\myb{A}}{\myb{x}}}) : (\myb{A} : \mytyp) \myarr \myb{A} \myarr \myb{A}
727 The first and most famous instance of this idea has been System F. This form
728 of polymorphism and has been wildly successful, also thanks to a well known
729 inference algorithm for a restricted version of System F known as
730 Hindley-Milner. Languages like Haskell and SML are based on this discipline.
731 \item[Types depending on types (towards $\lambda{\underline{\omega}}$)] We have
732 type operators. For example we could define a function that given types $R$
733 and $\mytya$ forms the type that represents a value of type $\mytya$ in
734 continuation passing style: {\small\[\displaystyle(\myabss{\myb{A} \myar \myb{R}}{\mytyp}{(\myb{A}
735 \myarr \myb{R}) \myarr \myb{R}}) : \mytyp \myarr \mytyp \myarr \mytyp\]}
736 \item[Types depending on terms (towards $\lambda{P}$)] Also known as `dependent
737 types', give great expressive power. For example, we can have values of whose
738 type depend on a boolean:
739 {\small\[\displaystyle(\myabss{\myb{x}}{\mybool}{\myite{\myb{x}}{\mynat}{\myrat}}) : \mybool
743 All the systems preserve the properties that make the STLC well behaved. The
744 system we are going to focus on, Intuitionistic Type Theory, has all of the
745 above additions, and thus would sit where $\lambda{C}$ sits in the
746 `$\lambda$-cube'. It will serve as the logical `core' of all the other
747 extensions that we will present and ultimately our implementation of a similar
750 \subsection{A Bit of History}
752 Logic frameworks and programming languages based on type theory have a long
753 history. Per Martin-L\"{o}f described the first version of his theory in 1971,
754 but then revised it since the original version was inconsistent due to its
755 impredicativity\footnote{In the early version there was only one universe
756 $\mytyp$ and $\mytyp : \mytyp$, see section \ref{sec:term-types} for an
757 explanation on why this causes problems.}. For this reason he gave a revised
758 and consistent definition later \citep{Martin-Lof1984}.
760 A related development is the polymorphic $\lambda$-calculus, and specifically
761 the previously mentioned System F, which was developed independently by Girard
762 and Reynolds. An overview can be found in \citep{Reynolds1994}. The surprising
763 fact is that while System F is impredicative it is still consistent and strongly
764 normalising. \cite{Coquand1986} further extended this line of work with the
765 Calculus of Constructions (CoC).
767 Most widely used interactive theorem provers are based on ITT. Popular ones
768 include Agda \citep{Norell2007, Bove2009}, Coq \citep{Coq}, and Epigram
769 \citep{McBride2004, EpigramTut}.
771 \subsection{A note on inference}
773 % TODO do this, adding links to the sections about bidi type checking and
774 % implicit universes.
775 In the following text I will often omit explicit typing for abstractions or
777 Moreover, I will use $\mytyp$ without bothering to specify a
778 universe, with the silent assumption that the definition is consistent
779 regarding to the hierarchy.
781 \subsection{A simple type theory}
784 The calculus I present follows the exposition in \citep{Thompson1991},
785 and is quite close to the original formulation of predicative ITT as
786 found in \citep{Martin-Lof1984}. The system's syntax and reduction
787 rules are presented in their entirety in figure \ref{fig:core-tt-syn}.
788 The typing rules are presented piece by piece. Agda and \mykant\
789 renditions of the presented theory and all the examples is reproduced in
790 appendix \ref{app:itt-code}.
795 \begin{array}{r@{\ }c@{\ }l}
796 \mytmsyn & ::= & \myb{x} \mysynsep
798 \myunit \mysynsep \mytt \mysynsep
799 \myempty \mysynsep \myapp{\myabsurd{\mytmsyn}}{\mytmsyn} \\
800 & | & \mybool \mysynsep \mytrue \mysynsep \myfalse \mysynsep
801 \myitee{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
802 & | & \myfora{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
803 \myabss{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
804 (\myapp{\mytmsyn}{\mytmsyn}) \\
805 & | & \myexi{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
806 \mypairr{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn} \\
807 & | & \myapp{\myfst}{\mytmsyn} \mysynsep \myapp{\mysnd}{\mytmsyn} \\
808 & | & \myw{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
809 \mytmsyn \mynode{\myb{x}}{\mytmsyn} \mytmsyn \\
810 & | & \myrec{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn} \\
816 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
819 \begin{array}{l@{ }l@{\ }c@{\ }l}
820 \myitee{\mytrue &}{\myb{x}}{\myse{P}}{\mytmm}{\mytmn} & \myred & \mytmm \\
821 \myitee{\myfalse &}{\myb{x}}{\myse{P}}{\mytmm}{\mytmn} & \myred & \mytmn \\
826 \myapp{(\myabss{\myb{x}}{\mytya}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{\myb{x}}{\mytmn}
830 \begin{array}{l@{ }l@{\ }c@{\ }l}
831 \myapp{\myfst &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmm \\
832 \myapp{\mysnd &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmn
840 \myrec{(\myse{s} \mynode{\myb{x}}{\myse{T}} \myse{f})}{\myb{y}}{\myse{P}}{\myse{p}} \myred
841 \myapp{\myapp{\myapp{\myse{p}}{\myse{s}}}{\myse{f}}}{(\myabss{\myb{t}}{\mysub{\myse{T}}{\myb{x}}{\myse{s}}}{
842 \myrec{\myapp{\myse{f}}{\myb{t}}}{\myb{y}}{\myse{P}}{\mytmt}
846 \caption{Syntax and reduction rules for our type theory.}
847 \label{fig:core-tt-syn}
850 \subsubsection{Types are terms, some terms are types}
851 \label{sec:term-types}
853 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
855 \AxiomC{$\myjud{\mytmt}{\mytya}$}
856 \AxiomC{$\mytya \mydefeq \mytyb$}
857 \BinaryInfC{$\myjud{\mytmt}{\mytyb}$}
860 \AxiomC{\phantom{$\myjud{\mytmt}{\mytya}$}}
861 \UnaryInfC{$\myjud{\mytyp_l}{\mytyp_{l + 1}}$}
866 The first thing to notice is that a barrier between values and types that we had
867 in the STLC is gone: values can appear in types, and the two are treated
868 uniformly in the syntax.
870 While the usefulness of doing this will become clear soon, a consequence is
871 that since types can be the result of computation, deciding type equality is
872 not immediate as in the STLC. For this reason we define \emph{definitional
873 equality}, $\mydefeq$, as the congruence relation extending
874 $\myred$---moreover, when comparing types syntactically we do it up to
875 renaming of bound names ($\alpha$-renaming). For example under this
876 discipline we will find that
878 \myabss{\myb{x}}{\mytya}{\myb{x}} \mydefeq \myabss{\myb{y}}{\mytya}{\myb{y}}
880 Types that are definitionally equal can be used interchangeably. Here
881 the `conversion' rule is not syntax directed, but it is possible to
882 employ $\myred$ to decide term equality in a systematic way, by always
883 reducing terms to their normal forms before comparing them, so that a
884 separate conversion rule is not needed. % TODO add section
885 Another thing to notice is that considering the need to reduce terms to
886 decide equality, it is essential for a dependently type system to be
887 terminating and confluent for type checking to be decidable.
889 Moreover, we specify a \emph{type hierarchy} to talk about `large'
890 types: $\mytyp_0$ will be the type of types inhabited by data:
891 $\mybool$, $\mynat$, $\mylist$, etc. $\mytyp_1$ will be the type of
892 $\mytyp_0$, and so on---for example we have $\mytrue : \mybool :
893 \mytyp_0 : \mytyp_1 : \cdots$. Each type `level' is often called a
894 universe in the literature. While it is possible to simplify things by
895 having only one universe $\mytyp$ with $\mytyp : \mytyp$, this plan is
896 inconsistent for much the same reason that impredicative na\"{\i}ve set
897 theory is \citep{Hurkens1995}. However various techniques can be
898 employed to lift the burden of explicitly handling universes, as we will
899 see in section \ref{sec:term-hierarchy}.
901 \subsubsection{Contexts}
903 \begin{minipage}{0.5\textwidth}
904 \mydesc{context validity:}{\myvalid{\myctx}}{
906 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
907 \UnaryInfC{$\myvalid{\myemptyctx}$}
910 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
911 \UnaryInfC{$\myvalid{\myctx ; \myb{x} : \mytya}$}
916 \begin{minipage}{0.5\textwidth}
917 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
918 \AxiomC{$\myctx(x) = \mytya$}
919 \UnaryInfC{$\myjud{\myb{x}}{\mytya}$}
925 We need to refine the notion context to make sure that every variable appearing
926 is typed correctly, or that in other words each type appearing in the context is
927 indeed a type and not a value. In every other rule, if no premises are present,
928 we assume the context in the conclusion to be valid.
930 Then we can re-introduce the old rule to get the type of a variable for a
933 \subsubsection{$\myunit$, $\myempty$}
935 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
937 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
938 \UnaryInfC{$\myjud{\myunit}{\mytyp_0}$}
940 \UnaryInfC{$\myjud{\myempty}{\mytyp_0}$}
943 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
944 \UnaryInfC{$\myjud{\mytt}{\myunit}$}
946 \UnaryInfC{\phantom{$\myjud{\myempty}{\mytyp_0}$}}
949 \AxiomC{$\myjud{\mytmt}{\myempty}$}
950 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
951 \BinaryInfC{$\myjud{\myapp{\myabsurd{\mytya}}{\mytmt}}{\mytya}$}
953 \UnaryInfC{\phantom{$\myjud{\myempty}{\mytyp_0}$}}
958 Nothing surprising here: $\myunit$ and $\myempty$ are unchanged from the STLC,
959 with the added rules to type $\myunit$ and $\myempty$ themselves, and to make
960 sure that we are invoking $\myabsurd{}$ over a type.
962 \subsubsection{$\mybool$, and dependent $\myfun{if}$}
964 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
967 \UnaryInfC{$\myjud{\mybool}{\mytyp_0}$}
971 \UnaryInfC{$\myjud{\mytrue}{\mybool}$}
975 \UnaryInfC{$\myjud{\myfalse}{\mybool}$}
980 \AxiomC{$\myjud{\mytmt}{\mybool}$}
981 \AxiomC{$\myjudd{\myctx : \mybool}{\mytya}{\mytyp_l}$}
983 \BinaryInfC{$\myjud{\mytmm}{\mysub{\mytya}{x}{\mytrue}}$ \hspace{0.7cm} $\myjud{\mytmn}{\mysub{\mytya}{x}{\myfalse}}$}
984 \UnaryInfC{$\myjud{\myitee{\mytmt}{\myb{x}}{\mytya}{\mytmm}{\mytmn}}{\mysub{\mytya}{\myb{x}}{\mytmt}}$}
988 With booleans we get the first taste of the `dependent' in `dependent
989 types'. While the two introduction rules ($\mytrue$ and $\myfalse$) are
990 not surprising, the typing rules for $\myfun{if}$ are. In most strongly
991 typed languages we expect the branches of an $\myfun{if}$ statements to
992 be of the same type, to preserve subject reduction, since execution
993 could take both paths. This is a pity, since the type system does not
994 reflect the fact that in each branch we gain knowledge on the term we
995 are branching on. Which means that programs along the lines of
997 \begin{verbatim}if null xs then head xs else 0
999 are a necessary, well typed, danger.
1001 However, in a more expressive system, we can do better: the branches' type can
1002 depend on the value of the scrutinised boolean. This is what the typing rule
1003 expresses: the user provides a type $\mytya$ ranging over an $\myb{x}$
1004 representing the scrutinised boolean type, and the branches are typechecked with
1005 the updated knowledge on the value of $\myb{x}$.
1007 \subsubsection{$\myarr$, or dependent function}
1009 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1010 \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
1011 \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
1012 \BinaryInfC{$\myjud{\myfora{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
1018 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytmt}{\mytyb}$}
1019 \UnaryInfC{$\myjud{\myabss{\myb{x}}{\mytya}{\mytmt}}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
1022 \AxiomC{$\myjud{\mytmm}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
1023 \AxiomC{$\myjud{\mytmn}{\mytya}$}
1024 \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mysub{\mytyb}{\myb{x}}{\mytmn}}$}
1029 Dependent functions are one of the two key features that perhaps most
1030 characterise dependent types---the other being dependent products. With
1031 dependent functions, the result type can depend on the value of the
1032 argument. This feature, together with the fact that the result type
1033 might be a type itself, brings a lot of interesting possibilities.
1034 Following this intuition, in the introduction rule, the return type is
1035 typechecked in a context with an abstracted variable of lhs' type, and
1036 in the elimination rule the actual argument is substituted in the return
1037 type. Keeping the correspondence with logic alive, dependent functions
1038 are much like universal quantifiers ($\forall$) in logic.
1040 For example, assuming that we have lists and natural numbers in our
1041 language, using dependent functions we would be able to
1045 \myfun{length} : (\myb{A} {:} \mytyp_0) \myarr \myapp{\mylist}{\myb{A}} \myarr \mynat \\
1046 \myarg \myfun{$>$} \myarg : \mynat \myarr \mynat \myarr \mytyp_0 \\
1047 \myfun{head} : (\myb{A} {:} \mytyp_0) \myarr (\myb{l} {:} \myapp{\mylist}{\myb{A}})
1048 \myarr \myapp{\myapp{\myfun{length}}{\myb{A}}}{\myb{l}} \mathrel{\myfun{>}} 0 \myarr
1053 \myfun{length} is the usual polymorphic length function. $\myfun{>}$ is
1054 a function that takes two naturals and returns a type: if the lhs is
1055 greater then the rhs, $\myunit$ is returned, $\myempty$ otherwise. This
1056 way, we can express a `non-emptyness' condition in $\myfun{head}$, by
1057 including a proof that the length of the list argument is non-zero.
1058 This allows us to rule out the `empty list' case, so that we can safely
1059 return the first element.
1061 Again, we need to make sure that the type hierarchy is respected, which is the
1062 reason why a type formed by $\myarr$ will live in the least upper bound of the
1063 levels of argument and return type. This trend will continue with the other
1064 type-level binders, $\myprod$ and $\mytyc{W}$.
1066 \subsubsection{$\myprod$, or dependent product}
1069 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1070 \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
1071 \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
1072 \BinaryInfC{$\myjud{\myexi{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
1078 \AxiomC{$\myjud{\mytmm}{\mytya}$}
1079 \AxiomC{$\myjud{\mytmn}{\mysub{\mytyb}{\myb{x}}{\mytmm}}$}
1080 \BinaryInfC{$\myjud{\mypairr{\mytmm}{\myb{x}}{\mytyb}{\mytmn}}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
1082 \UnaryInfC{\phantom{$--$}}
1085 \AxiomC{$\myjud{\mytmt}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
1086 \UnaryInfC{$\hspace{0.7cm}\myjud{\myapp{\myfst}{\mytmt}}{\mytya}\hspace{0.7cm}$}
1088 \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mysub{\mytyb}{\myb{x}}{\myapp{\myfst}{\mytmt}}}$}
1093 If dependent functions are a generalisation of $\myarr$ in the STLC,
1094 dependent products are a generalisation of $\myprod$ in the STLC. The
1095 improvement is that the second element's type can depend on the value of
1096 the first element. The corrispondence with logic is through the
1097 existential quantifier: $\exists x \in \mathbb{N}. even(x)$ can be
1098 expressed as $\myexi{\myb{x}}{\mynat}{\myapp{\myfun{even}}{\myb{x}}}$.
1099 The first element will be a number, and the second evidence that the
1100 number is even. This highlights the fact that we are working in a
1101 constructive logic: if we have an existence proof, we can always ask for
1102 a witness. This means, for instance, that $\neg \forall \neg$ is not
1103 equivalent to $\exists$.
1105 Another perhaps more `dependent' application of products, paired with
1106 $\mybool$, is to offer choice between different types. For example we
1107 can easily recover disjunctions:
1110 \myarg\myfun{$\vee$}\myarg : \mytyp_0 \myarr \mytyp_0 \myarr \mytyp_0 \\
1111 \myb{A} \mathrel{\myfun{$\vee$}} \myb{B} \mapsto \myexi{\myb{x}}{\mybool}{\myite{\myb{x}}{\myb{A}}{\myb{B}}} \\ \ \\
1112 \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} \\
1113 \myfun{case} \myappsp \myb{A} \myappsp \myb{B} \myappsp \myb{C} \myappsp \myb{f} \myappsp \myb{g} \myappsp \myb{x} \mapsto \\
1114 \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}})}
1118 \subsubsection{$\mytyc{W}$, or well-order}
1119 \label{sec:well-order}
1121 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1122 \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
1123 \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
1124 \BinaryInfC{$\myjud{\myw{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
1129 \AxiomC{$\myjud{\mytmt}{\mytya}$}
1130 \AxiomC{$\myjud{\mysynel{f}}{\mysub{\mytyb}{\myb{x}}{\mytmt} \myarr \myw{\myb{x}}{\mytya}{\mytyb}}$}
1131 \BinaryInfC{$\myjud{\mytmt \mynode{\myb{x}}{\mytyb} \myse{f}}{\myw{\myb{x}}{\mytya}{\mytyb}}$}
1136 \AxiomC{$\myjud{\myse{u}}{\myw{\myb{x}}{\myse{S}}{\myse{T}}}$}
1137 \AxiomC{$\myjudd{\myctx; \myb{w} : \myw{\myb{x}}{\myse{S}}{\myse{T}}}{\myse{P}}{\mytyp_l}$}
1139 \BinaryInfC{$\myjud{\myse{p}}{
1140 \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}}}}
1142 \UnaryInfC{$\myjud{\myrec{\myse{u}}{\myb{w}}{\myse{P}}{\myse{p}}}{\mysub{\myse{P}}{\myb{w}}{\myse{u}}}$}
1146 Finally, the well-order type, or in short $\mytyc{W}$-type, which will
1147 let us represent inductive data in a general (but clumsy) way. The core
1151 \section{The struggle for equality}
1152 \label{sec:equality}
1154 In the previous section we saw how a type checker (or a human) needs a
1155 notion of \emph{definitional equality}. Beyond this meta-theoretic
1156 notion, in this section we will explore the ways of expressing equality
1157 \emph{inside} the theory, as a reasoning tool available to the user.
1158 This area is the main concern of this thesis, and in general a very
1159 active research topic, since we do not have a fully satisfactory
1160 solution, yet. As in the previous section, everything presented is
1161 formalised in Agda in appendix \ref{app:agda-itt}.
1163 \subsection{Propositional equality}
1166 \begin{minipage}{0.5\textwidth}
1169 \begin{array}{r@{\ }c@{\ }l}
1170 \mytmsyn & ::= & \cdots \\
1171 & | & \mytmsyn \mypeq{\mytmsyn} \mytmsyn \mysynsep
1172 \myapp{\myrefl}{\mytmsyn} \\
1173 & | & \myjeq{\mytmsyn}{\mytmsyn}{\mytmsyn}
1178 \begin{minipage}{0.5\textwidth}
1179 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
1181 \myjeq{\myse{P}}{(\myapp{\myrefl}{\mytmm})}{\mytmn} \myred \mytmn
1187 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1188 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
1189 \AxiomC{$\myjud{\mytmm}{\mytya}$}
1190 \AxiomC{$\myjud{\mytmn}{\mytya}$}
1191 \TrinaryInfC{$\myjud{\mytmm \mypeq{\mytya} \mytmn}{\mytyp_l}$}
1197 \AxiomC{$\begin{array}{c}\ \\\myjud{\mytmm}{\mytya}\hspace{1.1cm}\mytmm \mydefeq \mytmn\end{array}$}
1198 \UnaryInfC{$\myjud{\myapp{\myrefl}{\mytmm}}{\mytmm \mypeq{\mytya} \mytmn}$}
1203 \myjud{\myse{P}}{\myfora{\myb{x}\ \myb{y}}{\mytya}{\myfora{q}{\myb{x} \mypeq{\mytya} \myb{y}}{\mytyp_l}}} \\
1204 \myjud{\myse{q}}{\mytmm \mypeq{\mytya} \mytmn}\hspace{1.1cm}\myjud{\myse{p}}{\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmm}}{(\myapp{\myrefl}{\mytmm})}}
1207 \UnaryInfC{$\myjud{\myjeq{\myse{P}}{\myse{q}}{\myse{p}}}{\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmn}}{q}}$}
1212 To express equality between two terms inside ITT, the obvious way to do so is
1213 to have the equality construction to be a type-former. Here we present what
1214 has survived as the dominating form of equality in systems based on ITT up to
1217 Our type former is $\mypeq{\mytya}$, which given a type (in this case
1218 $\mytya$) relates equal terms of that type. $\mypeq{}$ has one introduction
1219 rule, $\myrefl$, which introduces an equality relation between definitionally
1222 Finally, we have one eliminator for $\mypeq{}$, $\myjeqq$. $\myjeq{\myse{P}}{\myse{q}}{\myse{p}}$ takes
1224 \item $\myse{P}$, a predicate working with two terms of a certain type (say
1225 $\mytya$) and a proof of their equality
1226 \item $\myse{q}$, a proof that two terms in $\mytya$ (say $\myse{m}$ and
1227 $\myse{n}$) are equal
1228 \item and $\myse{p}$, an inhabitant of $\myse{P}$ applied to $\myse{m}$, plus
1229 the trivial proof by reflexivity showing that $\myse{m}$ is equal to itself
1231 Given these ingredients, $\myjeqq$ retuns a member of $\myse{P}$ applied to
1232 $\mytmm$, $\mytmn$, and $\myse{q}$. In other words $\myjeqq$ takes a
1233 witness that $\myse{P}$ works with \emph{definitionally equal} terms, and
1234 returns a witness of $\myse{P}$ working with \emph{propositionally equal}
1235 terms. Invokations of $\myjeqq$ will vanish when the equality proofs will
1236 reduce to invocations to reflexivity, at which point the arguments must be
1237 definitionally equal, and thus the provided
1238 $\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmm}}{(\myapp{\myrefl}{\mytmm})}$
1241 While the $\myjeqq$ rule is slightly convoluted, ve can derive many more
1242 `friendly' rules from it, for example a more obvious `substitution' rule, that
1243 replaces equal for equal in predicates:
1246 \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}}}}} \\
1247 \myfun{subst}\myappsp \myb{A}\myappsp\myb{P}\myappsp\myb{x}\myappsp\myb{y}\myappsp\myb{q}\myappsp\myb{p} \mapsto
1248 \myjeq{(\myabs{\myb{x}\ \myb{y}\ \myb{q}}{\myapp{\myb{P}}{\myb{y}}})}{\myb{p}}{\myb{q}}
1251 Once we have $\myfun{subst}$, we can easily prove more familiar laws regarding
1252 equality, such as symmetry, transitivity, and a congruence law.
1256 \subsection{Common extensions}
1258 Our definitional equality can be made larger in various ways, here we
1259 review some common extensions.
1261 \subsubsection{Congruence laws and $\eta$-expansion}
1263 A simple type-directed check that we can do on functions and records is
1264 $\eta$-expansion. We can then have
1266 \mydesc{definitional equality:}{\myjud{\mytmm \mydefeq \mytmn}{\mytmsyn}}{
1268 \AxiomC{$\myjud{f \mydefeq (\myabss{\myb{x}}{\mytya}{\myapp{\myse{g}}{\myb{x}}})}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
1269 \UnaryInfC{$\myjud{\myse{f} \mydefeq \myse{g}}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
1272 \AxiomC{$\myjud{\mytmm \mydefeq \mypair{\myapp{\myfst}{\mytmn}}{\myapp{\mysnd}{\mytmn}}}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
1273 \UnaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
1279 \AxiomC{$\myjud{\mytmm}{\myunit}$}
1280 \AxiomC{$\myjud{\mytmn}{\myunit}$}
1281 \BinaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\myunit}$}
1285 % \mydesc{definitional equality:}{\mytmsyn \mydefeq \mytmsyn}{
1286 % \begin{tabular}{cc}
1294 \subsubsection{Uniqueness of identity proofs}
1296 % TODO reference the fact that J does not imply J
1297 % TODO mention univalence
1300 \mydesc{definitional equality:}{\myjud{\mytmm \mydefeq \mytmn}{\mytmsyn}}{
1303 \myjud{\myse{P}}{\myfora{\myb{x}}{\mytya}{\myb{x} \mypeq{\mytya} \myb{x} \myarr \mytyp}} \\\
1304 \myjud{\myse{p}}{\myfora{\myb{x}}{\mytya}{\myse{P} \myappsp \myb{x} \myappsp \myb{x} \myappsp (\myrefl \myapp \myb{x})}} \hspace{1cm}
1305 \myjud{\mytmt}{\mytya} \hspace{1cm}
1306 \myjud{\myse{q}}{\mytmt \mypeq{\mytya} \mytmt}
1309 \UnaryInfC{$\myjud{\myfun{K} \myappsp \myse{P} \myappsp \myse{p} \myappsp \myse{t} \myappsp \myse{q}}{\myse{P} \myappsp \mytmt \myappsp \myse{q}}$}
1313 \subsection{Limitations}
1315 \epigraph{\emph{Half of my time spent doing research involves thinking up clever
1316 schemes to avoid needing functional extensionality.}}{@larrytheliquid}
1318 However, propositional equality as described is quite restricted when
1319 reasoning about equality beyond the term structure, which is what definitional
1320 equality gives us (extension notwithstanding).
1322 The problem is best exemplified by \emph{function extensionality}. In
1323 mathematics, we would expect to be able to treat functions that give equal
1324 output for equal input as the same. When reasoning in a mechanised framework
1325 we ought to be able to do the same: in the end, without considering the
1326 operational behaviour, all functions equal extensionally are going to be
1327 replaceable with one another.
1329 However this is not the case, or in other words with the tools we have we have
1332 \myfun{ext} : \myfora{\myb{A}\ \myb{B}}{\mytyp}{\myfora{\myb{f}\ \myb{g}}{
1333 \myb{A} \myarr \myb{B}}{
1334 (\myfora{\myb{x}}{\myb{A}}{\myapp{\myb{f}}{\myb{x}} \mypeq{\myb{B}} \myapp{\myb{g}}{\myb{x}}}) \myarr
1335 \myb{f} \mypeq{\myb{A} \myarr \myb{B}} \myb{g}
1339 To see why this is the case, consider the functions
1340 {\small\[\myabs{\myb{x}}{0 \mathrel{\myfun{+}} \myb{x}}$ and $\myabs{\myb{x}}{\myb{x} \mathrel{\myfun{+}} 0}\]}
1341 where $\myfun{+}$ is defined by recursion on the first argument,
1342 gradually destructing it to build up successors of the second argument.
1343 The two functions are clearly extensionally equal, and we can in fact
1346 \myfora{\myb{x}}{\mynat}{(0 \mathrel{\myfun{+}} \myb{x}) \mypeq{\mynat} (\myb{x} \mathrel{\myfun{+}} 0)}
1348 By analysis on the $\myb{x}$. However, the two functions are not
1349 definitionally equal, and thus we won't be able to get rid of the
1352 For the reasons above, theories that offer a propositional equality
1353 similar to what we presented are called \emph{intensional}, as opposed
1354 to \emph{extensional}. Most systems in wide use today (such as Agda,
1355 Coq, and Epigram) are of this kind.
1357 This is quite an annoyance that often makes reasoning awkward to execute. It
1358 also extends to other fields, for example proving bisimulation between
1359 processes specified by coinduction, or in general proving equivalences based
1360 on the behaviour on a term.
1362 \subsection{Equality reflection}
1364 One way to `solve' this problem is by identifying propositional equality with
1365 definitional equality:
1367 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1368 \AxiomC{$\myjud{\myse{q}}{\mytmm \mypeq{\mytya} \mytmn}$}
1369 \UnaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\mytya}$}
1373 This rule takes the name of \emph{equality reflection}, and is a very
1374 different rule from the ones we saw up to now: it links a typing judgement
1375 internal to the type theory to a meta-theoretic judgement that the type
1376 checker uses to work with terms. It is easy to see the dangerous consequences
1379 \item The rule is syntax directed, and the type checker is presumably expected
1380 to come up with equality proofs when needed.
1381 \item More worryingly, type checking becomes undecidable also because
1382 computing under false assumptions becomes unsafe.
1383 Consider for example
1385 \myabss{\myb{q}}{\mytya \mypeq{\mytyp} (\mytya \myarr \mytya)}{\myhole{?}}
1387 Using the assumed proof in tandem with equality reflection we could easily
1388 write a classic Y combinator, sending the compiler into a loop.
1391 Given these facts theories employing equality reflection, like NuPRL
1392 \citep{NuPRL}, carry the derivations that gave rise to each typing judgement
1393 to keep the systems manageable. % TODO more info, problems with that.
1395 For all its faults, equality reflection does allow us to prove extensionality,
1396 using the extensions we gave above. Assuming that $\myctx$ contains
1397 {\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}}}\]}
1401 \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}$}
1402 \RightLabel{equality reflection}
1403 \UnaryInfC{$\myjudd{\myctx; \myb{x} : \myb{A}}{\myapp{\myb{f}}{\myb{x}} \mydefeq \myapp{\myb{g}}{\myb{x}}}{\myb{B}}$}
1404 \RightLabel{congruence for $\lambda$s}
1405 \UnaryInfC{$\myjud{(\myabs{\myb{x}}{\myapp{\myb{f}}{\myb{x}}}) \mydefeq (\myabs{\myb{x}}{\myapp{\myb{g}}{\myb{x}}})}{\myb{A} \myarr \myb{B}}$}
1406 \RightLabel{$\eta$-law for $\lambda$}
1407 \UnaryInfC{$\hspace{1.45cm}\myjud{\myb{f} \mydefeq \myb{g}}{\myb{A} \myarr \myb{B}}\hspace{1.45cm}$}
1408 \RightLabel{$\myrefl$}
1409 \UnaryInfC{$\myjud{\myapp{\myrefl}{\myb{f}}}{\myb{f} \mypeq{} \myb{g}}$}
1412 Now, the question is: do we need to give up well-behavedness of our theory to
1413 gain extensionality?
1415 \subsection{Some alternatives}
1417 % TODO add `extentional axioms' (Hoffman), setoid models (Thorsten)
1419 \section{Observational equality}
1422 A recent development by \citet{Altenkirch2007}, \emph{Observational Type
1423 Theory} (OTT), promises to keep the well behavedness of ITT while
1424 being able to gain many useful equality proofs\footnote{It is suspected
1425 that OTT gains \emph{all} the equality proofs of ETT, but no proof
1426 exists yet.}, including function extensionality. The main idea is to
1427 give the user the possibility to \emph{coerce} (or transport) values
1428 from a type $\mytya$ to a type $\mytyb$, if the type checker can prove
1429 structurally that $\mytya$ and $\mytya$ are equal; and providing a
1430 value-level equality based on similar principles. Here we give an
1431 exposition which follows closely the original paper.
1433 \subsection{A simpler theory, a propositional fragment}
1436 $\mytyp_l$ is replaced by $\mytyp$. \\\ \\
1438 \begin{array}{r@{\ }c@{\ }l}
1439 \mytmsyn & ::= & \cdots \mysynsep \myprdec{\myprsyn} \mysynsep
1440 \myITE{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
1441 \myprsyn & ::= & \mybot \mysynsep \mytop \mysynsep \myprsyn \myand \myprsyn
1442 \mysynsep \myprfora{\myb{x}}{\mytmsyn}{\myprsyn}
1447 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1449 \AxiomC{$\myjud{\myse{P}}{\myprop}$}
1450 \UnaryInfC{$\myjud{\myprdec{\myse{P}}}{\mytyp}$}
1453 \AxiomC{$\myjud{\mytmt}{\mybool}$}
1454 \AxiomC{$\myjud{\mytya}{\mytyp}$}
1455 \AxiomC{$\myjud{\mytyb}{\mytyp}$}
1456 \TrinaryInfC{$\myjud{\myITE{\mytmt}{\mytya}{\mytyb}}{\mytyp}$}
1461 \mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
1463 \AxiomC{\phantom{$\myjud{\myse{P}}{\myprop}$}}
1464 \UnaryInfC{$\myjud{\mytop}{\myprop}$}
1466 \UnaryInfC{$\myjud{\mybot}{\myprop}$}
1469 \AxiomC{$\myjud{\myse{P}}{\myprop}$}
1470 \AxiomC{$\myjud{\myse{Q}}{\myprop}$}
1471 \BinaryInfC{$\myjud{\myse{P} \myand \myse{Q}}{\myprop}$}
1473 \UnaryInfC{\phantom{$\myjud{\mybot}{\myprop}$}}
1479 \AxiomC{$\myjud{\myse{A}}{\mytyp}$}
1480 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\myse{P}}{\myprop}$}
1481 \BinaryInfC{$\myjud{\myprfora{\myb{x}}{\mytya}{\myse{P}}}{\myprop}$}
1485 Our foundation will be a type theory like the one of section
1486 \ref{sec:itt}, with only one level: $\mytyp_0$. In this context we will
1487 drop the $0$ and call $\mytyp_0$ $\mytyp$. Moreover, since the old
1488 $\myfun{if}\myarg\myfun{then}\myarg\myfun{else}$ was able to return
1489 types thanks to the hierarchy (which is gone), we need to reintroduce an
1490 ad-hoc conditional for types, where the reduction rule is the obvious
1493 However, we have an addition: a universe of \emph{propositions},
1494 $\myprop$. $\myprop$ isolates a fragment of types at large, and
1495 indeed we can `inject' any $\myprop$ back in $\mytyp$ with $\myprdec{\myarg}$: \\
1496 \mydesc{proposition decoding:}{\myprdec{\mytmsyn} \myred \mytmsyn}{
1499 \begin{array}{l@{\ }c@{\ }l}
1500 \myprdec{\mybot} & \myred & \myempty \\
1501 \myprdec{\mytop} & \myred & \myunit
1506 \begin{array}{r@{ }c@{ }l@{\ }c@{\ }l}
1507 \myprdec{&\myse{P} \myand \myse{Q} &} & \myred & \myprdec{\myse{P}} \myprod \myprdec{\myse{Q}} \\
1508 \myprdec{&\myprfora{\myb{x}}{\mytya}{\myse{P}} &} & \myred &
1509 \myfora{\myb{x}}{\mytya}{\myprdec{\myse{P}}}
1514 Propositions are what we call the types of \emph{proofs}, or types
1515 whose inhabitants contain no `data', much like $\myunit$. The goal of
1516 doing this is twofold: erasing all top-level propositions when
1517 compiling; and to identify all equivalent propositions as the same, as
1520 Why did we choose what we have in $\myprop$? Given the above
1521 criteria, $\mytop$ obviously fits the bill. A pair of propositions
1522 $\myse{P} \myand \myse{Q}$ still won't get us data. Finally, if
1523 $\myse{P}$ is a proposition and we have
1524 $\myprfora{\myb{x}}{\mytya}{\myse{P}}$ , the decoding will be a
1525 function which returns propositional content. The only threat is
1526 $\mybot$, by which we can fabricate anything we want: however if we
1527 are consistent there will be nothing of type $\mybot$ at the top
1528 level, which is what we care about regarding proof erasure.
1530 \subsection{Equality proofs}
1534 \begin{array}{r@{\ }c@{\ }l}
1535 \mytmsyn & ::= & \cdots \mysynsep
1536 \mycoee{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \mysynsep
1537 \mycohh{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
1538 \myprsyn & ::= & \cdots \mysynsep \mytmsyn \myeq \mytmsyn \mysynsep
1539 \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn}
1544 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1546 \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
1547 \AxiomC{$\myjud{\mytmt}{\mytya}$}
1548 \BinaryInfC{$\myjud{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}$}
1551 \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
1552 \AxiomC{$\myjud{\mytmt}{\mytya}$}
1553 \BinaryInfC{$\myjud{\mycohh{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\myprdec{\myjm{\mytmt}{\mytya}{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}}}$}
1559 \mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
1564 \myjud{\myse{A}}{\mytyp} \hspace{1cm} \myjud{\myse{B}}{\mytyp}
1567 \UnaryInfC{$\myjud{\mytya \myeq \mytyb}{\myprop}$}
1572 \myjud{\myse{A}}{\mytyp} \hspace{1cm} \myjud{\mytmm}{\myse{A}} \\
1573 \myjud{\myse{B}}{\mytyp} \hspace{1cm} \myjud{\mytmn}{\myse{B}}
1576 \UnaryInfC{$\myjud{\myjm{\mytmm}{\myse{A}}{\mytmn}{\myse{B}}}{\myprop}$}
1583 While isolating a propositional universe as presented can be a useful
1584 exercises on its own, what we are really after is a useful notion of
1585 equality. In OTT we want to maintain the notion that things judged to
1586 be equal are still always repleaceable for one another with no
1587 additional changes. Note that this is not the same as saying that they
1588 are definitionally equal, since as we saw extensionally equal functions,
1589 while satisfying the above requirement, are not definitionally equal.
1591 Towards this goal we introduce two equality constructs in
1592 $\myprop$---the fact that they are in $\myprop$ indicates that they
1593 indeed have no computational content. The first construct, $\myarg
1594 \myeq \myarg$, relates types, the second,
1595 $\myjm{\myarg}{\myarg}{\myarg}{\myarg}$, relates values. The
1596 value-level equality is different from our old propositional equality:
1597 instead of ranging over only one type, we might form equalities between
1598 values of different types---the usefulness of this construct will be
1599 clear soon. In the literature this equality is known as `heterogeneous'
1600 or `John Major', since
1603 John Major's `classless society' widened people's aspirations to
1604 equality, but also the gap between rich and poor. After all, aspiring
1605 to be equal to others than oneself is the politics of envy. In much
1606 the same way, forms equations between members of any type, but they
1607 cannot be treated as equals (ie substituted) unless they are of the
1608 same type. Just as before, each thing is only equal to
1609 itself. \citep{McBride1999}.
1612 Correspondingly, at the term level, $\myfun{coe}$ (`coerce') lets us
1613 transport values between equal types; and $\myfun{coh}$ (`coherence')
1614 guarantees that $\myfun{coe}$ respects the value-level equality, or in
1615 other words that it really has no computational component: if we
1616 transport $\mytmm : \mytya$ to $\mytmn : \mytyb$, $\mytmm$ and $\mytmn$
1617 will still be the same.
1619 Before introducing the core ideas that make OTT work, let us distinguish
1620 between \emph{canonical} and \emph{neutral} types. Canonical types are
1621 those arising from the ground types ($\myempty$, $\myunit$, $\mybool$)
1622 and the three type formers ($\myarr$, $\myprod$, $\mytyc{W}$). Neutral
1623 types are those formed by
1624 $\myfun{If}\myarg\myfun{Then}\myarg\myfun{Else}\myarg$.
1625 Correspondingly, canonical terms are those inhabiting canonical types
1626 ($\mytt$, $\mytrue$, $\myfalse$, $\myabss{\myb{x}}{\mytya}{\mytmt}$,
1627 ...), and neutral terms those formed by eliminators\footnote{Using the
1628 terminology from section \ref{sec:types}, we'd say that canonical
1629 terms are in \emph{weak head normal form}.}. In the current system
1630 (and hopefully in well-behaved systems), all closed terms reduce to a
1631 canonical term, and all canonical types are inhabited by canonical
1634 \subsubsection{Type equality, and coercions}
1636 The plan is to decompose type-level equalities between canonical types
1637 into decodable propositions containing equalities regarding the
1638 subterms, and to use coerce recursively on the subterms using the
1639 generated equalities. This interplay between type equalities and
1640 \myfun{coe} ensures that invocations of $\myfun{coe}$ will vanish when
1641 we have evidence of the structural equality of the types we are
1642 transporting terms across. If the type is neutral, the equality won't
1643 reduce and thus $\myfun{coe}$ won't reduce either. If we come an
1644 equality between different canonical types, then we reduce the equality
1645 to bottom, making sure that no such proof can exist, and providing an
1646 `escape hatch' in $\myfun{coe}$.
1650 \mydesc{equality reduction:}{\myprsyn \myred \myprsyn}{
1652 \begin{array}{c@{\ }c@{\ }c@{\ }l}
1653 \myempty & \myeq & \myempty & \myred \mytop \\
1654 \myunit & \myeq & \myunit & \myred \mytop \\
1655 \mybool & \myeq & \mybool & \myred \mytop \\
1656 \myexi{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myexi{\myb{x_2}}{\mytya_2}{\mytya_2} & \myred \\
1658 \myind{2} \mytya_1 \myeq \mytyb_1 \myand
1659 \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 \myeq \mytyb_2}
1661 \myfora{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myfora{\myb{x_2}}{\mytya_2}{\mytyb_2} & \myred \cdots \\
1662 \myw{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myw{\myb{x_2}}{\mytya_2}{\mytyb_2} & \myred \cdots \\
1663 \mytya & \myeq & \mytyb & \myred \mybot\ \text{if $\mytya$ and $\mytyb$ are canonical.}
1668 \mydesc{reduction}{\mytmsyn \myred \mytmsyn}{
1670 \begin{array}[t]{@{}l@{\ }l@{\ }l@{\ }l@{\ }l@{\ }c@{\ }l@{\ }}
1671 \mycoe & \myempty & \myempty & \myse{Q} & \myse{t} & \myred & \myse{t} \\
1672 \mycoe & \myunit & \myunit & \myse{Q} & \mytt & \myred & \mytt \\
1673 \mycoe & \mybool & \mybool & \myse{Q} & \mytrue & \myred & \mytrue \\
1674 \mycoe & \mybool & \mybool & \myse{Q} & \myfalse & \myred & \myfalse \\
1675 \mycoe & (\myexi{\myb{x_1}}{\mytya_1}{\mytyb_1}) &
1676 (\myexi{\myb{x_2}}{\mytya_2}{\mytyb_2}) & \myse{Q} &
1677 \mytmt_1 & \myred & \\
1679 \myind{2}\begin{array}[t]{l@{\ }l@{\ }c@{\ }l}
1680 \mysyn{let} & \myb{\mytmm_1} & \mapsto & \myapp{\myfst}{\mytmt_1} : \mytya_1 \\
1681 & \myb{\mytmn_1} & \mapsto & \myapp{\mysnd}{\mytmt_1} : \mysub{\mytyb_1}{\myb{x_1}}{\myb{\mytmm_1}} \\
1682 & \myb{Q_A} & \mapsto & \myapp{\myfst}{\myse{Q}} : \mytya_1 \myeq \mytya_2 \\
1683 & \myb{\mytmm_2} & \mapsto & \mycoee{\mytya_1}{\mytya_2}{\myb{Q_A}}{\myb{\mytmm_1}} : \mytya_2 \\
1684 & \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}}} \\
1685 & \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}} \\
1686 \mysyn{in} & \multicolumn{3}{@{}l}{\mypair{\myb{\mytmm_2}}{\myb{\mytmn_2}}}
1689 \mycoe & (\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}) &
1690 (\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}) & \myse{Q} &
1694 \mycoe & (\myw{\myb{x_1}}{\mytya_1}{\mytyb_1}) &
1695 (\myw{\myb{x_2}}{\mytya_2}{\mytyb_2}) & \myse{Q} &
1699 \mycoe & \mytya & \mytyb & \myse{Q} & \mytmt & \myred & \\
1701 \myind{2}\myapp{\myabsurd{\mytyb}}{\myse{Q}}\ \text{if $\mytya$ and $\mytyb$ are canonical.}
1706 \caption{Reducing type equalities, and using them when
1707 $\myfun{coe}$rcing.}
1711 Figure \ref{fig:eqred} illustrates this idea in practice. For ground
1712 types, the proof is the trivial element, and \myfun{coe} is the
1713 identity. For the three type binders, things are similar but subtly
1714 different---the choices we make in the type equality are dictated by
1715 the desire of writing the $\myfun{coe}$ in a natural way.
1717 $\myprod$ is the easiest case: we decompose the proof into proofs that
1718 the first element's types are equal ($\mytya_1 \myeq \mytya_2$), and a
1719 proof that given equal values in the first element, the types of the
1720 second elements are equal too
1721 ($\myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{\myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2}}
1722 \myimpl \mytyb_1 \myeq \mytyb_2}$)\footnote{We are using $\myimpl$ to
1723 indicate a $\forall$ where we discard the first value. Also note that
1724 the $\myb{x_1}$ in the $\mytyb_1$ inside the $\forall$ is re-bound to
1725 the quantification, and similarly for $\myb{x_2}$ and $\mytyb_2$.}.
1726 This also explains the need for heterogeneous equality, since in the
1727 second proof it would be awkward to express the fact that $\myb{A_1}$ is
1728 the same as $\myb{A_2}$. In the respective $\myfun{coe}$ case, since
1729 the types are canonical, we know at this point that the proof of
1730 equality is a pair of the shape described above. Thus, we can
1731 immediately coerce the first element of the pair using the first element
1732 of the proof, and then instantiate the second element with the two first
1733 elements and a proof by coherence of their equality, since we know that
1734 the types are equal. The cases for the other binders are omitted for
1735 brevity, but they follow the same principle.
1737 \subsubsection{$\myfun{coe}$, laziness, and $\myfun{coh}$erence}
1739 It is important to notice that in the reduction rules for $\myfun{coe}$
1740 are never obstructed by the proofs: with the exception of comparisons
1741 between different canonical types we never pattern match on the pairs,
1742 but always look at the projections. This means that, as long as we are
1743 consistent, and thus as long as we don't have $\mybot$-inducing proofs,
1744 we can add propositional axioms for equality and $\myfun{coe}$ will
1745 still compute. Thus, we can take $\myfun{coh}$ as axiomatic, and we can
1746 add back familiar useful equality rules:
1748 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1749 \AxiomC{$\myjud{\mytmt}{\mytya}$}
1750 \UnaryInfC{$\myjud{\myapp{\myrefl}{\mytmt}}{\myprdec{\myjm{\myb{x}}{\myb{\mytya}}{\myb{x}}{\myb{\mytya}}}}$}
1755 \AxiomC{$\myjud{\mytya}{\mytyp}$}
1756 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytyb}{\mytyp}$}
1757 \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}}}}}$}
1761 $\myrefl$ is the equivalent of the reflexivity rule in propositional
1762 equality, and $\mytyc{R}$ asserts that if we have a we have a $\mytyp$
1763 abstracting over a value we can substitute equal for equal---this lets
1764 us recover $\myfun{subst}$. Note that while we need to provide ad-hoc
1765 rules in the restricted, non-hierarchical theory that we have, if our
1766 theory supports abstraction over $\mytyp$s we can easily add these
1767 axioms as abstracted variables.
1769 \subsubsection{Value-level equality}
1771 \mydesc{equality reduction:}{\myprsyn \myred \myprsyn}{
1773 \begin{array}{r@{ }c@{\ }c@{\ }c@{}l@{\ }c@{\ }r@{}c@{\ }c@{\ }c@{}l@{\ }l}
1774 (&\mytmt_1 & : & \myempty&) & \myeq & (&\mytmt_2 & : & \myempty &) & \myred \mytop \\
1775 (&\mytmt_1 & : & \myempty&) & \myeq & (&\mytmt_2 & : & \myempty&) & \myred \mytop \\
1776 (&\mytrue & : & \mybool&) & \myeq & (&\mytrue & : & \mybool&) & \myred \mytop \\
1777 (&\myfalse & : & \mybool&) & \myeq & (&\myfalse & : & \mybool&) & \myred \mytop \\
1778 (&\mytmt_1 & : & \mybool&) & \myeq & (&\mytmt_1 & : & \mybool&) & \myred \mybot \\
1779 (&\mytmt_1 & : & \myexi{\mytya_1}{\myb{x_1}}{\mytyb_1}&) & \myeq & (&\mytmt_2 & : & \myexi{\mytya_2}{\myb{x_2}}{\mytyb_2}&) & \myred \\
1780 & \multicolumn{11}{@{}l}{
1781 \myind{2} \myjm{\myapp{\myfst}{\mytmt_1}}{\mytya_1}{\myapp{\myfst}{\mytmt_2}}{\mytya_2} \myand
1782 \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}}}
1784 (&\myse{f}_1 & : & \myfora{\mytya_1}{\myb{x_1}}{\mytyb_1}&) & \myeq & (&\myse{f}_2 & : & \myfora{\mytya_2}{\myb{x_2}}{\mytyb_2}&) & \myred \\
1785 & \multicolumn{11}{@{}l}{
1786 \myind{2} \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{
1787 \myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2} \myimpl
1788 \myjm{\myapp{\myse{f}_1}{\myb{x_1}}}{\mytyb_1}{\myapp{\myse{f}_2}{\myb{x_2}}}{\mytyb_2}
1791 (&\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 \\
1792 (&\mytmt_1 & : & \mytya_1&) & \myeq & (&\mytmt_2 & : & \mytya_2 &) & \myred \\
1793 & \multicolumn{11}{@{}l}{
1794 \myind{2} \mybot\ \text{if $\mytya_1$ and $\mytya_2$ are canonical.}
1800 As with type-level equality, we want value-level equality to reduce
1801 based on the structure of the compared terms.
1803 \subsection{Proof irrelevance}
1805 % \section{Augmenting ITT}
1806 % \label{sec:practical}
1808 % \subsection{A more liberal hierarchy}
1810 % \subsection{Type inference}
1812 % \subsubsection{Bidirectional type checking}
1814 % \subsubsection{Pattern unification}
1816 % \subsection{Pattern matching and explicit fixpoints}
1818 % \subsection{Induction-recursion}
1820 % \subsection{Coinduction}
1822 % \subsection{Dealing with partiality}
1824 % \subsection{Type holes}
1826 \section{\mykant : the theory}
1827 \label{sec:kant-theory}
1829 \mykant\ is an interactive theorem prover developed as part of this thesis.
1830 The plan is to present a core language which would be capable of serving as
1831 the basis for a more featureful system, while still presenting interesting
1832 features and more importantly observational equality.
1834 The author learnt the hard way the implementations challenges for such a
1835 project, and while there is a solid and working base to work on, observational
1836 equality is not currently implemented. However, a detailed plan on how to add
1837 it this functionality is provided, and should not prove to be too much work.
1839 The features currently implemented in \mykant\ are:
1842 \item[Full dependent types] As we would expect, we have dependent a system
1843 which is as expressive as the `best' corner in the lambda cube described in
1844 section \ref{sec:itt}.
1846 \item[Implicit, cumulative universe hierarchy] The user does not need to
1847 specify universe level explicitly, and universes are \emph{cumulative}.
1849 \item[User defined data types and records] Instead of forcing the user to
1850 choose from a restricted toolbox, we let her define inductive data types,
1851 with associated primitive recursion operators; or records, with associated
1852 projections for each field.
1854 \item[Bidirectional type checking] While no `fancy' inference via unification
1855 is present, we take advantage of an type synthesis system in the style of
1856 \cite{Pierce2000}, extending the concept for user defined data types.
1858 \item[Type holes] When building up programs interactively, it is useful to
1859 leave parts unfinished while exploring the current context. This is what
1863 The planned features are:
1866 \item[Observational equality] As described in section \ref{sec:ott} but
1867 extended to work with the type hierarchy and to admit equality between
1868 arbitrary data types.
1870 \item[Coinductive data] ...
1873 We will analyse the features one by one, along with motivations and tradeoffs
1874 for the design decisions made.
1876 \subsection{Bidirectional type checking}
1878 We start by describing bidirectional type checking since it calls for fairly
1879 different typing rules that what we have seen up to now. The idea is to have
1880 two kind of terms: terms for which a type can always be inferred, and terms
1881 that need to be checked against a type. A nice observation is that this
1882 duality runs through the semantics of the terms: data destructors (function
1883 application, record projections, primitive re cursors) \emph{infer} types,
1884 while data constructors (abstractions, record/data types data constructors)
1885 need to be checked. In the literature these terms are respectively known as
1887 To introduce the concept and notation, we will revisit the STLC in a
1888 bidirectional style. The presentation follows \cite{Loh2010}.
1890 % TODO do this --- is it even necessary
1894 \subsection{Base terms and types}
1896 Let us begin by describing the primitives available without the user
1897 defining any data types, and without equality. The way we handle
1898 variables and substitution is left unspecified, and explained in section
1899 \ref{sec:term-repr}, along with other implementation issues. We are
1900 also going to give an account of the implicit type hierarchy separately
1901 in section \ref{sec:term-hierarchy}, so as not to clutter derivation
1902 rules too much, and just treat types as impredicative for the time
1907 \begin{array}{r@{\ }c@{\ }l}
1908 \mytmsyn & ::= & \mynamesyn \mysynsep \mytyp \\
1909 & | & \myfora{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
1910 \myabs{\myb{x}}{\mytmsyn} \mysynsep
1911 (\myapp{\mytmsyn}{\mytmsyn}) \mysynsep
1912 (\myann{\mytmsyn}{\mytmsyn}) \\
1913 \mynamesyn & ::= & \myb{x} \mysynsep \myfun{f}
1918 The syntax for our calculus includes just two basic constructs:
1919 abstractions and $\mytyp$s. Everything else will be provided by
1920 user-definable constructs. Since we let the user define values, we will
1921 need a context capable of carrying the body of variables along with
1922 their type. Bound names and defined names are treated separately in the
1923 syntax, and while both can be associated to a type in the context, only
1924 defined names can be associated with a body:
1926 \mydesc{context validity:}{\myvalid{\myctx}}{
1927 \begin{tabular}{ccc}
1928 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
1929 \UnaryInfC{$\myvalid{\myemptyctx}$}
1932 \AxiomC{$\myjud{\mytya}{\mytyp}$}
1933 \AxiomC{$\mynamesyn \not\in \myctx$}
1934 \BinaryInfC{$\myvalid{\myctx ; \mynamesyn : \mytya}$}
1937 \AxiomC{$\myjud{\mytmt}{\mytya}$}
1938 \AxiomC{$\myfun{f} \not\in \myctx$}
1939 \BinaryInfC{$\myvalid{\myctx ; \myfun{f} \mapsto \mytmt : \mytya}$}
1944 Now we can present the reduction rules, which are unsurprising. We have
1945 the usual function application ($\beta$-reduction), but also a rule to
1946 replace names with their bodies ($\delta$-reduction), and one to discard
1947 type annotations. For this reason reduction is done in-context, as
1948 opposed to what we have seen in the past:
1950 \mydesc{reduction:}{\myctx \vdash \mytmsyn \myred \mytmsyn}{
1951 \begin{tabular}{ccc}
1952 \AxiomC{\phantom{$\myb{x} \mapsto \mytmt : \mytya \in \myctx$}}
1953 \UnaryInfC{$\myctx \vdash \myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn}
1954 \myred \mysub{\mytmm}{\myb{x}}{\mytmn}$}
1957 \AxiomC{$\myfun{f} \mapsto \mytmt : \mytya \in \myctx$}
1958 \UnaryInfC{$\myctx \vdash \myfun{f} \myred \mytmt$}
1961 \AxiomC{\phantom{$\myb{x} \mapsto \mytmt : \mytya \in \myctx$}}
1962 \UnaryInfC{$\myctx \vdash \myann{\mytmm}{\mytya} \myred \mytmm$}
1967 We can now give types to our terms. The type of names, both defined and
1968 abstract, is inferred. The type of applications is inferred too,
1969 propagating types down the applied term. Abstractions are checked.
1970 Finally, we have a rule to check the type of an inferrable term. We
1971 defer the question of term equality (which is needed for type checking)
1972 to section \label{sec:kant-irr}.
1974 \mydesc{typing:}{\myctx \vdash \mytmsyn \Leftrightarrow \mytmsyn}{
1975 \begin{tabular}{ccc}
1976 \AxiomC{$\myse{name} : A \in \myctx$}
1977 \UnaryInfC{$\myinf{\myse{name}}{A}$}
1980 \AxiomC{$\myfun{f} \mapsto \mytmt : A \in \myctx$}
1981 \UnaryInfC{$\myinf{\myfun{f}}{A}$}
1984 \AxiomC{$\myinf{\mytmt}{\mytya}$}
1985 \UnaryInfC{$\mychk{\myann{\mytmt}{\mytya}}{\mytya}$}
1990 \begin{tabular}{ccc}
1991 \AxiomC{$\myinf{\mytmm}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
1992 \AxiomC{$\mychk{\mytmn}{\mytya}$}
1993 \BinaryInfC{$\myinf{\myapp{\mytmm}{\mytmn}}{\mysub{\mytyb}{\myb{x}}{\mytmn}}$}
1998 \AxiomC{$\mychkk{\myctx; \myb{x}: \mytya}{\mytmt}{\mytyb}$}
1999 \UnaryInfC{$\mychk{\myabs{\myb{x}}{\mytmt}}{\myfora{\myb{x}}{\mytyb}{\mytyb}}$}
2004 \subsection{Elaboration}
2006 As we mentioned, $\mykant$\ allows the user to define not only values
2007 but also custom data types and records. \emph{Elaboration} consists of
2008 turning these declarations into workable syntax, types, and reduction
2009 rules. The treatment of custom types in $\mykant$\ is heavily inspired
2010 by McBride and McKinna early work on Epigram \citep{McBride2004},
2011 although with some differences.
2013 \subsubsection{Term vectors, telescopes, and assorted notation}
2015 We use a vector notation to refer to a series of term applied to
2016 another, for example $\mytyc{D} \myappsp \vec{A}$ is a shorthand for
2017 $\mytyc{D} \myappsp \mytya_1 \cdots \mytya_n$, for some $n$. $n$ is
2018 consistently used to refer to the length of such vectors, and $i$ to
2019 refer to an index in such vectors. We also often need to `build up'
2020 terms vectors, in which case we use $\myemptyctx$ for an empty vector
2021 and add elements to an existing vector with $\myarg ; \myarg$, similarly
2022 to what we do for context.
2024 To present the elaboration and operations on user defined data types, we
2025 frequently make use what de Bruijn called \emph{telescopes}
2026 \citep{Bruijn91}, a construct that will prove useful when dealing with
2027 the types of type and data constructors. A telescope is a series of
2028 nested typed bindings, such as $(\myb{x} {:} \mynat); (\myb{p} :
2029 \myapp{\myfun{even}}{\myb{x}})$. Consistently with the notation for
2030 contexts and term vectors, we use $\myemptyctx$ to denote an empty
2031 telescope and $\myarg ; \myarg$ to add a new binding to an existing
2034 We refer to telescopes with $\mytele$, $\mytele'$, $\mytele_i$, etc. If
2035 $\mytele$ refers to a telescope, $\mytelee$ refers to the term vector
2036 made up of all the variables bound by $\mytele$. $\mytele \myarr
2037 \mytya$ refers to the type made by turning the telescope into a series
2038 of $\myarr$. Returning to the examples above, we have that
2040 (\myb{x} {:} \mynat); (\myb{p} : \myapp{\myfun{even}}{\myb{x}}) \myarr \mynat =
2041 (\myb{x} {:} \mynat) \myarr (\myb{p} : \myapp{\myfun{even}}{\myb{x}}) \myarr \mynat
2044 We make use of various operations to manipulate telescopes:
2046 \item $\myhead(\mytele)$ refers to the first type appearing in
2047 $\mytele$: $\myhead((\myb{x} {:} \mynat); (\myb{p} :
2048 \myapp{\myfun{even}}{\myb{x}})) = \mynat$. Similarly,
2049 $\myix_i(\mytele)$ refers to the $i^{th}$ type in a telescope
2051 \item $\mytake_i(\mytele)$ refers to the telescope created by taking the
2052 first $i$ elements of $\mytele$: $\mytake_1((\myb{x} {:} \mynat); (\myb{p} :
2053 \myapp{\myfun{even}}{\myb{x}})) = (\myb{x} {:} \mynat)$
2054 \item $\mytele \vec{A}$ refers to the telescope made by `applying' the
2055 terms in $\vec{A}$ on $\mytele$: $((\myb{x} {:} \mynat); (\myb{p} :
2056 \myapp{\myfun{even}}{\myb{x}}))42 = (\myb{p} :
2057 \myapp{\myfun{even}}{42})$.
2060 \subsubsection{Declarations syntax}
2064 \begin{array}{r@{\ }c@{\ }l}
2065 \mydeclsyn & ::= & \myval{\myb{x}}{\mytmsyn}{\mytmsyn} \\
2066 & | & \mypost{\myb{x}}{\mytmsyn} \\
2067 & | & \myadt{\mytyc{D}}{\mytelesyn}{}{\mydc{c} : \mytelesyn\ |\ \cdots } \\
2068 & | & \myreco{\mytyc{D}}{\mytelesyn}{}{\myfun{f} : \mytmsyn,\ \cdots } \\
2070 \mytelesyn & ::= & \myemptytele \mysynsep \mytelesyn \mycc (\myb{x} {:} \mytmsyn) \\
2071 \mynamesyn & ::= & \cdots \mysynsep \mytyc{D} \mysynsep \mytyc{D}.\mydc{c} \mysynsep \mytyc{D}.\myfun{f}
2076 In \mykant\ we have four kind of declarations:
2079 \item[Defined value] A variable, together with a type and a body.
2080 \item[Abstract variable] An abstract variable, with a type but no body.
2081 \item[Inductive data] A datatype, with a type constructor and various data
2082 constructors---somewhat similar to what we find in Haskell. A primitive
2083 recursor (or `destructor') will be generated automatically.
2084 \item[Record] A record, which consists of one data constructor and various
2085 fields, with no recursive occurrences.
2088 Elaborating defined variables consists of type checking body against the
2089 given type, and updating the context to contain the new binding.
2090 Elaborating abstract variables and abstract variables consists of type
2091 checking the type, and updating the context with a new typed variable:
2093 \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
2095 \AxiomC{$\myjud{\mytmt}{\mytya}$}
2096 \AxiomC{$\myfun{f} \not\in \myctx$}
2098 $\myctx \myelabt \myval{\myfun{f}}{\mytya}{\mytmt} \ \ \myelabf\ \ \myctx; \myfun{f} \mapsto \mytmt : \mytya$
2102 \AxiomC{$\myjud{\mytya}{\mytyp}$}
2103 \AxiomC{$\myfun{f} \not\in \myctx$}
2106 \myctx \myelabt \mypost{\myfun{f}}{\mytya}
2107 \ \ \myelabf\ \ \myctx; \myfun{f} : \mytya
2114 \subsubsection{User defined types}
2117 \begin{subfigure}[b]{\textwidth}
2123 \mynamesyn ::= \cdots \mysynsep \mytyc{D} \mysynsep \mytyc{D}.\mydc{c} \mysynsep \mytyc{D}.\myfun{f}
2128 \mydesc{syntax elaboration:}{\mydeclsyn \myelabf \mytmsyn ::= \cdots}{
2131 \begin{array}{r@{\ }l}
2132 & \myadt{\mytyc{D}}{\mytele}{}{\cdots\ |\ \mydc{c}_n : \mytele_n } \\
2135 \begin{array}{r@{\ }c@{\ }l}
2136 \mytmsyn & ::= & \cdots \mysynsep \myapp{\mytyc{D}}{\mytmsyn^{\mytele}} \mysynsep \cdots \mysynsep
2137 \mytyc{D}.\mydc{c}_n \myappsp \mytmsyn^{\mytele_n} \mysynsep \mytyc{D}.\myfun{elim} \myappsp \mytmsyn \\
2143 \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
2148 \myinf{\mytele \myarr \mytyp}{\mytyp}\hspace{0.8cm}
2149 \mytyc{D} \not\in \myctx \\
2150 \myinff{\myctx;\ \mytyc{D} : \mytele \myarr \mytyp}{\mytele \mycc \mytele_i \myarr \myapp{\mytyc{D}}{\mytelee}}{\mytyp}\ \ \ (1 \leq i \leq n) \\
2151 \text{For each $(\myb{x} {:} \mytya)$ in each $\mytele_i$, if $\mytyc{D} \in \mytya$, then $\mytya = \myapp{\mytyc{D}}{\vec{\mytmt}}$.}
2155 \begin{array}{r@{\ }c@{\ }l}
2156 \myctx & \myelabt & \myadt{\mytyc{D}}{\mytele}{}{ \cdots \ |\ \mydc{c}_n : \mytele_n } \\
2157 & & \vspace{-0.2cm} \\
2158 & \myelabf & \myctx;\ \mytyc{D} : \mytele \myarr \mytyp;\ \cdots;\ \mytyc{D}.\mydc{c}_n : \mytele \mycc \mytele_n \myarr \myapp{\mytyc{D}}{\mytelee}; \\
2160 \begin{array}{@{}r@{\ }l l}
2161 \mytyc{D}.\myfun{elim} : & \mytele \myarr (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr & \textbf{target} \\
2162 & (\myb{P} {:} \myapp{\mytyc{D}}{\mytelee} \myarr \mytyp) \myarr & \textbf{motive} \\
2166 (\mytele_n \mycc \myhyps(\myb{P}, \mytele_n) \myarr \myapp{\myb{P}}{(\myapp{\mytyc{D}.\mydc{c}_n}{\mytelee_n})}) \myarr
2167 \end{array} \right \}
2168 & \textbf{methods} \\
2169 & \myapp{\myb{P}}{\myb{x}} &
2173 \DisplayProof \\ \vspace{0.2cm}\ \\
2175 \begin{array}{@{}l l@{\ } l@{} r c l}
2176 \textbf{where} & \myhyps(\myb{P}, & \myemptytele &) & \mymetagoes & \myemptytele \\
2177 & \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) \\
2178 & \myhyps(\myb{P}, & (\myb{x} {:} \mytya) \mycc \mytele & ) & \mymetagoes & \myhyps(\myb{P}, \mytele)
2184 \mydesc{reduction elaboration:}{\mydeclsyn \myelabf \myctx \vdash \mytmsyn \myred \mytmsyn}{
2186 $\myadt{\mytyc{D}}{\mytele}{}{ \cdots \ |\ \mydc{c}_n : \mytele_n } \ \ \myelabf$
2187 \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
2188 \AxiomC{$\mytyc{D}.\mydc{c}_i : \mytele;\mytele_i \myarr \myapp{\mytyc{D}}{\mytelee} \in \myctx$}
2190 \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)}
2192 \DisplayProof \\ \vspace{0.2cm}\ \\
2194 \begin{array}{@{}l l@{\ } l@{} r c l}
2195 \textbf{where} & \myrecs(\myse{P}, \vec{m}, & \myemptytele &) & \mymetagoes & \myemptytele \\
2196 & \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) \\
2197 & \myrecs(\myse{P}, \vec{m}, & (\myb{x} {:} \mytya); \mytele &) & \mymetagoes & \myrecs(\myse{P}, \vec{m}, \mytele)
2203 \begin{subfigure}[b]{\textwidth}
2204 \mydesc{syntax elaboration:}{\myelab{\mydeclsyn}{\mytmsyn ::= \cdots}}{
2207 \begin{array}{r@{\ }c@{\ }l}
2208 \myctx & \myelabt & \myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \\
2211 \begin{array}{r@{\ }c@{\ }l}
2212 \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 \\
2219 \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
2223 \myinf{\mytele \myarr \mytyp}{\mytyp}\hspace{0.8cm}
2224 \mytyc{D} \not\in \myctx \\
2225 \myinff{\myctx; \mytele; (\myb{f}_j : \myse{F}_j)_{j=1}^{i - 1}}{F_i}{\mytyp} \myind{3} (1 \le i \le n)
2229 \begin{array}{r@{\ }c@{\ }l}
2230 \myctx & \myelabt & \myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \\
2231 & & \vspace{-0.2cm} \\
2232 & \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}; \\
2233 & & \mytyc{D}.\mydc{constr} : \mytele \myarr \myse{F}_1 \myarr \cdots \myarr \myse{F}_n \myarr \myapp{\mytyc{D}}{\mytelee};
2239 \mydesc{reduction elaboration:}{\mydeclsyn \myelabf \myctx \vdash \mytmsyn \myred \mytmsyn}{
2241 $\myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \ \ \myelabf$
2242 \AxiomC{$\mytyc{D} \in \myctx$}
2243 \UnaryInfC{$\myctx \vdash \myapp{\mytyc{D}.\myfun{f}_i}{(\mytyc{D}.\mydc{constr} \myappsp \vec{t})} \myred t_i$}
2248 \caption{Elaboration for data types and records.}
2252 Elaborating user defined types is the real effort. First, let's explain
2253 what we can defined, with some examples.
2256 \item[Natural numbers] To define natural numbers, we create a data type
2257 with two constructors: one with zero arguments ($\mydc{zero}$) and one
2258 with one recursive argument ($\mydc{suc}$):
2261 \myadt{\mynat}{ }{ }{
2262 \mydc{zero} \mydcsep \mydc{suc} \myappsp \mynat
2266 This is very similar to what we would write in Haskell:
2268 \begin{verbatim}data Nat = Zero | Suc Nat
2270 Once the data type is defined, $\mykant$\ will generate syntactic
2271 constructs for the type and data constructors, so that we will have
2274 \begin{tabular}{ccc}
2275 \AxiomC{\phantom{$\mychk{\mytmt}{\mynat}$}}
2276 \UnaryInfC{$\myinf{\mynat}{\mytyp}$}
2279 \AxiomC{\phantom{$\mychk{\mytmt}{\mynat}$}}
2280 \UnaryInfC{$\myinf{\mytyc{\mynat}.\mydc{zero}}{\mynat}$}
2283 \AxiomC{$\mychk{\mytmt}{\mynat}$}
2284 \UnaryInfC{$\myinf{\mytyc{\mynat}.\mydc{suc} \myappsp \mytmt}{\mynat}$}
2288 While in Haskell (or indeed in Agda or Coq) data constructors are
2289 treated the same way as functions, in $\mykant$\ they are syntax, so
2290 for example using $\mytyc{\mynat}.\mydc{suc}$ on its own will be a
2291 syntax error. This is necessary so that we can easily infer the type
2292 of polymorphic data constructors, as we will see later.
2294 Moreover, each data constructor is prefixed by the type constructor
2295 name, since we need to retrieve the type constructor of a data
2296 constructor when type checking. This measure aids in the presentation
2297 of various features but it is not needed in the implementation, where
2298 we can have a dictionary to lookup the type constructor corresponding
2299 to each data constructor. When using data constructors in examples I
2300 will omit the type constructor prefix for brevity.
2302 Along with user defined constructors, $\mykant$\ automatically
2303 generates an \emph{eliminator}, or \emph{destructor}, to compute with
2304 natural numbers: If we have $\mytmt : \mynat$, we can destruct
2305 $\mytmt$ using the generated eliminator `$\mynat.\myfun{elim}$':
2308 \AxiomC{$\mychk{\mytmt}{\mynat}$}
2310 \myinf{\mytyc{\mynat}.\myfun{elim} \myappsp \mytmt}{
2312 \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}}
2316 $\mynat.\myfun{elim}$ corresponds to the induction principle for
2317 natural numbers: if we have a predicate on numbers ($\myb{P}$), and we
2318 know that predicate holds for the base case
2319 ($\myapp{\myb{P}}{\mydc{zero}}$) and for each inductive step
2320 ($\myfora{\myb{x}}{\mynat}{\myapp{\myb{P}}{\myb{x}} \myarr
2321 \myapp{\myb{P}}{(\myapp{\mydc{suc}}{\myb{x}})}}$), then $\myb{P}$
2322 holds for any number. As with the data constructors, we require the
2323 eliminator to be applied to the `destructed' element.
2325 While the induction principle is usually seen as a mean to prove
2326 properties about numbers, in the intuitionistic setting it is also a
2327 mean to compute. In this specific case we will $\mynat.\myfun{elim}$
2328 will return the base case if the provided number is $\mydc{zero}$, and
2329 recursively apply the inductive step if the number is a
2332 \begin{array}{@{}l@{}l}
2333 \mytyc{\mynat}.\myfun{elim} \myappsp \mydc{zero} & \myappsp \myse{P} \myappsp \myse{pz} \myappsp \myse{ps} \myred \myse{pz} \\
2334 \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})
2337 % TODO maybe more examples, e.g. Haskell eliminator and fibonacci
2339 \item[Binary trees] Now for a polymorphic data type: binary trees, since
2340 lists are too similar to natural numbers to be interesting.
2343 \myadt{\mytree}{\myappsp (\myb{A} {:} \mytyp)}{ }{
2344 \mydc{leaf} \mydcsep \mydc{node} \myappsp (\myapp{\mytree}{\myb{A}}) \myappsp \myb{A} \myappsp (\myapp{\mytree}{\myb{A}})
2348 Now the purpose of constructors as syntax can be explained: what would
2349 the type of $\mydc{leaf}$ be? If we were to treat it as a `normal'
2350 term, we would have to specify the type parameter of the tree each
2351 time the constructor is applied:
2353 \begin{array}{@{}l@{\ }l}
2354 \mydc{leaf} & : \myfora{\myb{A}}{\mytyp}{\myapp{\mytree}{\myb{A}}} \\
2355 \mydc{node} & : \myfora{\myb{A}}{\mytyp}{\myapp{\mytree}{\myb{A}} \myarr \myb{A} \myarr \myapp{\mytree}{\myb{A}} \myarr \myapp{\mytree}{\myb{A}}}
2358 The problem with this approach is that creating terms is incredibly
2359 verbose and dull, since we would need to specify the type parameters
2360 each time. For example if we wished to create a $\mytree \myappsp
2361 \mynat$ with two nodes and three leaves, we would have to write
2363 \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)
2365 The redundancy of $\mynat$s is quite irritating. Instead, if we treat
2366 constructors as syntactic elements, we can `extract' the type of the
2367 parameter from the type that the term gets checked against, much like
2368 we get the type of abstraction arguments:
2372 \AxiomC{$\mychk{\mytya}{\mytyp}$}
2373 \UnaryInfC{$\mychk{\mydc{leaf}}{\myapp{\mytree}{\mytya}}$}
2376 \AxiomC{$\mychk{\mytmm}{\mytree \myappsp \mytya}$}
2377 \AxiomC{$\mychk{\mytmt}{\mytya}$}
2378 \AxiomC{$\mychk{\mytmm}{\mytree \myappsp \mytya}$}
2379 \TrinaryInfC{$\mychk{\mydc{node} \myappsp \mytmm \myappsp \mytmt \myappsp \mytmn}{\mytree \myappsp \mytya}$}
2383 Which enables us to write, much more concisely
2385 \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}
2387 We gain an annotation, but we lose the myriad of types applied to the
2388 constructors. Conversely, with the eliminator for $\mytree$, we can
2389 infer the type of the arguments given the type of the destructed:
2392 \AxiomC{$\myinf{\mytmt}{\myapp{\mytree}{\mytya}}$}
2394 \myinf{\mytree.\myfun{elim} \myappsp \mytmt}{
2396 (\myb{P} {:} \myapp{\mytree}{\mytya} \myarr \mytyp) \myarr \\
2397 \myapp{\myb{P}}{\mydc{leaf}} \myarr \\
2398 ((\myb{l} {:} \myapp{\mytree}{\mytya}) (\myb{x} {:} \mytya) (\myb{r} {:} \myapp{\mytree}{\mytya}) \myarr \myapp{\myb{P}}{\myb{l}} \myarr
2399 \myapp{\myb{P}}{\myb{r}} \myarr \myb{P} \myappsp (\mydc{node} \myappsp \myb{l} \myappsp \myb{x} \myappsp \myb{r})) \myarr \\
2400 \myapp{\myb{P}}{\mytmt}
2405 As expected, the eliminator embodies structural induction on trees.
2407 \item[Empty type] We have presented types that have at least one
2408 constructors, but nothing prevents us from defining types with
2409 \emph{no} constructors:
2411 \myadt{\mytyc{Empty}}{ }{ }{ }
2413 What shall the `induction principle' on $\mytyc{Empty}$ be? Does it
2414 even make sense to talk about induction on $\mytyc{Empty}$?
2415 $\mykant$\ does not care, and generates an eliminator with no `cases',
2416 and thus corresponding to the $\myfun{absurd}$ that we know and love:
2419 \AxiomC{$\myinf{\mytmt}{\mytyc{Empty}}$}
2420 \UnaryInfC{$\myinf{\myempty.\myfun{elim} \myappsp \mytmt}{(\myb{P} {:} \mytmt \myarr \mytyp) \myarr \myapp{\myb{P}}{\mytmt}}$}
2423 \item[Ordered lists] Up to this point, the examples shown are nothing
2424 new to the \{Haskell, SML, OCaml, functional\} programmer. However
2425 dependent types let us express much more than
2428 \item[Dependent products] Apart from $\mysyn{data}$, $\mykant$\ offers
2429 us another way to define types: $\mysyn{record}$. A record is a
2430 datatype with one constructor and `projections' to extract specific
2431 fields of the said constructor.
2433 For example, we can recover dependent products:
2436 \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}}}
2439 Here $\myfst$ and $\mysnd$ are the projections, with their respective
2440 types. Note that each field can refer to the preceding fields. A
2441 constructor will be automatically generated, under the name of
2442 $\mytyc{Prod}.\mydc{constr}$. Dually to data types, we will omit the
2443 type constructor prefix for record projections.
2445 Following the bidirectionality of the system, we have that projections
2446 (the destructors of the record) infer the type, while the constructor
2451 \AxiomC{$\mychk{\mytmm}{\mytya}$}
2452 \AxiomC{$\mychk{\mytmn}{\myapp{\mytyb}{\mytmm}}$}
2453 \BinaryInfC{$\mychk{\mytyc{Prod}.\mydc{constr} \myappsp \mytmm \myappsp \mytmn}{\mytyc{Prod} \myappsp \mytya \myappsp \mytyb}$}
2455 \UnaryInfC{\phantom{$\myinf{\myfun{snd} \myappsp \mytmt}{\mytyb \myappsp (\myfst \myappsp \mytmt)}$}}
2458 \AxiomC{$\myinf{\mytmt}{\mytyc{Prod} \myappsp \mytya \myappsp \mytyb}$}
2459 \UnaryInfC{$\myinf{\myfun{fst} \myappsp \mytmt}{\mytya}$}
2461 \UnaryInfC{$\myinf{\myfun{snd} \myappsp \mytmt}{\mytyb \myappsp (\myfst \myappsp \mytmt)}$}
2465 What we have is equivalent to ITT's dependent products.
2468 Following the intuition given by the examples, the mechanised
2469 elaboration is presented in figure \ref{fig:elab}, which is essentially
2470 a modification of figure 9 of \citep{McBride2004}\footnote{However, our
2471 datatypes do not have indices, we do bidirectional typechecking by
2472 treating constructors/destructors are syntactic constructors, and we
2475 In data types declarations we allow recursive occurrences as long as
2476 they are \emph{strictly positive}, employing a syntactic check to make
2477 sure that this is the case. See \cite{Dybjer1991} for a more formal
2478 treatment of inductive definitions in ITT.
2480 For what concerns records, recursive occurrences are disallowed. The
2481 reason for this choice is answered by the reason for the choice of
2482 having records at all: we need records to give the user types with
2483 $\eta$-laws for equality, as we saw in section % TODO add section
2484 and in the treatment of OTT in section \ref{sec:ott}. If we tried to
2485 $\eta$-expand recursive data types, we would expand forever.
2487 To implement bidirectional type checking for constructors and
2488 destructors, we store their types in full in the context, and then
2489 instantiate when due:
2491 \mydesc{typing:}{ }{
2494 \mytyc{D} : \mytele \myarr \mytyp \in \myctx \hspace{1cm}
2495 \mytyc{D}.\mydc{c} : \mytele \mycc \mytele' \myarr
2496 \myapp{\mytyc{D}}{\mytelee} \in \myctx \\
2497 \mytele'' = (\mytele;\mytele')\vec{A} \hspace{1cm}
2498 \mychkk{\myctx; \mytake_{i-1}(\mytele'')}{t_i}{\myix_i( \mytele'')}\ \
2499 (1 \le i \le \mytele'')
2502 \UnaryInfC{$\mychk{\myapp{\mytyc{D}.\mydc{c}}{\vec{t}}}{\myapp{\mytyc{D}}{\vec{A}}}$}
2507 \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
2508 \AxiomC{$\mytyc{D}.\myfun{f} : \mytele \mycc (\myb{x} {:}
2509 \myapp{\mytyc{D}}{\mytelee}) \myarr \myse{F}$}
2510 \AxiomC{$\myjud{\mytmt}{\myapp{\mytyc{D}}{\vec{A}}}$}
2511 \TrinaryInfC{$\myinf{\myapp{\mytyc{D}.\myfun{f}}{\mytmt}}{(\mytele
2512 \mycc (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr
2513 \myse{F})(\vec{A};\mytmt)}$}
2517 \subsubsection{Why user defined types?}
2519 % TODO reference levitated theories, indexed containers
2523 \subsection{Cumulative hierarchy and typical ambiguity}
2524 \label{sec:term-hierarchy}
2526 A type hierarchy as presented in section \label{sec:itt} is a
2527 considerable burden on the user, on various levels. Consider for
2528 example how we recovered disjunctions in section \label{sec:disju}: we
2529 have a function that takes two $\mytyp_0$ and forms a new $\mytyp_0$.
2530 What if we wanted to form a disjunction containing two $\mytyp_0$, or
2531 $\mytyp_{42}$? Our definition would fail us, since $\mytyp_0 :
2534 One way to solve this issue is a \emph{cumulative} hierarchy, where
2535 $\mytyp_{l_1} : \mytyp_{l_2}$ iff $l_1 < l_2$. This way we retain
2536 consistency, while allowing for `large' definitions that work on small
2537 types too. For example we might define our disjunction to be
2539 \myarg\myfun{$\vee$}\myarg : \mytyp_{100} \myarr \mytyp_{100} \myarr \mytyp_{100}
2541 And hope that $\mytyp_{100}$ will be large enough to fit all the types
2542 that we want to use with our disjunction. However, there are two
2543 problems with this. First, there is the obvious clumsyness of having to
2544 manually specify the size of types. More importantly, if we want to use
2545 $\myfun{$\vee$}$ itself as an argument to other type-formers, we need to
2546 make sure that those allow for types at least as large as
2549 A better option is to employ a mechanised version of what Russell called
2550 \emph{typical ambiguity}: we let the user live under the illusion that
2551 $\mytyp : \mytyp$, but check that the statements about types are
2552 consistent behind the hood. $\mykant$\ implements this following the
2553 lines of \cite{Huet1988}. See also \citep{Harper1991} for a published
2554 reference, although describing a more complex system allowing for both
2555 explicit and explicit hierarchy at the same time.
2557 We define a partial ordering on the levels, with both weak ($\le$) and
2558 strong ($<$) constraints---the laws governing them being the same as the
2559 ones governing $<$ and $\le$ for the natural numbers. Each occurrence
2560 of $\mytyp$ is decorated with a unique reference, and we keep a set of
2561 constraints and add new constraints as we type check, generating new
2562 references when needed.
2564 For example, when type checking the type $\mytyp\, r_1$, where $r_1$
2565 denotes the unique reference assigned to that term, we will generate a
2566 new fresh reference $\mytyp\, r_2$, and add the constraint $r_1 < r_2$
2567 to the set. When type checking $\myctx \vdash
2568 \myfora{\myb{x}}{\mytya}{\mytyb}$, if $\myctx \vdash \mytya : \mytyp\,
2569 r_1$ and $\myctx; \myb{x} : \mytyb \vdash \mytyb : \mytyp\,r_2$; we will
2570 generate new reference $r$ and add $r_1 \le r$ and $r_2 \le r$ to the
2573 If at any point the constraint set becomes inconsistent, type checking
2574 fails. Moreover, when comparing two $\mytyp$ terms we equate their
2575 respective references with two $\le$ constraints---the details are
2576 explained in section \ref{sec:hier-impl}.
2578 Another more flexible but also more verbose alternative is the one
2579 chosen by Agda, where levels can be quantified so that the relationship
2580 between arguments and result in type formers can be explicitly
2583 \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}
2585 Inference algorithms to automatically derive this kind of relationship
2586 are currently subject of research. We chose less flexible but more
2587 concise way, since it is easier to implement and better understood.
2589 \subsection{Observational equality, \mykant\ style}
2591 There are two correlated differences between $\mykant$\ and the theory
2592 used to present OTT. The first is that in $\mykant$ we have a type
2593 hierarchy, which lets us, for example, abstract over types. The second
2594 is that we let the user define inductive types.
2596 Reconciling propositions for OTT and a hierarchy had already been
2597 investigated by Conor McBride\footnote{See
2598 \url{http://www.e-pig.org/epilogue/index.html?p=1098.html}.}, and we
2599 follow his footsteps. Most of the work, as an extension of elaboration,
2600 is to generate reduction rules and coercions.
2602 \subsubsection{The \mykant\ prelude, and $\myprop$ositions}
2604 Before defining $\myprop$, we define some basic types inside $\mykant$,
2605 as the target for the $\myprop$ decoder:
2611 \myadt{\mytyc{Empty}}{}{ }{ } \\
2612 \myfun{absurd} : (\myb{A} {:} \mytyp) \myarr \mytyc{Empty} \myarr \myb{A} \mapsto \\
2613 \myind{2} \myabs{\myb{A\ \myb{bot}}}{\mytyc{Empty}.\myfun{elim} \myappsp \myb{bot} \myappsp (\myabs{\_}{\myb{A}})} \\
2616 \myreco{\mytyc{Unit}}{}{\mydc{tt}}{ } \\ \ \\
2618 \myreco{\mytyc{Prod}}{\myappsp (\myb{A}\ \myb{B} {:} \mytyp)}{ }{\myfun{fst} : \myb{A}, \myfun{snd} : \myb{B} }
2622 When using $\mytyc{Prod}$, we shall use $\myprod$ to define `nested'
2623 products, and $\myproj{n}$ to project elements from them, so that
2627 \mytya \myprod \mytyb = \mytyc{Prod} \myappsp \mytya \myappsp (\mytyc{Prod} \myappsp \mytyb \myappsp \myunit) \\
2628 \mytya \myprod \mytyb \myprod \myse{C} = \mytyc{Prod} \myappsp \mytya \myappsp (\mytyc{Prod} \myappsp \mytyb \myappsp (\mytyc{Prod} \myappsp \mytyc \myappsp \myunit)) \\
2630 \myproj{1} : \mytyc{Prod} \myappsp \mytya \myappsp \mytyb \myarr \mytya \\
2631 \myproj{2} : \mytyc{Prod} \myappsp \mytya \myappsp (\mytyc{Prod} \myappsp \mytyb \myappsp \myse{C}) \myarr \mytyb \\
2636 And so on, so that $\myproj{n}$ will work with all products with at
2637 least than $n$ elements. Then we can define propositions, and decoding:
2641 \begin{array}{r@{\ }c@{\ }l}
2642 \mytmsyn & ::= & \cdots \mysynsep \myprdec{\myprsyn} \\
2643 \myprsyn & ::= & \mybot \mysynsep \mytop \mysynsep \myprsyn \myand \myprsyn \mysynsep \myprfora{\myb{x}}{\mytmsyn}{\myprsyn}
2648 \mydesc{proposition decoding:}{\myprdec{\mytmsyn} \myred \mytmsyn}{
2651 \begin{array}{l@{\ }c@{\ }l}
2652 \myprdec{\mybot} & \myred & \myempty \\
2653 \myprdec{\mytop} & \myred & \myunit
2658 \begin{array}{r@{ }c@{ }l@{\ }c@{\ }l}
2659 \myprdec{&\myse{P} \myand \myse{Q} &} & \myred & \myprdec{\myse{P}} \myprod \myprdec{\myse{Q}} \\
2660 \myprdec{&\myprfora{\myb{x}}{\mytya}{\myse{P}} &} & \myred &
2661 \myfora{\myb{x}}{\mytya}{\myprdec{\myse{P}}}
2667 \subsubsection{Why $\myprop$?}
2669 It is worth to ask if $\myprop$ is needed at all. It is perfectly
2670 possible to have the type checker identify propositional types
2671 automatically, and in fact that is what The author initially planned to
2672 identify the propositional fragment iinternally \cite{Jacobs1994}.
2674 \subsubsection{OTT constructs}
2678 \begin{array}{r@{\ }c@{\ }l}
2679 \mytmsyn & ::= & \cdots \mysynsep \mycoee{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \mysynsep
2680 \mycohh{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
2681 \myprsyn & ::= & \cdots \mysynsep \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
2686 \mydesc{equality reduction:}{\myctx \vdash \myprsyn \myred \myprsyn}{
2690 \begin{array}{r@{\ }l}
2692 \myjm{\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}}{\mytyp}{\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}}{\mytyp} \myred \\
2693 & \myind{2} \mytya_2 \myeq \mytya_1 \myand \\
2694 & \myind{2} \myprfora{\myb{x_2}}{\mytya_2}{\myprfora{\myb{x_1}}{\mytya_1}{
2695 \myjm{\myb{x_2}}{\mytya_2}{\myb{x_1}}{\mytya_1} \myimpl \mytyb_1 \myeq \mytyb_2
2703 \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
2705 \begin{array}{r@{\ }l}
2707 \myjm{\mytyc{D} \myappsp \vec{A}}{\mytyp}{\mytyc{D} \myappsp \vec{B}}{\mytyp} \myred \\
2708 & \myind{2} \myjm{\mytya_1}{\myhead(\mytele)}{\mytyb_1}{\myhead(\mytele)} \myand \cdots \myand \\
2709 & \myind{2} \myjm{\mytya_n}{\myhead(\mytele(A_1 \cdots A_{n-1}))}{\mytyb_n}{\myhead(\mytele(B_1 \cdots B_{n-1}))}
2717 \UnaryInfC{$\myctx \vdash \myjm{\mytyp}{\mytyp}{\mytyp}{\mytyp} \myred \mytop$}
2724 \mydataty(\mytyc{D}, \myctx)\hspace{0.8cm}
2725 \mytyc{D}.\mydc{c}_i : \mytele;\mytele' \myarr \mytyc{D} \myappsp \mytelee \in \myctx \\
2726 \mytele_A = (\mytele;\mytele')\vec{A}\hspace{0.8cm}
2727 \mytele_B = (\mytele;\mytele')\vec{B}
2732 \myctx \vdash \myjm{\mytyc{D}.\mydc{c}_i \myappsp \vec{\mytmm}}{\mytyc{D} \myappsp \vec{A}}{\mytyc{D}.\mydc{c}_i \myappsp \vec{\mytmn}}{\mytyc{D} \myappsp \vec{B}} \myred \\
2733 \myind{2} \myjm{\mytmm_1}{\myhead(\mytele_A)}{\mytmn_1}{\myhead(\mytele_B)} \myand \cdots \myand \\
2734 \myind{2} \myjm{\mytmm_n}{\mytya_n}{\mytmn_n}{\mytyb_n}
2741 \AxiomC{$\myisreco(\mytyc{D}, \myctx)$}
2742 \UnaryInfC{$\myctx \vdash \myjm{\mytmm}{\mytyc{D} \myappsp \vec{A}}{\mytmn}{\mytyc{D} \myappsp \vec{B}} \myred foo$}
2747 \UnaryInfC{$\mytya \myeq \mytyb \myred \mybot\ \text{if $\mytya$ and $\mytyb$ are canonical types.}$}
2751 \subsubsection{$\myprop$ and the hierarchy}
2753 Where is $\myprop$ placed in the $\mytyp$ hierarchy?
2755 \subsubsection{Quotation and irrelevance}
2760 \section{\mykant : The practice}
2761 \label{sec:kant-practice}
2763 The codebase consists of around 2500 lines of Haskell, as reported by
2764 the \texttt{cloc} utility. The high level design is inspired by Conor
2765 McBride's work on various incarnations of Epigram, and specifically by
2766 the first version as described \citep{McBride2004} and the codebase for
2767 the new version \footnote{Available intermittently as a \texttt{darcs}
2768 repository at \url{http://sneezy.cs.nott.ac.uk/darcs/Pig09}.}. In
2769 many ways \mykant\ is something in between the first and second version
2772 The interaction happens in a read-eval-print loop (REPL). The REPL is a
2773 available both as a commandline application and in a web interface,
2774 which is available at \url{kant.mazzo.li} and presents itself as in
2775 figure \ref{fig:kant-web}.
2779 \includegraphics[scale=1.0]{kant-web.png}
2781 \caption{The \mykant\ web prompt.}
2782 \label{fig:kant-web}
2785 The interaction with the user takes place in a loop living in and updating a
2786 context \mykant\ declarations. The user inputs a new declaration that goes
2787 through various stages starts with the user inputing a \mykant\ declaration or
2788 another REPL command, which then goes through various stages that can end up
2789 in a context update, or in failures of various kind. The process is described
2790 diagrammatically in figure \ref{fig:kant-process}:
2793 \item[Parse] In this phase the text input gets converted to a sugared
2794 version of the core language.
2796 \item[Desugar] The sugared declaration is converted to a core term.
2798 \item[Reference] Occurrences of $\mytyp$ get decorated by a unique reference,
2799 which is necessary to implement the type hierarchy check.
2801 \item[Elaborate] Convert the declaration to some context item, which might be
2802 a value declaration (type and body) or a data type declaration (constructors
2803 and destructors). This phase works in tandem with \textbf{Typechecking},
2804 which in turns needs to \textbf{Evaluate} terms.
2806 \item[Distill] and report the result. `Distilling' refers to the process of
2807 converting a core term back to a sugared version that the user can
2808 visualise. This can be necessary both to display errors including terms or
2809 to display result of evaluations or type checking that the user has
2812 \item[Pretty print] Format the terms in a nice way, and display the result to
2819 \tikzstyle{block} = [rectangle, draw, text width=5em, text centered, rounded
2820 corners, minimum height=2.5em, node distance=0.7cm]
2822 \tikzstyle{decision} = [diamond, draw, text width=4.5em, text badly
2823 centered, inner sep=0pt, node distance=0.7cm]
2825 \tikzstyle{line} = [draw, -latex']
2827 \tikzstyle{cloud} = [draw, ellipse, minimum height=2em, text width=5em, text
2828 centered, node distance=1.5cm]
2831 \begin{tikzpicture}[auto]
2832 \node [cloud] (user) {User};
2833 \node [block, below left=1cm and 0.1cm of user] (parse) {Parse};
2834 \node [block, below=of parse] (desugar) {Desugar};
2835 \node [block, below=of desugar] (reference) {Reference};
2836 \node [block, below=of reference] (elaborate) {Elaborate};
2837 \node [block, left=of elaborate] (tycheck) {Typecheck};
2838 \node [block, left=of tycheck] (evaluate) {Evaluate};
2839 \node [decision, right=of elaborate] (error) {Error?};
2840 \node [block, right=of parse] (distill) {Distill};
2841 \node [block, right=of desugar] (update) {Update context};
2843 \path [line] (user) -- (parse);
2844 \path [line] (parse) -- (desugar);
2845 \path [line] (desugar) -- (reference);
2846 \path [line] (reference) -- (elaborate);
2847 \path [line] (elaborate) edge[bend right] (tycheck);
2848 \path [line] (tycheck) edge[bend right] (elaborate);
2849 \path [line] (elaborate) -- (error);
2850 \path [line] (error) edge[out=0,in=0] node [near start] {yes} (distill);
2851 \path [line] (error) -- node [near start] {no} (update);
2852 \path [line] (update) -- (distill);
2853 \path [line] (distill) -- (user);
2854 \path [line] (tycheck) edge[bend right] (evaluate);
2855 \path [line] (evaluate) edge[bend right] (tycheck);
2858 \caption{High level overview of the life of a \mykant\ prompt cycle.}
2859 \label{fig:kant-process}
2862 \subsection{Parsing and Sugar}
2864 \subsection{Term representation and context}
2865 \label{sec:term-repr}
2867 \subsection{Type checking}
2869 \subsection{Type hierarchy}
2870 \label{sec:hier-impl}
2872 \subsection{Elaboration}
2874 \section{Evaluation}
2876 \section{Future work}
2878 % TODO coinduction (obscoin, gimenez), pattern unification (miller,
2879 % gundry), partiality monad (NAD)
2883 \section{Notation and syntax}
2885 Syntax, derivation rules, and reduction rules, are enclosed in frames describing
2886 the type of relation being established and the syntactic elements appearing,
2889 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
2890 Typing derivations here.
2893 In the languages presented and Agda code samples I also highlight the syntax,
2894 following a uniform color and font convention:
2897 \begin{tabular}{c | l}
2898 $\mytyc{Sans}$ & Type constructors. \\
2899 $\mydc{sans}$ & Data constructors. \\
2900 % $\myfld{sans}$ & Field accessors (e.g. \myfld{fst} and \myfld{snd} for products). \\
2901 $\mysyn{roman}$ & Keywords of the language. \\
2902 $\myfun{roman}$ & Defined values and destructors. \\
2903 $\myb{math}$ & Bound variables.
2907 Moreover, I will from time to time give examples in the Haskell programming
2908 language as defined in \citep{Haskell2010}, which I will typeset in
2909 \texttt{teletype} font. I assume that the reader is already familiar with
2910 Haskell, plenty of good introductions are available \citep{LYAH,ProgInHask}.
2912 When presenting grammars, I will use a word in $\mysynel{math}$ font
2913 (e.g. $\mytmsyn$ or $\mytysyn$) to indicate indicate nonterminals. Additionally,
2914 I will use quite flexibly a $\mysynel{math}$ font to indicate a syntactic
2915 element. More specifically, terms are usually indicated by lowercase letters
2916 (often $\mytmt$, $\mytmm$, or $\mytmn$); and types by an uppercase letter (often
2917 $\mytya$, $\mytyb$, or $\mytycc$).
2919 When presenting type derivations, I will often abbreviate and present multiple
2920 conclusions, each on a separate line:
2922 \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
2923 \UnaryInfC{$\myjud{\myapp{\myfst}{\mytmt}}{\mytya}$}
2925 \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mytyb}$}
2928 I will often present `definition' in the described calculi and in
2929 $\mykant$\ itself, like so:
2932 \myfun{name} : \mytysyn \\
2933 \myfun{name} \myappsp \myb{arg_1} \myappsp \myb{arg_2} \myappsp \cdots \mapsto \mytmsyn
2936 To define operators, I use a mixfix notation similar
2937 to Agda, where $\myarg$s denote arguments, for example
2940 \myarg \mathrel{\myfun{$\wedge$}} \myarg : \mybool \myarr \mybool \myarr \mybool \\
2941 \myb{b_1} \mathrel{\myfun{$\wedge$}} \myb{b_2} \mapsto \cdots
2947 \subsection{ITT renditions}
2948 \label{app:itt-code}
2950 \subsubsection{Agda}
2951 \label{app:agda-itt}
2953 Note that in what follows rules for `base' types are
2954 universe-polymorphic, to reflect the exposition. Derived definitions,
2955 on the other hand, mostly work with \mytyc{Set}, reflecting the fact
2956 that in the theory presented we don't have universe polymorphism.
2962 data Empty : Set where
2964 absurd : ∀ {a} {A : Set a} → Empty → A
2967 ¬_ : ∀ {a} → (A : Set a) → Set a
2970 record Unit : Set where
2973 record _×_ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
2980 data Bool : Set where
2983 if_/_then_else_ : ∀ {a} (x : Bool) (P : Bool → Set a) → P true → P false → P x
2984 if true / _ then x else _ = x
2985 if false / _ then _ else x = x
2987 if_then_else_ : ∀ {a} (x : Bool) {P : Bool → Set a} → P true → P false → P x
2988 if_then_else_ x {P} = if_/_then_else_ x P
2990 data W {s p} (S : Set s) (P : S → Set p) : Set (s ⊔ p) where
2991 _◁_ : (s : S) → (P s → W S P) → W S P
2993 rec : ∀ {a b} {S : Set a} {P : S → Set b}
2994 (C : W S P → Set) → -- some conclusion we hope holds
2995 ((s : S) → -- given a shape...
2996 (f : P s → W S P) → -- ...and a bunch of kids...
2997 ((p : P s) → C (f p)) → -- ...and C for each kid in the bunch...
2998 C (s ◁ f)) → -- ...does C hold for the node?
2999 (x : W S P) → -- If so, ...
3000 C x -- ...C always holds.
3001 rec C c (s ◁ f) = c s f (λ p → rec C c (f p))
3003 module Examples-→ where
3010 -- These pragmas are needed so we can use number literals.
3011 {-# BUILTIN NATURAL ℕ #-}
3012 {-# BUILTIN ZERO zero #-}
3013 {-# BUILTIN SUC suc #-}
3015 data List (A : Set) : Set where
3017 _∷_ : A → List A → List A
3019 length : ∀ {A} → List A → ℕ
3021 length (_ ∷ l) = suc (length l)
3026 suc x > suc y = x > y
3028 head : ∀ {A} → (l : List A) → length l > 0 → A
3029 head [] p = absurd p
3032 module Examples-× where
3038 even (suc zero) = Empty
3039 even (suc (suc n)) = even n
3044 5-not-even : ¬ (even 5)
3047 there-is-an-even-number : ℕ × even
3048 there-is-an-even-number = 6 , 6-even
3050 _∨_ : (A B : Set) → Set
3051 A ∨ B = Bool × (λ b → if b then A else B)
3053 left : ∀ {A B} → A → A ∨ B
3056 right : ∀ {A B} → B → A ∨ B
3059 [_,_] : {A B C : Set} → (A → C) → (B → C) → A ∨ B → C
3061 (if (fst x) / (λ b → if b then _ else _ → _) then f else g) (snd x)
3063 module Examples-W where
3068 Tr b = if b then Unit else Empty
3074 zero = false ◁ absurd
3077 suc n = true ◁ (λ _ → n)
3083 if b / (λ b → (Tr b → ℕ) → (Tr b → ℕ) → ℕ)
3084 then (λ _ f → (suc (f tt))) else (λ _ _ → y))
3087 List : (A : Set) → Set
3088 List A = W (A ∨ Unit) (λ s → Tr (fst s))
3091 [] = (false , tt) ◁ absurd
3093 _∷_ : ∀ {A} → A → List A → List A
3094 x ∷ l = (true , x) ◁ (λ _ → l)
3096 _++_ : ∀ {A} → List A → List A → List A
3098 (λ _ → List _ → List _)
3102 module Equality where
3105 data _≡_ {a} {A : Set a} : A → A → Set a where
3108 ≡-elim : ∀ {a b} {A : Set a}
3109 (P : (x y : A) → x ≡ y → Set b) →
3110 ∀ {x y} → P x x (refl x) → (x≡y : x ≡ y) → P x y x≡y
3111 ≡-elim P p (refl x) = p
3113 subst : ∀ {A : Set} (P : A → Set) → ∀ {x y} → (x≡y : x ≡ y) → P x → P y
3114 subst P x≡y p = ≡-elim (λ _ y _ → P y) p x≡y
3116 sym : ∀ {A : Set} (x y : A) → x ≡ y → y ≡ x
3117 sym x y p = subst (λ y′ → y′ ≡ x) p (refl x)
3119 trans : ∀ {A : Set} (x y z : A) → x ≡ y → y ≡ z → x ≡ z
3120 trans x y z p q = subst (λ z′ → x ≡ z′) q p
3122 cong : ∀ {A B : Set} (x y : A) → x ≡ y → (f : A → B) → f x ≡ f y
3123 cong x y p f = subst (λ z → f x ≡ f z) p (refl (f x))
3126 \subsubsection{\mykant}
3128 The following things are missing: $\mytyc{W}$-types, since our
3129 positivity check is overly strict, and equality, since we haven't
3130 implemented that yet.
3133 \verbatiminput{itt.ka}
3136 \subsection{\mykant\ examples}
3139 \verbatiminput{examples.ka}
3142 \subsection{\mykant's hierachy}
3144 This rendition of the Hurken's paradox does not type check with the
3145 hierachy enabled, type checks and loops without it. Adapted from an
3146 Agda version, available at
3147 \url{http://code.haskell.org/Agda/test/succeed/Hurkens.agda}.
3150 \verbatiminput{hurkens.ka}
3153 \bibliographystyle{authordate1}
3154 \bibliography{thesis}