1 \documentclass[report]{article}
4 % \usepackage{fullpage}
16 \usepackage[fleqn]{amsmath}
19 \usepackage{bussproofs}
24 %% -----------------------------------------------------------------------------
26 \usepackage[english]{babel}
27 \usepackage[conor]{agda}
28 \renewcommand{\AgdaKeywordFontStyle}[1]{\ensuremath{\mathrm{\underline{#1}}}}
29 \renewcommand{\AgdaFunction}[1]{\textbf{\textcolor{AgdaFunction}{#1}}}
30 \renewcommand{\AgdaField}{\AgdaFunction}
31 % \definecolor{AgdaBound} {HTML}{000000}
32 \definecolor{AgdaHole} {HTML} {FFFF33}
34 \DeclareUnicodeCharacter{9665}{\ensuremath{\lhd}}
35 \DeclareUnicodeCharacter{964}{\ensuremath{\tau}}
36 \DeclareUnicodeCharacter{963}{\ensuremath{\sigma}}
37 \DeclareUnicodeCharacter{915}{\ensuremath{\Gamma}}
38 \DeclareUnicodeCharacter{8799}{\ensuremath{\stackrel{?}{=}}}
39 \DeclareUnicodeCharacter{9655}{\ensuremath{\rhd}}
42 %% -----------------------------------------------------------------------------
45 \newcommand{\mysyn}{\AgdaKeyword}
46 \newcommand{\mytyc}{\AgdaDatatype}
47 \newcommand{\mydc}{\AgdaInductiveConstructor}
48 \newcommand{\myfld}{\AgdaField}
49 \newcommand{\myfun}{\AgdaFunction}
50 % TODO make this use AgdaBound
51 \newcommand{\myb}[1]{\AgdaBound{#1}}
52 \newcommand{\myfield}{\AgdaField}
53 \newcommand{\myind}{\AgdaIndent}
54 \newcommand{\mykant}{\textsc{Kant}}
55 \newcommand{\mysynel}[1]{#1}
56 \newcommand{\myse}{\mysynel}
57 \newcommand{\mytmsyn}{\mysynel{term}}
58 \newcommand{\mysp}{\ }
59 % TODO \mathbin or \mathre here?
60 \newcommand{\myabs}[2]{\mydc{$\lambda$} #1 \mathrel{\mydc{$\mapsto$}} #2}
61 \newcommand{\myappsp}{\hspace{0.07cm}}
62 \newcommand{\myapp}[2]{#1 \myappsp #2}
63 \newcommand{\mysynsep}{\ \ |\ \ }
66 \newcommand{\mydesc}[3]{
69 \hfill \textbf{#1} $#2$
77 % TODO is \mathbin the correct thing for arrow and times?
79 \newcommand{\mytmt}{\mysynel{t}}
80 \newcommand{\mytmm}{\mysynel{m}}
81 \newcommand{\mytmn}{\mysynel{n}}
82 \newcommand{\myred}{\leadsto}
83 \newcommand{\mysub}[3]{#1[#2 / #3]}
84 \newcommand{\mytysyn}{\mysynel{type}}
85 \newcommand{\mybasetys}{K}
86 % TODO change this name
87 \newcommand{\mybasety}[1]{B_{#1}}
88 \newcommand{\mytya}{\myse{A}}
89 \newcommand{\mytyb}{\myse{B}}
90 \newcommand{\mytycc}{\myse{C}}
91 \newcommand{\myarr}{\mathrel{\textcolor{AgdaDatatype}{\to}}}
92 \newcommand{\myprod}{\mathrel{\textcolor{AgdaDatatype}{\times}}}
93 \newcommand{\myctx}{\Gamma}
94 \newcommand{\myvalid}[1]{#1 \vdash \underline{\mathrm{valid}}}
95 \newcommand{\myjudd}[3]{#1 \vdash #2 : #3}
96 \newcommand{\myjud}[2]{\myjudd{\myctx}{#1}{#2}}
97 % TODO \mathbin or \mathrel here?
98 \newcommand{\myabss}[3]{\mydc{$\lambda$} #1 {:} #2 \mathrel{\mydc{$\mapsto$}} #3}
99 \newcommand{\mytt}{\mydc{$\langle\rangle$}}
100 \newcommand{\myunit}{\mytyc{$\top$}}
101 \newcommand{\mypair}[2]{\mathopen{\mydc{$\langle$}}#1\mathpunct{\mydc{,}} #2\mathclose{\mydc{$\rangle$}}}
102 \newcommand{\myfst}{\myfld{fst}}
103 \newcommand{\mysnd}{\myfld{snd}}
104 \newcommand{\myconst}{\myse{c}}
105 \newcommand{\myemptyctx}{\cdot}
106 \newcommand{\myhole}{\AgdaHole}
107 \newcommand{\myfix}[3]{\mysyn{fix} \myappsp #1 {:} #2 \mapsto #3}
108 \newcommand{\mysum}{\mathbin{\textcolor{AgdaDatatype}{+}}}
109 \newcommand{\myleft}[1]{\mydc{left}_{#1}}
110 \newcommand{\myright}[1]{\mydc{right}_{#1}}
111 \newcommand{\myempty}{\mytyc{$\bot$}}
112 \newcommand{\mycase}[2]{\mathopen{\myfun{[}}#1\mathpunct{\myfun{,}} #2 \mathclose{\myfun{]}}}
113 \newcommand{\myabsurd}[1]{\myfun{absurd}_{#1}}
114 \newcommand{\myarg}{\_}
115 \newcommand{\myderivsp}{\vspace{0.3cm}}
116 \newcommand{\mytyp}{\mytyc{Type}}
117 \newcommand{\myneg}{\myfun{$\neg$}}
118 \newcommand{\myar}{\,}
119 \newcommand{\mybool}{\mytyc{Bool}}
120 \newcommand{\mytrue}{\mydc{true}}
121 \newcommand{\myfalse}{\mydc{false}}
122 \newcommand{\myitee}[5]{\myfun{if}\,#1 / {#2.#3}\,\myfun{then}\,#4\,\myfun{else}\,#5}
123 \newcommand{\mynat}{\mytyc{$\mathbb{N}$}}
124 \newcommand{\myrat}{\mytyc{$\mathbb{R}$}}
125 \newcommand{\myite}[3]{\myfun{if}\,#1\,\myfun{then}\,#2\,\myfun{else}\,#3}
126 \newcommand{\myfora}[3]{(#1 {:} #2) \myarr #3}
127 \newcommand{\myexi}[3]{(#1 {:} #2) \myprod #3}
128 \newcommand{\mypairr}[4]{\mathopen{\mydc{$\langle$}}#1\mathpunct{\mydc{,}} #4\mathclose{\mydc{$\rangle$}}_{#2{.}#3}}
129 \newcommand{\mylist}{\mytyc{List}}
130 \newcommand{\mynil}[1]{\mydc{[]}_{#1}}
131 \newcommand{\mycons}{\mathbin{\mydc{∷}}}
132 \newcommand{\myfoldr}{\myfun{foldr}}
133 \newcommand{\myw}[3]{\myapp{\myapp{\mytyc{W}}{(#1 {:} #2)}}{#3}}
134 \newcommand{\mynode}[2]{\mathbin{\mydc{$\lhd$}_{#1.#2}}}
135 \newcommand{\myrec}[4]{\myfun{rec}\,#1 / {#2.#3}\,\myfun{with}\,#4}
136 \newcommand{\mylub}{\sqcup}
137 \newcommand{\mydefeq}{\cong}
139 %% -----------------------------------------------------------------------------
141 \title{\mykant: Implementing Observational Equality}
142 \author{Francesco Mazzoli \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{<fm2209@ic.ac.uk>}}}
156 The marriage between programming and logic has been a very fertile one. In
157 particular, since the simply typed lambda calculus (STLC), a number of type
158 systems have been devised with increasing expressive power.
160 Section \ref{sec:types} will give a very brief overview of STLC, and then
161 illustrate how it can be interpreted as a natural deduction system. Section
162 \ref{sec:itt} will introduce Inutitionistic Type Theory (ITT), which expands
163 on this concept, employing a more expressive logic. The exposition is quite
164 dense since there is a lot of material to cover; for a more complete treatment
165 of the material the reader can refer to \citep{Thompson1991, Pierce2002}.
166 Section \ref{sec:equality} will explain why equality has always been a tricky
167 business in these theories, and talk about the various attempts that have been
168 made to make the situation better. One interesting development has recently
169 emerged: Observational Type theory.
171 Section \ref{sec:practical} will describe common extensions found in the
172 systems currently in use. Finally, section \ref{sec:kant} will describe a
173 system developed by the author that implements a core calculus based on the
174 principles described.
183 \section{Simple and not-so-simple types}
186 \subsection{The untyped $\lambda$-calculus}
188 Along with Turing's machines, the earliest attempts to formalise computation
189 lead to the $\lambda$-calculus \citep{Church1936}. This early programming
190 language encodes computation with a minimal syntax and no `data' in the
191 traditional sense, but just functions. Here we give a brief overview of the
192 language, which will give the chance to introduce concepts central to the
193 analysis of all the following calculi. The exposition follows the one found in
194 chapter 5 of \cite{Queinnec2003}.
196 The syntax of $\lambda$-terms consists of three things: variables, abstractions,
201 \begin{array}{r@{\ }c@{\ }l}
202 \mytmsyn & ::= & \myb{x} \mysynsep \myabs{\myb{x}}{\mytmsyn} \mysynsep (\myapp{\mytmsyn}{\mytmsyn}) \\
203 x & \in & \text{Some enumerable set of symbols}
208 Parenthesis will be omitted in the usual way:
209 $\myapp{\myapp{\mytmt}{\mytmm}}{\mytmn} =
210 \myapp{(\myapp{\mytmt}{\mytmm})}{\mytmn}$.
212 Abstractions roughly corresponds to functions, and their semantics is more
213 formally explained by the $\beta$-reduction rule:
215 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
218 \myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{\myb{x}}{\mytmn}\text{, where} \\
220 \begin{array}{l@{\ }c@{\ }l}
221 \mysub{\myb{x}}{\myb{x}}{\mytmn} & = & \mytmn \\
222 \mysub{\myb{y}}{\myb{x}}{\mytmn} & = & y\text{, with } \myb{x} \neq y \\
223 \mysub{(\myapp{\mytmt}{\mytmm})}{\myb{x}}{\mytmn} & = & (\myapp{\mysub{\mytmt}{\myb{x}}{\mytmn}}{\mysub{\mytmm}{\myb{x}}{\mytmn}}) \\
224 \mysub{(\myabs{\myb{x}}{\mytmm})}{\myb{x}}{\mytmn} & = & \myabs{\myb{x}}{\mytmm} \\
225 \mysub{(\myabs{\myb{y}}{\mytmm})}{\myb{x}}{\mytmn} & = & \myabs{\myb{z}}{\mysub{\mysub{\mytmm}{\myb{y}}{\myb{z}}}{\myb{x}}{\mytmn}}, \\
226 \multicolumn{3}{l}{\myind{1} \text{with $\myb{x} \neq \myb{y}$ and $\myb{z}$ not free in $\myapp{\mytmm}{\mytmn}$}}
232 The care required during substituting variables for terms is required to avoid
233 name capturing. We will use substitution in the future for other name-binding
234 constructs assuming similar precautions.
236 These few elements are of remarkable expressiveness, and in fact Turing
237 complete. As a corollary, we must be able to devise a term that reduces forever
238 (`loops' in imperative terms):
240 (\myapp{\omega}{\omega}) \myred (\myapp{\omega}{\omega}) \myred \dots\text{, with $\omega = \myabs{x}{\myapp{x}{x}}$}
243 A \emph{redex} is a term that can be reduced. In the untyped $\lambda$-calculus
244 this will be the case for an application in which the first term is an
245 abstraction, but in general we call aterm reducible if it appears to the left of
246 a reduction rule. When a term contains no redexes it's said to be in
247 \emph{normal form}. Given the observation above, not all terms reduce to a
248 normal forms: we call the ones that do \emph{normalising}, and the ones that
249 don't \emph{non-normalising}.
251 The reduction rule presented is not syntax directed, but \emph{evaluation
252 strategies} can be employed to reduce term systematically. Common evaluation
253 strategies include \emph{call by value} (or \emph{strict}), where arguments of
254 abstractions are reduced before being applied to the abstraction; and conversely
255 \emph{call by name} (or \emph{lazy}), where we reduce only when we need to do so
256 to proceed---in other words when we have an application where the function is
257 still not a $\lambda$. In both these reduction strategies we never reduce under
258 an abstraction: for this reason a weaker form of normalisation is used, where
259 both abstractions and normal forms are said to be in \emph{weak head normal
262 \subsection{The simply typed $\lambda$-calculus}
264 A convenient way to `discipline' and reason about $\lambda$-terms is to assign
265 \emph{types} to them, and then check that the terms that we are forming make
266 sense given our typing rules \citep{Curry1934}. The first most basic instance
267 of this idea takes the name of \emph{simply typed $\lambda$ calculus}, whose
268 rules are shown in figure \ref{fig:stlc}.
270 Our types contain a set of \emph{type variables} $\Phi$, which might correspond
271 to some `primitive' types; and $\myarr$, the type former for `arrow' types, the
272 types of functions. The language is explicitly typed: when we bring a variable
273 into scope with an abstraction, we explicitly declare its type. $\mytya$,
274 $\mytyb$, $\mytycc$, will be used to refer to a generic type. Reduction is
275 unchanged from the untyped $\lambda$-calculus.
280 \begin{array}{r@{\ }c@{\ }l}
281 \mytmsyn & ::= & \myb{x} \mysynsep \myabss{\myb{x}}{\mytysyn}{\mytmsyn} \mysynsep
282 (\myapp{\mytmsyn}{\mytmsyn}) \\
283 \mytysyn & ::= & \myse{\phi} \mysynsep \mytysyn \myarr \mytysyn \mysynsep \\
284 \myb{x} & \in & \text{Some enumerable set of symbols} \\
285 \myse{\phi} & \in & \Phi
290 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
293 \AxiomC{$\myctx(x) = A$}
294 \UnaryInfC{$\myjud{\myb{x}}{A}$}
297 \AxiomC{$\myjudd{\myctx;\myb{x} : A}{\mytmt}{\mytyb}$}
298 \UnaryInfC{$\myjud{\myabss{x}{A}{\mytmt}}{\mytyb}$}
301 \AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$}
302 \AxiomC{$\myjud{\mytmn}{\mytya}$}
303 \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mytyb}$}
308 \caption{Syntax and typing rules for the STLC. Reduction is unchanged from
309 the untyped $\lambda$-calculus.}
313 In the typing rules, a context $\myctx$ is used to store the types of bound
314 variables: $\myctx; \myb{x} : \mytya$ adds a variable to the context and
315 $\myctx(x)$ returns the type of the rightmost occurrence of $x$.
317 This typing system takes the name of `simply typed lambda calculus' (STLC), and
318 enjoys a number of properties. Two of them are expected in most type systems
321 \item[Progress] A well-typed term is not stuck---it is either a variable, or its
322 constructor does not appear on the left of the $\myred$ relation (currently
323 only $\lambda$), or it can take a step according to the evaluation rules.
324 \item[Preservation] If a well-typed term takes a step of evaluation, then the
325 resulting term is also well-typed, and preserves the previous type. Also
326 known as \emph{subject reduction}.
329 However, STLC buys us much more: every well-typed term is normalising
330 \citep{Tait1967}. It is easy to see that we can't fill the blanks if we want to
331 give types to the non-normalising term shown before:
333 \myapp{(\myabss{\myb{x}}{\myhole{?}}{\myapp{\myb{x}}{\myb{x}}})}{(\myabss{\myb{x}}{\myhole{?}}{\myapp{\myb{x}}{\myb{x}}})}
336 This makes the STLC Turing incomplete. We can recover the ability to loop by
337 adding a combinator that recurses:
340 \begin{minipage}{0.5\textwidth}
342 $ \mytmsyn ::= \dotsb \mysynsep \myfix{\myb{x}}{\mytysyn}{\mytmsyn} $
346 \begin{minipage}{0.5\textwidth}
347 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}} {
349 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytmt}{\mytya}$}
350 \UnaryInfC{$\myjud{\myfix{\myb{x}}{\mytya}{\mytmt}}{\mytya}$}
356 \mydesc{reduction:}{\myjud{\mytmsyn}{\mytmsyn}}{
358 $ \myfix{\myb{x}}{\mytya}{\mytmt} \myred \mysub{\mytmt}{\myb{x}}{(\myfix{\myb{x}}{\mytya}{\mytmt})}$
362 This will deprive us of normalisation, which is a particularly bad thing if we
363 want to use the STLC as described in the next section.
365 \subsection{The Curry-Howard correspondence}
367 It turns out that the STLC can be seen a natural deduction system for
368 intuitionistic propositional logic. Terms are proofs, and their types are the
369 propositions they prove. This remarkable fact is known as the Curry-Howard
370 correspondence, or isomorphism.
372 The arrow ($\myarr$) type corresponds to implication. If we wish to prove that
373 that $(\mytya \myarr \mytyb) \myarr (\mytyb \myarr \mytycc) \myarr (\mytya
374 \myarr \mytycc)$, all we need to do is to devise a $\lambda$-term that has the
377 \myabss{\myb{f}}{(\mytya \myarr \mytyb)}{\myabss{\myb{g}}{(\mytyb \myarr \mytycc)}{\myabss{\myb{x}}{\mytya}{\myapp{\myb{g}}{(\myapp{\myb{f}}{\myb{x}})}}}}
379 That is, function composition. Going beyond arrow types, we can extend our bare
380 lambda calculus with useful types to represent other logical constructs, as
381 shown in figure \ref{fig:natded}.
386 \begin{array}{r@{\ }c@{\ }l}
387 \mytmsyn & ::= & \dots \\
388 & | & \mytt \mysynsep \myapp{\myabsurd{\mytysyn}}{\mytmsyn} \\
389 & | & \myapp{\myleft{\mytysyn}}{\mytmsyn} \mysynsep
390 \myapp{\myright{\mytysyn}}{\mytmsyn} \mysynsep
391 \myapp{\mycase{\mytmsyn}{\mytmsyn}}{\mytmsyn} \\
392 & | & \mypair{\mytmsyn}{\mytmsyn} \mysynsep
393 \myapp{\myfst}{\mytmsyn} \mysynsep \myapp{\mysnd}{\mytmsyn} \\
394 \mytysyn & ::= & \dots \mysynsep \myunit \mysynsep \myempty \mysynsep \mytmsyn \mysum \mytmsyn \mysynsep \mytysyn \myprod \mytysyn
399 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
403 \begin{array}{l@{ }l@{\ }c@{\ }l}
404 \myapp{\mycase{\mytmm}{\mytmn}}{(\myapp{\myleft{\mytya} &}{\mytmt})} & \myred &
405 \myapp{\mytmm}{\mytmt} \\
406 \myapp{\mycase{\mytmm}{\mytmn}}{(\myapp{\myright{\mytya} &}{\mytmt})} & \myred &
407 \myapp{\mytmn}{\mytmt}
412 \begin{array}{l@{ }l@{\ }c@{\ }l}
413 \myapp{\myfst &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmm \\
414 \myapp{\mysnd &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmn
421 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
424 \AxiomC{\phantom{$\myjud{\mytmt}{\myempty}$}}
425 \UnaryInfC{$\myjud{\mytt}{\myunit}$}
428 \AxiomC{$\myjud{\mytmt}{\myempty}$}
429 \UnaryInfC{$\myjud{\myapp{\myabsurd{\mytya}}{\mytmt}}{\mytya}$}
436 \AxiomC{$\myjud{\mytmt}{\mytya}$}
437 \UnaryInfC{$\myjud{\myapp{\myleft{\mytyb}}{\mytmt}}{\mytya \mysum \mytyb}$}
440 \AxiomC{$\myjud{\mytmt}{\mytyb}$}
441 \UnaryInfC{$\myjud{\myapp{\myright{\mytya}}{\mytmt}}{\mytya \mysum \mytyb}$}
449 \AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$}
450 \AxiomC{$\myjud{\mytmn}{\mytya \myarr \mytycc}$}
451 \AxiomC{$\myjud{\mytmt}{\mytya \mysum \mytyb}$}
452 \TrinaryInfC{$\myjud{\myapp{\mycase{\mytmm}{\mytmn}}{\mytmt}}{\mytycc}$}
459 \AxiomC{$\myjud{\mytmm}{\mytya}$}
460 \AxiomC{$\myjud{\mytmn}{\mytyb}$}
461 \BinaryInfC{$\myjud{\mypair{\mytmm}{\mytmn}}{\mytya \myprod \mytyb}$}
464 \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
465 \UnaryInfC{$\myjud{\myapp{\myfst}{\mytmt}}{\mytya}$}
468 \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
469 \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mytyb}$}
474 \caption{Rules for the extendend STLC. Only the new features are shown, all the
475 rules and syntax for the STLC apply here too.}
479 Tagged unions (or sums, or coproducts---$\mysum$ here, \texttt{Either} in
480 Haskell) correspond to disjunctions, and dually tuples (or pairs, or
481 products---$\myprod$ here, tuples in Haskell) correspond to conjunctions. This
482 is apparent looking at the ways to construct and destruct the values inhabiting
483 those types: for $\mysum$ $\myleft{ }$ and $\myright{ }$ correspond to $\vee$
484 introduction, and $\mycase{\_}{\_}$ to $\vee$ elimination; for $\myprod$
485 $\mypair{\_}{\_}$ corresponds to $\wedge$ introduction, $\myfst$ and $\mysnd$ to
486 $\wedge$ elimination.
488 The trivial type $\myunit$ corresponds to the logical $\top$, and dually
489 $\myempty$ corresponds to the logical $\bot$. $\myunit$ has one introduction
490 rule ($\mytt$), and thus one inhabitant; and no eliminators. $\myempty$ has no
491 introduction rules, and thus no inhabitants; and one eliminator ($\myabsurd{
492 }$), corresponding to the logical \emph{ex falso quodlibet}. Note that in the
493 constructors for the sums and the destructor for $\myempty$ we need to include
494 some type information to keep type checking decidable.
496 With these rules, our STLC now looks remarkably similar in power and use to the
497 natural deduction we already know. $\myneg \mytya$ can be expressed as $\mytya
498 \myarr \myempty$. However, there is an important omission: there is no term of
499 the type $\mytya \mysum \myneg \mytya$ (excluded middle), or equivalently
500 $\myneg \myneg \mytya \myarr \mytya$ (double negation), or indeed any term with
501 a type equivalent to those.
503 This has a considerable effect on our logic and it's no coincidence, since there
504 is no obvious computational behaviour for laws like the excluded middle.
505 Theories of this kind are called \emph{intuitionistic}, or \emph{constructive},
506 and all the systems analysed will have this characteristic since they build on
507 the foundation of the STLC\footnote{There is research to give computational
508 behaviour to classical logic, but I will not touch those subjects.}.
510 As in logic, if we want to keep our system consistent, we must make sure that no
511 closed terms (in other words terms not under a $\lambda$) inhabit $\myempty$.
512 The variant of STLC presented here is indeed
513 consistent, a result that follows from the fact that it is
514 normalising. % TODO explain
515 Going back to our $\mysyn{fix}$ combinator, it is easy to see how it ruins our
516 desire for consistency. The following term works for every type $\mytya$,
519 (\myfix{\myb{x}}{\mytya}{\myb{x}}) : \mytya
522 \subsection{Inductive data}
524 To make the STLC more useful as a programming language or reasoning tool it is
525 common to include (or let the user define) inductive data types. These comprise
526 of a type former, various constructors, and an eliminator (or destructor) that
527 serves as primitive recursor.
529 For example, we might add a $\mylist$ type constructor, along with an `empty
530 list' ($\mynil{ }$) and `cons cell' ($\mycons$) constructor. The eliminator for
531 lists will be the usual folding operation ($\myfoldr$). See figure
537 \begin{array}{r@{\ }c@{\ }l}
538 \mytmsyn & ::= & \dots \mysynsep \mynil{\mytysyn} \mysynsep \mytmsyn \mycons \mytmsyn
540 \myapp{\myapp{\myapp{\myfoldr}{\mytmsyn}}{\mytmsyn}}{\mytmsyn} \\
541 \mytysyn & ::= & \dots \mysynsep \myapp{\mylist}{\mytysyn}
545 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
548 \begin{array}{l@{\ }c@{\ }l}
549 \myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{\mynil{\mytya}} & \myred & \mytmt \\
551 \myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{(\mytmm \mycons \mytmn)} & \myred &
552 \myapp{\myapp{\myse{f}}{\mytmm}}{(\myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{\mytmn})}
557 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
560 \AxiomC{\phantom{$\myjud{\mytmm}{\mytya}$}}
561 \UnaryInfC{$\myjud{\mynil{\mytya}}{\myapp{\mylist}{\mytya}}$}
564 \AxiomC{$\myjud{\mytmm}{\mytya}$}
565 \AxiomC{$\myjud{\mytmn}{\myapp{\mylist}{\mytya}}$}
566 \BinaryInfC{$\myjud{\mytmm \mycons \mytmn}{\myapp{\mylist}{\mytya}}$}
572 \AxiomC{$\myjud{\mysynel{f}}{\mytya \myarr \mytyb \myarr \mytyb}$}
573 \AxiomC{$\myjud{\mytmm}{\mytyb}$}
574 \AxiomC{$\myjud{\mytmn}{\myapp{\mylist}{\mytya}}$}
575 \TrinaryInfC{$\myjud{\myapp{\myapp{\myapp{\myfoldr}{\mysynel{f}}}{\mytmm}}{\mytmn}}{\mytyb}$}
579 \caption{Rules for lists in the STLC.}
583 In section \ref{sec:well-order} we will see how to give a general account of
584 inductive data. %TODO does this make sense to have here?
586 \section{Intuitionistic Type Theory}
589 \subsection{Extending the STLC}
591 The STLC can be made more expressive in various ways. \cite{Barendregt1991}
592 succinctly expressed geometrically how we can add expressivity:
596 & \lambda\omega \ar@{-}[rr]\ar@{-}'[d][dd]
597 & & \lambda C \ar@{-}[dd]
599 \lambda2 \ar@{-}[ur]\ar@{-}[rr]\ar@{-}[dd]
600 & & \lambda P2 \ar@{-}[ur]\ar@{-}[dd]
602 & \lambda\underline\omega \ar@{-}'[r][rr]
603 & & \lambda P\underline\omega
605 \lambda{\to} \ar@{-}[rr]\ar@{-}[ur]
606 & & \lambda P \ar@{-}[ur]
609 Here $\lambda{\to}$, in the bottom left, is the STLC. From there can move along
612 \item[Terms depending on types (towards $\lambda{2}$)] We can quantify over
613 types in our type signatures. For example, we can define a polymorphic
616 (\myabss{\myb{A}}{\mytyp}{\myabss{\myb{x}}{\myb{A}}{\myb{x}}}) : (\myb{A} : \mytyp) \myarr \myb{A} \myarr \myb{A}
618 The first and most famous instance of this idea has been System F. This form
619 of polymorphism and has been wildly successful, also thanks to a well known
620 inference algorithm for a restricted version of System F known as
621 Hindley-Milner. Languages like Haskell and SML are based on this discipline.
622 \item[Types depending on types (towards $\lambda{\underline{\omega}}$)] We have
623 type operators. For example we could define a function that given types $R$
624 and $\mytya$ forms the type that represents a value of type $\mytya$ in
625 continuation passing style: \[\displaystyle(\myabss{\myb{A} \myar \myb{R}}{\mytyp}{(\myb{A}
626 \myarr \myb{R}) \myarr \myb{R}}) : \mytyp \myarr \mytyp \myarr \mytyp\]
627 \item[Types depending on terms (towards $\lambda{P}$)] Also known as `dependent
628 types', give great expressive power. For example, we can have values of whose
629 type depend on a boolean:
630 \[\displaystyle(\myabss{\myb{x}}{\mybool}{\myite{\myb{x}}{\mynat}{\myrat}}) : \mybool
634 All the systems preserve the properties that make the STLC well behaved. The
635 system we are going to focus on, Intuitionistic Type Theory, has all of the
636 above additions, and thus would sit where $\lambda{C}$ sits in the
637 `$\lambda$-cube'. It will serve as the logical `core' of all the other
638 extensions that we will present and ultimately our implementation of a similar
641 \subsection{A Bit of History}
643 Logic frameworks and programming languages based on type theory have a long
644 history. Per Martin-L\"{o}f described the first version of his theory in 1971,
645 but then revised it since the original version was inconsistent due to its
646 impredicativity\footnote{In the early version there was only one universe
647 $\mytyp$ and $\mytyp : \mytyp$, see section \ref{sec:term-types} for an
648 explanation on why this causes problems.}. For this reason he gave a revised
649 and consistent definition later \citep{Martin-Lof1984}.
651 A related development is the polymorphic $\lambda$-calculus, and specifically
652 the previously mentioned System F, which was developed independently by Girard
653 and Reynolds. An overview can be found in \citep{Reynolds1994}. The surprising
654 fact is that while System F is impredicative it is still consistent and strongly
655 normalising. \cite{Coquand1986} further extended this line of work with the
656 Calculus of Constructions (CoC).
658 \subsection{A simple type theory}
661 The calculus I present follows the exposition in \citep{Thompson1991}, and is
662 quite close to the original formulation of predicative ITT as found in
663 \citep{Martin-Lof1984}. The system's syntax and reduction rules are presented
664 in their entirety in figure \ref{fig:core-tt-syn}. The typing rules are
665 presented piece by piece. An Agda rendition of the presented theory is
666 reproduced in appendix \ref{app:agda-code}.
671 \begin{array}{r@{\ }c@{\ }l}
672 \mytmsyn & ::= & \myb{x} \mysynsep
674 \myunit \mysynsep \mytt \mysynsep
675 \myempty \mysynsep \myapp{\myabsurd{\mytmsyn}}{\mytmsyn} \\
676 & | & \mybool \mysynsep \mytrue \mysynsep \myfalse \mysynsep
677 \myitee{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
678 & | & \myfora{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
679 \myabss{\myb{x}}{\mytmsyn}{\mytmsyn} \\
680 & | & \myexi{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
681 \mypairr{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn} \\
682 & | & \myapp{\myfst}{\mytmsyn} \mysynsep \myapp{\mysnd}{\mytmsyn} \\
683 & | & \myw{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
684 \mytmsyn \mynode{\myb{x}}{\mytmsyn} \mytmsyn \\
685 & | & \myrec{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn} \\
691 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
695 \begin{array}{l@{ }l@{\ }c@{\ }l}
696 \myitee{\mytrue &}{\myb{x}}{\myse{P}}{\mytmm}{\mytmn} & \myred & \mytmm \\
697 \myitee{\myfalse &}{\myb{x}}{\myse{P}}{\mytmm}{\mytmn} & \myred & \mytmn \\
702 \myapp{(\myabss{\myb{x}}{\mytya}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{\myb{x}}{\mytmn}
707 \begin{array}{l@{ }l@{\ }c@{\ }l}
708 \myapp{\myfst &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmm \\
709 \myapp{\mysnd &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmn
715 \myrec{(\myse{s} \mynode{\myb{x}}{\myse{T}} \myse{f})}{\myb{y}}{\myse{P}}{\myse{p}} \myred
716 \myapp{\myapp{\myapp{\myse{p}}{\myse{s}}}{\myse{f}}}{(\myabss{\myb{t}}{\mysub{\myse{T}}{\myb{x}}{\myse{s}}}{
717 \myrec{\myapp{\myse{f}}{\myb{t}}}{\myb{y}}{\myse{P}}{\mytmt}
722 \caption{Syntax and reduction rules for our type theory.}
723 \label{fig:core-tt-syn}
726 \subsubsection{Types are terms, some terms are types}
727 \label{sec:term-types}
729 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
732 \AxiomC{$\myjud{\mytmt}{\mytya}$}
733 \AxiomC{$\mytya \mydefeq \mytyb$}
734 \BinaryInfC{$\myjud{\mytmt}{\mytyb}$}
737 \AxiomC{\phantom{$\myjud{\mytmt}{\mytya}$}}
738 \UnaryInfC{$\myjud{\mytyp_l}{\mytyp_{l + 1}}$}
744 The first thing to notice is that a barrier between values and types that we had
745 in the STLC is gone: values can appear in types, and the two are treated
746 uniformly in the syntax.
748 While the usefulness of doing this will become clear soon, a consequence is that
749 since types can be the result of computation, deciding type equality is not
750 immediate as in the STLC. For this reason we define \emph{definitional
751 equality}, $\mydefeq$, as the congruence relation extending $\myred$. Types
752 that are definitionally equal can be used interchangeably. Here the
753 `conversion' rule is not syntax directed, however we will see how it is possible
754 to employ $\myred$ to decide term equality in a systematic way. % TODO add section
755 Another thing to notice is that considering the need to reduce terms to decide
756 equality, it is essential for a dependently type system to be terminating and
757 confluent for type checking to be decidable.
759 Moreover, we specify a \emph{type hierarchy} to talk about `large' types:
760 $\mytyp_0$ will be the type of types inhabited by data: $\mybool$, $\mynat$,
761 $\mylist$, etc. $\mytyp_1$ will be the type of $\mytyp_0$, and so on---for
762 example we have $\mytrue : \mybool : \mytyp_0 : \mytyp_1 : \dots$. Each type
763 `level' is often called a universe in the literature. While it is possible, to
764 simplify things by having only one universe $\mytyp$ with $\mytyp : \mytyp$,
765 this plan is inconsistent for much the same reason that impredicative na\"{\i}ve
766 set theory is \citep{Hurkens1995}. Moreover, various techniques can be employed
767 to lift the burden of explicitly handling universes.
768 % TODO add sectioon about universes
770 \subsubsection{Contexts}
772 \begin{minipage}{0.5\textwidth}
773 \mydesc{context validity:}{\myvalid{\myctx}}{
776 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
777 \UnaryInfC{$\myvalid{\myemptyctx}$}
780 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
781 \UnaryInfC{$\myvalid{\myctx ; \myb{x} : \mytya}$}
787 \begin{minipage}{0.5\textwidth}
788 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
790 \AxiomC{$\myctx(x) = \mytya$}
791 \UnaryInfC{$\myjud{\myb{x}}{\mytya}$}
798 We need to refine the notion context to make sure that every variable appearing
799 is typed correctly, or that in other words each type appearing in the context is
800 indeed a type and not a value. In every other rule, if no premises are present,
801 we assume the context in the conclusion to be valid.
803 Then we can re-introduce the old rule to get the type of a variable for a
806 \subsubsection{$\myunit$, $\myempty$}
808 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
811 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
812 \UnaryInfC{$\myjud{\myunit}{\mytyp_0}$}
814 \UnaryInfC{$\myjud{\myempty}{\mytyp_0}$}
817 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
818 \UnaryInfC{$\myjud{\mytt}{\myunit}$}
820 \UnaryInfC{\phantom{$\myjud{\myempty}{\mytyp_0}$}}
823 \AxiomC{$\myjud{\mytmt}{\myempty}$}
824 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
825 \BinaryInfC{$\myjud{\myapp{\myabsurd{\mytya}}{\mytmt}}{\mytya}$}
827 \UnaryInfC{\phantom{$\myjud{\myempty}{\mytyp_0}$}}
833 Nothing surprising here: $\myunit$ and $\myempty$ are unchanged from the STLC,
834 with the added rules to type $\myunit$ and $\myempty$ themselves, and to make
835 sure that we are invoking $\myabsurd{}$ over a type.
837 \subsubsection{$\mybool$, and dependent $\myfun{if}$}
839 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
843 \UnaryInfC{$\myjud{\mybool}{\mytyp_0}$}
847 \UnaryInfC{$\myjud{\mytrue}{\mybool}$}
851 \UnaryInfC{$\myjud{\myfalse}{\mybool}$}
856 \AxiomC{$\myjud{\mytmt}{\mybool}$}
857 \AxiomC{$\myjudd{\myctx : \mybool}{\mytya}{\mytyp_l}$}
859 \BinaryInfC{$\myjud{\mytmm}{\mysub{\mytya}{x}{\mytrue}}$ \hspace{0.7cm} $\myjud{\mytmn}{\mysub{\mytya}{x}{\myfalse}}$}
860 \UnaryInfC{$\myjud{\myitee{\mytmt}{\myb{x}}{\mytya}{\mytmm}{\mytmn}}{\mysub{\mytya}{\myb{x}}{\mytmt}}$}
866 With booleans we get the first taste of `dependent' in `dependent types'. While
867 the two introduction rules ($\mytrue$ and $\myfalse$) are not surprising, the
868 typing rules for $\myfun{if}$ are. In most strongly typed languages we expect
869 the branches of an $\myfun{if}$ statements to be of the same type, to preserve
870 subject reduction, since execution could take both paths. This is a pity, since
871 the type system does not reflect the fact that in each branch we gain knowledge
872 on the term we are branching on. Which means that programs along the lines of
874 if null xs then head xs else 0
876 are a necessary, well typed, danger.
878 However, in a more expressive system, we can do better: the branches' type can
879 depend on the value of the scrutinised boolean. This is what the typing rule
880 expresses: the user provides a type $\mytya$ ranging over an $\myb{x}$
881 representing the scrutinised boolean type, and the branches are typechecked with
882 the updated knowledge on the value of $\myb{x}$.
884 \subsubsection{$\myarr$, or dependent function}
886 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
888 \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
889 \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
890 \BinaryInfC{$\myjud{\myfora{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
896 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytmt}{\mytyb}$}
897 \UnaryInfC{$\myjud{\myabss{\myb{x}}{\mytya}{\mytmt}}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
900 \AxiomC{$\myjud{\mytmm}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
901 \AxiomC{$\myjud{\mytmn}{\mytya}$}
902 \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mysub{\mytyb}{\myb{x}}{\mytmn}}$}
908 Dependent functions are one of the two key features that perhaps most
909 characterise dependent types---the other being dependent products. With
910 dependent functions, the result type can depend on the value of the argument.
911 This feature, together with the fact that the result type might be a type
912 itself, brings a lot of interesting possibilities. Keeping the correspondence
913 with logic alive, dependent functions are much like universal quantifiers
914 ($\forall$) in logic.
916 Again, we need to make sure that the type hierarchy is respected, which is the
917 reason why a type formed by $\myarr$ will live in the least upper bound of the
918 levels of argument and return type. This trend will continue with the other
919 type-level binders, $\myprod$ and $\mytyc{W}$.
921 % TODO maybe examples?
923 \subsubsection{$\myprod$, or dependent product}
926 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
928 \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
929 \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
930 \BinaryInfC{$\myjud{\myexi{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
936 \AxiomC{$\myjud{\mytmm}{\mytya}$}
937 \AxiomC{$\myjud{\mytmn}{\mysub{\mytyb}{\myb{x}}{\mytmm}}$}
938 \BinaryInfC{$\myjud{\mypairr{\mytmm}{\myb{x}}{\mytyb}{\mytmn}}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
940 \UnaryInfC{\phantom{$--$}}
943 \AxiomC{$\myjud{\mytmt}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
944 \UnaryInfC{$\hspace{0.7cm}\myjud{\myapp{\myfst}{\mytmt}}{\mytya}\hspace{0.7cm}$}
946 \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mysub{\mytyb}{\myb{x}}{\myapp{\myfst}{\mytmt}}}$}
954 \subsubsection{$\mytyc{W}$, or well-order}
955 \label{sec:well-order}
957 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
959 \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
960 \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
961 \BinaryInfC{$\myjud{\myw{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
966 \AxiomC{$\myjud{\mytmt}{\mytya}$}
967 \AxiomC{$\myjud{\mysynel{f}}{\mysub{\mytyb}{\myb{x}}{\mytmt} \myarr \myw{\myb{x}}{\mytya}{\mytyb}}$}
968 \BinaryInfC{$\myjud{\mytmt \mynode{\myb{x}}{\mytyb} \myse{f}}{\myw{\myb{x}}{\mytya}{\mytyb}}$}
973 \AxiomC{$\myjud{\myse{u}}{\myw{\myb{x}}{\myse{S}}{\myse{T}}}$}
974 \AxiomC{$\myjudd{\myctx; \myb{w} : \myw{\myb{x}}{\myse{S}}{\myse{T}}}{\myse{P}}{\mytyp_l}$}
976 \BinaryInfC{$\myjud{\myse{p}}{
977 \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}}}}
979 \UnaryInfC{$\myjud{\myrec{\myse{u}}{\myb{w}}{\myse{P}}{\myse{p}}}{\mysub{\myse{P}}{\myb{w}}{\myse{u}}}$}
985 \section{The struggle for equality}
988 \subsection{Propositional equality...}
990 \subsection{...and its limitations}
998 \subsection{Equality reflection}
1000 \subsection{Observational equality}
1002 \subsection{Univalence foundations}
1004 \section{Augmenting ITT}
1005 \label{sec:practical}
1007 \subsection{A more liberal hierarchy}
1009 \subsection{Type inference}
1011 \subsubsection{Bidirectional type checking}
1013 \subsubsection{Pattern unification}
1015 \subsection{Pattern matching and explicit fixpoints}
1017 \subsection{Induction-recursion}
1019 \subsection{Coinduction}
1021 \subsection{Dealing with partiality}
1023 \subsection{Type holes}
1031 \section{Notation and syntax}
1033 Syntax, derivation rules, and reduction rules, are enclosed in frames describing
1034 the type of relation being established and the syntactic elements appearing,
1037 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
1038 Typing derivations here.
1041 In the languages presented and Agda code samples I also highlight the syntax,
1042 following a uniform color and font convention:
1045 \begin{tabular}{c | l}
1046 $\mytyc{Sans}$ & Type constructors. \\
1047 $\mydc{sans}$ & Data constructors. \\
1048 % $\myfld{sans}$ & Field accessors (e.g. \myfld{fst} and \myfld{snd} for products). \\
1049 $\mysyn{roman}$ & Keywords of the language. \\
1050 $\myfun{roman}$ & Defined values and destructors. \\
1051 $\myb{math}$ & Bound variables.
1055 Moreover, I will from time to time give examples in the Haskell programming
1056 language as defined in \citep{Haskell2010}, which I will typeset in
1057 \texttt{teletype} font. I assume that the reader is already familiar with
1058 Haskell, plenty of good introductions are available \citep{LYAH,ProgInHask}.
1060 When presenting grammars, I will use a word in $\mysynel{math}$ font
1061 (e.g. $\mytmsyn$ or $\mytysyn$) to indicate indicate nonterminals. Additionally,
1062 I will use quite flexibly a $\mysynel{math}$ font to indicate a syntactic
1063 element. More specifically, terms are usually indicated by lowercase letters
1064 (often $\mytmt$, $\mytmm$, or $\mytmn$); and types by an uppercase letter (often
1065 $\mytya$, $\mytyb$, or $\mytycc$).
1067 When presenting type derivations, I will often abbreviate and present multiple
1068 conclusions, each on a separate line:
1071 \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
1072 \UnaryInfC{$\myjud{\myapp{\myfst}{\mytmt}}{\mytya}$}
1074 \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mytyb}$}
1077 \section{Agda rendition of core ITT}
1078 \label{app:agda-code}
1086 absurd : ∀ {a} {A : Set a} → ⊥ → A
1089 record ⊤ : Set where
1092 record _×_ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
1098 data Bool : Set where
1101 if_then_else_ : ∀ {a} {P : Bool → Set a} (x : Bool) → P true → P false → P x
1102 if true then x else _ = x
1103 if false then _ else x = x
1105 data W {s p} (S : Set s) (P : S → Set p) : Set (s ⊔ p) where
1106 _◁_ : (s : S) → (P s → W S P) → W S P
1108 rec : ∀ {a b} {S : Set a} {P : S → Set b}
1109 (C : W S P → Set) → -- some conclusion we hope holds
1110 ((s : S) → -- given a shape...
1111 (f : P s → W S P) → -- ...and a bunch of kids...
1112 ((p : P s) → C (f p)) → -- ...and C for each kid in the bunch...
1113 C (s ◁ f)) → -- ...does C hold for the node?
1114 (x : W S P) → -- If so, ...
1115 C x -- ...C always holds.
1116 rec C c (s ◁ f) = c s f (λ p → rec C c (f p))
1120 \bibliographystyle{authordate1}
1121 \bibliography{thesis}