}
+@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},
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},
url = {http://www.springerlink.com/index/h12lq70470983732.pdf},
year = {2009}
}
-@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{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{Yorgey2012,
+@article{Chapman2010,
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},
+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 = {{Giving Haskell a promotion}},
-url = {http://dl.acm.org/citation.cfm?doid=2103786.2103795},
-year = {2012}
+title = {{The gentle art of levitation}},
+url = {http://portal.acm.org/citation.cfm?doid=1863543.1863547},
+year = {2010}
}
-@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},
+@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,
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},
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},
url = {http://portal.acm.org/citation.cfm?doid=1411204.1411213},
year = {2008}
}
-@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}
-}
-@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{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{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{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{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{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{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},
url = {http://reference.kfupm.edu.sa/content/i/m/implicit\_syntax\_\_1183660.pdf},
year = {1992}
}
-@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{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},
url = {http://portal.acm.org/citation.cfm?doid=1190315.1190324},
year = {2007}
}
-@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{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{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{Vytiniotis2011,
author = {Vytiniotis, Dimitrios and Jones, Simon Peyton and Schrijvers, Tom and Sulzmann, Martin},
file = {:home/bitonic/docs/papers/outsidein.pdf:pdf},
volume = {21},
year = {2011}
}
-@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}
+@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}
}
particular, since the simply typed lambda calculus (STLC), a number of type
systems have been devised with increasing expressive power.
-Section \ref{sec:types} I will give a very brief overview of STLC, and then
+In section \ref{sec:types} I will give a very brief overview of STLC, and then
illustrate how it can be interpreted as a natural deduction system. Section
\ref{sec:itt} will introduce Inutitionistic Type Theory (ITT), which expands on
this concept, employing a more expressive logic. The exposition is quite dense
since there is a lot of material to cover; for a more complete treatment of the
material the reader can refer to \citep{Thompson1991, Pierce2002}. Section
-\ref{sec:practical} will describe additions common in practical programming
-languages based on ITT.
-
-Finally, I will explain why equality has been a tricky business in these
-theories, and talk about the various attempts have been made to make the
-situation better. One interesting development has recently emerged:
-Observational Type theory. I propose to explore the ways to turn these ideas
-into useful practices for programming and theorem proving.
+\ref{sec:practical} will describe additions common in programming languages
+based on ITT.
+
+Finally, in section \ref{sec:equality} I 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. I propose to explore the ways
+to turn these ideas into useful practices for programming and theorem proving.
\end{abstract}
\tableofcontents
language encodes computation with a minimal syntax and no `data' in the
traditional sense, but just functions.
-The syntax of $\lambda$-terms consists of just three things: variables,
-abstractions, and applications:
+The syntax of $\lambda$-terms consists of three things: variables, abstractions,
+and applications:
\begin{center}
\axname{syntax}
$$
\end{center}
-
-% I will omit parethesis in the usual manner. %TODO explain how
-
I will use $\termt,\termm,\termn,\dots$ to indicate a generic term, and $x,y$
-for variables. I will also assume that all variable names in a term are unique
-to avoid problems with name capturing. Intuitively, abstractions
-($\abs{x}{\termt}$) introduce functions with a named parameter ($x$), and
-applications ($\app{\termt}{\termm}$) apply a function ($\termt$) to an argument
-($\termm$).
+for variables. Parenthesis will be omitted in the usual way:
+$\app{\app{t}{m}}{n} = \app{(\app{t}{m})}{n}$. I will also assume that all
+variable names in a term are unique to avoid problems with name capturing.
+Intuitively, abstractions ($\abs{x}{\termt}$) introduce functions with a named
+parameter ($x$), and applications ($\app{\termt}{\termm}$) apply a function
+($\termt$) to an argument ($\termm$).
The `applying' is more formally explained with a reduction rule:
\vspace{0.5cm}
\begin{tabular}{c c c}
- \AxiomC{\phantom{1em}}
- \UnaryInfC{$\Gamma; x : \tya \vdash x : \tya$}
+ \AxiomC{$\Gamma; x : \tya \vdash x : \tya$}
\DisplayProof
&
\AxiomC{$\Gamma; x : \tya \vdash \termt : \tyb$}
and enjoys a number of properties. Two of them are expected in most type
systems \citep{Pierce2002}:
\begin{description}
-\item[Progress] A well-typed term is not stuck - either it is a \emph{canonical}
- value or it can take a step according to the evaluation rules. With canonical
- value we indicate terms formed by canonical constructors, in this case only
- $\lambda$\footnote{See section \ref{sec:fun-ext} for more information on
- canonicity.}.
+\item[Progress] A well-typed term is not stuck - it is either a variable, or its
+ constructor does not appear on the left of the $\bred$ relation (currently only
+ $\lambda$), or it can take a step according to the evaluation rules.
\item[Preservation] If a well-typed term takes a step of evaluation, then the
- resulting term is also well typed.
+ resulting term is also well-typed, and preserves the previous type.
\end{description}
-However, STLC buys us much more: every well-typed term
-is normalising. It is easy to see that we can't fill the blanks if we want to
-give types to the non-normalising term shown before:
+However, STLC buys us much more: every well-typed term is normalising. It is
+easy to see that we can't fill the blanks if we want to give types to the
+non-normalising term shown before:
\begin{equation*}
\app{(\abs{x : ?}{\app{x}{x}})}{(\abs{x : ?}{\app{x}{x}})}
\end{equation*}
$$
\lcfix{x : \tya}{\termt} \bred \termt[\lcfix{x : \tya}{\termt}]
$$
-Which will deprive us of normalisation, which is a particularly bad thing if we
+This will deprive us of normalisation, which is a particularly bad thing if we
want to use the STLC as described in the next section.
\subsection{The Curry-Howard correspondence}
\axdesc{typing}{\Gamma \vdash \termsyn : \tysyn}
\begin{prooftree}
\AxiomC{$\Gamma \vdash \termt : \tya$}
- \RightLabel{$\orint$}
\UnaryInfC{$\Gamma \vdash \lcinl \termt : \tya \vee \tyb$}
\noLine
\UnaryInfC{$\Gamma \vdash \lcinr \termt : \tyb \vee \tya$}
\AxiomC{$\Gamma \vdash \termt : \tya \vee \tyb$}
\AxiomC{$\Gamma \vdash \termm : \tya \tyarr \tyc$}
\AxiomC{$\Gamma \vdash \termn : \tyb \tyarr \tyc$}
- \RightLabel{$\orel$}
\TrinaryInfC{$\Gamma \vdash \lccase{\termt}{\termm}{\termn} : \tyc$}
\end{prooftree}
\begin{tabular}{c c}
\AxiomC{$\Gamma \vdash \termt : \tya$}
\AxiomC{$\Gamma \vdash \termm : \tyb$}
- \RightLabel{$\andint$}
\BinaryInfC{$\Gamma \vdash (\tya , \tyb) : \tya \wedge \tyb$}
\DisplayProof
&
\AxiomC{$\Gamma \vdash \termt : \tya \wedge \tyb$}
- \RightLabel{$\andel$}
\UnaryInfC{$\Gamma \vdash \lcfst \termt : \tya$}
\noLine
\UnaryInfC{$\Gamma \vdash \lcsnd \termt : \tyb$}
\begin{tabular}{c c}
\AxiomC{$\Gamma \vdash \termt : \bot$}
- \RightLabel{$\botel$}
\UnaryInfC{$\Gamma \vdash \lcabsurdd{\tya} \termt : \tya$}
\DisplayProof
&
\AxiomC{}
- \RightLabel{$\top I$}
\UnaryInfC{$\Gamma \vdash \lcunit : \top$}
\DisplayProof
\end{tabular}
it allows us to prove everything: $(\lcfix{x : \tya}{x}) : \tya$ clearly works
for any $A$! This is a crucial point: in general we wish to have systems that
do not let the user devise a term of type $\bot$, otherwise our logic will be
-unsound\footnote{Obviously such a term can be present under a $\lambda$.}.
+inconsistent\footnote{Obviously such a term can be present under a $\lambda$.}.
\subsection{Extending the STLC}
\newcommand{\lcforall}[3]{(#1 : #2) \tyarr #3}
\newcommand{\lcexists}[3]{(#1 : #2) \times #3}
-The STLC can be made more expressive in various ways. Henk Barendregt
-succinctly expressed geometrically how we can expand our type system:
+The STLC can be made more expressive in various ways. \cite{Barendregt1991}
+succinctly expressed geometrically how we can add expressively:
$$
\xymatrix@!0@=1.5cm{
normalising. \cite{Coquand1986} further extended this line of work with the
Calculus of Constructions (CoC).
-\subsection{A Core Type Theory}
+\subsection{A core type theory}
\label{sec:core-tt}
The calculus I present follows the exposition in \citep{Thompson1991}, and is
\vspace{0.5cm}
\begin{tabular}{c c c}
- \AxiomC{\phantom{1em}}
- \UnaryInfC{$\Gamma;x : \tya \vdash x : \tya$}
+ \AxiomC{$\Gamma;x : \tya \vdash x : \tya$}
\DisplayProof
&
\AxiomC{$\Gamma \vdash \termt : \tya$}
\AxiomC{$\Gamma \vdash \termt : \tya$}
\AxiomC{$\Gamma \vdash \termm : \tyb[\termt ]$}
\BinaryInfC{$\Gamma \vdash (\termt, \termm)_{x.\tyb} : \lcexists{x}{\tya}{\tyb}$}
- \noLine
- \UnaryInfC{$\phantom{1em}$}
\DisplayProof
&
\AxiomC{$\Gamma \vdash \termt: \lcexists{x}{\tya}{\tyb}$}
\vspace{0.5cm}
\begin{tabular}{c c}
- \AxiomC{$\phantom{1em}$}
+ \AxiomC{}
\UnaryInfC{$\Gamma \vdash \lcset{n} : \lcset{n + 1}$}
- \noLine
- \UnaryInfC{$\phantom{1em}$}
\DisplayProof
&
\AxiomC{$\Gamma \vdash \tya : \lcset{n}$}
When showing examples types will be omitted when this can be done without loss
of clarity, for example $\abs{x}{x}$ in place of $\abs{A : \lcsetz}{\abs{x :
- A}{x}}$. I will also use $\lcsetz$ as $\lcset{0}$.
+ A}{x}}$. I will also use $\lcsetz$ for $\lcset{0}$.
There are a lot of new factors at play here. The first thing to notice is that
the separation between types and terms is gone. All we have is terms, that
include both values (terms of type $\lcset{0}$) and types (terms of type
$\lcset{n}$, with $n > 0$). This change is reflected in the typing rules.
While in the STLC values and types are kept well separated (values never go
-`right of the colon'), in ITT types can freely depend on values.
+`right of the colon'), in ITT types can freely depend on values (they are
+`dependent types').
This relation is expressed in the typing rules for $\tyarr$ and $\times$: if a
function has type $\lcforall{x}{\tya}{\tyb}$, $\tyb$ can depend on $x$.
Examples will make this clearer once some base types are added in section
\ref{sec:base-types}.
-$\tyarr$ and $\times$ are at the core of the machinery of ITT:
+The Curry-Howard correspondence runs through ITT as it did with the STLC with
+the difference that ITT corresponds to an higher order propositional
+logic. $\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
of section \ref{sec:curry-howard}, and thus I will call it `dependent
product'. Like $\wedge$, it is formed by providing a pair of things. In our
logic, it represents existential quantification. Similarly to $\tyarr$, it is
- always written as $\exists x : \tya. \tyb$.
+ often written as $\exists x : \tya. \tyb$.
- For added confusion, in the literature that calls forall $\Pi$, $\exists$ is
+ For added confusion, in the literature that calls $\tyarr$ $\Pi$, $\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
create functions that accept and return types. For this reason we define
$\defeq$ as the smallest equivalence relation extending $\bredc$, where $\bredc$
is the reflexive transitive closure of $\bred$; and we treat types that are
-relate according to $\defeq$ as the same. Another way of seeing $\defeq$ is
+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
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
there is a $p$ such that $\termm \bredc \termp$ and $\termn \bredc \termp$).
This measure makes sure that, for instance, $\app{(\abs{x :
\lctype}{x})}{\lcbool} \defeq \lcbool$. The theme of equality is central
-and will be analysed better later.
+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
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.
-Note that the Curry-Howard correspondence runs through ITT as it did with the
-STLC with the difference that ITT corresponds to an higher order propositional
-logic.
-
\subsection{Base Types}
\label{sec:base-types}
&
\AxiomC{}
\UnaryInfC{$\Gamma \vdash \lcunit : \top$}
- \noLine
- \UnaryInfC{\phantom{1em}}
\DisplayProof
&
\AxiomC{}
of each node is dependent on the value (`shape') in the node. This is captured
by the $\lhd$ constructor, where the argument on the left is the value, and the
argument on the right is a function that returns a child for each possible value
-of $\tyb[\text{node value}]$, if $\lcw{x}{\tya}{\tyb}$. The recursor
-$\lcrec{\termt}{x}{\tyc}{\termp}$ uses $p$ to inductively prove that
-$\tyc[\termt]$ holds.
+of $\tyb[\text{node value}]$. The recursor $\lcrec{\termt}{x}{\tyc}{\termp}$
+uses $p$ to inductively prove that $\tyc[\termt]$ holds.
-\subsection{Some examples}
+\subsection{Examples}
Now we can finally provide some meaningful examples. Apart from omitting types,
I will also use some abbreviations:
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
+I postpone more complex examples after the introduction of inductive families
and pattern matching, since $\lccon{W}$ types get unwieldy very quickly.
\subsection{Propositional Equality}
\label{sec:propeq}
-We can finally introduce one of the central subjects of my project:
-propositional equality.
+I can finally introduce one of the central subjects of my project: propositional
+equality.
\newcommand{\lceq}[3]{#2 =_{#1} #3}
\newcommand{\lceqz}[2]{#1 = #2}
\vspace{0.5cm}
- \begin{tabular}{c c}
+ \begin{tabular}{c}
\AxiomC{$\Gamma \vdash \termt : \tya$}
\UnaryInfC{$\Gamma \vdash \lcrefl{\tya}{\termt} : \lceq{\tya}{\termt}{\termt}$}
\DisplayProof
- &
+ \end{tabular}
+
+ \vspace{0.5cm}
+
+ \begin{tabular}{c}
\AxiomC{$\Gamma \vdash \termp : \lceq{\tya}{\termt}{\termm}$}
\AxiomC{$\Gamma \vdash \tyb : \tya \tyarr \lcsetz$}
\AxiomC{$\Gamma \vdash \termn : \app{\tyb}{\termt}$}
\section{A more useful language}
\label{sec:practical}
-While our core type theory equipped with $\lccon{W}$ types is very usefully
+While our core type theory equipped with $\lccon{W}$ types is very useful
conceptually as a simple but complete language, things get messy very fast,
since handling $\lccon{W}$ types directly is incredibly cumbersome. In this
section I will present the elements that are usually included in theorem provers
or programming languages to make them usable by mathematicians or programmers.
-All the features presented are present in the second version of the Agda system
+All the features are presented following the second version of the Agda system
\citep{Norell2007, Bove2009}. Agda follows a tradition of theorem provers based
on ITT with inductive families and pattern matching. The closest relative of
Agda, apart from previous versions, is Epigram \citep{McBride2004, EpigramTut}.
and most popular \citep{Coq}.
The main difference between Coq and Agda/Epigram is that the former focuses on
-theorem proving, while the latter also want to be useful as functional
+theorem proving, while the latter also wants 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). Every feature will be
-presented as it is Agda.
+but better support for pattern matching in Agda/Epigram).
-As previously, all the examples presented have been codified in Agda, see
-appendix \ref{app:agda-code}.
+Again, all the examples presented have been codified in Agda, see appendix
+\ref{app:agda-code}.
\subsection{Type inference}
human being), this is a great burden. Complete inference is undecidable - which
is hardly surprising considering the role that types play - but partial
inference in the style of \cite{Pierce2000}, also called `bidirectional type
-checking' in this context, will have to be deployed in a practical system.
+checking', will have to be deployed in a practical system.
Agda gives users an explicit way to indicate which fields should be implicit, by
wrapping them in curly braces in type signatures: $\{A : \lcsetz\} \tyarr
variables.}.
Inductive families bring this concept one step further by allowing some of the
-parameters to be constrained by constructors. We call these `variable'
-parameters `indices'. For example we might define natural numbers
+parameters to be constrained by constructors. We call these parameters
+`indices'. For example we might define natural numbers:
\[
\begin{array}{l}
\lcdata{\lcnat} : \lcsetz \lcwhere \\
\end{array}
\end{array}
\]
-And then define a type for lists indexed by length:
+And then define a family for lists indexed by length:
\[
\begin{array}{l}
\lcdata{\lccon{Vec}}\appsp (A : \lcsetz) : \lcnat \tyarr \lcsetz \lcwhere \\
Also note that the parameters' identifiers will be in scope across all
constructors, while indices' won't.
-In this $\lccon{Vec}$ example, when we form a new list the length is
+In the $\lccon{Vec}$ example, when we form a new list the length is
$\lccon{zero}$. When we append a new element to an existing list of length $n$,
the new list is of length $\app{\lccon{suc}}{n}$, that is, one more than the
previous length. Once $\lccon{Vec}$ is defined we can do things much more
\subsubsection{Computing with inductive families}
-I have carefully avoided to define the functions that I mentioned as example,
+I have carefully avoided defining the functions that I mentioned as examples,
since one question still is unanswered: `how do we work with inductive
-families'? The most basic approach is to work with eliminators, that can be
+families'? The most basic approach is to use eliminators, that can be
automatically provided by the programming language for each data type defined.
For example the induction principle on natural numbers will serve as an
eliminator for $\lcnat$:
\end{array}
\]
-That is, if we provide an $A$ (base case), and then given a number and an $A$ we
-give the next $A$ (inductive step), then an $A$ can be computed for every
+That is, if we provide an $A$ (base case), and if given a number and an $A$ we
+can provide the next $A$ (inductive step), then an $A$ can be computed for every
number. This can be expressed easily in Haskell:
\begin{lstlisting}
data Nat = Zero | Suc Nat
\emph{General} recursion (exemplified by the $\lcsyn{fix}$ combinator in section
\ref{sec:stlc}) cannot be added if we want to keep our theory free of $\bot$.
The common solution to this problem is to allow recursive calls only if the
-arguments are structurally smaller than what the function received, what is
-known as \emph{structural} recursion. For example, if we have a $\lccon{Tree}$
-family with a $\lccon{node}\appsp l \appsp r$ (and maybe others) constructor,
-functions that work on $\lccon{Tree}$ will be able to make recursive calls on
-$l$ and $r$.
+arguments are structurally smaller than what the function received. For
+example, if we have a $\lccon{Tree}$ family with a $\lccon{node}\appsp l \appsp
+r$ constructor, functions that work on $\lccon{Tree}$ will be able to make
+recursive calls on $l$ and $r$.
Pattern matching on the other hand gains considerable power with inductive
families, since when we match a constructor we are gaining information on the
\subsection{Friendlier universes}
-Universes as presented in section \ref{sec:core-tt} are quite cumbersome to work
+Universes as presented in section \ref{sec:core-tt} are quite annoying to work
with. Consider the example where we define an inductive family for booleans and
then we want to define an `if then else' eliminator:
\[
quite a lot of noise. An inference algorithm that automatically quantifies and
instantiates levels (much like Hindley-Milner for types) seems feasible, but is
currently not implemented anywhere. The ideal situation would be polymorphic,
-cumulative levels, with an easy way to omit treatment of levels unless in the
-(possibly few) cases where the inference algorithm breaks down.
+cumulative levels, with an easy way to omit explicit treatment of levels unless
+in the (possibly few) cases where the inference algorithm breaks down.
\subsection{Coinduction}
as implemented by Coq and Agda is not satisfactory in different ways.
\section{Many equalities}
+\label{sec:equality}
\subsection{Revision, and function extensionality}
\label{sec:fun-ext}
($\defeq$) and \emph{propositional} equality ($=_{\tya}$).
Definitional equality relates terms that the type checker identifies as equal.
-Our definition in section \ref{sec:core-tt} consisted of `reduce the two terms
+The definition in section \ref{sec:core-tt} consisted of `reduce the two terms
to their normal forms, then check if they are equal (up to $\alpha$-renaming)'.
-We can extend this definition in other ways so that more terms will be
-identified as equal. Common ones include doing $\eta$-expansion, which converts
-partial appications of functions, and congruence laws for $\lambda$:
+We can extend this in other ways so that more terms will be identified as equal.
+Common tricks include doing $\eta$-expansion, which converts partial appications
+of functions, and congruence laws for $\lambda$:
\begin{center}
\begin{tabular}{c c c}
\AxiomC{$\Gamma \vdash \termf : \tya \tyarr \tyb$}
It is worth noting that all $\lcfun{subst}$s, in ITT, are guaranteed to reduce
at the top level. This is because $\lccon{refl}$ is the only constructor for
-propositional equality, and thus without false assumptions every top level proof
+propositional equality, and thus without false assumptions every closed proof
will have that shape. Extending this idea to other types, in ITT, at the top
level, expressions have \emph{canonical} values - a property known as
-\emph{canonicity}. We call canonical those values formed by constructors:
-$\lambda$, $(,)$, $\lhd$, etc. In other words a value is canonical if it's not
-something that is supposed to reduced (an eliminator) but is stuck on some
-variable.
+\emph{canonicity}. We call canonical those values formed by canonical
+constructors, that do not appear on the left of $\bred$: $\lambda$, $(,)$,
+$\lhd$, etc. In other words a value is canonical if it's not something that is
+supposed to reduce (an eliminator) but is stuck on some variable.
While propositional equality is a very useful construct, we can prove less terms
equal than we would like to. For example, if we have the usual functions
needs to carry complete derivations for each typing judgement, instead of
relying on terms only.
+This is troubling if we want to retain the good computational behaviour of ITT
+and has kept languages like Agda, Epigram, and Coq from adopting the equality
+reflection rule.
+
\subsection{Observational equality}
\newcommand{\lcprop}{\lccon{Prop}}
\newcommand{\lcparr}{\Rightarrow}
A recent development by \citet{Altenkirch2007} promises to keep the well
-behavedness of ITT while being able to gain many useful equality proofs,
-including function extensionality. The main idea is to give the user the
-possibility to \emph{coerce} (or transport) values from a type $A$ to a type
-$B$, if the type checker can prove structurally that $A$ and $B$ are equal.
-
-This said, starting from a theory similar to the one presented in section
-\ref{sec:itt} but with only $\lcset{0}$ and without propositional equality, a
-propositional subuniverse of $\lcsetz$ is introduced, plus a `decoding' function
-$\lcdec{\_}$:
+behavedness of ITT while being able to gain many useful equality
+proofs\footnote{It is suspected that Observational Type Theory gains \emph{all}
+ the equality proofs of ETT, but no proof exists yet.}, including function
+extensionality. The main idea is to give the user the possibility to
+\emph{coerce} (or transport) values from a type $A$ to a type $B$, if the type
+checker can prove structurally that $A$ and $B$ are equal; and providing a
+value-level equality based on similar principles.
+
+Starting from a theory similar to the one presented in section \ref{sec:itt} but
+with only $\lcset{0}$ and without propositional equality, a propositional
+subuniverse of $\lcsetz$ is introduced, plus a `decoding' function $\lcdec{\_}$:
\begin{center}
\axname{syntax}
\vspace{0.5cm}
\begin{tabular}{c c c}
- \AxiomC{\phantom{1em}}
+ \AxiomC{}
\UnaryInfC{$\Gamma \vdash \lcprop : \lcsetz$}
- \noLine
- \UnaryInfC{\phantom{1em}}
\DisplayProof
&
- \AxiomC{\phantom{1em}}
+ \AxiomC{}
\UnaryInfC{$\Gamma \vdash \bot : \lcprop$}
\noLine
\UnaryInfC{$\Gamma \vdash \top : \lcprop$}
\AxiomC{$\Gamma \vdash P : \lcprop$}
\AxiomC{$\Gamma \vdash Q : \lcprop$}
\BinaryInfC{$\Gamma \vdash P \wedge Q : \lcprop$}
- \noLine
- \UnaryInfC{\phantom{1em}}
\DisplayProof
\end{tabular}
\end{eqnarray*}
\end{center}
I will use $P \lcparr Q$ as an abbreviation for $\lcpropf{\_}{P}{Q}$. Note that
-$\lcprop$ has no `data', but only proofs. This has the consequence that code
-using proofs, when compiled, will be able to safely erase every $\lcprop$, as
-long as it doesn't compute under binder - and we most likely don't need to
-compute under binders after we type checked and we just need to run the code.
-Moreover, we can extend $\lcprop$ with other axioms while retaining canonicity,
-since
+$\lcprop$ has no `data', but only proofs. This has the consequence that when
+compiling code using $\lcprop$ it will be safe to erase every $\lcprop$, as long
+as we don't compute under binders - and we most likely don't need to compute
+under binders after we type checked and we just need to run the code. Another
+consequence of the fact that $\lcprop$ is irrelevant computationally is that we
+can extend $\lcprop$ with other axioms while retaining canonicity. Note that
+this works as long as $\lcdec{\bot}$ is unhabited: if we add inconsistent axioms
+then we can `pull' data out of $\lcprop$.
\newcommand{\lccoe}[4]{\lcfun{coe}\appsp#1\appsp#2\appsp#3\appsp#4}
\newcommand{\lccoh}[4]{\lcfun{coh}\appsp#1\appsp#2\appsp#3\appsp#4}
In the first row, $=$ forms equality between types, and $\lcfun{coe}$ (`coerce')
transports values of equal types. On the second row, $=$ forms equality between
values, and $\lcfun{coh}$ (`coherence') guarantees that all equalities are
-really between equal things. Now the tricky part is to define reduction rules
-to reduce the proofs of equality to something $\lcdec{\_}$ can reduce, so that
-proof of equality will exist only between equal things, and that $\lcfun{coe}$
-will compute only when those proofs are derivable.
+really between equal things. Note that the value equality is quite different
+from the propositional equality that we are used to, since it allows equality
+between arbitrary types. This kind of equality is called `heterogeneous'
+equality and was introduced by \cite{McBride1999}. Now the tricky part is to
+define reduction rules to reduce the proofs of equality to something
+$\lcdec{\_}$ can work with, being careful that proofs of equality will exist
+only between equal things.
Let's start with type-level $=$:
$$
\bot & = & \bot & \bred & \top \\
\top & = & \top & \bred & \top \\
\lcbool & = & \lcbool & \bred & \top \\
- (s : S) \times T & = & (s' : S') \times T' & \bred & S = S' \wedge \lcpropf{s}{S}{\lcpropf{s'}{S'}{(s : S) = (s' : S') \lcparr T[x] = T'[x']}} \\
- (s : S) \tyarr T & = & (s' : S') \tyarr T' & \bred & S' = S \wedge \lcpropf{s'}{S'}{\lcpropf{s}{S}{(s' : S') = (s : S) \lcparr T[x] = T'[x']}} \\
- \lcw{s}{S}{T} & = & \lcw{s'}{S'}{T'} & \bred & S = S' \wedge \lcpropf{s}{S}{\lcpropf{s'}{S'}{(s : S) = (s' : S') \lcparr T'[x'] = T[x]}} \\
- S & = & T & \bred & \bot\ \text{for every other canonical sets $S$ and $T$}
+ (s : S) \times T & = & (s' : S') \times T' & \bred & \\
+ \multicolumn{5}{l}{
+ \hspace{0.8cm}
+ S = S' \wedge \lcpropf{s}{S}{\lcpropf{s'}{S'}{(s : S) = (s' : S') \lcparr T[x] = T'[x']}}
+ } \\
+ (s : S) \tyarr T & = & (s' : S') \tyarr T' & \bred & \\
+ \multicolumn{5}{l}{
+ \hspace{0.8cm}
+ S' = S \wedge \lcpropf{s'}{S'}{\lcpropf{s}{S}{(s' : S') = (s : S) \lcparr T[x] = T'[x']}}
+ } \\
+ \lcw{s}{S}{T} & = & \lcw{s'}{S'}{T'} & \bred & \\
+ \multicolumn{5}{l}{
+ \hspace{0.8cm}
+ S = S' \wedge \lcpropf{s}{S}{\lcpropf{s'}{S'}{(s : S) = (s' : S') \lcparr T'[x'] = T[x]}}
+ } \\
+ S & = & T & \bred & \bot\ \text{for other canonical types}
\end{array}
$$
The rule for $\times$ is unsurprising: it requires the left types to be equal,
\lccoe{&\bot}{&\bot}{&Q}{z} & \bred & z \\
\lccoe{&\top}{&\top}{&Q}{u} & \bred & u \\
\lccoe{&\lcbool}{&\lcbool}{&Q}{b} & \bred & b \\
- \lccoe{&((x : S) \times T)}{&((x' : S') \times T')}{&Q}{(s, t)} & \bred & \\
+ \lccoe{&((s : S) \times T)}{&((s' : S') \times T')}{&Q}{p} & \bred & \\
\multicolumn{6}{l}{
\lcind
\begin{array}{l@{\ } l@{\ } c@{\ } l@{\ }}
- \lcsyn{let} & Q_S & \mapsto & \lcfst Q : \lcdec{S = S'} \\
+ \lcsyn{let} & s & \mapsto & \lcfst p : S \\
+ & t & \mapsto & \lcsnd p : T[s] \\
+ & Q_S & \mapsto & \lcfst Q : \lcdec{S = S'} \\
& s' & \mapsto & \lccoe{S}{S'}{Q}{s} : S' \\
& Q_T & \mapsto & \lcsnd Q \appsp s \appsp s' \appsp (\lccoh{S}{S'}{Q_S}{s}) : \lcdec{T[s] = T[s']} \\
& t' & \mapsto & \lccoe{T[t]}{T'[s']}{Q_T}{t} : T'[s'] \\
\tyarr \lcdec{T[x] = T'[x']})$$ We need to obtain a $(x' : S') \times T'$. We
can easily get the left part with the left of $Q$ and a coercion, and the right
with the help of $\lcfun{coh}$ and the right of $Q$. The rules for the other
-binders are similar but not reproduced here for brevity. The reader can refer
-to the paper for more details.
+binders are similar but not reproduced here for brevity. Note that
+$\lcfun{coe}$ computes on $Q$ and on the value very lazily, never matching on
+the pairs, meaning that $\lcfun{coe}$ will always reduce when working with
+canonical values and types.
-Now we are left
+Since $\lcfun{coh}$ is a propositional axiom, we can leave it without reduction
+rules. Now we are left with value equality:
+$$
+\begin{array}{r@{\ } c@{\ } l c l}
+ (z : \bot) &=& (z' : \bot) & \bred & \top \\
+ (u : \top) &=& (u' : \top) & \bred & \top \\
+ (\lctrue : \lcbool) &=& (\lctrue : \lcbool) & \bred & \top \\
+ (\lctrue : \lcbool) &=& (\lcfalse : \lcbool) & \bred & \top \\
+ (\lcfalse : \lcbool) &=& (\lctrue : \lcbool) & \bred & \bot \\
+ (\lcfalse : \lcbool) &=& (\lcfalse : \lcbool) & \bred & \top \\
+ (f : (s : S) \tyarr T) &=& (f' : (s' : S') \tyarr T) & \bred & \\
+ \multicolumn{5}{l}{
+ \hspace{1cm}
+ \lcpropf{s}{S}{\lcpropf{s'}{S'}{(s : S) = (s' : S') \lcparr (\app{f}{s} : T[s]) = (\app{f'}{s'} : T'[s'])}}
+ }\\
+ (p : (s : S) \times T) &=& (p : (s' : S') \times T') & \bred & \\
+ \multicolumn{5}{l}{
+ \hspace{1cm}
+ (\lcfst p : S) = (\lcfst p' : S') \wedge (\lcsnd p : T[\lcfst p]) = (\lcsnd p' : T'[\lcfst p'])
+ }\\
+ (s \lhd f : \lcw{s}{S}{T}) &=& (s' \lhd f' : \lcw{s'}{S'}{T'}) & \bred & \\
+ \multicolumn{5}{l}{
+ \hspace{1cm}
+ (s : S) = (s' : S') \wedge (\lcpropf{t}{T[s]}{\lcpropf{t'}{T'[s']}{(t : T[s]) = (t' : T'[s']) \lcparr}}
+ }\\
+ \multicolumn{5}{l}{
+ \hspace{4.5cm}
+ (\app{f}{s} : \lcw{s}{S}{T}) = (\app{f'}{s'} : \lcw{s}{S'}{T'}))
+ }\\
+ (s : S) &=& (s' : S') & \bred & \bot\ \text{for other canonical types}
+\end{array}
+$$
+Functions are equal if they take equal inputs to equal outputs, which satisfies
+our need of extensionality. $\times$ and $\lccon{W}$ work similiarly. The
+authors called this kind of equality `observational' since it computes based on
+the structure of the values, and theories implementing it take the name
+`Observational Type Theories' (OTTs). For lack of space, I have glossed over
+many details explained in the paper showing why OTT works, but hopefully my
+explanaition should give an idea on how the pieces fit together - the reader
+should refer to \citep{Altenkirch2007} for the complete story.
-% TODO put the coind paper
\section{What to do}
My goal is to advance the practice of OTT. Conor McBride and other
collaborators already implemented OTT and other measures as part of efforts
towards a new version of Epigram\footnote{Available at
- \url{http://www.e-pig.org/darcs/Pig09/web/}.}. However the development is
-stale right now and it is not clear when and if Epigram 2 will be released.
+ \url{http://www.e-pig.org/darcs/Pig09/web/}.}. However development is stale
+and it is not clear when and if Epigram 2 will be released.
The first thing that would be very useful to do is to have a small, core
language that supports OTT, on which a more expressive language can be built.
This follows an established tradition in functional programming and theorem
proving of layering several languages of increasing complexity, so that type
-checking at a lower level is much simpler and those more prone to bugs. For
-example GHC Haskell uses an internal language, System F\textsubscript{C}
+checking at a lower level is much simpler and less prone to bugs. For example
+GHC Haskell uses an internal language, System F\textsubscript{C}
\citep{Sulzmann2007}, which includes only minimal features compared to Haskell.
I have already implemented a type theory as described in section
\ref{sec:itt}\footnote{Available at \url{https://github.com/bitonic/mfixed}.} to
make myself comfortable with how such systems work. From that, a good starting
point to build something more useful could be $\Pi\Sigma$
-\citep{Altenkirch2007}, a core, partial language, thought to be a good target
+\citep{Altenkirch2007}, a core partial language, devised to be a good target
for high level languages like Agda, with facilities to implement inductive
families and corecursion. Starting to think about how OTT would work in such a
language is my immediate goal.
level language would look like and how it would be `elaborated' to the lower
level core theory. Epigram 2 can certainly be an inspiration, although it
employs a sophisticated reflection system \citep{Chapman2010} that I do not plan
-to implement. In any case, there are many things to do, with the most salients
-point being how to treat inductive families and pattern matching, corecursion,
-and what a friendly interface for OTT would be from the
-programmer/mathematician's perspective (or maybe whether it's feasible to always
+to reproduce. In any case, there are many things to think about, with the most
+salients point being how to treat inductive families and pattern matching,
+corecursion, and what a friendly interface for OTT would be from the
+programmer/mathematician's perspective (and whether it's feasible to always
infer coercions and/or equality proofs automatically).
-Interestingly, the mentioned System F\textsubscript{C} was introduced in GHC to
-be able to implement GADTs, which as said in section
+Interestingly, the mentioned System F\textsubscript{C} was introduced in GHC 7
+to be able to implement GADTs, which as said in section
\ref{sec:inductive-families} bear many similarities to inductive families. To
-do that it uses a system of coercions that is not too far away from OTT
-coercions. This is not a coincidence, since indices and propositional equality
-are often connected, and offers a lot of food for thought. For instance, GHC
-Haskell automatically generates and applies equality proofs, and the inference
-engine that serves this purpose is quite complex \citep{Vytiniotis2011} and
-often very confusing to the user; we would like to have a less `magic' but
-clearer system.
+do that it uses a system of coercions that is not too far away from OTT. This
+is not a coincidence, since indices and propositional equality are often
+connected, and offers a lot of food for thought. For instance, GHC
+automatically generates and applies equality proofs, and the inference engine
+that serves this purpose is quite complex \citep{Vytiniotis2011} and often very
+confusing to the user; we would like to have a less `magic' but clearer system.
\bibliographystyle{authordate1}
\bibliography{InterimReport}
projects / bitonic-mengthesis.git / commitdiff