year = {2002}
}
+@online{Coq,
+ author = {{The Coq Team}},
+ title = {The Coq Proof Assistant},
+ url = {\url{coq.inria.fr}},
+ year = {1984-2013},
+}
-@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{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{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{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}
}
-@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}
+@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{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{Chapman2010,
address = {New York, New York, USA},
url = {http://portal.acm.org/citation.cfm?doid=1863543.1863547},
year = {2010}
}
-@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{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{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},
volume = {511},
year = {1934}
}
-@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}
+@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}
}
@phdthesis{Norell2007,
author = {Norell, Ulf},
url = {http://www.cse.chalmers.se/~ulfn/papers/thesis.pdf},
year = {2007}
}
-@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{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{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{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{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}
}
\usepackage{graphicx}
\usepackage{subcaption}
+% Unicode
+\usepackage{ucs}
+\usepackage[utf8x]{inputenc}
+% \usepackage{autofe}
+
%% -----------------------------------------------------------------------------
%% Fonts
%% \usepackage[osf]{libertine}
%% -----------------------------------------------------------------------------
%% Symbols
-\usepackage{amssymb,amsmath}
+\usepackage[fleqn]{amsmath}
+\usepackage{amssymb}
\usepackage{wasysym}
\usepackage{turnstile}
\usepackage{centernot}
\usepackage{umoline}
\usepackage[export]{adjustbox}
\usepackage{multicol}
+\usepackage{listings}
+\lstset{
+ basicstyle=\footnotesize\ttfamily,
+ extendedchars=\true,
+ inputencoding=utf8x
+}
%% -----------------------------------------------------------------------------
%% Bibtex
The syntax of $\lambda$-terms consists of just three things: variables,
abstractions, and applications:
-\newcommand{\appspace}{\hspace{0.07cm}}
-\newcommand{\app}[2]{#1\appspace#2}
+\newcommand{\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}
\begin{center}
\axname{syntax}
-\begin{eqnarray*}
+$$
+\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{eqnarray*}
+\end{array}
+$$
\end{center}
These few elements are of remarkable expressiveness, and in fact Turing
complete. As a corollary, we must be able to devise a term that reduces forever
(`loops' in imperative terms):
-\begin{equation*}
+\[
\app{(\abs{x}{\app{x}{x}})}{(\abs{x}{\app{x}{x}})} \bred \app{(\abs{x}{\app{x}{x}})}{(\abs{x}{\app{x}{x}})} \bred \dotsb
-\end{equation*}
+\]
Terms that can be reduced only a finite number of times (the non-looping ones)
are said to be \emph{normalising}, and the `final' term is called \emph{normal
form}. These concepts (reduction and normal forms) will run through all the
\app{(\abs{x : ?}{\app{x}{x}})}{(\abs{x : ?}{\app{x}{x}})}
\end{equation*}
-\newcommand{\lcfix}[2]{\mathsf{fix} \appspace #1\absspace.\absspace #2}
+\newcommand{\lcfix}[2]{\mathsf{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:
-\begin{equation*}
+$$
\termsyn ::= \dots \separ \lcfix{x : \tysyn}{\termsyn}
-\end{equation*}
+$$
\begin{center}
\begin{prooftree}
\AxiomC{$\Gamma;x : \tya \vdash \termt : \tya$}
\UnaryInfC{$\Gamma \vdash \lcfix{x : \tya}{\termt} : \tya$}
\end{prooftree}
\end{center}
-\begin{equation*}
+$$
\lcfix{x : \tya}{\termt} \bred \termt[(\lcfix{x : \tya}{\termt}) ]
-\end{equation*}
+$$
However, we will keep STLC without such a facility. In the next section we shall
see why that is preferable for our needs.
type is presented, then we can derive any type, which expresses absurdity.
Conversely, $\top$ is the type with just one trivial element, $\lcunit$.
-\newcommand{\lcinl}{\mathsf{inl}\appspace}
-\newcommand{\lcinr}{\mathsf{inr}\appspace}
-\newcommand{\lccase}[3]{\lcsyn{case}\appspace#1\appspace\lcsyn{of}\appspace#2\appspace#3}
-\newcommand{\lcfst}{\mathsf{fst}\appspace}
-\newcommand{\lcsnd}{\mathsf{snd}\appspace}
+\newcommand{\lcinl}{\mathsf{inl}\appsp}
+\newcommand{\lcinr}{\mathsf{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{\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}\appspace}
-\newcommand{\lcabsurdd}[1]{\mathsf{absurd}_{#1}\appspace}
+\newcommand{\lcabsurd}{\mathsf{absurd}\appsp}
+\newcommand{\lcabsurdd}[1]{\mathsf{absurd}_{#1}\appsp}
+
\begin{center}
\axname{syntax}
- \begin{eqnarray*}
+ $$
+ \begin{array}{rcl}
\termsyn & ::= & \dots \\
& | & \lcinl \termsyn \separ \lcinr \termsyn \separ \lccase{\termsyn}{\termsyn}{\termsyn} \\
& | & (\termsyn , \termsyn) \separ \lcfst \termsyn \separ \lcsnd \termsyn \\
& | & \lcunit \\
\tysyn & ::= & \dots \separ \tysyn \vee \tysyn \separ \tysyn \wedge \tysyn \separ \bot \separ \top
- \end{eqnarray*}
+ \end{array}
+ $$
\end{center}
\begin{center}
\axdesc{typing}{\Gamma \vdash \termsyn : \tysyn}
\subsection{Extending the STLC}
\newcommand{\lctype}{\mathsf{Type}}
-\newcommand{\lcite}[3]{\lcsyn{if}\appspace#1\appspace\lcsyn{then}\appspace#2\appspace\lcsyn{else}\appspace#3}
+\newcommand{\lcite}[3]{\lcsyn{if}\appsp#1\appsp\lcsyn{then}\appsp#2\appsp\lcsyn{else}\appsp#3}
\newcommand{\lcbool}{\mathsf{Bool}}
\newcommand{\lcforallz}[2]{\forall #1 \absspace.\absspace #2}
-\newcommand{\lcforall}[3]{\forall #1 : #2 \absspace.\absspace #3}
+\newcommand{\lcforall}[3]{(#1 : #2) \tyarr #3}
\newcommand{\lcexists}[3]{\exists #1 : #2 \absspace.\absspace #3}
The STLC can be made more expressive in various ways. Henk Barendregt
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.
+ quantify over types in our type signatures: $(\abs{A : \lctype}{\abs{x :
+ A}{x}}) : \lcforallz{A}{A \tyarr A}$. The first and most famous instance
+ of this idea has been System F. This gives us a form of polymorphism and has
+ been wildly successful, also thanks to a well known inference algorithm for a
+ restricted version of System F known as Hindley-Milner. Languages like
+ Haskell and SML are based on this discipline.
\item[Types depending on types (towards $\lambda{\underline{\omega}}$)] In other
words, we have type operators: $(\abs{A : \lctype}{\abs{R : \lctype}{(A \to R) \to R}}) : \lctype \to \lctype \to \lctype$.
\item[Types depending on terms (towards $\lambda{P}$)] Also known as `dependent
Intuitionistic Type Theory, has all of the above additions, and thus would sit
where $\lambda{C}$ sits in the `$\lambda$-cube' above.
-\section{Intuitionistic Type Theory}
+\section{Intuitionistic Type Theory and dependent types}
\newcommand{\lcset}[1]{\mathsf{Type}_{#1}}
\newcommand{\lcsetz}{\mathsf{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 $\forall$ and $\exists$: if a
+This relation is expressed in the typing rules for $\tyarr$ and $\exists$: if a
function has type $\lcforall{x}{\tya}{\tyb}$, $\tyb$ can depend on $x$.
Examples will make this clearer once some base types are added in section
\ref{sec:base-types}.
-$\forall$ and $\exists$ are at the core of the machinery of ITT:
+$\tyarr$ and $\exists$ are at the core of the machinery of ITT:
\begin{description}
-\item[`forall' ($\forall$)] is a generalisation of $\tyarr$ in the STLC and
- expresses universal quantification in our logic. In the literature this is
- also known as `dependent product' and shown as $\Pi$, following the
- interpretation of functions as infinitary products. We will just call it
- `dependent function', reserving `product' for $\exists$.
+\item[`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
+ literature this is also known as `dependent product' and shown as $\Pi$,
+ following the interpretation of functions as infinitary products. We will just
+ call it `dependent function', reserving `product' for $\exists$.
\item[`exists' ($\exists$)] is a generalisation of $\wedge$ in the extended
STLC of section \ref{sec:curry-howard}, and thus we will call it `dependent
product'. Like $\wedge$, it is formed by providing a pair of things. In our
logic, it represents existential quantification.
- For added confusion, in the literature that calls $\forall$ $\Pi$, $\exists$
- is often named `dependent sum' and shown as $\Sigma$. This is following the
+ For added confusion, in the literature that calls forall $\Pi$, $\exists$ is
+ often named `dependent sum' and shown as $\Sigma$. This is following the
interpretation of $\exists$ as a generalised, infinitary $\vee$, where the
first element of the pair is the `tag' that decides which type the second
element will have.
great burden if one wants to use the theory directly. Complete inference is
undecidable (which is hardly surprising considering the role that types play)
but partial inference (also called `bidirectional type checking' in this
-context) in the style of \citep{Pierce2000} will have to be deployed in a
-practical system. When showing examples obvious types will be omitted when this
-can be done without loss of clarity.
+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}}$.
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
\newcommand{\lcw}[3]{\mathsf{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}\appspace#1/#2\appspace.\appspace#3\appspace\lcsyn{then}\appspace#4\appspace\lcsyn{else}\appspace#5}
-\newcommand{\lcrec}[4]{\lcsyn{rec}\appspace#1/#2\appspace.\appspace#3\appspace\lcsyn{with}\appspace#4}
-\newcommand{\lcrecz}[2]{\lcsyn{rec}\appspace#1\appspace\lcsyn{with}\appspace#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$}
\begin{center}
\axname{syntax}
\begin{eqnarray*}
- \termsyn & ::= & ... \\
+ \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}
\DisplayProof
&
\AxiomC{}
- \RightLabel{$\lcbool I_{1,2}$}
\UnaryInfC{$\Gamma \vdash \lctrue : \lcbool$}
\noLine
\UnaryInfC{$\Gamma \vdash \lcfalse : \lcbool$}
\subsection{Some examples}
-Now we can finally provide some meaningful examples. I will use some
-abbreviations and convenient syntax:
+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 : \tya\}}{\dotsb}$ to define an abstraction that I will not
- explicitly apply since the $x$ can be inferred easily.
- \item $\abs{x\appspace y\appspace z : \tya}{\dotsb}$ to define multiple abstractions at the same
+ \item $\abs{x\appsp y\appsp z : \tya}{\dotsb}$ to define multiple abstractions at the same
time
- \item I will omit the explicit typing when forming $\exists$ or $\mathsf{W}$,
- and when eliminating $\lcbool$, since the types are almost always clear and
- writing them each time is extremely cumbersome.
\end{itemize}
\subsubsection{Sum types}
We would like to recover our sum type, or disjunction, $\vee$. This is easily
done with $\exists$:
-\begin{eqnarray*}
- \_\vee\_ & = & \abs{\tya\appspace\tyb : \lcsetz}{\lcexists{x}{\lcbool}{\lcite{x}{\tya}{\tyb}}} \\
- \lcinl & = & \abs{\{\tya\appspace\tyb : \lcsetz\}}{\abs{x : \tya \vee \tyb}{(\lctrue, x)}} \\
- \lcinr & = & \abs{\{\tya\appspace\tyb : \lcsetz\}}{\abs{x : \tya \vee \tyb}{(\lcfalse, x)}} \\
- \mathsf{case} & = & \abs{\{\tya\appspace\tyb\appspace\tyc : \lcsetz\}}{\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{eqnarray*}
+\[
+\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}{ \\
+ & & \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
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 and similarly lists}
+\subsubsection{Naturals}
Now it's time to showcase the power of $\mathsf{W}$ types.
-
\begin{eqnarray*}
- \mathsf{Nat} & = & \lcw{b}{\lcbool}{\abs{b}{\lcite{b}{\top}{\bot}}} \\
+ \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\appspace y}{\lcrecz{x}{\abs{b}{\lcite{b}{\abs{\_\appspace f}{\app{\mathsf{suc}}{(\app{f}{\lcunit})}}}{\abs{\_\appspace\_}{y}}}}}
+ \mathsf{plus} & = & \abs{x\appsp y}{\lcrecz{x}{(\abs{b}{\lcite{b}{\abs{\_\appsp f}{\app{\mathsf{suc}}{(\app{f}{\lcunit})}}}{\abs{\_\appsp\_}{y}}})}}
\end{eqnarray*}
+Here we encode natural numbers through $\mathsf{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.
+
+We postpone more complex examples after the introduction of inductive families
+and pattern matching, since $\mathsf{W}$ types get unwieldy very quickly.
+
+\subsubsection{Propositional Equality}
+
+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}
+
+\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. 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.
+
+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:
+ \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}
+
+While our core type theory equipped with $\mathsf{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
+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}.
+
+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 present in Agda (if possible, since some features are not present in Agda
+yet).
+
+\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{\mathsf{List}}{#1}}
+\newcommand{\lcnat}{\app{\mathsf{Nat}}}
+\newcommand{\lcvec}[2]{\app{\app{\mathsf{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
+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}
+\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
+$\_::\_ : \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
+\[
+\begin{array}{l}
+\lcdata{\lcnat} : \lcsetz \lcwhere \\
+ \begin{array}{l@{\ }l}
+ \lcind \mathsf{zero} &: \lcnat \\
+ \lcind \mathsf{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 \\
+ \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})}
+ \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:
+\[
+\begin{array}{l}
+\mathsf{head} : \{A\ n\} \tyarr \lcvec{A}{(\app{\mathsf{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
+number.
+
+\newcommand{\lcfin}[1]{\app{\mathsf{Fin}}{#1}}
+
+If we wish to index a $\mathsf{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 \\
+ \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})}
+ \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}$:
+\[
+\begin{array}{l}
+\_\mathsf{!!}\_ : \{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.
+
+
+\subsection{Pattern matching}
+
+\subsection{Guarded recursion}
+
+\subsection{Corecursion}
+
+\subsection{Quotient types}
+
+
+\section{Why dependent types?}
+
+\section{Many equalities}
+
+\subsection{Revision}
+
+\subsection{Extensional equality and its problems}
+
+\subsection{Observational equality}
+
+\section{What to do}
+
\bibliographystyle{authordate1}
\bibliography{background}
+\appendix
+\section{Agda code}
+\label{app:agda-code}
+
\end{document}
projects / bitonic-mengthesis.git / commitdiff