1 \documentclass[report]{article}
4 % \usepackage{fullpage}
16 \usepackage[fleqn]{amsmath}
17 \usepackage{stmaryrd} %llbracket
20 \usepackage{bussproofs}
33 \usetikzlibrary{shapes,arrows,positioning}
34 % \usepackage{tikz-cd}
35 % \usepackage{pgfplots}
38 %% -----------------------------------------------------------------------------
40 \usepackage[english]{babel}
41 \usepackage[conor]{agda}
42 \renewcommand{\AgdaKeywordFontStyle}[1]{\ensuremath{\mathrm{\underline{#1}}}}
43 \renewcommand{\AgdaFunction}[1]{\textbf{\textcolor{AgdaFunction}{#1}}}
44 \renewcommand{\AgdaField}{\AgdaFunction}
45 % \definecolor{AgdaBound} {HTML}{000000}
46 \definecolor{AgdaHole} {HTML} {FFFF33}
48 \DeclareUnicodeCharacter{9665}{\ensuremath{\lhd}}
49 \DeclareUnicodeCharacter{964}{\ensuremath{\tau}}
50 \DeclareUnicodeCharacter{963}{\ensuremath{\sigma}}
51 \DeclareUnicodeCharacter{915}{\ensuremath{\Gamma}}
52 \DeclareUnicodeCharacter{8799}{\ensuremath{\stackrel{?}{=}}}
53 \DeclareUnicodeCharacter{9655}{\ensuremath{\rhd}}
56 %% -----------------------------------------------------------------------------
59 \newcommand{\mysyn}{\AgdaKeyword}
60 \newcommand{\mytyc}{\AgdaDatatype}
61 \newcommand{\mydc}{\AgdaInductiveConstructor}
62 \newcommand{\myfld}{\AgdaField}
63 \newcommand{\myfun}{\AgdaFunction}
64 % TODO make this use AgdaBound
65 \newcommand{\myb}[1]{\AgdaBound{#1}}
66 \newcommand{\myfield}{\AgdaField}
67 \newcommand{\myind}{\AgdaIndent}
68 \newcommand{\mykant}{\textsc{Kant}}
69 \newcommand{\mysynel}[1]{#1}
70 \newcommand{\myse}{\mysynel}
71 \newcommand{\mytmsyn}{\mysynel{term}}
72 \newcommand{\mysp}{\ }
73 % TODO \mathbin or \mathre here?
74 \newcommand{\myabs}[2]{\mydc{$\lambda$} #1 \mathrel{\mydc{$\mapsto$}} #2}
75 \newcommand{\myappsp}{\hspace{0.07cm}}
76 \newcommand{\myapp}[2]{#1 \myappsp #2}
77 \newcommand{\mysynsep}{\ \ |\ \ }
80 \newcommand{\mydesc}[3]{
86 \hfill \textbf{#1} $#2$
88 \framebox[\textwidth]{
100 % TODO is \mathbin the correct thing for arrow and times?
102 \newcommand{\mytmt}{\mysynel{t}}
103 \newcommand{\mytmm}{\mysynel{m}}
104 \newcommand{\mytmn}{\mysynel{n}}
105 \newcommand{\myred}{\leadsto}
106 \newcommand{\mysub}[3]{#1[#2 / #3]}
107 \newcommand{\mytysyn}{\mysynel{type}}
108 \newcommand{\mybasetys}{K}
109 % TODO change this name
110 \newcommand{\mybasety}[1]{B_{#1}}
111 \newcommand{\mytya}{\myse{A}}
112 \newcommand{\mytyb}{\myse{B}}
113 \newcommand{\mytycc}{\myse{C}}
114 \newcommand{\myarr}{\mathrel{\textcolor{AgdaDatatype}{\to}}}
115 \newcommand{\myprod}{\mathrel{\textcolor{AgdaDatatype}{\times}}}
116 \newcommand{\myctx}{\Gamma}
117 \newcommand{\myvalid}[1]{#1 \vdash \underline{\mathrm{valid}}}
118 \newcommand{\myjudd}[3]{#1 \vdash #2 : #3}
119 \newcommand{\myjud}[2]{\myjudd{\myctx}{#1}{#2}}
120 % TODO \mathbin or \mathrel here?
121 \newcommand{\myabss}[3]{\mydc{$\lambda$} #1 {:} #2 \mathrel{\mydc{$\mapsto$}} #3}
122 \newcommand{\mytt}{\mydc{$\langle\rangle$}}
123 \newcommand{\myunit}{\mytyc{Unit}}
124 \newcommand{\mypair}[2]{\mathopen{\mydc{$\langle$}}#1\mathpunct{\mydc{,}} #2\mathclose{\mydc{$\rangle$}}}
125 \newcommand{\myfst}{\myfld{fst}}
126 \newcommand{\mysnd}{\myfld{snd}}
127 \newcommand{\myconst}{\myse{c}}
128 \newcommand{\myemptyctx}{\cdot}
129 \newcommand{\myhole}{\AgdaHole}
130 \newcommand{\myfix}[3]{\mysyn{fix} \myappsp #1 {:} #2 \mapsto #3}
131 \newcommand{\mysum}{\mathbin{\textcolor{AgdaDatatype}{+}}}
132 \newcommand{\myleft}[1]{\mydc{left}_{#1}}
133 \newcommand{\myright}[1]{\mydc{right}_{#1}}
134 \newcommand{\myempty}{\mytyc{Empty}}
135 \newcommand{\mycase}[2]{\mathopen{\myfun{[}}#1\mathpunct{\myfun{,}} #2 \mathclose{\myfun{]}}}
136 \newcommand{\myabsurd}[1]{\myfun{absurd}_{#1}}
137 \newcommand{\myarg}{\_}
138 \newcommand{\myderivsp}{\vspace{0.3cm}}
139 \newcommand{\mytyp}{\mytyc{Type}}
140 \newcommand{\myneg}{\myfun{$\neg$}}
141 \newcommand{\myar}{\,}
142 \newcommand{\mybool}{\mytyc{Bool}}
143 \newcommand{\mytrue}{\mydc{true}}
144 \newcommand{\myfalse}{\mydc{false}}
145 \newcommand{\myitee}[5]{\myfun{if}\,#1 / {#2.#3}\,\myfun{then}\,#4\,\myfun{else}\,#5}
146 \newcommand{\mynat}{\mytyc{$\mathbb{N}$}}
147 \newcommand{\myrat}{\mytyc{$\mathbb{R}$}}
148 \newcommand{\myite}[3]{\myfun{if}\,#1\,\myfun{then}\,#2\,\myfun{else}\,#3}
149 \newcommand{\myfora}[3]{(#1 {:} #2) \myarr #3}
150 \newcommand{\myexi}[3]{(#1 {:} #2) \myprod #3}
151 \newcommand{\mypairr}[4]{\mathopen{\mydc{$\langle$}}#1\mathpunct{\mydc{,}} #4\mathclose{\mydc{$\rangle$}}_{#2{.}#3}}
152 \newcommand{\mylist}{\mytyc{List}}
153 \newcommand{\mynil}[1]{\mydc{[]}_{#1}}
154 \newcommand{\mycons}{\mathbin{\mydc{∷}}}
155 \newcommand{\myfoldr}{\myfun{foldr}}
156 \newcommand{\myw}[3]{\myapp{\myapp{\mytyc{W}}{(#1 {:} #2)}}{#3}}
157 \newcommand{\mynode}[2]{\mathbin{\mydc{$\lhd$}_{#1.#2}}}
158 \newcommand{\myrec}[4]{\myfun{rec}\,#1 / {#2.#3}\,\myfun{with}\,#4}
159 \newcommand{\mylub}{\sqcup}
160 \newcommand{\mydefeq}{\cong}
161 \newcommand{\myrefl}{\mydc{refl}}
162 \newcommand{\mypeq}[1]{\mathrel{\mytyc{=}_{#1}}}
163 \newcommand{\myjeqq}{\myfun{=-elim}}
164 \newcommand{\myjeq}[3]{\myapp{\myapp{\myapp{\myjeqq}{#1}}{#2}}{#3}}
165 \newcommand{\mysubst}{\myfun{subst}}
166 \newcommand{\myprsyn}{\myse{prop}}
167 \newcommand{\myprdec}[1]{\llbracket #1 \rrbracket}
168 \newcommand{\myand}{\wedge}
169 \newcommand{\myprfora}[3]{\forall #1 {:} #2. #3}
170 \newcommand{\mybot}{\bot}
171 \newcommand{\mytop}{\top}
172 \newcommand{\mycoe}{\myfun{coe}}
173 \newcommand{\mycoee}[4]{\myapp{\myapp{\myapp{\myapp{\mycoe}{#1}}{#2}}{#3}}{#4}}
174 \newcommand{\mycoh}{\myfun{coh}}
175 \newcommand{\mycohh}[4]{\myapp{\myapp{\myapp{\myapp{\mycoh}{#1}}{#2}}{#3}}{#4}}
176 \newcommand{\myjm}[4]{(#1 {:} #2) = (#3 {:} #4)}
177 \newcommand{\myprop}{\mytyc{Prop}}
179 %% -----------------------------------------------------------------------------
181 \title{\mykant: Implementing Observational Equality}
182 \author{Francesco Mazzoli \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{<fm2209@ic.ac.uk>}}}
196 The marriage between programming and logic has been a very fertile one. In
197 particular, since the simply typed lambda calculus (STLC), a number of type
198 systems have been devised with increasing expressive power.
200 Section \ref{sec:types} will give a very brief overview of STLC, and then
201 illustrate how it can be interpreted as a natural deduction system. Section
202 \ref{sec:itt} will introduce Inutitionistic Type Theory (ITT), which expands
203 on this concept, employing a more expressive logic. The exposition is quite
204 dense since there is a lot of material to cover; for a more complete treatment
205 of the material the reader can refer to \citep{Thompson1991, Pierce2002}.
206 Section \ref{sec:equality} will explain why equality has always been a tricky
207 business in these theories, and talk about the various attempts that have been
208 made to make the situation better. One interesting development has recently
209 emerged: Observational Type theory.
211 Section \ref{sec:practical} will describe common extensions found in the
212 systems currently in use. Finally, section \ref{sec:kant} will describe a
213 system developed by the author that implements a core calculus based on the
214 principles described.
223 \section{Simple and not-so-simple types}
226 \subsection{The untyped $\lambda$-calculus}
228 Along with Turing's machines, the earliest attempts to formalise computation
229 lead to the $\lambda$-calculus \citep{Church1936}. This early programming
230 language encodes computation with a minimal syntax and no `data' in the
231 traditional sense, but just functions. Here we give a brief overview of the
232 language, which will give the chance to introduce concepts central to the
233 analysis of all the following calculi. The exposition follows the one found in
234 chapter 5 of \cite{Queinnec2003}.
236 The syntax of $\lambda$-terms consists of three things: variables, abstractions,
241 \begin{array}{r@{\ }c@{\ }l}
242 \mytmsyn & ::= & \myb{x} \mysynsep \myabs{\myb{x}}{\mytmsyn} \mysynsep (\myapp{\mytmsyn}{\mytmsyn}) \\
243 x & \in & \text{Some enumerable set of symbols}
248 Parenthesis will be omitted in the usual way:
249 $\myapp{\myapp{\mytmt}{\mytmm}}{\mytmn} =
250 \myapp{(\myapp{\mytmt}{\mytmm})}{\mytmn}$.
252 Abstractions roughly corresponds to functions, and their semantics is more
253 formally explained by the $\beta$-reduction rule:
255 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
258 \myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{\myb{x}}{\mytmn}\text{, where} \\
260 \begin{array}{l@{\ }c@{\ }l}
261 \mysub{\myb{x}}{\myb{x}}{\mytmn} & = & \mytmn \\
262 \mysub{\myb{y}}{\myb{x}}{\mytmn} & = & y\text{, with } \myb{x} \neq y \\
263 \mysub{(\myapp{\mytmt}{\mytmm})}{\myb{x}}{\mytmn} & = & (\myapp{\mysub{\mytmt}{\myb{x}}{\mytmn}}{\mysub{\mytmm}{\myb{x}}{\mytmn}}) \\
264 \mysub{(\myabs{\myb{x}}{\mytmm})}{\myb{x}}{\mytmn} & = & \myabs{\myb{x}}{\mytmm} \\
265 \mysub{(\myabs{\myb{y}}{\mytmm})}{\myb{x}}{\mytmn} & = & \myabs{\myb{z}}{\mysub{\mysub{\mytmm}{\myb{y}}{\myb{z}}}{\myb{x}}{\mytmn}}, \\
266 \multicolumn{3}{l}{\myind{1} \text{with $\myb{x} \neq \myb{y}$ and $\myb{z}$ not free in $\myapp{\mytmm}{\mytmn}$}}
272 The care required during substituting variables for terms is required to avoid
273 name capturing. We will use substitution in the future for other name-binding
274 constructs assuming similar precautions.
276 These few elements are of remarkable expressiveness, and in fact Turing
277 complete. As a corollary, we must be able to devise a term that reduces forever
278 (`loops' in imperative terms):
280 (\myapp{\omega}{\omega}) \myred (\myapp{\omega}{\omega}) \myred \dots\text{, with $\omega = \myabs{x}{\myapp{x}{x}}$}
283 A \emph{redex} is a term that can be reduced. In the untyped $\lambda$-calculus
284 this will be the case for an application in which the first term is an
285 abstraction, but in general we call aterm reducible if it appears to the left of
286 a reduction rule. When a term contains no redexes it's said to be in
287 \emph{normal form}. Given the observation above, not all terms reduce to a
288 normal forms: we call the ones that do \emph{normalising}, and the ones that
289 don't \emph{non-normalising}.
291 The reduction rule presented is not syntax directed, but \emph{evaluation
292 strategies} can be employed to reduce term systematically. Common evaluation
293 strategies include \emph{call by value} (or \emph{strict}), where arguments of
294 abstractions are reduced before being applied to the abstraction; and conversely
295 \emph{call by name} (or \emph{lazy}), where we reduce only when we need to do so
296 to proceed---in other words when we have an application where the function is
297 still not a $\lambda$. In both these reduction strategies we never reduce under
298 an abstraction: for this reason a weaker form of normalisation is used, where
299 both abstractions and normal forms are said to be in \emph{weak head normal
302 \subsection{The simply typed $\lambda$-calculus}
304 A convenient way to `discipline' and reason about $\lambda$-terms is to assign
305 \emph{types} to them, and then check that the terms that we are forming make
306 sense given our typing rules \citep{Curry1934}. The first most basic instance
307 of this idea takes the name of \emph{simply typed $\lambda$ calculus}, whose
308 rules are shown in figure \ref{fig:stlc}.
310 Our types contain a set of \emph{type variables} $\Phi$, which might correspond
311 to some `primitive' types; and $\myarr$, the type former for `arrow' types, the
312 types of functions. The language is explicitly typed: when we bring a variable
313 into scope with an abstraction, we explicitly declare its type. $\mytya$,
314 $\mytyb$, $\mytycc$, will be used to refer to a generic type. Reduction is
315 unchanged from the untyped $\lambda$-calculus.
320 \begin{array}{r@{\ }c@{\ }l}
321 \mytmsyn & ::= & \myb{x} \mysynsep \myabss{\myb{x}}{\mytysyn}{\mytmsyn} \mysynsep
322 (\myapp{\mytmsyn}{\mytmsyn}) \\
323 \mytysyn & ::= & \myse{\phi} \mysynsep \mytysyn \myarr \mytysyn \mysynsep \\
324 \myb{x} & \in & \text{Some enumerable set of symbols} \\
325 \myse{\phi} & \in & \Phi
330 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
333 \AxiomC{$\myctx(x) = A$}
334 \UnaryInfC{$\myjud{\myb{x}}{A}$}
337 \AxiomC{$\myjudd{\myctx;\myb{x} : A}{\mytmt}{\mytyb}$}
338 \UnaryInfC{$\myjud{\myabss{x}{A}{\mytmt}}{\mytyb}$}
341 \AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$}
342 \AxiomC{$\myjud{\mytmn}{\mytya}$}
343 \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mytyb}$}
348 \caption{Syntax and typing rules for the STLC. Reduction is unchanged from
349 the untyped $\lambda$-calculus.}
353 In the typing rules, a context $\myctx$ is used to store the types of bound
354 variables: $\myctx; \myb{x} : \mytya$ adds a variable to the context and
355 $\myctx(x)$ returns the type of the rightmost occurrence of $x$.
357 This typing system takes the name of `simply typed lambda calculus' (STLC), and
358 enjoys a number of properties. Two of them are expected in most type systems
361 \item[Progress] A well-typed term is not stuck---it is either a variable, or its
362 constructor does not appear on the left of the $\myred$ relation (currently
363 only $\lambda$), or it can take a step according to the evaluation rules.
364 \item[Preservation] If a well-typed term takes a step of evaluation, then the
365 resulting term is also well-typed, and preserves the previous type. Also
366 known as \emph{subject reduction}.
369 However, STLC buys us much more: every well-typed term is normalising
370 \citep{Tait1967}. It is easy to see that we can't fill the blanks if we want to
371 give types to the non-normalising term shown before:
373 \myapp{(\myabss{\myb{x}}{\myhole{?}}{\myapp{\myb{x}}{\myb{x}}})}{(\myabss{\myb{x}}{\myhole{?}}{\myapp{\myb{x}}{\myb{x}}})}
376 This makes the STLC Turing incomplete. We can recover the ability to loop by
377 adding a combinator that recurses:
380 \begin{minipage}{0.5\textwidth}
382 $ \mytmsyn ::= \dotsb \mysynsep \myfix{\myb{x}}{\mytysyn}{\mytmsyn} $
386 \begin{minipage}{0.5\textwidth}
387 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}} {
389 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytmt}{\mytya}$}
390 \UnaryInfC{$\myjud{\myfix{\myb{x}}{\mytya}{\mytmt}}{\mytya}$}
396 \mydesc{reduction:}{\myjud{\mytmsyn}{\mytmsyn}}{
398 $ \myfix{\myb{x}}{\mytya}{\mytmt} \myred \mysub{\mytmt}{\myb{x}}{(\myfix{\myb{x}}{\mytya}{\mytmt})}$
402 This will deprive us of normalisation, which is a particularly bad thing if we
403 want to use the STLC as described in the next section.
405 \subsection{The Curry-Howard correspondence}
407 It turns out that the STLC can be seen a natural deduction system for
408 intuitionistic propositional logic. Terms are proofs, and their types are the
409 propositions they prove. This remarkable fact is known as the Curry-Howard
410 correspondence, or isomorphism.
412 The arrow ($\myarr$) type corresponds to implication. If we wish to prove that
413 that $(\mytya \myarr \mytyb) \myarr (\mytyb \myarr \mytycc) \myarr (\mytya
414 \myarr \mytycc)$, all we need to do is to devise a $\lambda$-term that has the
417 \myabss{\myb{f}}{(\mytya \myarr \mytyb)}{\myabss{\myb{g}}{(\mytyb \myarr \mytycc)}{\myabss{\myb{x}}{\mytya}{\myapp{\myb{g}}{(\myapp{\myb{f}}{\myb{x}})}}}}
419 That is, function composition. Going beyond arrow types, we can extend our bare
420 lambda calculus with useful types to represent other logical constructs, as
421 shown in figure \ref{fig:natded}.
426 \begin{array}{r@{\ }c@{\ }l}
427 \mytmsyn & ::= & \dots \\
428 & | & \mytt \mysynsep \myapp{\myabsurd{\mytysyn}}{\mytmsyn} \\
429 & | & \myapp{\myleft{\mytysyn}}{\mytmsyn} \mysynsep
430 \myapp{\myright{\mytysyn}}{\mytmsyn} \mysynsep
431 \myapp{\mycase{\mytmsyn}{\mytmsyn}}{\mytmsyn} \\
432 & | & \mypair{\mytmsyn}{\mytmsyn} \mysynsep
433 \myapp{\myfst}{\mytmsyn} \mysynsep \myapp{\mysnd}{\mytmsyn} \\
434 \mytysyn & ::= & \dots \mysynsep \myunit \mysynsep \myempty \mysynsep \mytmsyn \mysum \mytmsyn \mysynsep \mytysyn \myprod \mytysyn
439 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
443 \begin{array}{l@{ }l@{\ }c@{\ }l}
444 \myapp{\mycase{\mytmm}{\mytmn}}{(\myapp{\myleft{\mytya} &}{\mytmt})} & \myred &
445 \myapp{\mytmm}{\mytmt} \\
446 \myapp{\mycase{\mytmm}{\mytmn}}{(\myapp{\myright{\mytya} &}{\mytmt})} & \myred &
447 \myapp{\mytmn}{\mytmt}
452 \begin{array}{l@{ }l@{\ }c@{\ }l}
453 \myapp{\myfst &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmm \\
454 \myapp{\mysnd &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmn
461 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
464 \AxiomC{\phantom{$\myjud{\mytmt}{\myempty}$}}
465 \UnaryInfC{$\myjud{\mytt}{\myunit}$}
468 \AxiomC{$\myjud{\mytmt}{\myempty}$}
469 \UnaryInfC{$\myjud{\myapp{\myabsurd{\mytya}}{\mytmt}}{\mytya}$}
476 \AxiomC{$\myjud{\mytmt}{\mytya}$}
477 \UnaryInfC{$\myjud{\myapp{\myleft{\mytyb}}{\mytmt}}{\mytya \mysum \mytyb}$}
480 \AxiomC{$\myjud{\mytmt}{\mytyb}$}
481 \UnaryInfC{$\myjud{\myapp{\myright{\mytya}}{\mytmt}}{\mytya \mysum \mytyb}$}
489 \AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$}
490 \AxiomC{$\myjud{\mytmn}{\mytya \myarr \mytycc}$}
491 \AxiomC{$\myjud{\mytmt}{\mytya \mysum \mytyb}$}
492 \TrinaryInfC{$\myjud{\myapp{\mycase{\mytmm}{\mytmn}}{\mytmt}}{\mytycc}$}
499 \AxiomC{$\myjud{\mytmm}{\mytya}$}
500 \AxiomC{$\myjud{\mytmn}{\mytyb}$}
501 \BinaryInfC{$\myjud{\mypair{\mytmm}{\mytmn}}{\mytya \myprod \mytyb}$}
504 \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
505 \UnaryInfC{$\myjud{\myapp{\myfst}{\mytmt}}{\mytya}$}
508 \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
509 \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mytyb}$}
514 \caption{Rules for the extendend STLC. Only the new features are shown, all the
515 rules and syntax for the STLC apply here too.}
519 Tagged unions (or sums, or coproducts---$\mysum$ here, \texttt{Either} in
520 Haskell) correspond to disjunctions, and dually tuples (or pairs, or
521 products---$\myprod$ here, tuples in Haskell) correspond to conjunctions. This
522 is apparent looking at the ways to construct and destruct the values inhabiting
523 those types: for $\mysum$ $\myleft{ }$ and $\myright{ }$ correspond to $\vee$
524 introduction, and $\mycase{\_}{\_}$ to $\vee$ elimination; for $\myprod$
525 $\mypair{\_}{\_}$ corresponds to $\wedge$ introduction, $\myfst$ and $\mysnd$ to
526 $\wedge$ elimination.
528 The trivial type $\myunit$ corresponds to the logical $\top$, and dually
529 $\myempty$ corresponds to the logical $\bot$. $\myunit$ has one introduction
530 rule ($\mytt$), and thus one inhabitant; and no eliminators. $\myempty$ has no
531 introduction rules, and thus no inhabitants; and one eliminator ($\myabsurd{
532 }$), corresponding to the logical \emph{ex falso quodlibet}. Note that in the
533 constructors for the sums and the destructor for $\myempty$ we need to include
534 some type information to keep type checking decidable.
536 With these rules, our STLC now looks remarkably similar in power and use to the
537 natural deduction we already know. $\myneg \mytya$ can be expressed as $\mytya
538 \myarr \myempty$. However, there is an important omission: there is no term of
539 the type $\mytya \mysum \myneg \mytya$ (excluded middle), or equivalently
540 $\myneg \myneg \mytya \myarr \mytya$ (double negation), or indeed any term with
541 a type equivalent to those.
543 This has a considerable effect on our logic and it's no coincidence, since there
544 is no obvious computational behaviour for laws like the excluded middle.
545 Theories of this kind are called \emph{intuitionistic}, or \emph{constructive},
546 and all the systems analysed will have this characteristic since they build on
547 the foundation of the STLC\footnote{There is research to give computational
548 behaviour to classical logic, but I will not touch those subjects.}.
550 As in logic, if we want to keep our system consistent, we must make sure that no
551 closed terms (in other words terms not under a $\lambda$) inhabit $\myempty$.
552 The variant of STLC presented here is indeed
553 consistent, a result that follows from the fact that it is
554 normalising. % TODO explain
555 Going back to our $\mysyn{fix}$ combinator, it is easy to see how it ruins our
556 desire for consistency. The following term works for every type $\mytya$,
559 (\myfix{\myb{x}}{\mytya}{\myb{x}}) : \mytya
562 \subsection{Inductive data}
564 To make the STLC more useful as a programming language or reasoning tool it is
565 common to include (or let the user define) inductive data types. These comprise
566 of a type former, various constructors, and an eliminator (or destructor) that
567 serves as primitive recursor.
569 For example, we might add a $\mylist$ type constructor, along with an `empty
570 list' ($\mynil{ }$) and `cons cell' ($\mycons$) constructor. The eliminator for
571 lists will be the usual folding operation ($\myfoldr$). See figure
577 \begin{array}{r@{\ }c@{\ }l}
578 \mytmsyn & ::= & \dots \mysynsep \mynil{\mytysyn} \mysynsep \mytmsyn \mycons \mytmsyn
580 \myapp{\myapp{\myapp{\myfoldr}{\mytmsyn}}{\mytmsyn}}{\mytmsyn} \\
581 \mytysyn & ::= & \dots \mysynsep \myapp{\mylist}{\mytysyn}
585 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
588 \begin{array}{l@{\ }c@{\ }l}
589 \myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{\mynil{\mytya}} & \myred & \mytmt \\
591 \myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{(\mytmm \mycons \mytmn)} & \myred &
592 \myapp{\myapp{\myse{f}}{\mytmm}}{(\myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{\mytmn})}
597 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
600 \AxiomC{\phantom{$\myjud{\mytmm}{\mytya}$}}
601 \UnaryInfC{$\myjud{\mynil{\mytya}}{\myapp{\mylist}{\mytya}}$}
604 \AxiomC{$\myjud{\mytmm}{\mytya}$}
605 \AxiomC{$\myjud{\mytmn}{\myapp{\mylist}{\mytya}}$}
606 \BinaryInfC{$\myjud{\mytmm \mycons \mytmn}{\myapp{\mylist}{\mytya}}$}
612 \AxiomC{$\myjud{\mysynel{f}}{\mytya \myarr \mytyb \myarr \mytyb}$}
613 \AxiomC{$\myjud{\mytmm}{\mytyb}$}
614 \AxiomC{$\myjud{\mytmn}{\myapp{\mylist}{\mytya}}$}
615 \TrinaryInfC{$\myjud{\myapp{\myapp{\myapp{\myfoldr}{\mysynel{f}}}{\mytmm}}{\mytmn}}{\mytyb}$}
619 \caption{Rules for lists in the STLC.}
623 In section \ref{sec:well-order} we will see how to give a general account of
624 inductive data. %TODO does this make sense to have here?
626 \section{Intuitionistic Type Theory}
629 \subsection{Extending the STLC}
631 The STLC can be made more expressive in various ways. \cite{Barendregt1991}
632 succinctly expressed geometrically how we can add expressivity:
636 & \lambda\omega \ar@{-}[rr]\ar@{-}'[d][dd]
637 & & \lambda C \ar@{-}[dd]
639 \lambda2 \ar@{-}[ur]\ar@{-}[rr]\ar@{-}[dd]
640 & & \lambda P2 \ar@{-}[ur]\ar@{-}[dd]
642 & \lambda\underline\omega \ar@{-}'[r][rr]
643 & & \lambda P\underline\omega
645 \lambda{\to} \ar@{-}[rr]\ar@{-}[ur]
646 & & \lambda P \ar@{-}[ur]
649 Here $\lambda{\to}$, in the bottom left, is the STLC. From there can move along
652 \item[Terms depending on types (towards $\lambda{2}$)] We can quantify over
653 types in our type signatures. For example, we can define a polymorphic
656 (\myabss{\myb{A}}{\mytyp}{\myabss{\myb{x}}{\myb{A}}{\myb{x}}}) : (\myb{A} : \mytyp) \myarr \myb{A} \myarr \myb{A}
658 The first and most famous instance of this idea has been System F. This form
659 of polymorphism and has been wildly successful, also thanks to a well known
660 inference algorithm for a restricted version of System F known as
661 Hindley-Milner. Languages like Haskell and SML are based on this discipline.
662 \item[Types depending on types (towards $\lambda{\underline{\omega}}$)] We have
663 type operators. For example we could define a function that given types $R$
664 and $\mytya$ forms the type that represents a value of type $\mytya$ in
665 continuation passing style: \[\displaystyle(\myabss{\myb{A} \myar \myb{R}}{\mytyp}{(\myb{A}
666 \myarr \myb{R}) \myarr \myb{R}}) : \mytyp \myarr \mytyp \myarr \mytyp\]
667 \item[Types depending on terms (towards $\lambda{P}$)] Also known as `dependent
668 types', give great expressive power. For example, we can have values of whose
669 type depend on a boolean:
670 \[\displaystyle(\myabss{\myb{x}}{\mybool}{\myite{\myb{x}}{\mynat}{\myrat}}) : \mybool
674 All the systems preserve the properties that make the STLC well behaved. The
675 system we are going to focus on, Intuitionistic Type Theory, has all of the
676 above additions, and thus would sit where $\lambda{C}$ sits in the
677 `$\lambda$-cube'. It will serve as the logical `core' of all the other
678 extensions that we will present and ultimately our implementation of a similar
681 \subsection{A Bit of History}
683 Logic frameworks and programming languages based on type theory have a long
684 history. Per Martin-L\"{o}f described the first version of his theory in 1971,
685 but then revised it since the original version was inconsistent due to its
686 impredicativity\footnote{In the early version there was only one universe
687 $\mytyp$ and $\mytyp : \mytyp$, see section \ref{sec:term-types} for an
688 explanation on why this causes problems.}. For this reason he gave a revised
689 and consistent definition later \citep{Martin-Lof1984}.
691 A related development is the polymorphic $\lambda$-calculus, and specifically
692 the previously mentioned System F, which was developed independently by Girard
693 and Reynolds. An overview can be found in \citep{Reynolds1994}. The surprising
694 fact is that while System F is impredicative it is still consistent and strongly
695 normalising. \cite{Coquand1986} further extended this line of work with the
696 Calculus of Constructions (CoC).
698 Most widely used interactive theorem provers are based on ITT. Popular ones
699 include Agda \citep{Norell2007, Bove2009}, Coq \citep{Coq}, and Epigram
700 \citep{McBride2004, EpigramTut}.
702 \subsection{A note on inference}
704 % TODO do this, adding links to the sections about bidi type checking and
705 % implicit universes.
706 In the following text I will often omit explicit typing for abstractions or
708 Moreover, I will use $\mytyp$ without bothering to specify a
709 universe, with the silent assumption that the definition is consistent
710 regarding to the hierarchy.
712 \subsection{A simple type theory}
715 The calculus I present follows the exposition in \citep{Thompson1991}, and is
716 quite close to the original formulation of predicative ITT as found in
717 \citep{Martin-Lof1984}. The system's syntax and reduction rules are presented
718 in their entirety in figure \ref{fig:core-tt-syn}. The typing rules are
719 presented piece by piece. An Agda rendition of the presented theory is
720 reproduced in appendix \ref{app:agda-code}.
725 \begin{array}{r@{\ }c@{\ }l}
726 \mytmsyn & ::= & \myb{x} \mysynsep
728 \myunit \mysynsep \mytt \mysynsep
729 \myempty \mysynsep \myapp{\myabsurd{\mytmsyn}}{\mytmsyn} \\
730 & | & \mybool \mysynsep \mytrue \mysynsep \myfalse \mysynsep
731 \myitee{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
732 & | & \myfora{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
733 \myabss{\myb{x}}{\mytmsyn}{\mytmsyn} \\
734 & | & \myexi{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
735 \mypairr{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn} \\
736 & | & \myapp{\myfst}{\mytmsyn} \mysynsep \myapp{\mysnd}{\mytmsyn} \\
737 & | & \myw{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
738 \mytmsyn \mynode{\myb{x}}{\mytmsyn} \mytmsyn \\
739 & | & \myrec{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn} \\
745 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
749 \begin{array}{l@{ }l@{\ }c@{\ }l}
750 \myitee{\mytrue &}{\myb{x}}{\myse{P}}{\mytmm}{\mytmn} & \myred & \mytmm \\
751 \myitee{\myfalse &}{\myb{x}}{\myse{P}}{\mytmm}{\mytmn} & \myred & \mytmn \\
756 \myapp{(\myabss{\myb{x}}{\mytya}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{\myb{x}}{\mytmn}
761 \begin{array}{l@{ }l@{\ }c@{\ }l}
762 \myapp{\myfst &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmm \\
763 \myapp{\mysnd &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmn
769 \myrec{(\myse{s} \mynode{\myb{x}}{\myse{T}} \myse{f})}{\myb{y}}{\myse{P}}{\myse{p}} \myred
770 \myapp{\myapp{\myapp{\myse{p}}{\myse{s}}}{\myse{f}}}{(\myabss{\myb{t}}{\mysub{\myse{T}}{\myb{x}}{\myse{s}}}{
771 \myrec{\myapp{\myse{f}}{\myb{t}}}{\myb{y}}{\myse{P}}{\mytmt}
776 \caption{Syntax and reduction rules for our type theory.}
777 \label{fig:core-tt-syn}
780 \subsubsection{Types are terms, some terms are types}
781 \label{sec:term-types}
783 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
786 \AxiomC{$\myjud{\mytmt}{\mytya}$}
787 \AxiomC{$\mytya \mydefeq \mytyb$}
788 \BinaryInfC{$\myjud{\mytmt}{\mytyb}$}
791 \AxiomC{\phantom{$\myjud{\mytmt}{\mytya}$}}
792 \UnaryInfC{$\myjud{\mytyp_l}{\mytyp_{l + 1}}$}
798 The first thing to notice is that a barrier between values and types that we had
799 in the STLC is gone: values can appear in types, and the two are treated
800 uniformly in the syntax.
802 While the usefulness of doing this will become clear soon, a consequence is
803 that since types can be the result of computation, deciding type equality is
804 not immediate as in the STLC. For this reason we define \emph{definitional
805 equality}, $\mydefeq$, as the congruence relation extending
806 $\myred$---moreover, when comparing types syntactically we do it up to
807 renaming of bound names ($\alpha$-renaming). For example under this
808 discipline we will find that
810 \myabss{\myb{x}}{\mytya}{\myb{x}} \mydefeq \myabss{\myb{y}}{\mytya}{\myb{y}}
812 Types that are definitionally equal can be used interchangeably. Here the
813 `conversion' rule is not syntax directed, however we will see how it is
814 possible to employ $\myred$ to decide term equality in a systematic
815 way. % TODO add section
816 Another thing to notice is that considering the need to reduce terms to decide
817 equality, it is essential for a dependently type system to be terminating and
818 confluent for type checking to be decidable.
820 Moreover, we specify a \emph{type hierarchy} to talk about `large' types:
821 $\mytyp_0$ will be the type of types inhabited by data: $\mybool$, $\mynat$,
822 $\mylist$, etc. $\mytyp_1$ will be the type of $\mytyp_0$, and so on---for
823 example we have $\mytrue : \mybool : \mytyp_0 : \mytyp_1 : \dots$. Each type
824 `level' is often called a universe in the literature. While it is possible,
825 to simplify things by having only one universe $\mytyp$ with $\mytyp :
826 \mytyp$, this plan is inconsistent for much the same reason that impredicative
827 na\"{\i}ve set theory is \citep{Hurkens1995}. Moreover, various techniques
828 can be employed to lift the burden of explicitly handling universes.
829 % TODO add sectioon about universes
831 \subsubsection{Contexts}
833 \begin{minipage}{0.5\textwidth}
834 \mydesc{context validity:}{\myvalid{\myctx}}{
837 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
838 \UnaryInfC{$\myvalid{\myemptyctx}$}
841 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
842 \UnaryInfC{$\myvalid{\myctx ; \myb{x} : \mytya}$}
848 \begin{minipage}{0.5\textwidth}
849 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
851 \AxiomC{$\myctx(x) = \mytya$}
852 \UnaryInfC{$\myjud{\myb{x}}{\mytya}$}
859 We need to refine the notion context to make sure that every variable appearing
860 is typed correctly, or that in other words each type appearing in the context is
861 indeed a type and not a value. In every other rule, if no premises are present,
862 we assume the context in the conclusion to be valid.
864 Then we can re-introduce the old rule to get the type of a variable for a
867 \subsubsection{$\myunit$, $\myempty$}
869 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
872 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
873 \UnaryInfC{$\myjud{\myunit}{\mytyp_0}$}
875 \UnaryInfC{$\myjud{\myempty}{\mytyp_0}$}
878 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
879 \UnaryInfC{$\myjud{\mytt}{\myunit}$}
881 \UnaryInfC{\phantom{$\myjud{\myempty}{\mytyp_0}$}}
884 \AxiomC{$\myjud{\mytmt}{\myempty}$}
885 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
886 \BinaryInfC{$\myjud{\myapp{\myabsurd{\mytya}}{\mytmt}}{\mytya}$}
888 \UnaryInfC{\phantom{$\myjud{\myempty}{\mytyp_0}$}}
894 Nothing surprising here: $\myunit$ and $\myempty$ are unchanged from the STLC,
895 with the added rules to type $\myunit$ and $\myempty$ themselves, and to make
896 sure that we are invoking $\myabsurd{}$ over a type.
898 \subsubsection{$\mybool$, and dependent $\myfun{if}$}
900 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
904 \UnaryInfC{$\myjud{\mybool}{\mytyp_0}$}
908 \UnaryInfC{$\myjud{\mytrue}{\mybool}$}
912 \UnaryInfC{$\myjud{\myfalse}{\mybool}$}
917 \AxiomC{$\myjud{\mytmt}{\mybool}$}
918 \AxiomC{$\myjudd{\myctx : \mybool}{\mytya}{\mytyp_l}$}
920 \BinaryInfC{$\myjud{\mytmm}{\mysub{\mytya}{x}{\mytrue}}$ \hspace{0.7cm} $\myjud{\mytmn}{\mysub{\mytya}{x}{\myfalse}}$}
921 \UnaryInfC{$\myjud{\myitee{\mytmt}{\myb{x}}{\mytya}{\mytmm}{\mytmn}}{\mysub{\mytya}{\myb{x}}{\mytmt}}$}
927 With booleans we get the first taste of `dependent' in `dependent types'. While
928 the two introduction rules ($\mytrue$ and $\myfalse$) are not surprising, the
929 typing rules for $\myfun{if}$ are. In most strongly typed languages we expect
930 the branches of an $\myfun{if}$ statements to be of the same type, to preserve
931 subject reduction, since execution could take both paths. This is a pity, since
932 the type system does not reflect the fact that in each branch we gain knowledge
933 on the term we are branching on. Which means that programs along the lines of
935 if null xs then head xs else 0
937 are a necessary, well typed, danger.
939 However, in a more expressive system, we can do better: the branches' type can
940 depend on the value of the scrutinised boolean. This is what the typing rule
941 expresses: the user provides a type $\mytya$ ranging over an $\myb{x}$
942 representing the scrutinised boolean type, and the branches are typechecked with
943 the updated knowledge on the value of $\myb{x}$.
945 \subsubsection{$\myarr$, or dependent function}
947 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
949 \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
950 \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
951 \BinaryInfC{$\myjud{\myfora{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
957 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytmt}{\mytyb}$}
958 \UnaryInfC{$\myjud{\myabss{\myb{x}}{\mytya}{\mytmt}}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
961 \AxiomC{$\myjud{\mytmm}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
962 \AxiomC{$\myjud{\mytmn}{\mytya}$}
963 \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mysub{\mytyb}{\myb{x}}{\mytmn}}$}
969 Dependent functions are one of the two key features that perhaps most
970 characterise dependent types---the other being dependent products. With
971 dependent functions, the result type can depend on the value of the argument.
972 This feature, together with the fact that the result type might be a type
973 itself, brings a lot of interesting possibilities. Keeping the correspondence
974 with logic alive, dependent functions are much like universal quantifiers
975 ($\forall$) in logic.
977 Again, we need to make sure that the type hierarchy is respected, which is the
978 reason why a type formed by $\myarr$ will live in the least upper bound of the
979 levels of argument and return type. This trend will continue with the other
980 type-level binders, $\myprod$ and $\mytyc{W}$.
982 % TODO maybe examples?
984 \subsubsection{$\myprod$, or dependent product}
987 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
989 \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
990 \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
991 \BinaryInfC{$\myjud{\myexi{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
997 \AxiomC{$\myjud{\mytmm}{\mytya}$}
998 \AxiomC{$\myjud{\mytmn}{\mysub{\mytyb}{\myb{x}}{\mytmm}}$}
999 \BinaryInfC{$\myjud{\mypairr{\mytmm}{\myb{x}}{\mytyb}{\mytmn}}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
1001 \UnaryInfC{\phantom{$--$}}
1004 \AxiomC{$\myjud{\mytmt}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
1005 \UnaryInfC{$\hspace{0.7cm}\myjud{\myapp{\myfst}{\mytmt}}{\mytya}\hspace{0.7cm}$}
1007 \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mysub{\mytyb}{\myb{x}}{\myapp{\myfst}{\mytmt}}}$}
1015 \subsubsection{$\mytyc{W}$, or well-order}
1016 \label{sec:well-order}
1018 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1020 \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
1021 \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
1022 \BinaryInfC{$\myjud{\myw{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
1027 \AxiomC{$\myjud{\mytmt}{\mytya}$}
1028 \AxiomC{$\myjud{\mysynel{f}}{\mysub{\mytyb}{\myb{x}}{\mytmt} \myarr \myw{\myb{x}}{\mytya}{\mytyb}}$}
1029 \BinaryInfC{$\myjud{\mytmt \mynode{\myb{x}}{\mytyb} \myse{f}}{\myw{\myb{x}}{\mytya}{\mytyb}}$}
1034 \AxiomC{$\myjud{\myse{u}}{\myw{\myb{x}}{\myse{S}}{\myse{T}}}$}
1035 \AxiomC{$\myjudd{\myctx; \myb{w} : \myw{\myb{x}}{\myse{S}}{\myse{T}}}{\myse{P}}{\mytyp_l}$}
1037 \BinaryInfC{$\myjud{\myse{p}}{
1038 \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}}}}
1040 \UnaryInfC{$\myjud{\myrec{\myse{u}}{\myb{w}}{\myse{P}}{\myse{p}}}{\mysub{\myse{P}}{\myb{w}}{\myse{u}}}$}
1045 \section{The struggle for equality}
1046 \label{sec:equality}
1048 In the previous section we saw how a type checker (or a human) needs a notion of
1049 \emph{definitional equality}. Beyond this meta-theoretic notion, in this
1050 section we will explore the ways of expressing equality \emph{inside} the
1051 theory, as a reasoning tool available to the user. This area is the main
1052 concern of this thesis, and in general a very active research topic, since we do
1053 not have a fully satisfactory solution, yet.
1055 \subsection{Propositional equality}
1058 \begin{minipage}{0.5\textwidth}
1061 \begin{array}{r@{\ }c@{\ }l}
1062 \mytmsyn & ::= & \dots \\
1063 & | & \mytmsyn \mypeq{\mytmsyn} \mytmsyn \mysynsep
1064 \myapp{\myrefl}{\mytmsyn} \\
1065 & | & \myjeq{\mytmsyn}{\mytmsyn}{\mytmsyn}
1070 \begin{minipage}{0.5\textwidth}
1071 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
1074 \myjeq{\myse{P}}{(\myapp{\myrefl}{\mytmm})}{\mytmn} \myred \mytmn
1081 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1083 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
1084 \AxiomC{$\myjud{\mytmm}{\mytya}$}
1085 \AxiomC{$\myjud{\mytmn}{\mytya}$}
1086 \TrinaryInfC{$\myjud{\mytmm \mypeq{\mytya} \mytmn}{\mytyp_l}$}
1092 \AxiomC{\phantom{$\myctx P \mytyp_l$}}
1094 \UnaryInfC{$\myjud{\mytmt}{\mytya}$}
1095 \UnaryInfC{$\myjud{\myapp{\myrefl}{\mytmt}}{\mytmt \mypeq{\mytya} \mytmt}$}
1098 \AxiomC{$\myjud{\myse{P}}{\myfora{\myb{x}\ \myb{y}}{\mytya}{\myfora{q}{\myb{x} \mypeq{\mytya} \myb{y}}{\mytyp_l}}}$}
1100 \UnaryInfC{$\myjud{\myse{q}}{\mytmm \mypeq{\mytya} \mytmn}\hspace{1.2cm}\myjud{\myse{p}}{\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmm}}{(\myapp{\myrefl}{\mytmm})}}$}
1101 \UnaryInfC{$\myjud{\myjeq{\myse{P}}{\myse{q}}{\myse{p}}}{\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmn}}{q}}$}
1107 To express equality between two terms inside ITT, the obvious way to do so is
1108 to have the equality construction to be a type-former. Here we present what
1109 has survived as the dominating form of equality in systems based on ITT up to
1112 Our type former is $\mypeq{\mytya}$, which given a type (in this case
1113 $\mytya$) relates equal terms of that type. $\mypeq{}$ has one introduction
1114 rule, $\myrefl$, which introduces an equality relation between definitionally
1115 equal terms---in the typing rule we display the term as `the same', meaning
1116 `the same up to $\mydefeq$'. % TODO maybe mention this earlier
1118 Finally, we have one eliminator for $\mypeq{}$, $\myjeqq$. $\myjeq{\myse{P}}{\myse{q}}{\myse{p}}$ takes
1120 \item $\myse{P}$, a predicate working with two terms of a certain type (say
1121 $\mytya$) and a proof of their equality
1122 \item $\myse{q}$, a proof that two terms in $\mytya$ (say $\myse{m}$ and
1123 $\myse{n}$) are equal
1124 \item and $\myse{p}$, an inhabitant of $\myse{P}$ applied to $\myse{m}$, plus
1125 the trivial proof by reflexivity showing that $\myse{m}$ is equal to itself
1127 Given these ingredients, $\myjeqq$ retuns a member of $\myse{P}$ applied to
1128 $\mytmm$, $\mytmn$, and $\myse{q}$. In other words $\myjeqq$ takes a
1129 witness that $\myse{P}$ works with \emph{definitionally equal} terms, and
1130 returns a witness of $\myse{P}$ working with \emph{propositionally equal}
1131 terms. Invokations of $\myjeqq$ will vanish when the equality proofs will
1132 reduce to invocations to reflexivity, at which point the arguments must be
1133 definitionally equal, and thus the provided
1134 $\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmm}}{(\myapp{\myrefl}{\mytmm})}$
1137 While the $\myjeqq$ rule is slightly convoluted, ve can derive many more
1138 `friendly' rules from it, for example a more obvious `substitution' rule, that
1139 replaces equal for equal in predicates:
1142 (\myabs{\myb{A}\ \myb{P}\ \myb{x}\ \myb{y}\ \myb{q}\ \myb{p}}{
1143 \myjeq{(\myabs{\myb{x}\ \myb{y}\ \myb{q}}{\myapp{\myb{P}}{\myb{y}}})}{\myb{q}}{\myb{p}}}) : \\
1144 \myind{1} \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}}}}}
1147 This rule is often called $\myfun{subst}$---here we will invoke it without
1148 specifying the type ($\myb{A}$) and the sides of the equality
1149 ($\myb{x},\myb{y}$).
1151 Once we have $\myfun{subst}$, we can easily prove more familiar laws regarding
1152 equality, such as symmetry, transitivity, and a congruence law:
1156 \subsection{Common extensions}
1164 \subsection{Limitations}
1166 \epigraph{\emph{Half of my time spent doing research involves thinking up clever
1167 schemes to avoid needing functional extensionality.}}{@larrytheliquid}
1169 However, propositional equality as described is quite restricted when
1170 reasoning about equality beyond the term structure, which is what definitional
1171 equality gives us (extension notwithstanding).
1173 The problem is best exemplified by \emph{function extensionality}. In
1174 mathematics, we would expect to be able to treat functions that give equal
1175 output for equal input as the same. When reasoning in a mechanised framework
1176 we ought to be able to do the same: in the end, without considering the
1177 operational behaviour, all functions equal extensionally are going to be
1178 replaceable with one another.
1180 However this is not the case, or in other words with the tools we have we have
1183 \myfun{ext} : \myfora{\myb{A}\ \myb{B}}{\mytyp}{\myfora{\myb{f}\ \myb{g}}{
1184 \myb{A} \myarr \myb{B}}{
1185 (\myfora{\myb{x}}{\myb{A}}{\myapp{\myb{f}}{\myb{x}} \mypeq{\myb{B}} \myapp{\myb{g}}{\myb{x}}}) \myarr
1186 \myb{f} \mypeq{\myb{A} \myarr \myb{B}} \myb{g}
1190 To see why this is the case, consider the functions
1191 \[\myabs{\myb{x}}{0 \mathrel{\myfun{+}} \myb{x}}$ and $\myabs{\myb{x}}{\myb{x} \mathrel{\myfun{+}} 0}\]
1192 where $\myfun{+}$ is defined by recursion on the first argument, gradually
1193 destructing it to build up successors of the second argument. The two
1194 functions are clearly denotationally the same, and we can in fact prove that
1196 \myfora{\myb{x}}{\mynat}{(0 \mathrel{\myfun{+}} \myb{x}) \mypeq{\mynat} (\myb{x} \mathrel{\myfun{+}} 0)}
1198 By analysis on the $\myb{x}$. However, the two functions are not
1199 definitionally equal, and thus we won't be able to get rid of the
1202 For the reasons above, theories that offer a propositional equality similar to
1203 what we presented are called \emph{intensional}, as opposed to
1204 \emph{extensional}. Most systems in wide use today (such as Agda, Coq and
1205 Epigram) are of this kind.
1207 This is quite an annoyance that often makes reasoning awkward to execute. It
1208 also extends to other fields, for example proving bisimulation between
1209 processes specified by coinduction, or in general proving equivalences based
1210 on the behaviour on a term.
1212 \subsection{Equality reflection}
1214 One way to `solve' this problem is by identifying propositional equality with
1215 definitional equality:
1217 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1219 \AxiomC{$\myjud{\myse{q}}{\mytmm \mypeq{\mytya} \mytmn}$}
1220 \UnaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\mytya}$}
1225 This rule takes the name of \emph{equality reflection}, and is a very
1226 different rule from the ones we saw up to now: it links a typing judgement
1227 internal to the type theory to a meta-theoretic judgement that the type
1228 checker uses to work with terms. It is easy to see the dangerous consequences
1231 \item The rule is syntax directed, and the type checker is presumably expected
1232 to come up with equality proofs when needed.
1233 \item More worryingly, type checking becomes undecidable also because
1234 computing under false assumptions becomes unsafe.
1235 Consider for example
1237 \myabss{\myb{q}}{\mytya \mypeq{\mytyp} (\mytya \myarr \mytya)}{\myhole{?}}
1239 Using the assumed proof in tandem with equality reflection we could easily
1240 write a classic Y combinator, sending the compiler into a loop.
1243 Given these facts theories employing equality reflection, like NuPRL
1244 \citep{NuPRL}, carry the derivations that gave rise to each typing judgement
1245 to keep the systems manageable. % TODO more info, problems with that.
1247 For all its faults, equality reflection does allow us to prove extensionality,
1248 using the extensions we gave above. Assuming that $\myctx$ contains
1249 \[\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}}}\]
1252 \AxiomC{$\myjudd{\myctx; \myb{x} : \myb{A}}{\myapp{\myb{q}}{\myb{x}}}{\myapp{\myb{f}}{\myb{x}} \mypeq{} \myapp{\myb{g}}{\myb{x}}}$}
1253 \RightLabel{equality reflection}
1254 \UnaryInfC{$\myjudd{\myctx; \myb{x} : \myb{A}}{\myapp{\myb{f}}{\myb{x}} \mydefeq \myapp{\myb{g}}{\myb{x}}}{\myb{B}}$}
1255 \RightLabel{congruence for $\lambda$s}
1256 \UnaryInfC{$\myjud{(\myabs{\myb{x}}{\myapp{\myb{f}}{\myb{x}}}) \mydefeq (\myabs{\myb{x}}{\myapp{\myb{g}}{\myb{x}}})}{\myb{A} \myarr \myb{B}}$}
1257 \RightLabel{$\eta$-law for $\lambda$}
1258 \UnaryInfC{$\myjud{\myb{f} \mydefeq \myb{g}}{\myb{A} \myarr \myb{B}}$}
1259 \RightLabel{$\myrefl$}
1260 \UnaryInfC{$\myjud{\myapp{\myrefl}{\myb{f}}}{\myb{f} \mypeq{} \myb{g}}$}
1263 Now, the question is: do we need to give up well-behavedness of our theory to
1264 gain extensionality?
1266 \subsection{Observational equality}
1269 % TODO should we explain this in detail?
1270 A recent development by \citet{Altenkirch2007}, \emph{Observational Type
1271 Theory} (OTT), promises to keep the well behavedness of ITT while being able
1272 to gain many useful equality proofs\footnote{It is suspected that OTT gains
1273 \emph{all} the equality proofs of ETT, but no proof exists yet.}, including
1274 function extensionality. The main idea is to give the user the possibility to
1275 \emph{coerce} (or transport) values from a type $\mytya$ to a type $\mytyb$,
1276 if the type checker can prove structurally that $\mytya$ and $\mytya$ are
1277 equal; and providing a value-level equality based on similar principles. A
1278 brief overview is given below,
1282 \begin{array}{r@{\ }c@{\ }l}
1283 \mytmsyn & ::= & \dots \\
1284 & | & \myprdec{\myprsyn} \mysynsep
1285 \mycoee{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \mysynsep
1286 \mycohh{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
1287 \myprsyn & ::= & \mybot \mysynsep \mytop \mysynsep \myprsyn \myand \myprsyn
1288 \mysynsep \myprfora{\myb{x}}{\mytmsyn}{\myprsyn} \\\
1289 & | & \mytmsyn = \mytmsyn \mysynsep
1290 \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn}
1294 \mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
1299 The original presentation of OTT employs the theory presented above. It is
1300 close to the one presented in section \ref{sec:itt}, with the additions
1301 presented above, and the change that only one the `first' universe, the type
1302 of small types ($\mytyp_0$), is present.
1304 The propositional universe is meant to be where equality proofs live in. The
1305 equality proofs are respectively between types ($\mytya = \mytyb$), and
1310 However, only one universe is present ($\mytyp_0$), and a \emph{propositional}
1311 universe is isolated, intended to be the universe where equality proofs live
1312 in. Propositions (as long as our system is consistent) are inhabited only by
1313 one element, and thus can all be treated as definitionally equal.
1317 \section{Augmenting ITT}
1318 \label{sec:practical}
1320 \subsection{A more liberal hierarchy}
1322 \subsection{Type inference}
1324 \subsubsection{Bidirectional type checking}
1326 \subsubsection{Pattern unification}
1328 \subsection{Pattern matching and explicit fixpoints}
1330 \subsection{Induction-recursion}
1332 \subsection{Coinduction}
1334 \subsection{Dealing with partiality}
1336 \subsection{Type holes}
1341 \mykant is an interactive theorem prover developed as part of this thesis.
1342 The plan is to present a core language which would be capable of serving as
1343 the basis for a more featureful system, while still presenting interesting
1344 features and more importantly observational equality.
1346 The author learnt the hard way the implementations challenges for such a
1347 project, and while there is a solid and working base to work on, observational
1348 equality is not currently implemented. However, a detailed plan on how to add
1349 it this functionality is provided, and should not prove to be too much work.
1351 \subsection{High level overview}
1353 \subsubsection{Features}
1355 The features currently implemented in \mykant are:
1358 \item[Full dependent types] As we would expect, we have dependent a system
1359 which is as expressive as the `best' corner in the lambda cube described in
1360 section \ref{sec:itt}.
1362 \item[Implicit, cumulative universe hierarchy] The user does not need to
1363 specify universe level explicitly, and universes are \emph{cumulative}.
1365 \item[User defined data types and records] Instead of forcing the user to
1366 choose from a restricted toolbox, we let her define inductive data types,
1367 with associated primitive recursion operators; or records, with associated
1368 projections for each field.
1370 \item[Bidirectional type checking] While no `fancy' inference via unification
1371 is present, we take advantage of an type synthesis system in the style of
1372 \cite{Pierce2000}, extending the concept for user defined data types.
1374 \item[Type holes] When building up programs interactively, it is useful to
1375 leave parts unfinished while exploring the current context. This is what
1379 The planned features are:
1382 \item[Observational equality] As described in section \label{sec:ott} but
1383 extended to work with the type hierarchy and to admit equality between
1384 arbitrary data types.
1386 \item[Coinductive data] ...
1389 We will analyse the features one by one, along with motivations and tradeoffs
1390 for the design decisions made.
1392 \subsubsection{Implementation}
1394 The codebase consists of around 2500 lines of Haskell, as reported by the
1395 \texttt{cloc} utility. The high level design is heavily inspired by Conor
1396 McBride's work on various incarnations of Epigram, and specifically by the
1397 first version as described \citep{McBride2004} and the codebase for the new
1398 version \footnote{Available intermittently as a \texttt{darcs} repository at
1399 \url{http://sneezy.cs.nott.ac.uk/darcs/Pig09}.}. In many ways \mykant is
1400 something in between the first and second version of Epigram.
1402 The interaction happens in a read-eval-print loop (REPL). The repl is a
1403 available both as a commandline application and in a web interface, which is
1404 available at \url{kant.mazzo.li} and presents itself as in figure
1409 \includegraphics[scale=1.0]{kant-web.png}
1411 \caption{The \mykant web prompt.}
1412 \label{fig:kant-web}
1415 The interaction with the user takes place in a loop living in and updating a
1416 context \mykant declarations. The user inputs a new declaration that goes
1417 through various stages starts with the user inputing a \mykant declaration,
1418 which then goes through various stages that can end up in a context update, or
1419 in failures of various kind. The process is described in figure
1420 \ref{fig:kant-process}. The workings of each phase will be illustrated in the
1425 \tikzstyle{block} = [rectangle, draw, text width=5em, text centered, rounded
1426 corners, minimum height=2.5em, node distance=0.7cm]
1428 \tikzstyle{decision} = [diamond, draw, text width=4.5em, text badly
1429 centered, inner sep=0pt, node distance=0.7cm]
1431 \tikzstyle{line} = [draw, -latex']
1433 \tikzstyle{cloud} = [draw, ellipse, minimum height=2em, text width=5em, text
1434 centered, node distance=1.5cm]
1437 \begin{tikzpicture}[auto]
1438 \node [cloud] (user) {User};
1439 \node [block, below left=1cm and 0.1cm of user] (parse) {Parse};
1440 \node [block, below=of parse] (desugar) {Desugar};
1441 \node [block, below=of desugar] (reference) {Reference};
1442 \node [block, below=of reference] (elaborate) {Elaborate};
1443 \node [block, below=of elaborate] (tycheck) {Typecheck};
1444 \node [decision, right=of elaborate] (error) {Error?};
1445 \node [block, right=of parse] (distill) {Distill};
1446 \node [block, right=of desugar] (update) {Update context};
1448 \path [line] (user) -- (parse);
1449 \path [line] (parse) -- (desugar);
1450 \path [line] (desugar) -- (reference);
1451 \path [line] (reference) -- (elaborate);
1452 \path [line] (elaborate) edge[bend right] (tycheck);
1453 \path [line] (tycheck) edge[bend right] (elaborate);
1454 \path [line] (elaborate) -- (error);
1455 \path [line] (error) edge[out=0,in=0] node [near start] {yes} (distill);
1456 \path [line] (error) -- node [near start] {no} (update);
1457 \path [line] (update) -- (distill);
1458 \path [line] (distill) -- (user);
1463 \caption{High level overview of the life of a \mykant prompt cycle.}
1464 \label{fig:kant-process}
1467 \subsection{Bidirectional type checking}
1469 We start by describing bidirectional type checking since it calls for fairly
1470 different typing rules that what we have seen up to now. The idea is to have
1471 two kind of terms: terms for which a type can always be inferred, and terms
1472 that need to be checked against a type. A nice observation is that this
1473 duality runs through the semantics of the terms: data destructors (function
1474 application, record projections, primitive recursors) \emph{infer} types,
1475 while data constructors (abstractions, record/data types data constructors)
1478 To introduce the concept and notation, we will revisit the STLC in a
1479 bidirectional style.
1483 \section{Notation and syntax}
1485 Syntax, derivation rules, and reduction rules, are enclosed in frames describing
1486 the type of relation being established and the syntactic elements appearing,
1489 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
1490 \centering{Typing derivations here.}
1493 In the languages presented and Agda code samples I also highlight the syntax,
1494 following a uniform color and font convention:
1497 \begin{tabular}{c | l}
1498 $\mytyc{Sans}$ & Type constructors. \\
1499 $\mydc{sans}$ & Data constructors. \\
1500 % $\myfld{sans}$ & Field accessors (e.g. \myfld{fst} and \myfld{snd} for products). \\
1501 $\mysyn{roman}$ & Keywords of the language. \\
1502 $\myfun{roman}$ & Defined values and destructors. \\
1503 $\myb{math}$ & Bound variables.
1507 Moreover, I will from time to time give examples in the Haskell programming
1508 language as defined in \citep{Haskell2010}, which I will typeset in
1509 \texttt{teletype} font. I assume that the reader is already familiar with
1510 Haskell, plenty of good introductions are available \citep{LYAH,ProgInHask}.
1512 When presenting grammars, I will use a word in $\mysynel{math}$ font
1513 (e.g. $\mytmsyn$ or $\mytysyn$) to indicate indicate nonterminals. Additionally,
1514 I will use quite flexibly a $\mysynel{math}$ font to indicate a syntactic
1515 element. More specifically, terms are usually indicated by lowercase letters
1516 (often $\mytmt$, $\mytmm$, or $\mytmn$); and types by an uppercase letter (often
1517 $\mytya$, $\mytyb$, or $\mytycc$).
1519 When presenting type derivations, I will often abbreviate and present multiple
1520 conclusions, each on a separate line:
1523 \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
1524 \UnaryInfC{$\myjud{\myapp{\myfst}{\mytmt}}{\mytya}$}
1526 \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mytyb}$}
1529 \section{Agda rendition of core ITT}
1530 \label{app:agda-code}
1538 absurd : ∀ {a} {A : Set a} → ⊥ → A
1541 record ⊤ : Set where
1544 record _×_ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
1550 data Bool : Set where
1553 if_then_else_ : ∀ {a} {P : Bool → Set a} (x : Bool) → P true → P false → P x
1554 if true then x else _ = x
1555 if false then _ else x = x
1557 data W {s p} (S : Set s) (P : S → Set p) : Set (s ⊔ p) where
1558 _◁_ : (s : S) → (P s → W S P) → W S P
1560 rec : ∀ {a b} {S : Set a} {P : S → Set b}
1561 (C : W S P → Set) → -- some conclusion we hope holds
1562 ((s : S) → -- given a shape...
1563 (f : P s → W S P) → -- ...and a bunch of kids...
1564 ((p : P s) → C (f p)) → -- ...and C for each kid in the bunch...
1565 C (s ◁ f)) → -- ...does C hold for the node?
1566 (x : W S P) → -- If so, ...
1567 C x -- ...C always holds.
1568 rec C c (s ◁ f) = c s f (λ p → rec C c (f p))
1570 data _≡_ {a} {A : Set a} : A → A → Set a where
1573 J : ∀ {a b} {A : Set a}
1574 (P : (x y : A) → x ≡ y → Set b) →
1575 ∀ {x y} → P x x (refl x) → (x≡y : x ≡ y) → P x y x≡y
1578 subst : ∀ {a b} {A : Set a}
1580 ∀ {x y} → (x≡y : x ≡ y) → P x → P y
1581 subst P q p = J (λ _ y _ → P y) p q
1585 \bibliographystyle{authordate1}
1586 \bibliography{thesis}