author = {{The Coq Team}},
title = {The Coq Proof Assistant},
url = {\url{coq.inria.fr}},
- year = {1984-2013},
+ howpublished = {\url{http://coq.inria.fr}},
+ year = 2013
}
+@online{GHC,
+ author = {{The GHC Team}},
+ title = {The Glorious Glasgow Haskell Compilation System User's Guide},
+ url = {http://www.haskell.org/ghc/docs/latest/html/users_guide/},
+ howpublished = {\url{http://www.haskell.org/ghc/docs/latest/html/users_guide/}},
+ year = 2013
+}
-@article{Vytiniotis2011,
-author = {Vytiniotis, Dimitrios and Jones, Simon Peyton and Schrijvers, Tom and Sulzmann, Martin},
-file = {:home/bitonic/docs/papers/outsidein.pdf:pdf},
-journal = {Journal of Functional Programming},
-number = {4-5},
-pages = {333--412},
-title = {{OutsideIn (X) Modular type inference with local assumptions}},
-url = {http://journals.cambridge.org/production/action/cjoGetFulltext?fulltextid=8274818},
-volume = {21},
-year = {2011}
+@online{EpigramTut,
+ author = {Conor McBride},
+ title = {Epigram: Practical Programming with Dependent Types},
+ url = {http://strictlypositive.org/epigram-notes.ps.gz},
+ howpublished = {\url{http://strictlypositive.org/epigram-notes.ps.gz}},
+ year = 2004
}
-@article{McBride2004,
-author = {McBride, Conor},
-doi = {10.1017/S0956796803004829},
-file = {:home/bitonic/docs/papers/view-from-the-left.ps.gz:gz},
-journal = {Journal of Functional Programming},
-month = jan,
-number = {1},
-pages = {69--111},
-title = {{The View from The Left}},
-url = {http://strictlypositive.org/view.ps.gz},
-volume = {14},
-year = {2004}
+
+
+@article{Altenkirch2010,
+author = {Altenkirch, Thorsten and Danielsson, N and L\"{o}h, A and Oury, Nicolas},
+file = {:home/bitonic/docs/papers/PiSigma.pdf:pdf},
+journal = {Functional and Logic \ldots},
+number = {Sheard 2005},
+title = {{$\Pi$$\Sigma$: dependent types without the sugar}},
+url = {http://www.springerlink.com/index/91W712G2806R575H.pdf},
+year = {2010}
}
@article{Altenkirch2007,
address = {New York, New York, USA},
url = {http://portal.acm.org/citation.cfm?doid=1292597.1292608},
year = {2007}
}
-@article{Pierce2000,
-author = {Pierce, Benjamin C. and Turner, David N.},
-doi = {10.1145/345099.345100},
-file = {:home/bitonic/docs/papers/local-type-inference.pdf:pdf},
-issn = {01640925},
-journal = {ACM Transactions on Programming Languages and Systems},
-month = jan,
-number = {1},
-pages = {1--44},
-title = {{Local type inference}},
-url = {http://portal.acm.org/citation.cfm?doid=345099.345100},
-volume = {22},
-year = {2000}
-}
-@article{Hurkens1995,
-author = {Hurkens, Antonius J.C.},
-file = {:home/bitonic/docs/papers/hurkens-paradox.pdf:pdf},
-journal = {Typed Lambda Calculi and Applications},
-title = {{A simplification of Girard's paradox}},
-url = {http://www.springerlink.com/index/W718604JN467672H.pdf},
-year = {1995}
-}
-@article{Reynolds1994,
-author = {Reynolds, John C.},
-file = {:home/bitonic/docs/papers/reynolds-polymorphic-lc.ps:ps},
-journal = {Logical Foundations of Functional Programming},
-title = {{An introduction to the polymorphic lambda calculus}},
-url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.7.9916\&rep=rep1\&type=pdf},
-year = {1994}
-}
-@article{Yorgey2012,
-address = {New York, New York, USA},
-author = {Yorgey, Brent a. and Weirich, Stephanie and Cretin, Julien and {Peyton Jones}, Simon and Vytiniotis, Dimitrios and Magalh\~{a}es, Jos\'{e} Pedro},
-doi = {10.1145/2103786.2103795},
-file = {:home/bitonic/docs/papers/haskell-promotion.pdf:pdf},
-isbn = {9781450311205},
-journal = {Proceedings of the 8th ACM SIGPLAN workshop on Types in language design and implementation - TLDI '12},
-pages = {53},
-publisher = {ACM Press},
-title = {{Giving Haskell a promotion}},
-url = {http://dl.acm.org/citation.cfm?doid=2103786.2103795},
-year = {2012}
-}
-@article{Sulzmann2007,
-address = {New York, New York, USA},
-author = {Sulzmann, Martin and Chakravarty, Manuel M. T. and Jones, Simon Peyton and Donnelly, Kevin},
-doi = {10.1145/1190315.1190324},
-file = {:home/bitonic/docs/papers/systemf-coercions.pdf:pdf},
-isbn = {159593393X},
-journal = {Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation - TLDI '07},
-pages = {53},
-publisher = {ACM Press},
-title = {{System F with type equality coercions}},
-url = {http://portal.acm.org/citation.cfm?doid=1190315.1190324},
-year = {2007}
-}
@article{Barendregt1991,
author = {Barendregt, Henk},
file = {:home/bitonic/docs/papers/lambda-cube.pdf:pdf},
url = {http://www.diku.dk/hjemmesider/ansatte/henglein/papers/barendregt1991.pdf},
year = {1991}
}
-@book{Martin-Lof1984,
-author = {Martin-L\"{o}f, Per},
-file = {:home/bitonic/docs/papers/martin-lof-tt.pdf:pdf},
-isbn = {8870881059},
-publisher = {Bibliopolis},
-title = {{Intuitionistic type theory}},
-year = {1984}
-}
-@article{Church1936,
-author = {Church, Alonzo},
-file = {:home/bitonic/docs/papers/church-lc.pdf:pdf},
-journal = {American journal of mathematics},
-number = {2},
-pages = {345--363},
-title = {{An unsolvable problem of elementary number theory}},
-url = {http://www.ams.org/leavingmsn?url=http://dx.doi.org/10.2307/2371045},
-volume = {58},
-year = {1936}
+@article{Bove2009,
+author = {Bove, Ana and Dybjer, Peter and Norell, Ulf},
+file = {:home/bitonic/docs/papers/agda-overview.pdf:pdf},
+journal = {Theorem Proving in Higher Order Logics},
+title = {{A brief overview of Agda - a functional language with dependent types}},
+url = {http://www.springerlink.com/index/h12lq70470983732.pdf},
+year = {2009}
}
-@article{Oury2008,
-address = {New York, New York, USA},
-author = {Oury, Nicolas and Swierstra, Wouter},
-doi = {10.1145/1411204.1411213},
-file = {:home/bitonic/docs/papers/powerofpi.pdf:pdf},
-isbn = {9781595939197},
-journal = {Proceeding of the 13th ACM SIGPLAN international conference on Functional programming - ICFP '08},
-pages = {39},
-publisher = {ACM Press},
-title = {{The power of Pi}},
-url = {http://portal.acm.org/citation.cfm?doid=1411204.1411213},
-year = {2008}
+@article{Brady2012,
+author = {Brady, Edwin},
+file = {:home/bitonic/docs/papers/idris-implementation.pdf:pdf},
+journal = {Unpublished draft},
+number = {November},
+title = {{Implementing General Purpose Dependently Typed Programming Languages}},
+url = {http://www.cs.st-andrews.ac.uk/~eb/drafts/impldtp.pdf},
+year = {2012}
}
@article{Chapman2010,
address = {New York, New York, USA},
url = {http://portal.acm.org/citation.cfm?doid=1863543.1863547},
year = {2010}
}
-@article{Pollack1990,
-author = {Pollack, Robert},
-file = {:home/bitonic/docs/papers/implicit-syntax.ps:ps},
-journal = {Informal Proceedings of First Workshop on Logical Frameworks},
-title = {{Implicit syntax}},
-url = {http://reference.kfupm.edu.sa/content/i/m/implicit\_syntax\_\_1183660.pdf},
-year = {1992}
+@article{Church1936,
+author = {Church, Alonzo},
+file = {:home/bitonic/docs/papers/church-lc.pdf:pdf},
+journal = {American journal of mathematics},
+number = {2},
+pages = {345--363},
+title = {{An unsolvable problem of elementary number theory}},
+url = {http://www.ams.org/leavingmsn?url=http://dx.doi.org/10.2307/2371045},
+volume = {58},
+year = {1936}
+}
+@article{Church1940,
+author = {Church, Alonzo},
+file = {:home/bitonic/docs/papers/church-stlc.pdf:pdf},
+journal = {J. Symb. Log.},
+number = {2},
+pages = {56--68},
+title = {{A formulation of the simple theory of types}},
+url = {http://www.ams.org/leavingmsn?url=http://dx.doi.org/10.2307/2266170},
+volume = {5},
+year = {1940}
}
@article{Coquand1986,
author = {Coquand, Thierry and Huet, Gerard},
url = {http://hal.inria.fr/docs/00/07/60/24/PDF/RR-0530.pdf},
year = {1986}
}
-@article{Brady2012,
-author = {Brady, Edwin},
-file = {:home/bitonic/docs/papers/idris-implementation.pdf:pdf},
-journal = {Unpublished draft},
-number = {November},
-title = {{Implementing General Purpose Dependently Typed Programming Languages}},
-url = {http://www.cs.st-andrews.ac.uk/~eb/drafts/impldtp.pdf},
-year = {2012}
-}
@article{Curry1934,
author = {Curry, Haskell B.},
file = {:home/bitonic/docs/papers/curry-stlc.pdf:pdf},
-journal = {Proceedings of the National Academy of Sciences of \ldots},
+journal = {Proceedings of the National Academy of Sciences of the United States of America},
number = {1930},
pages = {584--590},
title = {{Functionality in combinatory logic}},
volume = {511},
year = {1934}
}
-@article{Church1940,
-author = {Church, Alonzo},
-file = {:home/bitonic/docs/papers/church-stlc.pdf:pdf},
-journal = {J. Symb. Log.},
-number = {2},
-pages = {56--68},
-title = {{A formulation of the simple theory of types}},
-url = {http://www.ams.org/leavingmsn?url=http://dx.doi.org/10.2307/2266170},
-volume = {5},
-year = {1940}
+@article{Dybjer1991,
+author = {Dybjer, Peter},
+file = {:home/bitonic/docs/papers/dybjer-inductive.ps:ps},
+journal = {Logical Frameworks},
+title = {{Inductive sets and families in Martin-L\"{o}f's type theory and their set-theoretic semantics}},
+url = {http://books.google.com/books?hl=en\&lr=\&id=X9wfWwslFQIC\&oi=fnd\&pg=PA280\&dq=Inductive+Sets+and+Families+in+Martin-L\%C3\%B6f\%27s+Type+Theory+and+Their+Set-Theoretic+Semantics\&ots=LewzM17GcW\&sig=vF4GgtlEBSf1uwRV1o\_unDtLats},
+year = {1991}
+}
+@article{Hurkens1995,
+author = {Hurkens, Antonius J.C.},
+file = {:home/bitonic/docs/papers/hurkens-paradox.pdf:pdf},
+journal = {Typed Lambda Calculi and Applications},
+title = {{A simplification of Girard's paradox}},
+url = {http://www.springerlink.com/index/W718604JN467672H.pdf},
+year = {1995}
+}
+@book{Martin-Lof1984,
+author = {Martin-L\"{o}f, Per},
+file = {:home/bitonic/docs/papers/martin-lof-tt.pdf:pdf},
+isbn = {8870881059},
+publisher = {Bibliopolis},
+title = {{Intuitionistic type theory}},
+year = {1984}
+}
+@article{McBride2004,
+author = {McBride, Conor},
+doi = {10.1017/S0956796803004829},
+file = {:home/bitonic/docs/papers/view-from-the-left.ps.gz:gz},
+journal = {Journal of Functional Programming},
+month = jan,
+number = {1},
+pages = {69--111},
+title = {{The View from The Left}},
+url = {http://strictlypositive.org/view.ps.gz},
+volume = {14},
+year = {2004}
}
@phdthesis{Norell2007,
author = {Norell, Ulf},
url = {http://www.cse.chalmers.se/~ulfn/papers/thesis.pdf},
year = {2007}
}
-@article{Altenkirch2010,
-author = {Altenkirch, Thorsten and Danielsson, N and L\"{o}h, A and Oury, Nicolas},
-file = {:home/bitonic/docs/papers/PiSigma.pdf:pdf},
-journal = {Functional and Logic \ldots},
-number = {Sheard 2005},
-title = {{$\Pi$$\Sigma$: dependent types without the sugar}},
-url = {http://www.springerlink.com/index/91W712G2806R575H.pdf},
-year = {2010}
+@article{Oury2008,
+address = {New York, New York, USA},
+author = {Oury, Nicolas and Swierstra, Wouter},
+doi = {10.1145/1411204.1411213},
+file = {:home/bitonic/docs/papers/powerofpi.pdf:pdf},
+isbn = {9781595939197},
+journal = {Proceeding of the 13th ACM SIGPLAN international conference on Functional programming - ICFP '08},
+pages = {39},
+publisher = {ACM Press},
+title = {{The power of Pi}},
+url = {http://portal.acm.org/citation.cfm?doid=1411204.1411213},
+year = {2008}
}
-@article{Dybjer1991,
-author = {Dybjer, Peter},
-file = {:home/bitonic/docs/papers/dybjer-inductive.ps:ps},
-journal = {Logical Frameworks},
-title = {{Inductive sets and families in Martin-L\"{o}f's type theory and their set-theoretic semantics}},
-url = {http://books.google.com/books?hl=en\&lr=\&id=X9wfWwslFQIC\&oi=fnd\&pg=PA280\&dq=Inductive+Sets+and+Families+in+Martin-L\%C3\%B6f\%27s+Type+Theory+and+Their+Set-Theoretic+Semantics\&ots=LewzM17GcW\&sig=vF4GgtlEBSf1uwRV1o\_unDtLats},
-year = {1991}
+@article{Pierce2000,
+author = {Pierce, Benjamin C. and Turner, David N.},
+doi = {10.1145/345099.345100},
+file = {:home/bitonic/docs/papers/local-type-inference.pdf:pdf},
+issn = {01640925},
+journal = {ACM Transactions on Programming Languages and Systems},
+month = jan,
+number = {1},
+pages = {1--44},
+title = {{Local type inference}},
+url = {http://portal.acm.org/citation.cfm?doid=345099.345100},
+volume = {22},
+year = {2000}
+}
+@article{Pollack1990,
+author = {Pollack, Robert},
+file = {:home/bitonic/docs/papers/implicit-syntax.ps:ps},
+journal = {Informal Proceedings of First Workshop on Logical Frameworks},
+title = {{Implicit syntax}},
+url = {http://reference.kfupm.edu.sa/content/i/m/implicit\_syntax\_\_1183660.pdf},
+year = {1992}
+}
+@article{Reynolds1994,
+author = {Reynolds, John C.},
+file = {:home/bitonic/docs/papers/reynolds-polymorphic-lc.ps:ps},
+journal = {Logical Foundations of Functional Programming},
+title = {{An introduction to the polymorphic lambda calculus}},
+url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.7.9916\&rep=rep1\&type=pdf},
+year = {1994}
+}
+@article{Sulzmann2007,
+address = {New York, New York, USA},
+author = {Sulzmann, Martin and Chakravarty, Manuel M. T. and Jones, Simon Peyton and Donnelly, Kevin},
+doi = {10.1145/1190315.1190324},
+file = {:home/bitonic/docs/papers/systemf-coercions.pdf:pdf},
+isbn = {159593393X},
+journal = {Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation - TLDI '07},
+pages = {53},
+publisher = {ACM Press},
+title = {{System F with type equality coercions}},
+url = {http://portal.acm.org/citation.cfm?doid=1190315.1190324},
+year = {2007}
+}
+@article{Vytiniotis2011,
+author = {Vytiniotis, Dimitrios and Jones, Simon Peyton and Schrijvers, Tom and Sulzmann, Martin},
+file = {:home/bitonic/docs/papers/outsidein.pdf:pdf},
+journal = {Journal of Functional Programming},
+number = {4-5},
+pages = {333--412},
+title = {{OutsideIn (X) Modular type inference with local assumptions}},
+url = {http://journals.cambridge.org/production/action/cjoGetFulltext?fulltextid=8274818},
+volume = {21},
+year = {2011}
+}
+@article{Yorgey2012,
+address = {New York, New York, USA},
+author = {Yorgey, Brent a. and Weirich, Stephanie and Cretin, Julien and {Peyton Jones}, Simon and Vytiniotis, Dimitrios and Magalh\~{a}es, Jos\'{e} Pedro},
+doi = {10.1145/2103786.2103795},
+file = {:home/bitonic/docs/papers/haskell-promotion.pdf:pdf},
+isbn = {9781450311205},
+journal = {Proceedings of the 8th ACM SIGPLAN workshop on Types in language design and implementation - TLDI '12},
+pages = {53},
+publisher = {ACM Press},
+title = {{Giving Haskell a promotion}},
+url = {http://dl.acm.org/citation.cfm?doid=2103786.2103795},
+year = {2012}
}
\usepackage{multicol}
\usepackage{listings}
\lstset{
- basicstyle=\footnotesize\ttfamily,
+ basicstyle=\small\ttfamily,
extendedchars=\true,
- inputencoding=utf8x
+ inputencoding=utf8x,
+ xleftmargin=1cm
}
%% -----------------------------------------------------------------------------
breaklinks=true,
bookmarks=true,
pdfauthor={Francesco Mazzoli <fm2209@ic.ac.uk>},
- pdftitle={The Paths Towards Observational Equality},
+ pdftitle={Observational Equality},
colorlinks=false,
pdfborder={0 0 0}
}
% avoid problems with \sout in headers with hyperref:
\pdfstringdefDisableCommands{\renewcommand{\sout}{}}
-\title{The Paths Towards Observational Equality}
+\title{Observational Equality}
\author{Francesco Mazzoli \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{<fm2209@ic.ac.uk>}}}
\date{December 2012}
\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.
-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. 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: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 the status of practical programming languages
+based on ITT.
-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.
+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{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 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:
+\subsection{A note on notation}
\newcommand{\appsp}{\hspace{0.07cm}}
\newcommand{\app}[2]{#1\appsp#2}
\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}
+
+\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{center}
\axdesc{reduction}{\termsyn \bred \termsyn}
-$$\app{(\abs{x}{\termt})}{\termm} \bred \termt[\termm ]$$
+$$\app{(\abs{x}{\termt})}{\termm} \bred \termt[\termm / x]$$
\end{center}
-Where $\termt[\termm ]$ expresses the operation that substitutes all
+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 ]$. In the systems presented, the
+$[\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.
-% % 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):
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$$
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.
+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
\vspace{0.5cm}
\begin{tabular}{c c c}
- \AxiomC{}
+ \AxiomC{\phantom{1em}}
\UnaryInfC{$\Gamma; x : \tya \vdash x : \tya$}
\DisplayProof
&
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
+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
\app{(\abs{x : ?}{\app{x}{x}})}{(\abs{x : ?}{\app{x}{x}})}
\end{equation*}
-\newcommand{\lcfix}[2]{\mathsf{fix} \appsp #1\absspace.\absspace #2}
+\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 ::= \dots \separ \lcfix{x : \tysyn}{\termsyn}
+ \termsyn ::= \dotsb \separ \lcfix{x : \tysyn}{\termsyn}
$$
\begin{center}
\begin{prooftree}
\end{prooftree}
\end{center}
$$
- \lcfix{x : \tya}{\termt} \bred \termt[(\lcfix{x : \tya}{\termt}) ]
+ \lcfix{x : \tya}{\termt} \bred \termt[\lcfix{x : \tya}{\termt}]
$$
-
-However, we will keep STLC without such a facility. In the next section we shall
-see why that is preferable for our needs.
+Which will deprive us of normalisation for every term.
\subsection{The Curry-Howard correspondence}
\label{sec:curry-howard}
-\newcommand{\lcunit}{\mathsf{\langle\rangle}}
+\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 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:
+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 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}\appsp}
-\newcommand{\lcinr}{\mathsf{inr}\appsp}
+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: 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}{\mathsf{fst}\appsp}
-\newcommand{\lcsnd}{\mathsf{snd}\appsp}
+\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{\andint}{\wedge I}
\newcommand{\andel}{\wedge E_{1,2}}
\newcommand{\botel}{\bot E}
-\newcommand{\lcabsurd}{\mathsf{absurd}\appsp}
-\newcommand{\lcabsurdd}[1]{\mathsf{absurd}_{#1}\appsp}
+\newcommand{\lcabsurd}{\lcfun{absurd}\appsp}
+\newcommand{\lcabsurdd}[1]{\lcfun{absurd}_{#1}\appsp}
\begin{center}
\axname{syntax}
$$
\begin{array}{rcl}
- \termsyn & ::= & \dots \\
+ \termsyn & ::= & \dotsb \\
& | & \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
+ \tysyn & ::= & \dotsb \separ \tysyn \vee \tysyn \separ \tysyn \wedge \tysyn \separ \bot \separ \top
\end{array}
$$
\end{center}
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.}.
+ behaviour to classical logic, but I will not touch those subjects.}.
-Finally, going back to our $\mathsf{fix}$ combinator, it's now easy to see how
+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
\subsection{Extending the STLC}
-\newcommand{\lctype}{\mathsf{Type}}
+\newcommand{\lctype}{\lccon{Type}}
\newcommand{\lcite}[3]{\lcsyn{if}\appsp#1\appsp\lcsyn{then}\appsp#2\appsp\lcsyn{else}\appsp#3}
-\newcommand{\lcbool}{\mathsf{Bool}}
+\newcommand{\lcbool}{\lccon{Bool}}
\newcommand{\lcforallz}[2]{\forall #1 \absspace.\absspace #2}
\newcommand{\lcforall}[3]{(#1 : #2) \tyarr #3}
-\newcommand{\lcexists}[3]{\exists #1 : #2 \absspace.\absspace #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:
-\begin{equation*}
+$$
\xymatrix@!0@=1.5cm{
& \lambda\omega \ar@{-}[rr]\ar@{-}'[d][dd]
& & \lambda C \ar@{-}[dd]
\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[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 (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.
+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]{\mathsf{Type}_{#1}}
-\newcommand{\lcsetz}{\mathsf{Type}}
-\newcommand{\defeq}{\equiv}
+\newcommand{\lcset}[1]{\lccon{Type}_{#1}}
+\newcommand{\lcsetz}{\lccon{Type}}
+\newcommand{\defeq}{\cong}
\subsection{A Bit of History}
\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 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} Huet further extended this line of
-work with the Calculus of Constructions (CoC).
+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 as
-said previously is quite close to the original formulation of predicative ITT as
-found in \citep{Martin-Lof1984}.
+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}
\vspace{0.5cm}
\begin{tabular}{c c c}
- \AxiomC{}
- \RightLabel{var}
+ \AxiomC{\phantom{1em}}
\UnaryInfC{$\Gamma;x : \tya \vdash x : \tya$}
\DisplayProof
&
- \AxiomC{$\Gamma \vdash \termt : \bot$}
- \UnaryInfC{$\Gamma \vdash \lcabsurdd{\tya} \termt : \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}
\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}$}
\vspace{0.5cm}
\begin{tabular}{c c}
- \AxiomC{}
+ \AxiomC{$\phantom{1em}$}
\UnaryInfC{$\Gamma \vdash \lcset{n} : \lcset{n + 1}$}
+ \noLine
+ \UnaryInfC{$\phantom{1em}$}
\DisplayProof
&
\AxiomC{$\Gamma \vdash \tya : \lcset{n}$}
\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
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 $\exists$: if a
+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 $\exists$ are at the core of the machinery of ITT:
+$\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 : \mathsf{Bool}. \dotsb$. In the
+ 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. We will just
+ following the interpretation of functions as infinitary products. I 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
+\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.
+ 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 decides which type the second
+ 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 $\defeq$ as
-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.
+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
\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 \cite{Pierce2000} will have to be deployed in a
-practical system. 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}}$.
+we are at a stage at which we do not care - we will see instances of the latter
+later.
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.
-% TODO describe abbreviations somewhere
-% I will use various abbreviations:
-% \begin{itemize}
-% \item $\lcsetz$ for $\lcset{0}$
-% \item $\tya \tyarr \tyb$ for $\lcforall{-}{\tya}{\tyb}$, when $\tyb$ does not
-% depend on the value of type $\tya$
-% \item $(
-
\subsection{Base Types}
\label{sec:base-types}
-\newcommand{\lctrue}{\mathsf{true}}
-\newcommand{\lcfalse}{\mathsf{false}}
-\newcommand{\lcw}[3]{\mathsf{W} #1 : #2 \absspace.\absspace #3}
+\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}
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 $\mathsf{W}$, a
-very general tree-like structure useful to represent inductively defined types.
+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}
&
\AxiomC{}
\UnaryInfC{$\Gamma \vdash \lcunit : \top$}
+ \noLine
+ \UnaryInfC{\phantom{1em}}
\DisplayProof
&
\AxiomC{}
\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 \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}
Note that in the $\lcite{\dotsb}{\dotsb}{\dotsb}$ construct the type of the
branches are dependent on the value of the conditional.
-The rules for $\mathsf{W}$, on the other hand, are quite an eyesore. The idea
-behind $\mathsf{W}$ types is to build up `trees' where shape of 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
+% 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}
\subsubsection{Sum types}
We would like to recover our sum type, or disjunction, $\vee$. This is easily
-done with $\exists$:
+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)} \\
- \mathsf{case} & = & \abs{x : \tya \vee \tyb}{\abs{f : \tya \tyarr \tyc}{\abs{g : \tyb \tyarr \tyc}{ \\
+ \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
-$\mathsf{case}$ we use $\lcite{\lcfst x}{\dotsb}{\dotsb}$ to discriminate on the
+$\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 $\mathsf{W}$ types.
+Now it's time to showcase the power of $\lccon{W}$ types.
\begin{eqnarray*}
- \mathsf{Nat} & = & \lcw{b}{\lcbool}{\lcite{b}{\top}{\bot}} \\
- \mathsf{zero} & = & \lcfalse \lhd \abs{z}{\lcabsurd z} \\
- \mathsf{suc} & = & \abs{n}{(\lctrue \lhd \abs{\_}{n})} \\
- \mathsf{plus} & = & \abs{x\appsp y}{\lcrecz{x}{(\abs{b}{\lcite{b}{\abs{\_\appsp f}{\app{\mathsf{suc}}{(\app{f}{\lcunit})}}}{\abs{\_\appsp\_}{y}}})}}
+ \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 $\mathsf{W}$ types. Each node contains a
+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 \mathsf{Nat}$: this is our $0$. If it's $\lctrue$,
-we need one child only: the predecessor. Similarly, we recurse giving to
-$\lcsyn{rec}$ a function that handles the `base case' 0 when the $\lcbool$ is
-$\lctrue$, and the inductive case otherwise.
+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 $\mathsf{W}$ types get unwieldy very quickly.
+and pattern matching, since $\lccon{W}$ types get unwieldy very quickly.
-\subsubsection{Propositional Equality}
+\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]{\mathsf{refl}_{#1}\appsp #2}
-\newcommand{\lcsubst}[3]{\mathsf{subst}\appsp#1\appsp#2\appsp#3}
+\newcommand{\lcrefl}[2]{\lccon{refl}_{#1}\appsp #2}
+\newcommand{\lcsubst}[3]{\lcfun{subst}\appsp#1\appsp#2\appsp#3}
\begin{center}
\axname{syntax}
\end{eqnarray*}
\end{center}
-Propositional equality internalises equality as a type. This lets us prove
-useful things. The only way to introduce an equality proof is by reflexivity
-($\mathsf{refl}$). The eliminator is in the style of `Leibnitz's law' of
-equality: `equals can be substituted for equals' ($\mathsf{subst}$). The
-computation rule refers to the fact that every canonical proof of equality will
-be a $\mathsf{refl}$. We can use $\neg (\lceq{\tya}{x}{y})$ to express
-inequality.
+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 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:
+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}.
+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 $\mathsf{W}$ types is very usefully
+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 we will present the elements that are usually include in theorem
+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, except for quotient types, are present in the second
-version of the Agda system, which is described in the PhD thesis of the author
-\citep{Norell2007}. 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, whose type theory is described in
-\cite{McBride2004}. Coq is another notable theorem prover based on the same
-concepts, and the first and most popular \cite{Coq}.
+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
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 present in Agda (if possible, since some features are not present in Agda
-yet).
+is Agda.
+
+\subsection{Friendlier universes}
+
+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.
+
+\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{\lcdb}{\ |\ }
\newcommand{\lcind}{\hspace{0.2cm}}
\newcommand{\lcwhere}{\appsp \lcsyn{where}}
-\newcommand{\lclist}[1]{\app{\mathsf{List}}{#1}}
-\newcommand{\lcnat}{\app{\mathsf{Nat}}}
-\newcommand{\lcvec}[2]{\app{\app{\mathsf{Vec}}{#1}}{#2}}
+\newcommand{\lclist}[1]{\app{\lccon{List}}{#1}}
+\newcommand{\lcnat}{\app{\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).
-% TODO: add citation
+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{array}{l}
-\lcdata{\lclist{A}} = \mathsf{Nil} \lcdb A :: \lclist{A}
+\lcdata{\lclist{A}} = \lccon{Nil} \lcdb A :: \lclist{A}
\end{array}
\]
-In this way we define the $\mathsf{List}$ type once while allowing elements to
-be of any type. $\mathsf{List}$ will be a type constructor of type $\lcsetz
-\tyarr \lcsetz$, while $\mathsf{nil} : \lcforall{A}{\lcsetz}{\lclist{A}}$ and
+In this way we define the $\lccon{List}$ type once while allowing elements to
+be of any type. $\lccon{List}$ will be a type constructor of type $\lcsetz
+\tyarr \lcsetz$, while $\lccon{nil} : \lcforall{A}{\lcsetz}{\lclist{A}}$ and
$\_::\_ : \lcforall{A}{\lcsetz}{A \tyarr \lclist{A} \tyarr \lclist{A}}$.
Inductive families bring this concept one step further by allowing some of the
-parameters to be constrained in constructors. We call these parameters
-`indices'. For example we might define natural numbers
+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 \mathsf{zero} &: \lcnat \\
- \lcind \mathsf{suc} &: \lcnat \tyarr \lcnat
+ \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{\mathsf{Vec}}\appsp (A : \lcsetz) : \lcnat \tyarr \lcsetz \lcwhere \\
+\lcdata{\lccon{Vec}}\appsp (A : \lcsetz) : \lcnat \tyarr \lcsetz \lcwhere \\
\begin{array}{l@{\ }l}
- \lcind \mathsf{nil} &: \lcvec{A}{\mathsf{zero}} \\
- \lcind \_::\_ &: \{n : \mathsf{Nat}\} \tyarr A \tyarr \lcvec{A}{n} \tyarr \lcvec{A}{\app{(\mathsf{suc}}{n})}
+ \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 constructor and data constructors. In
-$\mathsf{Vec}$, $A$ is a parameter (same across all constructors) while the
-$\lcnat$ is an integer. 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 can be named across all
-constructors, while indices can't.
-
-In this $\mathsf{Vec}$ example, when we form a new list the length is
-$\mathsf{zero}$. When we append a new element to an existing list of length
-$n$, the new list is of length $\app{\mathsf{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
-how Agda works.
-
-Once we have our $\mathsf{Vec}$ we can do things much more safely than with
-normal lists. For example, we can define an $\mathsf{head}$ function that
-returns the first element of the list:
+$\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}
-\mathsf{head} : \{A\ n\} \tyarr \lcvec{A}{(\app{\mathsf{suc}}{n})} \tyarr A
+\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}{\mathsf{zero}}$, since it needs an index which is a successor of some
+$\lcvec{A}{\lccon{zero}}$, since it needs an index which is a successor of some
number.
-\newcommand{\lcfin}[1]{\app{\mathsf{Fin}}{#1}}
+\newcommand{\lcfin}[1]{\app{\lccon{Fin}}{#1}}
-If we wish to index a $\mathsf{Vec}$ safely, we can define an inductive family
+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{\mathsf{Fin}} : \lcnat \tyarr \lcsetz \lcwhere \\
+ \lcdata{\lccon{Fin}} : \lcnat \tyarr \lcsetz \lcwhere \\
\begin{array}{l@{\ }l}
- \lcind \mathsf{fzero} &: \{n\} \tyarr \lcfin{n} \\
- \lcind \mathsf{fsuc} &: \{n\} \tyarr (i : \lcfin{n}) \tyarr \lcfin{(\app{\mathsf{suc}}{n})}
+ \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}
\]
-$\mathsf{fzero}$ is smaller than any number apart from $\mathsf{zero}$. Given
-the family of numbers smaller than $i$, we can produce the family of numbers
-smaller than $\app{\mathsf{suc}}{n}$. Now we can define an `indexing' operation
-for our $\mathsf{Vec}$:
+$\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}
-\_\mathsf{!!}\_ : \{A\ n\} \tyarr \lcvec{A}{n} \tyarr \lcfin{n} \tyarr A
+\_\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 $\mathsf{Vec}$ provided.
+than the length of the $\lccon{Vec}$ provided.
+\subsubsection{Computing with inductive families}
-\subsection{Pattern matching}
+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}
+\]
-\subsection{Guarded recursion}
+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$.
-\subsection{Corecursion}
+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.
-\subsection{Quotient types}
+More details on the implementations of inductive families can be found in
+\citep{McBride2004, Norell2007}.
+\subsection{Corecursion}
\section{Why dependent types?}
\subsection{Revision}
-\subsection{Extensional equality and its problems}
+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 way 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 $\lambda$s, 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} \cong \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.
+
+\subsection{Extensional type theory and its problems}
\subsection{Observational equality}
projects / bitonic-mengthesis.git / commitdiff