1 \documentclass[article, a4paper]{article}
2 \usepackage[T1]{fontenc}
5 \usepackage[normalem]{ulem}
7 \usepackage{subcaption}
11 \usepackage[utf8x]{inputenc}
14 %% -----------------------------------------------------------------------------
16 %% \usepackage[osf]{libertine}
17 %% \usepackage{helvet}
18 %% \usepackage{lmodern}
19 %% \IfFileExists{microtype.sty}{\usepackage{microtype}}{}
21 %% -----------------------------------------------------------------------------
24 % \usetikzlibrary{positioning}
25 %% \usetikzlibrary{shapes}
26 %% \usetikzlibrary{arrows}
27 %% \usepackage{tikz-cd}
28 %% \usepackage{pgfplots}
31 %% -----------------------------------------------------------------------------
33 \usepackage[fleqn]{amsmath}
36 \usepackage{turnstile}
37 \usepackage{centernot}
39 %% -----------------------------------------------------------------------------
41 \usepackage{bussproofs}
43 \usepackage[export]{adjustbox}
45 \usepackage{listingsutf8}
47 basicstyle=\small\ttfamily,
54 %% -----------------------------------------------------------------------------
59 %% \setcounter{secnumdepth}{0}
61 %% -----------------------------------------------------------------------------
62 % We will generate all images so they have a width \maxwidth. This means
63 % that they will get their normal width if they fit onto the page, but
64 % are scaled down if they would overflow the margins.
67 \ifdim\Gin@nat@width>\linewidth\linewidth
68 \else\Gin@nat@width\fi
72 %% -----------------------------------------------------------------------------
75 setpagesize=false, % page size defined by xetex
76 unicode=false, % unicode breaks when used with xetex
83 pdfauthor={Francesco Mazzoli <fm2209@ic.ac.uk>},
84 pdftitle={Observational Equality},
89 % Make links footnotes instead of hotlinks:
90 % \renewcommand{\href}[2]{#2\footnote{\url{#1}}}
92 % avoid problems with \sout in headers with hyperref:
93 \pdfstringdefDisableCommands{\renewcommand{\sout}{}}
95 \title{Observational Equality}
96 \author{Francesco Mazzoli \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{<fm2209@ic.ac.uk>}}}
103 \setlength{\tabcolsep}{12pt}
106 The marriage between programming and logic has been a very fertile one. In
107 particular, since the simply typed lambda calculus (STLC), a number of type
108 systems have been devised with increasing expressive power.
110 Section \ref{sec:types} I will give a very brief overview of STLC, and then
111 illustrate how it can be interpreted as a natural deduction system. Section
112 \ref{sec:itt} will introduce Inutitionistic Type Theory (ITT), which expands on
113 this concept, employing a more expressive logic. The exposition is quite dense
114 since there is a lot of material to cover; for a more complete treatment of the
115 material the reader can refer to \citep{Thompson1991, Pierce2002}. Section
116 \ref{sec:practical} will describe additions common in practical programming
117 languages based on ITT.
119 Finally, I will explain why equality has been a tricky business in these
120 theories, and talk about the various attempts have been made to make the
121 situation better. One interesting development has recently emerged:
122 Observational Type theory. I propose to explore the ways to turn these ideas
123 into useful practices for programming and theorem proving.
128 \section{Simple and not-so-simple types}
131 \subsection{A note on notation}
133 \newcommand{\appsp}{\hspace{0.07cm}}
134 \newcommand{\app}[2]{#1\appsp#2}
135 \newcommand{\absspace}{\hspace{0.03cm}}
136 \newcommand{\abs}[2]{\lambda #1\absspace.\absspace#2}
137 \newcommand{\termt}{t}
138 \newcommand{\termm}{m}
139 \newcommand{\termn}{n}
140 \newcommand{\termp}{p}
141 \newcommand{\termf}{f}
142 \newcommand{\separ}{\ \ |\ \ }
143 \newcommand{\termsyn}{\mathit{term}}
144 \newcommand{\axname}[1]{\textbf{#1}}
145 \newcommand{\axdesc}[2]{\axname{#1} \fbox{$#2$}}
146 \newcommand{\lcsyn}[1]{\mathrm{\underline{#1}}}
147 \newcommand{\lccon}[1]{\mathsf{#1}}
148 \newcommand{\lcfun}[1]{\mathbf{#1}}
149 \newcommand{\tyarr}{\to}
150 \newcommand{\tysyn}{\mathit{type}}
151 \newcommand{\ctxsyn}{\mathit{context}}
152 \newcommand{\emptyctx}{\cdot}
154 In the following sections I will introduce a lot of syntax, typing, and
155 reduction rules, along with examples. To make the exposition clearer, usually
156 the rules are preceded by what the rule looks like and what it shows (for
157 example \axdesc{typing}{\Gamma \vdash \termsyn : \tysyn}).
159 In the languages presented I will also use different fonts for different things:
160 \begin{tabular}{c | l}
161 $\lccon{Sans}$ & Sans serif, capitalised, for type constructors. \\
162 $\lccon{sans}$ & Sans serif, not capitalised, for data constructors. \\
163 $\lcsyn{roman}$ & Roman, underlined, for the syntax of the language. \\
164 $\lcfun{roman}$ & Roman, bold, for defined functions and values. \\
165 $math$ & Math mode font for quantified variables and syntax elements.
168 Moreover, I will from time to time give examples in the Haskell programming
169 language as defined in \citep{Haskell2010}, which I will typeset in
170 \texttt{typewriter} font. I assume that the reader is already familiar with
171 Haskell, plenty of good introductions are available \citep{LYAH,ProgInHask}.
173 \subsection{Untyped $\lambda$-calculus}
175 Along with Turing's machines, the earliest attempts to formalise computation
176 lead to the $\lambda$-calculus \citep{Church1936}. This early programming
177 language encodes computation with a minimal syntax and no `data' in the
178 traditional sense, but just functions.
180 The syntax of $\lambda$-terms consists of just three things: variables,
181 abstractions, and applications:
187 \termsyn & ::= & x \separ (\abs{x}{\termsyn}) \separ (\app{\termsyn}{\termsyn}) \\
188 x & \in & \text{Some enumerable set of symbols, e.g.}\ \{x, y, z, \dots , x_1, x_2, \dots\}
194 % I will omit parethesis in the usual manner. %TODO explain how
196 I will use $\termt,\termm,\termn,\dots$ to indicate a generic term, and $x,y$
197 for variables. I will also assume that all variable names in a term are unique
198 to avoid problems with name capturing. Intuitively, abstractions
199 ($\abs{x}{\termt}$) introduce functions with a named parameter ($x$), and
200 applications ($\app{\termt}{\termm}$) apply a function ($\termt$) to an argument
203 The `applying' is more formally explained with a reduction rule:
205 \newcommand{\bred}{\leadsto}
206 \newcommand{\bredc}{\bred^*}
209 \axdesc{reduction}{\termsyn \bred \termsyn}
210 $$\app{(\abs{x}{\termt})}{\termm} \bred \termt[\termm / x]$$
213 Where $\termt[\termm / x]$ expresses the operation that substitutes all
214 occurrences of $x$ with $\termm$ in $\termt$. In the future, I will use
215 $[\termt]$ as an abbreviation for $[\termt / x]$. In the systems presented, the
216 $\bred$ relation also includes reduction of subterms, for example if $\termt
217 \bred \termm$ then $\app{\termt}{\termn} \bred \app{\termm}{\termn}$, and so on.
219 These few elements are of remarkable expressiveness, and in fact Turing
220 complete. As a corollary, we must be able to devise a term that reduces forever
221 (`loops' in imperative terms):
223 \app{(\abs{x}{\app{x}{x}})}{(\abs{x}{\app{x}{x}})} \bred \app{(\abs{x}{\app{x}{x}})}{(\abs{x}{\app{x}{x}})} \bred \dotsb
225 Terms that can be reduced only a finite number of times (the non-looping ones)
226 are said to be \emph{normalising}, and the `final' term (where no reductions are
227 possible on the term or on its subterms) is called \emph{normal form}.
229 \subsection{The simply typed $\lambda$-calculus}
235 One way to `discipline' $\lambda$-terms is to assign \emph{types} to them, and
236 then check that the terms that we are forming make sense given our typing rules
239 We wish to introduce rules of the form $\Gamma \vdash \termt : \tya$, which
240 reads `in context $\Gamma$, term $\termt$ has type $\tya$'.
242 The syntax for types is as follows:
246 $$\tysyn ::= x \separ \tysyn \tyarr \tysyn$$
249 I will use $\tya,\tyb,\dots$ to indicate a generic type.
251 A context $\Gamma$ is a map from variables to types. I will use the notation
252 $\Gamma; x : \tya$ to augment it and to `extract' pairs from it.
254 Predictably, $\tya \tyarr \tyb$ is the type of a function from $\tya$ to
255 $\tyb$. We need to be able to decorate our abstractions with
256 types\footnote{Actually, we don't need to: computers can infer the right type
257 easily, but that is another story.}:
260 $$\termsyn ::= x \separ (\abs{x : \tysyn}{\termsyn}) \separ (\app{\termsyn}{\termsyn})$$
262 Now we are ready to give the typing judgements:
265 \axdesc{typing}{\Gamma \vdash \termsyn : \tysyn}
269 \begin{tabular}{c c c}
270 \AxiomC{\phantom{1em}}
271 \UnaryInfC{$\Gamma; x : \tya \vdash x : \tya$}
274 \AxiomC{$\Gamma; x : \tya \vdash \termt : \tyb$}
275 \UnaryInfC{$\Gamma \vdash \abs{x : \tya}{\termt} : \tya \tyarr \tyb$}
282 \AxiomC{$\Gamma \vdash \termt : \tya \tyarr \tyb$}
283 \AxiomC{$\Gamma \vdash \termm : \tya$}
284 \BinaryInfC{$\Gamma \vdash \app{\termt}{\termm} : \tyb$}
289 This typing system takes the name of `simply typed lambda calculus' (STLC),
290 and enjoys a number of properties. Two of them are expected in most type
291 systems \citep{Pierce2002}:
293 \item[Progress] A well-typed term is not stuck - either it is a value or it can
294 take a step according to the evaluation rules. With `value' we mean a term
295 whose subterms (including itself) don't appear to the left of the $\bred$
297 \item[Preservation] If a well-typed term takes a step of evaluation, then the
298 resulting term is also well typed.
301 However, STLC buys us much more: every well-typed term
302 is normalising. It is easy to see that we can't fill the blanks if we want to
303 give types to the non-normalising term shown before:
305 \app{(\abs{x : ?}{\app{x}{x}})}{(\abs{x : ?}{\app{x}{x}})}
308 \newcommand{\lcfix}[2]{\lcsyn{fix} \appsp #1\absspace.\absspace #2}
310 This makes the STLC Turing incomplete. We can recover the ability to loop by
311 adding a combinator that recurses:
313 \termsyn ::= \dotsb \separ \lcfix{x : \tysyn}{\termsyn}
317 \AxiomC{$\Gamma;x : \tya \vdash \termt : \tya$}
318 \UnaryInfC{$\Gamma \vdash \lcfix{x : \tya}{\termt} : \tya$}
322 \lcfix{x : \tya}{\termt} \bred \termt[\lcfix{x : \tya}{\termt}]
324 Which will deprive us of normalisation. There is however a price to pay, which
325 will be made clear in the next section.
327 \subsection{The Curry-Howard correspondence}
328 \label{sec:curry-howard}
330 \newcommand{\lcunit}{\lcfun{\langle\rangle}}
332 It turns out that the STLC can be seen a natural deduction system for
333 propositional logic. Terms are proofs, and their types are the propositions
334 they prove. This remarkable fact is known as the Curry-Howard correspondence,
337 The `arrow' ($\to$) type corresponds to implication. If we wish to prove that
338 $(\tya \tyarr \tyb) \tyarr (\tyb \tyarr \tyc) \tyarr (\tya \tyarr \tyc)$, all we
339 need to do is to devise a $\lambda$-term that has the correct type:
341 \abs{f : (\tya \tyarr \tyb)}{\abs{g : (\tyb \tyarr \tyc)}{\abs{x : \tya}{\app{g}{(\app{f}{x})}}}}
343 That is, function composition. We might want extend our bare lambda calculus
344 with a couple of terms former to make our natural deduction more pleasant to
345 use. For example, tagged unions (\texttt{Either} in Haskell) are disjunctions,
346 and tuples (or products) are conjunctions. We also want to be able to express
347 falsity ($\bot$): that can done by introducing a type inhabited by no terms. If
348 evidence of such a type is presented, then we can derive any type, which
349 expresses absurdity. Conversely, truth ($\top$) is the type with just one
350 trivial element ($\lcunit$).
352 \newcommand{\lcinl}{\lccon{inl}\appsp}
353 \newcommand{\lcinr}{\lccon{inr}\appsp}
354 \newcommand{\lccase}[3]{\lcsyn{case}\appsp#1\appsp\lcsyn{of}\appsp#2\appsp#3}
355 \newcommand{\lcfst}{\lcfun{fst}\appsp}
356 \newcommand{\lcsnd}{\lcfun{snd}\appsp}
357 \newcommand{\orint}{\vee I_{1,2}}
358 \newcommand{\orintl}{\vee I_{1}}
359 \newcommand{\orintr}{\vee I_{2}}
360 \newcommand{\orel}{\vee E}
361 \newcommand{\andint}{\wedge I}
362 \newcommand{\andel}{\wedge E_{1,2}}
363 \newcommand{\botel}{\bot E}
364 \newcommand{\lcabsurd}{\lcfun{absurd}\appsp}
365 \newcommand{\lcabsurdd}[1]{\lcfun{absurd}_{#1}\appsp}
372 \termsyn & ::= & \dotsb \\
373 & | & \lcinl \termsyn \separ \lcinr \termsyn \separ \lccase{\termsyn}{\termsyn}{\termsyn} \\
374 & | & (\termsyn , \termsyn) \separ \lcfst \termsyn \separ \lcsnd \termsyn \\
376 \tysyn & ::= & \dotsb \separ \tysyn \vee \tysyn \separ \tysyn \wedge \tysyn \separ \bot \separ \top
381 \axdesc{typing}{\Gamma \vdash \termsyn : \tysyn}
383 \AxiomC{$\Gamma \vdash \termt : \tya$}
384 \RightLabel{$\orint$}
385 \UnaryInfC{$\Gamma \vdash \lcinl \termt : \tya \vee \tyb$}
387 \UnaryInfC{$\Gamma \vdash \lcinr \termt : \tyb \vee \tya$}
390 \AxiomC{$\Gamma \vdash \termt : \tya \vee \tyb$}
391 \AxiomC{$\Gamma \vdash \termm : \tya \tyarr \tyc$}
392 \AxiomC{$\Gamma \vdash \termn : \tyb \tyarr \tyc$}
394 \TrinaryInfC{$\Gamma \vdash \lccase{\termt}{\termm}{\termn} : \tyc$}
398 \AxiomC{$\Gamma \vdash \termt : \tya$}
399 \AxiomC{$\Gamma \vdash \termm : \tyb$}
400 \RightLabel{$\andint$}
401 \BinaryInfC{$\Gamma \vdash (\tya , \tyb) : \tya \wedge \tyb$}
404 \AxiomC{$\Gamma \vdash \termt : \tya \wedge \tyb$}
405 \RightLabel{$\andel$}
406 \UnaryInfC{$\Gamma \vdash \lcfst \termt : \tya$}
408 \UnaryInfC{$\Gamma \vdash \lcsnd \termt : \tyb$}
415 \AxiomC{$\Gamma \vdash \termt : \bot$}
416 \RightLabel{$\botel$}
417 \UnaryInfC{$\Gamma \vdash \lcabsurdd{\tya} \termt : \tya$}
421 \RightLabel{$\top I$}
422 \UnaryInfC{$\Gamma \vdash \lcunit : \top$}
427 \axdesc{reduction}{\termsyn \bred \termsyn}
429 \lccase{(\lcinl \termt)}{\termm}{\termn} & \bred & \app{\termm}{\termt} \\
430 \lccase{(\lcinr \termt)}{\termm}{\termn} & \bred & \app{\termn}{\termt} \\
431 \lcfst (\termt , \termm) & \bred & \termt \\
432 \lcsnd (\termt , \termm) & \bred & \termm
436 With these rules, our STLC now looks remarkably similar in power and use to the
437 natural deduction we already know. $\neg A$ can be expressed as $A \tyarr
438 \bot$. However, there is an important omission: there is no term of the type $A
439 \vee \neg A$ (excluded middle), or equivalently $\neg \neg A \tyarr A$ (double
440 negation), or indeed any term with a type equivalent to those.
442 This has a considerable effect on our logic and it's no coincidence, since there
443 is no obvious computational behaviour for laws like the excluded middle.
444 Theories of this kind are called \emph{intuitionistic}, or \emph{constructive},
445 and all the systems analysed will have this characteristic since they build on
446 the foundation of the STLC\footnote{There is research to give computational
447 behaviour to classical logic, but I will not touch those subjects.}.
449 Finally, going back to our $\lcsyn{fix}$ combinator, it's now easy to see how
450 we would want to exclude such a thing if we want to use STLC as a logic, since
451 it allows us to prove everything: $(\lcfix{x : \tya}{x}) : \tya$ clearly works
452 for any $A$! This is a crucial point: in general we wish to have systems that
453 do not let the user devise a term of type $\bot$, otherwise our logic will be
454 unsound\footnote{Obviously such a term can be present under a $\lambda$.}.
456 \subsection{Extending the STLC}
458 \newcommand{\lctype}{\lccon{Type}}
459 \newcommand{\lcite}[3]{\lcsyn{if}\appsp#1\appsp\lcsyn{then}\appsp#2\appsp\lcsyn{else}\appsp#3}
460 \newcommand{\lcbool}{\lccon{Bool}}
461 \newcommand{\lcforallz}[2]{\forall #1 \absspace.\absspace #2}
462 \newcommand{\lcforall}[3]{(#1 : #2) \tyarr #3}
463 \newcommand{\lcexists}[3]{(#1 : #2) \times #3}
465 The STLC can be made more expressive in various ways. Henk Barendregt
466 succinctly expressed geometrically how we can expand our type system:
470 & \lambda\omega \ar@{-}[rr]\ar@{-}'[d][dd]
471 & & \lambda C \ar@{-}[dd]
473 \lambda2 \ar@{-}[ur]\ar@{-}[rr]\ar@{-}[dd]
474 & & \lambda P2 \ar@{-}[ur]\ar@{-}[dd]
476 & \lambda\underline\omega \ar@{-}'[r][rr]
477 & & \lambda P\underline\omega
479 \lambda{\to} \ar@{-}[rr]\ar@{-}[ur]
480 & & \lambda P \ar@{-}[ur]
483 Here $\lambda{\to}$, in the bottom left, is the STLC. From there can move along
486 \item[Terms depending on types (towards $\lambda{2}$)] We can quantify over
487 types in our type signatures: $(\abs{A : \lctype}{\abs{x : A}{x}}) :
488 \lcforallz{A}{A \tyarr A}$. The first and most famous instance of this idea
489 has been System F. This gives us a form of polymorphism and has been wildly
490 successful, also thanks to a well known inference algorithm for a restricted
491 version of System F known as Hindley-Milner. Languages like Haskell and SML
492 are based on this discipline.
493 \item[Types depending on types (towards $\lambda{\underline{\omega}}$)] We have
494 type operators: $(\abs{A : \lctype}{\abs{R : \lctype}{(A \to R) \to R}}) :
495 \lctype \to \lctype \to \lctype$.
496 \item[Types depending on terms (towards $\lambda{P}$)] Also known as `dependent
497 types', give great expressive power: $(\abs{x : \lcbool}{\lcite{x}{\mathbb{N}}{\mathbb{Q}}}) : \lcbool \to \lctype$.
500 All the systems preserve the properties that make the STLC well behaved. The
501 system we are going to focus on, Intuitionistic Type Theory, has all of the
502 above additions, and thus would sit where $\lambda{C}$ sits in the
505 \section{Intuitionistic Type Theory and dependent types}
508 \newcommand{\lcset}[1]{\lccon{Type}_{#1}}
509 \newcommand{\lcsetz}{\lccon{Type}}
510 \newcommand{\defeq}{\cong}
512 \subsection{A Bit of History}
514 Logic frameworks and programming languages based on type theory have a long
515 history. Per Martin-L\"{o}f described the first version of his theory in 1971,
516 but then revised it since the original version was too impredicative and thus
517 inconsistent\footnote{In the early version $\lcsetz : \lcsetz$, see section
518 \ref{sec:core-tt} for an explanation on why this causes problems.}. For this
519 reason he gave a revised and consistent definition later \citep{Martin-Lof1984}.
521 A related development is the polymorphic $\lambda$-calculus, and specifically
522 the previously mentioned System F, which was developed independently by Girard
523 and Reynolds. An overview can be found in \citep{Reynolds1994}. The surprising
524 fact is that while System F is impredicative it is still consistent and strongly
525 normalising. \cite{Coquand1986} further extended this line of work with the
526 Calculus of Constructions (CoC).
528 \subsection{A Core Type Theory}
531 The calculus I present follows the exposition in \citep{Thompson1991}, and is
532 quite close to the original formulation of predicative ITT as found in
533 \citep{Martin-Lof1984}.
538 \termsyn & ::= & x \\
539 & | & \lcforall{x}{\termsyn}{\termsyn} \separ \abs{x : \termsyn}{\termsyn} \separ \app{\termsyn}{\termsyn} \\
540 & | & \lcexists{x}{\termsyn}{\termsyn} \separ (\termsyn , \termsyn)_{x.\termsyn} \separ \lcfst \termsyn \separ \lcsnd \termsyn \\
541 & | & \bot \separ \lcabsurd_{\termsyn} \termsyn \\
546 \axdesc{typing}{\Gamma \vdash \termsyn : \termsyn}
550 \begin{tabular}{c c c}
551 \AxiomC{\phantom{1em}}
552 \UnaryInfC{$\Gamma;x : \tya \vdash x : \tya$}
555 \AxiomC{$\Gamma \vdash \termt : \tya$}
556 \AxiomC{$\tya \defeq \tyb$}
557 \BinaryInfC{$\Gamma \vdash \termt : \tyb$}
560 \AxiomC{$\Gamma \vdash \termt : \bot$}
561 \UnaryInfC{$\Gamma \vdash \lcabsurdd{\tya} \termt : \tya$}
568 \AxiomC{$\Gamma;x : \tya \vdash \termt : \tya$}
569 \UnaryInfC{$\Gamma \vdash \abs{x : \tya}{\termt} : \lcforall{x}{\tya}{\tyb}$}
572 \AxiomC{$\Gamma \vdash \termt : \lcforall{x}{\tya}{\tyb}$}
573 \AxiomC{$\Gamma \vdash \termm : \tya$}
574 \BinaryInfC{$\Gamma \vdash \app{\termt}{\termm} : \tyb[\termm ]$}
581 \AxiomC{$\Gamma \vdash \termt : \tya$}
582 \AxiomC{$\Gamma \vdash \termm : \tyb[\termt ]$}
583 \BinaryInfC{$\Gamma \vdash (\termt, \termm)_{x.\tyb} : \lcexists{x}{\tya}{\tyb}$}
585 \UnaryInfC{$\phantom{1em}$}
588 \AxiomC{$\Gamma \vdash \termt: \lcexists{x}{\tya}{\tyb}$}
589 \UnaryInfC{$\hspace{0.7cm} \Gamma \vdash \lcfst \termt : \tya \hspace{0.7cm}$}
591 \UnaryInfC{$\Gamma \vdash \lcsnd \termt : \tyb[\lcfst \termt ]$}
598 \AxiomC{$\phantom{1em}$}
599 \UnaryInfC{$\Gamma \vdash \lcset{n} : \lcset{n + 1}$}
601 \UnaryInfC{$\phantom{1em}$}
604 \AxiomC{$\Gamma \vdash \tya : \lcset{n}$}
605 \AxiomC{$\Gamma; x : \tya \vdash \tyb : \lcset{m}$}
606 \BinaryInfC{$\Gamma \vdash \lcforall{x}{\tya}{\tyb} : \lcset{n \sqcup m}$}
608 \UnaryInfC{$\Gamma \vdash \lcexists{x}{\tya}{\tyb} : \lcset{n \sqcup m}$}
614 \axdesc{reduction}{\termsyn \bred \termsyn}
616 \app{(\abs{x}{\termt})}{\termm} & \bred & \termt[\termm ] \\
617 \lcfst (\termt, \termm) & \bred & \termt \\
618 \lcsnd (\termt, \termm) & \bred & \termm
622 When showing examples types will be omitted when this can be done without loss
623 of clarity, for example $\abs{x}{x}$ in place of $\abs{A : \lcsetz}{\abs{x :
624 A}{x}}$. I will also use $\lcsetz$ as $\lcset{0}$.
626 There are a lot of new factors at play here. The first thing to notice is that
627 the separation between types and terms is gone. All we have is terms, that
628 include both values (terms of type $\lcset{0}$) and types (terms of type
629 $\lcset{n}$, with $n > 0$). This change is reflected in the typing rules.
630 While in the STLC values and types are kept well separated (values never go
631 `right of the colon'), in ITT types can freely depend on values.
633 This relation is expressed in the typing rules for $\tyarr$ and $\times$: if a
634 function has type $\lcforall{x}{\tya}{\tyb}$, $\tyb$ can depend on $x$.
635 Examples will make this clearer once some base types are added in section
636 \ref{sec:base-types}.
638 $\tyarr$ and $\times$ are at the core of the machinery of ITT:
641 \item[`forall' ($\tyarr$)] is a generalisation of $\tyarr$ in the STLC and
642 expresses universal quantification in our logic. It is often written with a
643 syntax closer to logic, e.g. $\forall x : \tya. \tyb$. In the
644 literature this is also known as `dependent product' and shown as $\Pi$,
645 following the interpretation of functions as infinitary products. I will just
646 call it `dependent function', reserving `product' for $\exists$.
648 \item[`exists' ($\times$)] is a generalisation of $\wedge$ in the extended STLC
649 of section \ref{sec:curry-howard}, and thus I will call it `dependent
650 product'. Like $\wedge$, it is formed by providing a pair of things. In our
651 logic, it represents existential quantification. Similarly to $\tyarr$, it is
652 always written as $\exists x : \tya. \tyb$.
654 For added confusion, in the literature that calls forall $\Pi$, $\exists$ is
655 often named `dependent sum' and shown as $\Sigma$. This is following the
656 interpretation of $\exists$ as a generalised, infinitary $\vee$, where the
657 first element of the pair is the `tag' that determines which type the second
661 Another thing to notice is that types are very `first class': we are free to
662 create functions that accept and return types. For this reason we define
663 $\defeq$ as the smallest equivalence relation extending $\bredc$, where $\bredc$
664 is the reflexive transitive closure of $\bred$; and we treat types that are
665 relate according to $\defeq$ as the same. Another way of seeing $\defeq$ is
666 this: when we want to compare two types for equality, we reduce them as far as
667 possible and then check if they are equal\footnote{Note that when comparing
668 terms we do it up to $\alpha$-renaming. That is, we do not consider
669 relabelling of variables as a difference - for example $\abs{x : A}{x} \defeq
670 \abs{y : A}{y}$.}. This works since not only each term has a normal form (ITT
671 is strongly normalising), but the normal form is also unique; or in other words
672 $\bred$ is confluent (if $\termt \bredc \termm$ and $\termt \bredc \termn$, then
673 there is a $p$ such that $\termm \bredc \termp$ and $\termn \bredc \termp$).
674 This measure makes sure that, for instance, $\app{(\abs{x :
675 \lctype}{x})}{\lcbool} \defeq \lcbool$. The theme of equality is central
676 and will be analysed better later.
678 The theory presented is \emph{stratified}. We have a hierarchy of types
679 $\lcset{0} : \lcset{1} : \lcset{2} : \dots$, so that there is no `type of all
680 types', and our theory is predicative. Type-formers like $\tyarr$ and $\times$
681 take the least upper bound $\sqcup$ of the contained types. The layers of the
682 hierarchy are called `universes'. Theories where $\lcsetz : \lcsetz$ are
683 inconsistent due to Girard's paradox \citep{Hurkens1995}, and thus lose their
684 well-behavedness. Some impredicativity sometimes has its place, either because
685 the theory retain good properties (normalization, consistency, etc.) anyway,
686 like in System F and CoC; or because we are at a stage at which we do not care -
687 we will see instances in section \ref{foo}
688 % TODO put citation here
690 Note that the Curry-Howard correspondence runs through ITT as it did with the
691 STLC with the difference that ITT corresponds to an higher order propositional
694 \subsection{Base Types}
695 \label{sec:base-types}
697 \newcommand{\lctrue}{\lccon{true}}
698 \newcommand{\lcfalse}{\lccon{false}}
699 \newcommand{\lcw}[3]{\lccon{W} #1 : #2 \absspace.\absspace #3}
700 \newcommand{\lcnode}[4]{#1 \lhd_{#2 . #3} #4}
701 \newcommand{\lcnodez}[2]{#1 \lhd #2}
702 \newcommand{\lcited}[5]{\lcsyn{if}\appsp#1/#2\appsp.\appsp#3\appsp\lcsyn{then}\appsp#4\appsp\lcsyn{else}\appsp#5}
703 \newcommand{\lcrec}[4]{\lcsyn{rec}\appsp#1/#2\appsp.\appsp#3\appsp\lcsyn{with}\appsp#4}
704 \newcommand{\lcrecz}[2]{\lcsyn{rec}\appsp#1\appsp\lcsyn{with}\appsp#2}
705 \newcommand{\AxiomL}[1]{\Axiom$\fCenter #1$}
706 \newcommand{\UnaryInfL}[1]{\UnaryInf$\fCenter #1$}
708 While the ITT presented is a fairly complete logic, it is not that useful for
709 programming. If we wish to make it better, we can add some base types to
710 represent the data structures we know and love, such as numbers, lists, and
711 trees. Apart from some unsurprising data types, we introduce $\lccon{W}$, a
712 very general tree-like structure useful to represent inductively defined types
713 and that will allow us to express structural recursion in an equally general
719 \termsyn & ::= & \dots \\
720 & | & \top \separ \lcunit \\
721 & | & \lcbool \separ \lctrue \separ \lcfalse \separ \lcited{\termsyn}{x}{\termsyn}{\termsyn}{\termsyn} \\
722 & | & \lcw{x}{\termsyn}{\termsyn} \separ \lcnode{\termsyn}{x}{\termsyn}{\termsyn} \separ \lcrec{\termsyn}{x}{\termsyn}{\termsyn}
725 \axdesc{typing}{\Gamma \vdash \termsyn : \termsyn}
729 \begin{tabular}{c c c}
731 \UnaryInfC{$\hspace{0.2cm}\Gamma \vdash \top : \lcset{0} \hspace{0.2cm}$}
733 \UnaryInfC{$\Gamma \vdash \lcbool : \lcset{0}$}
737 \UnaryInfC{$\Gamma \vdash \lcunit : \top$}
739 \UnaryInfC{\phantom{1em}}
743 \UnaryInfC{$\Gamma \vdash \lctrue : \lcbool$}
745 \UnaryInfC{$\Gamma \vdash \lcfalse : \lcbool$}
752 \AxiomC{$\Gamma \vdash \termt : \lcbool$}
753 \AxiomC{$\Gamma \vdash \termm : \tya[\lctrue]$}
754 \AxiomC{$\Gamma \vdash \termn : \tya[\lcfalse]$}
755 \TrinaryInfC{$\Gamma \vdash \lcited{\termt}{x}{\tya}{\termm}{\termn} : \tya[\termt]$}
762 \AxiomC{$\Gamma \vdash \tya : \lcset{n}$}
763 \AxiomC{$\Gamma; x : \tya \vdash \tyb : \lcset{m}$}
764 \BinaryInfC{$\Gamma \vdash \lcw{x}{\tya}{\tyb} : \lcset{n \sqcup m}$}
771 \AxiomC{$\Gamma \vdash \termt : \tya$}
772 \AxiomC{$\Gamma \vdash \termf : \tyb[\termt ] \tyarr \lcw{x}{\tya}{\tyb}$}
773 \BinaryInfC{$\Gamma \vdash \lcnode{\termt}{x}{\tyb}{\termf} : \lcw{x}{\tya}{\tyb}$}
780 \AxiomC{$\Gamma \vdash \termt: \lcw{x}{\tya}{\tyb}$}
782 \UnaryInfC{$\Gamma \vdash \lcforall{\termm}{\tya}{\lcforall{\termf}{\tyb[\termm] \tyarr \lcw{x}{\tya}{\tyb}}{(\lcforall{\termn}{\tyb[\termm]}{\tyc[\app{\termf}{\termn}]}) \tyarr \tyc[\lcnodez{\termm}{\termf}]}}$}
783 \UnaryInfC{$\Gamma \vdash \lcrec{\termt}{x}{\tyc}{\termp} : \tyc[\termt]$}
789 \axdesc{reduction}{\termsyn \bred \termsyn}
791 \lcited{\lctrue}{x}{\tya}{\termt}{\termm} & \bred & \termt \\
792 \lcited{\lcfalse}{x}{\tya}{\termt}{\termm} & \bred & \termm \\
793 \lcrec{\lcnodez{\termt}{\termf}}{x}{\tya}{\termp} & \bred & \app{\app{\app{\termp}{\termt}}{\termf}}{(\abs{\termm}{\lcrec{\app{f}{\termm}}{x}{\tya}{\termp}})}
797 The introduction and elimination for $\top$ and $\lcbool$ are unsurprising.
798 Note that in the $\lcite{\dotsb}{\dotsb}{\dotsb}$ construct the type of the
799 branches are dependent on the value of the conditional.
801 % TODO: explain better here
803 The rules for $\lccon{W}$, on the other hand, are quite an eyesore. The idea
804 behind $\lccon{W}$ types is to build up `trees' where the number of `children'
805 of each node is dependent on the value in the node. This is captured by the
806 $\lhd$ constructor, where the argument on the left is the value, and the
807 argument on the right is a function that returns a child for each possible value
808 of $\tyb[\text{node value}]$, if $\lcw{x}{\tya}{\tyb}$. The recursor
809 $\lcrec{\termt}{x}{\tyc}{\termp}$ uses $p$ to inductively prove that
810 $\tyc[\termt]$ holds.
812 \subsection{Some examples}
814 Now we can finally provide some meaningful examples. Apart from omitting types,
815 I will also use some abbreviations:
817 \item $\_\mathit{operator}\_$ to define infix operators
818 \item $\abs{x\appsp y\appsp z : \tya}{\dotsb}$ to define multiple abstractions at the same
822 \subsubsection{Sum types}
824 We would like to recover our sum type, or disjunction, $\vee$. This is easily
825 achieved with $\times$:
828 \_\vee\_ & = & \abs{\tya\appsp\tyb : \lcsetz}{\lcexists{x}{\lcbool}{\lcite{x}{\tya}{\tyb}}} \\
829 \lcinl & = & \abs{x}{(\lctrue, x)} \\
830 \lcinr & = & \abs{x}{(\lcfalse, x)} \\
831 \lcfun{case} & = & \abs{x : \tya \vee \tyb}{\abs{f : \tya \tyarr \tyc}{\abs{g : \tyb \tyarr \tyc}{ \\
832 & & \hspace{0.5cm} \app{(\lcited{\lcfst x}{b}{(\lcite{b}{A}{B}) \tyarr C}{f}{g})}{(\lcsnd x)}}}}
835 What is going on here? We are using $\exists$ with $\lcbool$ as a tag, so that
836 we can choose between one of two types in the second element. In
837 $\lcfun{case}$ we use $\lcite{\lcfst x}{\dotsb}{\dotsb}$ to discriminate on the
838 tag, that is, the first element of $x : \tya \vee \tyb$. If the tag is true,
839 then we know that the second element is of type $\tya$, and we will apply $f$.
840 The same applies to the other branch, with $\tyb$ and $g$.
842 \subsubsection{Naturals}
844 Now it's time to showcase the power of $\lccon{W}$ types.
846 \lccon{Nat} & = & \lcw{b}{\lcbool}{\lcite{b}{\top}{\bot}} \\
847 \lccon{zero} & = & \lcfalse \lhd \abs{z}{\lcabsurd z} \\
848 \lccon{suc} & = & \abs{n}{(\lctrue \lhd \abs{\_}{n})} \\
849 \lcfun{plus} & = & \abs{x\appsp y}{\lcrecz{x}{(\abs{b}{\lcite{b}{\abs{\_\appsp f}{\app{\lccon{suc}}{(\app{f}{\lcunit})}}}{\abs{\_\appsp\_}{y}}})}}
851 Here we encode natural numbers through $\lccon{W}$ types. Each node contains a
852 $\lcbool$. If the $\lcbool$ is $\lcfalse$, then there are no children, since we
853 have a function $\bot \tyarr \lccon{Nat}$: this is our $0$. If it's $\lctrue$,
854 we need one child only: the predecessor. We recurse giving $\lcsyn{rec}$ a
855 function that handles the `base case' 0 when the $\lcbool$ is $\lctrue$, and the
856 inductive case otherwise.
858 We postpone more complex examples after the introduction of inductive families
859 and pattern matching, since $\lccon{W}$ types get unwieldy very quickly.
861 \subsection{Propositional Equality}
864 We can finally introduce one of the central subjects of my project:
865 propositional equality.
867 \newcommand{\lceq}[3]{#2 =_{#1} #3}
868 \newcommand{\lceqz}[2]{#1 = #2}
869 \newcommand{\lcrefl}[2]{\lccon{refl}_{#1}\appsp #2}
870 \newcommand{\lcsubst}[3]{\lcfun{subst}\appsp#1\appsp#2\appsp#3}
875 \termsyn & ::= & ... \\
876 & | & \lceq{\termsyn}{\termsyn}{\termsyn} \separ \lcrefl{\termsyn}{\termsyn} \separ \lcsubst{\termsyn}{\termsyn}{\termsyn}
879 \axdesc{typing}{\Gamma \vdash \termsyn : \termsyn}
884 \AxiomC{$\Gamma \vdash \termt : \tya$}
885 \UnaryInfC{$\Gamma \vdash \lcrefl{\tya}{\termt} : \lceq{\tya}{\termt}{\termt}$}
888 \AxiomC{$\Gamma \vdash \termp : \lceq{\tya}{\termt}{\termm}$}
889 \AxiomC{$\Gamma \vdash \tyb : \tya \tyarr \lcsetz$}
890 \AxiomC{$\Gamma \vdash \termn : \app{\tyb}{\termt}$}
891 \TrinaryInfC{$\Gamma \vdash \lcsubst{\termp}{\tyb}{\termn} : \app{\tyb}{\termm}$}
897 \axdesc{reduction}{\termsyn \bred \termsyn}
899 \lcsubst{(\lcrefl{\tya}{\termt})}{\tyb}{\termm} \bred \termm
903 Propositional equality internalises equality as a type. The only way to
904 introduce an equality proof is by reflexivity ($\lccon{refl}$). The eliminator
905 is in the style of `Leibnitz's law' of equality: `equals can be substituted for
906 equals' ($\lcfun{subst}$). The computation rule refers to the fact that every
907 proof of equality will be a $\lccon{refl}$. We can use $\neg
908 (\lceq{\tya}{x}{y})$ to express inequality.
910 These elements conclude our presentation of a `core' type theory. For an
911 extended example of a similar theory in use see Section 6.2 of
912 \cite{Thompson1991}\footnote{Note that while I attempted to formalise the proof
913 in Agda, I found a bug in the book! See the errata for details:
914 \url{http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/errata.html}.}. The above
915 language and examples have been codified in Agda\footnote{More on Agda in the
916 next section.}, see appendix \ref{app:agda-code}.
918 \section{A more useful language}
919 \label{sec:practical}
921 While our core type theory equipped with $\lccon{W}$ types is very usefully
922 conceptually as a simple but complete language, things get messy very fast. In
923 this section I will present the elements that are usually included in theorem
924 provers or programming languages to make them usable by mathematicians or
927 All the features presented are present in the second version of the Agda system
928 \citep{Norell2007, Bove2009}. Agda follows a tradition of theorem provers based
929 on ITT with inductive families and pattern matching. The closest relative of
930 Agda, apart from previous versions, is Epigram \citep{McBride2004, EpigramTut}.
931 Coq is another notable theorem prover based on the same concepts, and the first
932 and most popular \citep{Coq}.
934 The main difference between Coq and Agda/Epigram is that the former focuses on
935 theorem proving, while the latter also want to be useful as functional
936 programming languages, while still offering good tools to express
937 mathematics\footnote{In fact, currently, Agda is used almost exclusively to
938 express mathematics, rather than to program.}. This is reflected in a series
939 of differences that I will not discuss here (most notably the absence of tactics
940 but better support for pattern matching in Agda/Epigram). I will take the same
941 approach as Agda/Epigram and will give a perspective focused on functional
942 programming rather than theorem proving. Every feature will be presented as it
945 \subsection{Bidirectional type checking}
947 Lastly, the theory I present is fully explicit in the sense that the user has to
948 specify every type when forming abstractions, products, etc. This can be a
949 great burden if one wants to use the theory directly. Complete inference is
950 undecidable (which is hardly surprising considering the role that types play)
951 but partial inference (also called `bidirectional type checking' in this
952 context) in the style of \cite{Pierce2000} will have to be deployed in a
955 \subsection{Inductive families}
957 \newcommand{\lcdata}[1]{\lcsyn{data}\appsp #1}
958 \newcommand{\lcdb}{\ |\ }
959 \newcommand{\lcind}{\hspace{0.2cm}}
960 \newcommand{\lcwhere}{\appsp \lcsyn{where}}
961 \newcommand{\lclist}[1]{\app{\lccon{List}}{#1}}
962 \newcommand{\lcnat}{\lccon{Nat}}
963 \newcommand{\lcvec}[2]{\app{\app{\lccon{Vec}}{#1}}{#2}}
965 Inductive families were first introduced by \cite{Dybjer1991}. For the reader
966 familiar with the recent developments present in the GHC compiler for Haskell,
967 inductive families will look similar to GADTs (Generalised Abstract Data Types)
968 \citep[Section 7.4.7]{GHC}.
969 Haskell style data types provide \emph{parametric polymorphism}, so that we can
970 define types that range over type parameters:
972 List a = Nil | Cons a (List a)
974 In this way we define the \texttt{List} type once while allowing elements to be
975 of any type. In Haskell \texttt{List} will be a type constructor of kind
976 \texttt{* -> *}, while \texttt{Nil :: List a} and \texttt{Cons :: a -> List a -> List a}\footnote{Note that the \texttt{a}s are implicitly quantified type variables}.
978 Inductive families bring this concept one step further by allowing some of the
979 parameters to be constrained by constructors. We call these `variable'
980 parameters `indices'. For example we might define natural numbers
983 \lcdata{\lcnat} : \lcsetz \lcwhere \\
984 \begin{array}{l@{\ }l}
985 \lcind \lccon{zero} &: \lcnat \\
986 \lcind \lccon{suc} &: \lcnat \tyarr \lcnat
990 And then define a type for lists indexed by length:
993 \lcdata{\lccon{Vec}}\appsp (A : \lcsetz) : \lcnat \tyarr \lcsetz \lcwhere \\
994 \begin{array}{l@{\ }l}
995 \lcind \lccon{nil} &: \lcvec{A}{\lccon{zero}} \\
996 \lcind \_::\_ &: \{n : \lccon{Nat}\} \tyarr A \tyarr \lcvec{A}{n} \tyarr \lcvec{A}{\app{(\lccon{suc}}{n})}
1000 Note that contrary to the Haskell ADT notation, with inductive families we
1001 explicitly list the types for the type and data constructors. In $\lccon{Vec}$,
1002 $A$ is a parameter (same across all constructors) while the $\lcnat$ is an
1003 index. In our syntax, in the $\lcsyn{data}$ declaration, things to the left of
1004 the colon are parameters, while on the right we can define the type of indices.
1005 Also note that the parameters' identifiers will be in scope across all
1006 constructors, while indices' won't.
1008 In this $\lccon{Vec}$ example, when we form a new list the length is
1009 $\lccon{zero}$. When we append a new element to an existing list of length $n$,
1010 the new list is of length $\app{\lccon{suc}}{n}$, that is, one more than the
1011 previous length. Also note that we are using the $\{n : \lcnat\} \tyarr \dotsb$
1012 syntax to indicate an argument that we will omit when using $\_::\_$. In the
1013 future I shall also omit the type of these implicit parameters, in line with how
1016 Once we have $\lccon{Vec}$ we can do things much more safely than with normal
1017 lists. For example, we can define an $\lcfun{head}$ function that returns the
1018 first element of the list:
1021 \lcfun{head} : \{A\ n\} \tyarr \lcvec{A}{(\app{\lccon{suc}}{n})} \tyarr A
1024 Note that we will not be able to provide this function with a
1025 $\lcvec{A}{\lccon{zero}}$, since it needs an index which is a successor of some
1028 \newcommand{\lcfin}[1]{\app{\lccon{Fin}}{#1}}
1030 If we wish to index a $\lccon{Vec}$ safely, we can define an inductive family
1031 $\lcfin{n}$, which represents the family of numbers smaller than a given number
1035 \lcdata{\lccon{Fin}} : \lcnat \tyarr \lcsetz \lcwhere \\
1036 \begin{array}{l@{\ }l}
1037 \lcind \lccon{fzero} &: \{n\} \tyarr \lcfin{(\app{\lccon{suc}}{n})} \\
1038 \lcind \lccon{fsuc} &: \{n\} \tyarr \lcfin{n} \tyarr \lcfin{(\app{\lccon{suc}}{n})}
1042 $\lccon{fzero}$ is smaller than any number apart from $\lccon{zero}$. Given
1043 the family of numbers smaller than $n$, we can produce the family of numbers
1044 smaller than $\app{\lccon{suc}}{n}$. Now we can define an `indexing' operation
1045 for our $\lccon{Vec}$:
1048 \_\lcfun{!!}\_ : \{A\ n\} \tyarr \lcvec{A}{n} \tyarr \lcfin{n} \tyarr A
1051 In this way we will be sure that the number provided as an index will be smaller
1052 than the length of the $\lccon{Vec}$ provided.
1054 \subsubsection{Computing with inductive families}
1056 I have carefully avoided to define the functions that I mentioned as example,
1057 since one question still is unanswered: `how do we work with inductive
1058 families'? The most basic approach is to work with eliminators, that can be
1059 automatically provided by the programming language for each data type defined.
1060 For example the induction principle on natural numbers will serve as an
1061 eliminator for $\lcnat$:
1063 \begin{array}{l@{\ } c@{\ } l}
1064 \lcfun{NatInd} & : & (A : \lcsetz) \tyarr \\
1065 & & A \tyarr (\lcnat \tyarr A \tyarr A) \tyarr \\
1070 That is, if we provide an $A$ (base case), and then given a number and an $A$ we
1071 give the next $A$ (inductive step), then an $A$ can be computed for every
1072 number. This can be expressed easily in Haskell:
1074 data Nat = Zero | Suc Nat
1075 natInd :: a -> (Nat -> a -> a) -> Nat -> a
1077 natInd z f (Suc n) = f n (natInd z f n)
1079 However, in a dependent setting, we can do better:
1081 \begin{array}{l@{\ } c@{\ } l}
1082 \lcfun{NatInd} & : & (P : \lcnat \tyarr \lcsetz) \tyarr \\
1083 & & \app{P}{\lccon{zero}} \tyarr ((n : \lcnat) \tyarr \app{P}{n} \tyarr \app{P}{(\app{\lccon{suc}}{n})}) \tyarr \\
1084 & & (n : \lcnat) \tyarr \app{P}{n}
1087 This expresses the fact that the resulting type can be dependent on the number.
1088 In other words, we are proving that $P$ holds for all $n : \lcnat$.
1090 Naturally a reduction rule will be associated with each eliminator:
1092 \begin{array}{l c l}
1093 \app{\app{\app{\app{\lcfun{NatInd}}{P}}{z}}{f}}{\lccon{zero}} & \bred & z \\
1094 \app{\app{\app{\app{\lcfun{NatInd}}{P}}{z}}{f}}{(\app{\lccon{suc}}{n})} & \bred & \app{\app{f}{n}}{(\app{\app{\app{\app{\lcfun{NatInd}}{P}}{z}}{f}}{n})}
1097 Which echoes the \texttt{natInd} function defined in Haskell. An extensive
1098 account on combinators and inductive families can be found in \cite{McBride2004}.
1100 \subsubsection{Pattern matching and guarded recursion}
1102 However, combinators are far more cumbersome to use than the techniques usually
1103 employed in functional programming: pattern matching and recursion.
1104 \emph{General} recursion cannot be added if we want to keep our theory free of
1105 $\bot$. The common solution to this problem is to allow recursive calls only if
1106 the arguments are structurally smaller than what the function received. Pattern
1107 matching on the other hand gains considerable power with inductive families,
1108 since when we match a constructor we are gaining information on the indices of
1109 the family. Thus matching constructors will enable us to restrict patterns of
1112 Following this discipline defining $\lcfun{head}$ becomes easy:
1115 \lcfun{head} : \{A\ n\} \tyarr \lcvec{A}{(\app{\lccon{suc}}{n})} \tyarr A \\
1116 \lcfun{head}\appsp(x :: \_) = x
1119 We need no case for $\lccon{nil}$, since the type checker knows that the
1120 equation $n = \lccon{zero} = \app{\lccon{suc}}{n'}$ cannot be satisfied.
1122 More details on the implementations of inductive families can be found in
1123 \citep{McBride2004, Norell2007}.
1125 \subsection{Friendlier universes}
1127 Universes as presented in section \ref{sec:core-tt} are quite cumbersome to work
1128 with. Consider the example where we define an inductive family for booleans and
1129 then we want to define an `if then else' eliminator:
1132 \lcdata{\lcbool} : \lcsetz \lcwhere \\
1133 \begin{array}{l@{\ }l}
1134 \lcind \lccon{true} &: \lcbool \\
1135 \lcind \lccon{false} &: \lcbool
1138 \lcfun{ite} : \{A : \lcset{0}\} \tyarr \lcbool \tyarr A \tyarr A \tyarr A \\
1139 \lcfun{ite} \appsp \lccon{true} \appsp x \appsp \_ = x \\
1140 \lcfun{ite} \appsp \lccon{false} \appsp \_ \appsp x = x
1144 What if we want to use $\lcfun{ite}$ with types, for example $\lcfun{ite} \appsp
1145 b \appsp \lcnat \appsp \lccon{Bool}$? Clearly $\lcnat$ is not of type
1146 $\lcset{0}$, so we'd have to redefine $\lcfun{ite}$ with exactly the same body,
1147 but different type signature. The problem is even more evident with type
1148 families: for example our $\lccon{List}$ can only contain values, and if we want
1149 to build lists of types we need to define another identical, but differently
1152 One option is to have a \emph{cumulative} theory, where $\lcset{n} : \lcset{m}$
1153 iff $n < m$. Then we can have a sufficiently large level in our type signature
1154 and forget about it. Moreover, levels in this setting can be inferred
1155 mechanically \citep{Pollack1990}, and thus we might lift the burden of universes
1156 from the user. This is the approach taken by Epigram.
1158 Another more expressive (but currently more cumbersome) way is to expose
1159 universes more, giving the user a way to quantify them and to take the least
1160 upper bound of two levels. This is the approach taken by Agda, where for
1161 example we can define a level-polymorphic $\times$:
1164 \lcdata{\_\times\_}\ \{a\ b : \lccon{Level}\}\ (A : \lcset{a})\ (B : A \tyarr \lcset{b}) : \lcset{a \sqcup b} \lcwhere \\
1165 \lcind \_ , \_ : (x : A) \tyarr \app{B}{x} \tyarr A \times \app{B}{x}
1168 Levels can be made implicit as shown and can be almost always inferred.
1169 However, having to decorate each type signature with quantified levels adds
1170 quite a lot of noise. An inference algorithm that automatically quantifies and
1171 instantiates levels (much like Hindley-Milner for types) seems feasible, but
1172 currently not implemented anywhere.
1174 \subsection{Coinduction}
1176 One thing that the Haskell programmer will miss in ITT as presented is the
1177 possibility to work with infinite data. The classic example is the manipulation
1178 of infinite streams:
1180 zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
1183 fibs = 0 : 1 : zipWith (+) fibs (tail fibs)
1185 While we can clearly write useful programs of this kind, we need to be careful,
1186 since \texttt{length fibs}, for example, does not make much sense\footnote{Note
1187 that if instead of machine \texttt{Int}s we used naturals as defined
1188 previously, getting the length of an infinite list would a productive
1191 In less informal terms, we need to distinguish between \emph{productive} and
1192 non-productive definitions. A productive definition is one for which pattern
1193 matching on data will never diverge, which is the case for \texttt{fibs} but
1194 not, for example, for \texttt{let x = x in x :: [Int]}. It is very desirable to
1195 recover \emph{only} the productive definition so that total programs working
1196 with infinite data can be written.
1198 This desire has lead to work on coindunction
1201 \section{Many equalities}
1203 \subsection{Revision, and function extensionality}
1205 \epigraph{\emph{Half of my time spent doing research involves thinking up clever
1206 schemes to avoid needing functional extensionality.}}{@larrytheliquid}
1208 Up to this point, I have introduced two equalities: \emph{definitional} equality
1209 ($\defeq$) and \emph{propositional} equality ($=_{\tya}$).
1211 Definitional equality relates terms that the type checker identifies as equal.
1212 Our definition in section \ref{sec:core-tt} consisted of `reduce the two terms
1213 to their normal forms, then check if they are equal (up to $\alpha$-renaming)'.
1214 We can extend this definition in other ways so that more terms will be
1215 identified as equal. Common ones include doing $\eta$-expansion, which converts
1216 partial appications of functions, and congruence laws for $\lambda$:
1218 \begin{tabular}{c c c}
1219 \AxiomC{$\Gamma \vdash \termf : \tya \tyarr \tyb$}
1220 \UnaryInfC{$\Gamma \vdash \termf \defeq \abs{x}{\app{\termf}{x}}$}
1223 \AxiomC{$\Gamma; x : \tya \vdash \termf \defeq g$}
1224 \UnaryInfC{$\Gamma \vdash \abs{x}{\termf} \defeq \abs{x}{g}$}
1228 Definitional equality is used in the type checking process, and this means that
1229 in dependently typed languages type checking and evaluation are intertwined,
1230 since we need to reduce types to normal forms to check if they are equal. It
1231 also means that we need be able to compute under binders, for example to
1232 determine that $\abs{x}{\app{(\abs{y}{y})}{\tya}} \defeq \abs{x}{\tya}$. This
1233 process goes on `under the hood' and is outside the control of the user.
1235 Propositional equality, on the other hand, is available to the user to reason
1236 about equality, internalising it as a type. As we have seen in section
1237 \ref{sec:propeq} propositional equality is introduced by reflexivity and
1238 eliminated with a `Leibnitz's law' style rule ($\lcfun{subst}$). Now that we
1239 have inductive families and dependent pattern matching we do not need hard coded
1240 rules to express this concepts\footnote{Here I use Agda notation, and thus I
1241 cannot redefine $=$ and use subscripts, so I am forced to use $\equiv$ with
1242 implicit types. After I will carry on using the old notation.}:
1245 \lcdata{\lccon{\_\equiv\_}} : \{A : \lcsetz\} : A \tyarr A \tyarr \lcsetz \lcwhere \\
1246 \begin{array}{l@{\ }l}
1247 \lcind \lccon{refl} &: \{x : A\} \tyarr x \equiv x
1250 \lcfun{subst} : \{A : \lcsetz\} \tyarr \{t\ m : A\} \tyarr t \equiv m \tyarr (B : A \tyarr \lcsetz) \tyarr \app{B}{t} \tyarr \app{B}{m} \\
1251 \lcfun{subst} \appsp \lccon{refl}\appsp B \appsp n = n
1254 Here matching $\lccon{refl}$ tells the type checker that $t \defeq m$, and thus
1255 $\app{B}{t} \defeq \app{B}{m}$, so we can just return $n$.
1257 While propositional equality is a very useful construct, we can prove less terms
1258 equal than we would like to. For example, if we have the usual functions
1260 \begin{array}{l@{\ } l}
1261 \lcfun{id} & : \{A : \lcsetz\} \tyarr A \tyarr A \\
1262 \lcfun{map} & : \{A\ B : \lcsetz\} \tyarr (A \tyarr B) \tyarr \app{\lccon{List}}{A} \tyarr \app{\lccon{List}}{B}
1265 we would certainly like to have a term of type
1266 \[\{A\ B : \lcsetz\} \tyarr
1267 \app{\lcfun{map}}{\lcfun{id}} =_{\lclist{A} \tyarr \lclist{B}} \lcfun{id}\]
1268 We cannot do this in ITT, since the things on the sides of $=$ look too
1269 different at the term level. What we can have is
1271 \{A\ B : \lcsetz\} \tyarr (x : \lclist{A}) \tyarr \app{\app{\lcfun{map}}{\lcfun{id}}}{x}
1272 =_{\lclist{B}} \app{\lcfun{id}}{x}
1274 Since the type checker has something to compute with (even if only a variable)
1275 and reduce the two lists to equal normal forms. The root of this problem is
1276 that \emph{function extensionality} does not hold:
1278 \begin{array}{l@{\ } l}
1279 \lcfun{ext} : & \{A\ B : \lcsetz\} \tyarr (f\ g : A \tyarr B) \tyarr \\
1280 & ((x : A) \tyarr \app{f}{x} =_{A} \app{g}{x}) \tyarr f =_{A \tyarr B} g
1283 Which is a long standing issue in ITT.
1285 \subsection{Extensional Type Theory and its problems}
1287 One way to `solve' the problem and gain extensionality is to allow the type
1288 checker to derive definitional equality from propositional equality, introducing
1289 what is known as the `equality reflection' rule:
1292 \AxiomC{$\Gamma \vdash t =_A m$}
1293 \UnaryInfC{$\Gamma \vdash t \defeq m$}
1296 This jump from types to a metatheoretic relation has deep consequences. But
1297 firstly, let's get extensionality out of the way. Given $\Gamma = \lcfun{eq} :
1298 (x : A) \tyarr \app{f}{x} = \app{g}{x}$, we have:
1301 \AxiomC{$\Gamma; x : A \vdash \app{\lcfun{eq}}{x} : \app{f}{x} = \app{g}{x}$}
1302 \RightLabel{(equality reflection)}
1303 \UnaryInfC{$\Gamma; x : A \vdash \app{f}{x} \defeq \app{g}{x}$}
1304 \RightLabel{(congruence for $\lambda$)}
1305 \UnaryInfC{$\Gamma \vdash \abs{x : A}{\app{f}{x}} \defeq \abs{x : A}{\app{g}{x}}$}
1306 \RightLabel{($\eta$-law)}
1307 \UnaryInfC{$\Gamma \vdash f \defeq g$}
1308 \RightLabel{($\lccon{refl}$)}
1309 \UnaryInfC{$\Gamma \vdash f = g$}
1312 Since the above is possible, theories that include the equality reflection rule
1313 are often called `Extensional Type Theories', or ETTs. A notable exponent of
1314 this discipline is the NuPRL system \citep{Constable86}. Moreover, equality
1315 reflection simplifies $\lcfun{subst}$-like operations, since if we have $t = m$
1316 and $\app{A}{t}$, then by equality reflection clearly $\app{A}{t} \defeq
1319 However equality reflection comes at a great price. The first hit is that it is
1320 now unsafe to compute under binders, since we can send the type checker into a
1321 loop given that under binders we can have any equality proof we might want
1322 (think about what happens with $\abs{x : \bot}{\dotsb}$), and thus we can
1323 convince the type checker that a term has any type we might want. Secondly,
1324 equality reflection is not syntax directed, thus the type checker would need to
1325 `invent' proofs of propositional equality to prove two terms definitionally
1326 equal, rendering the type checking process undecidable. Thus the type checker
1327 needs to carry complete derivations for each typing judgement, instead of
1328 relying on terms only.
1330 \subsection{Observational equality}
1332 A recent development by \cite{Altenkirch2007} promises to keep the well
1333 behavedness of ITT while being able to gain many useful equality proofs,
1334 including function extensionality. Starting from a theory similar to the one
1335 presented in section \ref{sec:itt} but with only $\lcset{0}$, a propositional
1336 subuniverse of $\lcsetz$ is introduced, plus a `decoding' function:
1338 \newcommand{\lcprop}{\lccon{Prop}}
1341 \begin{tabular}{c c c}
1342 \AxiomC{\phantom{1em}}
1343 \UnaryInfC{$\Gamma \vdash \lcprop : \lcsetz$}
1345 \UnaryInfC{\phantom{1em}}
1348 \AxiomC{\phantom{1em}}
1349 \UnaryInfC{$\Gamma \vdash \bot : \lcprop$}
1351 \UnaryInfC{$\Gamma \vdash \top : \lcprop$}
1354 \AxiomC{$\Gamma \vdash P : \lcprop$}
1355 \AxiomC{$\Gamma \vdash Q : \lcprop$}
1356 \BinaryInfC{$\Gamma \vdash P \wedge Q : \lcprop$}
1358 \UnaryInfC{\phantom{1em}}
1365 \AxiomC{$\Gamma \vdash S : \lcsetz$}
1366 \AxiomC{$\Gamma \vdash q : \lcprop$}
1367 \BinaryInfC{$\Gamma \vdash p \wedge q : \lcprop$}
1369 \UnaryInfC{\phantom{1em}}
1374 \section{What to do}
1377 \bibliographystyle{authordate1}
1378 \bibliography{background}
1382 \label{app:agda-code}
1388 \lstinputlisting{background.agda}