docs/background.tex

   1 \documentclass[article, a4paper]{article}
   2 \usepackage[T1]{fontenc}
   3 \usepackage{fixltx2e}
   4 \usepackage{enumitem}
   5 \usepackage[normalem]{ulem}
   6 \usepackage{graphicx}
   7 \usepackage{subcaption}
   8
   9 %% -----------------------------------------------------------------------------
  10 %% Fonts
  11 %% \usepackage[osf]{libertine}
  12 %% \usepackage{helvet}
  13 %% \usepackage{lmodern}
  14 %% \IfFileExists{microtype.sty}{\usepackage{microtype}}{}
  15
  16 %% -----------------------------------------------------------------------------
  17 %% Diagrams
  18 % \usepackage{tikz}
  19 % \usetikzlibrary{positioning}
  20 %% \usetikzlibrary{shapes}
  21 %% \usetikzlibrary{arrows}
  22 %% \usepackage{tikz-cd}
  23 %% \usepackage{pgfplots}
  24 \usepackage[all]{xy}
  25
  26 %% -----------------------------------------------------------------------------
  27 %% Symbols
  28 \usepackage{amssymb,amsmath}
  29 \usepackage{wasysym}
  30 \usepackage{turnstile}
  31 \usepackage{centernot}
  32
  33 %% -----------------------------------------------------------------------------
  34 %% Utils
  35 \usepackage{bussproofs}
  36 \usepackage{umoline}
  37 \usepackage[export]{adjustbox}
  38 \usepackage{multicol}
  39
  40 %% Numbering depth
  41 %% \setcounter{secnumdepth}{0}
  42
  43 %% -----------------------------------------------------------------------------
  44 % We will generate all images so they have a width \maxwidth. This means
  45 % that they will get their normal width if they fit onto the page, but
  46 % are scaled down if they would overflow the margins.
  47 \makeatletter
  48 \def\maxwidth{
  49   \ifdim\Gin@nat@width>\linewidth\linewidth
  50   \else\Gin@nat@width\fi
  51 }
  52 \makeatother
  53
  54 %% -----------------------------------------------------------------------------
  55 %% Links
  56 \usepackage[
  57   setpagesize=false, % page size defined by xetex
  58   unicode=false, % unicode breaks when used with xetex
  59   xetex
  60 ]{hyperref}
  61
  62 \hypersetup{
  63   breaklinks=true,
  64   bookmarks=true,
  65   pdfauthor={Francesco Mazzoli <fm2209@ic.ac.uk>},
  66   pdftitle={The Paths Towards Observational Equality},
  67   colorlinks=false,
  68   pdfborder={0 0 0}
  69 }
  70
  71 % Make links footnotes instead of hotlinks:
  72 \renewcommand{\href}[2]{#2\footnote{\url{#1}}}
  73
  74 % avoid problems with \sout in headers with hyperref:
  75 \pdfstringdefDisableCommands{\renewcommand{\sout}{}}
  76
  77 \title{The Paths Towards Observational Equality}
  78 \author{Francesco Mazzoli \url{<fm2209@ic.ac.uk>}}
  79 \date{December 2012}
  80
  81 \begin{document}
  82
  83 \maketitle
  84
  85 \setlength{\tabcolsep}{12pt}
  86
  87 The marriage between programming and logic has been a very fertile one.  In
  88 particular, since the simply typed lambda calculus (STLC), a number of type
  89 systems have been devised with increasing expressive power.
  90
  91 In the next sections I will give a very brief overview of STLC, and then
  92 describe how to augment it to reach the theory I am interested in,
  93 Inutitionistic Type Theory (ITT), also known as Martin-L\"{o}f Type Theory after
  94 its inventor.
  95
  96 I will then explain why equality has been a tricky business in this theories,
  97 and talk about the various attempts have been made.  One interesting development
  98 has recently emerged: Observational Type theory.  I propose to explore the ways
  99 to turn these ideas into useful practices for programming and theorem proving.
 100
 101 \section{Simple and not-so-simple types}
 102
 103 \subsection{Untyped $\lambda$-calculus}
 104
 105 Along with Turing's machines, the earliest attempts to formalise computation
 106 lead to the $\lambda$-calculus.  This early programming language encodes
 107 computation with a minimal sintax and most notably no ``data'' in the
 108 traditional sense, but just functions.
 109
 110 The syntax of $\lambda$-terms consists of just three things: variables,
 111 abstractions, and applications:
 112
 113 \newcommand{\appspace}{\hspace{0.07cm}}
 114 \newcommand{\app}[2]{#1\appspace#2}
 115 \newcommand{\absspace}{\hspace{0.03cm}}
 116 \newcommand{\abs}[2]{\lambda #1\absspace.\absspace#2}
 117 \newcommand{\termt}{t}
 118 \newcommand{\termm}{m}
 119 \newcommand{\termn}{n}
 120 \newcommand{\termp}{p}
 121 \newcommand{\termf}{f}
 122 \newcommand{\separ}{\ \ |\ \ }
 123 \newcommand{\termsyn}{\mathit{term}}
 124 \newcommand{\axname}[1]{\textbf{#1}}
 125 \newcommand{\axdesc}[2]{\axname{#1} \fbox{$#2$}}
 126
 127 \begin{center}
 128 \axname{syntax}
 129 \begin{eqnarray*}
 130   \termsyn & ::= & x \separ (\abs{x}{\termsyn}) \separ (\app{\termsyn}{\termsyn}) \\
 131          x & \in & \text{Some enumerable set of symbols, e.g.}\ \{x, y, z, \dots , x_1, x_2, \dots\}
 132 \end{eqnarray*}
 133 \end{center}
 134
 135
 136 % I will omit parethesis in the usual manner. %TODO explain how
 137
 138 I will use $\termt,\termm,\termn,\dots$ to indicate a generic term, and $x,y$
 139 for variables.  I will also assume that all variable names in a term are unique
 140 to avoid problems with name capturing.  Intuitively, abstractions
 141 ($\abs{x}{\termt}$) introduce functions with a named parameter ($x$), and
 142 applications ($\app{\termt}{\termm}$) apply a function ($\termt$) to an argument
 143 ($\termm$).
 144
 145 The ``applying'' is more formally explained with a reduction rule:
 146
 147 \newcommand{\bred}{\leadsto}
 148 \newcommand{\bredc}{\bred^*}
 149
 150 \begin{center}
 151 \axdesc{reduction}{\termsyn \bred \termsyn}
 152 $$\app{(\abs{x}{\termt})}{\termm} \bred \termt[\termm / x]$$
 153 \end{center}
 154
 155 Where $\termt[\termm / x]$ expresses the operation that substitutes all
 156 occurrences of $x$ with $\termm$ in $\termt$.  In the systems presented, the
 157 $\bred$ relation also includes reduction of subterms, for example if $\termt
 158 \bred \termm$ then $\app{\termt}{\termn} \bred \app{\termm}{\termn}$, and so on.
 159
 160 % % TODO put the trans closure
 161
 162 These few elements are of remarkable expressiveness, and in fact Turing
 163 complete.  As a corollary, we must be able to devise a term that reduces forever
 164 (``loops'' in imperative terms):
 165 \begin{equation*}
 166   \app{(\abs{x}{\app{x}{x}})}{(\abs{x}{\app{x}{x}})} \bred \app{(\abs{x}{\app{x}{x}})}{(\abs{x}{\app{x}{x}})} \bred \dots
 167 \end{equation*}
 168 Terms that can be reduced only a finite number of times (the non-looping ones)
 169 are said to be \emph{normalising}, and the ``final'' term is called \emph{normal
 170   form}.  These concepts (reduction and normal forms) will run through all the
 171 material analysed.
 172
 173 \subsection{The simply typed $\lambda$-calculus}
 174
 175 \newcommand{\tya}{A}
 176 \newcommand{\tyb}{B}
 177 \newcommand{\tyc}{C}
 178
 179 One way to ``discipline'' $\lambda$-terms is to assign \emph{types} to them, and
 180 then check that the terms that we are forming make sense given our typing rules.
 181
 182 We wish to introduce rules of the form $\Gamma \vdash \termt : \tya$, which
 183 reads ``in context $\Gamma$, term $\termt$ has type $\tya$''.
 184
 185 The syntax for types is as follows:
 186
 187 \newcommand{\tyarr}{\to}
 188 \newcommand{\tysyn}{\mathit{type}}
 189 \newcommand{\ctxsyn}{\mathit{context}}
 190 \newcommand{\emptyctx}{\cdot}
 191
 192 \begin{center}
 193   \axname{syntax}
 194    $$\tysyn ::= x \separ \tysyn \tyarr \tysyn$$
 195 \end{center}
 196
 197 I will use $\tya,\tyb,\dots$ to indicate a generic type.
 198
 199 A context $\Gamma$ is a map from variables to types.  We use the notation
 200 $\Gamma; x : \tya$ to augment it, and to ``extract'' pairs from it.
 201
 202 Predictably, $\tya \tyarr \tyb$ is the type of a function from $\tya$ to
 203 $\tyb$.  We need to be able to decorate our abstractions with
 204 types\footnote{Actually, we don't need to: computers can infer the right type
 205   easily, but that is another story.}:
 206 \begin{center}
 207   \axname{syntax}
 208    $$\termsyn ::= x \separ (\abs{x : \tysyn}{\termsyn}) \separ (\app{\termsyn}{\termsyn})$$
 209 \end{center}
 210 Now we are ready to give the typing judgements:
 211
 212 \begin{center}
 213   \axdesc{typing}{\Gamma \vdash \termsyn : \tysyn}
 214
 215   \vspace{0.5cm}
 216
 217   \begin{tabular}{c c c}
 218     \AxiomC{}
 219     \UnaryInfC{$\Gamma; x : \tya \vdash x : \tya$}
 220     \DisplayProof
 221     &
 222     \AxiomC{$\Gamma; x : \tya \vdash \termt : \tyb$}
 223     \UnaryInfC{$\Gamma \vdash \abs{x : \tya}{\termt} : \tya \tyarr \tyb$}
 224     \DisplayProof
 225   \end{tabular}
 226
 227   \vspace{0.5cm}
 228
 229   \begin{tabular}{c}
 230     \AxiomC{$\Gamma \vdash \termt : \tya \tyarr \tyb$}
 231     \AxiomC{$\Gamma \vdash \termm : \tya$}
 232     \BinaryInfC{$\Gamma \vdash \app{\termt}{\termm} : \tyb$}
 233     \DisplayProof
 234   \end{tabular}
 235 \end{center}
 236
 237 This typing system takes the name of ``simply typed lambda calculus'' (STLC),
 238 and enjoys a number of properties.  Two of them are expected in most type
 239 systems: %TODO add credit to pierce
 240 \begin{description}
 241 \item[Progress] A well-typed term is not stuck - either it is a value or it can
 242   take a step according to the evaluation rules.  With ``value'' we mean a term
 243   whose subterms (including itself) don't appear to the left of the $\bred$
 244   relation.
 245 \item[Preservation] If a well-typed term takes a step of evaluation, then the
 246   resulting term is also well typed.
 247 \end{description}
 248
 249 However, STLC buys us much more: every well-typed term
 250 is normalising.  It is easy to see that we can't fill the blanks if we want to
 251 give types to the non-normalising term shown before:
 252 \begin{equation*}
 253   \app{(\abs{x : ?}{\app{x}{x}})}{(\abs{x : ?}{\app{x}{x}})}
 254 \end{equation*}
 255
 256 \newcommand{\lcfix}[2]{\mathsf{fix} \appspace #1\absspace.\absspace #2}
 257
 258 This makes the STLC Turing incomplete.  We can recover the ability to loop by
 259 adding a combinator that recurses:
 260 \begin{equation*}
 261   \termsyn ::= \dots \separ  \lcfix{x : \tysyn}{\termsyn}
 262 \end{equation*}
 263 \begin{center}
 264   \begin{prooftree}
 265     \AxiomC{$\Gamma;x : \tya \vdash \termt : \tya$}
 266     \UnaryInfC{$\Gamma \vdash \lcfix{x : \tya}{\termt} : \tya$}
 267   \end{prooftree}
 268 \end{center}
 269 \begin{equation*}
 270   \lcfix{x : \tya}{\termt} \bred \termt[(\lcfix{x : \tya}{\termt}) / x]
 271 \end{equation*}
 272
 273 However, we will keep STLC without such a facility. In the next section we shall
 274 see why that is preferable for our needs.
 275
 276 \subsection{The Curry-Howard correspondence}
 277 \label{sec:curry-howard}
 278
 279 \newcommand{\lcunit}{\mathsf{()}}
 280
 281 It turns out that the STLC can be seen a natural deduction system.  Terms are
 282 proofs, and their types are the propositions they prove.  This remarkable fact
 283 is known as the Curry-Howard correspondence, or isomorphism.
 284
 285 The ``arrow'' ($\to$) type corresponds to implication.  If we wished to
 286 prove that $(\tya \tyarr \tyb) \tyarr (\tyb \tyarr \tyc) \tyarr (\tya
 287 \tyarr \tyc)$, all we need to do is to devise a $\lambda$-term that has the
 288 correct type:
 289 \begin{equation*}
 290   \abs{f : (\tya \tyarr \tyb)}{\abs{g : (\tyb \tyarr \tyc)}{\abs{x : \tya}{\app{g}{(\app{f}{x})}}}}
 291 \end{equation*}
 292 That is, function composition.  We might want extend our bare lambda calculus
 293 with a couple of terms to make our natural deduction more pleasant to use.  For
 294 example, tagged unions (\texttt{Either} in Haskell) are disjunctions, and tuples
 295 (or products) are conjunctions.  We also want to be able to express falsity, and
 296 that is done by introducing a type inhabited by no terms.  If evidence of such a
 297 type is presented, then we can derive any type, which expresses absurdity.
 298 Conversely, $\top$ is the type with just one trivial element, $\lcunit$.
 299
 300 \newcommand{\lcinl}{\mathsf{inl}\appspace}
 301 \newcommand{\lcinr}{\mathsf{inr}\appspace}
 302 \newcommand{\lccase}[3]{\mathsf{case}\appspace#1\appspace#2\appspace#3}
 303 \newcommand{\lcfst}{\mathsf{fst}\appspace}
 304 \newcommand{\lcsnd}{\mathsf{snd}\appspace}
 305 \newcommand{\orint}{\vee I_{1,2}}
 306 \newcommand{\orintl}{\vee I_{1}}
 307 \newcommand{\orintr}{\vee I_{2}}
 308 \newcommand{\orel}{\vee E}
 309 \newcommand{\andint}{\wedge I}
 310 \newcommand{\andel}{\wedge E_{1,2}}
 311 \newcommand{\botel}{\bot E}
 312 \newcommand{\lcabsurd}{\mathsf{absurd}\appspace}
 313
 314 \begin{center}
 315   \axname{syntax}
 316   \begin{eqnarray*}
 317     \termsyn & ::= & \dots \\
 318              &  |  & \lcinl \termsyn \separ \lcinr \termsyn \separ \lccase{\termsyn}{\termsyn}{\termsyn} \\
 319              &  |  & (\termsyn , \termsyn) \separ \lcfst \termsyn \separ \lcsnd \termsyn \\
 320              &  |  & \lcunit \\
 321     \tysyn & ::= & \dots \separ \tysyn \vee \tysyn \separ \tysyn \wedge \tysyn \separ \bot \separ \top
 322   \end{eqnarray*}
 323 \end{center}
 324 \begin{center}
 325   \axdesc{typing}{\Gamma \vdash \termsyn : \tysyn}
 326   \begin{prooftree}
 327     \AxiomC{$\Gamma \vdash \termt : \tya$}
 328     \RightLabel{$\orint$}
 329     \UnaryInfC{$\Gamma \vdash \lcinl \termt : \tya \vee \tyb$}
 330     \noLine
 331     \UnaryInfC{$\Gamma \vdash \lcinr \termt : \tyb \vee \tya$}
 332   \end{prooftree}
 333   \begin{prooftree}
 334     \AxiomC{$\Gamma \vdash \termt : \tya \vee \tyb$}
 335     \AxiomC{$\Gamma \vdash \termm : \tya \tyarr \tyc$}
 336     \AxiomC{$\Gamma \vdash \termn : \tyb \tyarr \tyc$}
 337     \RightLabel{$\orel$}
 338     \TrinaryInfC{$\Gamma \vdash \lccase{\termt}{\termm}{\termn} : \tyc$}
 339   \end{prooftree}
 340
 341   \begin{tabular}{c c}
 342     \AxiomC{$\Gamma \vdash \termt : \tya$}
 343     \AxiomC{$\Gamma \vdash \termm : \tyb$}
 344     \RightLabel{$\andint$}
 345     \BinaryInfC{$\Gamma \vdash (\tya , \tyb) : \tya \wedge \tyb$}
 346     \DisplayProof
 347     &
 348     \AxiomC{$\Gamma \vdash \termt : \tya \wedge \tyb$}
 349     \RightLabel{$\andel$}
 350     \UnaryInfC{$\Gamma \vdash \lcfst \termt : \tya$}
 351     \noLine
 352     \UnaryInfC{$\Gamma \vdash \lcsnd \termt : \tyb$}
 353     \DisplayProof
 354   \end{tabular}
 355
 356   \vspace{0.5cm}
 357
 358   \begin{tabular}{c c}
 359     \AxiomC{$\Gamma \vdash \termt : \bot$}
 360     \RightLabel{$\botel$}
 361     \UnaryInfC{$\Gamma \vdash \lcabsurd \termt : \tya$}
 362     \DisplayProof
 363     &
 364     \AxiomC{}
 365     \RightLabel{$\top I$}
 366     \UnaryInfC{$\Gamma \vdash \lcunit : \top$}
 367     \DisplayProof
 368   \end{tabular}
 369 \end{center}
 370 \begin{center}
 371   \axdesc{reduction}{\termsyn \bred \termsyn}
 372   \begin{eqnarray*}
 373     \lccase{(\lcinl \termt)}{\termm}{\termn} & \bred & \app{\termm}{\termt} \\
 374     \lccase{(\lcinr \termt)}{\termm}{\termn} & \bred & \app{\termn}{\termt} \\
 375     \lcfst (\termt , \termm)                 & \bred & \termt \\
 376     \lcsnd (\termt , \termm)                 & \bred & \termm
 377   \end{eqnarray*}
 378 \end{center}
 379
 380 With these rules, our STLC now looks remarkably similar in power and use to the
 381 natural deduction we already know.  $\neg A$ can be expressed as $A \tyarr
 382 \bot$.  However, there is an important omission: there is no term of the type $A
 383 \vee \neg A$ (excluded middle), or equivalently $\neg \neg A \tyarr A$ (double
 384 negation), or indeed any term with a type equivalent to those.
 385
 386 This has a considerable effect on our logic and it's no coincidence, since there
 387 is no obvious computational behaviour for laws like the excluded middle.
 388 Theories of this kind are called \emph{intuitionistic}, or \emph{constructive},
 389 and all the systems analysed will have this characteristic since they build on
 390 the foundation of the STLC\footnote{There is research to give computational
 391   behaviour to classical logic, but we will not touch those subjects.}.
 392
 393 Finally, going back to our $\mathsf{fix}$ combinator, it's now easy to see how
 394 we would want to exclude such a thing if we want to use STLC as a logic, since
 395 it allows us to prove everything: $(\lcfix{x : \tya}{x}) : \tya$ clearly works
 396 for any $A$!  This is a crucial point: in general we wish to have systems that
 397 do not let the user devise a term of type $\bot$, otherwise our logic will be
 398 unsound\footnote{Obviously such a term can be present under a $\lambda$.}.
 399
 400 \subsection{Extending the STLC}
 401
 402 \newcommand{\lctype}{\mathsf{Type}}
 403 \newcommand{\lcite}[3]{\mathsf{if}\appspace#1\appspace\mathsf{then}\appspace#2\appspace\mathsf{else}\appspace#3}
 404 \newcommand{\lcbool}{\mathsf{Bool}}
 405 \newcommand{\lcforallz}[2]{\forall #1 \absspace.\absspace #2}
 406 \newcommand{\lcforall}[3]{\forall #1 : #2 \absspace.\absspace #3}
 407 \newcommand{\lcexists}[3]{\exists #1 : #2 \absspace.\absspace #3}
 408
 409 The STLC can be made more expressive in various ways.  Henk Barendregt
 410 succinctly expressed geometrically how we can expand our type system:
 411
 412 \begin{equation*}
 413 \xymatrix@!0@=1.5cm{
 414   & \lambda\omega \ar@{-}[rr]\ar@{-}'[d][dd]
 415   & & \lambda C \ar@{-}[dd]
 416   \\
 417   \lambda2 \ar@{-}[ur]\ar@{-}[rr]\ar@{-}[dd]
 418   & & \lambda P2 \ar@{-}[ur]\ar@{-}[dd]
 419   \\
 420   & \lambda\underline\omega \ar@{-}'[r][rr]
 421   & & \lambda P\underline\omega
 422   \\
 423   \lambda{\to} \ar@{-}[rr]\ar@{-}[ur]
 424   & & \lambda P \ar@{-}[ur]
 425 }
 426 \end{equation*}
 427 Here $\lambda{\to}$, in the bottom left, is the STLC.  From there can move along
 428 3 dimensions:
 429 \begin{description}
 430 \item[Terms depending on types (towards $\lambda{2}$)] In other words, we can
 431   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
 432   has been System F.  This gives us a form of polymorphism and has been wildly
 433   successful, also thanks to a well known inference algorithm for a restricted
 434   version of System F known as Hindley-Milner.  Languages like Haskell and SML
 435   are based on this discipline.
 436 \item[Types depending on types (towards $\lambda{\underline{\omega}}$)] In other
 437   words, we have type operators: $(\abs{A : \lctype}{\abs{R : \lctype}{(A \to R) \to R}}) : \lctype \to \lctype \to \lctype$.
 438 \item[Types depending on terms (towards $\lambda{P}$)] Also known as ``dependent
 439   types'', give great expressive power: $(\abs{x : \lcbool}{\lcite{x}{\mathbb{N}}{\mathbb{Q}}}) : \lcbool \to \lctype$.
 440 \end{description}
 441
 442 All the systems preserve the properties that make the STLC well behaved (some of
 443 which I haven't mentioned yet).  The system we are going to focus on,
 444 Intuitionistic Type Theory, has all of the above additions, and thus would sit
 445 where $\lambda{C}$ sits in the ``$\lambda$-cube'' above.
 446
 447 \section{Intuitionistic Type Theory}
 448
 449 Intuitionistic Type Theory (ITT) is a very expressive system first described by
 450 Per Martin-L\"{o}f at the end of the 70s.  It extends the STLC giving it all the
 451 properties described above, while retaining good computational properties.  Here
 452 we will present a core type theory and illustrate its components and properties
 453 one by one, and then describe the various additions that make it useful as a
 454 programming language and as a theorem prover.
 455
 456 \newcommand{\lcset}[1]{\mathsf{Type}_{#1}}
 457 \newcommand{\lcsetz}{\mathsf{Type}}
 458 \newcommand{\defeq}{\equiv}
 459
 460 \begin{center}
 461   \axname{syntax}
 462   \begin{eqnarray*}
 463   \termsyn & ::= & x \\
 464          &  |  & \lcforall{x}{\termsyn}{\termsyn} \separ \abs{x : \termsyn}{\termsyn} \separ \app{\termsyn}{\termsyn} \\
 465          &  |  & \lcexists{x}{\termsyn}{\termsyn} \separ (\termsyn , \termsyn) \separ \lcfst \termsyn \separ \lcsnd \termsyn \\
 466          &  |  & \bot \separ \lcabsurd \termt \\
 467          &  |  & \lcset{n} \\
 468    n     & \in & \mathbb{N}
 469  \end{eqnarray*}
 470
 471   \axdesc{typing}{\Gamma \vdash \termsyn : \termsyn}
 472
 473   \vspace{0.5cm}
 474
 475   \begin{tabular}{c c c}
 476     \AxiomC{}
 477     \RightLabel{var}
 478     \UnaryInfC{$\Gamma;x : \tya \vdash x : \tya$}
 479     \DisplayProof
 480     &
 481     \AxiomC{$\Gamma \vdash \termt : \bot$}
 482     \RightLabel{$\bot E$}
 483     \UnaryInfC{$\Gamma \vdash \lcabsurd \termt : A$}
 484     \DisplayProof
 485     &
 486     \AxiomC{$\Gamma \vdash \termt : \tya$}
 487     \AxiomC{$\tya \defeq \tyb$}
 488     \RightLabel{$\defeq$ type}
 489     \BinaryInfC{$\Gamma \vdash \termt : \tyb$}
 490     \DisplayProof
 491   \end{tabular}
 492
 493   \vspace{0.5cm}
 494
 495   \begin{tabular}{c c}
 496     \AxiomC{$\Gamma;x : \tya \vdash \termt : \tya$}
 497     \RightLabel{$\forall I$}
 498     \UnaryInfC{$\Gamma \vdash \abs{x : \tya}{\termt} : \lcforall{x}{\tya}{\tyb}$}
 499     \DisplayProof
 500     &
 501     \AxiomC{$\Gamma \vdash \termt : \lcforall{x}{\tya}{\tyb}$}
 502     \AxiomC{$\Gamma \vdash \termm : \tya$}
 503     \RightLabel{$\forall E$}
 504     \BinaryInfC{$\Gamma \vdash \app{\termt}{\termm} : \tyb[\termm / x]$}
 505     \DisplayProof
 506   \end{tabular}
 507
 508   \vspace{0.5cm}
 509
 510   \begin{tabular}{c c}
 511     \AxiomC{$\Gamma \vdash \termt : \tya$}
 512     \AxiomC{$\Gamma \vdash \termm : \tyb[\termt / x]$}
 513     \RightLabel{$\exists I$}
 514     \BinaryInfC{$\Gamma \vdash (\termt, \termm) : \lcexists{x}{\tya}{\tyb}$}
 515     \DisplayProof
 516     &
 517     \AxiomC{$\Gamma \vdash \termt: \lcexists{x}{\tya}{\tyb}$}
 518     \RightLabel{$\exists E_{1,2}$}
 519     \UnaryInfC{$\hspace{0.7cm} \Gamma \vdash \lcfst \termt : \tya \hspace{0.7cm}$}
 520     \noLine
 521     \UnaryInfC{$\Gamma \vdash \lcsnd \termt : \tyb[\lcfst \termt / x]$}
 522     \DisplayProof
 523   \end{tabular}
 524
 525   \vspace{0.5cm}
 526
 527   \begin{tabular}{c c}
 528     \AxiomC{}
 529     \RightLabel{type}
 530     \UnaryInfC{$\Gamma \vdash \lcset{n} : \lcset{n + 1}$}
 531     \DisplayProof
 532     &
 533     \AxiomC{$\Gamma \vdash \tya : \lcset{n}$}
 534     \AxiomC{$\Gamma; x : \tya \vdash \tyb : \lcset{m}$}
 535     \RightLabel{$\forall, \exists$ type}
 536     \BinaryInfC{$\Gamma \vdash \lcforall{x}{\tya}{\tyb} : \lcset{n \sqcup m}$}
 537     \noLine
 538     \UnaryInfC{$\Gamma \vdash \lcexists{x}{\tya}{\tyb} : \lcset{n \sqcup m}$}
 539     \DisplayProof
 540   \end{tabular}
 541
 542   \vspace{0.5cm}
 543
 544   \axdesc{reduction}{\termsyn \bred \termsyn}
 545   \begin{eqnarray*}
 546     \app{(\abs{x}{\termt})}{\termm} & \bred & \termt[\termm / x] \\
 547     \lcfst (\termt, \termm) & \bred & \termt \\
 548     \lcsnd (\termt, \termm) & \bred & \termm
 549   \end{eqnarray*}
 550 \end{center}
 551
 552 I will abbreviate $\lcset{0}$ as $\lcsetz$.
 553
 554 There are a lot of new factors at play here. The first thing to notice is that
 555 the separation between types and terms is gone.  All we have is terms, that
 556 include both values (terms of type $\lcset{0}$) and types (terms of type
 557 $\lcset{n}$, with $n > 0$).  This change is reflected in the typing rules.
 558 While in the STLC terms and types are kept well separated (terms never go
 559 ``right of the colon''), in ITT types can freely depend on terms.
 560
 561 This relation is expressed in the typing rules for $\forall$ and $\exists$: if a
 562 function has type $\lcforall{x}{\tya}{\tyb}$, $\tyb$ can depend on $x$.
 563 Examples will make this clearer once some base types are added in the next
 564 section.
 565
 566 $\forall$ and $\exists$ are at the core of the machinery of ITT:
 567
 568 \begin{description}
 569 \item[$\forall$] is a generalisation of $\tyarr$ in the STLC and expresses
 570   universal quantification in our logic.  In the literature this is also known
 571   as ``dependent product'' and shown as $\Pi$, following an interpretation of
 572   functions as infinitary products. We will just call it ``dependent function'',
 573   reserving ``product'' for $\exists$.
 574
 575 \item[$\exists$] is a generalisation of $\wedge$ in the extended STLC of section
 576   \ref{sec:curry-howard}, and thus we will call it ``dependent product''.  In
 577   our logic, it represents existential quantification.
 578
 579   For added confusion, in the literature that calls $\forall$ $\Pi$ $\exists$ is
 580   often named ``dependent sum'' and shown as $\Sigma$.  This is following the
 581   interpretation of $\exists$ as a generalised $\vee$, where the first element
 582   of the pair is the ``tag'' that decides which type the second element will
 583   have.
 584 \end{description}
 585
 586 Another thing to notice is that types are very ``first class'': we are free to
 587 create functions that accept and return types.  For this reason we $\defeq$ as
 588 the smallest
 589
 590 \begin{thebibliography}{9}
 591
 592 \bibitem{levitation}
 593   James Chapman, Pierre-Evariste Dagand, Conor McBride, and Peter Morris.
 594   \emph{The gentle art of levitation}.
 595   SIGPLAN Not., 45:3–14, September 2010.
 596
 597 \bibitem{outsidein}
 598   Dimitrios Vytiniotis, Simon Peyton Jones, Tom Schrijvers, and Martin
 599   Sulzmann.
 600   \emph{OutsideIn(X): Modular Type inference with local assumptions}.
 601   Journal of Functional Programming, 21, 2011.
 602
 603 \bibitem{haskell-promotion}
 604   Brent A. Yorgey, Stephanie Weirich, Julien Cretin, Simon Peyton Jones,
 605   Dimitrios Vytiniotis, and Jos\'{e} Pedro Magalh\~{a}es.
 606   \emph{Giving Haskell a promotion}.
 607   In Proceedings of the 8th ACM SIGPLAN Workshop on Types in Language Design and
 608   Implementation, TLDI ’12, pages 53–66, New York, NY, USA, 2012. ACM. doi:
 609   10.1145/2103786.2103795.
 610
 611 \bibitem{idris}
 612   Edwin Brady.
 613   \emph{Implementing General Purpose Dependently Typed Programming Languages}.
 614   Unpublished draft.
 615
 616 \bibitem{bidirectional}
 617   Benjamin C. Pierce and David N. Turner.
 618   \emph{Local type inference}.
 619   ACM Transactions on Programming Languages and Systems, 22(1):1–44, January
 620   2000. ISSN 0164-0925. doi: 10.1145/345099.345100.
 621
 622 \end{thebibliography}
 623
 624 \end{document}