From: Francesco Mazzoli Date: Wed, 22 May 2013 11:26:59 +0000 (+0100) Subject: thesis stub X-Git-Url: https://git.enpas.org/?p=bitonic-mengthesis.git;a=commitdiff_plain;h=0f7b3d5caf45b74d21a2a0042aa73a4112f805df thesis stub --- diff --git a/InterimReport.agda b/InterimReport.agda index c433d59..839060f 100644 --- a/InterimReport.agda +++ b/InterimReport.agda @@ -147,4 +147,4 @@ module Ext where map-#==#-map' : forall {A B C} (f : B -> C) (g : A -> B) -> map (f # g) == (map f # map g) - map-#==#-map' f g = ext (map-#==#-map f g) \ No newline at end of file + map-#==#-map' f g = ext (map-#==#-map f g) diff --git a/InterimReport.tex b/InterimReport.tex index 752288c..1c89260 100644 --- a/InterimReport.tex +++ b/InterimReport.tex @@ -36,6 +36,7 @@ \usepackage{turnstile} \usepackage{centernot} \usepackage{stmaryrd} +\usepackage{bm} %% ----------------------------------------------------------------------------- %% Utils @@ -170,7 +171,7 @@ In the languages presented I will also use different fonts for different things: Moreover, I will from time to time give examples in the Haskell programming language as defined in \citep{Haskell2010}, which I will typeset in -\texttt{typewriter} font. I assume that the reader is already familiar with +\texttt{teletype} font. I assume that the reader is already familiar with Haskell, plenty of good introductions are available \citep{LYAH,ProgInHask}. \subsection{Untyped $\lambda$-calculus} @@ -224,8 +225,21 @@ complete. As a corollary, we must be able to devise a term that reduces forever \app{(\abs{x}{\app{x}{x}})}{(\abs{x}{\app{x}{x}})} \bred \app{(\abs{x}{\app{x}{x}})}{(\abs{x}{\app{x}{x}})} \bred \dotsb \] Terms that can be reduced only a finite number of times (the non-looping ones) -are said to be \emph{normalising}, and the `final' term (where no reductions are -possible on the term or on its subterms) is called \emph{normal form}. +are said to be \emph{strongly normalising}, and the `final' term (where no +reductions are possible on the term or on its subterms) is called \emph{normal + form}. + +From now on I will omit the `strongly' in `strongly normalising', however weaker +notions of normalisation have been described. More generally, it is often +convenient not to reduce subterms indiscriminately, and have a more principled +approach to evaluation, or `evaluation strategy'. Common evaluation strategies +include `call by value' (or `strict'), where arguments of abstractions are +reduced before being applied to the abstraction; and conversely `call by name' +(or `lazy'), where we reduce only when we need to do so to proceed - in other +words when we have an application where the function is still not a $\lambda$. +In both these reduction strategies we never reduce under an abstraction, and a +different notion of normalisation (`weak head normal form') if often used, where +every abstraction is a weak head normal form. \subsection{The simply typed $\lambda$-calculus} \label{sec:stlc} @@ -245,21 +259,27 @@ The syntax for types is as follows: \begin{center} \axname{syntax} - $$\tysyn ::= x \separ \tysyn \tyarr \tysyn$$ +$$ +\begin{array}{rcl} + \tysyn & ::= & \alpha \separ \tysyn \tyarr \tysyn \\ + \alpha & \in & \text{A set of base types provided by the language} +\end{array} +$$ \end{center} -I will use $\tya,\tyb,\dots$ to indicate a generic type. +I will use $\tya,\tyb,\dots$ to indicate a generic type, carrying the convention +from set theory of denoting member of sets with lowercase letters and sets +themselves with capitals. A context $\Gamma$ is a map from variables to types. I will use the notation $\Gamma; x : \tya$ to augment it and to `extract' pairs from it. Predictably, $\tya \tyarr \tyb$ is the type of a function from $\tya$ to -$\tyb$. We need to be able to decorate our abstractions with -types\footnote{Actually, we don't need to: computers can infer the right type - easily, but that is another story.}: +$\tyb$. We extend the syntax and allow to decorate our abstractions with +types: \begin{center} \axname{syntax} - $$\termsyn ::= x \separ (\abs{x : \tysyn}{\termsyn}) \separ (\app{\termsyn}{\termsyn})$$ + $$\termsyn ::= x \separ (\abs{x{:}\tysyn}{\termsyn}) \separ (\app{\termsyn}{\termsyn})$$ \end{center} Now we are ready to give the typing judgements: @@ -273,7 +293,7 @@ Now we are ready to give the typing judgements: \DisplayProof & \AxiomC{$\Gamma; x : \tya \vdash \termt : \tyb$} - \UnaryInfC{$\Gamma \vdash \abs{x : \tya}{\termt} : \tya \tyarr \tyb$} + \UnaryInfC{$\Gamma \vdash \abs{x{:}\tya}{\termt} : \tya \tyarr \tyb$} \DisplayProof \end{tabular} @@ -344,10 +364,11 @@ That is, function composition. We might want extend our bare lambda calculus with a couple of terms former to make our natural deduction more pleasant to use. For example, tagged unions (\texttt{Either} in Haskell) are disjunctions, and tuples (or products) are conjunctions. We also want to be able to express -falsity ($\bot$): that can done by introducing a type inhabited by no terms. If -evidence of such a type is presented, then we can derive any type, which -expresses absurdity. Conversely, truth ($\top$) is the type with just one -trivial element ($\lcunit$). +falsity ($\bot$): that can done by introducing a type inhabited by no closed +terms. If evidence of such a type is presented (necessarily under an +abstraction), 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} @@ -364,7 +385,7 @@ trivial element ($\lcunit$). \newcommand{\lcabsurd}{\lcfun{absurd}\appsp} \newcommand{\lcabsurdd}[1]{\lcfun{absurd}_{#1}\appsp} - +% TODO make parens bold with \bm \begin{center} \axname{syntax} $$ @@ -507,10 +528,11 @@ above additions, and thus would sit where $\lambda{C}$ sits in the Logic frameworks and programming languages based on type theory have a long history. Per Martin-L\"{o}f described the first version of his theory in 1971, -but then revised it since the original version was too impredicative and thus -inconsistent\footnote{In the early version $\lcsetz : \lcsetz$, see section - \ref{sec:core-tt} for an explanation on why this causes problems.}. For this -reason he gave a revised and consistent definition later \citep{Martin-Lof1984}. +but then revised it since the original version was inconsistent due to its +impredicativity\footnote{In the early version there was only one universe + $\lcsetz$ and $\lcsetz : \lcsetz$, see section \ref{sec:core-tt} for an + explanation on why this causes problems.}. For this reason he gave a revised +and consistent definition later \citep{Martin-Lof1984}. A related development is the polymorphic $\lambda$-calculus, and specifically the previously mentioned System F, which was developed independently by Girard @@ -631,11 +653,12 @@ logic. $\tyarr$ and $\times$ are at the core of the machinery of ITT: \begin{description} \item[`forall' ($\tyarr$)] is a generalisation of $\tyarr$ in the STLC and - expresses universal quantification in our logic. It is often written with a - syntax closer to logic, e.g. $\forall x : \tya. \tyb$. In the - literature this is also known as `dependent product' and shown as $\Pi$, - following the interpretation of functions as infinitary products. I will just - call it `dependent function', reserving `product' for $\exists$. + expresses universal quantification in our logic, where $A \tyarr B$ can be + expressed as $(- : A) \tyarr B$. It is often written with a syntax closer to + logic, e.g. $\forall x : \tya. \tyb$. In the literature this is also known as + `dependent product' and shown as $\Pi$, following the interpretation of + functions as infinitary products. I will just call it `dependent function', + reserving `product' for $\exists$. \item[`exists' ($\times$)] is a generalisation of $\wedge$ in the extended STLC of section \ref{sec:curry-howard}, and thus I will call it `dependent @@ -643,8 +666,8 @@ logic. $\tyarr$ and $\times$ are at the core of the machinery of ITT: logic, it represents existential quantification. Similarly to $\tyarr$, it is often written as $\exists x : \tya. \tyb$. - For added confusion, in the literature that calls $\tyarr$ $\Pi$, $\times$ is - often named `dependent sum' and shown as $\Sigma$. This is following the + For added confusion, in the literature that uses $\Pi$ for $\tyarr$, $\times$ + is often named `dependent sum' and shown as $\Sigma$. This is following the interpretation of $\exists$ as a generalised, infinitary $\vee$, where the first element of the pair is the `tag' that determines which type the second element will have. @@ -655,12 +678,12 @@ 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 related 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 +this: when we want to compare two terms 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 + terms we do it up to $\alpha$-renaming. That is, we do not consider renaming + of bound 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 : @@ -669,13 +692,13 @@ and will be analysed better in section \ref{sec:equality}. The theory presented is \emph{stratified}. We have a hierarchy of types $\lcset{0} : \lcset{1} : \lcset{2} : \dots$, so that there is no `type of all -types', and our theory is predicative. Type-formers like $\tyarr$ and $\times$ +types', and our theory is predicative. Constructors like $\tyarr$ and $\times$ take the least upper bound $\sqcup$ of the contained types. The layers of the hierarchy are called `universes'. Theories where $\lcsetz : \lcsetz$ are inconsistent due to Girard's paradox \citep{Hurkens1995}, and thus lose their -well-behavedness. Some impredicativity sometimes has its place, either because -the theory retain good properties (normalization, consistency, etc.) anyway, -like in System F and CoC; or because we are at a stage at which we do not care. +well-behavedness. 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. \subsection{Base Types} \label{sec:base-types} diff --git a/Makefile b/Makefile index 1514e88..ad3f550 100644 --- a/Makefile +++ b/Makefile @@ -1,8 +1,22 @@ -SOURCES = $(wildcard *.tex) -OBJECTS = $(patsubst %.tex, %.pdf, $(SOURCES)) +SOURCEST = $(wildcard *.tex) +OBJECTST = $(patsubst %.tex, %.pdf, $(SOURCEST)) +SOURCESA = $(wildcard *.lagda) +OBJECTSA = $(patsubst %.lagda, %.pdf, $(SOURCESA)) +OBJECTS = $(OBJECTST) $(OBJECTSA) all: $(OBJECTS) +thesis.pdf: thesis.tex thesis.bib agda.sty + pdflatex -halt-on-error $< -o $@ + bibtex thesis + pdflatex -halt-on-error $< -o $@ + pdflatex -halt-on-error $< -o $@ + +agda.sty: thesis.tex + +thesis.tex: thesis.lagda + agda --latex --latex-dir . -i . -i ~/src/agda-lib/src/ thesis.lagda + InterimReport.pdf: InterimReport.tex InterimReport.bib InterimReport.agda xelatex -halt-on-error $< -o $@ bibtex InterimReport @@ -15,6 +29,8 @@ idris-proposal.pdf: idris-proposal.tex clean: cleanup rm -f $(OBJECTS) + rm -f thesis.tex agda.sty cleanup: - rm -f *.log *.aux *.nav *.snm *.toc *.vrb *.out *.bbl *.blg + rm -f *.log *.aux *.nav *.snm *.toc *.vrb *.out *.bbl *.blg *.agdai + diff --git a/thesis.bib b/thesis.bib new file mode 100644 index 0000000..9519f9f --- /dev/null +++ b/thesis.bib @@ -0,0 +1,314 @@ +@inbook{Thompson1991, + author = {Thompson, Simon}, + title = {Type Theory and Functional Programming}, + publisher = {Addison-Wesley}, + year = {1991} +} + +@inbook{Pierce2002, + author = {Pierce, Benjamin C.}, + title = {Types and Programming Languages}, + publisher = {The MIT Press}, + year = {2002} +} + +@online{Coq, + author = {{The Coq Team}}, + title = {The Coq Proof Assistant}, + url = {\url{coq.inria.fr}}, + howpublished = {\url{http://coq.inria.fr}}, + year = 2013 +} + +@online{GHC, + author = {{The GHC Team}}, + title = {The Glorious Glasgow Haskell Compilation System User's Guide, Version 7.6.1}, + url = {http://www.haskell.org/ghc/docs/7.6.1/html/users_guide/}, + howpublished = {\url{http://www.haskell.org/ghc/docs/latest/html/users_guide/}}, + year = 2012 +} + +@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 +} + +@online{Haskell2010, + author = {Simon Marlow}, + title = {Haskell 2010, Language Report}, + url = {http://www.haskell.org/onlinereport/haskell2010/}, + howpublished = {\url{http://www.haskell.org/onlinereport/haskell2010/}}, + year = 2010 +} + +@online{LYAH, + author = {Miran Lipova\v{c}a}, + title = {Learn You a Haskell for Great Good!}, + url = {http://learnyouahaskell.com/}, + howpublished = {\url{http://learnyouahaskell.com/}}, + year = 2009 +} + +@inbook{ProgInHask, + author = {Graham Hutton}, + title = {Programming in Haskell}, + year = 2007, + publisher = {Cambridge University Press} +} + +@inbook{NuPRL, + author = {Robert L. Constable and the PRL Group}, + title = {Implementing Mathematics with The NuPRL Proof Development System}, + year = 1986, + publisher = Prentice-Hall +} + + +@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}, +author = {Altenkirch, Thorsten and McBride, Conor and Swierstra, Wouter}, +doi = {10.1145/1292597.1292608}, +file = {:home/bitonic/docs/papers/OTT2.pdf:pdf}, +isbn = {9781595936776}, +journal = {Proceedings of the 2007 workshop on Programming languages meets program verification - PLPV '07}, +keywords = {case analysis relies on,datatypes are indexed in,equality,of any language where,ole in the programs,play a crucial internal,rˆ,solving,some way,type theory}, +pages = {57}, +publisher = {ACM Press}, +title = {{Observational equality, now!}}, +url = {http://portal.acm.org/citation.cfm?doid=1292597.1292608}, +year = {2007} +} +@article{Barendregt1991, +author = {Barendregt, Henk}, +file = {:home/bitonic/docs/papers/lambda-cube.pdf:pdf}, +journal = {Journal of functional programming}, +title = {{Introduction to generalized type systems}}, +url = {http://www.diku.dk/hjemmesider/ansatte/henglein/papers/barendregt1991.pdf}, +year = {1991} +} +@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{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}, +author = {Chapman, James and Dagand, Pierre-\'{E}variste and McBride, Conor and Morris, Peter}, +doi = {10.1145/1863543.1863547}, +file = {:home/bitonic/docs/papers/conor-levitation.pdf:pdf}, +isbn = {9781605587943}, +journal = {Proceedings of the 15th ACM SIGPLAN international conference on Functional programming - ICFP '10}, +pages = {3}, +publisher = {ACM Press}, +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{Coquand1986, +author = {Coquand, Thierry and Huet, Gerard}, +file = {:home/bitonic/docs/papers/coc.pdf:pdf}, +title = {{The calculus of constructions}}, +url = {http://hal.inria.fr/docs/00/07/60/24/PDF/RR-0530.pdf}, +year = {1986} +} +@article{Curry1934, +author = {Curry, Haskell B.}, +file = {:home/bitonic/docs/papers/curry-stlc.pdf:pdf}, +journal = {Proceedings of the National Academy of Sciences of the United States of America}, +number = {1930}, +pages = {584--590}, +title = {{Functionality in combinatory logic}}, +url = {http://www.ncbi.nlm.nih.gov/pmc/articles/pmc1076489/}, +volume = {511}, +year = {1934} +} +@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} +} +@article{Jacobs1997, +author = {Jacobs, Bart and Rutten, Jan}, +file = {:home/bitonic/docs/papers/coalgebra-coind.pdf:pdf}, +journal = {EATCS Bulletin}, +number = {1997}, +title = {{A tutorial on (co) algebras and (co) induction}}, +url = {http://synrc.com/publications/cat/Logic/CoinductionCoalgebrasTutorial.pdf}, +volume = {62}, +year = {1997} +} +@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}, +file = {:home/bitonic/docs/papers/ulf-thesis.pdf:pdf}, +isbn = {9789172919969}, +school = {Chalmers University of Technology and G\"{o}teborg University}, +title = {{Towards a practical programming language based on dependent type theory}}, +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{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} +} +@phdthesis{McBride1999, +author = {McBride, Conor}, +file = {:home/bitonic/docs/papers/conorthesis.pdf:pdf}, +school = {University of Edinburgh}, +title = {{Dependently typed functional programs and their proofs}}, +url = {http://lac-repo-live7.is.ed.ac.uk/handle/1842/374}, +year = {1999} +} diff --git a/thesis.lagda b/thesis.lagda new file mode 100644 index 0000000..985c611 --- /dev/null +++ b/thesis.lagda @@ -0,0 +1,153 @@ +\documentclass[report]{article} + +%% Narrow margins +\usepackage{fullpage} + +%% Bibtex +\usepackage{natbib} + +%% Links +\usepackage{hyperref} + +%% ----------------------------------------------------------------------------- +%% Commands for Agda +\usepackage[english]{babel} +\usepackage[conor]{agda} +\renewcommand{\AgdaKeywordFontStyle}[1]{\ensuremath{\mathrm{\underline{#1}}}} +\renewcommand{\AgdaFunction}[1]{\textbf{\textcolor{AgdaFunction}{#1}}} +\definecolor{AgdaBound} {HTML}{000000} + +\DeclareUnicodeCharacter{9665}{\ensuremath{\lhd}} + +%% ----------------------------------------------------------------------------- +%% Commands + +\newcommand{\mysyn}{\AgdaKeyword} +\newcommand{\mytyc}{\AgdaDatatype} +\newcommand{\myind}{\AgdaInductiveConstructor} +\newcommand{\myfld}{\AgdaField} +\newcommand{\myfun}{\AgdaFunction} +\newcommand{\myb}{\AgdaBound} +\newcommand{\myfield}{\AgdaField} + +%% ----------------------------------------------------------------------------- + +\title{\textsc{Kant}: Implementing Observational Equality} +% TODO remove double @ if we get rid of lhs2TeX +\author{Francesco Mazzoli \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{}}} +\date{June 2013} + +\begin{document} + +%if False +\begin{code} +module thesis where +open import Level +\end{code} +%endif + +\maketitle + +\begin{abstract} + The marriage between programming and logic has been a very fertile one. In + particular, since the simply typed lambda calculus (STLC), a number of type + systems have been devised with increasing expressive power. + + Section \ref{sec:types} 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:equality} will explain why equality has always been a tricky + business in these theories, and talk about the various attempts that have been + made to make the situation better. One interesting development has recently + emerged: Observational Type theory. + + Section \ref{sec:practical} will describe common extensions found in the + systems currently in use. Finally, section \ref{sec:kant} will describe a + system developed by the author that implements a core calculus based on the + principles described. +\end{abstract} + +\tableofcontents + +\section{Simple and not-so-simple types} +\label{sec:types} + +\section{Intuitionistic Type Theory and dependent types} +\label{sec:itt} + +\section{The struggle for equality} +\label{sec:equality} + +\section{A more useful language} +\label{sec:practical} + +\section{Kant} +\label{sec:kant} + +\appendix + +\section{Notation and syntax} + +In the languages presented I will also use different fonts and colors for +different things: + +\begin{center} + \begin{tabular}{c | l} + $\mytyc{Sans}$ & Type constructors. \\ + $\myind{sans}$ & Data constructors. \\ + $\myfld{sans}$ & Field accessors (e.g. \myfld{fst} and \myfld{snd} for products). \\ + $\mysyn{roman}$ & Syntax of the language. \\ + $\myfun{roman}$ & Defined values. \\ + $\myb{math}$ & Bound variables. + \end{tabular} +\end{center} + +\section{Agda rendition of a core ITT} +\label{app:agda-code} + +\begin{code} +module ITT where + data Empty : Set where + + absurd : ∀ {a} {A : Set a} → Empty → A + absurd () + + record Unit : Set where + constructor tt + + record _×_ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where + constructor _,_ + field + fst : A + snd : B fst + open _×_ public + + data Bool : Set where + true false : Bool + + if_/_then_else_ : ∀ {a} (x : Bool) → (P : Bool → Set a) → P true → P false → P x + if true / _ then x else _ = x + if false / _ then _ else x = x + + data W {s p} (S : Set s) (P : S → Set p) : Set (s ⊔ p) where + _◁_ : (s : S) → (P s → W S P) → W S P + + rec : ∀ {a b} {S : Set a} {P : S → Set b} + (C : W S P → Set) → -- some conclusion we hope holds + ((s : S) → -- given a shape... + (f : P s → W S P) → -- ...and a bunch of kids... + ((p : P s) → C (f p)) → -- ...and C for each kid in the bunch... + C (_◁_ s f)) → -- ...does C hold for the node? + (x : W S P) → -- If so, ... + C x -- ...C always holds. + rec C c (s ◁ f) = c s f (λ p → rec C c (f p)) +\end{code} + +\nocite{*} +\bibliographystyle{authordate1} +\bibliography{thesis} + +\end{document} diff --git a/thesis.ptb b/thesis.ptb new file mode 100644 index 0000000..77d5935 --- /dev/null +++ b/thesis.ptb @@ -0,0 +1,189 @@ +\def\PTtemp{..}\empty +\def\PTtemp{..}\empty +\def\PTtemp{2}\empty +\def\PTtemp{2.}\empty +\def\PTtemp{2}\empty +\def\PTtemp{2.}\empty +\def\PTtemp{2}\empty +\def\PTtemp{2.}\empty +\def\PTtemp{2}\empty +\def\PTtemp{2.}\empty +\def\PTtemp{4}\empty +\def\PTtemp{4.}\empty +\def\PTtemp{2}\empty +\def\PTtemp{2.}\empty +\def\PTtemp{4}\empty +\def\PTtemp{4.}\empty +\def\PTtemp{4}\empty +\def\PTtemp{4.}\empty +\def\PTtemp{6}\empty +\def\PTtemp{6.}\empty +\def\PTtemp{6}\empty +\def\PTtemp{6.}\empty +\def\PTtemp{2}\empty +\def\PTtemp{2.}\empty +\def\PTtemp{2}\empty +\def\PTtemp{2.}\empty +\def\PTtemp{4}\empty +\def\PTtemp{4.}\empty +\def\PTtemp{2}\empty +\def\PTtemp{2.}\empty +\def\PTtemp{2}\empty +\def\PTtemp{2.}\empty +\def\PTtemp{2}\empty +\def\PTtemp{2.}\empty +\def\PTtemp{2}\empty +\def\PTtemp{2.}\empty +\def\PTtemp{4}\empty +\def\PTtemp{4.}\empty +\def\PTtemp{2}\empty +\def\PTtemp{2.}\empty +\def\PTtemp{4}\empty +\def\PTtemp{29}\empty +\def\PTtemp{29.}\empty +\def\PTtemp{4}\empty +\def\PTtemp{29}\empty +\def\PTtemp{29.}\empty +\def\PTtemp{5}\empty +\def\PTtemp{29}\empty +\def\PTtemp{29.}\empty +\def\PTtemp{5}\empty +\def\PTtemp{5.}\empty +\def\PTtemp{5}\empty +\def\PTtemp{29}\empty +\def\PTtemp{29.}\empty +\def\PTtemp{4}\empty +\def\PTtemp{29}\empty +\def\PTtemp{29.}\empty +\def\PTtemp{4}\empty +\def\PTtemp{29}\empty +\def\PTtemp{29.}\empty +\def\PTtemp{2}\empty +\def\PTtemp{2.}\empty +\def\PTtemp{..}\empty +\def\PTtemp{..}\empty +\def\PTtemp{..}\empty +\def\PTtemp{2}\empty +\def\PTtemp{2.}\empty +\def\PTtemp{2}\empty +\def\PTtemp{2.}\empty +\def\PTtemp{2}\empty +\def\PTtemp{2.}\empty +\def\PTtemp{2}\empty +\def\PTtemp{2.}\empty +\def\PTtemp{4}\empty +\def\PTtemp{4.}\empty +\def\PTtemp{2}\empty +\def\PTtemp{2.}\empty +\def\PTtemp{4}\empty +\def\PTtemp{4.}\empty +\def\PTtemp{4}\empty +\def\PTtemp{4.}\empty +\def\PTtemp{6}\empty +\def\PTtemp{6.}\empty +\def\PTtemp{6}\empty +\def\PTtemp{6.}\empty +\def\PTtemp{2}\empty +\def\PTtemp{2.}\empty +\def\PTtemp{2}\empty +\def\PTtemp{2.}\empty +\def\PTtemp{4}\empty +\def\PTtemp{4.}\empty +\def\PTtemp{2}\empty +\def\PTtemp{2.}\empty +\def\PTtemp{2}\empty +\def\PTtemp{2.}\empty +\def\PTtemp{2}\empty +\def\PTtemp{2.}\empty +\def\PTtemp{2}\empty +\def\PTtemp{2.}\empty +\def\PTtemp{4}\empty +\def\PTtemp{4.}\empty +\def\PTtemp{2}\empty +\def\PTtemp{2.}\empty +\def\PTtemp{4}\empty +\def\PTtemp{29}\empty +\def\PTtemp{29.}\empty +\def\PTtemp{4}\empty +\def\PTtemp{29}\empty +\def\PTtemp{29.}\empty +\def\PTtemp{5}\empty +\def\PTtemp{29}\empty +\def\PTtemp{29.}\empty +\def\PTtemp{5}\empty +\def\PTtemp{5.}\empty +\def\PTtemp{5}\empty +\def\PTtemp{29}\empty +\def\PTtemp{29.}\empty +\def\PTtemp{4}\empty +\def\PTtemp{29}\empty +\def\PTtemp{29.}\empty +\def\PTtemp{4}\empty +\def\PTtemp{29}\empty +\def\PTtemp{29.}\empty +\def\PTtemp{2}\empty +\def\PTtemp{2.}\empty +\def\PTtemp{..}\empty +\def\PTtemp{..}\empty +\def\PTtemp{..}\empty +\def\PTtemp{2}\empty +\def\PTtemp{2.}\empty +\def\PTtemp{2}\empty +\def\PTtemp{2.}\empty +\def\PTtemp{2}\empty +\def\PTtemp{2.}\empty +\def\PTtemp{2}\empty +\def\PTtemp{2.}\empty +\def\PTtemp{4}\empty +\def\PTtemp{4.}\empty +\def\PTtemp{2}\empty +\def\PTtemp{2.}\empty +\def\PTtemp{4}\empty +\def\PTtemp{4.}\empty +\def\PTtemp{4}\empty +\def\PTtemp{4.}\empty +\def\PTtemp{6}\empty +\def\PTtemp{6.}\empty +\def\PTtemp{6}\empty +\def\PTtemp{6.}\empty +\def\PTtemp{2}\empty +\def\PTtemp{2.}\empty +\def\PTtemp{2}\empty +\def\PTtemp{2.}\empty +\def\PTtemp{4}\empty +\def\PTtemp{4.}\empty +\def\PTtemp{2}\empty +\def\PTtemp{2.}\empty +\def\PTtemp{2}\empty +\def\PTtemp{2.}\empty +\def\PTtemp{2}\empty +\def\PTtemp{2.}\empty +\def\PTtemp{2}\empty +\def\PTtemp{2.}\empty +\def\PTtemp{4}\empty +\def\PTtemp{4.}\empty +\def\PTtemp{2}\empty +\def\PTtemp{2.}\empty +\def\PTtemp{4}\empty +\def\PTtemp{29}\empty +\def\PTtemp{29.}\empty +\def\PTtemp{4}\empty +\def\PTtemp{29}\empty +\def\PTtemp{29.}\empty +\def\PTtemp{5}\empty +\def\PTtemp{29}\empty +\def\PTtemp{29.}\empty +\def\PTtemp{5}\empty +\def\PTtemp{5.}\empty +\def\PTtemp{5}\empty +\def\PTtemp{29}\empty +\def\PTtemp{29.}\empty +\def\PTtemp{4}\empty +\def\PTtemp{29}\empty +\def\PTtemp{29.}\empty +\def\PTtemp{4}\empty +\def\PTtemp{29}\empty +\def\PTtemp{29.}\empty +\def\PTtemp{2}\empty +\def\PTtemp{2.}\empty +\def\PTtemp{..}\empty