path: root/docs/background.tex

\documentclass[article, a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage{fixltx2e}
\usepackage{enumitem}
\usepackage[normalem]{ulem}
\usepackage{graphicx}
\usepackage{subcaption}

%% -----------------------------------------------------------------------------
%% Fonts
%% \usepackage[osf]{libertine}
%% \usepackage{helvet}
%% \usepackage{lmodern}
%% \IfFileExists{microtype.sty}{\usepackage{microtype}}{}

%% -----------------------------------------------------------------------------
%% Diagrams
% \usepackage{tikz}
% \usetikzlibrary{positioning}
%% \usetikzlibrary{shapes}
%% \usetikzlibrary{arrows}
%% \usepackage{tikz-cd}
%% \usepackage{pgfplots}
\usepackage[all]{xy}

%% -----------------------------------------------------------------------------
%% Symbols
\usepackage{amssymb,amsmath}
\usepackage{wasysym}
\usepackage{turnstile}
\usepackage{centernot}

%% -----------------------------------------------------------------------------
%% Utils
\usepackage{bussproofs}
\usepackage{umoline}
\usepackage[export]{adjustbox}
\usepackage{multicol}

%% Numbering depth
%% \setcounter{secnumdepth}{0}

%% -----------------------------------------------------------------------------
% We will generate all images so they have a width \maxwidth. This means
% that they will get their normal width if they fit onto the page, but
% are scaled down if they would overflow the margins.
\makeatletter
\def\maxwidth{
  \ifdim\Gin@nat@width>\linewidth\linewidth
  \else\Gin@nat@width\fi
}
\makeatother

%% -----------------------------------------------------------------------------
%% Links
\usepackage[
  setpagesize=false, % page size defined by xetex
  unicode=false, % unicode breaks when used with xetex
  xetex
]{hyperref}

\hypersetup{
  breaklinks=true,
  bookmarks=true,
  pdfauthor={Francesco Mazzoli <fm2209@ic.ac.uk>},
  pdftitle={The Paths Towards Observational Equality},
  colorlinks=false,
  pdfborder={0 0 0}
}

% Make links footnotes instead of hotlinks:
\renewcommand{\href}[2]{#2\footnote{\url{#1}}}

% avoid problems with \sout in headers with hyperref:
\pdfstringdefDisableCommands{\renewcommand{\sout}{}}

\title{The Paths Towards Observational Equality}
\author{Francesco Mazzoli \url{<fm2209@ic.ac.uk>}}
\date{December 2012}

\begin{document}

\maketitle

\setlength{\tabcolsep}{12pt}

The marriage between programming and logic has been a very fertile one.  In
particular, since the simply typed lambda calculus (STLC), a number of type
systems have been devised with increasing expressive power.

In the next sections I will give a very brief overview of STLC, and then
describe how to augment it to reach the theory I am interested in,
Inutitionistic Type Theory (ITT), also known as Martin-L\"{o}f Type Theory after
its inventor.

I will then explain why equality has been a tricky business in this theories,
and talk about the various attempts have been made.  One interesting development
has recently emerged: Observational Type theory.  I propose to explore the ways
to turn these ideas into useful practices for programming and theorem proving.

\section{Simple and not-so-simple types}

\subsection{Untyped $\lambda$-calculus}

Along with Turing's machines, the earliest attempts to formalise computation
lead to the $\lambda$-calculus.  This early programming language encodes
computation with a minimal sintax and most notably no ``data'' in the
traditional sense, but just functions.

The syntax of $\lambda$-terms consists of just three things: variables,
abstractions, and applications:

\newcommand{\appspace}{\hspace{0.07cm}}
\newcommand{\app}[2]{#1\appspace#2}
\newcommand{\absspace}{\hspace{0.03cm}}
\newcommand{\abs}[2]{\lambda #1\absspace.\absspace#2}
\newcommand{\termt}{t}
\newcommand{\termm}{m}
\newcommand{\termn}{n}
\newcommand{\termp}{p}
\newcommand{\termf}{f}
\newcommand{\separ}{\ \ |\ \ }
\newcommand{\termsyn}{\mathit{term}}
\newcommand{\axname}[1]{\textbf{#1}}
\newcommand{\axdesc}[2]{\axname{#1} \fbox{$#2$}}

\begin{center}
\axname{syntax}
\begin{eqnarray*}
  \termsyn & ::= & x \separ (\abs{x}{\termsyn}) \separ (\app{\termsyn}{\termsyn}) \\
         x & \in & \text{Some enumerable set of symbols, e.g.}\ \{x, y, z, \dots , x_1, x_2, \dots\}
\end{eqnarray*}
\end{center}


% I will omit parethesis in the usual manner. %TODO explain how

I will use $\termt,\termm,\termn,\dots$ to indicate a generic term, and $x,y$
for variables.  I will also assume that all variable names in a term are unique
to avoid problems with name capturing.  Intuitively, abstractions
($\abs{x}{\termt}$) introduce functions with a named parameter ($x$), and
applications ($\app{\termt}{\termm}$) apply a function ($\termt$) to an argument
($\termm$).

The ``applying'' is more formally explained with a reduction rule:

\newcommand{\bred}{\leadsto}
\newcommand{\bredc}{\bred^*}

\begin{center}
\axdesc{reduction}{\termsyn \bred \termsyn}
$$\app{(\abs{x}{\termt})}{\termm} \bred \termt[\termm / x]$$
\end{center}

Where $\termt[\termm / x]$ expresses the operation that substitutes all
occurrences of $x$ with $\termm$ in $\termt$.  In the systems presented, the
$\bred$ relation also includes reduction of subterms, for example if $\termt
\bred \termm$ then $\app{\termt}{\termn} \bred \app{\termm}{\termn}$, and so on.

% % TODO put the trans closure

These few elements are of remarkable expressiveness, and in fact Turing
complete.  As a corollary, we must be able to devise a term that reduces forever
(``loops'' in imperative terms):
\begin{equation*}
  \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
\end{equation*}
Terms that can be reduced only a finite number of times (the non-looping ones)
are said to be \emph{normalising}, and the ``final'' term is called \emph{normal
  form}.  These concepts (reduction and normal forms) will run through all the
material analysed.

\subsection{The simply typed $\lambda$-calculus}

\newcommand{\tya}{A}
\newcommand{\tyb}{B}
\newcommand{\tyc}{C}

One way to ``discipline'' $\lambda$-terms is to assign \emph{types} to them, and
then check that the terms that we are forming make sense given our typing rules.

We wish to introduce rules of the form $\Gamma \vdash \termt : \tya$, which
reads ``in context $\Gamma$, term $\termt$ has type $\tya$''.

The syntax for types is as follows:

\newcommand{\tyarr}{\to}
\newcommand{\tysyn}{\mathit{type}}
\newcommand{\ctxsyn}{\mathit{context}}
\newcommand{\emptyctx}{\cdot}

\begin{center}
  \axname{syntax}
   $$\tysyn ::= x \separ \tysyn \tyarr \tysyn$$
\end{center}

I will use $\tya,\tyb,\dots$ to indicate a generic type.

A context $\Gamma$ is a map from variables to types.  We use the notation
$\Gamma; x : \tya$ to augment it, and to ``extract'' pairs from it.

Predictably, $\tya \tyarr \tyb$ is the type of a function from $\tya$ to
$\tyb$.  We need to be able to decorate our abstractions with
types\footnote{Actually, we don't need to: computers can infer the right type
  easily, but that is another story.}:
\begin{center}
  \axname{syntax}
   $$\termsyn ::= x \separ (\abs{x : \tysyn}{\termsyn}) \separ (\app{\termsyn}{\termsyn})$$
\end{center}
Now we are ready to give the typing judgements:

\begin{center}
  \axdesc{typing}{\Gamma \vdash \termsyn : \tysyn}

  \vspace{0.5cm}

  \begin{tabular}{c c c}
    \AxiomC{}
    \UnaryInfC{$\Gamma; x : \tya \vdash x : \tya$}
    \DisplayProof
    &
    \AxiomC{$\Gamma; x : \tya \vdash \termt : \tyb$}
    \UnaryInfC{$\Gamma \vdash \abs{x : \tya}{\termt} : \tya \tyarr \tyb$}
    \DisplayProof
  \end{tabular}

  \vspace{0.5cm}

  \begin{tabular}{c}
    \AxiomC{$\Gamma \vdash \termt : \tya \tyarr \tyb$}
    \AxiomC{$\Gamma \vdash \termm : \tya$}
    \BinaryInfC{$\Gamma \vdash \app{\termt}{\termm} : \tyb$}
    \DisplayProof
  \end{tabular}
\end{center}

This typing system takes the name of ``simply typed lambda calculus'' (STLC),
and enjoys a number of properties.  Two of them are expected in most type
systems: %TODO add credit to pierce
\begin{description}
\item[Progress] A well-typed term is not stuck - either it is a value or it can
  take a step according to the evaluation rules.  With ``value'' we mean a term
  whose subterms (including itself) don't appear to the left of the $\bred$
  relation.
\item[Preservation] If a well-typed term takes a step of evaluation, then the
  resulting term is also well typed.
\end{description}

However, STLC buys us much more: every well-typed term
is normalising.  It is easy to see that we can't fill the blanks if we want to
give types to the non-normalising term shown before:
\begin{equation*}
  \app{(\abs{x : ?}{\app{x}{x}})}{(\abs{x : ?}{\app{x}{x}})}
\end{equation*}

\newcommand{\lcfix}[2]{\mathsf{fix} \appspace #1\absspace.\absspace #2}

This makes the STLC Turing incomplete.  We can recover the ability to loop by
adding a combinator that recurses:
\begin{equation*}
  \termsyn ::= \dots \separ  \lcfix{x : \tysyn}{\termsyn}
\end{equation*}
\begin{center}
  \begin{prooftree}
    \AxiomC{$\Gamma;x : \tya \vdash \termt : \tya$}
    \UnaryInfC{$\Gamma \vdash \lcfix{x : \tya}{\termt} : \tya$}
  \end{prooftree}
\end{center}
\begin{equation*}
  \lcfix{x : \tya}{\termt} \bred \termt[(\lcfix{x : \tya}{\termt}) / x]
\end{equation*}

However, we will keep STLC without such a facility. In the next section we shall
see why that is preferable for our needs.

\subsection{The Curry-Howard correspondence}
\label{sec:curry-howard}

\newcommand{\lcunit}{\mathsf{()}}

It turns out that the STLC can be seen a natural deduction system.  Terms are
proofs, and their types are the propositions they prove.  This remarkable fact
is known as the Curry-Howard correspondence, or isomorphism.

The ``arrow'' ($\to$) type corresponds to implication.  If we wished to
prove that $(\tya \tyarr \tyb) \tyarr (\tyb \tyarr \tyc) \tyarr (\tya
\tyarr \tyc)$, all we need to do is to devise a $\lambda$-term that has the
correct type:
\begin{equation*}
  \abs{f : (\tya \tyarr \tyb)}{\abs{g : (\tyb \tyarr \tyc)}{\abs{x : \tya}{\app{g}{(\app{f}{x})}}}}
\end{equation*}
That is, function composition.  We might want extend our bare lambda calculus
with a couple of terms to make our natural deduction more pleasant to use.  For
example, tagged unions (\texttt{Either} in Haskell) are disjunctions, and tuples
(or products) are conjunctions.  We also want to be able to express falsity, and
that is done by introducing a type inhabited by no terms.  If evidence of such a
type is presented, then we can derive any type, which expresses absurdity.
Conversely, $\top$ is the type with just one trivial element, $\lcunit$.

\newcommand{\lcinl}{\mathsf{inl}\appspace}
\newcommand{\lcinr}{\mathsf{inr}\appspace}
\newcommand{\lccase}[3]{\mathsf{case}\appspace#1\appspace#2\appspace#3}
\newcommand{\lcfst}{\mathsf{fst}\appspace}
\newcommand{\lcsnd}{\mathsf{snd}\appspace}
\newcommand{\orint}{\vee I_{1,2}}
\newcommand{\orintl}{\vee I_{1}}
\newcommand{\orintr}{\vee I_{2}}
\newcommand{\orel}{\vee E}
\newcommand{\andint}{\wedge I}
\newcommand{\andel}{\wedge E_{1,2}}
\newcommand{\botel}{\bot E}
\newcommand{\lcabsurd}{\mathsf{absurd}\appspace}

\begin{center}
  \axname{syntax}
  \begin{eqnarray*}
    \termsyn & ::= & \dots \\
             &  |  & \lcinl \termsyn \separ \lcinr \termsyn \separ \lccase{\termsyn}{\termsyn}{\termsyn} \\
             &  |  & (\termsyn , \termsyn) \separ \lcfst \termsyn \separ \lcsnd \termsyn \\
             &  |  & \lcunit \\
    \tysyn & ::= & \dots \separ \tysyn \vee \tysyn \separ \tysyn \wedge \tysyn \separ \bot \separ \top
  \end{eqnarray*}
\end{center}
\begin{center}
  \axdesc{typing}{\Gamma \vdash \termsyn : \tysyn}
  \begin{prooftree}
    \AxiomC{$\Gamma \vdash \termt : \tya$}
    \RightLabel{$\orint$}
    \UnaryInfC{$\Gamma \vdash \lcinl \termt : \tya \vee \tyb$}
    \noLine
    \UnaryInfC{$\Gamma \vdash \lcinr \termt : \tyb \vee \tya$}
  \end{prooftree}
  \begin{prooftree}
    \AxiomC{$\Gamma \vdash \termt : \tya \vee \tyb$}
    \AxiomC{$\Gamma \vdash \termm : \tya \tyarr \tyc$}
    \AxiomC{$\Gamma \vdash \termn : \tyb \tyarr \tyc$}
    \RightLabel{$\orel$}
    \TrinaryInfC{$\Gamma \vdash \lccase{\termt}{\termm}{\termn} : \tyc$}
  \end{prooftree}

  \begin{tabular}{c c}
    \AxiomC{$\Gamma \vdash \termt : \tya$}
    \AxiomC{$\Gamma \vdash \termm : \tyb$}
    \RightLabel{$\andint$}
    \BinaryInfC{$\Gamma \vdash (\tya , \tyb) : \tya \wedge \tyb$}
    \DisplayProof
    &
    \AxiomC{$\Gamma \vdash \termt : \tya \wedge \tyb$}
    \RightLabel{$\andel$}
    \UnaryInfC{$\Gamma \vdash \lcfst \termt : \tya$}
    \noLine
    \UnaryInfC{$\Gamma \vdash \lcsnd \termt : \tyb$}
    \DisplayProof
  \end{tabular}

  \vspace{0.5cm}

  \begin{tabular}{c c}
    \AxiomC{$\Gamma \vdash \termt : \bot$}
    \RightLabel{$\botel$}
    \UnaryInfC{$\Gamma \vdash \lcabsurd \termt : \tya$}
    \DisplayProof
    &
    \AxiomC{}
    \RightLabel{$\top I$}
    \UnaryInfC{$\Gamma \vdash \lcunit : \top$}
    \DisplayProof
  \end{tabular}
\end{center}
\begin{center}
  \axdesc{reduction}{\termsyn \bred \termsyn}
  \begin{eqnarray*}
    \lccase{(\lcinl \termt)}{\termm}{\termn} & \bred & \app{\termm}{\termt} \\
    \lccase{(\lcinr \termt)}{\termm}{\termn} & \bred & \app{\termn}{\termt} \\
    \lcfst (\termt , \termm)                 & \bred & \termt \\
    \lcsnd (\termt , \termm)                 & \bred & \termm
  \end{eqnarray*}
\end{center}

With these rules, our STLC now looks remarkably similar in power and use to the
natural deduction we already know.  $\neg A$ can be expressed as $A \tyarr
\bot$.  However, there is an important omission: there is no term of the type $A
\vee \neg A$ (excluded middle), or equivalently $\neg \neg A \tyarr A$ (double
negation), or indeed any term with a type equivalent to those.

This has a considerable effect on our logic and it's no coincidence, since there
is no obvious computational behaviour for laws like the excluded middle.
Theories of this kind are called \emph{intuitionistic}, or \emph{constructive},
and all the systems analysed will have this characteristic since they build on
the foundation of the STLC\footnote{There is research to give computational
  behaviour to classical logic, but we will not touch those subjects.}.

Finally, going back to our $\mathsf{fix}$ combinator, it's now easy to see how
we would want to exclude such a thing if we want to use STLC as a logic, since
it allows us to prove everything: $(\lcfix{x : \tya}{x}) : \tya$ clearly works
for any $A$!  This is a crucial point: in general we wish to have systems that
do not let the user devise a term of type $\bot$, otherwise our logic will be
unsound\footnote{Obviously such a term can be present under a $\lambda$.}.

\subsection{Extending the STLC}

\newcommand{\lctype}{\mathsf{Type}}
\newcommand{\lcite}[3]{\mathsf{if}\appspace#1\appspace\mathsf{then}\appspace#2\appspace\mathsf{else}\appspace#3}
\newcommand{\lcbool}{\mathsf{Bool}}
\newcommand{\lcforallz}[2]{\forall #1 \absspace.\absspace #2}
\newcommand{\lcforall}[3]{\forall #1 : #2 \absspace.\absspace #3}
\newcommand{\lcexists}[3]{\exists #1 : #2 \absspace.\absspace #3}

The STLC can be made more expressive in various ways.  Henk Barendregt
succinctly expressed geometrically how we can expand our type system:

\begin{equation*}
\xymatrix@!0@=1.5cm{
  & \lambda\omega \ar@{-}[rr]\ar@{-}'[d][dd]
  & & \lambda C \ar@{-}[dd]
  \\
  \lambda2 \ar@{-}[ur]\ar@{-}[rr]\ar@{-}[dd]
  & & \lambda P2 \ar@{-}[ur]\ar@{-}[dd]
  \\
  & \lambda\underline\omega \ar@{-}'[r][rr]
  & & \lambda P\underline\omega
  \\
  \lambda{\to} \ar@{-}[rr]\ar@{-}[ur]
  & & \lambda P \ar@{-}[ur]
}
\end{equation*}
Here $\lambda{\to}$, in the bottom left, is the STLC.  From there can move along
3 dimensions:
\begin{description}
\item[Terms depending on types (towards $\lambda{2}$)] In other words, we can
  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
  has been System F.  This gives us a form of polymorphism and has been wildly
  successful, also thanks to a well known inference algorithm for a restricted
  version of System F known as Hindley-Milner.  Languages like Haskell and SML
  are based on this discipline.
\item[Types depending on types (towards $\lambda{\underline{\omega}}$)] In other
  words, we have type operators: $(\abs{A : \lctype}{\abs{R : \lctype}{(A \to R) \to R}}) : \lctype \to \lctype \to \lctype$.
\item[Types depending on terms (towards $\lambda{P}$)] Also known as ``dependent
  types'', give great expressive power: $(\abs{x : \lcbool}{\lcite{x}{\mathbb{N}}{\mathbb{Q}}}) : \lcbool \to \lctype$.
\end{description}

All the systems preserve the properties that make the STLC well behaved (some of
which I haven't mentioned yet).  The system we are going to focus on,
Intuitionistic Type Theory, has all of the above additions, and thus would sit
where $\lambda{C}$ sits in the ``$\lambda$-cube'' above.

\section{Intuitionistic Type Theory}

Intuitionistic Type Theory (ITT) is a very expressive system first described by
Per Martin-L\"{o}f at the end of the 70s.  It extends the STLC giving it all the
properties described above, while retaining good computational properties.  Here
we will present a core type theory and illustrate its components and properties
one by one, and then describe the various additions that make it useful as a
programming language and as a theorem prover.

\newcommand{\lcset}[1]{\mathsf{Type}_{#1}}
\newcommand{\lcsetz}{\mathsf{Type}}
\newcommand{\defeq}{\equiv}

\begin{center}
  \axname{syntax}
  \begin{eqnarray*}
  \termsyn & ::= & x \\
         &  |  & \lcforall{x}{\termsyn}{\termsyn} \separ \abs{x : \termsyn}{\termsyn} \separ \app{\termsyn}{\termsyn} \\
         &  |  & \lcexists{x}{\termsyn}{\termsyn} \separ (\termsyn , \termsyn) \separ \lcfst \termsyn \separ \lcsnd \termsyn \\
         &  |  & \bot \separ \lcabsurd \termt \\
         &  |  & \lcset{n} \\
   n     & \in & \mathbb{N}
 \end{eqnarray*}

  \axdesc{typing}{\Gamma \vdash \termsyn : \termsyn}

  \vspace{0.5cm}

  \begin{tabular}{c c c}
    \AxiomC{}
    \RightLabel{var}
    \UnaryInfC{$\Gamma;x : \tya \vdash x : \tya$}
    \DisplayProof
    &
    \AxiomC{$\Gamma \vdash \termt : \bot$}
    \RightLabel{$\bot E$}
    \UnaryInfC{$\Gamma \vdash \lcabsurd \termt : A$}
    \DisplayProof
    &
    \AxiomC{$\Gamma \vdash \termt : \tya$}
    \AxiomC{$\tya \defeq \tyb$}
    \RightLabel{$\defeq$ type}
    \BinaryInfC{$\Gamma \vdash \termt : \tyb$}
    \DisplayProof
  \end{tabular}

  \vspace{0.5cm}

  \begin{tabular}{c c}
    \AxiomC{$\Gamma;x : \tya \vdash \termt : \tya$}
    \RightLabel{$\forall I$}
    \UnaryInfC{$\Gamma \vdash \abs{x : \tya}{\termt} : \lcforall{x}{\tya}{\tyb}$}
    \DisplayProof
    &
    \AxiomC{$\Gamma \vdash \termt : \lcforall{x}{\tya}{\tyb}$}
    \AxiomC{$\Gamma \vdash \termm : \tya$}
    \RightLabel{$\forall E$}
    \BinaryInfC{$\Gamma \vdash \app{\termt}{\termm} : \tyb[\termm / x]$}
    \DisplayProof
  \end{tabular}

  \vspace{0.5cm}

  \begin{tabular}{c c}
    \AxiomC{$\Gamma \vdash \termt : \tya$}
    \AxiomC{$\Gamma \vdash \termm : \tyb[\termt / x]$}
    \RightLabel{$\exists I$}
    \BinaryInfC{$\Gamma \vdash (\termt, \termm) : \lcexists{x}{\tya}{\tyb}$}
    \DisplayProof
    &
    \AxiomC{$\Gamma \vdash \termt: \lcexists{x}{\tya}{\tyb}$}
    \RightLabel{$\exists E_{1,2}$}
    \UnaryInfC{$\hspace{0.7cm} \Gamma \vdash \lcfst \termt : \tya \hspace{0.7cm}$}
    \noLine
    \UnaryInfC{$\Gamma \vdash \lcsnd \termt : \tyb[\lcfst \termt / x]$}
    \DisplayProof
  \end{tabular}

  \vspace{0.5cm}

  \begin{tabular}{c c}
    \AxiomC{}
    \RightLabel{type}
    \UnaryInfC{$\Gamma \vdash \lcset{n} : \lcset{n + 1}$}
    \DisplayProof
    &
    \AxiomC{$\Gamma \vdash \tya : \lcset{n}$}
    \AxiomC{$\Gamma; x : \tya \vdash \tyb : \lcset{m}$}
    \RightLabel{$\forall, \exists$ type}
    \BinaryInfC{$\Gamma \vdash \lcforall{x}{\tya}{\tyb} : \lcset{n \sqcup m}$}
    \noLine
    \UnaryInfC{$\Gamma \vdash \lcexists{x}{\tya}{\tyb} : \lcset{n \sqcup m}$}
    \DisplayProof
  \end{tabular}

  \vspace{0.5cm}

  \axdesc{reduction}{\termsyn \bred \termsyn}
  \begin{eqnarray*}
    \app{(\abs{x}{\termt})}{\termm} & \bred & \termt[\termm / x] \\
    \lcfst (\termt, \termm) & \bred & \termt \\
    \lcsnd (\termt, \termm) & \bred & \termm
  \end{eqnarray*}
\end{center}

I will abbreviate $\lcset{0}$ as $\lcsetz$.

There are a lot of new factors at play here. The first thing to notice is that
the separation between types and terms is gone.  All we have is terms, that
include both values (terms of type $\lcset{0}$) and types (terms of type
$\lcset{n}$, with $n > 0$).  This change is reflected in the typing rules.
While in the STLC terms and types are kept well separated (terms never go
``right of the colon''), in ITT types can freely depend on terms.

This relation is expressed in the typing rules for $\forall$ and $\exists$: if a
function has type $\lcforall{x}{\tya}{\tyb}$, $\tyb$ can depend on $x$.
Examples will make this clearer once some base types are added in the next
section.

$\forall$ and $\exists$ are at the core of the machinery of ITT:

\begin{description}
\item[$\forall$] is a generalisation of $\tyarr$ in the STLC and expresses
  universal quantification in our logic.  In the literature this is also known
  as ``dependent product'' and shown as $\Pi$, following an interpretation of
  functions as infinitary products. We will just call it ``dependent function'',
  reserving ``product'' for $\exists$.

\item[$\exists$] is a generalisation of $\wedge$ in the extended STLC of section
  \ref{sec:curry-howard}, and thus we will call it ``dependent product''.  In
  our logic, it represents existential quantification.

  For added confusion, in the literature that calls $\forall$ $\Pi$ $\exists$ is
  often named ``dependent sum'' and shown as $\Sigma$.  This is following the
  interpretation of $\exists$ as a generalised $\vee$, where the first element
  of the pair is the ``tag'' that decides which type the second element will
  have.
\end{description}

Another thing to notice is that types are very ``first class'': we are free to
create functions that accept and return types.  For this reason we $\defeq$ as
the smallest 

\begin{thebibliography}{9}

\bibitem{levitation}
  James Chapman, Pierre-Evariste Dagand, Conor McBride, and Peter Morris.
  \emph{The gentle art of levitation}.
  SIGPLAN Not., 45:3–14, September 2010.

\bibitem{outsidein}
  Dimitrios Vytiniotis, Simon Peyton Jones, Tom Schrijvers, and Martin
  Sulzmann.
  \emph{OutsideIn(X): Modular Type inference with local assumptions}.
  Journal of Functional Programming, 21, 2011.

\bibitem{haskell-promotion}
  Brent A. Yorgey, Stephanie Weirich, Julien Cretin, Simon Peyton Jones,
  Dimitrios Vytiniotis, and Jos\'{e} Pedro Magalh\~{a}es.
  \emph{Giving Haskell a promotion}.
  In Proceedings of the 8th ACM SIGPLAN Workshop on Types in Language Design and
  Implementation, TLDI ’12, pages 53–66, New York, NY, USA, 2012. ACM. doi:
  10.1145/2103786.2103795.

\bibitem{idris}
  Edwin Brady.
  \emph{Implementing General Purpose Dependently Typed Programming Languages}.
  Unpublished draft.

\bibitem{bidirectional}
  Benjamin C. Pierce and David N. Turner.
  \emph{Local type inference}.
  ACM Transactions on Programming Languages and Systems, 22(1):1–44, January
  2000. ISSN 0164-0925. doi: 10.1145/345099.345100.

\end{thebibliography}

\end{document}