\documentclass[report]{article}
%% Narrow margins
-\usepackage{fullpage}
+% \usepackage{fullpage}
%% Bibtex
\usepackage{natbib}
%% Links
\usepackage{hyperref}
+%% Frames
+\usepackage{framed}
+
+%% Symbols
+\usepackage[fleqn]{amsmath}
+
+%% Proof trees
+\usepackage{bussproofs}
+
+%% Diagrams
+\usepackage[all]{xy}
+
%% -----------------------------------------------------------------------------
%% Commands for Agda
\usepackage[english]{babel}
\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
\newcommand{\mysyn}{\AgdaKeyword}
\newcommand{\mytyc}{\AgdaDatatype}
-\newcommand{\myind}{\AgdaInductiveConstructor}
+\newcommand{\mydc}{\AgdaInductiveConstructor}
\newcommand{\myfld}{\AgdaField}
\newcommand{\myfun}{\AgdaFunction}
-\newcommand{\myb}{\AgdaBound}
+% TODO make this use AgdaBound
+\newcommand{\myb}[1]{\ensuremath{#1}}
\newcommand{\myfield}{\AgdaField}
+\newcommand{\myind}{\AgdaIndent}
+\newcommand{\mykant}{\textsc{Kant}}
+\newcommand{\mysynel}[1]{#1}
+\newcommand{\mytmsyn}{\mysynel{term}}
+\newcommand{\mysp}{\ }
+% 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.2cm
+\newcommand{\mydesc}[3]{
+ \hfill \textbf{#1} $#2$
+ \vspace{-0.2cm}
+ \begin{framed}
+ #3
+ \end{framed}
+}
+
+% TODO is \mathbin the correct thing for arrow and times?
+
+\newcommand{\mytmt}{\myb{T}}
+\newcommand{\mytmm}{\myb{M}}
+\newcommand{\mytmn}{\myb{N}}
+\newcommand{\myred}{\leadsto}
+\newcommand{\mysub}[3]{#1[#2 \mapsto #3]}
+\newcommand{\mytysyn}{\mysynel{type}}
+\newcommand{\mybasetys}{K}
+% TODO change this name
+\newcommand{\mybasety}[1]{B_{#1}}
+\newcommand{\mytya}{\myb{A}}
+\newcommand{\mytyb}{\myb{B}}
+\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}}
+% 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]{\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}{\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}
%% -----------------------------------------------------------------------------
-\title{\textsc{Kant}: Implementing Observational Equality}
-% TODO remove double @ if we get rid of lhs2TeX
+\title{\mykant: Implementing Observational Equality}
\author{Francesco Mazzoli \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{<fm2209@ic.ac.uk>}}}
\date{June 2013}
\iffalse
\begin{code}
module thesis where
-open import Level
\end{code}
\fi
\section{Simple and not-so-simple types}
\label{sec:types}
-\section{Intuitionistic Type Theory and dependent types}
+\subsection{The untyped $\lambda$-calculus}
+
+Along with Turing's machines, the earliest attempts to formalise computation
+lead to the $\lambda$-calculus \citep{Church1936}. This early programming
+language encodes computation with a minimal syntax and no `data' in the
+traditional sense, but just functions. Here we give a brief overview of the
+language, which will give the chance to introduce concepts central to the
+analysis of all the following calculi. The exposition follows the one found in
+chapter 5 of \cite{Queinnec2003}.
+
+The syntax of $\lambda$-terms consists of three things: variables, abstractions,
+and applications:
+
+\mydesc{syntax}{ }{
+ $
+ \begin{array}{r@{\ }c@{\ }l}
+ \mytmsyn & ::= & \myb{x} \mysynsep \myabs{\myb{x}}{\mytmsyn} \mysynsep (\myapp{\mytmsyn}{\mytmsyn}) \\
+ x & \in & \text{Some enumerable set of symbols}
+ \end{array}
+ $
+}
+
+Through this text, I will use $\mytmt$, $\mytmm$, $\mytmn$ to indicate a generic
+term, and $x$, $y$ to refer to variables. Parenthesis will be omitted in the
+usual way: $\myapp{\myapp{\mytmt}{\mytmm}}{\mytmn} =
+\myapp{(\myapp{\mytmt}{\mytmm})}{\mytmn}$.
+
+Abstractions roughly corresponds to functions, and their semantics is more
+formally explained by the $\beta$-reduction rule:
+
+\mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
+ $
+ \begin{array}{l}
+ \myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{x}{\mytmn}\text{, where} \\
+ \myind{1}
+ \begin{array}{l@{\ }c@{\ }l}
+ \mysub{x}{x}{\mytmn} & = & \mytmn \\
+ \mysub{y}{x}{\mytmn} & = & y\text{, with } x \neq y \\
+ \mysub{\myapp{\mytmt}{\mytmm}}{x}{\mytmn} & = & (\myapp{\mysub{\mytmt}{x}{\mytmn}}{\mysub{\mytmm}{x}{\mytmn}}) \\
+ \mysub{(\myabs{x}{\mytmm})}{x}{\mytmn} & = & \myabs{x}{\mytmm} \\
+ \mysub{(\myabs{y}{\mytmm})}{x}{\mytmn} & = & \myabs{z}{\mysub{\mysub{\mytmm}{y}{z}}{x}{\mytmn}}, \\
+ \multicolumn{3}{l}{\myind{1} \text{with $x \neq y$ and $z$ not free in $\myapp{\mytmm}{\mytmn}$}}
+ \end{array}
+ \end{array}
+ $
+}
+
+The care required during substituting variables for terms is required to avoid
+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
+(`loops' in imperative terms):
+\[
+ (\myapp{\omega}{\omega}) \myred (\myapp{\omega}{\omega}) \myred \dots\text{, with $\omega = \myabs{x}{\myapp{x}{x}}$}
+\]
+
+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 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
+strategies include \emph{call by value} (or \emph{strict}), where arguments of
+abstractions are reduced before being applied to the abstraction; and conversely
+\emph{call by name} (or \emph{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: for this reason a weaker form of normalisation is used, where
+both abstractions and normal forms are said to be in \emph{weak head normal
+ form}.
+
+\subsection{The 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$, $\mytycc$, will be used to refer to a generic type. Reduction is
+unchanged from the untyped $\lambda$-calculus.
+
+\mydesc{syntax}{ }{
+ $
+ \begin{array}{r@{\ }c@{\ }l}
+ \mytmsyn & ::= & \myb{x} \mysynsep \myabss{\myb{x}}{\mytysyn}{\mytmsyn} \mysynsep
+ (\myapp{\mytmsyn}{\mytmsyn}) \\
+ \mytysyn & ::= & \myb{\phi} \mysynsep \mytysyn \myarr \mytysyn \mysynsep \\
+ \myb{x} & \in & \text{Some enumerable set of symbols} \\
+ \myb{\phi} & \in & \Phi
+ \end{array}
+ $
+}
+
+\mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
+ \centering{
+ \begin{tabular}{ccc}
+ \AxiomC{$\myctx(x) = A$}
+ \UnaryInfC{$\myjud{\myb{x}}{A}$}
+ \DisplayProof
+ &
+ \AxiomC{$\myjudd{\myctx;\myb{x} : A}{\mytmt}{\mytyb}$}
+ \UnaryInfC{$\myjud{\myabss{x}{A}{\mytmt}}{\mytyb}$}
+ \DisplayProof
+ &
+ \AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$}
+ \AxiomC{$\myjud{\mytmn}{\mytya}$}
+ \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mytyb}$}
+ \DisplayProof
+ \end{tabular}
+ }
+}
+
+In the typing rules, a context $\myctx$ is used to store the types of bound
+variables: $\myctx; \myb{x} : \mytya$ adds a variable to the context and
+$\myctx(x)$ returns the type of the rightmost occurrence of $x$.
+
+This typing system takes the name of `simply typed lambda calculus' (STLC), 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---it is either a variable, or its
+ constructor does not appear on the left of the $\myred$ 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, and preserves the previous type.
+\end{description}
+
+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*}
+
+This makes the STLC Turing incomplete. We can recover the ability to loop by
+adding a combinator that recurses:
+
+% TODO make this more compact
+
+\mydesc{syntax}{ } {
+ $ \mytmsyn ::= \dotsb \mysynsep \myfix{x}{\mytysyn}{\mytmsyn} $
+}
+
+\mydesc{typing:}{ } {
+ \AxiomC{$\myjudd{\myctx; x : \mytya}{\mytmt}{\mytya}$}
+ \UnaryInfC{$\myjud{\myfix{x}{\mytya}{\mytmt}}{\mytya}$}
+ \DisplayProof
+}
+
+\mydesc{reduction:}{ }{
+ $ \myfix{x}{\mytya}{\mytmt} \myred \mysub{\mytmt}{x}{(\myfix{x}{\mytya}{\mytmt})}$
+}
+
+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}
+
+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 & ::= & \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}
+ $
+}
+
+\mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
+ \centering{
+ \begin{tabular}{cc}
+ $
+ \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}
+ }
+}
+
+\mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
+ \centering{
+ \begin{tabular}{cc}
+ \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
+ &
+ \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}
-\section{A more useful language}
+\section{Extending ITT}
\label{sec:practical}
-\section{Kant}
+\section{\mykant}
\label{sec:kant}
\appendix
\section{Notation and syntax}
-In the languages presented I will also use different fonts and colors for
-different things:
+Syntax, derivation rules, and reduction rules, are enclosed in frames describing
+the type of relation being established and the syntactic elements appearing,
+for example
+
+\mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
+ Typing derivations here.
+}
+
+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. \\
- $\myind{sans}$ & Data 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}
projects / bitonic-mengthesis.git / blobdiff