X-Git-Url: https://git.enpas.org/?a=blobdiff_plain;f=docs%2Fbackground.tex;h=4d21c160fffa80d216177e3b837f302923ece69e;hb=e432bd5f35a1ac262f0f2734802aa2d4ecb853f6;hp=6e939197a8bcf82ee3dad1f5488a4d06afc8df48;hpb=b1c43d9ab075249fd141e99ce4934dbd1ea67fc8;p=bitonic-mengthesis.git diff --git a/docs/background.tex b/docs/background.tex index 6e93919..4d21c16 100644 --- a/docs/background.tex +++ b/docs/background.tex @@ -6,6 +6,11 @@ \usepackage{graphicx} \usepackage{subcaption} +% Unicode +\usepackage{ucs} +\usepackage[utf8x]{inputenc} +% \usepackage{autofe} + %% ----------------------------------------------------------------------------- %% Fonts %% \usepackage[osf]{libertine} @@ -14,17 +19,19 @@ %% \IfFileExists{microtype.sty}{\usepackage{microtype}}{} %% ----------------------------------------------------------------------------- -%% TikZ stuff -%% \usepackage{tikz} -%% \usetikzlibrary{positioning} +%% Diagrams +% \usepackage{tikz} +% \usetikzlibrary{positioning} %% \usetikzlibrary{shapes} %% \usetikzlibrary{arrows} %% \usepackage{tikz-cd} %% \usepackage{pgfplots} +\usepackage[all]{xy} %% ----------------------------------------------------------------------------- %% Symbols -\usepackage{amssymb,amsmath} +\usepackage[fleqn]{amsmath} +\usepackage{amssymb} \usepackage{wasysym} \usepackage{turnstile} \usepackage{centernot} @@ -35,6 +42,18 @@ \usepackage{umoline} \usepackage[export]{adjustbox} \usepackage{multicol} +\usepackage{listingsutf8} +\lstset{ + basicstyle=\small\ttfamily, + extendedchars=\true, + inputencoding=utf8x, + xleftmargin=1cm +} +\usepackage{epigraph} + +%% ----------------------------------------------------------------------------- +%% Bibtex +\usepackage{natbib} %% Numbering depth %% \setcounter{secnumdepth}{0} @@ -62,23 +81,1310 @@ breaklinks=true, bookmarks=true, pdfauthor={Francesco Mazzoli }, - pdftitle={The Path Towards Observational Equality}, + pdftitle={Observational Equality}, colorlinks=false, pdfborder={0 0 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 Path Towards Observational Equality} -\author{Francesco Mazzoli \url{}} +\title{Observational Equality} +\author{Francesco Mazzoli \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{}}} \date{December 2012} \begin{document} \maketitle +\setlength{\tabcolsep}{12pt} + +\begin{abstract} +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. + +Section \ref{sec:types} I will give a very brief overview of STLC, and then +illustrate how it can be interpreted as a natural deduction system. Section +\ref{sec:itt} will introduce Inutitionistic Type Theory (ITT), which expands on +this concept, employing a more expressive logic. 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}. Section +\ref{sec:practical} will describe additions common in practical programming +languages based on ITT. + +Finally, I will 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. +\end{abstract} + +\tableofcontents + +\section{Simple and not-so-simple types} +\label{sec:types} + +\subsection{A note on notation} + +\newcommand{\appsp}{\hspace{0.07cm}} +\newcommand{\app}[2]{#1\appsp#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$}} +\newcommand{\lcsyn}[1]{\mathrm{\underline{#1}}} +\newcommand{\lccon}[1]{\mathsf{#1}} +\newcommand{\lcfun}[1]{\mathbf{#1}} +\newcommand{\tyarr}{\to} +\newcommand{\tysyn}{\mathit{type}} +\newcommand{\ctxsyn}{\mathit{context}} +\newcommand{\emptyctx}{\cdot} + +In the following sections I will introduce a lot of syntax, typing, and +reduction rules, along with examples. To make the exposition clearer, usually +the rules are preceded by what the rule looks like and what it shows (for +example \axdesc{typing}{\Gamma \vdash \termsyn : \tysyn}). + +In the languages presented I will also use different fonts for different things: +\begin{tabular}{c | l} + $\lccon{Sans}$ & Sans serif, capitalised, for type constructors. \\ + $\lccon{sans}$ & Sans serif, not capitalised, for data constructors. \\ + $\lcsyn{roman}$ & Roman, underlined, for the syntax of the language. \\ + $\lcfun{roman}$ & Roman, bold, for defined functions and values. \\ + $math$ & Math mode font for quantified variables and syntax elements. +\end{tabular} + +Moreover, I will from time to time give examples in the Haskell programming +language as defined in \citep{Haskell2010}, which I will typeset in +\texttt{typewriter} font. I assume that the reader is already familiar with +Haskell, plenty of good introductions are available \citep{LYAH,ProgInHask}. + +\subsection{Untyped $\lambda$-calculus} + +Along with Turing's machines, the earliest attempts to formalise computation +lead to the $\lambda$-calculus \citep{Church1936}. This early programming +language encodes computation with a minimal syntax and no `data' in the +traditional sense, but just functions. + +The syntax of $\lambda$-terms consists of just three things: variables, +abstractions, and applications: + +\begin{center} +\axname{syntax} +$$ +\begin{array}{rcl} + \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{array} +$$ +\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 future, I will use +$[\termt]$ as an abbreviation for $[\termt / x]$. 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. + +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): +\[ + \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 +\] +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 (where no reductions are +possible on the term or on its subterms) is called \emph{normal form}. + +\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 +\citep{Curry1934}. + +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: + +\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. I will 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{\phantom{1em}} + \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 \citep{Pierce2002}: +\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]{\lcsyn{fix} \appsp #1\absspace.\absspace #2} + +This makes the STLC Turing incomplete. We can recover the ability to loop by +adding a combinator that recurses: +$$ + \termsyn ::= \dotsb \separ \lcfix{x : \tysyn}{\termsyn} +$$ +\begin{center} + \begin{prooftree} + \AxiomC{$\Gamma;x : \tya \vdash \termt : \tya$} + \UnaryInfC{$\Gamma \vdash \lcfix{x : \tya}{\termt} : \tya$} + \end{prooftree} +\end{center} +$$ + \lcfix{x : \tya}{\termt} \bred \termt[\lcfix{x : \tya}{\termt}] +$$ +Which will deprive us of normalisation. There is however a price to pay, which +will be made clear in the next section. + +\subsection{The Curry-Howard correspondence} +\label{sec:curry-howard} + +\newcommand{\lcunit}{\lcfun{\langle\rangle}} + +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 wish 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 former 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 ($\bot$): that can 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, truth ($\top$) is the type with just one +trivial element ($\lcunit$). + +\newcommand{\lcinl}{\lccon{inl}\appsp} +\newcommand{\lcinr}{\lccon{inr}\appsp} +\newcommand{\lccase}[3]{\lcsyn{case}\appsp#1\appsp\lcsyn{of}\appsp#2\appsp#3} +\newcommand{\lcfst}{\lcfun{fst}\appsp} +\newcommand{\lcsnd}{\lcfun{snd}\appsp} +\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}{\lcfun{absurd}\appsp} +\newcommand{\lcabsurdd}[1]{\lcfun{absurd}_{#1}\appsp} + + +\begin{center} + \axname{syntax} + $$ + \begin{array}{rcl} + \termsyn & ::= & \dotsb \\ + & | & \lcinl \termsyn \separ \lcinr \termsyn \separ \lccase{\termsyn}{\termsyn}{\termsyn} \\ + & | & (\termsyn , \termsyn) \separ \lcfst \termsyn \separ \lcsnd \termsyn \\ + & | & \lcunit \\ + \tysyn & ::= & \dotsb \separ \tysyn \vee \tysyn \separ \tysyn \wedge \tysyn \separ \bot \separ \top + \end{array} + $$ +\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 \lcabsurdd{\tya} \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 I will not touch those subjects.}. + +Finally, going back to our $\lcsyn{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}{\lccon{Type}} +\newcommand{\lcite}[3]{\lcsyn{if}\appsp#1\appsp\lcsyn{then}\appsp#2\appsp\lcsyn{else}\appsp#3} +\newcommand{\lcbool}{\lccon{Bool}} +\newcommand{\lcforallz}[2]{\forall #1 \absspace.\absspace #2} +\newcommand{\lcforall}[3]{(#1 : #2) \tyarr #3} +\newcommand{\lcexists}[3]{(#1 : #2) \times #3} + +The STLC can be made more expressive in various ways. Henk Barendregt +succinctly expressed geometrically how we can expand our type system: + +$$ +\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] +} +$$ +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}$)] 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}}$)] 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. 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'. + +\section{Intuitionistic Type Theory and dependent types} +\label{sec:itt} + +\newcommand{\lcset}[1]{\lccon{Type}_{#1}} +\newcommand{\lcsetz}{\lccon{Type}} +\newcommand{\defeq}{\cong} + +\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 polymorphic $\lambda$-calculus, and specifically +the previously mentioned System F, which was developed independently by Girard +and Reynolds. An overview can be found in \citep{Reynolds1994}. The surprising +fact is that while System F is impredicative it is still consistent and strongly +normalising. \cite{Coquand1986} further extended this line of work with the +Calculus of Constructions (CoC). + +\subsection{A Core Type Theory} +\label{sec:core-tt} + +The calculus I present follows the exposition in \citep{Thompson1991}, and is +quite close to the original formulation of predicative ITT as found in +\citep{Martin-Lof1984}. + +\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)_{x.\termsyn} \separ \lcfst \termsyn \separ \lcsnd \termsyn \\ + & | & \bot \separ \lcabsurd_{\termsyn} \termsyn \\ + & | & \lcset{n} \\ + n & \in & \mathbb{N} + \end{eqnarray*} + + \axdesc{typing}{\Gamma \vdash \termsyn : \termsyn} + + \vspace{0.5cm} + + \begin{tabular}{c c c} + \AxiomC{\phantom{1em}} + \UnaryInfC{$\Gamma;x : \tya \vdash x : \tya$} + \DisplayProof + & + \AxiomC{$\Gamma \vdash \termt : \tya$} + \AxiomC{$\tya \defeq \tyb$} + \BinaryInfC{$\Gamma \vdash \termt : \tyb$} + \DisplayProof + & + \AxiomC{$\Gamma \vdash \termt : \bot$} + \UnaryInfC{$\Gamma \vdash \lcabsurdd{\tya} \termt : \tya$} + \DisplayProof + \end{tabular} + + \vspace{0.5cm} + + \begin{tabular}{c c} + \AxiomC{$\Gamma;x : \tya \vdash \termt : \tya$} + \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$} + \BinaryInfC{$\Gamma \vdash \app{\termt}{\termm} : \tyb[\termm ]$} + \DisplayProof + \end{tabular} + + \vspace{0.5cm} + + \begin{tabular}{c c} + \AxiomC{$\Gamma \vdash \termt : \tya$} + \AxiomC{$\Gamma \vdash \termm : \tyb[\termt ]$} + \BinaryInfC{$\Gamma \vdash (\termt, \termm)_{x.\tyb} : \lcexists{x}{\tya}{\tyb}$} + \noLine + \UnaryInfC{$\phantom{1em}$} + \DisplayProof + & + \AxiomC{$\Gamma \vdash \termt: \lcexists{x}{\tya}{\tyb}$} + \UnaryInfC{$\hspace{0.7cm} \Gamma \vdash \lcfst \termt : \tya \hspace{0.7cm}$} + \noLine + \UnaryInfC{$\Gamma \vdash \lcsnd \termt : \tyb[\lcfst \termt ]$} + \DisplayProof + \end{tabular} + + \vspace{0.5cm} + + \begin{tabular}{c c} + \AxiomC{$\phantom{1em}$} + \UnaryInfC{$\Gamma \vdash \lcset{n} : \lcset{n + 1}$} + \noLine + \UnaryInfC{$\phantom{1em}$} + \DisplayProof + & + \AxiomC{$\Gamma \vdash \tya : \lcset{n}$} + \AxiomC{$\Gamma; x : \tya \vdash \tyb : \lcset{m}$} + \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 ] \\ + \lcfst (\termt, \termm) & \bred & \termt \\ + \lcsnd (\termt, \termm) & \bred & \termm + \end{eqnarray*} +\end{center} + +When showing examples types will be omitted when this can be done without loss +of clarity, for example $\abs{x}{x}$ in place of $\abs{A : \lcsetz}{\abs{x : + A}{x}}$. I will also use $\lcsetz$ as $\lcset{0}$. + +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 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 $\tyarr$ and $\times$: 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 section +\ref{sec:base-types}. + +$\tyarr$ and $\times$ are at the core of the machinery of ITT: + +\begin{description} +\item[`forall' ($\tyarr$)] is a generalisation of $\tyarr$ in the STLC and + expresses universal quantification in our logic. It is often written with a + syntax closer to logic, e.g. $\forall x : \tya. \tyb$. In the + literature this is also known as `dependent product' and shown as $\Pi$, + following the interpretation of functions as infinitary products. I will just + call it `dependent function', reserving `product' for $\exists$. + +\item[`exists' ($\times$)] is a generalisation of $\wedge$ in the extended STLC + of section \ref{sec:curry-howard}, and thus I will call it `dependent + product'. Like $\wedge$, it is formed by providing a pair of things. In our + logic, it represents existential quantification. Similarly to $\tyarr$, it is + always written as $\exists x : \tya. \tyb$. + + 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 determines 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 define +$\defeq$ as the smallest equivalence relation extending $\bredc$, where $\bredc$ +is the reflexive transitive closure of $\bred$; and we treat types that are +relate 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 +there is a $p$ such that $\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. Type-formers like $\tyarr$ and $\times$ +take the least upper bound $\sqcup$ of the contained types. The layers of the +hierarchy are called `universes'. Theories where $\lcsetz : \lcsetz$ are +inconsistent due to Girard's paradox \citep{Hurkens1995}, and thus lose their +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 in section \ref{foo} +% TODO put citation here + +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} +\label{sec:base-types} + +\newcommand{\lctrue}{\lccon{true}} +\newcommand{\lcfalse}{\lccon{false}} +\newcommand{\lcw}[3]{\lccon{W} #1 : #2 \absspace.\absspace #3} +\newcommand{\lcnode}[4]{#1 \lhd_{#2 . #3} #4} +\newcommand{\lcnodez}[2]{#1 \lhd #2} +\newcommand{\lcited}[5]{\lcsyn{if}\appsp#1/#2\appsp.\appsp#3\appsp\lcsyn{then}\appsp#4\appsp\lcsyn{else}\appsp#5} +\newcommand{\lcrec}[4]{\lcsyn{rec}\appsp#1/#2\appsp.\appsp#3\appsp\lcsyn{with}\appsp#4} +\newcommand{\lcrecz}[2]{\lcsyn{rec}\appsp#1\appsp\lcsyn{with}\appsp#2} +\newcommand{\AxiomL}[1]{\Axiom$\fCenter #1$} +\newcommand{\UnaryInfL}[1]{\UnaryInf$\fCenter #1$} + +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. Apart from some unsurprising data types, we introduce $\lccon{W}$, a +very general tree-like structure useful to represent inductively defined types +and that will allow us to express structural recursion in an equally general +manner. + +\begin{center} + \axname{syntax} + \begin{eqnarray*} + \termsyn & ::= & \dots \\ + & | & \top \separ \lcunit \\ + & | & \lcbool \separ \lctrue \separ \lcfalse \separ \lcited{\termsyn}{x}{\termsyn}{\termsyn}{\termsyn} \\ + & | & \lcw{x}{\termsyn}{\termsyn} \separ \lcnode{\termsyn}{x}{\termsyn}{\termsyn} \separ \lcrec{\termsyn}{x}{\termsyn}{\termsyn} + \end{eqnarray*} + + \axdesc{typing}{\Gamma \vdash \termsyn : \termsyn} + + \vspace{0.5cm} + + \begin{tabular}{c c c} + \AxiomC{} + \UnaryInfC{$\hspace{0.2cm}\Gamma \vdash \top : \lcset{0} \hspace{0.2cm}$} + \noLine + \UnaryInfC{$\Gamma \vdash \lcbool : \lcset{0}$} + \DisplayProof + & + \AxiomC{} + \UnaryInfC{$\Gamma \vdash \lcunit : \top$} + \noLine + \UnaryInfC{\phantom{1em}} + \DisplayProof + & + \AxiomC{} + \UnaryInfC{$\Gamma \vdash \lctrue : \lcbool$} + \noLine + \UnaryInfC{$\Gamma \vdash \lcfalse : \lcbool$} + \DisplayProof + \end{tabular} + + \vspace{0.5cm} + + \begin{tabular}{c} + \AxiomC{$\Gamma \vdash \termt : \lcbool$} + \AxiomC{$\Gamma \vdash \termm : \tya[\lctrue]$} + \AxiomC{$\Gamma \vdash \termn : \tya[\lcfalse]$} + \TrinaryInfC{$\Gamma \vdash \lcited{\termt}{x}{\tya}{\termm}{\termn} : \tya[\termt]$} + \DisplayProof + \end{tabular} + + \vspace{0.5cm} + + \begin{tabular}{c} + \AxiomC{$\Gamma \vdash \tya : \lcset{n}$} + \AxiomC{$\Gamma; x : \tya \vdash \tyb : \lcset{m}$} + \BinaryInfC{$\Gamma \vdash \lcw{x}{\tya}{\tyb} : \lcset{n \sqcup m}$} + \DisplayProof + \end{tabular} + + \vspace{0.5cm} + + \begin{tabular}{c} + \AxiomC{$\Gamma \vdash \termt : \tya$} + \AxiomC{$\Gamma \vdash \termf : \tyb[\termt ] \tyarr \lcw{x}{\tya}{\tyb}$} + \BinaryInfC{$\Gamma \vdash \lcnode{\termt}{x}{\tyb}{\termf} : \lcw{x}{\tya}{\tyb}$} + \DisplayProof + \end{tabular} + + \vspace{0.5cm} + + \begin{tabular}{c} + \AxiomC{$\Gamma \vdash \termt: \lcw{x}{\tya}{\tyb}$} + \noLine + \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}]}}$} + \UnaryInfC{$\Gamma \vdash \lcrec{\termt}{x}{\tyc}{\termp} : \tyc[\termt]$} + \DisplayProof + \end{tabular} + + \vspace{0.5cm} + + \axdesc{reduction}{\termsyn \bred \termsyn} + \begin{eqnarray*} + \lcited{\lctrue}{x}{\tya}{\termt}{\termm} & \bred & \termt \\ + \lcited{\lcfalse}{x}{\tya}{\termt}{\termm} & \bred & \termm \\ + \lcrec{\lcnodez{\termt}{\termf}}{x}{\tya}{\termp} & \bred & \app{\app{\app{\termp}{\termt}}{\termf}}{(\abs{\termm}{\lcrec{\app{f}{\termm}}{x}{\tya}{\termp}})} + \end{eqnarray*} +\end{center} + +The introduction and elimination for $\top$ and $\lcbool$ are unsurprising. +Note that in the $\lcite{\dotsb}{\dotsb}{\dotsb}$ construct the type of the +branches are dependent on the value of the conditional. + +% TODO: explain better here + +The rules for $\lccon{W}$, on the other hand, are quite an eyesore. The idea +behind $\lccon{W}$ types is to build up `trees' where the number of `children' +of each node is dependent on the value in the node. This is captured by the +$\lhd$ constructor, where the argument on the left is the value, and the +argument on the right is a function that returns a child for each possible value +of $\tyb[\text{node value}]$, if $\lcw{x}{\tya}{\tyb}$. The recursor +$\lcrec{\termt}{x}{\tyc}{\termp}$ uses $p$ to inductively prove that +$\tyc[\termt]$ holds. + +\subsection{Some examples} + +Now we can finally provide some meaningful examples. Apart from omitting types, +I will also use some abbreviations: +\begin{itemize} + \item $\_\mathit{operator}\_$ to define infix operators + \item $\abs{x\appsp y\appsp z : \tya}{\dotsb}$ to define multiple abstractions at the same + time +\end{itemize} + +\subsubsection{Sum types} + +We would like to recover our sum type, or disjunction, $\vee$. This is easily +achieved with $\times$: +\[ +\begin{array}{rcl} + \_\vee\_ & = & \abs{\tya\appsp\tyb : \lcsetz}{\lcexists{x}{\lcbool}{\lcite{x}{\tya}{\tyb}}} \\ + \lcinl & = & \abs{x}{(\lctrue, x)} \\ + \lcinr & = & \abs{x}{(\lcfalse, x)} \\ + \lcfun{case} & = & \abs{x : \tya \vee \tyb}{\abs{f : \tya \tyarr \tyc}{\abs{g : \tyb \tyarr \tyc}{ \\ + & & \hspace{0.5cm} \app{(\lcited{\lcfst x}{b}{(\lcite{b}{A}{B}) \tyarr C}{f}{g})}{(\lcsnd x)}}}} +\end{array} +\] +What is going on here? We are using $\exists$ with $\lcbool$ as a tag, so that +we can choose between one of two types in the second element. In +$\lcfun{case}$ we use $\lcite{\lcfst x}{\dotsb}{\dotsb}$ to discriminate on the +tag, that is, the first element of $x : \tya \vee \tyb$. If the tag is true, +then we know that the second element is of type $\tya$, and we will apply $f$. +The same applies to the other branch, with $\tyb$ and $g$. + +\subsubsection{Naturals} + +Now it's time to showcase the power of $\lccon{W}$ types. +\begin{eqnarray*} + \lccon{Nat} & = & \lcw{b}{\lcbool}{\lcite{b}{\top}{\bot}} \\ + \lccon{zero} & = & \lcfalse \lhd \abs{z}{\lcabsurd z} \\ + \lccon{suc} & = & \abs{n}{(\lctrue \lhd \abs{\_}{n})} \\ + \lcfun{plus} & = & \abs{x\appsp y}{\lcrecz{x}{(\abs{b}{\lcite{b}{\abs{\_\appsp f}{\app{\lccon{suc}}{(\app{f}{\lcunit})}}}{\abs{\_\appsp\_}{y}}})}} +\end{eqnarray*} +Here we encode natural numbers through $\lccon{W}$ types. Each node contains a +$\lcbool$. If the $\lcbool$ is $\lcfalse$, then there are no children, since we +have a function $\bot \tyarr \lccon{Nat}$: this is our $0$. If it's $\lctrue$, +we need one child only: the predecessor. We recurse giving $\lcsyn{rec}$ a +function that handles the `base case' 0 when the $\lcbool$ is $\lctrue$, and the +inductive case otherwise. + +We postpone more complex examples after the introduction of inductive families +and pattern matching, since $\lccon{W}$ types get unwieldy very quickly. + +\subsection{Propositional Equality} +\label{sec:propeq} + +We can finally introduce one of the central subjects of my project: +propositional equality. + +\newcommand{\lceq}[3]{#2 =_{#1} #3} +\newcommand{\lceqz}[2]{#1 = #2} +\newcommand{\lcrefl}[2]{\lccon{refl}_{#1}\appsp #2} +\newcommand{\lcsubst}[3]{\lcfun{subst}\appsp#1\appsp#2\appsp#3} + +\begin{center} + \axname{syntax} + \begin{eqnarray*} + \termsyn & ::= & ... \\ + & | & \lceq{\termsyn}{\termsyn}{\termsyn} \separ \lcrefl{\termsyn}{\termsyn} \separ \lcsubst{\termsyn}{\termsyn}{\termsyn} + \end{eqnarray*} + + \axdesc{typing}{\Gamma \vdash \termsyn : \termsyn} + + \vspace{0.5cm} + + \begin{tabular}{c c} + \AxiomC{$\Gamma \vdash \termt : \tya$} + \UnaryInfC{$\Gamma \vdash \lcrefl{\tya}{\termt} : \lceq{\tya}{\termt}{\termt}$} + \DisplayProof + & + \AxiomC{$\Gamma \vdash \termp : \lceq{\tya}{\termt}{\termm}$} + \AxiomC{$\Gamma \vdash \tyb : \tya \tyarr \lcsetz$} + \AxiomC{$\Gamma \vdash \termn : \app{\tyb}{\termt}$} + \TrinaryInfC{$\Gamma \vdash \lcsubst{\termp}{\tyb}{\termn} : \app{\tyb}{\termm}$} + \DisplayProof + \end{tabular} + + \vspace{0.5cm} + + \axdesc{reduction}{\termsyn \bred \termsyn} + \begin{eqnarray*} + \lcsubst{(\lcrefl{\tya}{\termt})}{\tyb}{\termm} \bred \termm + \end{eqnarray*} +\end{center} + +Propositional equality internalises equality as a type. The only way to +introduce an equality proof is by reflexivity ($\lccon{refl}$). The eliminator +is in the style of `Leibnitz's law' of equality: `equals can be substituted for +equals' ($\lcfun{subst}$). The computation rule refers to the fact that every +proof of equality will be a $\lccon{refl}$. We can use $\neg +(\lceq{\tya}{x}{y})$ to express inequality. + +These elements conclude our presentation of a `core' type theory. For an +extended example of a similar theory in use see Section 6.2 of +\cite{Thompson1991}\footnote{Note that while I attempted to formalise the proof + in Agda, I found a bug in the book! See the errata for details: + \url{http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/errata.html}.}. The above +language and examples have been codified in Agda\footnote{More on Agda in the + next section.}, see appendix \ref{app:agda-code}. + +\section{A more useful language} +\label{sec:practical} + +While our core type theory equipped with $\lccon{W}$ types is very usefully +conceptually as a simple but complete language, things get messy very fast. In +this section I will present the elements that are usually included in theorem +provers or programming languages to make them usable by mathematicians or +programmers. + +All the features presented are present in the second version of the Agda system +\citep{Norell2007, Bove2009}. Agda follows a tradition of theorem provers based +on ITT with inductive families and pattern matching. The closest relative of +Agda, apart from previous versions, is Epigram \citep{McBride2004, EpigramTut}. +Coq is another notable theorem prover based on the same concepts, and the first +and most popular \citep{Coq}. + +The main difference between Coq and Agda/Epigram is that the former focuses on +theorem proving, while the latter also want to be useful as functional +programming languages, while still offering good tools to express +mathematics\footnote{In fact, currently, Agda is used almost exclusively to + express mathematics, rather than to program.}. This is reflected in a series +of differences that I will not discuss here (most notably the absence of tactics +but better support for pattern matching in Agda/Epigram). I will take the same +approach as Agda/Epigram and will give a perspective focused on functional +programming rather than theorem proving. Every feature will be presented as it +is Agda. + +\subsection{Bidirectional type checking} + +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 \cite{Pierce2000} will have to be deployed in a +practical system. + +\subsection{Inductive families} + +\newcommand{\lcdata}[1]{\lcsyn{data}\appsp #1} +\newcommand{\lcdb}{\ |\ } +\newcommand{\lcind}{\hspace{0.2cm}} +\newcommand{\lcwhere}{\appsp \lcsyn{where}} +\newcommand{\lclist}[1]{\app{\lccon{List}}{#1}} +\newcommand{\lcnat}{\lccon{Nat}} +\newcommand{\lcvec}[2]{\app{\app{\lccon{Vec}}{#1}}{#2}} + +Inductive families were first introduced by \cite{Dybjer1991}. For the reader +familiar with the recent developments present in the GHC compiler for Haskell, +inductive families will look similar to GADTs (Generalised Abstract Data Types) +\citep[Section 7.4.7]{GHC}. +Haskell style data types provide \emph{parametric polymorphism}, so that we can +define types that range over type parameters: +\begin{lstlisting} +List a = Nil | Cons a (List a) +\end{lstlisting} +In this way we define the \texttt{List} type once while allowing elements to be +of any type. In Haskell \texttt{List} will be a type constructor of kind +\texttt{* -> *}, while \texttt{Nil :: List a} and \texttt{Cons :: a -> List a -> List a}\footnote{Note that the \texttt{a}s are implicitly quantified type variables}. + +Inductive families bring this concept one step further by allowing some of the +parameters to be constrained by constructors. We call these `variable' +parameters `indices'. For example we might define natural numbers +\[ +\begin{array}{l} +\lcdata{\lcnat} : \lcsetz \lcwhere \\ + \begin{array}{l@{\ }l} + \lcind \lccon{zero} &: \lcnat \\ + \lcind \lccon{suc} &: \lcnat \tyarr \lcnat + \end{array} +\end{array} +\] +And then define a type for lists indexed by length: +\[ +\begin{array}{l} +\lcdata{\lccon{Vec}}\appsp (A : \lcsetz) : \lcnat \tyarr \lcsetz \lcwhere \\ + \begin{array}{l@{\ }l} + \lcind \lccon{nil} &: \lcvec{A}{\lccon{zero}} \\ + \lcind \_::\_ &: \{n : \lccon{Nat}\} \tyarr A \tyarr \lcvec{A}{n} \tyarr \lcvec{A}{\app{(\lccon{suc}}{n})} + \end{array} +\end{array} +\] +Note that contrary to the Haskell ADT notation, with inductive families we +explicitly list the types for the type and data constructors. In $\lccon{Vec}$, +$A$ is a parameter (same across all constructors) while the $\lcnat$ is an +index. In our syntax, in the $\lcsyn{data}$ declaration, things to the left of +the colon are parameters, while on the right we can define the type of indices. +Also note that the parameters' identifiers will be in scope across all +constructors, while indices' won't. + +In this $\lccon{Vec}$ example, when we form a new list the length is +$\lccon{zero}$. When we append a new element to an existing list of length $n$, +the new list is of length $\app{\lccon{suc}}{n}$, that is, one more than the +previous length. Also note that we are using the $\{n : \lcnat\} \tyarr \dotsb$ +syntax to indicate an argument that we will omit when using $\_::\_$. In the +future I shall also omit the type of these implicit parameters, in line with how +Agda works. + +Once we have $\lccon{Vec}$ we can do things much more safely than with normal +lists. For example, we can define an $\lcfun{head}$ function that returns the +first element of the list: +\[ +\begin{array}{l} +\lcfun{head} : \{A\ n\} \tyarr \lcvec{A}{(\app{\lccon{suc}}{n})} \tyarr A +\end{array} +\] +Note that we will not be able to provide this function with a +$\lcvec{A}{\lccon{zero}}$, since it needs an index which is a successor of some +number. + +\newcommand{\lcfin}[1]{\app{\lccon{Fin}}{#1}} + +If we wish to index a $\lccon{Vec}$ safely, we can define an inductive family +$\lcfin{n}$, which represents the family of numbers smaller than a given number +$n$: +\[ +\begin{array}{l} + \lcdata{\lccon{Fin}} : \lcnat \tyarr \lcsetz \lcwhere \\ + \begin{array}{l@{\ }l} + \lcind \lccon{fzero} &: \{n\} \tyarr \lcfin{(\app{\lccon{suc}}{n})} \\ + \lcind \lccon{fsuc} &: \{n\} \tyarr \lcfin{n} \tyarr \lcfin{(\app{\lccon{suc}}{n})} + \end{array} +\end{array} +\] +$\lccon{fzero}$ is smaller than any number apart from $\lccon{zero}$. Given +the family of numbers smaller than $n$, we can produce the family of numbers +smaller than $\app{\lccon{suc}}{n}$. Now we can define an `indexing' operation +for our $\lccon{Vec}$: +\[ +\begin{array}{l} +\_\lcfun{!!}\_ : \{A\ n\} \tyarr \lcvec{A}{n} \tyarr \lcfin{n} \tyarr A +\end{array} +\] +In this way we will be sure that the number provided as an index will be smaller +than the length of the $\lccon{Vec}$ provided. + +\subsubsection{Computing with inductive families} + +I have carefully avoided to define the functions that I mentioned as example, +since one question still is unanswered: `how do we work with inductive +families'? The most basic approach is to work with eliminators, that can be +automatically provided by the programming language for each data type defined. +For example the induction principle on natural numbers will serve as an +eliminator for $\lcnat$: +\[ +\begin{array}{l@{\ } c@{\ } l} + \lcfun{NatInd} & : & (A : \lcsetz) \tyarr \\ + & & A \tyarr (\lcnat \tyarr A \tyarr A) \tyarr \\ + & & \lcnat \tyarr A +\end{array} +\] + +That is, if we provide an $A$ (base case), and then given a number and an $A$ we +give the next $A$ (inductive step), then an $A$ can be computed for every +number. This can be expressed easily in Haskell: +\begin{lstlisting} +data Nat = Zero | Suc Nat +natInd :: a -> (Nat -> a -> a) -> Nat -> a +natInd z _ Zero = z +natInd z f (Suc n) = f n (natInd z f n) +\end{lstlisting} +However, in a dependent setting, we can do better: +\[ +\begin{array}{l@{\ } c@{\ } l} + \lcfun{NatInd} & : & (P : \lcnat \tyarr \lcsetz) \tyarr \\ + & & \app{P}{\lccon{zero}} \tyarr ((n : \lcnat) \tyarr \app{P}{n} \tyarr \app{P}{(\app{\lccon{suc}}{n})}) \tyarr \\ + & & (n : \lcnat) \tyarr \app{P}{n} +\end{array} +\] +This expresses the fact that the resulting type can be dependent on the number. +In other words, we are proving that $P$ holds for all $n : \lcnat$. + +Naturally a reduction rule will be associated with each eliminator: +$$ +\begin{array}{l c l} +\app{\app{\app{\app{\lcfun{NatInd}}{P}}{z}}{f}}{\lccon{zero}} & \bred & z \\ +\app{\app{\app{\app{\lcfun{NatInd}}{P}}{z}}{f}}{(\app{\lccon{suc}}{n})} & \bred & \app{\app{f}{n}}{(\app{\app{\app{\app{\lcfun{NatInd}}{P}}{z}}{f}}{n})} +\end{array} +$$ +Which echoes the \texttt{natInd} function defined in Haskell. An extensive +account on combinators and inductive families can be found in \cite{McBride2004}. + +\subsubsection{Pattern matching and guarded recursion} + +However, combinators are far more cumbersome to use than the techniques usually +employed in functional programming: pattern matching and recursion. +\emph{General} recursion cannot be added if we want to keep our theory free of +$\bot$. The common solution to this problem is to allow recursive calls only if +the arguments are structurally smaller than what the function received. Pattern +matching on the other hand gains considerable power with inductive families, +since when we match a constructor we are gaining information on the indices of +the family. Thus matching constructors will enable us to restrict patterns of +other arguments. + +Following this discipline defining $\lcfun{head}$ becomes easy: +\[ +\begin{array}{l} +\lcfun{head} : \{A\ n\} \tyarr \lcvec{A}{(\app{\lccon{suc}}{n})} \tyarr A \\ +\lcfun{head}\appsp(x :: \_) = x +\end{array} +\] +We need no case for $\lccon{nil}$, since the type checker knows that the +equation $n = \lccon{zero} = \app{\lccon{suc}}{n'}$ cannot be satisfied. + +More details on the implementations of inductive families can be found in +\citep{McBride2004, Norell2007}. + +\subsection{Friendlier universes} + +Universes as presented in section \ref{sec:core-tt} are quite cumbersome to work +with. Consider the example where we define an inductive family for booleans and +then we want to define an `if then else' eliminator: +\[ +\begin{array}{l} +\lcdata{\lcbool} : \lcsetz \lcwhere \\ + \begin{array}{l@{\ }l} + \lcind \lccon{true} &: \lcbool \\ + \lcind \lccon{false} &: \lcbool + \end{array}\\ +\\ +\lcfun{ite} : \{A : \lcset{0}\} \tyarr \lcbool \tyarr A \tyarr A \tyarr A \\ +\lcfun{ite} \appsp \lccon{true} \appsp x \appsp \_ = x \\ +\lcfun{ite} \appsp \lccon{false} \appsp \_ \appsp x = x +\end{array} +\] + +What if we want to use $\lcfun{ite}$ with types, for example $\lcfun{ite} \appsp +b \appsp \lcnat \appsp \lccon{Bool}$? Clearly $\lcnat$ is not of type +$\lcset{0}$, so we'd have to redefine $\lcfun{ite}$ with exactly the same body, +but different type signature. The problem is even more evident with type +families: for example our $\lccon{List}$ can only contain values, and if we want +to build lists of types we need to define another identical, but differently +typed, family. + +One option is to have a \emph{cumulative} theory, where $\lcset{n} : \lcset{m}$ +iff $n < m$. Then we can have a sufficiently large level in our type signature +and forget about it. Moreover, levels in this setting can be inferred +mechanically \citep{Pollack1990}, and thus we might lift the burden of universes +from the user. This is the approach taken by Epigram. + +Another more expressive (but currently more cumbersome) way is to expose +universes more, giving the user a way to quantify them and to take the least +upper bound of two levels. This is the approach taken by Agda, where for +example we can define a level-polymorphic $\times$: +\[ +\begin{array}{l} +\lcdata{\_\times\_}\ \{a\ b : \lccon{Level}\}\ (A : \lcset{a})\ (B : A \tyarr \lcset{b}) : \lcset{a \sqcup b} \lcwhere \\ + \lcind \_ , \_ : (x : A) \tyarr \app{B}{x} \tyarr A \times \app{B}{x} +\end{array} +\] +Levels can be made implicit as shown and can be almost always inferred. +However, having to decorate each type signature with quantified levels adds +quite a lot of noise. An inference algorithm that automatically quantifies and +instantiates levels (much like Hindley-Milner for types) seems feasible, but +currently not implemented anywhere. + +\subsection{Coinduction} + +One thing that the Haskell programmer will miss in ITT as presented is the +possibility to work with infinite data. The classic example is the manipulation +of infinite streams: +\begin{lstlisting} +zipWith :: (a -> b -> c) -> [a] -> [b] -> [c] + +fibs :: [Int] +fibs = 0 : 1 : zipWith (+) fibs (tail fibs) +\end{lstlisting} +While we can clearly write useful programs of this kind, we need to be careful, +since \texttt{length fibs}, for example, does not make much sense\footnote{Note + that if instead of machine \texttt{Int}s we used naturals as defined + previously, getting the length of an infinite list would a productive + definition.}. + +In less informal terms, we need to distinguish between \emph{productive} and +non-productive definitions. A productive definition is one for which pattern +matching on data will never diverge, which is the case for \texttt{fibs} but +not, for example, for \texttt{let x = x in x :: [Int]}. It is very desirable to +recover \emph{only} the productive definition so that total programs working +with infinite data can be written. + +This desire has lead to work on coindunction +% TODO finish + +\section{Many equalities} + +\subsection{Revision, and function extensionality} + +\epigraph{\emph{Half of my time spent doing research involves thinking up clever + schemes to avoid needing functional extensionality.}}{@larrytheliquid} + +Up to this point, I have introduced two equalities: \emph{definitional} equality +($\defeq$) and \emph{propositional} equality ($=_{\tya}$). + +Definitional equality relates terms that the type checker identifies as equal. +Our definition in section \ref{sec:core-tt} consisted of `reduce the two terms +to their normal forms, then check if they are equal (up to $\alpha$-renaming)'. +We can extend this definition in other ways so that more terms will be +identified as equal. Common ones include doing $\eta$-expansion, which converts +partial appications of functions, and congruence laws for $\lambda$: +\begin{center} + \begin{tabular}{c c c} + \AxiomC{$\Gamma \vdash \termf : \tya \tyarr \tyb$} + \UnaryInfC{$\Gamma \vdash \termf \defeq \abs{x}{\app{\termf}{x}}$} + \DisplayProof + & + \AxiomC{$\Gamma; x : \tya \vdash \termf \defeq g$} + \UnaryInfC{$\Gamma \vdash \abs{x}{\termf} \defeq \abs{x}{g}$} + \DisplayProof + \end{tabular} +\end{center} +Definitional equality is used in the type checking process, and this means that +in dependently typed languages type checking and evaluation are intertwined, +since we need to reduce types to normal forms to check if they are equal. It +also means that we need be able to compute under binders, for example to +determine that $\abs{x}{\app{(\abs{y}{y})}{\tya}} \defeq \abs{x}{\tya}$. This +process goes on `under the hood' and is outside the control of the user. + +Propositional equality, on the other hand, is available to the user to reason +about equality, internalising it as a type. As we have seen in section +\ref{sec:propeq} propositional equality is introduced by reflexivity and +eliminated with a `Leibnitz's law' style rule ($\lcfun{subst}$). Now that we +have inductive families and dependent pattern matching we do not need hard coded +rules to express this concepts\footnote{Here I use Agda notation, and thus I + cannot redefine $=$ and use subscripts, so I am forced to use $\equiv$ with + implicit types. After I will carry on using the old notation.}: +\[ +\begin{array}{l} + \lcdata{\lccon{\_\equiv\_}} : \{A : \lcsetz\} : A \tyarr A \tyarr \lcsetz \lcwhere \\ + \begin{array}{l@{\ }l} + \lcind \lccon{refl} &: \{x : A\} \tyarr x \equiv x + \end{array} \\ + \\ + \lcfun{subst} : \{A : \lcsetz\} \tyarr \{t\ m : A\} \tyarr t \equiv m \tyarr (B : A \tyarr \lcsetz) \tyarr \app{B}{t} \tyarr \app{B}{m} \\ + \lcfun{subst} \appsp \lccon{refl}\appsp B \appsp n = n +\end{array} +\] +Here matching $\lccon{refl}$ tells the type checker that $t \defeq m$, and thus +$\app{B}{t} \defeq \app{B}{m}$, so we can just return $n$. + +While propositional equality is a very useful construct, we can prove less terms +equal than we would like to. For example, if we have the usual functions +\[ +\begin{array}{l@{\ } l} +\lcfun{id} & : \{A : \lcsetz\} \tyarr A \tyarr A \\ +\lcfun{map} & : \{A\ B : \lcsetz\} \tyarr (A \tyarr B) \tyarr \app{\lccon{List}}{A} \tyarr \app{\lccon{List}}{B} +\end{array} +\] +we would certainly like to have a term of type +\[\{A\ B : \lcsetz\} \tyarr +\app{\lcfun{map}}{\lcfun{id}} =_{\lclist{A} \tyarr \lclist{B}} \lcfun{id}\] +We cannot do this in ITT, since the things on the sides of $=$ look too +different at the term level. What we can have is +\[ +\{A\ B : \lcsetz\} \tyarr (x : \lclist{A}) \tyarr \app{\app{\lcfun{map}}{\lcfun{id}}}{x} +=_{\lclist{B}} \app{\lcfun{id}}{x} +\] +Since the type checker has something to compute with (even if only a variable) +and reduce the two lists to equal normal forms. The root of this problem is +that \emph{function extensionality} does not hold: +\[ +\begin{array}{l@{\ } l} +\lcfun{ext} : & \{A\ B : \lcsetz\} \tyarr (f\ g : A \tyarr B) \tyarr \\ + & ((x : A) \tyarr \app{f}{x} =_{A} \app{g}{x}) \tyarr f =_{A \tyarr B} g +\end{array} +\] +Which is a long standing issue in ITT. + +\subsection{Extensional Type Theory and its problems} + +One way to `solve' the problem and gain extensionality is to allow the type +checker to derive definitional equality from propositional equality, introducing +what is known as the `equality reflection' rule: +\begin{center} + \begin{prooftree} + \AxiomC{$\Gamma \vdash t =_A m$} + \UnaryInfC{$\Gamma \vdash t \defeq m$} + \end{prooftree} +\end{center} +This jump from types to a metatheoretic relation has deep consequences. But +firstly, let's get extensionality out of the way. Given $\Gamma = \lcfun{eq} : +(x : A) \tyarr \app{f}{x} = \app{g}{x}$, we have: +\begin{center} + \begin{prooftree} + \AxiomC{$\Gamma; x : A \vdash \app{\lcfun{eq}}{x} : \app{f}{x} = \app{g}{x}$} + \RightLabel{(equality reflection)} + \UnaryInfC{$\Gamma; x : A \vdash \app{f}{x} \defeq \app{g}{x}$} + \RightLabel{(congruence for $\lambda$)} + \UnaryInfC{$\Gamma \vdash \abs{x : A}{\app{f}{x}} \defeq \abs{x : A}{\app{g}{x}}$} + \RightLabel{($\eta$-law)} + \UnaryInfC{$\Gamma \vdash f \defeq g$} + \RightLabel{($\lccon{refl}$)} + \UnaryInfC{$\Gamma \vdash f = g$} + \end{prooftree} +\end{center} +Since the above is possible, theories that include the equality reflection rule +are often called `Extensional Type Theories', or ETTs. A notable exponent of +this discipline is the NuPRL system \citep{Constable86}. Moreover, equality +reflection simplifies $\lcfun{subst}$-like operations, since if we have $t = m$ +and $\app{A}{t}$, then by equality reflection clearly $\app{A}{t} \defeq +\app{A}{m}$. + +However equality reflection comes at a great price. The first hit is that it is +now unsafe to compute under binders, since we can send the type checker into a +loop given that under binders we can have any equality proof we might want +(think about what happens with $\abs{x : \bot}{\dotsb}$), and thus we can +convince the type checker that a term has any type we might want. Secondly, +equality reflection is not syntax directed, thus the type checker would need to +`invent' proofs of propositional equality to prove two terms definitionally +equal, rendering the type checking process undecidable. Thus the type checker +needs to carry complete derivations for each typing judgement, instead of +relying on terms only. + +\subsection{Observational equality} + +A recent development by \cite{Altenkirch2007} promises to keep the well +behavedness of ITT while being able to gain many useful equality proofs, +including function extensionality. Starting from a theory similar to the one +presented in section \ref{sec:itt} but with only $\lcset{0}$, a propositional +subuniverse of $\lcsetz$ is introduced, plus a `decoding' function: + +\newcommand{\lcprop}{\lccon{Prop}} + +\begin{center} + \begin{tabular}{c c c} + \AxiomC{\phantom{1em}} + \UnaryInfC{$\Gamma \vdash \lcprop : \lcsetz$} + \noLine + \UnaryInfC{\phantom{1em}} + \DisplayProof + & + \AxiomC{\phantom{1em}} + \UnaryInfC{$\Gamma \vdash \bot : \lcprop$} + \noLine + \UnaryInfC{$\Gamma \vdash \top : \lcprop$} + \DisplayProof + & + \AxiomC{$\Gamma \vdash P : \lcprop$} + \AxiomC{$\Gamma \vdash Q : \lcprop$} + \BinaryInfC{$\Gamma \vdash P \wedge Q : \lcprop$} + \noLine + \UnaryInfC{\phantom{1em}} + \DisplayProof + \end{tabular} + + \vspace{0.5cm} + + \begin{tabular}{c} + \AxiomC{$\Gamma \vdash S : \lcsetz$} + \AxiomC{$\Gamma \vdash q : \lcprop$} + \BinaryInfC{$\Gamma \vdash p \wedge q : \lcprop$} + \noLine + \UnaryInfC{\phantom{1em}} + \DisplayProof + \end{tabular} +\end{center} + +\section{What to do} + + +\bibliographystyle{authordate1} +\bibliography{background} + +\appendix +\section{Agda code} +\label{app:agda-code} + +\lstset{ + xleftmargin=0pt +} + +\lstinputlisting{background.agda} + \end{document}