+Here we encode natural numbers through $\mathsf{W}$ types. Each node contains a
+$\lcbool$. If the $\lcbool$ is $\lcfalse$, then there are no children, since we
+have a function $\bot \tyarr \mathsf{Nat}$: this is our $0$. If it's $\lctrue$,
+we need one child only: the predecessor. Similarly, we recurse giving to
+$\lcsyn{rec}$ a function that handles the `base case' 0 when the $\lcbool$ is
+$\lctrue$, and the inductive case otherwise.
+
+We postpone more complex examples after the introduction of inductive families
+and pattern matching, since $\mathsf{W}$ types get unwieldy very quickly.
+
+\subsubsection{Propositional Equality}
+
+We can finally introduce one of the central subjects of my project:
+propositional equality.
+
+\newcommand{\lceq}[3]{#2 =_{#1} #3}
+\newcommand{\lceqz}[2]{#1 = #2}
+\newcommand{\lcrefl}[2]{\mathsf{refl}_{#1}\appsp #2}
+\newcommand{\lcsubst}[3]{\mathsf{subst}\appsp#1\appsp#2\appsp#3}
+
+\begin{center}
+ \axname{syntax}
+ \begin{eqnarray*}
+ \termsyn & ::= & ... \\
+ & | & \lceq{\termsyn}{\termsyn}{\termsyn} \separ \lcrefl{\termsyn}{\termsyn} \separ \lcsubst{\termsyn}{\termsyn}{\termsyn}
+ \end{eqnarray*}
+
+ \axdesc{typing}{\Gamma \vdash \termsyn : \termsyn}
+
+ \vspace{0.5cm}
+
+ \begin{tabular}{c c}
+ \AxiomC{$\Gamma \vdash \termt : \tya$}
+ \UnaryInfC{$\Gamma \vdash \lcrefl{\tya}{\termt} : \lceq{\tya}{\termt}{\termt}$}
+ \DisplayProof
+ &
+ \AxiomC{$\Gamma \vdash \termp : \lceq{\tya}{\termt}{\termm}$}
+ \AxiomC{$\Gamma \vdash \tyb : \tya \tyarr \lcsetz$}
+ \AxiomC{$\Gamma \vdash \termn : \app{\tyb}{\termt}$}
+ \TrinaryInfC{$\Gamma \vdash \lcsubst{\termp}{\tyb}{\termn} : \app{\tyb}{\termm}$}
+ \DisplayProof
+ \end{tabular}
+
+ \vspace{0.5cm}
+
+ \axdesc{reduction}{\termsyn \bred \termsyn}
+ \begin{eqnarray*}
+ \lcsubst{(\lcrefl{\tya}{\termt})}{\tyb}{\termm} \bred \termm
+ \end{eqnarray*}
+\end{center}
+
+Propositional equality internalises equality as a type. This lets us prove
+useful things. The only way to introduce an equality proof is by reflexivity
+($\mathsf{refl}$). The eliminator is in the style of `Leibnitz's law' of
+equality: `equals can be substituted for equals' ($\mathsf{subst}$). The
+computation rule refers to the fact that every canonical proof of equality will
+be a $\mathsf{refl}$. We can use $\neg (\lceq{\tya}{x}{y})$ to express
+inequality.
+
+These elements conclude our presentation of a `core' type theory. For an
+extended example see Section 6.2 of \cite{Thompson1991}\footnote{Note that while I
+ attempted to formalise the proof in Agda, I found a bug in the book! See the
+ errata for details:
+ \url{http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/errata.html}.}. The above
+language and examples have been codified in Agda\footnote{More on Agda in
+ the next section.}, see appendix \ref{app:agda-code}.
+
+\section{A more useful language}
+
+While our core type theory equipped with $\mathsf{W}$ types is very usefully
+conceptually as a simple but complete language, things get messy very fast. In
+this section we will present the elements that are usually include in theorem
+provers or programming languages to make them usable by mathematicians or
+programmers.
+
+All the features presented, except for quotient types, are present in the second
+version of the Agda system, which is described in the PhD thesis of the author
+\citep{Norell2007}. Agda follows a tradition of theorem provers based on ITT
+with inductive families and pattern matching. The closest relative of Agda,
+apart from previous versions, is Epigram, whose type theory is described in
+\cite{McBride2004}. Coq is another notable theorem prover based on the same
+concepts, and the first and most popular \cite{Coq}.
+
+The main difference between Coq and Agda/Epigram is that the former focuses on
+theorem proving, while the latter also want to be useful as functional
+programming languages, while still offering good tools to express
+mathematics\footnote{In fact, currently, Agda is used almost exclusively to
+ express mathematics, rather than to program.}. This is reflected in a series
+of differences that I will not discuss here (most notably the absence of tactics
+but better support for pattern matching in Agda/Epigram). I will take the same
+approach as Agda/Epigram and will give a perspective focused on functional
+programming rather than theorem proving. Every feature will be presented as it
+is present in Agda (if possible, since some features are not present in Agda
+yet).
+
+\subsection{Inductive families}
+
+\newcommand{\lcdata}[1]{\lcsyn{data}\appsp #1}
+\newcommand{\lcdb}{\ |\ }
+\newcommand{\lcind}{\hspace{0.2cm}}
+\newcommand{\lcwhere}{\appsp \lcsyn{where}}
+\newcommand{\lclist}[1]{\app{\mathsf{List}}{#1}}
+\newcommand{\lcnat}{\app{\mathsf{Nat}}}
+\newcommand{\lcvec}[2]{\app{\app{\mathsf{Vec}}{#1}}{#2}}
+
+Inductive families were first introduced by \cite{Dybjer1991}. For the reader
+familiar with the recent developments present in the GHC compiler for Haskell,
+inductive families will look similar to GADTs (Generalised Abstract Data Types).
+% TODO: add citation
+Haskell style data types provide \emph{parametric polymorphism}, so that we can
+define types that range over type parameters:
+\[
+\begin{array}{l}
+\lcdata{\lclist{A}} = \mathsf{Nil} \lcdb A :: \lclist{A}
+\end{array}
+\]
+In this way we define the $\mathsf{List}$ type once while allowing elements to
+be of any type. $\mathsf{List}$ will be a type constructor of type $\lcsetz
+\tyarr \lcsetz$, while $\mathsf{nil} : \lcforall{A}{\lcsetz}{\lclist{A}}$ and
+$\_::\_ : \lcforall{A}{\lcsetz}{A \tyarr \lclist{A} \tyarr \lclist{A}}$.
+
+Inductive families bring this concept one step further by allowing some of the
+parameters to be constrained in constructors. We call these parameters
+`indices'. For example we might define natural numbers
+\[
+\begin{array}{l}
+\lcdata{\lcnat} : \lcsetz \lcwhere \\
+ \begin{array}{l@{\ }l}
+ \lcind \mathsf{zero} &: \lcnat \\
+ \lcind \mathsf{suc} &: \lcnat \tyarr \lcnat
+ \end{array}
+\end{array}
+\]
+And then define a type for lists indexed by length:
+\[
+\begin{array}{l}
+\lcdata{\mathsf{Vec}}\appsp (A : \lcsetz) : \lcnat \tyarr \lcsetz \lcwhere \\
+ \begin{array}{l@{\ }l}
+ \lcind \mathsf{nil} &: \lcvec{A}{\mathsf{zero}} \\
+ \lcind \_::\_ &: \{n : \mathsf{Nat}\} \tyarr A \tyarr \lcvec{A}{n} \tyarr \lcvec{A}{\app{(\mathsf{suc}}{n})}
+ \end{array}
+\end{array}
+\]
+Note that contrary to the Haskell ADT notation, with inductive families we
+explicitly list the types for the type constructor and data constructors. In
+$\mathsf{Vec}$, $A$ is a parameter (same across all constructors) while the
+$\lcnat$ is an integer. In our syntax, in the $\lcsyn{data}$ declaration,
+things to the left of the colon are parameters, while on the right we can define
+the type of indices. Also note that the parameters can be named across all
+constructors, while indices can't.
+
+In this $\mathsf{Vec}$ example, when we form a new list the length is
+$\mathsf{zero}$. When we append a new element to an existing list of length
+$n$, the new list is of length $\app{\mathsf{suc}}{n}$, that is, one more than
+the previous length. Also note that we are using the $\{n : \lcnat\} \tyarr
+\dotsb$ syntax to indicate an argument that we will omit when using $\_::\_$.
+In the future I shall also omit the type of these implicit parameters, in line
+how Agda works.
+
+Once we have our $\mathsf{Vec}$ we can do things much more safely than with
+normal lists. For example, we can define an $\mathsf{head}$ function that
+returns the first element of the list:
+\[
+\begin{array}{l}
+\mathsf{head} : \{A\ n\} \tyarr \lcvec{A}{(\app{\mathsf{suc}}{n})} \tyarr A
+\end{array}
+\]
+Note that we will not be able to provide this function with a
+$\lcvec{A}{\mathsf{zero}}$, since it needs an index which is a successor of some
+number.
+
+\newcommand{\lcfin}[1]{\app{\mathsf{Fin}}{#1}}
+
+If we wish to index a $\mathsf{Vec}$ safely, we can define an inductive family
+$\lcfin{n}$, which represents the family of numbers smaller than a given number
+$n$:
+\[
+\begin{array}{l}
+ \lcdata{\mathsf{Fin}} : \lcnat \tyarr \lcsetz \lcwhere \\
+ \begin{array}{l@{\ }l}
+ \lcind \mathsf{fzero} &: \{n\} \tyarr \lcfin{n} \\
+ \lcind \mathsf{fsuc} &: \{n\} \tyarr (i : \lcfin{n}) \tyarr \lcfin{(\app{\mathsf{suc}}{n})}
+ \end{array}
+\end{array}
+\]
+$\mathsf{fzero}$ is smaller than any number apart from $\mathsf{zero}$. Given
+the family of numbers smaller than $i$, we can produce the family of numbers
+smaller than $\app{\mathsf{suc}}{n}$. Now we can define an `indexing' operation
+for our $\mathsf{Vec}$:
+\[
+\begin{array}{l}
+\_\mathsf{!!}\_ : \{A\ n\} \tyarr \lcvec{A}{n} \tyarr \lcfin{n} \tyarr A
+\end{array}
+\]
+In this way we will be sure that the number provided as an index will be smaller
+than the length of the $\mathsf{Vec}$ provided.
+
+
+\subsection{Pattern matching}
+
+\subsection{Guarded recursion}
+
+\subsection{Corecursion}
+
+\subsection{Quotient types}
+
+
+\section{Why dependent types?}
+
+\section{Many equalities}
+
+\subsection{Revision}
+
+\subsection{Extensional equality and its problems}
+
+\subsection{Observational equality}
+
+\section{What to do}
+
projects / bitonic-mengthesis.git / commitdiff