From c75821e4f9ee774c188194993dbe418f16e755b0 Mon Sep 17 00:00:00 2001 From: Francesco Mazzoli Date: Sat, 12 Jan 2013 17:48:12 +0000 Subject: [PATCH] more stuff --- docs/background.bib | 301 +++++++++++++++++++----------------- docs/background.tex | 368 ++++++++++++++++++++++++++++++++++++-------- 2 files changed, 461 insertions(+), 208 deletions(-) diff --git a/docs/background.bib b/docs/background.bib index 328981b..41c3ec5 100644 --- a/docs/background.bib +++ b/docs/background.bib @@ -13,15 +13,37 @@ 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}, @@ -37,6 +59,62 @@ title = {{Observational equality, now!}}, 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}, @@ -45,14 +123,37 @@ title = {{Introduction to generalized type systems}}, 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}, @@ -67,27 +168,13 @@ title = {{The gentle art of levitation}}, 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}, @@ -96,6 +183,15 @@ title = {{The calculus of constructions}}, 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}, @@ -107,34 +203,16 @@ url = {http://www.ncbi.nlm.nih.gov/pmc/articles/pmc1076489/}, 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}, @@ -145,83 +223,20 @@ title = {{Towards a practical programming language based on dependent type theor 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} } diff --git a/docs/background.tex b/docs/background.tex index ac451f8..5d30645 100644 --- a/docs/background.tex +++ b/docs/background.tex @@ -6,6 +6,11 @@ \usepackage{graphicx} \usepackage{subcaption} +% Unicode +\usepackage{ucs} +\usepackage[utf8x]{inputenc} +% \usepackage{autofe} + %% ----------------------------------------------------------------------------- %% Fonts %% \usepackage[osf]{libertine} @@ -25,7 +30,8 @@ %% ----------------------------------------------------------------------------- %% Symbols -\usepackage{amssymb,amsmath} +\usepackage[fleqn]{amsmath} +\usepackage{amssymb} \usepackage{wasysym} \usepackage{turnstile} \usepackage{centernot} @@ -36,6 +42,12 @@ \usepackage{umoline} \usepackage[export]{adjustbox} \usepackage{multicol} +\usepackage{listings} +\lstset{ + basicstyle=\footnotesize\ttfamily, + extendedchars=\true, + inputencoding=utf8x +} %% ----------------------------------------------------------------------------- %% Bibtex @@ -117,8 +129,8 @@ in the traditional sense, but just functions. The syntax of $\lambda$-terms consists of just three things: variables, abstractions, and applications: -\newcommand{\appspace}{\hspace{0.07cm}} -\newcommand{\app}[2]{#1\appspace#2} +\newcommand{\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} @@ -134,10 +146,12 @@ abstractions, and applications: \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} @@ -171,9 +185,9 @@ $\bred$ relation also includes reduction of subterms, for example if $\termt 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 @@ -263,22 +277,22 @@ give types to the non-normalising term shown before: \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. @@ -308,11 +322,11 @@ that is done by introducing a type inhabited by no terms. If evidence of such a type is presented, then we can derive any type, which expresses absurdity. Conversely, $\top$ is the type with just one trivial element, $\lcunit$. -\newcommand{\lcinl}{\mathsf{inl}\appspace} -\newcommand{\lcinr}{\mathsf{inr}\appspace} -\newcommand{\lccase}[3]{\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}} @@ -320,18 +334,21 @@ Conversely, $\top$ is the type with just one trivial element, $\lcunit$. \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} @@ -412,10 +429,10 @@ unsound\footnote{Obviously such a term can be present under a $\lambda$.}. \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 @@ -440,11 +457,12 @@ 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. + 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 @@ -456,7 +474,7 @@ which I haven't mentioned yet). The system we are going to focus on, Intuitionistic Type Theory, has all of the above additions, and thus would sit where $\lambda{C}$ sits in the `$\lambda$-cube' above. -\section{Intuitionistic Type Theory} +\section{Intuitionistic Type Theory and dependent types} \newcommand{\lcset}[1]{\mathsf{Type}_{#1}} \newcommand{\lcsetz}{\mathsf{Type}} @@ -576,27 +594,28 @@ $\lcset{n}$, with $n > 0$). This change is reflected in the typing rules. While in the STLC values and types are kept well separated (values never go `right of the colon'), in ITT types can freely depend on values. -This relation is expressed in the typing rules for $\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. @@ -636,9 +655,10 @@ specify every type when forming abstractions, products, etc. This can be a great burden if one wants to use the theory directly. Complete inference is undecidable (which is hardly surprising considering the role that types play) but partial inference (also called `bidirectional type checking' in this -context) in the style of \citep{Pierce2000} will have to be deployed in a -practical system. When showing examples obvious types will be omitted 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 @@ -660,9 +680,9 @@ logic. \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$} @@ -675,7 +695,7 @@ very general tree-like structure useful to represent inductively defined types. \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} @@ -697,7 +717,6 @@ very general tree-like structure useful to represent inductively defined types. \DisplayProof & \AxiomC{} - \RightLabel{$\lcbool I_{1,2}$} \UnaryInfC{$\Gamma \vdash \lctrue : \lcbool$} \noLine \UnaryInfC{$\Gamma \vdash \lcfalse : \lcbool$} @@ -767,30 +786,27 @@ $\tyc[\termt]$ holds. \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 @@ -798,18 +814,240 @@ 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 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} -- 2.30.2