\usepackage[export]{adjustbox}
\usepackage{multicol}
+%% -----------------------------------------------------------------------------
+%% Bibtex
+\usepackage{natbib}
+
%% Numbering depth
%% \setcounter{secnumdepth}{0}
}
% Make links footnotes instead of hotlinks:
-\renewcommand{\href}[2]{#2\footnote{\url{#1}}}
+% \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>}}
+\author{Francesco Mazzoli \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{<fm2209@ic.ac.uk>}}}
\date{December 2012}
\begin{document}
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.
+its inventor. The exposition is quite dense since there is a lot of material to
+cover, for a more complete treatment of the material the reader can refer to
+\citep{Thompson1991, Pierce2002}.
-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.
+I will then explain why equality has been a tricky business in these theories,
+and talk about the various attempts have been made to make the situation better.
+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.
+lead to the $\lambda$-calculus \citep{Church1936}. 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{\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.
+then check that the terms that we are forming make sense given our typing rules
+\citep{Curry1934}.
We wish to introduce rules of the form $\Gamma \vdash \termt : \tya$, which
reads ``in context $\Gamma$, term $\termt$ has type $\tya$''.
\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.
+It turns out that the STLC can be seen a natural deduction system for
+propositional logic. 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
\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}
+\subsection{A Bit of History}
+
+Logic frameworks and programming languages based on type theory have a long
+history. Per Martin-L\"{o}f described the first version of his theory in 1971,
+but then revised it since the original version was too impredicative and thus
+inconsistent\footnote{In the early version $\lcsetz : \lcsetz$, see section
+ \ref{sec:core-tt} for an explanation on why this causes problems.}. For this
+reason he gave a revised and consistent definition later \citep{Martin-Lof1984}.
+
+A related development is the one of the polymorphic $\lambda$-calculus, and
+specifically the previously mentioned System F, which was invented independently
+by Girard and Reynolds. An can be found in \citep{Reynolds1994}. The
+surprising fact is that while System F is impredicative it is still consistent
+and strongly normalising. Coquand and Huet further extended this line of work
+with the Calculus of Constructions (CoC) \citep{Coquand1986}.
+
+\subsection{A Core Type Theory}
+\label{sec:core-tt}
+
+The calculus I present follows the exposition in \citep{Thompson1991}, and as
+said previously is quite close to the original formulation of predicative ITT as
+found in \citep{Martin-Lof1984}.
+
\begin{center}
\axname{syntax}
\begin{eqnarray*}
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.
+While in the STLC values and types are kept well separated (values never go
+``right of the colon''), in ITT types can freely depend on values.
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$.
$\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.
+\item[``forall'' ($\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 the
+ interpretation of functions as infinitary products. We will just call it
+ ``dependent function'', reserving ``product'' for $\exists$.
+
+\item[``exists'' ($\exists$)] is a generalisation of $\wedge$ in the extended
+ STLC of section \ref{sec:curry-howard}, and thus we will call it ``dependent
+ product''. Like $\wedge$, it is formed by providing a pair of things. 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, infinitary $\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}
+the smallest equivalence relation extending $\bredc$, where $\bredc$ is the
+reflexive transitive closure of $\bred$; and we treat types that are equal
+according to $\defeq$ as the same. Another way of seeing $\defeq$ is this: when
+we want to compare two types for equality, we reduce them as far as possible and
+then check if they are equal\footnote{Note that when comparing terms we do it up
+ to $\alpha$-renaming. That is, we do not consider relabelling of variables as
+ a difference - for example $\abs{x : A}{x} \defeq \abs{y : A}{y}$.}. This
+works since not only each term has a normal form (ITT is strongly normalising),
+but the normal form is also unique; or in other words $\bred$ is confluent (if
+$\termt \bredc \termm$ and $\termt \bredc \termn$, then $\termm \bredc \termp$
+and $\termn \bredc \termp$). This measure makes sure that, for instance,
+$\app{(\abs{x : \lctype}{x})}{\lcbool} \defeq \lcbool$. The theme of equality
+is central and will be analysed better later.
+
+The theory presented is \emph{stratified}. We have a hierarchy of types
+$\lcset{0} : \lcset{1} : \lcset{2} : \dots$, so that there is no ``type of all
+types'', and our theory is predicative. The layers of the hierarchy are called
+``universes''. $\lcsetz : \lcsetz$ ITT is inconsistent due to Girard's paradox
+\citep{Hurkens1995}, and thus loses its well-behavedness. Some impredicativity
+sometimes has its place, either because the theory retain good properties
+(normalization, consistency, etc.) anyway, like in System F and CoC; or because
+we are at a stage at which we do not care - we will see instances of the last
+motivation later. Moreover, universes can be inferred mechanically
+\citep{Pollack1990}. It is also convenient to have a \emph{cumulative} theory,
+where $\lcset{n} : \lcset{m}$ iff $n < m$. We eschew these measures to keep the
+presentation simple.
+
+Lastly, the theory I present is fully explicit in the sense that the user has to
+specify every type when forming abstractions, products, etc. This can be a
+great burden if one wants to use the theory directly. Complete inference is
+undecidable (which is hardly surprising considering the role that types play)
+but partial inference (also called ``bidirectional type checking'' in this
+context) in the style of \citep{Pierce2000} will have to be deployed in a
+practical system. When showing examples obvious types will be omitted.
+
+Note that the Curry-Howard correspondence runs through ITT as it did with the
+STLC with the difference that ITT corresponds to an higher order propositional
+logic.
+
+\subsection{Base Types}
+
+While the ITT presented is a fairly complete logic, it is not that useful for
+programming. If we wish to make it better, we can add some base types to
+represent the data structures we know and love, such as numbers, lists, and
+trees.
+
+\newcommand{\lctrue}{\mathsf{true}}
+\newcommand{\lcfalse}{\mathsf{false}}
+
+\begin{center}
+ \axname{syntax}
+ \begin{eqnarray*}
+ \termsyn & ::= & ... \\
+ & | & \lcbool \separ \lctrue \separ \lcfalse
+ \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}
+
+
+\bibliographystyle{authordate1}
+\bibliography{background}
\end{document}