\renewcommand{\AgdaKeywordFontStyle}[1]{\ensuremath{\mathrm{\underline{#1}}}}
\renewcommand{\AgdaFunction}[1]{\textbf{\textcolor{AgdaFunction}{#1}}}
\renewcommand{\AgdaField}{\AgdaFunction}
-\definecolor{AgdaBound} {HTML}{000000}
+% \definecolor{AgdaBound} {HTML}{000000}
\definecolor{AgdaHole} {HTML} {FFFF33}
\DeclareUnicodeCharacter{9665}{\ensuremath{\lhd}}
\DeclareUnicodeCharacter{963}{\ensuremath{\sigma}}
\DeclareUnicodeCharacter{915}{\ensuremath{\Gamma}}
\DeclareUnicodeCharacter{8799}{\ensuremath{\stackrel{?}{=}}}
+\DeclareUnicodeCharacter{9655}{\ensuremath{\rhd}}
%% -----------------------------------------------------------------------------
\newcommand{\myfld}{\AgdaField}
\newcommand{\myfun}{\AgdaFunction}
% TODO make this use AgdaBound
-\newcommand{\myb}[1]{\ensuremath{#1}}
+\newcommand{\myb}[1]{\AgdaBound{#1}}
\newcommand{\myfield}{\AgdaField}
\newcommand{\myind}{\AgdaIndent}
\newcommand{\mykant}{\textsc{Kant}}
\newcommand{\mysynel}[1]{#1}
+\newcommand{\myse}{\mysynel}
\newcommand{\mytmsyn}{\mysynel{term}}
\newcommand{\mysp}{\ }
% TODO \mathbin or \mathre here?
\FrameSep0.2cm
\newcommand{\mydesc}[3]{
+ {\small
+ \vspace{0.3cm}
\hfill \textbf{#1} $#2$
- \vspace{-0.2cm}
+ \vspace{-0.3cm}
\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{\mytmt}{\mysynel{t}}
+\newcommand{\mytmm}{\mysynel{m}}
+\newcommand{\mytmn}{\mysynel{n}}
\newcommand{\myred}{\leadsto}
-\newcommand{\mysub}[3]{#1[#2 \mapsto #3]}
+\newcommand{\mysub}[3]{#1[#2 / #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{\mytya}{\myse{A}}
+\newcommand{\mytyb}{\myse{B}}
+\newcommand{\mytycc}{\myse{C}}
\newcommand{\myarr}{\mathrel{\textcolor{AgdaDatatype}{\to}}}
\newcommand{\myprod}{\mathrel{\textcolor{AgdaDatatype}{\times}}}
\newcommand{\myctx}{\Gamma}
\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{\mytt}{\mydc{$\langle\rangle$}}
\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{\myconst}{\myse{c}}
\newcommand{\myemptyctx}{\cdot}
\newcommand{\myhole}{\AgdaHole}
\newcommand{\myfix}[3]{\mysyn{fix} \myappsp #1 {:} #2 \mapsto #3}
\newcommand{\myneg}{\myfun{$\neg$}}
\newcommand{\myar}{\,}
\newcommand{\mybool}{\mytyc{Bool}}
+\newcommand{\mytrue}{\mydc{true}}
+\newcommand{\myfalse}{\mydc{false}}
+\newcommand{\myitee}[5]{\myfun{if}\,#1 / {#2.#3}\,\myfun{then}\,#4\,\myfun{else}\,#5}
\newcommand{\mynat}{\mytyc{$\mathbb{N}$}}
\newcommand{\myrat}{\mytyc{$\mathbb{R}$}}
-\newcommand{\myite}[3]{\mysyn{if}\,#1\,\mysyn{then}\,#2\,\mysyn{else}\,#3}
+\newcommand{\myite}[3]{\myfun{if}\,#1\,\myfun{then}\,#2\,\myfun{else}\,#3}
\newcommand{\myfora}[3]{(#1 {:} #2) \myarr #3}
-\newcommand{\myexi}[3]{(#1 {:} #2) \mysum #3}
+\newcommand{\myexi}[3]{(#1 {:} #2) \myprod #3}
+\newcommand{\mypairr}[4]{\mathopen{\mydc{$\langle$}}#1\mathpunct{\mydc{,}} #4\mathclose{\mydc{$\rangle$}}_{#2{.}#3}}
+\newcommand{\mylist}{\mytyc{List}}
+\newcommand{\mynil}[1]{\mydc{[]}_{#1}}
+\newcommand{\mycons}{\mathbin{\mydc{∷}}}
+\newcommand{\myfoldr}{\myfun{foldr}}
+\newcommand{\myw}[3]{\myapp{\myapp{\mytyc{W}}{(#1 {:} #2)}}{#3}}
+\newcommand{\mynode}[2]{\mathbin{\mydc{$\lhd$}_{#1.#2}}}
+\newcommand{\myrec}[4]{\myfun{rec}\,#1 / {#2.#3}\,\myfun{with}\,#4}
+\newcommand{\mylub}{\sqcup}
+\newcommand{\mydefeq}{\cong}
%% -----------------------------------------------------------------------------
principles described.
\end{abstract}
+\clearpage
+
\tableofcontents
+\clearpage
+
\section{Simple and not-so-simple types}
\label{sec:types}
$
}
-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} =
+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
\mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
$
\begin{array}{l}
- \myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{x}{\mytmn}\text{, where} \\
+ \myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{\myb{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}$}}
+ \mysub{\myb{x}}{\myb{x}}{\mytmn} & = & \mytmn \\
+ \mysub{\myb{y}}{\myb{x}}{\mytmn} & = & y\text{, with } \myb{x} \neq y \\
+ \mysub{(\myapp{\mytmt}{\mytmm})}{\myb{x}}{\mytmn} & = & (\myapp{\mysub{\mytmt}{\myb{x}}{\mytmn}}{\mysub{\mytmm}{\myb{x}}{\mytmn}}) \\
+ \mysub{(\myabs{\myb{x}}{\mytmm})}{\myb{x}}{\mytmn} & = & \myabs{\myb{x}}{\mytmm} \\
+ \mysub{(\myabs{\myb{y}}{\mytmm})}{\myb{x}}{\mytmn} & = & \myabs{\myb{z}}{\mysub{\mysub{\mytmm}{\myb{y}}{\myb{z}}}{\myb{x}}{\mytmn}}, \\
+ \multicolumn{3}{l}{\myind{1} \text{with $\myb{x} \neq \myb{y}$ and $\myb{z}$ not free in $\myapp{\mytmm}{\mytmn}$}}
\end{array}
\end{array}
$
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}.
+of this idea takes the name of \emph{simply typed $\lambda$ calculus}, whose
+rules are shown in figure \ref{fig:stlc}.
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
$\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}
+\begin{figure}[t]
+ \mydesc{syntax}{ }{
+ $
+ \begin{array}{r@{\ }c@{\ }l}
+ \mytmsyn & ::= & \myb{x} \mysynsep \myabss{\myb{x}}{\mytysyn}{\mytmsyn} \mysynsep
+ (\myapp{\mytmsyn}{\mytmsyn}) \\
+ \mytysyn & ::= & \myse{\phi} \mysynsep \mytysyn \myarr \mytysyn \mysynsep \\
+ \myb{x} & \in & \text{Some enumerable set of symbols} \\
+ \myse{\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}
+ }
}
+ \caption{Syntax and typing rules for the STLC. Reduction is unchanged from
+ the untyped $\lambda$-calculus.}
+ \label{fig:stlc}
+\end{figure}
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
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.
+ resulting term is also well-typed, and preserves the previous type. Also
+ known as \emph{subject reduction}.
\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}})}
+ \myapp{(\myabss{\myb{x}}{\myhole{?}}{\myapp{\myb{x}}{\myb{x}}})}{(\myabss{\myb{x}}{\myhole{?}}{\myapp{\myb{x}}{\myb{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
-
+\noindent
+\begin{minipage}{0.5\textwidth}
\mydesc{syntax}{ } {
- $ \mytmsyn ::= \dotsb \mysynsep \myfix{x}{\mytysyn}{\mytmsyn} $
+ $ \mytmsyn ::= \dotsb \mysynsep \myfix{\myb{x}}{\mytysyn}{\mytmsyn} $
+ \vspace{0.4cm}
}
-
-\mydesc{typing:}{ } {
- \AxiomC{$\myjudd{\myctx; x : \mytya}{\mytmt}{\mytya}$}
- \UnaryInfC{$\myjud{\myfix{x}{\mytya}{\mytmt}}{\mytya}$}
- \DisplayProof
+\end{minipage}
+\begin{minipage}{0.5\textwidth}
+\mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}} {
+ \centering{
+ \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytmt}{\mytya}$}
+ \UnaryInfC{$\myjud{\myfix{\myb{x}}{\mytya}{\mytmt}}{\mytya}$}
+ \DisplayProof
+ }
}
+\end{minipage}
-\mydesc{reduction:}{ }{
- $ \myfix{x}{\mytya}{\mytmt} \myred \mysub{\mytmt}{x}{(\myfix{x}{\mytya}{\mytmt})}$
+\mydesc{reduction:}{\myjud{\mytmsyn}{\mytmsyn}}{
+ \centering{
+ $ \myfix{\myb{x}}{\mytya}{\mytmt} \myred \mysub{\mytmt}{\myb{x}}{(\myfix{\myb{x}}{\mytya}{\mytmt})}$
+ }
}
This will deprive us of normalisation, which is a particularly bad thing if we
\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})}}}}
+ \myabss{\myb{f}}{(\mytya \myarr \mytyb)}{\myabss{\myb{g}}{(\mytyb \myarr \mytycc)}{\myabss{\myb{x}}{\mytya}{\myapp{\myb{g}}{(\myapp{\myb{f}}{\myb{x}})}}}}
\]
-That is, function composition. We can extend our bare lambda calculus with
-useful types to represent other logical constructs.
+That is, function composition. Going beyond arrow types, we can extend our bare
+lambda calculus with useful types to represent other logical constructs, as
+shown in figure \ref{fig:natded}.
+\begin{figure}[t]
\mydesc{syntax}{ }{
$
\begin{array}{r@{\ }c@{\ }l}
\mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
\centering{
\begin{tabular}{cc}
- \AxiomC{}
+ \AxiomC{\phantom{$\myjud{\mytmt}{\myempty}$}}
\UnaryInfC{$\myjud{\mytt}{\myunit}$}
\DisplayProof
&
\end{tabular}
}
}
+\caption{Rules for the extendend STLC. Only the new features are shown, all the
+ rules and syntax for the STLC apply here too.}
+ \label{fig:natded}
+\end{figure}
Tagged unions (or sums, or coproducts---$\mysum$ here, \texttt{Either} in
Haskell) correspond to disjunctions, and dually tuples (or pairs, or
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 foundation of the STLC\footnote{There is research to give computational
behaviour to classical logic, but I will not touch those subjects.}.
+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 $\mysyn{fix}$ combinator, it is easy to see how it ruins our
+desire for consistency. The following term works for every type $\mytya$,
+including bottom:
+\[
+(\myfix{\myb{x}}{\mytya}{\myb{x}}) : \mytya
+\]
+
+\subsection{Inductive data}
+
+To make the STLC more useful as a programming language or reasoning tool it is
+common to include (or let the user define) inductive data types. These comprise
+of a type former, various constructors, and an eliminator (or destructor) that
+serves as primitive recursor.
+
+For example, we might add a $\mylist$ type constructor, along with an `empty
+list' ($\mynil{ }$) and `cons cell' ($\mycons$) constructor. The eliminator for
+lists will be the usual folding operation ($\myfoldr$). See figure
+\ref{fig:list}.
+
+\begin{figure}[h]
+\mydesc{syntax}{ }{
+ $
+ \begin{array}{r@{\ }c@{\ }l}
+ \mytmsyn & ::= & \dots \mysynsep \mynil{\mytysyn} \mysynsep \mytmsyn \mycons \mytmsyn
+ \mysynsep
+ \myapp{\myapp{\myapp{\myfoldr}{\mytmsyn}}{\mytmsyn}}{\mytmsyn} \\
+ \mytysyn & ::= & \dots \mysynsep \myapp{\mylist}{\mytysyn}
+ \end{array}
+ $
+}
+\mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
+ \centering{
+ $
+ \begin{array}{l@{\ }c@{\ }l}
+ \myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{\mynil{\mytya}} & \myred & \mytmt \\
+
+ \myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{(\mytmm \mycons \mytmn)} & \myred &
+ \myapp{\myapp{\myse{f}}{\mytmm}}{(\myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{\mytmn})}
+ \end{array}
+ $
+}
+}
+\mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
+ \centering{
+ \begin{tabular}{cc}
+ \AxiomC{\phantom{$\myjud{\mytmm}{\mytya}$}}
+ \UnaryInfC{$\myjud{\mynil{\mytya}}{\myapp{\mylist}{\mytya}}$}
+ \DisplayProof
+ &
+ \AxiomC{$\myjud{\mytmm}{\mytya}$}
+ \AxiomC{$\myjud{\mytmn}{\myapp{\mylist}{\mytya}}$}
+ \BinaryInfC{$\myjud{\mytmm \mycons \mytmn}{\myapp{\mylist}{\mytya}}$}
+ \DisplayProof
+ \end{tabular}
+ }
+ \myderivsp
+ \centering{
+ \AxiomC{$\myjud{\mysynel{f}}{\mytya \myarr \mytyb \myarr \mytyb}$}
+ \AxiomC{$\myjud{\mytmm}{\mytyb}$}
+ \AxiomC{$\myjud{\mytmn}{\myapp{\mylist}{\mytya}}$}
+ \TrinaryInfC{$\myjud{\myapp{\myapp{\myapp{\myfoldr}{\mysynel{f}}}{\mytmm}}{\mytmn}}{\mytyb}$}
+ \DisplayProof
+ }
+}
+\caption{Rules for lists in the STLC.}
+\label{fig:list}
+\end{figure}
+
+In section \ref{sec:well-order} we will see how to give a general account of
+inductive data. %TODO does this make sense to have here?
\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:
+succinctly expressed geometrically how we can add expressivity:
$$
\xymatrix@!0@=1.5cm{
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
+ types in our type signatures. For example, we can define 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
+ \[\displaystyle
+ (\myabss{\myb{A}}{\mytyp}{\myabss{\myb{x}}{\myb{A}}{\myb{x}}}) : (\myb{A} : \mytyp) \myarr \myb{A} \myarr \myb{A}
+ \]
+ The first and most famous instance of this idea has been System F. This 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$.
+ continuation passing style: \[\displaystyle(\myabss{\myb{A} \myar \myb{R}}{\mytyp}{(\myb{A}
+ \myarr \myb{R}) \myarr \myb{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$.
+ \[\displaystyle(\myabss{\myb{x}}{\mybool}{\myite{\myb{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'.
+`$\lambda$-cube'. It will serve as the logical `core' of all the other
+extensions that we will present and ultimately our implementation of a similar
+logic.
\subsection{A Bit of History}
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
+ $\mytyp$ and $\mytyp : \mytyp$, see section \ref{sec:term-types} for an
explanation on why this causes problems.}. For this reason he gave a revised
and consistent definition later \citep{Martin-Lof1984}.
normalising. \cite{Coquand1986} further extended this line of work with the
Calculus of Constructions (CoC).
-\subsection{A core type theory}
+\subsection{A simple 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}.
+\citep{Martin-Lof1984}. The system's syntax and reduction rules are presented
+in their entirety in figure \ref{fig:core-tt-syn}. The typing rules are
+presented piece by piece. An Agda rendition of the presented theory is
+reproduced in appendix \ref{app:agda-code}.
+\begin{figure}[t]
\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}
+ \mytmsyn & ::= & \myb{x} \mysynsep
+ \mytyp_{l} \mysynsep
+ \myunit \mysynsep \mytt \mysynsep
+ \myempty \mysynsep \myapp{\myabsurd{\mytmsyn}}{\mytmsyn} \\
+ & | & \mybool \mysynsep \mytrue \mysynsep \myfalse \mysynsep
+ \myitee{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
+ & | & \myfora{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
+ \myabss{\myb{x}}{\mytmsyn}{\mytmsyn} \\
+ & | & \myexi{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
+ \mypairr{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn} \\
+ & | & \myapp{\myfst}{\mytmsyn} \mysynsep \myapp{\mysnd}{\mytmsyn} \\
+ & | & \myw{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
+ \mytmsyn \mynode{\myb{x}}{\mytmsyn} \mytmsyn \\
+ & | & \myrec{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn} \\
+ l & \in & \mathbb{N}
\end{array}
$
}
\mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
+ \centering{
+ \begin{tabular}{cc}
+ $
+ \begin{array}{l@{ }l@{\ }c@{\ }l}
+ \myitee{\mytrue &}{\myb{x}}{\myse{P}}{\mytmm}{\mytmn} & \myred & \mytmm \\
+ \myitee{\myfalse &}{\myb{x}}{\myse{P}}{\mytmm}{\mytmn} & \myred & \mytmn \\
+ \end{array}
+ $
+ &
+ $
+ \myapp{(\myabss{\myb{x}}{\mytya}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{\myb{x}}{\mytmn}
+ $
+ \myderivsp
+ \end{tabular}
+ $
+ \begin{array}{l@{ }l@{\ }c@{\ }l}
+ \myapp{\myfst &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmm \\
+ \myapp{\mysnd &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmn
+ \end{array}
+ $
+ \myderivsp
+
+ $
+ \myrec{(\myse{s} \mynode{\myb{x}}{\myse{T}} \myse{f})}{\myb{y}}{\myse{P}}{\myse{p}} \myred
+ \myapp{\myapp{\myapp{\myse{p}}{\myse{s}}}{\myse{f}}}{(\myabss{\myb{t}}{\mysub{\myse{T}}{\myb{x}}{\myse{s}}}{
+ \myrec{\myapp{\myse{f}}{\myb{t}}}{\myb{y}}{\myse{P}}{\mytmt}
+ })}
+ $
+ }
+}
+\caption{Syntax and reduction rules for our type theory.}
+\label{fig:core-tt-syn}
+\end{figure}
+
+\subsubsection{Types are terms, some terms are types}
+\label{sec:term-types}
+
+\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
+ \centering{
+ \begin{tabular}{cc}
+ \AxiomC{$\myjud{\mytmt}{\mytya}$}
+ \AxiomC{$\mytya \mydefeq \mytyb$}
+ \BinaryInfC{$\myjud{\mytmt}{\mytyb}$}
+ \DisplayProof
+ &
+ \AxiomC{\phantom{$\myjud{\mytmt}{\mytya}$}}
+ \UnaryInfC{$\myjud{\mytyp_l}{\mytyp_{l + 1}}$}
+ \DisplayProof
+ \end{tabular}
+ }
+}
+
+The first thing to notice is that a barrier between values and types that we had
+in the STLC is gone: values can appear in types, and the two are treated
+uniformly in the syntax.
+
+While the usefulness of doing this will become clear soon, a consequence is that
+since types can be the result of computation, deciding type equality is not
+immediate as in the STLC. For this reason we define \emph{definitional
+ equality}, $\mydefeq$, as the congruence relation extending $\myred$. Types
+that are definitionally equal can be used interchangeably. Here the
+`conversion' rule is not syntax directed, however we will see how it is possible
+to employ $\myred$ to decide term equality in a systematic way. % TODO add section
+Another thing to notice is that considering the need to reduce terms to decide
+equality, it is essential for a dependently type system to be terminating and
+confluent for type checking to be decidable.
+
+Moreover, we specify a \emph{type hierarchy} to talk about `large' types:
+$\mytyp_0$ will be the type of types inhabited by data: $\mybool$, $\mynat$,
+$\mylist$, etc. $\mytyp_1$ will be the type of $\mytyp_0$, and so on---for
+example we have $\mytrue : \mybool : \mytyp_0 : \mytyp_1 : \dots$. Each type
+`level' is often called a universe in the literature. While it is possible, to
+simplify things by having only one universe $\mytyp$ with $\mytyp : \mytyp$,
+this plan is inconsistent for much the same reason that impredicative na\"{\i}ve
+set theory is \citep{Hurkens1995}. Moreover, various techniques can be employed
+to lift the burden of explicitly handling universes.
+% TODO add sectioon about universes
+
+\subsubsection{Contexts}
+
+\begin{minipage}{0.5\textwidth}
+ \mydesc{context validity:}{\myvalid{\myctx}}{
+ \centering{
+ \begin{tabular}{cc}
+ \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
+ \UnaryInfC{$\myvalid{\myemptyctx}$}
+ \DisplayProof
+ &
+ \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
+ \UnaryInfC{$\myvalid{\myctx ; \myb{x} : \mytya}$}
+ \DisplayProof
+ \end{tabular}
+ }
+ }
+\end{minipage}
+\begin{minipage}{0.5\textwidth}
+ \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
+ \centering{
+ \AxiomC{$\myctx(x) = \mytya$}
+ \UnaryInfC{$\myjud{\myb{x}}{\mytya}$}
+ \DisplayProof
+ }
+ }
+\end{minipage}
+\vspace{0.1cm}
+
+We need to refine the notion context to make sure that every variable appearing
+is typed correctly, or that in other words each type appearing in the context is
+indeed a type and not a value. In every other rule, if no premises are present,
+we assume the context in the conclusion to be valid.
+
+Then we can re-introduce the old rule to get the type of a variable for a
+context.
+
+\subsubsection{$\myunit$, $\myempty$}
+
+\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
+ \centering{
+ \begin{tabular}{ccc}
+ \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
+ \UnaryInfC{$\myjud{\myunit}{\mytyp_0}$}
+ \noLine
+ \UnaryInfC{$\myjud{\myempty}{\mytyp_0}$}
+ \DisplayProof
+ &
+ \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
+ \UnaryInfC{$\myjud{\mytt}{\myunit}$}
+ \noLine
+ \UnaryInfC{\phantom{$\myjud{\myempty}{\mytyp_0}$}}
+ \DisplayProof
+ &
+ \AxiomC{$\myjud{\mytmt}{\myempty}$}
+ \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
+ \BinaryInfC{$\myjud{\myapp{\myabsurd{\mytya}}{\mytmt}}{\mytya}$}
+ \noLine
+ \UnaryInfC{\phantom{$\myjud{\myempty}{\mytyp_0}$}}
+ \DisplayProof
+ \end{tabular}
+ }
+}
+
+Nothing surprising here: $\myunit$ and $\myempty$ are unchanged from the STLC,
+with the added rules to type $\myunit$ and $\myempty$ themselves, and to make
+sure that we are invoking $\myabsurd{}$ over a type.
+
+\subsubsection{$\mybool$, and dependent $\myfun{if}$}
+
+\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
+ \centering{
+ \begin{tabular}{ccc}
+ \AxiomC{}
+ \UnaryInfC{$\myjud{\mybool}{\mytyp_0}$}
+ \DisplayProof
+ &
+ \AxiomC{}
+ \UnaryInfC{$\myjud{\mytrue}{\mybool}$}
+ \DisplayProof
+ &
+ \AxiomC{}
+ \UnaryInfC{$\myjud{\myfalse}{\mybool}$}
+ \DisplayProof
+ \end{tabular}
+ \myderivsp
+
+ \AxiomC{$\myjud{\mytmt}{\mybool}$}
+ \AxiomC{$\myjudd{\myctx : \mybool}{\mytya}{\mytyp_l}$}
+ \noLine
+ \BinaryInfC{$\myjud{\mytmm}{\mysub{\mytya}{x}{\mytrue}}$ \hspace{0.7cm} $\myjud{\mytmn}{\mysub{\mytya}{x}{\myfalse}}$}
+ \UnaryInfC{$\myjud{\myitee{\mytmt}{\myb{x}}{\mytya}{\mytmm}{\mytmn}}{\mysub{\mytya}{\myb{x}}{\mytmt}}$}
+ \DisplayProof
+
+ }
+}
+With booleans we get the first taste of `dependent' in `dependent types'. While
+the two introduction rules ($\mytrue$ and $\myfalse$) are not surprising, the
+typing rules for $\myfun{if}$ are. In most strongly typed languages we expect
+the branches of an $\myfun{if}$ statements to be of the same type, to preserve
+subject reduction, since execution could take both paths. This is a pity, since
+the type system does not reflect the fact that in each branch we gain knowledge
+on the term we are branching on. Which means that programs along the lines of
+\begin{verbatim}
+if null xs then head xs else 0
+\end{verbatim}
+are a necessary, well typed, danger.
+
+However, in a more expressive system, we can do better: the branches' type can
+depend on the value of the scrutinised boolean. This is what the typing rule
+expresses: the user provides a type $\mytya$ ranging over an $\myb{x}$
+representing the scrutinised boolean type, and the branches are typechecked with
+the updated knowledge on the value of $\myb{x}$.
+
+\subsubsection{$\myarr$, or dependent function}
+
+ \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
+ \centering{
+ \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
+ \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
+ \BinaryInfC{$\myjud{\myfora{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
+ \DisplayProof
+
+ \myderivsp
+
+ \begin{tabular}{cc}
+ \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytmt}{\mytyb}$}
+ \UnaryInfC{$\myjud{\myabss{\myb{x}}{\mytya}{\mytmt}}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
+ \DisplayProof
+ &
+ \AxiomC{$\myjud{\mytmm}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
+ \AxiomC{$\myjud{\mytmn}{\mytya}$}
+ \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mysub{\mytyb}{\myb{x}}{\mytmn}}$}
+ \DisplayProof
+ \end{tabular}
+ }
}
+Dependent functions are one of the two key features that perhaps most
+characterise dependent types---the other being dependent products. With
+dependent functions, the result type can depend on the value of the argument.
+This feature, together with the fact that the result type might be a type
+itself, brings a lot of interesting possibilities. Keeping the correspondence
+with logic alive, dependent functions are much like universal quantifiers
+($\forall$) in logic.
+
+Again, we need to make sure that the type hierarchy is respected, which is the
+reason why a type formed by $\myarr$ will live in the least upper bound of the
+levels of argument and return type. This trend will continue with the other
+type-level binders, $\myprod$ and $\mytyc{W}$.
+
+% TODO maybe examples?
+
+\subsubsection{$\myprod$, or dependent product}
+
+
\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
+ \centering{
+ \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
+ \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
+ \BinaryInfC{$\myjud{\myexi{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
+ \DisplayProof
+
+ \myderivsp
+
+ \begin{tabular}{cc}
+ \AxiomC{$\myjud{\mytmm}{\mytya}$}
+ \AxiomC{$\myjud{\mytmn}{\mysub{\mytyb}{\myb{x}}{\mytmm}}$}
+ \BinaryInfC{$\myjud{\mypairr{\mytmm}{\myb{x}}{\mytyb}{\mytmn}}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
+ \noLine
+ \UnaryInfC{\phantom{$--$}}
+ \DisplayProof
+ &
+ \AxiomC{$\myjud{\mytmt}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
+ \UnaryInfC{$\hspace{0.7cm}\myjud{\myapp{\myfst}{\mytmt}}{\mytya}\hspace{0.7cm}$}
+ \noLine
+ \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mysub{\mytyb}{\myb{x}}{\myapp{\myfst}{\mytmt}}}$}
+ \DisplayProof
+ \end{tabular}
+
+ }
+}
+
+
+\subsubsection{$\mytyc{W}$, or well-order}
+\label{sec:well-order}
+\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
+ \centering{
+ \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
+ \AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
+ \BinaryInfC{$\myjud{\myw{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
+ \DisplayProof
+
+ \myderivsp
+
+ \AxiomC{$\myjud{\mytmt}{\mytya}$}
+ \AxiomC{$\myjud{\mysynel{f}}{\mysub{\mytyb}{\myb{x}}{\mytmt} \myarr \myw{\myb{x}}{\mytya}{\mytyb}}$}
+ \BinaryInfC{$\myjud{\mytmt \mynode{\myb{x}}{\mytyb} \myse{f}}{\myw{\myb{x}}{\mytya}{\mytyb}}$}
+ \DisplayProof
+
+ \myderivsp
+
+ \AxiomC{$\myjud{\myse{u}}{\myw{\myb{x}}{\myse{S}}{\myse{T}}}$}
+ \AxiomC{$\myjudd{\myctx; \myb{w} : \myw{\myb{x}}{\myse{S}}{\myse{T}}}{\myse{P}}{\mytyp_l}$}
+ \noLine
+ \BinaryInfC{$\myjud{\myse{p}}{
+ \myfora{\myb{s}}{\myse{S}}{\myfora{\myb{f}}{\mysub{\myse{T}}{\myb{x}}{\myse{s}} \myarr \myw{\myb{x}}{\myse{S}}{\myse{T}}}{(\myfora{\myb{t}}{\mysub{\myse{T}}{\myb{x}}{\myb{s}}}{\mysub{\myse{P}}{\myb{w}}{\myapp{\myb{f}}{\myb{t}}}}) \myarr \mysub{\myse{P}}{\myb{w}}{\myb{f}}}}
+ }$}
+ \UnaryInfC{$\myjud{\myrec{\myse{u}}{\myb{w}}{\myse{P}}{\myse{p}}}{\mysub{\myse{P}}{\myb{w}}{\myse{u}}}$}
+ \DisplayProof
+ }
}
+
\section{The struggle for equality}
\label{sec:equality}
-\section{Extending ITT}
+\subsection{Propositional equality...}
+
+\subsection{...and its limitations}
+
+eta law
+
+congruence
+
+UIP
+
+\subsection{Equality reflection}
+
+\subsection{Observational equality}
+
+\subsection{Univalence foundations}
+
+\section{Augmenting ITT}
\label{sec:practical}
+\subsection{A more liberal hierarchy}
+
+\subsection{Type inference}
+
+\subsubsection{Bidirectional type checking}
+
+\subsubsection{Pattern unification}
+
+\subsection{Pattern matching and explicit fixpoints}
+
+\subsection{Induction-recursion}
+
+\subsection{Coinduction}
+
+\subsection{Dealing with partiality}
+
+\subsection{Type holes}
+
\section{\mykant}
\label{sec:kant}
+
\appendix
\section{Notation and syntax}
Typing derivations here.
}
-In the languages presented I also highlight the syntax, following a uniform
-color and font convention:
+In the languages presented and Agda code samples 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. \\
+ $\mytyc{Sans}$ & Type constructors. \\
+ $\mydc{sans}$ & Data constructors. \\
% $\myfld{sans}$ & Field accessors (e.g. \myfld{fst} and \myfld{snd} for products). \\
- $\mysyn{roman}$ & Keywords of the language. \\
- $\myfun{roman}$ & Defined values and destructors. \\
- $\myb{math}$ & Bound variables.
+ $\mysyn{roman}$ & Keywords of the language. \\
+ $\myfun{roman}$ & Defined values and destructors. \\
+ $\myb{math}$ & Bound variables.
\end{tabular}
\end{center}
-\section{Agda code}
+Moreover, I will from time to time give examples in the Haskell programming
+language as defined in \citep{Haskell2010}, which I will typeset in
+\texttt{teletype} font. I assume that the reader is already familiar with
+Haskell, plenty of good introductions are available \citep{LYAH,ProgInHask}.
+
+When presenting grammars, I will use a word in $\mysynel{math}$ font
+(e.g. $\mytmsyn$ or $\mytysyn$) to indicate indicate nonterminals. Additionally,
+I will use quite flexibly a $\mysynel{math}$ font to indicate a syntactic
+element. More specifically, terms are usually indicated by lowercase letters
+(often $\mytmt$, $\mytmm$, or $\mytmn$); and types by an uppercase letter (often
+$\mytya$, $\mytyb$, or $\mytycc$).
+
+When presenting type derivations, I will often abbreviate and present multiple
+conclusions, each on a separate line:
+
+\begin{prooftree}
+ \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
+ \UnaryInfC{$\myjud{\myapp{\myfst}{\mytmt}}{\mytya}$}
+ \noLine
+ \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mytyb}$}
+\end{prooftree}
+
+\section{Agda rendition of core ITT}
\label{app:agda-code}
-\subsection{ITT}
-
\begin{code}
module ITT where
open import Level
projects / bitonic-mengthesis.git / commitdiff