1 \documentclass[report]{article}
5 % \usepackage{fullpage}
17 \usepackage[fleqn]{amsmath}
18 \usepackage{stmaryrd} %llbracket
21 \usepackage{bussproofs}
33 \usepackage{subcaption}
37 \usetikzlibrary{shapes,arrows,positioning}
38 % \usepackage{tikz-cd}
39 % \usepackage{pgfplots}
42 %% -----------------------------------------------------------------------------
44 \usepackage[english]{babel}
45 \usepackage[conor]{agda}
46 \renewcommand{\AgdaKeywordFontStyle}[1]{\ensuremath{\mathrm{\underline{#1}}}}
47 \renewcommand{\AgdaFunction}[1]{\textbf{\textcolor{AgdaFunction}{#1}}}
48 \renewcommand{\AgdaField}{\AgdaFunction}
49 % \definecolor{AgdaBound} {HTML}{000000}
50 \definecolor{AgdaHole} {HTML} {FFFF33}
52 \DeclareUnicodeCharacter{9665}{\ensuremath{\lhd}}
53 \DeclareUnicodeCharacter{964}{\ensuremath{\tau}}
54 \DeclareUnicodeCharacter{963}{\ensuremath{\sigma}}
55 \DeclareUnicodeCharacter{915}{\ensuremath{\Gamma}}
56 \DeclareUnicodeCharacter{8799}{\ensuremath{\stackrel{?}{=}}}
57 \DeclareUnicodeCharacter{9655}{\ensuremath{\rhd}}
60 %% -----------------------------------------------------------------------------
63 \newcommand{\mysyn}{\AgdaKeyword}
64 \newcommand{\mytyc}{\AgdaDatatype}
65 % TODO have this with math mode so I can have subscripts
66 \newcommand{\mydc}{\AgdaInductiveConstructor}
67 \newcommand{\myfld}{\AgdaField}
68 \newcommand{\myfun}{\AgdaFunction}
69 \newcommand{\myb}[1]{\AgdaBound{$#1$}}
70 \newcommand{\myfield}{\AgdaField}
71 \newcommand{\myind}{\AgdaIndent}
72 \newcommand{\mykant}{\textsc{Kant}}
73 \newcommand{\mysynel}[1]{#1}
74 \newcommand{\myse}{\mysynel}
75 \newcommand{\mytmsyn}{\mysynel{term}}
76 \newcommand{\mysp}{\ }
77 \newcommand{\myabs}[2]{\mydc{$\lambda$} #1 \mathrel{\mydc{$\mapsto$}} #2}
78 \newcommand{\myappsp}{\hspace{0.07cm}}
79 \newcommand{\myapp}[2]{#1 \myappsp #2}
80 \newcommand{\mysynsep}{\ \ |\ \ }
83 \newcommand{\mydesc}[3]{
89 \hfill \textbf{#1} $#2$
91 \framebox[\textwidth]{
105 % TODO is \mathbin the correct thing for arrow and times?
107 \newcommand{\mytmt}{\mysynel{t}}
108 \newcommand{\mytmm}{\mysynel{m}}
109 \newcommand{\mytmn}{\mysynel{n}}
110 \newcommand{\myred}{\leadsto}
111 \newcommand{\mysub}[3]{#1[#2 / #3]}
112 \newcommand{\mytysyn}{\mysynel{type}}
113 \newcommand{\mybasetys}{K}
114 % TODO change this name
115 \newcommand{\mybasety}[1]{B_{#1}}
116 \newcommand{\mytya}{\myse{A}}
117 \newcommand{\mytyb}{\myse{B}}
118 \newcommand{\mytycc}{\myse{C}}
119 \newcommand{\myarr}{\mathrel{\textcolor{AgdaDatatype}{\to}}}
120 \newcommand{\myprod}{\mathrel{\textcolor{AgdaDatatype}{\times}}}
121 \newcommand{\myctx}{\Gamma}
122 \newcommand{\myvalid}[1]{#1 \vdash \underline{\mathrm{valid}}}
123 \newcommand{\myjudd}[3]{#1 \vdash #2 : #3}
124 \newcommand{\myjud}[2]{\myjudd{\myctx}{#1}{#2}}
125 % TODO \mathbin or \mathrel here?
126 \newcommand{\myabss}[3]{\mydc{$\lambda$} #1 {:} #2 \mathrel{\mydc{$\mapsto$}} #3}
127 \newcommand{\mytt}{\mydc{$\langle\rangle$}}
128 \newcommand{\myunit}{\mytyc{Unit}}
129 \newcommand{\mypair}[2]{\mathopen{\mydc{$\langle$}}#1\mathpunct{\mydc{,}} #2\mathclose{\mydc{$\rangle$}}}
130 \newcommand{\myfst}{\myfld{fst}}
131 \newcommand{\mysnd}{\myfld{snd}}
132 \newcommand{\myconst}{\myse{c}}
133 \newcommand{\myemptyctx}{\cdot}
134 \newcommand{\myhole}{\AgdaHole}
135 \newcommand{\myfix}[3]{\mysyn{fix} \myappsp #1 {:} #2 \mapsto #3}
136 \newcommand{\mysum}{\mathbin{\textcolor{AgdaDatatype}{+}}}
137 \newcommand{\myleft}[1]{\mydc{left}_{#1}}
138 \newcommand{\myright}[1]{\mydc{right}_{#1}}
139 \newcommand{\myempty}{\mytyc{Empty}}
140 \newcommand{\mycase}[2]{\mathopen{\myfun{[}}#1\mathpunct{\myfun{,}} #2 \mathclose{\myfun{]}}}
141 \newcommand{\myabsurd}[1]{\myfun{absurd}_{#1}}
142 \newcommand{\myarg}{-}
143 \newcommand{\myderivsp}{\vspace{0.3cm}}
144 \newcommand{\mytyp}{\mytyc{Type}}
145 \newcommand{\myneg}{\myfun{$\neg$}}
146 \newcommand{\myar}{\,}
147 \newcommand{\mybool}{\mytyc{Bool}}
148 \newcommand{\mytrue}{\mydc{true}}
149 \newcommand{\myfalse}{\mydc{false}}
150 \newcommand{\myitee}[5]{\myfun{if}\,#1 / {#2.#3}\,\myfun{then}\,#4\,\myfun{else}\,#5}
151 \newcommand{\mynat}{\mytyc{$\mathbb{N}$}}
152 \newcommand{\myrat}{\mytyc{$\mathbb{R}$}}
153 \newcommand{\myite}[3]{\myfun{if}\,#1\,\myfun{then}\,#2\,\myfun{else}\,#3}
154 \newcommand{\myfora}[3]{(#1 {:} #2) \myarr #3}
155 \newcommand{\myexi}[3]{(#1 {:} #2) \myprod #3}
156 \newcommand{\mypairr}[4]{\mathopen{\mydc{$\langle$}}#1\mathpunct{\mydc{,}} #4\mathclose{\mydc{$\rangle$}}_{#2{.}#3}}
157 \newcommand{\mylist}{\mytyc{List}}
158 \newcommand{\mynil}[1]{\mydc{[]}_{#1}}
159 \newcommand{\mycons}{\mathbin{\mydc{∷}}}
160 \newcommand{\myfoldr}{\myfun{foldr}}
161 \newcommand{\myw}[3]{\myapp{\myapp{\mytyc{W}}{(#1 {:} #2)}}{#3}}
162 \newcommand{\mynode}[2]{\mathbin{\mydc{$\lhd$}_{#1.#2}}}
163 \newcommand{\myrec}[4]{\myfun{rec}\,#1 / {#2.#3}\,\myfun{with}\,#4}
164 \newcommand{\mylub}{\sqcup}
165 \newcommand{\mydefeq}{\cong}
166 \newcommand{\myrefl}{\mydc{refl}}
167 \newcommand{\mypeq}[1]{\mathrel{\mytyc{=}_{#1}}}
168 \newcommand{\myjeqq}{\myfun{=-elim}}
169 \newcommand{\myjeq}[3]{\myapp{\myapp{\myapp{\myjeqq}{#1}}{#2}}{#3}}
170 \newcommand{\mysubst}{\myfun{subst}}
171 \newcommand{\myprsyn}{\myse{prop}}
172 \newcommand{\myprdec}[1]{\mathopen{\mytyc{$\llbracket$}} #1 \mathopen{\mytyc{$\rrbracket$}}}
173 \newcommand{\myand}{\mathrel{\mytyc{$\wedge$}}}
174 \newcommand{\myprfora}[3]{\forall #1 {:} #2. #3}
175 \newcommand{\myimpl}{\mathrel{\mytyc{$\Rightarrow$}}}
176 \newcommand{\mybot}{\mytyc{$\bot$}}
177 \newcommand{\mytop}{\mytyc{$\top$}}
178 \newcommand{\mycoe}{\myfun{coe}}
179 \newcommand{\mycoee}[4]{\myapp{\myapp{\myapp{\myapp{\mycoe}{#1}}{#2}}{#3}}{#4}}
180 \newcommand{\mycoh}{\myfun{coh}}
181 \newcommand{\mycohh}[4]{\myapp{\myapp{\myapp{\myapp{\mycoh}{#1}}{#2}}{#3}}{#4}}
182 \newcommand{\myjm}[4]{(#1 {:} #2) \mathrel{\mytyc{=}} (#3 {:} #4)}
183 \newcommand{\myeq}{\mathrel{\mytyc{=}}}
184 \newcommand{\myprop}{\mytyc{Prop}}
185 \newcommand{\mytmup}{\mytmsyn\uparrow}
186 \newcommand{\mydefs}{\Delta}
187 \newcommand{\mynf}{\Downarrow}
188 \newcommand{\myinff}[3]{#1 \vdash #2 \Rightarrow #3}
189 \newcommand{\myinf}[2]{\myinff{\myctx}{#1}{#2}}
190 \newcommand{\mychkk}[3]{#1 \vdash #2 \Leftarrow #3}
191 \newcommand{\mychk}[2]{\mychkk{\myctx}{#1}{#2}}
192 \newcommand{\myann}[2]{#1 : #2}
193 \newcommand{\mydeclsyn}{\myse{decl}}
194 \newcommand{\myval}[3]{#1 : #2 \mapsto #3}
195 \newcommand{\mypost}[2]{\mysyn{postulate}\ #1 : #2}
196 \newcommand{\myadt}[4]{\mysyn{data}\ #1 : #2\ \mysyn{where}\ #3\{ #4 \}}
197 \newcommand{\myreco}[4]{\mysyn{record}\ #1 : #2\ \mysyn{where}\ #3\ \{ #4 \}}
199 \newcommand{\myelabt}{\vdash}
200 \newcommand{\myelabf}{\rhd}
201 \newcommand{\myelab}[2]{\myctx \myelabt #1 \myelabf #2}
202 \newcommand{\mytele}{\Delta}
203 \newcommand{\mytelee}{\delta}
204 \newcommand{\mydcctx}{\Gamma}
205 \newcommand{\mynamesyn}{\myse{name}}
206 \newcommand{\myvec}{\overrightarrow}
207 \newcommand{\mymeta}{\textsc}
208 \newcommand{\myhyps}{\mymeta{hyps}}
209 \newcommand{\mycc}{;}
210 \newcommand{\myemptytele}{\cdot}
211 \newcommand{\mymetagoes}{\Longrightarrow}
212 % \newcommand{\mytesctx}{\
213 \newcommand{\mytelesyn}{\myse{telescope}}
214 \newcommand{\myrecs}{\mymeta{recs}}
215 \newcommand{\myle}{\mathrel{\lcfun{$\le$}}}
217 %% -----------------------------------------------------------------------------
219 \title{\mykant: Implementing Observational Equality}
220 \author{Francesco Mazzoli \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{<fm2209@ic.ac.uk>}}}
234 The marriage between programming and logic has been a very fertile one. In
235 particular, since the simply typed lambda calculus (STLC), a number of type
236 systems have been devised with increasing expressive power.
238 Section \ref{sec:types} will give a very brief overview of STLC, and then
239 illustrate how it can be interpreted as a natural deduction system. Section
240 \ref{sec:itt} will introduce Inutitionistic Type Theory (ITT), which expands
241 on this concept, employing a more expressive logic. The exposition is quite
242 dense since there is a lot of material to cover; for a more complete treatment
243 of the material the reader can refer to \citep{Thompson1991, Pierce2002}.
244 Section \ref{sec:equality} will explain why equality has always been a tricky
245 business in these theories, and talk about the various attempts that have been
246 made to make the situation better. One interesting development has recently
247 emerged: Observational Type theory.
249 Section \ref{sec:practical} will describe common extensions found in the
250 systems currently in use. Finally, section \ref{sec:kant} will describe a
251 system developed by the author that implements a core calculus based on the
252 principles described.
261 \section{Simple and not-so-simple types}
264 \subsection{The untyped $\lambda$-calculus}
266 Along with Turing's machines, the earliest attempts to formalise computation
267 lead to the $\lambda$-calculus \citep{Church1936}. This early programming
268 language encodes computation with a minimal syntax and no `data' in the
269 traditional sense, but just functions. Here we give a brief overview of the
270 language, which will give the chance to introduce concepts central to the
271 analysis of all the following calculi. The exposition follows the one found in
272 chapter 5 of \cite{Queinnec2003}.
274 The syntax of $\lambda$-terms consists of three things: variables, abstractions,
279 \begin{array}{r@{\ }c@{\ }l}
280 \mytmsyn & ::= & \myb{x} \mysynsep \myabs{\myb{x}}{\mytmsyn} \mysynsep (\myapp{\mytmsyn}{\mytmsyn}) \\
281 x & \in & \text{Some enumerable set of symbols}
286 Parenthesis will be omitted in the usual way:
287 $\myapp{\myapp{\mytmt}{\mytmm}}{\mytmn} =
288 \myapp{(\myapp{\mytmt}{\mytmm})}{\mytmn}$.
290 Abstractions roughly corresponds to functions, and their semantics is more
291 formally explained by the $\beta$-reduction rule:
293 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
296 \myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{\myb{x}}{\mytmn}\text{, where} \\
298 \begin{array}{l@{\ }c@{\ }l}
299 \mysub{\myb{x}}{\myb{x}}{\mytmn} & = & \mytmn \\
300 \mysub{\myb{y}}{\myb{x}}{\mytmn} & = & y\text{, with } \myb{x} \neq y \\
301 \mysub{(\myapp{\mytmt}{\mytmm})}{\myb{x}}{\mytmn} & = & (\myapp{\mysub{\mytmt}{\myb{x}}{\mytmn}}{\mysub{\mytmm}{\myb{x}}{\mytmn}}) \\
302 \mysub{(\myabs{\myb{x}}{\mytmm})}{\myb{x}}{\mytmn} & = & \myabs{\myb{x}}{\mytmm} \\
303 \mysub{(\myabs{\myb{y}}{\mytmm})}{\myb{x}}{\mytmn} & = & \myabs{\myb{z}}{\mysub{\mysub{\mytmm}{\myb{y}}{\myb{z}}}{\myb{x}}{\mytmn}}, \\
304 \multicolumn{3}{l}{\myind{1} \text{with $\myb{x} \neq \myb{y}$ and $\myb{z}$ not free in $\myapp{\mytmm}{\mytmn}$}}
310 The care required during substituting variables for terms is required to avoid
311 name capturing. We will use substitution in the future for other name-binding
312 constructs assuming similar precautions.
314 These few elements are of remarkable expressiveness, and in fact Turing
315 complete. As a corollary, we must be able to devise a term that reduces forever
316 (`loops' in imperative terms):
318 (\myapp{\omega}{\omega}) \myred (\myapp{\omega}{\omega}) \myred \cdots \text{, with $\omega = \myabs{x}{\myapp{x}{x}}$}
321 A \emph{redex} is a term that can be reduced. In the untyped $\lambda$-calculus
322 this will be the case for an application in which the first term is an
323 abstraction, but in general we call aterm reducible if it appears to the left of
324 a reduction rule. When a term contains no redexes it's said to be in
325 \emph{normal form}. Given the observation above, not all terms reduce to a
326 normal forms: we call the ones that do \emph{normalising}, and the ones that
327 don't \emph{non-normalising}.
329 The reduction rule presented is not syntax directed, but \emph{evaluation
330 strategies} can be employed to reduce term systematically. Common evaluation
331 strategies include \emph{call by value} (or \emph{strict}), where arguments of
332 abstractions are reduced before being applied to the abstraction; and conversely
333 \emph{call by name} (or \emph{lazy}), where we reduce only when we need to do so
334 to proceed---in other words when we have an application where the function is
335 still not a $\lambda$. In both these reduction strategies we never reduce under
336 an abstraction: for this reason a weaker form of normalisation is used, where
337 both abstractions and normal forms are said to be in \emph{weak head normal
340 \subsection{The simply typed $\lambda$-calculus}
342 A convenient way to `discipline' and reason about $\lambda$-terms is to assign
343 \emph{types} to them, and then check that the terms that we are forming make
344 sense given our typing rules \citep{Curry1934}. The first most basic instance
345 of this idea takes the name of \emph{simply typed $\lambda$ calculus}, whose
346 rules are shown in figure \ref{fig:stlc}.
348 Our types contain a set of \emph{type variables} $\Phi$, which might
349 correspond to some `primitive' types; and $\myarr$, the type former for
350 `arrow' types, the types of functions. The language is explicitly
351 typed: when we bring a variable into scope with an abstraction, we
352 explicitly declare its type. Reduction is unchanged from the untyped
358 \begin{array}{r@{\ }c@{\ }l}
359 \mytmsyn & ::= & \myb{x} \mysynsep \myabss{\myb{x}}{\mytysyn}{\mytmsyn} \mysynsep
360 (\myapp{\mytmsyn}{\mytmsyn}) \\
361 \mytysyn & ::= & \myse{\phi} \mysynsep \mytysyn \myarr \mytysyn \mysynsep \\
362 \myb{x} & \in & \text{Some enumerable set of symbols} \\
363 \myse{\phi} & \in & \Phi
368 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
370 \AxiomC{$\myctx(x) = A$}
371 \UnaryInfC{$\myjud{\myb{x}}{A}$}
374 \AxiomC{$\myjudd{\myctx;\myb{x} : A}{\mytmt}{\mytyb}$}
375 \UnaryInfC{$\myjud{\myabss{x}{A}{\mytmt}}{\mytyb}$}
378 \AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$}
379 \AxiomC{$\myjud{\mytmn}{\mytya}$}
380 \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mytyb}$}
384 \caption{Syntax and typing rules for the STLC. Reduction is unchanged from
385 the untyped $\lambda$-calculus.}
389 In the typing rules, a context $\myctx$ is used to store the types of bound
390 variables: $\myctx; \myb{x} : \mytya$ adds a variable to the context and
391 $\myctx(x)$ returns the type of the rightmost occurrence of $x$.
393 This typing system takes the name of `simply typed lambda calculus' (STLC), and
394 enjoys a number of properties. Two of them are expected in most type systems
397 \item[Progress] A well-typed term is not stuck---it is either a variable, or its
398 constructor does not appear on the left of the $\myred$ relation (currently
399 only $\lambda$), or it can take a step according to the evaluation rules.
400 \item[Preservation] If a well-typed term takes a step of evaluation, then the
401 resulting term is also well-typed, and preserves the previous type. Also
402 known as \emph{subject reduction}.
405 However, STLC buys us much more: every well-typed term is normalising
406 \citep{Tait1967}. It is easy to see that we can't fill the blanks if we want to
407 give types to the non-normalising term shown before:
409 \myapp{(\myabss{\myb{x}}{\myhole{?}}{\myapp{\myb{x}}{\myb{x}}})}{(\myabss{\myb{x}}{\myhole{?}}{\myapp{\myb{x}}{\myb{x}}})}
412 This makes the STLC Turing incomplete. We can recover the ability to loop by
413 adding a combinator that recurses:
416 \begin{minipage}{0.5\textwidth}
418 $ \mytmsyn ::= \cdots b \mysynsep \myfix{\myb{x}}{\mytysyn}{\mytmsyn} $
422 \begin{minipage}{0.5\textwidth}
423 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}} {
424 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytmt}{\mytya}$}
425 \UnaryInfC{$\myjud{\myfix{\myb{x}}{\mytya}{\mytmt}}{\mytya}$}
430 \mydesc{reduction:}{\myjud{\mytmsyn}{\mytmsyn}}{
431 $ \myfix{\myb{x}}{\mytya}{\mytmt} \myred \mysub{\mytmt}{\myb{x}}{(\myfix{\myb{x}}{\mytya}{\mytmt})}$
434 This will deprive us of normalisation, which is a particularly bad thing if we
435 want to use the STLC as described in the next section.
437 \subsection{The Curry-Howard correspondence}
439 It turns out that the STLC can be seen a natural deduction system for
440 intuitionistic propositional logic. Terms are proofs, and their types are the
441 propositions they prove. This remarkable fact is known as the Curry-Howard
442 correspondence, or isomorphism.
444 The arrow ($\myarr$) type corresponds to implication. If we wish to prove that
445 that $(\mytya \myarr \mytyb) \myarr (\mytyb \myarr \mytycc) \myarr (\mytya
446 \myarr \mytycc)$, all we need to do is to devise a $\lambda$-term that has the
449 \myabss{\myb{f}}{(\mytya \myarr \mytyb)}{\myabss{\myb{g}}{(\mytyb \myarr \mytycc)}{\myabss{\myb{x}}{\mytya}{\myapp{\myb{g}}{(\myapp{\myb{f}}{\myb{x}})}}}}
451 That is, function composition. Going beyond arrow types, we can extend our bare
452 lambda calculus with useful types to represent other logical constructs, as
453 shown in figure \ref{fig:natded}.
458 \begin{array}{r@{\ }c@{\ }l}
459 \mytmsyn & ::= & \cdots \\
460 & | & \mytt \mysynsep \myapp{\myabsurd{\mytysyn}}{\mytmsyn} \\
461 & | & \myapp{\myleft{\mytysyn}}{\mytmsyn} \mysynsep
462 \myapp{\myright{\mytysyn}}{\mytmsyn} \mysynsep
463 \myapp{\mycase{\mytmsyn}{\mytmsyn}}{\mytmsyn} \\
464 & | & \mypair{\mytmsyn}{\mytmsyn} \mysynsep
465 \myapp{\myfst}{\mytmsyn} \mysynsep \myapp{\mysnd}{\mytmsyn} \\
466 \mytysyn & ::= & \cdots \mysynsep \myunit \mysynsep \myempty \mysynsep \mytmsyn \mysum \mytmsyn \mysynsep \mytysyn \myprod \mytysyn
471 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
474 \begin{array}{l@{ }l@{\ }c@{\ }l}
475 \myapp{\mycase{\mytmm}{\mytmn}}{(\myapp{\myleft{\mytya} &}{\mytmt})} & \myred &
476 \myapp{\mytmm}{\mytmt} \\
477 \myapp{\mycase{\mytmm}{\mytmn}}{(\myapp{\myright{\mytya} &}{\mytmt})} & \myred &
478 \myapp{\mytmn}{\mytmt}
483 \begin{array}{l@{ }l@{\ }c@{\ }l}
484 \myapp{\myfst &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmm \\
485 \myapp{\mysnd &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmn
491 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
493 \AxiomC{\phantom{$\myjud{\mytmt}{\myempty}$}}
494 \UnaryInfC{$\myjud{\mytt}{\myunit}$}
497 \AxiomC{$\myjud{\mytmt}{\myempty}$}
498 \UnaryInfC{$\myjud{\myapp{\myabsurd{\mytya}}{\mytmt}}{\mytya}$}
505 \AxiomC{$\myjud{\mytmt}{\mytya}$}
506 \UnaryInfC{$\myjud{\myapp{\myleft{\mytyb}}{\mytmt}}{\mytya \mysum \mytyb}$}
509 \AxiomC{$\myjud{\mytmt}{\mytyb}$}
510 \UnaryInfC{$\myjud{\myapp{\myright{\mytya}}{\mytmt}}{\mytya \mysum \mytyb}$}
518 \AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$}
519 \AxiomC{$\myjud{\mytmn}{\mytya \myarr \mytycc}$}
520 \AxiomC{$\myjud{\mytmt}{\mytya \mysum \mytyb}$}
521 \TrinaryInfC{$\myjud{\myapp{\mycase{\mytmm}{\mytmn}}{\mytmt}}{\mytycc}$}
528 \AxiomC{$\myjud{\mytmm}{\mytya}$}
529 \AxiomC{$\myjud{\mytmn}{\mytyb}$}
530 \BinaryInfC{$\myjud{\mypair{\mytmm}{\mytmn}}{\mytya \myprod \mytyb}$}
533 \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
534 \UnaryInfC{$\myjud{\myapp{\myfst}{\mytmt}}{\mytya}$}
537 \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
538 \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mytyb}$}
542 \caption{Rules for the extendend STLC. Only the new features are shown, all the
543 rules and syntax for the STLC apply here too.}
547 Tagged unions (or sums, or coproducts---$\mysum$ here, \texttt{Either}
548 in Haskell) correspond to disjunctions, and dually tuples (or pairs, or
549 products---$\myprod$ here, tuples in Haskell) correspond to
550 conjunctions. This is apparent looking at the ways to construct and
551 destruct the values inhabiting those types: for $\mysum$ $\myleft{ }$
552 and $\myright{ }$ correspond to $\vee$ introduction, and
553 $\mycase{\myarg}{\myarg}$ to $\vee$ elimination; for $\myprod$
554 $\mypair{\myarg}{\myarg}$ corresponds to $\wedge$ introduction, $\myfst$
555 and $\mysnd$ to $\wedge$ elimination.
557 The trivial type $\myunit$ corresponds to the logical $\top$, and dually
558 $\myempty$ corresponds to the logical $\bot$. $\myunit$ has one introduction
559 rule ($\mytt$), and thus one inhabitant; and no eliminators. $\myempty$ has no
560 introduction rules, and thus no inhabitants; and one eliminator ($\myabsurd{
561 }$), corresponding to the logical \emph{ex falso quodlibet}.
563 With these rules, our STLC now looks remarkably similar in power and use to the
564 natural deduction we already know. $\myneg \mytya$ can be expressed as $\mytya
565 \myarr \myempty$. However, there is an important omission: there is no term of
566 the type $\mytya \mysum \myneg \mytya$ (excluded middle), or equivalently
567 $\myneg \myneg \mytya \myarr \mytya$ (double negation), or indeed any term with
568 a type equivalent to those.
570 This has a considerable effect on our logic and it's no coincidence, since there
571 is no obvious computational behaviour for laws like the excluded middle.
572 Theories of this kind are called \emph{intuitionistic}, or \emph{constructive},
573 and all the systems analysed will have this characteristic since they build on
574 the foundation of the STLC\footnote{There is research to give computational
575 behaviour to classical logic, but I will not touch those subjects.}.
577 As in logic, if we want to keep our system consistent, we must make sure that no
578 closed terms (in other words terms not under a $\lambda$) inhabit $\myempty$.
579 The variant of STLC presented here is indeed
580 consistent, a result that follows from the fact that it is
581 normalising. % TODO explain
582 Going back to our $\mysyn{fix}$ combinator, it is easy to see how it ruins our
583 desire for consistency. The following term works for every type $\mytya$,
586 (\myfix{\myb{x}}{\mytya}{\myb{x}}) : \mytya
589 \subsection{Inductive data}
592 To make the STLC more useful as a programming language or reasoning tool it is
593 common to include (or let the user define) inductive data types. These comprise
594 of a type former, various constructors, and an eliminator (or destructor) that
595 serves as primitive recursor.
597 For example, we might add a $\mylist$ type constructor, along with an `empty
598 list' ($\mynil{ }$) and `cons cell' ($\mycons$) constructor. The eliminator for
599 lists will be the usual folding operation ($\myfoldr$). See figure
605 \begin{array}{r@{\ }c@{\ }l}
606 \mytmsyn & ::= & \cdots \mysynsep \mynil{\mytysyn} \mysynsep \mytmsyn \mycons \mytmsyn
608 \myapp{\myapp{\myapp{\myfoldr}{\mytmsyn}}{\mytmsyn}}{\mytmsyn} \\
609 \mytysyn & ::= & \cdots \mysynsep \myapp{\mylist}{\mytysyn}
613 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
615 \begin{array}{l@{\ }c@{\ }l}
616 \myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{\mynil{\mytya}} & \myred & \mytmt \\
618 \myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{(\mytmm \mycons \mytmn)} & \myred &
619 \myapp{\myapp{\myse{f}}{\mytmm}}{(\myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{\mytmn})}
623 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
625 \AxiomC{\phantom{$\myjud{\mytmm}{\mytya}$}}
626 \UnaryInfC{$\myjud{\mynil{\mytya}}{\myapp{\mylist}{\mytya}}$}
629 \AxiomC{$\myjud{\mytmm}{\mytya}$}
630 \AxiomC{$\myjud{\mytmn}{\myapp{\mylist}{\mytya}}$}
631 \BinaryInfC{$\myjud{\mytmm \mycons \mytmn}{\myapp{\mylist}{\mytya}}$}
636 \AxiomC{$\myjud{\mysynel{f}}{\mytya \myarr \mytyb \myarr \mytyb}$}
637 \AxiomC{$\myjud{\mytmm}{\mytyb}$}
638 \AxiomC{$\myjud{\mytmn}{\myapp{\mylist}{\mytya}}$}
639 \TrinaryInfC{$\myjud{\myapp{\myapp{\myapp{\myfoldr}{\mysynel{f}}}{\mytmm}}{\mytmn}}{\mytyb}$}
642 \caption{Rules for lists in the STLC.}
646 In section \ref{sec:well-order} we will see how to give a general account of
647 inductive data. %TODO does this make sense to have here?
649 \section{Intuitionistic Type Theory}
652 \subsection{Extending the STLC}
654 The STLC can be made more expressive in various ways. \cite{Barendregt1991}
655 succinctly expressed geometrically how we can add expressivity:
659 & \lambda\omega \ar@{-}[rr]\ar@{-}'[d][dd]
660 & & \lambda C \ar@{-}[dd]
662 \lambda2 \ar@{-}[ur]\ar@{-}[rr]\ar@{-}[dd]
663 & & \lambda P2 \ar@{-}[ur]\ar@{-}[dd]
665 & \lambda\underline\omega \ar@{-}'[r][rr]
666 & & \lambda P\underline\omega
668 \lambda{\to} \ar@{-}[rr]\ar@{-}[ur]
669 & & \lambda P \ar@{-}[ur]
672 Here $\lambda{\to}$, in the bottom left, is the STLC. From there can move along
675 \item[Terms depending on types (towards $\lambda{2}$)] We can quantify over
676 types in our type signatures. For example, we can define a polymorphic
679 (\myabss{\myb{A}}{\mytyp}{\myabss{\myb{x}}{\myb{A}}{\myb{x}}}) : (\myb{A} : \mytyp) \myarr \myb{A} \myarr \myb{A}
681 The first and most famous instance of this idea has been System F. This form
682 of polymorphism and has been wildly successful, also thanks to a well known
683 inference algorithm for a restricted version of System F known as
684 Hindley-Milner. Languages like Haskell and SML are based on this discipline.
685 \item[Types depending on types (towards $\lambda{\underline{\omega}}$)] We have
686 type operators. For example we could define a function that given types $R$
687 and $\mytya$ forms the type that represents a value of type $\mytya$ in
688 continuation passing style: \[\displaystyle(\myabss{\myb{A} \myar \myb{R}}{\mytyp}{(\myb{A}
689 \myarr \myb{R}) \myarr \myb{R}}) : \mytyp \myarr \mytyp \myarr \mytyp\]
690 \item[Types depending on terms (towards $\lambda{P}$)] Also known as `dependent
691 types', give great expressive power. For example, we can have values of whose
692 type depend on a boolean:
693 \[\displaystyle(\myabss{\myb{x}}{\mybool}{\myite{\myb{x}}{\mynat}{\myrat}}) : \mybool
697 All the systems preserve the properties that make the STLC well behaved. The
698 system we are going to focus on, Intuitionistic Type Theory, has all of the
699 above additions, and thus would sit where $\lambda{C}$ sits in the
700 `$\lambda$-cube'. It will serve as the logical `core' of all the other
701 extensions that we will present and ultimately our implementation of a similar
704 \subsection{A Bit of History}
706 Logic frameworks and programming languages based on type theory have a long
707 history. Per Martin-L\"{o}f described the first version of his theory in 1971,
708 but then revised it since the original version was inconsistent due to its
709 impredicativity\footnote{In the early version there was only one universe
710 $\mytyp$ and $\mytyp : \mytyp$, see section \ref{sec:term-types} for an
711 explanation on why this causes problems.}. For this reason he gave a revised
712 and consistent definition later \citep{Martin-Lof1984}.
714 A related development is the polymorphic $\lambda$-calculus, and specifically
715 the previously mentioned System F, which was developed independently by Girard
716 and Reynolds. An overview can be found in \citep{Reynolds1994}. The surprising
717 fact is that while System F is impredicative it is still consistent and strongly
718 normalising. \cite{Coquand1986} further extended this line of work with the
719 Calculus of Constructions (CoC).
721 Most widely used interactive theorem provers are based on ITT. Popular ones
722 include Agda \citep{Norell2007, Bove2009}, Coq \citep{Coq}, and Epigram
723 \citep{McBride2004, EpigramTut}.
725 \subsection{A note on inference}
727 % TODO do this, adding links to the sections about bidi type checking and
728 % implicit universes.
729 In the following text I will often omit explicit typing for abstractions or
731 Moreover, I will use $\mytyp$ without bothering to specify a
732 universe, with the silent assumption that the definition is consistent
733 regarding to the hierarchy.
735 \subsection{A simple type theory}
738 The calculus I present follows the exposition in \citep{Thompson1991},
739 and is quite close to the original formulation of predicative ITT as
740 found in \citep{Martin-Lof1984}. The system's syntax and reduction
741 rules are presented in their entirety in figure \ref{fig:core-tt-syn}.
742 The typing rules are presented piece by piece. An Agda rendition of the
743 presented theory and all the examples is reproduced in appendix
749 \begin{array}{r@{\ }c@{\ }l}
750 \mytmsyn & ::= & \myb{x} \mysynsep
752 \myunit \mysynsep \mytt \mysynsep
753 \myempty \mysynsep \myapp{\myabsurd{\mytmsyn}}{\mytmsyn} \\
754 & | & \mybool \mysynsep \mytrue \mysynsep \myfalse \mysynsep
755 \myitee{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
756 & | & \myfora{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
757 \myabss{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
758 (\myapp{\mytmsyn}{\mytmsyn}) \\
759 & | & \myexi{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
760 \mypairr{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn} \\
761 & | & \myapp{\myfst}{\mytmsyn} \mysynsep \myapp{\mysnd}{\mytmsyn} \\
762 & | & \myw{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
763 \mytmsyn \mynode{\myb{x}}{\mytmsyn} \mytmsyn \\
764 & | & \myrec{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn} \\
770 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
773 \begin{array}{l@{ }l@{\ }c@{\ }l}
774 \myitee{\mytrue &}{\myb{x}}{\myse{P}}{\mytmm}{\mytmn} & \myred & \mytmm \\
775 \myitee{\myfalse &}{\myb{x}}{\myse{P}}{\mytmm}{\mytmn} & \myred & \mytmn \\
780 \myapp{(\myabss{\myb{x}}{\mytya}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{\myb{x}}{\mytmn}
784 \begin{array}{l@{ }l@{\ }c@{\ }l}
785 \myapp{\myfst &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmm \\
786 \myapp{\mysnd &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmn
794 \myrec{(\myse{s} \mynode{\myb{x}}{\myse{T}} \myse{f})}{\myb{y}}{\myse{P}}{\myse{p}} \myred
795 \myapp{\myapp{\myapp{\myse{p}}{\myse{s}}}{\myse{f}}}{(\myabss{\myb{t}}{\mysub{\myse{T}}{\myb{x}}{\myse{s}}}{
796 \myrec{\myapp{\myse{f}}{\myb{t}}}{\myb{y}}{\myse{P}}{\mytmt}
800 \caption{Syntax and reduction rules for our type theory.}
801 \label{fig:core-tt-syn}
804 \subsubsection{Types are terms, some terms are types}
805 \label{sec:term-types}
807 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
809 \AxiomC{$\myjud{\mytmt}{\mytya}$}
810 \AxiomC{$\mytya \mydefeq \mytyb$}
811 \BinaryInfC{$\myjud{\mytmt}{\mytyb}$}
814 \AxiomC{\phantom{$\myjud{\mytmt}{\mytya}$}}
815 \UnaryInfC{$\myjud{\mytyp_l}{\mytyp_{l + 1}}$}
820 The first thing to notice is that a barrier between values and types that we had
821 in the STLC is gone: values can appear in types, and the two are treated
822 uniformly in the syntax.
824 While the usefulness of doing this will become clear soon, a consequence is
825 that since types can be the result of computation, deciding type equality is
826 not immediate as in the STLC. For this reason we define \emph{definitional
827 equality}, $\mydefeq$, as the congruence relation extending
828 $\myred$---moreover, when comparing types syntactically we do it up to
829 renaming of bound names ($\alpha$-renaming). For example under this
830 discipline we will find that
832 \myabss{\myb{x}}{\mytya}{\myb{x}} \mydefeq \myabss{\myb{y}}{\mytya}{\myb{y}}
834 Types that are definitionally equal can be used interchangeably. Here the
835 `conversion' rule is not syntax directed, however we will see how it is
836 possible to employ $\myred$ to decide term equality in a systematic
837 way. % TODO add section
838 Another thing to notice is that considering the need to reduce terms to decide
839 equality, it is essential for a dependently type system to be terminating and
840 confluent for type checking to be decidable.
842 Moreover, we specify a \emph{type hierarchy} to talk about `large' types:
843 $\mytyp_0$ will be the type of types inhabited by data: $\mybool$, $\mynat$,
844 $\mylist$, etc. $\mytyp_1$ will be the type of $\mytyp_0$, and so on---for
845 example we have $\mytrue : \mybool : \mytyp_0 : \mytyp_1 : \cdots$. Each type
846 `level' is often called a universe in the literature. While it is possible,
847 to simplify things by having only one universe $\mytyp$ with $\mytyp :
848 \mytyp$, this plan is inconsistent for much the same reason that impredicative
849 na\"{\i}ve set theory is \citep{Hurkens1995}. Moreover, various techniques
850 can be employed to lift the burden of explicitly handling universes.
851 % TODO add sectioon about universes
853 \subsubsection{Contexts}
855 \begin{minipage}{0.5\textwidth}
856 \mydesc{context validity:}{\myvalid{\myctx}}{
858 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
859 \UnaryInfC{$\myvalid{\myemptyctx}$}
862 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
863 \UnaryInfC{$\myvalid{\myctx ; \myb{x} : \mytya}$}
868 \begin{minipage}{0.5\textwidth}
869 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
870 \AxiomC{$\myctx(x) = \mytya$}
871 \UnaryInfC{$\myjud{\myb{x}}{\mytya}$}
877 We need to refine the notion context to make sure that every variable appearing
878 is typed correctly, or that in other words each type appearing in the context is
879 indeed a type and not a value. In every other rule, if no premises are present,
880 we assume the context in the conclusion to be valid.
882 Then we can re-introduce the old rule to get the type of a variable for a
885 \subsubsection{$\myunit$, $\myempty$}
887 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
889 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
890 \UnaryInfC{$\myjud{\myunit}{\mytyp_0}$}
892 \UnaryInfC{$\myjud{\myempty}{\mytyp_0}$}
895 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
896 \UnaryInfC{$\myjud{\mytt}{\myunit}$}
898 \UnaryInfC{\phantom{$\myjud{\myempty}{\mytyp_0}$}}
901 \AxiomC{$\myjud{\mytmt}{\myempty}$}
902 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
903 \BinaryInfC{$\myjud{\myapp{\myabsurd{\mytya}}{\mytmt}}{\mytya}$}
905 \UnaryInfC{\phantom{$\myjud{\myempty}{\mytyp_0}$}}
910 Nothing surprising here: $\myunit$ and $\myempty$ are unchanged from the STLC,
911 with the added rules to type $\myunit$ and $\myempty$ themselves, and to make
912 sure that we are invoking $\myabsurd{}$ over a type.
914 \subsubsection{$\mybool$, and dependent $\myfun{if}$}
916 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
919 \UnaryInfC{$\myjud{\mybool}{\mytyp_0}$}
923 \UnaryInfC{$\myjud{\mytrue}{\mybool}$}
927 \UnaryInfC{$\myjud{\myfalse}{\mybool}$}
932 \AxiomC{$\myjud{\mytmt}{\mybool}$}
933 \AxiomC{$\myjudd{\myctx : \mybool}{\mytya}{\mytyp_l}$}
935 \BinaryInfC{$\myjud{\mytmm}{\mysub{\mytya}{x}{\mytrue}}$ \hspace{0.7cm} $\myjud{\mytmn}{\mysub{\mytya}{x}{\myfalse}}$}
936 \UnaryInfC{$\myjud{\myitee{\mytmt}{\myb{x}}{\mytya}{\mytmm}{\mytmn}}{\mysub{\mytya}{\myb{x}}{\mytmt}}$}
940 With booleans we get the first taste of `dependent' in `dependent types'. While
941 the two introduction rules ($\mytrue$ and $\myfalse$) are not surprising, the
942 typing rules for $\myfun{if}$ are. In most strongly typed languages we expect
943 the branches of an $\myfun{if}$ statements to be of the same type, to preserve
944 subject reduction, since execution could take both paths. This is a pity, since
945 the type system does not reflect the fact that in each branch we gain knowledge
946 on the term we are branching on. Which means that programs along the lines of
948 if null xs then head xs else 0
950 are a necessary, well typed, danger.
952 However, in a more expressive system, we can do better: the branches' type can
953 depend on the value of the scrutinised boolean. This is what the typing rule
954 expresses: the user provides a type $\mytya$ ranging over an $\myb{x}$
955 representing the scrutinised boolean type, and the branches are typechecked with
956 the updated knowledge on the value of $\myb{x}$.
958 \subsubsection{$\myarr$, or dependent function}
960 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
961 \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
962 \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
963 \BinaryInfC{$\myjud{\myfora{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
969 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytmt}{\mytyb}$}
970 \UnaryInfC{$\myjud{\myabss{\myb{x}}{\mytya}{\mytmt}}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
973 \AxiomC{$\myjud{\mytmm}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
974 \AxiomC{$\myjud{\mytmn}{\mytya}$}
975 \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mysub{\mytyb}{\myb{x}}{\mytmn}}$}
980 Dependent functions are one of the two key features that perhaps most
981 characterise dependent types---the other being dependent products. With
982 dependent functions, the result type can depend on the value of the
983 argument. This feature, together with the fact that the result type
984 might be a type itself, brings a lot of interesting possibilities.
985 Following this intuition, in the introduction rule, the return type is
986 typechecked in a context with an abstracted variable of lhs' type, and
987 in the elimination rule the actual argument is substituted in the return
988 type. Keeping the correspondence with logic alive, dependent functions
989 are much like universal quantifiers ($\forall$) in logic.
991 For example, assuming that we have lists and natural numbers in our
992 language, using dependent functions we would be able to
995 \begin{array}{c@{\ }c@{\ }l@{\ }}
996 \myfun{length} & : & (\myb{A} {:} \mytyp_0) \myarr \myapp{\mylist}{\myb{A}} \myarr \mynat \\
997 \myarg \myfun{$>$} \myarg & : & \mynat \myarr \mynat \myarr \mytyp_0 \\
998 \myfun{head} & : & (\myb{A} {:} \mytyp_0) \myarr (\myb{l} {:} \myapp{\mylist}{\myb{A}})
999 \myarr \myapp{\myapp{\myfun{length}}{\myb{A}}}{\myb{l}} \mathrel{\myfun{>}} 0 \myarr
1004 \myfun{length} is the usual polymorphic length function. $\myfun{>}$ is
1005 a function that takes two naturals and returns a type: if the lhs is
1006 greater then the rhs, $\myunit$ is returned, $\myempty$ otherwise. This
1007 way, we can express a `non-emptyness' condition in $\myfun{head}$, by
1008 including a proof that the length of the list argument is non-zero.
1009 This allows us to rule out the `empty list' case, so that we can safely
1010 return the first element.
1012 Again, we need to make sure that the type hierarchy is respected, which is the
1013 reason why a type formed by $\myarr$ will live in the least upper bound of the
1014 levels of argument and return type. This trend will continue with the other
1015 type-level binders, $\myprod$ and $\mytyc{W}$.
1017 \subsubsection{$\myprod$, or dependent product}
1019 \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{\myexi{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
1028 \AxiomC{$\myjud{\mytmm}{\mytya}$}
1029 \AxiomC{$\myjud{\mytmn}{\mysub{\mytyb}{\myb{x}}{\mytmm}}$}
1030 \BinaryInfC{$\myjud{\mypairr{\mytmm}{\myb{x}}{\mytyb}{\mytmn}}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
1032 \UnaryInfC{\phantom{$--$}}
1035 \AxiomC{$\myjud{\mytmt}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
1036 \UnaryInfC{$\hspace{0.7cm}\myjud{\myapp{\myfst}{\mytmt}}{\mytya}\hspace{0.7cm}$}
1038 \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mysub{\mytyb}{\myb{x}}{\myapp{\myfst}{\mytmt}}}$}
1043 If dependent functions are a generalisation of $\myarr$ in the STLC,
1044 dependent products are a generalisation of $\myprod$ in the STLC. The
1045 improvement is that the second element's type can depend on the value of
1046 the first element. The corrispondence with logic is through the
1047 existential quantifier: $\exists x \in \mathbb{N}. even(x)$ can be
1048 expressed as $\myexi{\myb{x}}{\mynat}{\myapp{\myfun{even}}{\myb{x}}}$.
1049 The first element will be a number, and the second evidence that the
1050 number is even. This highlights the fact that we are working in a
1051 constructive logic: if we have an existence proof, we can always ask for
1052 a witness. This means, for instance, that $\neg \forall \neg$ is not
1053 equivalent to $\exists$.
1055 \subsubsection{$\mytyc{W}$, or well-order}
1056 \label{sec:well-order}
1058 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1059 \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
1060 \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
1061 \BinaryInfC{$\myjud{\myw{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
1066 \AxiomC{$\myjud{\mytmt}{\mytya}$}
1067 \AxiomC{$\myjud{\mysynel{f}}{\mysub{\mytyb}{\myb{x}}{\mytmt} \myarr \myw{\myb{x}}{\mytya}{\mytyb}}$}
1068 \BinaryInfC{$\myjud{\mytmt \mynode{\myb{x}}{\mytyb} \myse{f}}{\myw{\myb{x}}{\mytya}{\mytyb}}$}
1073 \AxiomC{$\myjud{\myse{u}}{\myw{\myb{x}}{\myse{S}}{\myse{T}}}$}
1074 \AxiomC{$\myjudd{\myctx; \myb{w} : \myw{\myb{x}}{\myse{S}}{\myse{T}}}{\myse{P}}{\mytyp_l}$}
1076 \BinaryInfC{$\myjud{\myse{p}}{
1077 \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}}}}
1079 \UnaryInfC{$\myjud{\myrec{\myse{u}}{\myb{w}}{\myse{P}}{\myse{p}}}{\mysub{\myse{P}}{\myb{w}}{\myse{u}}}$}
1083 \section{The struggle for equality}
1084 \label{sec:equality}
1086 In the previous section we saw how a type checker (or a human) needs a
1087 notion of \emph{definitional equality}. Beyond this meta-theoretic
1088 notion, in this section we will explore the ways of expressing equality
1089 \emph{inside} the theory, as a reasoning tool available to the user.
1090 This area is the main concern of this thesis, and in general a very
1091 active research topic, since we do not have a fully satisfactory
1092 solution, yet. As in the previous section, everything presented is
1093 formalised in Agda in appendix \ref{app:agda-code}.
1095 \subsection{Propositional equality}
1098 \begin{minipage}{0.5\textwidth}
1101 \begin{array}{r@{\ }c@{\ }l}
1102 \mytmsyn & ::= & \cdots \\
1103 & | & \mytmsyn \mypeq{\mytmsyn} \mytmsyn \mysynsep
1104 \myapp{\myrefl}{\mytmsyn} \\
1105 & | & \myjeq{\mytmsyn}{\mytmsyn}{\mytmsyn}
1110 \begin{minipage}{0.5\textwidth}
1111 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
1113 \myjeq{\myse{P}}{(\myapp{\myrefl}{\mytmm})}{\mytmn} \myred \mytmn
1119 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1120 \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
1121 \AxiomC{$\myjud{\mytmm}{\mytya}$}
1122 \AxiomC{$\myjud{\mytmn}{\mytya}$}
1123 \TrinaryInfC{$\myjud{\mytmm \mypeq{\mytya} \mytmn}{\mytyp_l}$}
1129 \AxiomC{\phantom{$\myctx P \mytyp_l$}}
1131 \UnaryInfC{$\myjud{\mytmm}{\mytya}\hspace{1.1cm}\mytmm \mydefeq \mytmn$}
1132 \UnaryInfC{$\myjud{\myapp{\myrefl}{\mytmm}}{\mytmm \mypeq{\mytya} \mytmn}$}
1135 \AxiomC{$\myjud{\myse{P}}{\myfora{\myb{x}\ \myb{y}}{\mytya}{\myfora{q}{\myb{x} \mypeq{\mytya} \myb{y}}{\mytyp_l}}}$}
1137 \UnaryInfC{$\myjud{\myse{q}}{\mytmm \mypeq{\mytya} \mytmn}\hspace{1.1cm}\myjud{\myse{p}}{\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmm}}{(\myapp{\myrefl}{\mytmm})}}$}
1138 \UnaryInfC{$\myjud{\myjeq{\myse{P}}{\myse{q}}{\myse{p}}}{\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmn}}{q}}$}
1143 To express equality between two terms inside ITT, the obvious way to do so is
1144 to have the equality construction to be a type-former. Here we present what
1145 has survived as the dominating form of equality in systems based on ITT up to
1148 Our type former is $\mypeq{\mytya}$, which given a type (in this case
1149 $\mytya$) relates equal terms of that type. $\mypeq{}$ has one introduction
1150 rule, $\myrefl$, which introduces an equality relation between definitionally
1151 equal terms---in the typing rule we display the term as `the same', meaning
1152 `the same up to $\mydefeq$'. % TODO maybe mention this earlier
1154 Finally, we have one eliminator for $\mypeq{}$, $\myjeqq$. $\myjeq{\myse{P}}{\myse{q}}{\myse{p}}$ takes
1156 \item $\myse{P}$, a predicate working with two terms of a certain type (say
1157 $\mytya$) and a proof of their equality
1158 \item $\myse{q}$, a proof that two terms in $\mytya$ (say $\myse{m}$ and
1159 $\myse{n}$) are equal
1160 \item and $\myse{p}$, an inhabitant of $\myse{P}$ applied to $\myse{m}$, plus
1161 the trivial proof by reflexivity showing that $\myse{m}$ is equal to itself
1163 Given these ingredients, $\myjeqq$ retuns a member of $\myse{P}$ applied to
1164 $\mytmm$, $\mytmn$, and $\myse{q}$. In other words $\myjeqq$ takes a
1165 witness that $\myse{P}$ works with \emph{definitionally equal} terms, and
1166 returns a witness of $\myse{P}$ working with \emph{propositionally equal}
1167 terms. Invokations of $\myjeqq$ will vanish when the equality proofs will
1168 reduce to invocations to reflexivity, at which point the arguments must be
1169 definitionally equal, and thus the provided
1170 $\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmm}}{(\myapp{\myrefl}{\mytmm})}$
1173 While the $\myjeqq$ rule is slightly convoluted, ve can derive many more
1174 `friendly' rules from it, for example a more obvious `substitution' rule, that
1175 replaces equal for equal in predicates:
1178 (\myabs{\myb{A}\ \myb{P}\ \myb{x}\ \myb{y}\ \myb{q}\ \myb{p}}{
1179 \myjeq{(\myabs{\myb{x}\ \myb{y}\ \myb{q}}{\myapp{\myb{P}}{\myb{y}}})}{\myb{q}}{\myb{p}}}) : \\
1180 \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}}}}}
1183 This rule is often called $\myfun{subst}$---here we will invoke it without
1184 specifying the type ($\myb{A}$) and the sides of the equality
1185 ($\myb{x},\myb{y}$).
1187 Once we have $\myfun{subst}$, we can easily prove more familiar laws regarding
1188 equality, such as symmetry, transitivity, and a congruence law:
1192 \subsection{Common extensions}
1200 \subsection{Limitations}
1202 \epigraph{\emph{Half of my time spent doing research involves thinking up clever
1203 schemes to avoid needing functional extensionality.}}{@larrytheliquid}
1205 However, propositional equality as described is quite restricted when
1206 reasoning about equality beyond the term structure, which is what definitional
1207 equality gives us (extension notwithstanding).
1209 The problem is best exemplified by \emph{function extensionality}. In
1210 mathematics, we would expect to be able to treat functions that give equal
1211 output for equal input as the same. When reasoning in a mechanised framework
1212 we ought to be able to do the same: in the end, without considering the
1213 operational behaviour, all functions equal extensionally are going to be
1214 replaceable with one another.
1216 However this is not the case, or in other words with the tools we have we have
1219 \myfun{ext} : \myfora{\myb{A}\ \myb{B}}{\mytyp}{\myfora{\myb{f}\ \myb{g}}{
1220 \myb{A} \myarr \myb{B}}{
1221 (\myfora{\myb{x}}{\myb{A}}{\myapp{\myb{f}}{\myb{x}} \mypeq{\myb{B}} \myapp{\myb{g}}{\myb{x}}}) \myarr
1222 \myb{f} \mypeq{\myb{A} \myarr \myb{B}} \myb{g}
1226 To see why this is the case, consider the functions
1227 \[\myabs{\myb{x}}{0 \mathrel{\myfun{+}} \myb{x}}$ and $\myabs{\myb{x}}{\myb{x} \mathrel{\myfun{+}} 0}\]
1228 where $\myfun{+}$ is defined by recursion on the first argument,
1229 gradually destructing it to build up successors of the second argument.
1230 The two functions are clearly extensionally equal, and we can in fact
1233 \myfora{\myb{x}}{\mynat}{(0 \mathrel{\myfun{+}} \myb{x}) \mypeq{\mynat} (\myb{x} \mathrel{\myfun{+}} 0)}
1235 By analysis on the $\myb{x}$. However, the two functions are not
1236 definitionally equal, and thus we won't be able to get rid of the
1239 For the reasons above, theories that offer a propositional equality similar to
1240 what we presented are called \emph{intensional}, as opposed to
1241 \emph{extensional}. Most systems in wide use today (such as Agda, Coq and
1242 Epigram) are of this kind.
1244 This is quite an annoyance that often makes reasoning awkward to execute. It
1245 also extends to other fields, for example proving bisimulation between
1246 processes specified by coinduction, or in general proving equivalences based
1247 on the behaviour on a term.
1249 \subsection{Equality reflection}
1251 One way to `solve' this problem is by identifying propositional equality with
1252 definitional equality:
1254 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1255 \AxiomC{$\myjud{\myse{q}}{\mytmm \mypeq{\mytya} \mytmn}$}
1256 \UnaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\mytya}$}
1260 This rule takes the name of \emph{equality reflection}, and is a very
1261 different rule from the ones we saw up to now: it links a typing judgement
1262 internal to the type theory to a meta-theoretic judgement that the type
1263 checker uses to work with terms. It is easy to see the dangerous consequences
1266 \item The rule is syntax directed, and the type checker is presumably expected
1267 to come up with equality proofs when needed.
1268 \item More worryingly, type checking becomes undecidable also because
1269 computing under false assumptions becomes unsafe.
1270 Consider for example
1272 \myabss{\myb{q}}{\mytya \mypeq{\mytyp} (\mytya \myarr \mytya)}{\myhole{?}}
1274 Using the assumed proof in tandem with equality reflection we could easily
1275 write a classic Y combinator, sending the compiler into a loop.
1278 Given these facts theories employing equality reflection, like NuPRL
1279 \citep{NuPRL}, carry the derivations that gave rise to each typing judgement
1280 to keep the systems manageable. % TODO more info, problems with that.
1282 For all its faults, equality reflection does allow us to prove extensionality,
1283 using the extensions we gave above. Assuming that $\myctx$ contains
1284 \[\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}}}\]
1287 \AxiomC{$\hspace{1.1cm}\myjudd{\myctx; \myb{x} : \myb{A}}{\myapp{\myb{q}}{\myb{x}}}{\myapp{\myb{f}}{\myb{x}} \mypeq{} \myapp{\myb{g}}{\myb{x}}}\hspace{1.1cm}$}
1288 \RightLabel{equality reflection}
1289 \UnaryInfC{$\myjudd{\myctx; \myb{x} : \myb{A}}{\myapp{\myb{f}}{\myb{x}} \mydefeq \myapp{\myb{g}}{\myb{x}}}{\myb{B}}$}
1290 \RightLabel{congruence for $\lambda$s}
1291 \UnaryInfC{$\myjud{(\myabs{\myb{x}}{\myapp{\myb{f}}{\myb{x}}}) \mydefeq (\myabs{\myb{x}}{\myapp{\myb{g}}{\myb{x}}})}{\myb{A} \myarr \myb{B}}$}
1292 \RightLabel{$\eta$-law for $\lambda$}
1293 \UnaryInfC{$\hspace{1.4cm}\myjud{\myb{f} \mydefeq \myb{g}}{\myb{A} \myarr \myb{B}}\hspace{1.4cm}$}
1294 \RightLabel{$\myrefl$}
1295 \UnaryInfC{$\myjud{\myapp{\myrefl}{\myb{f}}}{\myb{f} \mypeq{} \myb{g}}$}
1298 Now, the question is: do we need to give up well-behavedness of our theory to
1299 gain extensionality?
1301 \subsection{Observational equality}
1304 % TODO should we explain this in detail?
1305 A recent development by \citet{Altenkirch2007}, \emph{Observational Type
1306 Theory} (OTT), promises to keep the well behavedness of ITT while being able
1307 to gain many useful equality proofs\footnote{It is suspected that OTT gains
1308 \emph{all} the equality proofs of ETT, but no proof exists yet.}, including
1309 function extensionality. The main idea is to give the user the possibility to
1310 \emph{coerce} (or transport) values from a type $\mytya$ to a type $\mytyb$,
1311 if the type checker can prove structurally that $\mytya$ and $\mytya$ are
1312 equal; and providing a value-level equality based on similar principles. A
1313 brief overview is given below,
1316 $\mytyp_l$ is replaced by $\mytyp$. \\
1318 \begin{array}{r@{\ }c@{\ }l}
1319 \mytmsyn & ::= & \cdots \\
1320 & | & \myprdec{\myprsyn} \mysynsep
1321 \mycoee{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \mysynsep
1322 \mycohh{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
1323 \myprsyn & ::= & \mybot \mysynsep \mytop \mysynsep \myprsyn \myand \myprsyn
1324 \mysynsep \myprfora{\myb{x}}{\mytmsyn}{\myprsyn} \\\
1325 & | & \mytmsyn \myeq \mytmsyn \mysynsep
1326 \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn}
1331 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
1333 There is only $\mytyp$, which corresponds to $\mytyp_0$. \\ Thus all
1334 the type-formers take $\mytyp$ arguments and form a $\mytyp$. \\ \ \\
1336 % TODO insert large eliminator
1339 \AxiomC{$\myjud{\myse{P}}{\myprop}$}
1340 \UnaryInfC{$\myjud{\myprdec{\myse{P}}}{\mytyp}$}
1343 \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
1344 \AxiomC{$\myjud{\mytmt}{\mytya}$}
1345 \BinaryInfC{$\myjud{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}$}
1351 \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
1352 \AxiomC{$\myjud{\mytmt}{\mytya}$}
1353 \BinaryInfC{$\myjud{\mycohh{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\myprdec{\myjm{\mytmt}{\mytya}{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}}}$}
1357 \mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
1359 \AxiomC{\phantom{$\myjud{\myse{P}}{\myprop}$}}
1360 \UnaryInfC{$\myjud{\mytop}{\myprop}$}
1362 \UnaryInfC{$\myjud{\mybot}{\myprop}$}
1365 \AxiomC{$\myjud{\myse{P}}{\myprop}$}
1366 \AxiomC{$\myjud{\myse{Q}}{\myprop}$}
1367 \BinaryInfC{$\myjud{\myse{P} \myand \myse{Q}}{\myprop}$}
1369 \UnaryInfC{\phantom{$\myjud{\mybot}{\myprop}$}}
1376 \AxiomC{$\myjud{\myse{A}}{\mytyp}$}
1377 \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\myse{P}}{\myprop}$}
1378 \BinaryInfC{$\myjud{\myprfora{\myb{x}}{\mytya}{\myse{P}}}{\myprop}$}
1381 \AxiomC{$\myjud{\myse{A}}{\mytyp}$}
1382 \AxiomC{$\myjud{\myse{B}}{\mytyp}$}
1383 \BinaryInfC{$\myjud{\mytya \myeq \mytyb}{\myprop}$}
1389 \AxiomC{$\myjud{\myse{A}}{\mytyp}$}
1390 \AxiomC{$\myjud{\mytmm}{\myse{A}}$}
1391 \AxiomC{$\myjud{\myse{B}}{\mytyp}$}
1392 \AxiomC{$\myjud{\mytmn}{\myse{B}}$}
1393 \QuaternaryInfC{$\myjud{\myjm{\mytmm}{\myse{A}}{\mytmn}{\myse{B}}}{\myprop}$}
1397 \mydesc{proposition decoding:}{\myprdec{\mytmsyn} \myred \mytmsyn}{
1400 \begin{array}{l@{\ }c@{\ }l}
1401 \myprdec{\mybot} & \myred & \myempty \\
1402 \myprdec{\mytop} & \myred & \myunit
1407 \begin{array}{r@{ }c@{ }l@{\ }c@{\ }l}
1408 \myprdec{&\myse{P} \myand \myse{Q} &} & \myred & \myprdec{\myse{P}} \myprod \myprdec{\myse{Q}} \\
1409 \myprdec{&\myprfora{\myb{x}}{\mytya}{\myse{P}} &} & \myred &
1410 \myfora{\myb{x}}{\mytya}{\myprdec{\myse{P}}}
1416 \mydesc{equality reduction:}{\myprsyn \myred \myprsyn}{
1418 \begin{array}{c@{\ }c@{\ }c@{\ }l}
1419 \myempty & \myeq & \myempty & \myred \mytop \\
1420 \myunit & \myeq & \myunit & \myred \mytop \\
1421 \mybool & \myeq & \mybool & \myred \mytop \\
1422 \myexi{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myexi{\myb{x_2}}{\mytya_2}{\mytyb_2} & \myred \\
1424 \myind{2} \mytya_1 \myeq \mytyb_1 \myand
1425 \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{\myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2}} \myimpl \mytyb_1 \myeq \mytyb_2}
1427 \myfora{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myfora{\myb{x_2}}{\mytya_2}{\mytyb_2} & \myred \cdots \\
1428 \myw{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myw{\myb{x_2}}{\mytya_2}{\mytyb_2} & \myred \cdots \\
1429 \mytya & \myeq & \mytyb & \myred \mybot\ \text{for other canonical types.}
1434 \mydesc{reduction}{\mytmsyn \myred \mytmsyn}{
1436 \begin{array}{l@{\ }l@{\ }l@{\ }l@{\ }l@{\ }c@{\ }l@{\ }}
1437 \mycoe & \myempty & \myempty & \myse{Q} & \myse{t} & \myred & \myse{t} \\
1438 \mycoe & \myunit & \myunit & \myse{Q} & \mytt & \myred & \mytt \\
1439 \mycoe & \mybool & \mybool & \myse{Q} & \mytrue & \myred & \mytrue \\
1440 \mycoe & \mybool & \mybool & \myse{Q} & \myfalse & \myred & \myfalse \\
1441 \mycoe & (\myexi{\myb{x_1}}{\mytya_1}{\mytyb_1}) &
1442 (\myexi{\myb{x_2}}{\mytya_2}{\mytyb_2}) & \myse{Q} &
1445 \mycoe & (\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}) &
1446 (\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}) & \myse{Q} &
1450 \mycoe & (\myw{\myb{x_1}}{\mytya_1}{\mytyb_1}) &
1451 (\myw{\myb{x_2}}{\mytya_2}{\mytyb_2}) & \myse{Q} &
1455 \mycoe & \mytya & \mytyb & \myse{Q} & \mytmt & \myred & \myapp{\myabsurd{\mytyb}}{\myse{Q}}
1460 The original presentation of OTT employs the theory presented above. It is
1461 close to the one presented in section \ref{sec:itt}, with the additions
1462 presented above, and the change that only one the `first' universe, the type
1463 of small types ($\mytyp_0$), is present.
1465 The propositional universe is meant to be where equality proofs live in. The
1466 equality proofs are respectively between types ($\mytya = \mytyb$), and
1471 However, only one universe is present ($\mytyp_0$), and a \emph{propositional}
1472 universe is isolated, intended to be the universe where equality proofs live
1473 in. Propositions (as long as our system is consistent) are inhabited only by
1474 one element, and thus can all be treated as definitionally equal.
1478 % \section{Augmenting ITT}
1479 % \label{sec:practical}
1481 % \subsection{A more liberal hierarchy}
1483 % \subsection{Type inference}
1485 % \subsubsection{Bidirectional type checking}
1487 % \subsubsection{Pattern unification}
1489 % \subsection{Pattern matching and explicit fixpoints}
1491 % \subsection{Induction-recursion}
1493 % \subsection{Coinduction}
1495 % \subsection{Dealing with partiality}
1497 % \subsection{Type holes}
1499 \section{\mykant : the theory}
1500 \label{sec:kant-theory}
1502 \mykant\ is an interactive theorem prover developed as part of this thesis.
1503 The plan is to present a core language which would be capable of serving as
1504 the basis for a more featureful system, while still presenting interesting
1505 features and more importantly observational equality.
1507 The author learnt the hard way the implementations challenges for such a
1508 project, and while there is a solid and working base to work on, observational
1509 equality is not currently implemented. However, a detailed plan on how to add
1510 it this functionality is provided, and should not prove to be too much work.
1512 The features currently implemented in \mykant\ are:
1515 \item[Full dependent types] As we would expect, we have dependent a system
1516 which is as expressive as the `best' corner in the lambda cube described in
1517 section \ref{sec:itt}.
1519 \item[Implicit, cumulative universe hierarchy] The user does not need to
1520 specify universe level explicitly, and universes are \emph{cumulative}.
1522 \item[User defined data types and records] Instead of forcing the user to
1523 choose from a restricted toolbox, we let her define inductive data types,
1524 with associated primitive recursion operators; or records, with associated
1525 projections for each field.
1527 \item[Bidirectional type checking] While no `fancy' inference via unification
1528 is present, we take advantage of an type synthesis system in the style of
1529 \cite{Pierce2000}, extending the concept for user defined data types.
1531 \item[Type holes] When building up programs interactively, it is useful to
1532 leave parts unfinished while exploring the current context. This is what
1536 The planned features are:
1539 \item[Observational equality] As described in section \ref{sec:ott} but
1540 extended to work with the type hierarchy and to admit equality between
1541 arbitrary data types.
1543 \item[Coinductive data] ...
1546 We will analyse the features one by one, along with motivations and tradeoffs
1547 for the design decisions made.
1549 \subsection{Bidirectional type checking}
1551 We start by describing bidirectional type checking since it calls for fairly
1552 different typing rules that what we have seen up to now. The idea is to have
1553 two kind of terms: terms for which a type can always be inferred, and terms
1554 that need to be checked against a type. A nice observation is that this
1555 duality runs through the semantics of the terms: data destructors (function
1556 application, record projections, primitive re cursors) \emph{infer} types,
1557 while data constructors (abstractions, record/data types data constructors)
1558 need to be checked. In the literature these terms are respectively known as
1560 To introduce the concept and notation, we will revisit the STLC in a
1561 bidirectional style. The presentation follows \cite{Loh2010}.
1563 % TODO do this --- is it even necessary
1565 % \subsubsection{Declarations and contexts}
1567 % A \mykant declaration can be one of 4 kinds:
1569 % \begin{description}
1570 % \item[Value] A declared variable, together with a type and a body.
1571 % \item[Postulate] An abstract variable, with a type but no body.
1572 % \item[Inductive data] A datatype, with a type constructor and various data
1573 % constructors---somewhat similar to what we find in Haskell. A primitive
1574 % recursor (or `destructor') will be generated automatically.
1575 % \item[Record] A record, which consists of one data constructor and various
1576 % fields, with no recursive occurrences. We will explain the need for records
1582 \subsection{Base terms and types}
1584 Let us begin by describing the primitives available without the user defining
1585 any data types, and without equality. The syntax given here is the one of the
1586 core (`desugared') terms, and the way we handle variables and substitution is
1587 left unspecified, and explained in section \ref{sec:term-repr}, along with
1588 other implementation issues. We are also going to give an account of the
1589 implicit type hierarchy separately in section \ref{sec:term-hierarchy}, so as
1590 not to clutter derivation rules too much, and just treat types as
1591 impredicative for the time being.
1595 \begin{array}{r@{\ }c@{\ }l}
1596 \mytmsyn & ::= & \mynamesyn \mysynsep \mytyp \\
1597 & | & \myfora{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
1598 \myabss{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
1599 (\myapp{\mytmsyn}{\mytmsyn}) \mysynsep
1600 (\myann{\mytmsyn}{\mytmsyn}) \\
1601 \mynamesyn & ::= & \myb{x} \mysynsep \myfun{f}
1606 The syntax for our calculus includes just two basic constructs: abstractions
1607 and $\mytyp$s. Everything else will be provided by user-definable constructs.
1608 Since we let the user define values, we will need a context capable of
1609 carrying the body of variables along with their type. We also want to make
1610 sure not to have duplicate top names, so we enforce that.
1612 % \mytyc{D} \mysynsep \mytyc{D}.\mydc{c}
1613 % \mysynsep \mytyc{D}.\myfun{f} \mysynsep
1615 \mydesc{context validity:}{\myvalid{\myctx}}{
1616 \begin{tabular}{ccc}
1617 \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
1618 \UnaryInfC{$\myvalid{\myemptyctx}$}
1621 \AxiomC{$\myjud{\mytya}{\mytyp}$}
1622 \AxiomC{$\mynamesyn \not\in \myctx$}
1623 \BinaryInfC{$\myvalid{\myctx ; \mynamesyn : \mytya}$}
1626 \AxiomC{$\myjud{\mytmt}{\mytya}$}
1627 \AxiomC{$\myfun{f} \not\in \myctx$}
1628 \BinaryInfC{$\myvalid{\myctx ; \myfun{f} \mapsto \mytmt : \mytya}$}
1633 Now we can present the reduction rules, which are unsurprising. We have the
1634 usual functional application ($\beta$-reduction), but also a rule to replace
1635 names with their bodies, if in the context ($\delta$-reduction), and one to
1636 discard type annotations. For this reason the new reduction rules are
1637 dependent on the context:
1639 \mydesc{reduction:}{\myctx \vdash \mytmsyn \myred \mytmsyn}{
1640 \begin{tabular}{ccc}
1641 \AxiomC{\phantom{$\myb{x} \mapsto \mytmt : \mytya \in \myctx$}}
1642 \UnaryInfC{$\myctx \vdash \myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn}
1643 \myred \mysub{\mytmm}{\myb{x}}{\mytmn}$}
1646 \AxiomC{$\myfun{f} \mapsto \mytmt : \mytya \in \myctx$}
1647 \UnaryInfC{$\myctx \vdash \myfun{f} \myred \mytmt$}
1650 \AxiomC{\phantom{$\myb{x} \mapsto \mytmt : \mytya \in \myctx$}}
1651 \UnaryInfC{$\myctx \vdash \myann{\mytmm}{\mytya} \myred \mytmm$}
1656 We want to define a \emph{weak head normal form} (WHNF) for our terms, to give
1657 a syntax directed presentation of type rules with no `conversion' rule. We
1658 will consider all \emph{canonical} forms (abstractions and data constructors)
1659 to be in weak head normal form... % TODO finish
1661 We can now give types to our terms. Using our definition of WHNF, I will use
1662 $\mytmm \mynf \mytmn$ to indicate that $\mytmm$'s normal form is $\mytmn$.
1663 This way, we can avoid the non syntax-directed conversion rule, giving a more
1664 algorithmic presentation of type checking.
1666 \mydesc{typing:}{\myctx \vdash \mytmsyn \Leftrightarrow \mytmsyn}{
1667 \begin{tabular}{ccc}
1668 \AxiomC{$\myb{x} : A \in \myctx$ or $\myb{x} \mapsto \mytmt : A \in \myctx$}
1669 \UnaryInfC{$\myinf{\myb{x}}{A}$}
1672 \AxiomC{$\mychk{\mytmt}{\mytya}$}
1673 \UnaryInfC{$\myinf{\myann{\mytmt}{\mytya}}{\mytya}$}
1678 \AxiomC{$\myinf{\mytmm}{\mytya}$}
1679 \AxiomC{$\myctx \vdash \mytya \mynf \myfora{\myb{x}}{\mytyb}{\myse{C}}$}
1680 \AxiomC{$\mychk{\mytmn}{\mytyb}$}
1681 \TrinaryInfC{$\myinf{\myapp{\mytmm}{\mytmn}}{\mysub{\myse{C}}{\myb{x}}{\mytmn}}$}
1686 \AxiomC{$\myctx \vdash \mytya \mynf \myfora{\myb{x}}{\mytyb}{\myse{C}}$}
1687 \AxiomC{$\mychkk{\myctx; \myb{x}: \mytyb}{\mytmt}{\myse{C}}$}
1688 \BinaryInfC{$\mychk{\myabs{\myb{x}}{\mytmt}}{\mytya}$}
1692 \subsection{Elaboration}
1696 \begin{array}{r@{\ }c@{\ }l}
1697 \mydeclsyn & ::= & \myval{\myb{x}}{\mytmsyn}{\mytmsyn} \\
1698 & | & \mypost{\myb{x}}{\mytmsyn} \\
1699 & | & \myadt{\mytyc{D}}{\mytelesyn}{}{\mydc{c} : \mytelesyn\ |\ \cdots } \\
1700 & | & \myreco{\mytyc{D}}{\mytelesyn}{}{\myfun{f} : \mytmsyn,\ \cdots } \\
1702 \mytelesyn & ::= & \myemptytele \mysynsep \mytelesyn \mycc (\myb{x} {:} \mytmsyn)
1707 \mydesc{typing:}{\myctx \vdash \mytmsyn \Leftrightarrow \mytmsyn}{
1711 \subsubsection{Values and postulated variables}
1713 As mentioned, in \mykant\ we can defined top level variables, with or without
1714 a body. We call the variables
1716 \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
1718 \AxiomC{$\myjud{\mytmt}{\mytya}$}
1719 \AxiomC{$\myfun{f} \not\in \myctx$}
1721 $\myctx \myelabt \myval{\myfun{f}}{\mytya}{\mytmt} \ \ \myelabf\ \ \myctx; \myfun{f} \mapsto \mytmt : \mytya$
1725 \AxiomC{$\myjud{\mytya}{\mytyp}$}
1726 \AxiomC{$\myfun{f} \not\in \myctx$}
1729 \myctx \myelabt \mypost{\myfun{f}}{\mytya}
1730 \ \ \myelabf\ \ \myctx; \myfun{f} : \mytya
1737 \subsubsection{User defined types}
1742 \mynamesyn ::= \cdots \mysynsep \mytyc{D} \mysynsep \mytyc{D}.\mydc{c} \mysynsep \mytyc{D}.\myfun{f}
1747 \mydesc{typing:}{ }{
1748 \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
1749 \AxiomC{$\mytyc{D}.\mydc{c} : \mytele \mycc \mytele' \myarr
1750 \myapp{\mytyc{D}}{\mytelee} \in \myctx$}
1751 \BinaryInfC{$\mychk{\myapp{\mytyc{D}.\mydc{c}}{\vec{t}}}{\myapp{\mytyc{D}}{\vec{A}}}$}
1757 \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
1758 \AxiomC{$\mytyc{D}.\myfun{f} : \mytele \myarr
1759 \myapp{\mytyc{D}}{\mytelee} \myarr \myse{F}$}
1760 \AxiomC{$\myjud{\mytmt}{\myapp{\mytyc{D}}{\vec{A}}}$}
1761 \TrinaryInfC{$\myinf{\myapp{\mytyc{D}.\myfun{f}}{\mytmt}}{TODO}$}
1765 \subsubsection{Data types}
1768 \mydesc{syntax elaboration:}{\mydeclsyn \myelabf \mytmsyn ::= \cdots}{
1770 \begin{array}{r@{\ }l}
1771 & \myadt{\mytyc{D}}{\mytele}{}{\cdots\ |\ \mydc{c}_n : \myvec{(\myb{x} {:} \mytya)} \ |\ \cdots } \\
1774 \begin{array}{r@{\ }c@{\ }l}
1775 \mytmsyn & ::= & \cdots \mysynsep \myapp{\mytyc{D}}{\myvec{\mytmsyn}} \mysynsep
1776 \mytyc{D}.\mydc{c}_n \myappsp \myvec{\mytmsyn} \mysynsep \cdots \mysynsep \mytyc{D}.\myfun{elim} \myappsp \mytmsyn \\
1782 \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
1783 \AxiomC{$\myinf{\mytele \myarr \mytyp}{\mytyp}$}
1784 \AxiomC{$\mytyc{D} \not\in \myctx$}
1786 \BinaryInfC{$\myinff{\myctx;\ \mytyc{D} : \mytele \myarr \mytyp}{\mytele \mycc \mytele_i \myarr \myapp{\mytyc{D}}{\mytelee}}{\mytyp}\ \ \ (1 \leq i \leq n)$}
1788 \UnaryInfC{For each $(\myb{x} {:} \mytya)$ in each $\mytele_i$, if $\mytyc{D} \in \mytya$, then $\mytya = \myapp{\mytyc{D}}{\vec{\mytmt}}$.}
1790 \begin{array}{r@{\ }c@{\ }l}
1791 \myctx & \myelabt & \myadt{\mytyc{D}}{\mytele}{}{ \mydc{c} : \mytele_1 \ |\ \cdots \ |\ \mydc{c}_n : \mytele_n } \\
1792 & & \vspace{-0.2cm} \\
1793 & \myelabf & \myctx;\ \mytyc{D} : \mytele \mycc \mytyp;\ \mytyc{D}.\mydc{c}_1 : \mytele \mycc \mytele_1 \myarr \myapp{\mytyc{D}}{\mytelee};\ \cdots;\ \mytyc{D}.\mydc{c}_n : \mytele \mycc \mytele_n \myarr \myapp{\mytyc{D}}{\mytelee}; \\
1795 \begin{array}{@{}r@{\ }l l}
1796 \mytyc{D}.\myfun{elim} : & \mytele \myarr (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr & \textbf{target} \\
1797 & (\myb{P} {:} \myapp{\mytyc{D}}{\mytelee} \myarr \mytyp) \myarr & \textbf{motive} \\
1800 (\mytele_1 \mycc \myhyps(\myb{P}, \mytele_1) \myarr \myapp{\myb{P}}{(\myapp{\mytyc{D}.\mydc{c}_1}{\mytelee_1})}) \myarr \\
1802 (\mytele_n \mycc \myhyps(\myb{P}, \mytele_n) \myarr \myapp{\myb{P}}{(\myapp{\mytyc{D}.\mydc{c}_n}{\mytelee_n})}) \myarr
1803 \end{array} \right \}
1804 & \textbf{methods} \\
1805 & \myapp{\myb{P}}{\myb{x}} &
1809 \begin{array}{@{}l l@{\ } l@{} r c l}
1810 \textbf{where} & \myhyps(\myb{P}, & \myemptytele &) & \mymetagoes & \myemptytele \\
1811 & \myhyps(\myb{P}, & (\myb{r} {:} \myapp{\mytyc{D}}{\vec{\mytmt}}) \mycc \mytele &) & \mymetagoes & (\myb{r'} {:} \myapp{\myb{P}}{\myb{r}}) \mycc \myhyps(\myb{P}, \mytele) \\
1812 & \myhyps(\myb{P}, & (\myb{x} {:} \mytya) \mycc \mytele & ) & \mymetagoes & \myhyps(\myb{P}, \mytele)
1820 \mydesc{reduction elaboration:}{\mydeclsyn \myelabf \myctx \vdash \mytmsyn \myred \mytmsyn}{
1821 \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
1822 \AxiomC{$\mytyc{D}.\mydc{c}_i : \mytele;\mytele_i \myarr \myapp{\mytyc{D}}{\mytelee} \in \myctx$}
1825 \myctx \vdash \myapp{\myapp{\myapp{\mytyc{D}.\myfun{elim}}{(\myapp{\mytyc{D}.\mydc{c}_i}{\vec{\myse{t}}})}}{\myse{P}}}{\vec{\myse{m}}} \myred \myapp{\myapp{\myse{m}_i}{\vec{\mytmt}}}{\myrecs(\myse{P}, \vec{m}, \mytele_i)} \\ \\
1826 \begin{array}{@{}l l@{\ } l@{} r c l}
1827 \textbf{where} & \myrecs(\myse{P}, \vec{m}, & \myemptytele &) & \mymetagoes & \myemptytele \\
1828 & \myrecs(\myse{P}, \vec{m}, & (\myb{r} {:} \myapp{\mytyc{D}}{\vec{A}}); \mytele & ) & \mymetagoes & (\mytyc{D}.\myfun{elim} \myappsp \myb{r} \myappsp \myse{P} \myappsp \vec{m}); \myrecs(\myse{P}, \vec{m}, \mytele) \\
1829 & \myrecs(\myse{P}, \vec{m}, & (\myb{x} {:} \mytya); \mytele &) & \mymetagoes & \myrecs(\myse{P}, \vec{m}, \mytele)
1836 \caption{Elaborations for data types.}
1837 \label{fig:elab-adt}
1841 \subsubsection{Records}
1844 \mydesc{syntax elaboration:}{\myelab{\mydeclsyn}{\mytmsyn ::= \cdots}}{
1846 \begin{array}{r@{\ }c@{\ }l}
1847 \myctx & \myelabt & \myadt{\mytyc{D}}{\mytele}{}{\cdots\ |\ \mydc{c}_n : \myvec{(\myb{x} {:} \mytya)} \ |\ \cdots } \\
1850 \begin{array}{r@{\ }c@{\ }l}
1851 \mytmsyn & ::= & \cdots \mysynsep \myapp{\mytyc{D}}{\myvec{\mytmsyn}} \mysynsep
1852 \mytyc{D}.\mydc{c}_n \myappsp \myvec{\mytmsyn} \mysynsep \cdots \mysynsep \mytyc{D}.\myfun{elim} \myappsp \mytmsyn \\
1859 \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
1860 \AxiomC{$\myinf{\mytele \myarr \mytyp}{\mytyp}$}
1861 \AxiomC{$\mytyc{D} \not\in \myctx$}
1863 \BinaryInfC{$\myinff{\myctx; \mytele; (\myb{f}_j : \myse{F}_j)_{j=1}^{i - 1}}{F_i}{\mytyp} \myind{3} (1 \le i \le n)$}
1865 \begin{array}{r@{\ }c@{\ }l}
1866 \myctx & \myelabt & \myreco{\mytyc{D}}{\mytele}{}{ \myfun{f}_1 : \myse{F}_1, \cdots, \myfun{f}_n : \myse{F}_n } \\
1867 & & \vspace{-0.2cm} \\
1868 & \myelabf & \myctx;\ \mytyc{D} : \mytele \myarr \mytyp;\\
1869 & & \mytyc{D}.\myfun{f}_1 : \mytele \myarr \myapp{\mytyc{D}}{\mytelee} \myarr \myse{F}_1;\ \cdots;\ \mytyc{D}.\myfun{f}_n : \mytele \myarr (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr \mysub{\myse{F}_n}{\myb{f}_i}{\myapp{\myfun{f}_i}{\myb{x}}}_{i = 1}^{n-1}; \\
1870 & & \mytyc{D}.\mydc{constr} : \mytele \myarr \myse{F}_1 \myarr \cdots \myarr \myse{F}_n \myarr \myapp{\mytyc{D}}{\mytelee};
1876 \mydesc{reduction elaboration:}{\mydeclsyn \myelabf \myctx \vdash \mytmsyn \myred \mytmsyn}{
1877 \AxiomC{$\mytyc{D} \in \myctx$}
1878 \UnaryInfC{$\myctx \vdash \myapp{\mytyc{D}.\myfun{f}_i}{(\mytyc{D}.\mydc{constr} \myappsp \vec{t})} \myred t_i$}
1882 \caption{Elaborations for records.}
1883 \label{fig:elab-adt}
1887 \subsection{Type hierarchy}
1888 \label{sec:term-hierarchy}
1890 \subsection{Observational equality, \mykant\ style}
1894 \begin{array}{r@{\ }c@{\ }l}
1895 \mytmsyn & ::= & \mytmsyn \myeq \mytmsyn \mysynsep \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
1896 & | & \mycoee{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \mysynsep
1897 \mycohh{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn}
1902 \section{\mykant : The practice}
1903 \label{sec:kant-practice}
1905 The codebase consists of around 2500 lines of Haskell, as reported by the
1906 \texttt{cloc} utility. The high level design is heavily inspired by Conor
1907 McBride's work on various incarnations of Epigram, and specifically by the
1908 first version as described \citep{McBride2004} and the codebase for the new
1909 version \footnote{Available intermittently as a \texttt{darcs} repository at
1910 \url{http://sneezy.cs.nott.ac.uk/darcs/Pig09}.}. In many ways \mykant\ is
1911 something in between the first and second version of Epigram.
1913 The interaction happens in a read-eval-print loop (REPL). The repl is a
1914 available both as a commandline application and in a web interface, which is
1915 available at \url{kant.mazzo.li} and presents itself as in figure
1920 \includegraphics[scale=1.0]{kant-web.png}
1922 \caption{The \mykant\ web prompt.}
1923 \label{fig:kant-web}
1926 The interaction with the user takes place in a loop living in and updating a
1927 context \mykant\ declarations. The user inputs a new declaration that goes
1928 through various stages starts with the user inputing a \mykant\ declaration or
1929 another REPL command, which then goes through various stages that can end up
1930 in a context update, or in failures of various kind. The process is described
1931 diagrammatically in figure \ref{fig:kant-process}:
1934 \item[Parse] In this phase the text input gets converted to a sugared
1935 version of the core language.
1937 \item[Desugar] The sugared declaration is converted to a core term.
1939 \item[Reference] Occurrences of $\mytyp$ get decorated by a unique reference,
1940 which is necessary to implement the type hierarchy check.
1942 \item[Elaborate] Convert the declaration to some context item, which might be
1943 a value declaration (type and body) or a data type declaration (constructors
1944 and destructors). This phase works in tandem with \textbf{Typechecking},
1945 which in turns needs to \textbf{Evaluate} terms.
1947 \item[Distill] and report the result. `Distilling' refers to the process of
1948 converting a core term back to a sugared version that the user can
1949 visualise. This can be necessary both to display errors including terms or
1950 to display result of evaluations or type checking that the user has
1953 \item[Pretty print] Format the terms in a nice way, and display the result to
1958 The details of each phase will be described in section % TODO insert section
1962 \tikzstyle{block} = [rectangle, draw, text width=5em, text centered, rounded
1963 corners, minimum height=2.5em, node distance=0.7cm]
1965 \tikzstyle{decision} = [diamond, draw, text width=4.5em, text badly
1966 centered, inner sep=0pt, node distance=0.7cm]
1968 \tikzstyle{line} = [draw, -latex']
1970 \tikzstyle{cloud} = [draw, ellipse, minimum height=2em, text width=5em, text
1971 centered, node distance=1.5cm]
1974 \begin{tikzpicture}[auto]
1975 \node [cloud] (user) {User};
1976 \node [block, below left=1cm and 0.1cm of user] (parse) {Parse};
1977 \node [block, below=of parse] (desugar) {Desugar};
1978 \node [block, below=of desugar] (reference) {Reference};
1979 \node [block, below=of reference] (elaborate) {Elaborate};
1980 \node [block, left=of elaborate] (tycheck) {Typecheck};
1981 \node [block, left=of tycheck] (evaluate) {Evaluate};
1982 \node [decision, right=of elaborate] (error) {Error?};
1983 \node [block, right=of parse] (distill) {Distill};
1984 \node [block, right=of desugar] (update) {Update context};
1986 \path [line] (user) -- (parse);
1987 \path [line] (parse) -- (desugar);
1988 \path [line] (desugar) -- (reference);
1989 \path [line] (reference) -- (elaborate);
1990 \path [line] (elaborate) edge[bend right] (tycheck);
1991 \path [line] (tycheck) edge[bend right] (elaborate);
1992 \path [line] (elaborate) -- (error);
1993 \path [line] (error) edge[out=0,in=0] node [near start] {yes} (distill);
1994 \path [line] (error) -- node [near start] {no} (update);
1995 \path [line] (update) -- (distill);
1996 \path [line] (distill) -- (user);
1997 \path [line] (tycheck) edge[bend right] (evaluate);
1998 \path [line] (evaluate) edge[bend right] (tycheck);
2001 \caption{High level overview of the life of a \mykant\ prompt cycle.}
2002 \label{fig:kant-process}
2005 \subsection{Term representation}
2006 \label{sec:term-repr}
2008 \subsection{Type hierarchy}
2010 \subsection{Elaboration}
2012 \section{Evaluation}
2014 \section{Future work}
2018 \section{Notation and syntax}
2020 Syntax, derivation rules, and reduction rules, are enclosed in frames describing
2021 the type of relation being established and the syntactic elements appearing,
2024 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
2025 Typing derivations here.
2028 In the languages presented and Agda code samples I also highlight the syntax,
2029 following a uniform color and font convention:
2032 \begin{tabular}{c | l}
2033 $\mytyc{Sans}$ & Type constructors. \\
2034 $\mydc{sans}$ & Data constructors. \\
2035 % $\myfld{sans}$ & Field accessors (e.g. \myfld{fst} and \myfld{snd} for products). \\
2036 $\mysyn{roman}$ & Keywords of the language. \\
2037 $\myfun{roman}$ & Defined values and destructors. \\
2038 $\myb{math}$ & Bound variables.
2042 Moreover, I will from time to time give examples in the Haskell programming
2043 language as defined in \citep{Haskell2010}, which I will typeset in
2044 \texttt{teletype} font. I assume that the reader is already familiar with
2045 Haskell, plenty of good introductions are available \citep{LYAH,ProgInHask}.
2047 When presenting grammars, I will use a word in $\mysynel{math}$ font
2048 (e.g. $\mytmsyn$ or $\mytysyn$) to indicate indicate nonterminals. Additionally,
2049 I will use quite flexibly a $\mysynel{math}$ font to indicate a syntactic
2050 element. More specifically, terms are usually indicated by lowercase letters
2051 (often $\mytmt$, $\mytmm$, or $\mytmn$); and types by an uppercase letter (often
2052 $\mytya$, $\mytyb$, or $\mytycc$).
2054 When presenting type derivations, I will often abbreviate and present multiple
2055 conclusions, each on a separate line:
2058 \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
2059 \UnaryInfC{$\myjud{\myapp{\myfst}{\mytmt}}{\mytya}$}
2061 \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mytyb}$}
2064 \section{Agda rendition of ITT}
2065 \label{app:agda-itt}
2067 Note that in what follows rules for `base' types are
2068 universe-polymorphic, to reflect the exposition. Derived definitions,
2069 on the other hand, mostly work with \mytyc{Set}, reflecting the fact
2070 that in the theory presented we don't have universe polymorphism.
2076 data Empty : Set where
2078 absurd : ∀ {a} {A : Set a} → Empty → A
2081 ¬_ : ∀ {a} → (A : Set a) → Set a
2084 record Unit : Set where
2087 record _×_ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
2093 data Bool : Set where
2096 if_then_else_ : ∀ {a} {P : Bool → Set a} (x : Bool) → P true → P false → P x
2097 if true then x else _ = x
2098 if false then _ else x = x
2100 data W {s p} (S : Set s) (P : S → Set p) : Set (s ⊔ p) where
2101 _◁_ : (s : S) → (P s → W S P) → W S P
2103 rec : ∀ {a b} {S : Set a} {P : S → Set b}
2104 (C : W S P → Set) → -- some conclusion we hope holds
2105 ((s : S) → -- given a shape...
2106 (f : P s → W S P) → -- ...and a bunch of kids...
2107 ((p : P s) → C (f p)) → -- ...and C for each kid in the bunch...
2108 C (s ◁ f)) → -- ...does C hold for the node?
2109 (x : W S P) → -- If so, ...
2110 C x -- ...C always holds.
2111 rec C c (s ◁ f) = c s f (λ p → rec C c (f p))
2113 module Examples-→ where
2120 -- These pragmas are needed so we can use number literals.
2121 {-# BUILTIN NATURAL ℕ #-}
2122 {-# BUILTIN ZERO zero #-}
2123 {-# BUILTIN SUC suc #-}
2125 data List (A : Set) : Set where
2127 _∷_ : A → List A → List A
2129 length : ∀ {A} → List A → ℕ
2131 length (_ ∷ l) = suc (length l)
2136 suc x > suc y = x > y
2138 head : ∀ {A} → (l : List A) → length l > 0 → A
2139 head [] p = absurd p
2142 module Examples-× where
2148 even (suc zero) = Empty
2149 even (suc (suc n)) = even n
2154 5-is-not-even : ¬ (even 5)
2155 5-is-not-even = absurd
2157 there-is-an-even-number : ℕ × even
2158 there-is-an-even-number = 6 , 6-is-even
2160 module Equality where
2163 data _≡_ {a} {A : Set a} : A → A → Set a where
2166 ≡-elim : ∀ {a b} {A : Set a}
2167 (P : (x y : A) → x ≡ y → Set b) →
2168 ∀ {x y} → P x x (refl x) → (x≡y : x ≡ y) → P x y x≡y
2169 ≡-elim P p (refl x) = p
2171 subst : ∀ {A : Set} (P : A → Set) → ∀ {x y} → (x≡y : x ≡ y) → P x → P y
2172 subst P x≡y p = ≡-elim (λ _ y _ → P y) p x≡y
2174 sym : ∀ {A : Set} (x y : A) → x ≡ y → y ≡ x
2175 sym x y p = subst (λ y′ → y′ ≡ x) p (refl x)
2177 trans : ∀ {A : Set} (x y z : A) → x ≡ y → y ≡ z → x ≡ z
2178 trans x y z p q = subst (λ z′ → x ≡ z′) q p
2180 cong : ∀ {A B : Set} (x y : A) → x ≡ y → (f : A → B) → f x ≡ f y
2181 cong x y p f = subst (λ y′ → f x ≡ f y′) p (refl (f x))
2185 \bibliographystyle{authordate1}
2186 \bibliography{thesis}