diff options
| -rw-r--r-- | thesis.bib | 33 | ||||
| -rw-r--r-- | thesis.lagda | 386 |
2 files changed, 319 insertions, 100 deletions
@@ -73,12 +73,11 @@ publisher = Prentice-Hall } - @article{Altenkirch2010, -author = {Altenkirch, Thorsten and Danielsson, N and L\"{o}h, A and Oury, Nicolas}, +author = {Altenkirch, Thorsten and Danielsson, Nils Anders and L\"{o}h, Andres and Oury, Nicolas}, file = {:home/bitonic/docs/papers/PiSigma.pdf:pdf}, -journal = {Functional and Logic \ldots}, -number = {Sheard 2005}, +journal = {Functional and Logic Programming}, +pages = {40--55}, title = {{$\Pi$$\Sigma$: dependent types without the sugar}}, url = {http://www.springerlink.com/index/91W712G2806R575H.pdf}, year = {2010} @@ -222,6 +221,14 @@ url = {http://strictlypositive.org/view.ps.gz}, volume = {14}, year = {2004} } +@phdthesis{McBride1999, +author = {McBride, Conor}, +file = {:home/bitonic/.local/share/data/Mendeley Ltd./Mendeley Desktop/Downloaded/McBride - 1999 - Dependently typed functional programs and their proofs.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} +} @phdthesis{Norell2007, author = {Norell, Ulf}, file = {:home/bitonic/docs/papers/ulf-thesis.pdf:pdf}, @@ -287,6 +294,16 @@ title = {{System F with type equality coercions}}, url = {http://portal.acm.org/citation.cfm?doid=1190315.1190324}, year = {2007} } +@article{Tait1967, +author = {Tait, William W.}, +file = {:home/bitonic/docs/papers/tait-normalising.pdf:pdf}, +journal = {The Journal of Symbolic Logic}, +number = {2}, +pages = {198--212}, +title = {{Intensional Interpretations of Functionals of Finite Type}}, +volume = {32}, +year = {1967} +} @article{Vytiniotis2011, author = {Vytiniotis, Dimitrios and Jones, Simon Peyton and Schrijvers, Tom and Sulzmann, Martin}, file = {:home/bitonic/docs/papers/outsidein.pdf:pdf}, @@ -311,11 +328,3 @@ 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 index b1539c6..b18a2db 100644 --- a/thesis.lagda +++ b/thesis.lagda @@ -18,6 +18,9 @@ %% Proof trees \usepackage{bussproofs} +%% Diagrams +\usepackage[all]{xy} + %% ----------------------------------------------------------------------------- %% Commands for Agda \usepackage[english]{babel} @@ -26,8 +29,14 @@ \renewcommand{\AgdaFunction}[1]{\textbf{\textcolor{AgdaFunction}{#1}}} \renewcommand{\AgdaField}{\AgdaFunction} \definecolor{AgdaBound} {HTML}{000000} +\definecolor{AgdaHole} {HTML} {FFFF33} \DeclareUnicodeCharacter{9665}{\ensuremath{\lhd}} +\DeclareUnicodeCharacter{964}{\ensuremath{\tau}} +\DeclareUnicodeCharacter{963}{\ensuremath{\sigma}} +\DeclareUnicodeCharacter{915}{\ensuremath{\Gamma}} +\DeclareUnicodeCharacter{8799}{\ensuremath{\stackrel{?}{=}}} + %% ----------------------------------------------------------------------------- %% Commands @@ -37,20 +46,21 @@ \newcommand{\mydc}{\AgdaInductiveConstructor} \newcommand{\myfld}{\AgdaField} \newcommand{\myfun}{\AgdaFunction} -% TODO make this use AgdaBount +% TODO make this use AgdaBound \newcommand{\myb}[1]{\ensuremath{#1}} \newcommand{\myfield}{\AgdaField} \newcommand{\myind}{\AgdaIndent} \newcommand{\mykant}{\textsc{Kant}} -\newcommand{\mysynel}[1]{\langle #1 \rangle} +\newcommand{\mysynel}[1]{#1} \newcommand{\mytmsyn}{\mysynel{term}} \newcommand{\mysp}{\ } -\newcommand{\myabs}[2]{\lambda #1 \mapsto #2} +% TODO \mathbin or \mathre here? +\newcommand{\myabs}[2]{\mydc{$\lambda$} #1 \mathrel{\mydc{$\mapsto$}} #2} \newcommand{\myappsp}{\hspace{0.07cm}} \newcommand{\myapp}[2]{#1 \myappsp #2} \newcommand{\mysynsep}{\ \ |\ \ } -\FrameSep0.3cm +\FrameSep0.2cm \newcommand{\mydesc}[3]{ \hfill \textbf{#1} $#2$ \vspace{-0.2cm} @@ -72,22 +82,41 @@ \newcommand{\mybasety}[1]{B_{#1}} \newcommand{\mytya}{\myb{A}} \newcommand{\mytyb}{\myb{B}} -\newcommand{\myarr}{\mathbin{\textcolor{AgdaDatatype}{\to}}} -\newcommand{\myprod}{\mathbin{\textcolor{AgdaDatatype}{\times}}} +\newcommand{\mytycc}{\myb{C}} +\newcommand{\myarr}{\mathrel{\textcolor{AgdaDatatype}{\to}}} +\newcommand{\myprod}{\mathrel{\textcolor{AgdaDatatype}{\times}}} \newcommand{\myctx}{\Gamma} \newcommand{\myvalid}[1]{#1 \vdash \underline{\mathrm{valid}}} \newcommand{\myjudd}[3]{#1 \vdash #2 : #3} \newcommand{\myjud}[2]{\myjudd{\myctx}{#1}{#2}} -\newcommand{\myabss}[3]{\lambda #1 {:} #2 \mapsto #3} +% TODO \mathbin or \mathrel here? +\newcommand{\myabss}[3]{\mydc{$\lambda$} #1 {:} #2 \mathrel{\mydc{$\mapsto$}} #3} \newcommand{\mytt}{\mydc{tt}} \newcommand{\myunit}{\mytyc{$\top$}} -\newcommand{\mypair}[2]{(#1\mathpunct{\textcolor{AgdaInductiveConstructor}{,}} #2)} -\newcommand{\myfst}[1]{\myapp{\myfld{fst}}{#1}} -\newcommand{\mysnd}[1]{\myapp{\myfld{snd}}{#1}} +\newcommand{\mypair}[2]{\mathopen{\mydc{$\langle$}}#1\mathpunct{\mydc{,}} #2\mathclose{\mydc{$\rangle$}}} +\newcommand{\myfst}{\myfld{fst}} +\newcommand{\mysnd}{\myfld{snd}} \newcommand{\myconst}{\myb{c}} \newcommand{\myemptyctx}{\cdot} -\newcommand{\myhole}{\AgdaUnsolvedMeta} +\newcommand{\myhole}{\AgdaHole} \newcommand{\myfix}[3]{\mysyn{fix} \myappsp #1 {:} #2 \mapsto #3} +\newcommand{\mysum}{\mathbin{\textcolor{AgdaDatatype}{+}}} +\newcommand{\myleft}[1]{\mydc{left}_{#1}} +\newcommand{\myright}[1]{\mydc{right}_{#1}} +\newcommand{\myempty}{\mytyc{$\bot$}} +\newcommand{\mycase}[2]{\mathopen{\myfun{[}}#1\mathpunct{\myfun{,}} #2 \mathclose{\myfun{]}}} +\newcommand{\myabsurd}[1]{\myfun{absurd}_{#1}} +\newcommand{\myarg}{\_} +\newcommand{\myderivsp}{\vspace{0.3cm}} +\newcommand{\mytyp}{\mytyc{Type}} +\newcommand{\myneg}{\myfun{$\neg$}} +\newcommand{\myar}{\,} +\newcommand{\mybool}{\mytyc{Bool}} +\newcommand{\mynat}{\mytyc{$\mathbb{N}$}} +\newcommand{\myrat}{\mytyc{$\mathbb{R}$}} +\newcommand{\myite}[3]{\mysyn{if}\,#1\,\mysyn{then}\,#2\,\mysyn{else}\,#3} +\newcommand{\myfora}[3]{(#1 {:} #2) \myarr #3} +\newcommand{\myexi}[3]{(#1 {:} #2) \mysum #3} %% ----------------------------------------------------------------------------- @@ -100,7 +129,6 @@ \iffalse \begin{code} module thesis where -open import Level \end{code} \fi @@ -181,7 +209,8 @@ formally explained by the $\beta$-reduction rule: } The care required during substituting variables for terms is required to avoid -name capturing. +name capturing. We will use substitution in the future for other name-binding +constructs assuming similar precautions. 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 @@ -192,11 +221,11 @@ complete. As a corollary, we must be able to devise a term that reduces forever A \emph{redex} is a term that can be reduced. In the untyped $\lambda$-calculus this will be the case for an application in which the first term is an -abstraction, but in general a term is reducible if it appears to the left of a -reduction rule. When a term contains no redex it's said to be in \emph{normal - form}. Given the observation above, not all terms reduce to a normal forms: -we call the ones that do \emph{normalising}, and the ones that don't -\emph{non-normalising}. +abstraction, but in general we call aterm reducible if it appears to the left of +a reduction rule. When a term contains no redexes it's said to be in +\emph{normal form}. Given the observation above, not all terms reduce to a +normal forms: we call the ones that do \emph{normalising}, and the ones that +don't \emph{non-normalising}. The reduction rule presented is not syntax directed, but \emph{evaluation strategies} can be employed to reduce term systematically. Common evaluation @@ -211,17 +240,17 @@ both abstractions and normal forms are said to be in \emph{weak head normal \subsection{The simply typed $\lambda$-calculus} -A convenient way to `discipline' $\lambda$-terms is to assign \emph{types} to -them, and then check that the terms that we are forming make sense given our -typing rules \citep{Curry1934}. The first most basic instance of this idea -takes the name of \emph{simply typed $\lambda$ calculus}. +A convenient way to `discipline' and reason about $\lambda$-terms is to assign +\emph{types} to them, and then check that the terms that we are forming make +sense given our typing rules \citep{Curry1934}. The first most basic instance +of this idea takes the name of \emph{simply typed $\lambda$ calculus}. Our types contain a set of \emph{type variables} $\Phi$, which might correspond to some `primitive' types; and $\myarr$, the type former for `arrow' types, the types of functions. The language is explicitly typed: when we bring a variable into scope with an abstraction, we explicitly declare its type. $\mytya$, -$\mytyb$ will be used to refer to a generic type. Reduction is unchanged from -the untyped $\lambda$-calculus. +$\mytyb$, $\mytycc$, will be used to refer to a generic type. Reduction is +unchanged from the untyped $\lambda$-calculus. \mydesc{syntax}{ }{ $ @@ -269,9 +298,9 @@ enjoys a number of properties. Two of them are expected in most type systems 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 +\citep{Tait1967}. 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*} \myapp{(\myabss{x}{\myhole{?}}{\myapp{x}{x}})}{(\myabss{x}{\myhole{?}}{\myapp{x}{x}})} \end{equation*} @@ -300,27 +329,32 @@ want to use the STLC as described in the next section. \subsection{The Curry-Howard correspondence} -Moreover, -we have a product (or pair, or tuple) type $\mytya \myprod \mytyb$ for each pair -of types $\mytya$ and $\mytyb$, and a function (or arrow) type $\mytya \myarr -\mytyb$ for each pair of types $\mytya$ and $\mytyb$. $\beta$-reduction is -unchanged, but we have added reduction rules for products. Products are not -essential, but they serve as a good example of a type former apart from the -arrow type. +It turns out that the STLC can be seen a natural deduction system for +intuitionistic propositional logic. Terms are proofs, and their types are the +propositions they prove. This remarkable fact is known as the Curry-Howard +correspondence, or isomorphism. + +The arrow ($\myarr$) type corresponds to implication. If we wish to prove that +that $(\mytya \myarr \mytyb) \myarr (\mytyb \myarr \mytycc) \myarr (\mytya +\myarr \mytycc)$, all we need to do is to devise a $\lambda$-term that has the +correct type: +\[ + \myabss{f}{(\mytya \myarr \mytyb)}{\myabss{g}{(\mytyb \myarr \mytycc)}{\myabss{x}{\mytya}{\myapp{g}{(\myapp{f}{x})}}}} +\] +That is, function composition. We can extend our bare lambda calculus with +useful types to represent other logical constructs. \mydesc{syntax}{ }{ $ \begin{array}{r@{\ }c@{\ }l} - \mytmsyn & ::= & \myb{x} \mysynsep \myconst \mysynsep - \myabss{\myb{x}}{\mytysyn}{\mytmsyn} \mysynsep - (\myapp{\mytmsyn}{\mytmsyn}) \\ - & | & \mytt \mysynsep \mypair{\mytmsyn}{\mytmsyn} \mysynsep - \myfst{\mytmsyn} \mysynsep \mysnd{\mytmsyn} \\ - \mytysyn & ::= & \mytysyn \myprod \mytysyn \mysynsep - \mytysyn \myarr \mytysyn \mysynsep - \mybasety{\myconst} \\ - \myb{x} & \in & \text{Some enumerable set of symbols} \\ - \myconst & \in & \text{Some set $C$ of constants} \\ + \mytmsyn & ::= & \dots \\ + & | & \mytt \mysynsep \myapp{\myabsurd{\mytysyn}}{\mytmsyn} \\ + & | & \myapp{\myleft{\mytysyn}}{\mytmsyn} \mysynsep + \myapp{\myright{\mytysyn}}{\mytmsyn} \mysynsep + \myapp{\mycase{\mytmsyn}{\mytmsyn}}{\mytmsyn} \\ + & | & \mypair{\mytmsyn}{\mytmsyn} \mysynsep + \myapp{\myfst}{\mytmsyn} \mysynsep \myapp{\mysnd}{\mytmsyn} \\ + \mytysyn & ::= & \dots \mysynsep \myunit \mysynsep \myempty \mysynsep \mytmsyn \mysum \mytmsyn \mysynsep \mytysyn \myprod \mytysyn \end{array} $ } @@ -328,48 +362,221 @@ arrow type. \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{ \centering{ \begin{tabular}{cc} - $\myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{x}{\mytmn}$ & $ - \begin{array}{r@{\ }c@{\ }l} - \myapp{\myfst}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmm \\ - \myapp{\mysnd}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmn + \begin{array}{l@{ }l@{\ }c@{\ }l} + \myapp{\mycase{\mytmm}{\mytmn}}{(\myapp{\myleft{\mytya} &}{\mytmt})} & \myred & + \myapp{\mytmm}{\mytmt} \\ + \myapp{\mycase{\mytmm}{\mytmn}}{(\myapp{\myright{\mytya} &}{\mytmt})} & \myred & + \myapp{\mytmn}{\mytmt} + \end{array} + $ + & + $ + \begin{array}{l@{ }l@{\ }c@{\ }l} + \myapp{\myfst &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmm \\ + \myapp{\mysnd &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmn \end{array} $ \end{tabular} } } -% TODO write context rules -% \mydesc{validity:}{\myvalid{\myctx}}{ -% \centering{ -% \begin{tabular}{ccc} -% \AxiomC{} -% \UnaryInfC{$\myvalid{\myemptyctx}$} -% \DisplayProof -% & -% \AxiomC{$\mytmt : \mytya$} -% \UnaryInfC{$\myvalid{\myctx; x : \mytya -% bar & -% baz -% \end{tabular} -% } -% } - \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{ \centering{ \begin{tabular}{cc} - \AxiomC{$x : A \in \myctx$} - \UnaryInfC{$\myjud{x}{A}$} + \AxiomC{} + \UnaryInfC{$\myjud{\mytt}{\myunit}$} + \DisplayProof + & + \AxiomC{$\myjud{\mytmt}{\myempty}$} + \UnaryInfC{$\myjud{\myapp{\myabsurd{\mytya}}{\mytmt}}{\mytya}$} + \DisplayProof + \end{tabular} + } + \myderivsp + \centering{ + \begin{tabular}{cc} + \AxiomC{$\myjud{\mytmt}{\mytya}$} + \UnaryInfC{$\myjud{\myapp{\myleft{\mytyb}}{\mytmt}}{\mytya \mysum \mytyb}$} + \DisplayProof + & + \AxiomC{$\myjud{\mytmt}{\mytyb}$} + \UnaryInfC{$\myjud{\myapp{\myright{\mytya}}{\mytmt}}{\mytya \mysum \mytyb}$} + \DisplayProof + + \end{tabular} + } + \myderivsp + \centering{ + \begin{tabular}{cc} + \AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$} + \AxiomC{$\myjud{\mytmn}{\mytya \myarr \mytycc}$} + \AxiomC{$\myjud{\mytmt}{\mytya \mysum \mytyb}$} + \TrinaryInfC{$\myjud{\myapp{\mycase{\mytmm}{\mytmn}}{\mytmt}}{\mytycc}$} + \DisplayProof + \end{tabular} + } + \myderivsp + \centering{ + \begin{tabular}{ccc} + \AxiomC{$\myjud{\mytmm}{\mytya}$} + \AxiomC{$\myjud{\mytmn}{\mytyb}$} + \BinaryInfC{$\myjud{\mypair{\mytmm}{\mytmn}}{\mytya \myprod \mytyb}$} + \DisplayProof + & + \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$} + \UnaryInfC{$\myjud{\myapp{\myfst}{\mytmt}}{\mytya}$} \DisplayProof & - foo + \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$} + \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mytyb}$} + \DisplayProof \end{tabular} } } +Tagged unions (or sums, or coproducts---$\mysum$ here, \texttt{Either} in +Haskell) correspond to disjunctions, and dually tuples (or pairs, or +products---$\myprod$ here, tuples in Haskell) correspond to conjunctions. This +is apparent looking at the ways to construct and destruct the values inhabiting +those types: for $\mysum$ $\myleft{ }$ and $\myright{ }$ correspond to $\vee$ +introduction, and $\mycase{\_}{\_}$ to $\vee$ elimination; for $\myprod$ +$\mypair{\_}{\_}$ corresponds to $\wedge$ introduction, $\myfst$ and $\mysnd$ to +$\wedge$ elimination. + +The trivial type $\myunit$ corresponds to the logical $\top$, and dually +$\myempty$ corresponds to the logical $\bot$. $\myunit$ has one introduction +rule ($\mytt$), and thus one inhabitant; and no eliminators. $\myempty$ has no +introduction rules, and thus no inhabitants; and one eliminator ($\myabsurd{ +}$), corresponding to the logical \emph{ex falso quodlibet}. Note that in the +constructors for the sums and the destructor for $\myempty$ we need to include +some type information to keep type checking decidable. + +As in logic, if we want to keep our system consistent, we must make sure that no +closed terms (in other words terms not under a $\lambda$) inhabit $\myempty$. +The variant of STLC presented here is indeed consistent, a result that follows +from the fact that it is normalising. % TODO explain +Going back to our $\myfix{ }{ }{ }$ combinator, it is easy to see how it breaks +our desire for consistency. The following term works for every type $\mytya$, +including bottom: +\[ +(\myfix{x}{\mytya}{x}) : \mytya +\] + +With these rules, our STLC now looks remarkably similar in power and use to the +natural deduction we already know. $\myneg \mytya$ can be expressed as $\mytya +\myarr \myempty$. However, there is an important omission: there is no term of +the type $\mytya \mysum \myneg \mytya$ (excluded middle), or equivalently +$\myneg \myneg \mytya \myarr \mytya$ (double negation), or indeed any term with +a type equivalent to those. + +This has a considerable effect on our logic and it's no coincidence, since there +is no obvious computational behaviour for laws like the excluded middle. +Theories of this kind are called \emph{intuitionistic}, or \emph{constructive}, +and all the systems analysed will have this characteristic since they build on +the foundation of the STLC\footnote{There is research to give computational + behaviour to classical logic, but I will not touch those subjects.}. + + \section{Intuitionistic Type Theory} \label{sec:itt} +\subsection{Extending the STLC} + +The STLC can be made more expressive in various ways. \cite{Barendregt1991} +succinctly expressed geometrically how we can add expressively: + +$$ +\xymatrix@!0@=1.5cm{ + & \lambda\omega \ar@{-}[rr]\ar@{-}'[d][dd] + & & \lambda C \ar@{-}[dd] + \\ + \lambda2 \ar@{-}[ur]\ar@{-}[rr]\ar@{-}[dd] + & & \lambda P2 \ar@{-}[ur]\ar@{-}[dd] + \\ + & \lambda\underline\omega \ar@{-}'[r][rr] + & & \lambda P\underline\omega + \\ + \lambda{\to} \ar@{-}[rr]\ar@{-}[ur] + & & \lambda P \ar@{-}[ur] +} +$$ +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}$)] We can quantify over + types in our type signatures. For example, we can defined a polymorphic + identity function: + $\displaystyle + (\myabss{\mytya}{\mytyp}{\myabss{x}{A}{x}}) : (\mytya : \mytyp) \myarr \mytya \myarr \mytya + $. + The first and most famous instance of this idea has been System F. This gives + us a form of polymorphism and has been wildly successful, also thanks to a + well known inference algorithm for a restricted version of System F known as + Hindley-Milner. Languages like Haskell and SML are based on this discipline. +\item[Types depending on types (towards $\lambda{\underline{\omega}}$)] We have + type operators. For example we could define a function that given types $R$ + and $\mytya$ forms the type that represents a value of type $\mytya$ in + continuation passing style: $\displaystyle(\myabss{A \myar R}{\mytyp}{(\mytya + \myarr R) \myarr R}) : \mytyp \myarr \mytyp \myarr \mytyp$. +\item[Types depending on terms (towards $\lambda{P}$)] Also known as `dependent + types', give great expressive power. For example, we can have values of whose + type depend on a boolean: + $\displaystyle(\myabss{x}{\mybool}{\myite{x}{\mynat}{\myrat}}) : \mybool + \myarr \mytyp$. +\end{description} + +All the systems preserve the properties that make the STLC well behaved. The +system we are going to focus on, Intuitionistic Type Theory, has all of the +above additions, and thus would sit where $\lambda{C}$ sits in the +`$\lambda$-cube'. + +\subsection{A Bit of History} + +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 inconsistent due to its +impredicativity\footnote{In the early version there was only one universe + $\mytyp$ and $\mytyp : \mytyp$, 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 +and Reynolds. An overview can be found in \citep{Reynolds1994}. The surprising +fact is that while System F is impredicative it is still consistent and strongly +normalising. \cite{Coquand1986} further extended this line of work with the +Calculus of Constructions (CoC). + +\subsection{A core type theory} +\label{sec:core-tt} + +The calculus I present follows the exposition in \citep{Thompson1991}, and is +quite close to the original formulation of predicative ITT as found in +\citep{Martin-Lof1984}. + +\mydesc{syntax}{ }{ + $ + \begin{array}{r@{\ }c@{\ }l} + \mytmsyn & ::= & \myb{x} \\ + & | & \myunit \mysynsep \mytt \\ + & | & \myempty \mysynsep \myapp{\myabsurd{\mytmsyn}}{\mytmsyn} \\ + & | & \myfora{x}{\mytmsyn}{\mytmsyn} \mysynsep + \myabss{x}{\mytmsyn}{\mytmsyn} \\ + & | & \myexi{x}{\mytmsyn}{\mytmsyn} \mysynsep + \mypair{\mytmsyn}{\mytmsyn} \mysynsep \myapp{\myfst}{\mytmsyn} + \end{array} + $ +} + +\mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{ + +} + +\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{ + +} + \section{The struggle for equality} \label{sec:equality} @@ -391,58 +598,61 @@ for example Typing derivations here. } -In the languages presented I will also use different fonts and colors for -different things: +In the languages presented I also highlight the syntax, following a uniform +color and font convention: \begin{center} \begin{tabular}{c | l} $\mytyc{Sans}$ & Type constructors. \\ $\mydc{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. \\ + $\mysyn{roman}$ & Keywords of the language. \\ + $\myfun{roman}$ & Defined values and destructors. \\ $\myb{math}$ & Bound variables. \end{tabular} \end{center} -\section{Agda rendition of a core ITT} +\section{Agda code} \label{app:agda-code} +\subsection{ITT} + \begin{code} module ITT where - data Empty : Set where + open import Level + + data ⊥ : Set where - absurd : ∀ {a} {A : Set a} → Empty → A + absurd : ∀ {a} {A : Set a} → ⊥ → A absurd () - record Unit : Set where + record ⊤ : 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 + fst : A + snd : B fst 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 + if_then_else_ : ∀ {a} {P : Bool → Set a} (x : Bool) → 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. + (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} |