1 \documentclass[article, a4paper]{article}
2 \usepackage[T1]{fontenc}
5 \usepackage[normalem]{ulem}
7 \usepackage{subcaption}
9 %% -----------------------------------------------------------------------------
11 %% \usepackage[osf]{libertine}
12 %% \usepackage{helvet}
13 %% \usepackage{lmodern}
14 %% \IfFileExists{microtype.sty}{\usepackage{microtype}}{}
16 %% -----------------------------------------------------------------------------
19 % \usetikzlibrary{positioning}
20 %% \usetikzlibrary{shapes}
21 %% \usetikzlibrary{arrows}
22 %% \usepackage{tikz-cd}
23 %% \usepackage{pgfplots}
26 %% -----------------------------------------------------------------------------
28 \usepackage{amssymb,amsmath}
30 \usepackage{turnstile}
31 \usepackage{centernot}
33 %% -----------------------------------------------------------------------------
35 \usepackage{bussproofs}
37 \usepackage[export]{adjustbox}
40 %% -----------------------------------------------------------------------------
45 %% \setcounter{secnumdepth}{0}
47 %% -----------------------------------------------------------------------------
48 % We will generate all images so they have a width \maxwidth. This means
49 % that they will get their normal width if they fit onto the page, but
50 % are scaled down if they would overflow the margins.
53 \ifdim\Gin@nat@width>\linewidth\linewidth
54 \else\Gin@nat@width\fi
58 %% -----------------------------------------------------------------------------
61 setpagesize=false, % page size defined by xetex
62 unicode=false, % unicode breaks when used with xetex
69 pdfauthor={Francesco Mazzoli <fm2209@ic.ac.uk>},
70 pdftitle={The Paths Towards Observational Equality},
75 % Make links footnotes instead of hotlinks:
76 % \renewcommand{\href}[2]{#2\footnote{\url{#1}}}
78 % avoid problems with \sout in headers with hyperref:
79 \pdfstringdefDisableCommands{\renewcommand{\sout}{}}
81 \title{The Paths Towards Observational Equality}
82 \author{Francesco Mazzoli \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{<fm2209@ic.ac.uk>}}}
89 \setlength{\tabcolsep}{12pt}
91 The marriage between programming and logic has been a very fertile one. In
92 particular, since the simply typed lambda calculus (STLC), a number of type
93 systems have been devised with increasing expressive power.
95 In the next sections I will give a very brief overview of STLC, and then
96 describe how to augment it to reach the theory I am interested in,
97 Inutitionistic Type Theory (ITT), also known as Martin-L\"{o}f Type Theory after
98 its inventor. The exposition is quite dense since there is a lot of material to
99 cover, for a more complete treatment of the material the reader can refer to
100 \citep{Thompson1991, Pierce2002}.
102 I will then explain why equality has been a tricky business in these theories,
103 and talk about the various attempts have been made to make the situation better.
104 One interesting development has recently emerged: Observational Type theory. I
105 propose to explore the ways to turn these ideas into useful practices for
106 programming and theorem proving.
108 \section{Simple and not-so-simple types}
110 \subsection{Untyped $\lambda$-calculus}
112 Along with Turing's machines, the earliest attempts to formalise computation
113 lead to the $\lambda$-calculus \citep{Church1936}. This early programming
114 language encodes computation with a minimal sintax and most notably no `data'
115 in the traditional sense, but just functions.
117 The syntax of $\lambda$-terms consists of just three things: variables,
118 abstractions, and applications:
120 \newcommand{\appspace}{\hspace{0.07cm}}
121 \newcommand{\app}[2]{#1\appspace#2}
122 \newcommand{\absspace}{\hspace{0.03cm}}
123 \newcommand{\abs}[2]{\lambda #1\absspace.\absspace#2}
124 \newcommand{\termt}{t}
125 \newcommand{\termm}{m}
126 \newcommand{\termn}{n}
127 \newcommand{\termp}{p}
128 \newcommand{\termf}{f}
129 \newcommand{\separ}{\ \ |\ \ }
130 \newcommand{\termsyn}{\mathit{term}}
131 \newcommand{\axname}[1]{\textbf{#1}}
132 \newcommand{\axdesc}[2]{\axname{#1} \fbox{$#2$}}
133 \newcommand{\lcsyn}[1]{\mathrm{\underline{#1}}}
138 \termsyn & ::= & x \separ (\abs{x}{\termsyn}) \separ (\app{\termsyn}{\termsyn}) \\
139 x & \in & \text{Some enumerable set of symbols, e.g.}\ \{x, y, z, \dots , x_1, x_2, \dots\}
144 % I will omit parethesis in the usual manner. %TODO explain how
146 I will use $\termt,\termm,\termn,\dots$ to indicate a generic term, and $x,y$
147 for variables. I will also assume that all variable names in a term are unique
148 to avoid problems with name capturing. Intuitively, abstractions
149 ($\abs{x}{\termt}$) introduce functions with a named parameter ($x$), and
150 applications ($\app{\termt}{\termm}$) apply a function ($\termt$) to an argument
153 The `applying' is more formally explained with a reduction rule:
155 \newcommand{\bred}{\leadsto}
156 \newcommand{\bredc}{\bred^*}
159 \axdesc{reduction}{\termsyn \bred \termsyn}
160 $$\app{(\abs{x}{\termt})}{\termm} \bred \termt[\termm ]$$
163 Where $\termt[\termm ]$ expresses the operation that substitutes all
164 occurrences of $x$ with $\termm$ in $\termt$. In the future, I will use
165 $[\termt]$ as an abbreviation for $[\termt ]$. In the systems presented, the
166 $\bred$ relation also includes reduction of subterms, for example if $\termt
167 \bred \termm$ then $\app{\termt}{\termn} \bred \app{\termm}{\termn}$, and so on.
169 % % TODO put the trans closure
171 These few elements are of remarkable expressiveness, and in fact Turing
172 complete. As a corollary, we must be able to devise a term that reduces forever
173 (`loops' in imperative terms):
175 \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
177 Terms that can be reduced only a finite number of times (the non-looping ones)
178 are said to be \emph{normalising}, and the `final' term is called \emph{normal
179 form}. These concepts (reduction and normal forms) will run through all the
182 \subsection{The simply typed $\lambda$-calculus}
188 One way to `discipline' $\lambda$-terms is to assign \emph{types} to them, and
189 then check that the terms that we are forming make sense given our typing rules
192 We wish to introduce rules of the form $\Gamma \vdash \termt : \tya$, which
193 reads `in context $\Gamma$, term $\termt$ has type $\tya$'.
195 The syntax for types is as follows:
197 \newcommand{\tyarr}{\to}
198 \newcommand{\tysyn}{\mathit{type}}
199 \newcommand{\ctxsyn}{\mathit{context}}
200 \newcommand{\emptyctx}{\cdot}
204 $$\tysyn ::= x \separ \tysyn \tyarr \tysyn$$
207 I will use $\tya,\tyb,\dots$ to indicate a generic type.
209 A context $\Gamma$ is a map from variables to types. We use the notation
210 $\Gamma; x : \tya$ to augment it, and to `extract' pairs from it.
212 Predictably, $\tya \tyarr \tyb$ is the type of a function from $\tya$ to
213 $\tyb$. We need to be able to decorate our abstractions with
214 types\footnote{Actually, we don't need to: computers can infer the right type
215 easily, but that is another story.}:
218 $$\termsyn ::= x \separ (\abs{x : \tysyn}{\termsyn}) \separ (\app{\termsyn}{\termsyn})$$
220 Now we are ready to give the typing judgements:
223 \axdesc{typing}{\Gamma \vdash \termsyn : \tysyn}
227 \begin{tabular}{c c c}
229 \UnaryInfC{$\Gamma; x : \tya \vdash x : \tya$}
232 \AxiomC{$\Gamma; x : \tya \vdash \termt : \tyb$}
233 \UnaryInfC{$\Gamma \vdash \abs{x : \tya}{\termt} : \tya \tyarr \tyb$}
240 \AxiomC{$\Gamma \vdash \termt : \tya \tyarr \tyb$}
241 \AxiomC{$\Gamma \vdash \termm : \tya$}
242 \BinaryInfC{$\Gamma \vdash \app{\termt}{\termm} : \tyb$}
247 This typing system takes the name of `simply typed lambda calculus' (STLC),
248 and enjoys a number of properties. Two of them are expected in most type
249 systems: %TODO add credit to pierce
251 \item[Progress] A well-typed term is not stuck - either it is a value or it can
252 take a step according to the evaluation rules. With `value' we mean a term
253 whose subterms (including itself) don't appear to the left of the $\bred$
255 \item[Preservation] If a well-typed term takes a step of evaluation, then the
256 resulting term is also well typed.
259 However, STLC buys us much more: every well-typed term
260 is normalising. It is easy to see that we can't fill the blanks if we want to
261 give types to the non-normalising term shown before:
263 \app{(\abs{x : ?}{\app{x}{x}})}{(\abs{x : ?}{\app{x}{x}})}
266 \newcommand{\lcfix}[2]{\mathsf{fix} \appspace #1\absspace.\absspace #2}
268 This makes the STLC Turing incomplete. We can recover the ability to loop by
269 adding a combinator that recurses:
271 \termsyn ::= \dots \separ \lcfix{x : \tysyn}{\termsyn}
275 \AxiomC{$\Gamma;x : \tya \vdash \termt : \tya$}
276 \UnaryInfC{$\Gamma \vdash \lcfix{x : \tya}{\termt} : \tya$}
280 \lcfix{x : \tya}{\termt} \bred \termt[(\lcfix{x : \tya}{\termt}) ]
283 However, we will keep STLC without such a facility. In the next section we shall
284 see why that is preferable for our needs.
286 \subsection{The Curry-Howard correspondence}
287 \label{sec:curry-howard}
289 \newcommand{\lcunit}{\mathsf{\langle\rangle}}
291 It turns out that the STLC can be seen a natural deduction system for
292 propositional logic. Terms are proofs, and their types are the propositions
293 they prove. This remarkable fact is known as the Curry-Howard correspondence,
296 The `arrow' ($\to$) type corresponds to implication. If we wished to
297 prove that $(\tya \tyarr \tyb) \tyarr (\tyb \tyarr \tyc) \tyarr (\tya
298 \tyarr \tyc)$, all we need to do is to devise a $\lambda$-term that has the
301 \abs{f : (\tya \tyarr \tyb)}{\abs{g : (\tyb \tyarr \tyc)}{\abs{x : \tya}{\app{g}{(\app{f}{x})}}}}
303 That is, function composition. We might want extend our bare lambda calculus
304 with a couple of terms to make our natural deduction more pleasant to use. For
305 example, tagged unions (\texttt{Either} in Haskell) are disjunctions, and tuples
306 (or products) are conjunctions. We also want to be able to express falsity, and
307 that is done by introducing a type inhabited by no terms. If evidence of such a
308 type is presented, then we can derive any type, which expresses absurdity.
309 Conversely, $\top$ is the type with just one trivial element, $\lcunit$.
311 \newcommand{\lcinl}{\mathsf{inl}\appspace}
312 \newcommand{\lcinr}{\mathsf{inr}\appspace}
313 \newcommand{\lccase}[3]{\lcsyn{case}\appspace#1\appspace\lcsyn{of}\appspace#2\appspace#3}
314 \newcommand{\lcfst}{\mathsf{fst}\appspace}
315 \newcommand{\lcsnd}{\mathsf{snd}\appspace}
316 \newcommand{\orint}{\vee I_{1,2}}
317 \newcommand{\orintl}{\vee I_{1}}
318 \newcommand{\orintr}{\vee I_{2}}
319 \newcommand{\orel}{\vee E}
320 \newcommand{\andint}{\wedge I}
321 \newcommand{\andel}{\wedge E_{1,2}}
322 \newcommand{\botel}{\bot E}
323 \newcommand{\lcabsurd}{\mathsf{absurd}\appspace}
324 \newcommand{\lcabsurdd}[1]{\mathsf{absurd}_{#1}\appspace}
329 \termsyn & ::= & \dots \\
330 & | & \lcinl \termsyn \separ \lcinr \termsyn \separ \lccase{\termsyn}{\termsyn}{\termsyn} \\
331 & | & (\termsyn , \termsyn) \separ \lcfst \termsyn \separ \lcsnd \termsyn \\
333 \tysyn & ::= & \dots \separ \tysyn \vee \tysyn \separ \tysyn \wedge \tysyn \separ \bot \separ \top
337 \axdesc{typing}{\Gamma \vdash \termsyn : \tysyn}
339 \AxiomC{$\Gamma \vdash \termt : \tya$}
340 \RightLabel{$\orint$}
341 \UnaryInfC{$\Gamma \vdash \lcinl \termt : \tya \vee \tyb$}
343 \UnaryInfC{$\Gamma \vdash \lcinr \termt : \tyb \vee \tya$}
346 \AxiomC{$\Gamma \vdash \termt : \tya \vee \tyb$}
347 \AxiomC{$\Gamma \vdash \termm : \tya \tyarr \tyc$}
348 \AxiomC{$\Gamma \vdash \termn : \tyb \tyarr \tyc$}
350 \TrinaryInfC{$\Gamma \vdash \lccase{\termt}{\termm}{\termn} : \tyc$}
354 \AxiomC{$\Gamma \vdash \termt : \tya$}
355 \AxiomC{$\Gamma \vdash \termm : \tyb$}
356 \RightLabel{$\andint$}
357 \BinaryInfC{$\Gamma \vdash (\tya , \tyb) : \tya \wedge \tyb$}
360 \AxiomC{$\Gamma \vdash \termt : \tya \wedge \tyb$}
361 \RightLabel{$\andel$}
362 \UnaryInfC{$\Gamma \vdash \lcfst \termt : \tya$}
364 \UnaryInfC{$\Gamma \vdash \lcsnd \termt : \tyb$}
371 \AxiomC{$\Gamma \vdash \termt : \bot$}
372 \RightLabel{$\botel$}
373 \UnaryInfC{$\Gamma \vdash \lcabsurdd{\tya} \termt : \tya$}
377 \RightLabel{$\top I$}
378 \UnaryInfC{$\Gamma \vdash \lcunit : \top$}
383 \axdesc{reduction}{\termsyn \bred \termsyn}
385 \lccase{(\lcinl \termt)}{\termm}{\termn} & \bred & \app{\termm}{\termt} \\
386 \lccase{(\lcinr \termt)}{\termm}{\termn} & \bred & \app{\termn}{\termt} \\
387 \lcfst (\termt , \termm) & \bred & \termt \\
388 \lcsnd (\termt , \termm) & \bred & \termm
392 With these rules, our STLC now looks remarkably similar in power and use to the
393 natural deduction we already know. $\neg A$ can be expressed as $A \tyarr
394 \bot$. However, there is an important omission: there is no term of the type $A
395 \vee \neg A$ (excluded middle), or equivalently $\neg \neg A \tyarr A$ (double
396 negation), or indeed any term with a type equivalent to those.
398 This has a considerable effect on our logic and it's no coincidence, since there
399 is no obvious computational behaviour for laws like the excluded middle.
400 Theories of this kind are called \emph{intuitionistic}, or \emph{constructive},
401 and all the systems analysed will have this characteristic since they build on
402 the foundation of the STLC\footnote{There is research to give computational
403 behaviour to classical logic, but we will not touch those subjects.}.
405 Finally, going back to our $\mathsf{fix}$ combinator, it's now easy to see how
406 we would want to exclude such a thing if we want to use STLC as a logic, since
407 it allows us to prove everything: $(\lcfix{x : \tya}{x}) : \tya$ clearly works
408 for any $A$! This is a crucial point: in general we wish to have systems that
409 do not let the user devise a term of type $\bot$, otherwise our logic will be
410 unsound\footnote{Obviously such a term can be present under a $\lambda$.}.
412 \subsection{Extending the STLC}
414 \newcommand{\lctype}{\mathsf{Type}}
415 \newcommand{\lcite}[3]{\lcsyn{if}\appspace#1\appspace\lcsyn{then}\appspace#2\appspace\lcsyn{else}\appspace#3}
416 \newcommand{\lcbool}{\mathsf{Bool}}
417 \newcommand{\lcforallz}[2]{\forall #1 \absspace.\absspace #2}
418 \newcommand{\lcforall}[3]{\forall #1 : #2 \absspace.\absspace #3}
419 \newcommand{\lcexists}[3]{\exists #1 : #2 \absspace.\absspace #3}
421 The STLC can be made more expressive in various ways. Henk Barendregt
422 succinctly expressed geometrically how we can expand our type system:
426 & \lambda\omega \ar@{-}[rr]\ar@{-}'[d][dd]
427 & & \lambda C \ar@{-}[dd]
429 \lambda2 \ar@{-}[ur]\ar@{-}[rr]\ar@{-}[dd]
430 & & \lambda P2 \ar@{-}[ur]\ar@{-}[dd]
432 & \lambda\underline\omega \ar@{-}'[r][rr]
433 & & \lambda P\underline\omega
435 \lambda{\to} \ar@{-}[rr]\ar@{-}[ur]
436 & & \lambda P \ar@{-}[ur]
439 Here $\lambda{\to}$, in the bottom left, is the STLC. From there can move along
442 \item[Terms depending on types (towards $\lambda{2}$)] In other words, we can
443 quantify over types in our type signatures: $(\abs{A : \lctype}{\abs{x : A}{x}}) : \lcforallz{A}{A \tyarr A}$. The first and most famous instance of this idea
444 has been System F. This gives us a form of polymorphism and has been wildly
445 successful, also thanks to a well known inference algorithm for a restricted
446 version of System F known as Hindley-Milner. Languages like Haskell and SML
447 are based on this discipline.
448 \item[Types depending on types (towards $\lambda{\underline{\omega}}$)] In other
449 words, we have type operators: $(\abs{A : \lctype}{\abs{R : \lctype}{(A \to R) \to R}}) : \lctype \to \lctype \to \lctype$.
450 \item[Types depending on terms (towards $\lambda{P}$)] Also known as `dependent
451 types', give great expressive power: $(\abs{x : \lcbool}{\lcite{x}{\mathbb{N}}{\mathbb{Q}}}) : \lcbool \to \lctype$.
454 All the systems preserve the properties that make the STLC well behaved (some of
455 which I haven't mentioned yet). The system we are going to focus on,
456 Intuitionistic Type Theory, has all of the above additions, and thus would sit
457 where $\lambda{C}$ sits in the `$\lambda$-cube' above.
459 \section{Intuitionistic Type Theory}
461 \newcommand{\lcset}[1]{\mathsf{Type}_{#1}}
462 \newcommand{\lcsetz}{\mathsf{Type}}
463 \newcommand{\defeq}{\equiv}
465 \subsection{A Bit of History}
467 Logic frameworks and programming languages based on type theory have a long
468 history. Per Martin-L\"{o}f described the first version of his theory in 1971,
469 but then revised it since the original version was too impredicative and thus
470 inconsistent\footnote{In the early version $\lcsetz : \lcsetz$, see section
471 \ref{sec:core-tt} for an explanation on why this causes problems.}. For this
472 reason he gave a revised and consistent definition later \citep{Martin-Lof1984}.
474 A related development is the one of the polymorphic $\lambda$-calculus, and
475 specifically the previously mentioned System F, which was invented independently
476 by Girard and Reynolds. An overview can be found in \citep{Reynolds1994}. The
477 surprising fact is that while System F is impredicative it is still consistent
478 and strongly normalising. \cite{Coquand1986} Huet further extended this line of
479 work with the Calculus of Constructions (CoC).
481 \subsection{A Core Type Theory}
484 The calculus I present follows the exposition in \citep{Thompson1991}, and as
485 said previously is quite close to the original formulation of predicative ITT as
486 found in \citep{Martin-Lof1984}.
491 \termsyn & ::= & x \\
492 & | & \lcforall{x}{\termsyn}{\termsyn} \separ \abs{x : \termsyn}{\termsyn} \separ \app{\termsyn}{\termsyn} \\
493 & | & \lcexists{x}{\termsyn}{\termsyn} \separ (\termsyn , \termsyn)_{x.\termsyn} \separ \lcfst \termsyn \separ \lcsnd \termsyn \\
494 & | & \bot \separ \lcabsurd_{\termsyn} \termsyn \\
499 \axdesc{typing}{\Gamma \vdash \termsyn : \termsyn}
503 \begin{tabular}{c c c}
506 \UnaryInfC{$\Gamma;x : \tya \vdash x : \tya$}
509 \AxiomC{$\Gamma \vdash \termt : \bot$}
510 \UnaryInfC{$\Gamma \vdash \lcabsurdd{\tya} \termt : \tya$}
513 \AxiomC{$\Gamma \vdash \termt : \tya$}
514 \AxiomC{$\tya \defeq \tyb$}
515 \BinaryInfC{$\Gamma \vdash \termt : \tyb$}
522 \AxiomC{$\Gamma;x : \tya \vdash \termt : \tya$}
523 \UnaryInfC{$\Gamma \vdash \abs{x : \tya}{\termt} : \lcforall{x}{\tya}{\tyb}$}
526 \AxiomC{$\Gamma \vdash \termt : \lcforall{x}{\tya}{\tyb}$}
527 \AxiomC{$\Gamma \vdash \termm : \tya$}
528 \BinaryInfC{$\Gamma \vdash \app{\termt}{\termm} : \tyb[\termm ]$}
535 \AxiomC{$\Gamma \vdash \termt : \tya$}
536 \AxiomC{$\Gamma \vdash \termm : \tyb[\termt ]$}
537 \BinaryInfC{$\Gamma \vdash (\termt, \termm)_{x.\tyb} : \lcexists{x}{\tya}{\tyb}$}
540 \AxiomC{$\Gamma \vdash \termt: \lcexists{x}{\tya}{\tyb}$}
541 \UnaryInfC{$\hspace{0.7cm} \Gamma \vdash \lcfst \termt : \tya \hspace{0.7cm}$}
543 \UnaryInfC{$\Gamma \vdash \lcsnd \termt : \tyb[\lcfst \termt ]$}
551 \UnaryInfC{$\Gamma \vdash \lcset{n} : \lcset{n + 1}$}
554 \AxiomC{$\Gamma \vdash \tya : \lcset{n}$}
555 \AxiomC{$\Gamma; x : \tya \vdash \tyb : \lcset{m}$}
556 \BinaryInfC{$\Gamma \vdash \lcforall{x}{\tya}{\tyb} : \lcset{n \sqcup m}$}
558 \UnaryInfC{$\Gamma \vdash \lcexists{x}{\tya}{\tyb} : \lcset{n \sqcup m}$}
564 \axdesc{reduction}{\termsyn \bred \termsyn}
566 \app{(\abs{x}{\termt})}{\termm} & \bred & \termt[\termm ] \\
567 \lcfst (\termt, \termm) & \bred & \termt \\
568 \lcsnd (\termt, \termm) & \bred & \termm
572 There are a lot of new factors at play here. The first thing to notice is that
573 the separation between types and terms is gone. All we have is terms, that
574 include both values (terms of type $\lcset{0}$) and types (terms of type
575 $\lcset{n}$, with $n > 0$). This change is reflected in the typing rules.
576 While in the STLC values and types are kept well separated (values never go
577 `right of the colon'), in ITT types can freely depend on values.
579 This relation is expressed in the typing rules for $\forall$ and $\exists$: if a
580 function has type $\lcforall{x}{\tya}{\tyb}$, $\tyb$ can depend on $x$.
581 Examples will make this clearer once some base types are added in section
582 \ref{sec:base-types}.
584 $\forall$ and $\exists$ are at the core of the machinery of ITT:
587 \item[`forall' ($\forall$)] is a generalisation of $\tyarr$ in the STLC and
588 expresses universal quantification in our logic. In the literature this is
589 also known as `dependent product' and shown as $\Pi$, following the
590 interpretation of functions as infinitary products. We will just call it
591 `dependent function', reserving `product' for $\exists$.
593 \item[`exists' ($\exists$)] is a generalisation of $\wedge$ in the extended
594 STLC of section \ref{sec:curry-howard}, and thus we will call it `dependent
595 product'. Like $\wedge$, it is formed by providing a pair of things. In our
596 logic, it represents existential quantification.
598 For added confusion, in the literature that calls $\forall$ $\Pi$, $\exists$
599 is often named `dependent sum' and shown as $\Sigma$. This is following the
600 interpretation of $\exists$ as a generalised, infinitary $\vee$, where the
601 first element of the pair is the `tag' that decides which type the second
605 Another thing to notice is that types are very `first class': we are free to
606 create functions that accept and return types. For this reason we $\defeq$ as
607 the smallest equivalence relation extending $\bredc$, where $\bredc$ is the
608 reflexive transitive closure of $\bred$; and we treat types that are equal
609 according to $\defeq$ as the same. Another way of seeing $\defeq$ is this: when
610 we want to compare two types for equality, we reduce them as far as possible and
611 then check if they are equal\footnote{Note that when comparing terms we do it up
612 to $\alpha$-renaming. That is, we do not consider relabelling of variables as
613 a difference - for example $\abs{x : A}{x} \defeq \abs{y : A}{y}$.}. This
614 works since not only each term has a normal form (ITT is strongly normalising),
615 but the normal form is also unique; or in other words $\bred$ is confluent (if
616 $\termt \bredc \termm$ and $\termt \bredc \termn$, then $\termm \bredc \termp$
617 and $\termn \bredc \termp$). This measure makes sure that, for instance,
618 $\app{(\abs{x : \lctype}{x})}{\lcbool} \defeq \lcbool$. The theme of equality
619 is central and will be analysed better later.
621 The theory presented is \emph{stratified}. We have a hierarchy of types
622 $\lcset{0} : \lcset{1} : \lcset{2} : \dots$, so that there is no `type of all
623 types', and our theory is predicative. The layers of the hierarchy are called
624 `universes'. $\lcsetz : \lcsetz$ ITT is inconsistent due to Girard's paradox
625 \citep{Hurkens1995}, and thus loses its well-behavedness. Some impredicativity
626 sometimes has its place, either because the theory retain good properties
627 (normalization, consistency, etc.) anyway, like in System F and CoC; or because
628 we are at a stage at which we do not care - we will see instances of the last
629 motivation later. Moreover, universes can be inferred mechanically
630 \citep{Pollack1990}. It is also convenient to have a \emph{cumulative} theory,
631 where $\lcset{n} : \lcset{m}$ iff $n < m$. We eschew these measures to keep the
634 Lastly, the theory I present is fully explicit in the sense that the user has to
635 specify every type when forming abstractions, products, etc. This can be a
636 great burden if one wants to use the theory directly. Complete inference is
637 undecidable (which is hardly surprising considering the role that types play)
638 but partial inference (also called `bidirectional type checking' in this
639 context) in the style of \citep{Pierce2000} will have to be deployed in a
640 practical system. When showing examples obvious types will be omitted when this
641 can be done without loss of clarity.
643 Note that the Curry-Howard correspondence runs through ITT as it did with the
644 STLC with the difference that ITT corresponds to an higher order propositional
647 % TODO describe abbreviations somewhere
648 % I will use various abbreviations:
650 % \item $\lcsetz$ for $\lcset{0}$
651 % \item $\tya \tyarr \tyb$ for $\lcforall{-}{\tya}{\tyb}$, when $\tyb$ does not
652 % depend on the value of type $\tya$
655 \subsection{Base Types}
656 \label{sec:base-types}
658 \newcommand{\lctrue}{\mathsf{true}}
659 \newcommand{\lcfalse}{\mathsf{false}}
660 \newcommand{\lcw}[3]{\mathsf{W} #1 : #2 \absspace.\absspace #3}
661 \newcommand{\lcnode}[4]{#1 \lhd_{#2 . #3} #4}
662 \newcommand{\lcnodez}[2]{#1 \lhd #2}
663 \newcommand{\lcited}[5]{\lcsyn{if}\appspace#1/#2\appspace.\appspace#3\appspace\lcsyn{then}\appspace#4\appspace\lcsyn{else}\appspace#5}
664 \newcommand{\lcrec}[4]{\lcsyn{rec}\appspace#1/#2\appspace.\appspace#3\appspace\lcsyn{with}\appspace#4}
665 \newcommand{\lcrecz}[2]{\lcsyn{rec}\appspace#1\appspace\lcsyn{with}\appspace#2}
666 \newcommand{\AxiomL}[1]{\Axiom$\fCenter #1$}
667 \newcommand{\UnaryInfL}[1]{\UnaryInf$\fCenter #1$}
669 While the ITT presented is a fairly complete logic, it is not that useful for
670 programming. If we wish to make it better, we can add some base types to
671 represent the data structures we know and love, such as numbers, lists, and
672 trees. Apart from some unsurprising data types, we introduce $\mathsf{W}$, a
673 very general tree-like structure useful to represent inductively defined types.
678 \termsyn & ::= & ... \\
679 & | & \top \separ \lcunit \\
680 & | & \lcbool \separ \lctrue \separ \lcfalse \separ \lcited{\termsyn}{x}{\termsyn}{\termsyn}{\termsyn} \\
681 & | & \lcw{x}{\termsyn}{\termsyn} \separ \lcnode{\termsyn}{x}{\termsyn}{\termsyn} \separ \lcrec{\termsyn}{x}{\termsyn}{\termsyn}
684 \axdesc{typing}{\Gamma \vdash \termsyn : \termsyn}
688 \begin{tabular}{c c c}
690 \UnaryInfC{$\hspace{0.2cm}\Gamma \vdash \top : \lcset{0} \hspace{0.2cm}$}
692 \UnaryInfC{$\Gamma \vdash \lcbool : \lcset{0}$}
696 \UnaryInfC{$\Gamma \vdash \lcunit : \top$}
700 \RightLabel{$\lcbool I_{1,2}$}
701 \UnaryInfC{$\Gamma \vdash \lctrue : \lcbool$}
703 \UnaryInfC{$\Gamma \vdash \lcfalse : \lcbool$}
710 \AxiomC{$\Gamma \vdash \termt : \lcbool$}
711 \AxiomC{$\Gamma \vdash \termm : \tya[\lctrue]$}
712 \AxiomC{$\Gamma \vdash \termn : \tya[\lcfalse]$}
713 \TrinaryInfC{$\Gamma \vdash \lcited{\termt}{x}{\tya}{\termm}{\termn} : \tya[\termt]$}
720 \AxiomC{$\Gamma \vdash \tya : \lcset{n}$}
721 \AxiomC{$\Gamma; x : \tya \vdash \tyb : \lcset{m}$}
722 \BinaryInfC{$\Gamma \vdash \lcw{x}{\tya}{\tyb} : \lcset{n \sqcup m}$}
729 \AxiomC{$\Gamma \vdash \termt : \tya$}
730 \AxiomC{$\Gamma \vdash \termf : \tyb[\termt ] \tyarr \lcw{x}{\tya}{\tyb}$}
731 \BinaryInfC{$\Gamma \vdash \lcnode{\termt}{x}{\tyb}{\termf} : \lcw{x}{\tya}{\tyb}$}
738 \AxiomC{$\Gamma \vdash \termt: \lcw{x}{\tya}{\tyb}$}
740 \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}]}}$}
741 \UnaryInfC{$\Gamma \vdash \lcrec{\termt}{x}{\tyc}{\termp} : \tyc[\termt]$}
747 \axdesc{reduction}{\termsyn \bred \termsyn}
749 \lcited{\lctrue}{x}{\tya}{\termt}{\termm} & \bred & \termt \\
750 \lcited{\lcfalse}{x}{\tya}{\termt}{\termm} & \bred & \termm \\
751 \lcrec{\lcnodez{\termt}{\termf}}{x}{\tya}{\termp} & \bred & \app{\app{\app{\termp}{\termt}}{\termf}}{(\abs{\termm}{\lcrec{\app{f}{\termm}}{x}{\tya}{\termp}})}
755 The introduction and elimination for $\top$ and $\lcbool$ are unsurprising.
756 Note that in the $\lcite{\dotsb}{\dotsb}{\dotsb}$ construct the type of the
757 branches are dependent on the value of the conditional.
759 The rules for $\mathsf{W}$, on the other hand, are quite an eyesore. The idea
760 behind $\mathsf{W}$ types is to build up `trees' where shape of the number of
761 `children' of each node is dependent on the value in the node. This is
762 captured by the $\lhd$ constructor, where the argument on the left is the value,
763 and the argument on the right is a function that returns a child for each
764 possible value of $\tyb[\text{node value}]$, if $\lcw{x}{\tya}{\tyb}$. The
765 recursor $\lcrec{\termt}{x}{\tyc}{\termp}$ uses $p$ to inductively prove that
766 $\tyc[\termt]$ holds.
768 \subsection{Some examples}
770 Now we can finally provide some meaningful examples. I will use some
771 abbreviations and convenient syntax:
773 \item $\_\mathit{operator}\_$ to define infix operators
774 \item $\abs{\{x : \tya\}}{\dotsb}$ to define an abstraction that I will not
775 explicitly apply since the $x$ can be inferred easily.
776 \item $\abs{x\appspace y\appspace z : \tya}{\dotsb}$ to define multiple abstractions at the same
778 \item I will omit the explicit typing when forming $\exists$ or $\mathsf{W}$,
779 and when eliminating $\lcbool$, since the types are almost always clear and
780 writing them each time is extremely cumbersome.
783 \subsubsection{Sum types}
785 We would like to recover our sum type, or disjunction, $\vee$. This is easily
788 \_\vee\_ & = & \abs{\tya\appspace\tyb : \lcsetz}{\lcexists{x}{\lcbool}{\lcite{x}{\tya}{\tyb}}} \\
789 \lcinl & = & \abs{\{\tya\appspace\tyb : \lcsetz\}}{\abs{x : \tya \vee \tyb}{(\lctrue, x)}} \\
790 \lcinr & = & \abs{\{\tya\appspace\tyb : \lcsetz\}}{\abs{x : \tya \vee \tyb}{(\lcfalse, x)}} \\
791 \mathsf{case} & = & \abs{\{\tya\appspace\tyb\appspace\tyc : \lcsetz\}}{\abs{x : \tya \vee \tyb}{\abs{f : \tya \tyarr \tyc}{\abs{g : \tyb \tyarr \tyc}{ \\
792 & & \hspace{0.5cm} \app{(\lcited{\lcfst x}{b}{(\lcite{b}{A}{B}) \tyarr C}{f}{g})}{(\lcsnd x)}}}}}
794 What is going on here? We are using $\exists$ with $\lcbool$ as a tag, so that
795 we can choose between one of two types in the second element. In
796 $\mathsf{case}$ we use $\lcite{\lcfst x}{\dotsb}{\dotsb}$ to discriminate on the
797 tag, that is, the first element of $x : \tya \vee \tyb$. If the tag is true,
798 then we know that the second element is of type $\tya$, and we will apply $f$.
799 The same applies to the other branch, with $\tyb$ and $g$.
801 \subsubsection{Naturals and similarly lists}
803 Now it's time to showcase the power of $\mathsf{W}$ types.
806 \mathsf{Nat} & = & \lcw{b}{\lcbool}{\abs{b}{\lcite{b}{\top}{\bot}}} \\
807 \mathsf{zero} & = & \lcfalse \lhd \abs{z}{\lcabsurd z} \\
808 \mathsf{suc} & = & \abs{n}{(\lctrue \lhd \abs{\_}{n})} \\
809 \mathsf{plus} & = & \abs{x\appspace y}{\lcrecz{x}{\abs{b}{\lcite{b}{\abs{\_\appspace f}{\app{\mathsf{suc}}{(\app{f}{\lcunit})}}}{\abs{\_\appspace\_}{y}}}}}
812 \bibliographystyle{authordate1}
813 \bibliography{background}