-\documentclass[report, 11pt]{article}
+\documentclass[11pt, fleqn]{article}
\usepackage{etex}
\usepackage[sc,slantedGreek]{mathpazo}
-\linespread{1.05}
+% \linespread{1.05}
% \usepackage{times}
\oddsidemargin 0in
\textheight 9.5in
\textwidth 6.2in
\topmargin -7mm
-\parindent 10pt
+%% \parindent 10pt
+
+\headheight 0pt
+\headsep 0pt
%% Narrow margins
\usepackage{subcaption}
\usepackage{verbatim}
+\usepackage{fancyvrb}
+
+\RecustomVerbatimEnvironment
+ {Verbatim}{Verbatim}
+ {xleftmargin=9mm}
%% diagrams
\usepackage{tikz}
\newcommand{\myb}[1]{\AgdaBound{$#1$}}
\newcommand{\myfield}{\AgdaField}
\newcommand{\myind}{\AgdaIndent}
-\newcommand{\mykant}{\textsc{Kant}}
+\newcommand{\mykant}{\textsc{Bertus}}
\newcommand{\mysynel}[1]{#1}
\newcommand{\myse}{\mysynel}
\newcommand{\mytmsyn}{\mysynel{term}}
\newcommand{\myfst}{\myfld{fst}}
\newcommand{\mysnd}{\myfld{snd}}
\newcommand{\myconst}{\myse{c}}
-\newcommand{\myemptyctx}{\cdot}
+\newcommand{\myemptyctx}{\varepsilon}
\newcommand{\myhole}{\AgdaHole}
\newcommand{\myfix}[3]{\mysyn{fix} \myappsp #1 {:} #2 \mapsto #3}
\newcommand{\mysum}{\mathbin{\textcolor{AgdaDatatype}{+}}}
\newcommand{\mymeta}{\textsc}
\newcommand{\myhyps}{\mymeta{hyps}}
\newcommand{\mycc}{;}
-\newcommand{\myemptytele}{\cdot}
+\newcommand{\myemptytele}{\varepsilon}
\newcommand{\mymetagoes}{\Longrightarrow}
% \newcommand{\mytesctx}{\
\newcommand{\mytelesyn}{\myse{telescope}}
\newcommand{\myproj}[1]{\myfun{$\pi_{#1}$}}
\newcommand{\mysigma}{\mytyc{$\Sigma$}}
\newcommand{\mynegder}{\vspace{-0.3cm}}
-\newcommand{\myquot}{\Downarrow}
+\newcommand{\myquot}{\Uparrow}
+\newcommand{\mynquot}{\, \Downarrow}
+\renewcommand{\[}{\begin{equation*}}
+\renewcommand{\]}{\end{equation*}}
+\newcommand{\mymacol}[2]{\text{\textcolor{#1}{$#2$}}}
%% -----------------------------------------------------------------------------
\begin{minipage}{0.4\textwidth}
\begin{flushleft} \large
\emph{Supervisor:}\\
- Dr. Steffen \textsc{van Backel}
+ Dr. Steffen \textsc{van Bakel}
\end{flushleft}
\end{minipage}
\begin{minipage}{0.4\textwidth}
\label{sec:types}
\subsection{The untyped $\lambda$-calculus}
+\label{sec:untyped}
Along with Turing's machines, the earliest attempts to formalise computation
lead to the $\lambda$-calculus \citep{Church1936}. This early programming
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):
-{\mysmall
\[
(\myapp{\omega}{\omega}) \myred (\myapp{\omega}{\omega}) \myred \cdots \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
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{\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:
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:
-{\mysmall\[
+\[
\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. 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}.
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.}.
+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$.
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:
-{\mysmall\[
-(\myfix{\myb{x}}{\mytya}{\myb{x}}) : \mytya
-\]}
+\[(\myfix{\myb{x}}{\mytya}{\myb{x}}) : \mytya\]
\subsection{Inductive data}
\label{sec:ind-data}
\label{fig:list}
\end{figure}
-In section \ref{sec:well-order} we will see how to give a general account of
+In Section \ref{sec:well-order} we will see how to give a general account of
inductive data.
\section{Intuitionistic Type Theory}
The STLC can be made more expressive in various ways. \cite{Barendregt1991}
succinctly expressed geometrically how we can add expressivity:
-
$$
\xymatrix@!0@=1.5cm{
& \lambda\omega \ar@{-}[rr]\ar@{-}'[d][dd]
\item[Terms depending on types (towards $\lambda{2}$)] We can quantify over
types in our type signatures. For example, we can define a polymorphic
identity function:
- {\mysmall\[\displaystyle
+ \[\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
\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: {\mysmall\[\displaystyle(\myabss{\myb{A} \myar \myb{R}}{\mytyp}{(\myb{A}
- \myarr \myb{R}) \myarr \myb{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:
- {\mysmall\[\displaystyle(\myabss{\myb{x}}{\mybool}{\myite{\myb{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
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:term-types} for an
- explanation on why this causes problems.}. For this reason he gave a revised
+impredicativity.\footnote{In the early version there was only one universe
+ $\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}.
A related development is the polymorphic $\lambda$-calculus, and specifically
$
\begin{array}{r@{\ }c@{\ }l}
\mytmsyn & ::= & \myb{x} \mysynsep
- \mytyp_{l} \mysynsep
+ \mytyp_{level} \mysynsep
\myunit \mysynsep \mytt \mysynsep
\myempty \mysynsep \myapp{\myabsurd{\mytmsyn}}{\mytmsyn} \\
& | & \mybool \mysynsep \mytrue \mysynsep \myfalse \mysynsep
& | & \myw{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
\mytmsyn \mynode{\myb{x}}{\mytmsyn} \mytmsyn \\
& | & \myrec{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn} \\
- l & \in & \mathbb{N}
+ level & \in & \mathbb{N}
\end{array}
$
}
$\myred$---moreover, when comparing types syntactically we do it up to
renaming of bound names ($\alpha$-renaming). For example under this
discipline we will find that
-{\mysmall\[
+\[
\myabss{\myb{x}}{\mytya}{\myb{x}} \mydefeq \myabss{\myb{y}}{\mytya}{\myb{y}}
-\]}
+\]
Types that are definitionally equal can be used interchangeably. Here
the `conversion' rule is not syntax directed, but it is possible to
employ $\myred$ to decide term equality in a systematic way, by always
inconsistent for much the same reason that impredicative na\"{\i}ve set
theory is \citep{Hurkens1995}. However various techniques can be
employed to lift the burden of explicitly handling universes, as we will
-see in section \ref{sec:term-hierarchy}.
+see in Section \ref{sec:term-hierarchy}.
\subsubsection{Contexts}
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
-{\mysmall\[\text{\texttt{if null xs then head xs else 0}}\]}
+\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
For example, assuming that we have lists and natural numbers in our
language, using dependent functions we would be able to
write:
-{\mysmall\[
+\[
\begin{array}{l}
\myfun{length} : (\myb{A} {:} \mytyp_0) \myarr \myapp{\mylist}{\myb{A}} \myarr \mynat \\
\myarg \myfun{$>$} \myarg : \mynat \myarr \mynat \myarr \mytyp_0 \\
\myarr \myapp{\myapp{\myfun{length}}{\myb{A}}}{\myb{l}} \mathrel{\myfun{$>$}} 0 \myarr
\myb{A}
\end{array}
-\]}
+\]
\myfun{length} is the usual polymorphic length
function. $\myarg\myfun{$>$}\myarg$ is a function that takes two naturals
Another perhaps more `dependent' application of products, paired with
$\mybool$, is to offer choice between different types. For example we
can easily recover disjunctions:
-{\mysmall\[
+\[
\begin{array}{l}
\myarg\myfun{$\vee$}\myarg : \mytyp_0 \myarr \mytyp_0 \myarr \mytyp_0 \\
\myb{A} \mathrel{\myfun{$\vee$}} \myb{B} \mapsto \myexi{\myb{x}}{\mybool}{\myite{\myb{x}}{\myb{A}}{\myb{B}}} \\ \ \\
\myfun{case} : (\myb{A}\ \myb{B}\ \myb{C} {:} \mytyp_0) \myarr (\myb{A} \myarr \myb{C}) \myarr (\myb{B} \myarr \myb{C}) \myarr \myb{A} \mathrel{\myfun{$\vee$}} \myb{B} \myarr \myb{C} \\
\myfun{case} \myappsp \myb{A} \myappsp \myb{B} \myappsp \myb{C} \myappsp \myb{f} \myappsp \myb{g} \myappsp \myb{x} \mapsto \\
- \myind{2} \myapp{(\myitee{\myapp{\myfst}{\myb{b}}}{\myb{x}}{(\myite{\myb{b}}{\myb{A}}{\myb{B}})}{\myb{f}}{\myb{g}})}{(\myapp{\mysnd}{\myb{x}})}
+ \myind{2} \myapp{(\myitee{\myapp{\myfst}{\myb{x}}}{\myb{b}}{(\myite{\myb{b}}{\myb{A}}{\myb{B}})}{\myb{f}}{\myb{g}})}{(\myapp{\mysnd}{\myb{x}})}
\end{array}
-\]}
+\]
\subsubsection{$\mytyc{W}$, or well-order}
\label{sec:well-order}
$\myfun{rec}\ \myfun{with}$ acts as an induction principle on
$\mytyc{W}$, given a predicate an a function dealing with the inductive
case---we will gain more intuition about inductive data in ITT in
-section \ref{sec:user-type}.
+Section \ref{sec:user-type}.
For example, if we want to form natural numbers, we can take
-{\mysmall\[
+\[
\begin{array}{@{}l}
\mytyc{Tr} : \mybool \myarr \mytyp_0 \\
\mytyc{Tr} \myappsp \myb{b} \mapsto \myfun{if}\, \myb{b}\, \myunit\, \myfun{else}\, \myempty \\
\mynat : \mytyp_0 \\
\mynat \mapsto \myw{\myb{b}}{\mybool}{(\mytyc{Tr}\myappsp\myb{b})}
\end{array}
- \]} Each node will contain a boolean. If $\mytrue$, the number is
-non-zero, and we will have one child representing its predecessor, given
-that $\mytyc{Tr}$ will return $\myunit$. If $\myfalse$, the number is
-zero, and we will have no predecessors (children), given the $\myempty$:
-{\mysmall\[
+\]
+Each node will contain a boolean. If $\mytrue$, the number is non-zero,
+and we will have one child representing its predecessor, given that
+$\mytyc{Tr}$ will return $\myunit$. If $\myfalse$, the number is zero,
+and we will have no predecessors (children), given the $\myempty$:
+\[
\begin{array}{@{}l}
\mydc{zero} : \mynat \\
\mydc{zero} \mapsto \myfalse \mynodee (\myabs{\myb{z}}{\myabsurd{\mynat} \myappsp \myb{x}}) \\
\mydc{suc} : \mynat \myarr \mynat \\
\mydc{suc}\myappsp \myb{x} \mapsto \mytrue \mynodee (\myabs{\myarg}{\myb{x}})
\end{array}
-\]}
+\]
And with a bit of effort, we can recover addition:
-{\mysmall\[
+\[
\begin{array}{@{}l}
\myfun{plus} : \mynat \myarr \mynat \myarr \mynat \\
\myfun{plus} \myappsp \myb{x} \myappsp \myb{y} \mapsto \\
\myind{2}\myind{2}\myfun{if}\, \myb{b} / \myb{b'}.((\mytyc{Tr} \myappsp \myb{b'} \myarr \mynat) \myarr (\mytyc{Tr} \myappsp \myb{b'} \myarr \mynat) \myarr \mynat) \\
\myind{2}\myind{2}\myfun{then}\,(\myabs{\myarg\, \myb{f}}{\mydc{suc}\myappsp (\myapp{\myb{f}}{\mytt})})\, \myfun{else}\, (\myabs{\myarg\, \myarg}{\myb{y}})}
\end{array}
- \]} Note how we explicitly have to type the branches to make them
+ \]
+Note how we explicitly have to type the branches to make them
match with the definition of $\mynat$---which gives a taste of the
`clumsiness' of $\mytyc{W}$-types, which while useful as a reasoning
tool are useless to the user modelling data types.
While the $\myjeqq$ rule is slightly convoluted, ve can derive many more
`friendly' rules from it, for example a more obvious `substitution' rule, that
replaces equal for equal in predicates:
-{\mysmall\[
+\[
\begin{array}{l}
\myfun{subst} : \myfora{\myb{A}}{\mytyp}{\myfora{\myb{P}}{\myb{A} \myarr \mytyp}{\myfora{\myb{x}\ \myb{y}}{\myb{A}}{\myb{x} \mypeq{\myb{A}} \myb{y} \myarr \myapp{\myb{P}}{\myb{x}} \myarr \myapp{\myb{P}}{\myb{y}}}}} \\
\myfun{subst}\myappsp \myb{A}\myappsp\myb{P}\myappsp\myb{x}\myappsp\myb{y}\myappsp\myb{q}\myappsp\myb{p} \mapsto
\myjeq{(\myabs{\myb{x}\ \myb{y}\ \myb{q}}{\myapp{\myb{P}}{\myb{y}}})}{\myb{p}}{\myb{q}}
\end{array}
-\]}
+\]
Once we have $\myfun{subst}$, we can easily prove more familiar laws regarding
equality, such as symmetry, transitivity, congruence laws, etc.
\mydefeq \mypair{\myfst \myappsp \myb{x}}{\mysnd \myappsp \myb{x}}$.
Similarly, all one inhabitants of $\myunit$ and all zero inhabitants of
$\myempty$ can be considered equal. Quotation can be performed in a
-type-directed way, as we will witness in section \ref{sec:kant-irr}.
+type-directed way, as we will witness in Section \ref{sec:kant-irr}.
To justify this process in our type system we will add a congruence law
for abstractions and a similar law for products, plus the fact that all
permutations---one is the identity, and one swaps the elements. Given
this, $\myfun{K}$ and univalence are inconsistent, and thus a form of
dependent pattern matching that does not imply $\myfun{K}$ is subject of
-research\footnote{More information about univalence can be found at
- \url{http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations.html}.}.
+research.\footnote{More information about univalence can be found at
+ \url{http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations.html}.}
\subsection{Limitations}
However this is not the case, or in other words with the tools we have we have
no term of type
-{\mysmall\[
+\[
\myfun{ext} : \myfora{\myb{A}\ \myb{B}}{\mytyp}{\myfora{\myb{f}\ \myb{g}}{
\myb{A} \myarr \myb{B}}{
(\myfora{\myb{x}}{\myb{A}}{\myapp{\myb{f}}{\myb{x}} \mypeq{\myb{B}} \myapp{\myb{g}}{\myb{x}}}) \myarr
\myb{f} \mypeq{\myb{A} \myarr \myb{B}} \myb{g}
}
}
-\]}
+\]
To see why this is the case, consider the functions
-{\mysmall\[\myabs{\myb{x}}{0 \mathrel{\myfun{$+$}} \myb{x}}$ and $\myabs{\myb{x}}{\myb{x} \mathrel{\myfun{$+$}} 0}\]}
+\[\myabs{\myb{x}}{0 \mathrel{\myfun{$+$}} \myb{x}}$ and $\myabs{\myb{x}}{\myb{x} \mathrel{\myfun{$+$}} 0}\]
where $\myfun{$+$}$ is defined by recursion on the first argument,
gradually destructing it to build up successors of the second argument.
The two functions are clearly extensionally equal, and we can in fact
prove that
-{\mysmall\[
+\[
\myfora{\myb{x}}{\mynat}{(0 \mathrel{\myfun{$+$}} \myb{x}) \mypeq{\mynat} (\myb{x} \mathrel{\myfun{$+$}} 0)}
-\]}
+\]
By analysis on the $\myb{x}$. However, the two functions are not
definitionally equal, and thus we won't be able to get rid of the
quantification.
For all its faults, equality reflection does allow us to prove extensionality,
using the extensions we gave above. Assuming that $\myctx$ contains
-{\mysmall\[\myb{A}, \myb{B} : \mytyp; \myb{f}, \myb{g} : \myb{A} \myarr \myb{B}; \myb{q} : \myfora{\myb{x}}{\myb{A}}{\myapp{\myb{f}}{\myb{x}} \mypeq{} \myapp{\myb{g}}{\myb{x}}}\]}
+\[\myb{A}, \myb{B} : \mytyp; \myb{f}, \myb{g} : \myb{A} \myarr \myb{B}; \myb{q} : \myfora{\myb{x}}{\myb{A}}{\myapp{\myb{f}}{\myb{x}} \mypeq{} \myapp{\myb{g}}{\myb{x}}}\]
We can then derive
\begin{prooftree}
\mysmall
A recent development by \citet{Altenkirch2007}, \emph{Observational Type
Theory} (OTT), promises to keep the well behavedness of ITT while
-being able to gain many useful equality proofs\footnote{It is suspected
+being able to gain many useful equality proofs,\footnote{It is suspected
that OTT gains \emph{all} the equality proofs of ETT, but no proof
- exists yet.}, including function extensionality. The main idea is to
+ exists yet.} including function extensionality. The main idea is to
give the user the possibility to \emph{coerce} (or transport) values
from a type $\mytya$ to a type $\mytyb$, if the type checker can prove
structurally that $\mytya$ and $\mytya$ are equal; and providing a
$\myfun{If}\myarg\myfun{Then}\myarg\myfun{Else}\myarg$.
Correspondingly, canonical terms are those inhabiting canonical types
($\mytt$, $\mytrue$, $\myfalse$, $\myabss{\myb{x}}{\mytya}{\mytmt}$,
-...), and neutral terms those formed by eliminators\footnote{Using the
- terminology from section \ref{sec:types}, we'd say that canonical
- terms are in \emph{weak head normal form}.}. In the current system
+...), and neutral terms those formed by eliminators.\footnote{Using the
+ terminology from Section \ref{sec:types}, we'd say that canonical
+ terms are in \emph{weak head normal form}.} In the current system
(and hopefully in well-behaved systems), all closed terms reduce to a
canonical term, and all canonical types are inhabited by canonical
terms.
proof that given equal values in the first element, the types of the
second elements are equal too
($\myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{\myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2}}
- \myimpl \mytyb_1 \myeq \mytyb_2}$)\footnote{We are using $\myimpl$ to
+ \myimpl \mytyb_1 \myeq \mytyb_2}$).\footnote{We are using $\myimpl$ to
indicate a $\forall$ where we discard the first value. We write
$\mytyb_1[\myb{x_1}]$ to indicate that the $\myb{x_1}$ in $\mytyb_1$
is re-bound to the $\myb{x_1}$ quantified by the $\forall$, and
- similarly for $\myb{x_2}$ and $\mytyb_2$.}. This also explains the
+ similarly for $\myb{x_2}$ and $\mytyb_2$.} This also explains the
need for heterogeneous equality, since in the second proof it would be
awkward to express the fact that $\myb{A_1}$ is the same as $\myb{A_2}$.
In the respective $\myfun{coe}$ case, since the types are canonical, we
$\mybool$, we check that such data matches, and return bottom otherwise.
\subsection{Proof irrelevance and stuck coercions}
+\label{sec:ott-quot}
The last effort is required to make sure that proofs (members of
$\myprop$) are \emph{irrelevant}. Since they are devoid of
Moreover we can safely advance `stuck' $\myfun{coe}$rcions between
non-canonical but definitionally equal types. Consider for example
-{\mysmall\[
- \mycoee{(\myITE{\myb{b}}{\mynat}{\mybool})}{(\myITE{\myb{b}}{\mynat}{\mybool})}{\myb{x}}
- \]} Where $\myb{b}$ and $\myb{x}$ are abstracted variables. This
+\[
+\mycoee{(\myITE{\myb{b}}{\mynat}{\mybool})}{(\myITE{\myb{b}}{\mynat}{\mybool})}{\myb{x}}
+\]
+Where $\myb{b}$ and $\myb{x}$ are abstracted variables. This
$\myfun{coe}$ will not advance, since the types are not canonical.
However they are definitionally equal, and thus we can safely remove the
coerce and return $\myb{x}$ as it is.
features and more importantly observational equality.
We will first present the features of the system, and then describe the
-implementation we have developed in section \ref{sec:kant-practice}.
+implementation we have developed in Section \ref{sec:kant-practice}.
The defining features of \mykant\ are:
\begin{description}
\item[Full dependent types] As we would expect, we have dependent a system
which is as expressive as the `best' corner in the lambda cube described in
- section \ref{sec:itt}.
+ Section \ref{sec:itt}.
\item[Implicit, cumulative universe hierarchy] The user does not need to
specify universe level explicitly, and universes are \emph{cumulative}.
in the style of \cite{Pierce2000}, extending the concept for user
defined data types.
-\item[Type holes] When building up programs interactively, it is useful to
- leave parts unfinished while exploring the current context. This is what
- type holes are for.
-
-\item[Observational equality] As described in section \ref{sec:ott} but
+\item[Observational equality] As described in Section \ref{sec:ott} but
extended to work with the type hierarchy and to admit equality between
arbitrary data types.
\end{description}
\begin{array}{r@{\ }c@{\ }l}
\mytmsyn & ::= & \myb{x} \mysynsep \myabs{\myb{x}}{\mytmsyn} \mysynsep (\myapp{\mytmsyn}{\mytmsyn}) \mysynsep (\mytmsyn : \mytysyn)
\end{array}
- $ } We will have two kinds of typing judgements: \emph{inference} and
+ $
+}
+We will have two kinds of typing judgements: \emph{inference} and
\emph{checking}. $\myinf{\mytmt}{\mytya}$ indicates that $\mytmt$
infers the type $\mytya$, while $\mychk{\mytmt}{\mytya}$ can be checked
against type $\mytya$. The type of variables in context is inferred,
\end{tabular}
}
+For example, if we wanted to type function composition (in this case for
+naturals), we would have to annotate the term:
+\[
+ \myfun{comp} \mapsto (\myabs{\myb{f}\, \myb{g}\, \myb{x}}{\myb{f}\myappsp(\myb{g}\myappsp\myb{x})}) : (\mynat \myarr \mynat) \myarr (\mynat \myarr \mynat) \myarr \mynat \myarr \mynat
+\]
+But we would not have to annotate functions passed to it, since the type would be propagated to the arguments:
+\[
+ \myfun{comp}\myappsp (\myabs{\myb{x}}{\myb{x} \mathrel{\myfun{$+$}} 3}) \myappsp (\myabs{\myb{x}}{\myb{x} \mathrel{\myfun{$*$}} 4}) \myappsp 42
+\]
+
\subsection{Base terms and types}
Let us begin by describing the primitives available without the user
variables and substitution is left unspecified, and explained in section
\ref{sec:term-repr}, along with other implementation issues. We are
also going to give an account of the implicit type hierarchy separately
-in section \ref{sec:term-hierarchy}, so as not to clutter derivation
+in Section \ref{sec:term-hierarchy}, so as not to clutter derivation
rules too much, and just treat types as impredicative for the time
being.
\end{tabular}
}
-We can now give types to our terms. We defer the question of term
-equality (which is needed for type checking) to section
-\ref{sec:kant-irr}.
+We can now give types to our terms. Although we include the usual
+conversion rule, we defer a detailed account of definitional equality to
+Section \ref{sec:kant-irr}.
\mydesc{typing:}{\myctx \vdash \mytmsyn \Leftrightarrow \mytmsyn}{
\begin{tabular}{cccc}
\DisplayProof
&
\AxiomC{$\myinf{\mytmt}{\mytya}$}
- \UnaryInfC{$\mychk{\mytmt}{\mytya}$}
+ \AxiomC{$\myctx \vdash \mytya \mydefeq \mytyb$}
+ \BinaryInfC{$\mychk{\mytmt}{\mytyb}$}
\DisplayProof
\end{tabular}
\myderivspp
made up of all the variables bound by $\mytele$. $\mytele \myarr
\mytya$ refers to the type made by turning the telescope into a series
of $\myarr$. Returning to the examples above, we have that
-{\mysmall\[
+\[
(\myb{x} {:} \mynat); (\myb{p} : \myapp{\myfun{even}}{\myb{x}}) \myarr \mynat =
(\myb{x} {:} \mynat) \myarr (\myb{p} : \myapp{\myfun{even}}{\myb{x}}) \myarr \mynat
-\]}
+\]
We make use of various operations to manipulate telescopes:
\begin{itemize}
(1-indexed).
\item $\mytake_i(\mytele)$ refers to the telescope created by taking the
first $i$ elements of $\mytele$: $\mytake_1((\myb{x} {:} \mynat); (\myb{p} :
- \myapp{\myfun{even}}{\myb{x}})) = (\myb{x} {:} \mynat)$
+ \myapp{\myfun{even}}{\myb{x}})) = (\myb{x} {:} \mynat)$.
\item $\mytele \vec{A}$ refers to the telescope made by `applying' the
terms in $\vec{A}$ on $\mytele$: $((\myb{x} {:} \mynat); (\myb{p} :
\myapp{\myfun{even}}{\myb{x}}))42 = (\myb{p} :
\item[Natural numbers] To define natural numbers, we create a data type
with two constructors: one with zero arguments ($\mydc{zero}$) and one
with one recursive argument ($\mydc{suc}$):
- {\mysmall\[
+ \[
\begin{array}{@{}l}
\myadt{\mynat}{ }{ }{
\mydc{zero} \mydcsep \mydc{suc} \myappsp \mynat
}
\end{array}
- \]}
+ \]
This is very similar to what we would write in Haskell:
- {\mysmall\[\text{\texttt{data Nat = Zero | Suc Nat}}\]}
+ \begin{Verbatim}
+data Nat = Zero | Suc Nat
+ \end{Verbatim}
Once the data type is defined, $\mykant$\ will generate syntactic
constructs for the type and data constructors, so that we will have
\begin{center}
will return the base case if the provided number is $\mydc{zero}$, and
recursively apply the inductive step if the number is a
$\mydc{suc}$cessor:
- {\mysmall\[
+ \[
\begin{array}{@{}l@{}l}
\mytyc{\mynat}.\myfun{elim} \myappsp \mydc{zero} & \myappsp \myse{P} \myappsp \myse{pz} \myappsp \myse{ps} \myred \myse{pz} \\
\mytyc{\mynat}.\myfun{elim} \myappsp (\mydc{suc} \myappsp \mytmt) & \myappsp \myse{P} \myappsp \myse{pz} \myappsp \myse{ps} \myred \myse{ps} \myappsp \mytmt \myappsp (\mynat.\myfun{elim} \myappsp \mytmt \myappsp \myse{P} \myappsp \myse{pz} \myappsp \myse{ps})
\end{array}
- \]}
+ \]
The Haskell equivalent would be
- {\mysmall\[
- \begin{array}{@{}l}
- \text{\texttt{elim :: Nat -> a -> (Nat -> a -> a) -> a}}\\
- \text{\texttt{elim Zero pz ps = pz}}\\
- \text{\texttt{elim (Suc n) pz ps = ps n (elim n pz ps)}}
- \end{array}
- \]}
+ \begin{Verbatim}
+elim :: Nat -> a -> (Nat -> a -> a) -> a
+elim Zero pz ps = pz
+elim (Suc n) pz ps = ps n (elim n pz ps)
+\end{Verbatim}
Which buys us the computational behaviour, but not the reasoning power.
\item[Binary trees] Now for a polymorphic data type: binary trees, since
lists are too similar to natural numbers to be interesting.
- {\mysmall\[
+ \[
\begin{array}{@{}l}
\myadt{\mytree}{\myappsp (\myb{A} {:} \mytyp)}{ }{
\mydc{leaf} \mydcsep \mydc{node} \myappsp (\myapp{\mytree}{\myb{A}}) \myappsp \myb{A} \myappsp (\myapp{\mytree}{\myb{A}})
}
\end{array}
- \]}
+ \]
Now the purpose of constructors as syntax can be explained: what would
the type of $\mydc{leaf}$ be? If we were to treat it as a `normal'
term, we would have to specify the type parameter of the tree each
time the constructor is applied:
- {\mysmall\[
+ \[
\begin{array}{@{}l@{\ }l}
\mydc{leaf} & : \myfora{\myb{A}}{\mytyp}{\myapp{\mytree}{\myb{A}}} \\
\mydc{node} & : \myfora{\myb{A}}{\mytyp}{\myapp{\mytree}{\myb{A}} \myarr \myb{A} \myarr \myapp{\mytree}{\myb{A}} \myarr \myapp{\mytree}{\myb{A}}}
\end{array}
- \]}
+ \]
The problem with this approach is that creating terms is incredibly
verbose and dull, since we would need to specify the type parameters
each time. For example if we wished to create a $\mytree \myappsp
\mynat$ with two nodes and three leaves, we would have to write
- {\mysmall\[
+ \[
\mydc{node} \myappsp \mynat \myappsp (\mydc{node} \myappsp \mynat \myappsp (\mydc{leaf} \myappsp \mynat) \myappsp (\myapp{\mydc{suc}}{\mydc{zero}}) \myappsp (\mydc{leaf} \myappsp \mynat)) \myappsp \mydc{zero} \myappsp (\mydc{leaf} \myappsp \mynat)
- \]}
+ \]
The redundancy of $\mynat$s is quite irritating. Instead, if we treat
constructors as syntactic elements, we can `extract' the type of the
parameter from the type that the term gets checked against, much like
\end{tabular}
\end{center}
Which enables us to write, much more concisely
- {\mysmall\[
+ \[
\mydc{node} \myappsp (\mydc{node} \myappsp \mydc{leaf} \myappsp (\myapp{\mydc{suc}}{\mydc{zero}}) \myappsp \mydc{leaf}) \myappsp \mydc{zero} \myappsp \mydc{leaf} : \myapp{\mytree}{\mynat}
- \]}
+ \]
We gain an annotation, but we lose the myriad of types applied to the
constructors. Conversely, with the eliminator for $\mytree$, we can
infer the type of the arguments given the type of the destructed:
\item[Empty type] We have presented types that have at least one
constructors, but nothing prevents us from defining types with
\emph{no} constructors:
- {\mysmall\[
- \myadt{\mytyc{Empty}}{ }{ }{ }
- \]}
+ \[\myadt{\mytyc{Empty}}{ }{ }{ }\]
What shall the `induction principle' on $\mytyc{Empty}$ be? Does it
even make sense to talk about induction on $\mytyc{Empty}$?
$\mykant$\ does not care, and generates an eliminator with no `cases',
ordering on natural numbers, $\myfun{le}$---`less or equal'.
$\myfun{le}\myappsp \mytmm \myappsp \mytmn$ will be inhabited only if
$\mytmm \le \mytmn$:
- {\mysmall\[
+ \[
\begin{array}{@{}l}
\myfun{le} : \mynat \myarr \mynat \myarr \mytyp \\
\myfun{le} \myappsp \myb{n} \mapsto \\
\mynat.\myfun{elim} \myappsp \myb{m} \myappsp (\myabs{\myarg}{\mytyp}) \myappsp \myempty \myappsp (\myabs{\myb{m'}\, \myarg}{\myapp{\myb{f}}{\myb{m'}}})
})
\end{array}
- \]} We return $\myunit$ if the scrutinised is $\mydc{zero}$ (every
+ \]
+ We return $\myunit$ if the scrutinised is $\mydc{zero}$ (every
number in less or equal than zero), $\myempty$ if the first number is
a $\mydc{suc}$cessor and the second a $\mydc{zero}$, and we recurse if
they are both successors. Since we want the list to have possibly
`lifted' naturals with a bottom (less than everything) and top
(greater than everything) elements, along with an associated comparison
function:
- {\mysmall\[
+ \[
\begin{array}{@{}l}
\myadt{\mytyc{Lift}}{ }{ }{\mydc{bot} \mydcsep \mydc{lift} \myappsp \mynat \mydcsep \mydc{top}}\\
\myfun{le'} : \mytyc{Lift} \myarr \mytyc{Lift} \myarr \mytyp\\
\mytyc{Lift}.\myfun{elim} \myappsp \myb{l_2} \myappsp (\myabs{\myarg}{\mytyp}) \myappsp \myempty \myappsp (\myabs{\myarg}{\myempty}) \myappsp \myunit
})
\end{array}
- \]} Finally, we can defined a type of ordered lists. The type is
+ \]
+ Finally, we can defined a type of ordered lists. The type is
parametrised over two values representing the lower and upper bounds
of the elements, as opposed to the type parameters that we are used
to. Then, an empty list will have to have evidence that the bounds
are ordered, and each time we add an element we require the list to
have a matching lower bound:
- {\mysmall\[
+ \[
\begin{array}{@{}l}
\myadt{\mytyc{OList}}{\myappsp (\myb{low}\ \myb{upp} {:} \mytyc{Lift})}{\\ \myind{2}}{
\mydc{nil} \myappsp (\myfun{le'} \myappsp \myb{low} \myappsp \myb{upp}) \mydcsep \mydc{cons} \myappsp (\myb{n} {:} \mynat) \myappsp (\mytyc{OList} \myappsp (\myfun{lift} \myappsp \myb{n}) \myappsp \myb{upp}) \myappsp (\myfun{le'} \myappsp \myb{low} \myappsp (\myfun{lift} \myappsp \myb{n})
}
\end{array}
- \]} If we want we can then employ this structure to write and prove
- correct various sorting algorithms\footnote{See this presentation by
+ \]
+ If we want we can then employ this structure to write and prove
+ correct various sorting algorithms.\footnote{See this presentation by
Conor McBride:
\url{https://personal.cis.strath.ac.uk/conor.mcbride/Pivotal.pdf},
and this blog post by the author:
- \url{http://mazzo.li/posts/AgdaSort.html}.}.
+ \url{http://mazzo.li/posts/AgdaSort.html}.}
\item[Dependent products] Apart from $\mysyn{data}$, $\mykant$\ offers
us another way to define types: $\mysyn{record}$. A record is a
fields of the said constructor.
For example, we can recover dependent products:
- {\mysmall\[
+ \[
\begin{array}{@{}l}
\myreco{\mytyc{Prod}}{\myappsp (\myb{A} {:} \mytyp) \myappsp (\myb{B} {:} \myb{A} \myarr \mytyp)}{\\ \myind{2}}{\myfst : \myb{A}, \mysnd : \myapp{\myb{B}}{\myb{fst}}}
\end{array}
- \]}
+ \]
Here $\myfst$ and $\mysnd$ are the projections, with their respective
types. Note that each field can refer to the preceding fields. A
constructor will be automatically generated, under the name of
For what concerns records, recursive occurrences are disallowed. The
reason for this choice is answered by the reason for the choice of
having records at all: we need records to give the user types with
-$\eta$-laws for equality, as we saw in section \ref{sec:eta-expand}
-and in the treatment of OTT in section \ref{sec:ott}. If we tried to
+$\eta$-laws for equality, as we saw in Section \ref{sec:eta-expand}
+and in the treatment of OTT in Section \ref{sec:ott}. If we tried to
$\eta$-expand recursive data types, we would expand forever.
To implement bidirectional type checking for constructors and
\subsubsection{Why user defined types? Why eliminators?}
+The `hardest' design choice when designing $\mykant$\ was to decide
+whether user defined types should be included. In the end, we can
+devise
+
% TODO reference levitated theories, indexed containers
foobar
\subsection{Cumulative hierarchy and typical ambiguity}
\label{sec:term-hierarchy}
-A type hierarchy as presented in section \label{sec:itt} is a
+Having a well founded type hierarchy is crucial if we want to retain
+consistency, otherwise we can break our type systems by proving bottom,
+as shown in Appendix \ref{sec:hurkens}.
+
+However, hierarchy as presented in section \label{sec:itt} is a
considerable burden on the user, on various levels. Consider for
-example how we recovered disjunctions in section \ref{sec:disju}: we
+example how we recovered disjunctions in Section \ref{sec:disju}: we
have a function that takes two $\mytyp_0$ and forms a new $\mytyp_0$.
What if we wanted to form a disjunction containing something a
$\mytyp_1$, or $\mytyp_{42}$? Our definition would fail us, since
% TODO finish
\mydesc{cumulativity:}{\myctx \vdash \mytmsyn \mycumul \mytmsyn}{
\begin{tabular}{ccc}
- \AxiomC{\phantom{$\myctx \vdash \mytya \mycumul \mytyb$}}
- \UnaryInfC{$\myctx \vdash \mytya \mycumul \mytya$}
+ \AxiomC{$\myctx \vdash \mytya \mydefeq \mytyb$}
+ \UnaryInfC{$\myctx \vdash \mytya \mycumul \mytyb$}
\DisplayProof
&
\AxiomC{\phantom{$\myctx \vdash \mytya \mydefeq \mytyb$}}
\myderivspp
\begin{tabular}{ccc}
- \AxiomC{$\myctx \vdash \mytya_1 \ \mytyb$}
- \UnaryInfC{$\myctx \vdash \mytya \mycumul \mytyb$}
- \DisplayProof
- &
- \AxiomC{\phantom{$\myctx \vdash \mytya \mydefeq \mytyb$}}
- \UnaryInfC{$\myctx \vdash \mytyp_l \mycumul \mytyp_{l+1}$}
+ \AxiomC{$\myjud{\mytmt}{\mytya}$}
+ \AxiomC{$\myctx \vdash \mytya \mycumul \mytyb$}
+ \BinaryInfC{$\myjud{\mytmt}{\mytyb}$}
\DisplayProof
&
- \AxiomC{$\myctx \vdash \mytya \mycumul \mytyb$}
- \AxiomC{$\myctx \vdash \mytyb \mycumul \myse{C}$}
- \BinaryInfC{$\myctx \vdash \mytya \mycumul \myse{C}$}
+ \AxiomC{$\myctx \vdash \mytya_1 \mydefeq \mytya_2$}
+ \AxiomC{$\myctx; \myb{x} : \mytya_1 \vdash \mytyb_1 \mycumul \mytyb_2$}
+ \BinaryInfC{$\myctx (\myb{x} {:} \mytya_1) \myarr \mytyb_1 \mycumul (\myb{x} {:} \mytya_2) \myarr \mytyb_2$}
\DisplayProof
\end{tabular}
}
-\caption{Cumulativity rules for \mykant, plus a `conversion' rule for
- cumulative types.}
+\caption{Cumulativity rules for base types in \mykant, plus a
+ `conversion' rule for cumulative types.}
\label{fig:cumulativity}
\end{figure}
cumulativity for types, abstractions, and data constructors.
For example we might define our disjunction to be
-{\mysmall\[
+\[
\myarg\myfun{$\vee$}\myarg : \mytyp_{100} \myarr \mytyp_{100} \myarr \mytyp_{100}
-\]}
+\]
And hope that $\mytyp_{100}$ will be large enough to fit all the types
that we want to use with our disjunction. However, there are two
problems with this. First, there is the obvious clumsyness of having to
If at any point the constraint set becomes inconsistent, type checking
fails. Moreover, when comparing two $\mytyp$ terms we equate their
respective references with two $\le$ constraints---the details are
-explained in section \ref{sec:hier-impl}.
+explained in Section \ref{sec:hier-impl}.
Another more flexible but also more verbose alternative is the one
chosen by Agda, where levels can be quantified so that the relationship
between arguments and result in type formers can be explicitly
expressed:
-{\mysmall\[
+\[
\myarg\myfun{$\vee$}\myarg : (l_1\, l_2 : \mytyc{Level}) \myarr \mytyp_{l_1} \myarr \mytyp_{l_2} \myarr \mytyp_{l_1 \mylub l_2}
-\]}
+\]
Inference algorithms to automatically derive this kind of relationship
are currently subject of research. We chose less flexible but more
concise way, since it is easier to implement and better understood.
is that we let the user define inductive types.
Reconciling propositions for OTT and a hierarchy had already been
-investigated by Conor McBride\footnote{See
- \url{http://www.e-pig.org/epilogue/index.html?p=1098.html}.}, and we
+investigated by Conor McBride,\footnote{See
+ \url{http://www.e-pig.org/epilogue/index.html?p=1098.html}.} and we
follow his broad design plan, although with some modifications. Most of
the work, as an extension of elaboration, is to handle reduction rules
and coercions for data types---both type constructors and data
Before defining $\myprop$, we define some basic types inside $\mykant$,
as the target for the $\myprop$ decoder:
-{\mysmall\[
+\[
\begin{array}{l}
\myadt{\mytyc{Empty}}{}{ }{ } \\
\myfun{absurd} : (\myb{A} {:} \mytyp) \myarr \mytyc{Empty} \myarr \myb{A} \mapsto \\
\myreco{\mytyc{Prod}}{\myappsp (\myb{A}\ \myb{B} {:} \mytyp)}{ }{\myfun{fst} : \myb{A}, \myfun{snd} : \myb{B} }
\end{array}
-\]}
+\]
When using $\mytyc{Prod}$, we shall use $\myprod$ to define `nested'
products, and $\myproj{n}$ to project elements from them, so that
-{\mysmall
\[
\begin{array}{@{}l}
\mytya \myprod \mytyb = \mytyc{Prod} \myappsp \mytya \myappsp (\mytyc{Prod} \myappsp \mytyb \myappsp \myunit) \\
\myind{2} \vdots
\end{array}
\]
-}
And so on, so that $\myproj{n}$ will work with all products with at
least than $n$ elements. Then we can define propositions, and decoding:
sums' in the literature, referring to the interpretation that
identifies the first element as a `tag' deciding the type of the
second element, which lets us recover sum types (disjuctions), as we
- saw in section \ref{sec:user-type}. Thus, $\mysigma$.} to
- avoid confusion with the $\mytyc{Prod}$ in the prelude: {\mysmall\[
+ saw in Section \ref{sec:user-type}. Thus, $\mysigma$.} to
+ avoid confusion with the $\mytyc{Prod}$ in the prelude:
+ \[
\begin{array}{@{}l}
\myreco{\mysigma}{\myappsp (\myb{A} {:} \mytyp) \myappsp (\myb{B} {:} \myb{A} \myarr \mytyp)}{\\ \myind{2}}{\myfst : \myb{A}, \mysnd : \myapp{\myb{B}}{\myb{fst}}}
\end{array}
- \]} Let's start with type-level equality. The result we want is
- {\mysmall\[
+ \]
+ Let's start with type-level equality. The result we want is
+ \[
\begin{array}{@{}l}
\mysigma \myappsp \mytya_1 \myappsp \mytyb_1 \myeq \mysigma \myappsp \mytya_2 \myappsp \mytyb_2 \myred \\
\myind{2} \mytya_1 \myeq \mytya_2 \myand \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{\myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2}} \myimpl \myapp{\mytyb_1}{\myb{x_1}} \myeq \myapp{\mytyb_2}{\myb{x_2}}}
\end{array}
- \]} The difference here is that in the original presentation of OTT
+ \]
+ The difference here is that in the original presentation of OTT
the type binders are explicit, while here $\mytyb_1$ and $\mytyb_2$
functions returning types. We can do this thanks to the type
hierarchy, and this hints at the fact that heterogeneous equality will
provides the solution to simplify the equality above.
If we take, just like we saw previously in OTT
- {\mysmall\[
+ \[
\begin{array}{@{}l}
\myjm{\myse{f}_1}{\myfora{\mytya_1}{\myb{x_1}}{\mytyb_1}}{\myse{f}_2}{\myfora{\mytya_2}{\myb{x_2}}{\mytyb_2}} \myred \\
\myind{2} \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{
\myjm{\myapp{\myse{f}_1}{\myb{x_1}}}{\mytyb_1[\myb{x_1}]}{\myapp{\myse{f}_2}{\myb{x_2}}}{\mytyb_2[\myb{x_2}]}
}}
\end{array}
- \]} Then we can simply take
- {\mysmall\[
+ \]
+ Then we can simply take
+ \[
\begin{array}{@{}l}
\mysigma \myappsp \mytya_1 \myappsp \mytyb_1 \myeq \mysigma \myappsp \mytya_2 \myappsp \mytyb_2 \myred \\ \myind{2} \mytya_1 \myeq \mytya_2 \myand \myjm{\mytyb_1}{\mytya_1 \myarr \mytyp}{\mytyb_2}{\mytya_2 \myarr \mytyp}
\end{array}
- \]} Which will reduce to precisely what we desire. For what
+ \]
+ Which will reduce to precisely what we desire. For what
concerns coercions and quotation, things stay the same (apart from the
fact that we apply to the second argument instead of substituting).
We can recognise records such as $\mysigma$ as such and employ
- projections in value equality, coercions, and quotation; as to not
+ projections in value equality and coercions; as to not
impede progress if not necessary.
\item[Lists] Now for finite lists, which will give us a taste for data
constructors:
- {\mysmall\[
+ \[
\begin{array}{@{}l}
\myadt{\mylist}{\myappsp (\myb{A} {:} \mytyp)}{ }{\mydc{nil} \mydcsep \mydc{cons} \myappsp \myb{A} \myappsp (\myapp{\mylist}{\myb{A}})}
\end{array}
- \]}
+ \]
Type equality is simple---we only need to compare the parameter:
- {\mysmall\[
+ \[
\mylist \myappsp \mytya_1 \myeq \mylist \myappsp \mytya_2 \myred \mytya_1 \myeq \mytya_2
- \]} For coercions, we transport based on the constructor, recycling
- the proof for the inductive occurrence: {\mysmall\[
+ \]
+ For coercions, we transport based on the constructor, recycling the
+ proof for the inductive occurrence:
+ \[
\begin{array}{@{}l@{\ }c@{\ }l}
\mycoe \myappsp (\mylist \myappsp \mytya_1) \myappsp (\mylist \myappsp \mytya_2) \myappsp \myse{Q} \myappsp \mydc{nil} & \myred & \mydc{nil} \\
\mycoe \myappsp (\mylist \myappsp \mytya_1) \myappsp (\mylist \myappsp \mytya_2) \myappsp \myse{Q} \myappsp (\mydc{cons} \myappsp \mytmm \myappsp \mytmn) & \myred & \\
\multicolumn{3}{l}{\myind{2} \mydc{cons} \myappsp (\mycoe \myappsp \mytya_1 \myappsp \mytya_2 \myappsp \myse{Q} \myappsp \mytmm) \myappsp (\mycoe \myappsp (\mylist \myappsp \mytya_1) \myappsp (\mylist \myappsp \mytya_2) \myappsp \myse{Q} \myappsp \mytmn)}
\end{array}
- \]} Value equality is unsurprising---we match the constructors, and
+ \]
+ Value equality is unsurprising---we match the constructors, and
return bottom for mismatches. However, we also need to equate the
- parameter in $\mydc{nil}$: {\mysmall\[
+ parameter in $\mydc{nil}$:
+ \[
\begin{array}{r@{ }c@{\ }c@{\ }c@{}l@{\ }c@{\ }r@{}c@{\ }c@{\ }c@{}l@{\ }l}
(& \mydc{nil} & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{nil} & : & \myapp{\mylist}{\mytya_2} &) \myred \mytya_1 \myeq \mytya_2 \\
(& \mydc{cons} \myappsp \mytmm_1 \myappsp \mytmn_1 & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{cons} \myappsp \mytmm_2 \myappsp \mytmn_2 & : & \myapp{\mylist}{\mytya_2} &) \myred \\
(& \mydc{nil} & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{cons} \myappsp \mytmm_2 \myappsp \mytmn_2 & : & \myapp{\mylist}{\mytya_2} &) \myred \mybot \\
(& \mydc{cons} \myappsp \mytmm_1 \myappsp \mytmn_1 & : & \myapp{\mylist}{\mytya_1} &) & \myeq & (& \mydc{nil} & : & \myapp{\mylist}{\mytya_2} &) \myred \mybot
\end{array}
- \]}
- Finally, quotation
+ \]
% TODO quotation
\item[Evil type]
Where is $\myprop$ placed in the type hierarchy? The main indicator
is the decoding operator, since it converts into things that already
live in the hierarchy. For example, if we
-have {\mysmall\[
+have
+\[
\myprdec{\mynat \myarr \mybool \myeq \mynat \myarr \mybool} \myred
\mytop \myand ((\myb{x}\, \myb{y} : \mynat) \myarr \mytop \myarr \mytop)
- \]} we will better make sure that the `to be decoded' is at the same
+\]
+we will better make sure that the `to be decoded' is at the same
level as its reduction as to preserve subject reduction. In the example
above, we'll have that proposition to be at least as large as the type
of $\mynat$, since the reduced proof will abstract over it. Pretending
\end{center}
$\mybot$ and $\mytop$ living at any level, $\myand$ and $\forall$
following rules similar to the ones for $\myprod$ and $\myarr$ in
-section \ref{sec:itt}. However, we need to be careful with value
-equality since for example we have that {\mysmall\[
+Section \ref{sec:itt}. However, we need to be careful with value
+equality since for example we have that
+\[
\myprdec{\myjm{\myse{f}_1}{\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}}{\myse{f}_2}{\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}}}
\myred
\myfora{\myb{x_1}}{\mytya_1}{\myfora{\myb{x_2}}{\mytya_2}{\cdots}}
- \]} where the proposition decodes into something of type
- $\mytyp_l$, where $\mytya : \mytyp_l$ and $\mytyb : \mytyp_l$. We
- can resolve this tension by making all equalities larger:
+\]
+where the proposition decodes into something of type $\mytyp_l$, where
+$\mytya : \mytyp_l$ and $\mytyb : \mytyp_l$. We can resolve this
+tension by making all equalities larger:
\begin{prooftree}
\AxiomC{$\myjud{\mytmm}{\mytya}$}
\AxiomC{$\myjud{\mytya}{\mytyp_l}$}
That is, we are small when we can (type equalities) and large otherwise.
This would not work in a non-cumulative theory because subject reduction
-would not hold. Consider for instance {\mysmall\[
+would not hold. Consider for instance
+\[
\myjm{\mynat}{\myITE{\mytrue}{\mytyp_0}{\mytyp_0}}{\mybool}{\myITE{\mytrue}{\mytyp_0}{\mytyp_0}}
: \myprop_1
-\]}
+\]
which reduces to
-{\mysmall\[
- \myjm{\mynat}{\mytyp_0}{\mybool}{\mytyp_0} : \myprop_0
- \]} We need $\myprop_0$ to be $\myprop_1$ too, which will be the case
-with cumulativity. This is not the most elegant of systems, but it buys
-us a cheap type level equality without having to replicate functionality
-with a dedicated construct.
-
-\subsubsection{Quotation and term equality}
+\[\myjm{\mynat}{\mytyp_0}{\mybool}{\mytyp_0} : \myprop_0 \]
+We need $\myprop_0$ to be $\myprop_1$ too, which will be the case with
+cumulativity. This is not the most elegant of systems, but it buys us a
+cheap type level equality without having to replicate functionality with
+a dedicated construct.
+
+\subsubsection{Quotation and definitional equality}
\label{sec:kant-irr}
-% \begin{figure}[t]
-% \mydesc{reduction}{\mytmsyn \myred \mytmsyn}{
+Now we can give an account of definitional equality, by explaining how
+to perform quotation (as defined in Section \ref{sec:eta-expand})
+towards the goal described in Section \ref{sec:ott-quot}.
-% }
-% \caption{Quotation in \mykant.}
-% \label{fig:kant-quot}
-% \end{figure}
+We want to:
+\begin{itemize}
+\item Perform $\eta$-expansion on functions and records.
+
+\item As a consequence of the previous point, identify all records with
+no projections as equal, since they will have only one element.
+
+\item Identify all members of types with no elements as equal.
+
+\item Identify all equivalent proofs as equal---with `equivalent proof'
+we mean those proving the same propositions.
+
+\item Advance coercions working across definitionally equal types.
+\end{itemize}
+Towards these goals and following the intuition between bidirectional
+type checking we define two mutually recursive functions, one quoting
+canonical terms against their types (since we need the type to typecheck
+canonical terms), one quoting neutral terms while recovering their
+types.
+
+Our quotation will work on normalised terms, so that all defined values
+will have been replaced. Moreover, we match on datatype eliminators and
+all their arguments, so that $\mynat.\myfun{elim} \myappsp \vec{\mytmt}$
+will stand for $\mynat.\myfun{elim}$ applied to the scrutinised
+$\mynat$, plus its three arguments. This measure can be easily
+implemented by checking the head of applications and `consuming' the
+needed terms.
+
+% TODO finish this
+\begin{figure}[t]
+ \mydesc{canonical quotation}{\myctx \vdash \mytmsyn \myquot \mytmsyn \mapsto \mytmsyn}{
+
+ }
+
+ \mynegder
+
+ \mydesc{neutral quotation}{\myctx \vdash \mynquot \mytmsyn \mapsto \mytmsyn : \mytmsyn}{
+
+ }
+ \caption{Quotation in \mykant.}
+ \label{fig:kant-quot}
+\end{figure}
% TODO finish
% TODO finish
-\subsection{Type holes}
-
\section{\mykant : The practice}
\label{sec:kant-practice}
The codebase consists of around 2500 lines of Haskell, as reported by
-the \texttt{cloc} utility. The high level design is inspired by Conor
-McBride's work on various incarnations of Epigram, and specifically by
-the first version as described \citep{McBride2004} and the codebase for
-the new version \footnote{Available intermittently as a \texttt{darcs}
- repository at \url{http://sneezy.cs.nott.ac.uk/darcs/Pig09}.}. In
-many ways \mykant\ is something in between the first and second version
-of Epigram.
+the \texttt{cloc} utility. The high level design is inspired by the
+work on various incarnations of Epigram, and specifically by the first
+version as described \citep{McBride2004} and the codebase for the new
+version.\footnote{Available intermittently as a \texttt{darcs}
+repository at \url{http://sneezy.cs.nott.ac.uk/darcs/Pig09}.} In many
+ways \mykant\ is something in between the first and second version of
+Epigram.
The author learnt the hard way the implementations challenges for such a
project, and while there is a solid and working base to work on, the
implementation of observational equality is not currently complete.
-However, given the detailed plan in the previous section, doing so would
+However, given the detailed plan in the previous section, doing so
should not prove to be too much work.
The interaction happens in a read-eval-print loop (REPL). The REPL is a
which is available at \url{kant.mazzo.li} and presents itself as in
figure \ref{fig:kant-web}.
-\begin{figure}
- \centering{
- \includegraphics[scale=1.0]{kant-web.png}
- }
- \caption{The \mykant\ web prompt.}
+\begin{figure}[t]
+{\small\begin{verbatim}B E R T U S
+Version 0.0, made in London, year 2013.
+>>> :h
+<decl> Declare value/data type/record
+:t <term> Typecheck
+:e <term> Normalise
+:p <term> Pretty print
+:l <file> Load file
+:r <file> Reload file (erases previous environment)
+:i <name> Info about an identifier
+:q Quit
+>>> :l data/samples/good/common.ka
+OK
+>>> :e plus three two
+suc (suc (suc (suc (suc zero))))
+>>> :t plus three two
+Type: Nat\end{verbatim}
+}
+
+ \caption{A sample run of the \mykant\ prompt.}
\label{fig:kant-web}
\end{figure}
\item[Reference] Occurrences of $\mytyp$ get decorated by a unique reference,
which is necessary to implement the type hierarchy check.
-\item[Elaborate] Convert the declaration to some context item, which might be
- a value declaration (type and body) or a data type declaration (constructors
- and destructors). This phase works in tandem with \textbf{Typechecking},
- which in turns needs to \textbf{Evaluate} terms.
+\item[Elaborate] Converts the declaration to some context items, which
+ might be a value declaration (type and body) or a data type
+ declaration (constructors and destructors). This phase works in
+ tandem with \textbf{Type checking}, which in turns needs to
+ \textbf{Evaluate} terms.
\item[Distill] and report the result. `Distilling' refers to the process of
converting a core term back to a sugared version that the user can
\label{fig:kant-process}
\end{figure}
-\subsection{Parsing and \texttt{Sugar}}
+Here we will review only a sampling of the more interesting
+implementation challenges present when implementing an interactive
+theorem prover.
-\subsection{Term representation and context}
+\subsection{Term and context representation}
\label{sec:term-repr}
-\subsection{Type checking}
+\subsubsection{Naming and substituting}
+
+Perhaps surprisingly, one of the most fundamental challenges in
+implementing a theory of the kind presented is choosing a good data type
+for terms, and specifically handling substitutions in a sane way.
+
+There are two broad schools of thought when it comes to naming
+variables, and thus substituting:
+\begin{description}
+\item[Nameful] Bound variables are represented by some enumerable data
+ type, just as we have described up to now, starting from Section
+ \ref{sec:untyped}. The problem is that avoiding name capturing is a
+ nightmare, both in the sense that it is not performant---given that we
+ need to rename rename substitute each time we `enter' a binder---but
+ most importantly given the fact that in even more slightly complicated
+ systems it is very hard to get right, even for experts.
+
+ One of the sore spots of explicit names is comparing terms up
+ $\alpha$-renaming, which again generates a huge amounts of
+ substitutions and requires special care. We can represent the
+ relationship between variables and their binders, by...
+
+\item[Nameless] ...getting rid of names altogether, and representing
+ bound variables with an index referring to the `binding' structure, a
+ notion introduced by \cite{de1972lambda}. Classically $0$ represents
+ the variable bound by the innermost binding structure, $1$ the
+ second-innermost, and so on. For instance with simple abstractions we
+ might have
+ \[\mymacol{red}{\lambda}\, (\mymacol{blue}{\lambda}\, \mymacol{blue}{0}\, (\mymacol{AgdaInductiveConstructor}{\lambda\, 0}))\, (\mymacol{AgdaFunction}{\lambda}\, \mymacol{red}{1}\, \mymacol{AgdaFunction}{0}) : ((\mytya \myarr \mytya) \myarr \mytyb) \myarr \mytyb \]
+
+ While this technique is obviously terrible in terms of human
+ usability,\footnote{With some people going as far as defining it akin
+ to an inverse Turing test.} it is much more convenient as an
+ internal representation to deal with terms mechanically---at least in
+ simple cases. Moreover, $\alpha$ renaming ceases to be an issue, and
+ term comparison is purely syntactical.
+
+ Nonetheless, more complex, more complex constructs such as pattern
+ matching put some strain on the indices and many systems end up using
+ explicit names anyway (Agda, Coq, \dots).
+
+\end{description}
+
+In the past decade or so advancements in the Haskell's type system and
+in general the spread new programming practices have enabled to make the
+second option much more amenable. \mykant\ thus takes the second path
+through the use of Edward Kmett's excellent \texttt{bound}
+library.\footnote{Available at
+\url{http://hackage.haskell.org/package/bound}.} We decribe its
+advantages but also pitfalls in the previously relatively unknown
+territory of dependent types---\texttt{bound} being created mostly to
+handle more simply typed systems.
+
+\texttt{bound} builds on two core ideas. The first is the suggestion by
+\cite{Bird1999} consists of parametrising the term type over the type of
+the variables, and `nest' the type each time we enter a scope. If we
+wanted to define a term for the untyped $\lambda$-calculus, we might
+have
+\begin{Verbatim}
+data Void
+
+data Var v = Bound | Free v
+
+data Tm v
+ = V v -- Bound variable
+ | App (Tm v) (Tm v) -- Term application
+ | Lam (Tm (Var v)) -- Abstraction
+\end{Verbatim}
+Closed terms would be of type \texttt{Tm Void}, so that there would be
+no occurrences of \texttt{V}. However, inside an abstraction, we can
+have \texttt{V Bound}, representing the bound variable, and inside a
+second abstraction we can have \texttt{V Bound} or \texttt{V (Free
+Bound)}. Thus the term $\myabs{\myb{x}}{\myabs{\myb{y}}{\myb{x}}}$ could be represented as
+\begin{Verbatim}
+Lam (Lam (Free Bound))
+\end{Verbatim}
+This allows us to reflect at the type level the `nestedness' of a type,
+and since we usually work with functions polymorphic on the parameter
+\texttt{v} it's very hard to make mistakes by putting terms of the wrong
+nestedness where they don't belong.
+
+Even more interestingly, the substitution operation is perfectly
+captured by the \verb|>>=| (bind) operator of the \texttt{Monad}
+typeclass:
+\begin{Verbatim}
+class Monad m where
+ return :: m a
+ (>>=) :: m a -> (a -> m b) -> m b
+
+instance Monad Tm where
+ -- `return'ing turns a variable into a `Tm'
+ return = V
+
+ -- `t >>= f' takes a term `t' and a mapping from variables to terms
+ -- `f' and applies `f' to all the variables in `t', replacing them
+ -- with the mapped terms.
+ V v >>= f = f v
+ App m n >>= f = App (m >>= f) (n >>= f)
+
+ -- `Lam' is the tricky case: we modify the function to work with bound
+ -- variables, so that if it encounters `Bound' it leaves it untouched
+ -- (since the mapping referred to the outer scope); if it encounters a
+ -- free variable it asks `f' for the term and then updates all the
+ -- variables to make them refer to the outer scope they were meant to
+ -- be in.
+ Lam s >>= f = Lam (s >>= bump)
+ where bump Bound = return Bound
+ bump (Free v) = f v >>= V . Free
+\end{Verbatim}
+With this in mind, we can define functions which will not only work on
+\verb|Tm|, but on any \verb|Monad|!
+\begin{Verbatim}
+-- Replaces free variable `v' with `m' in `n'.
+subst :: (Eq v, Monad m) => v -> m v -> m v -> m v
+subst v m n = n >>= \v' -> if v == v' then m else return v'
+
+-- Replace the variable bound by `s' with term `t'.
+inst :: Monad m => m v -> m (Var v) -> m v
+inst t s = do v <- s
+ case v of
+ Bound -> t
+ Free v' -> return v'
+\end{Verbatim}
+The beauty of this technique is that in a few simple function we have
+defined all the core operations in a general and `obviously correct'
+way, with the extra confidence of having the type checker looking our
+back.
+
+Moreover, if we take the top level term type to be \verb|Tm String|, we
+get for free a representation of terms with top-level, definitions;
+where closed terms contain only \verb|String| references to said
+definitions---see also \cite{McBride2004b}.
+
+What are then the pitfalls of this seemingly invincible technique? The
+most obvious impediment is the need for polymorphic recursion.
+Functions traversing terms parametrised by the variable type will have
+types such as
+\begin{Verbatim}
+-- Infer the type of a term, or return an error.
+infer :: Tm v -> Either Error (Tm v)
+\end{Verbatim}
+When traversing under a \verb|Scope| the parameter changes from \verb|v|
+to \verb|Var v|, and thus if we do not specify the type for our function explicitly
+inference will fail---type inference for polymorphic recursion being
+undecidable \citep{henglein1993type}. This causes some annoyance,
+especially in the presence of many local definitions that we would like
+to leave untyped.
+
+But the real issue is the fact that giving a type parametrised over a
+variable---say \verb|m v|---a \verb|Monad| instance means being able to
+only substitute variables for values of type \verb|m v|. This is a
+considerable inconvenience. Consider for instance the case of
+telescopes, which are a central tool to deal with contexts and other
+constructs:
+\begin{Verbatim}
+data Tele m v = End (m v) | Bind (m v) (Tele (Var v))
+type TeleTm = Tele Tm
+\end{Verbatim}
+The problem here is that what we want to substitute for variables in
+\verb|Tele m v| is \verb|m v| (probably \verb|Tm v|), not \verb|Tele m v| itself! What we need is
+\begin{Verbatim}
+bindTele :: Monad m => Tele m a -> (a -> m b) -> Tele m b
+substTele :: (Eq v, Monad m) => v -> m v -> Tele m v -> Tele m v
+instTele :: Monad m => m v -> Tele m (Var v) -> Tele m v
+\end{Verbatim}
+Not what \verb|Monad| gives us. Solving this issue in an elegant way
+has been a major sink of time and source of headaches for the author,
+who analysed some of the alternatives---most notably the work by
+\cite{weirich2011binders}---but found it impossible to give up the
+simplicity of the model above.
+
+That said, our term type is still reasonably brief, as shown in full in
+Figure \ref{fig:term}. The fact that propositions cannot be factored
+out in another data type is a consequence of the problems described
+above. However the real pain is during elaboration, where we are forced
+to treat everything as a type while we would much rather have
+telescopes. Future work would include writing a library that marries a
+nice interface similar to the one of \verb|bound| with a more flexible
+interface.
+
+\begin{figure}[t]
+{\small\begin{verbatim}-- A top-level name.
+type Id = String
+-- A data/type constructor name.
+type ConId = String
+
+-- A term, parametrised over the variable (`v') and over the reference
+-- type used in the type hierarchy (`r').
+data Tm r v
+ = V v -- Variable.
+ | Ty r -- Type, with a hierarchy reference.
+ | Lam (TmScope r v) -- Abstraction.
+ | Arr (Tm r v) (TmScope r v) -- Dependent function.
+ | App (Tm r v) (Tm r v) -- Application.
+ | Ann (Tm r v) (Tm r v) -- Annotated term.
+ -- Data constructor, the first ConId is the type constructor and
+ -- the second is the data constructor.
+ | Con ADTRec ConId ConId [Tm r v]
+ -- Data destrutor, again first ConId being the type constructor
+ -- and the second the name of the eliminator.
+ | Destr ADTRec ConId Id (Tm r v)
+ -- A type hole.
+ | Hole HoleId [Tm r v]
+ -- Decoding of propositions.
+ | Dec (Tm r v)
+
+ -- Propositions.
+ | Prop r -- The type of proofs, with hierarchy reference.
+ | Top
+ | Bot
+ | And (Tm r v) (Tm r v)
+ | Forall (Tm r v) (TmScope r v)
+ -- Heterogeneous equality.
+ | Eq (Tm r v) (Tm r v) (Tm r v) (Tm r v)
+
+-- Either a data type, or a record.
+data ADTRec = ADT | Rec
+
+-- Either a coercion, or coherence.
+data Coeh = Coe | Coh\end{verbatim}
+}
+ \caption{Data type for terms in \mykant.}
+ \label{fig:term}
+\end{figure}
+
+We also make use of a `forgetful' data type (as provided by
+\verb|bound|) to store user-provided variables names along with the
+`nameless' representation, so that the names will not be considered when
+compared terms, but will be available when distilling so that we can
+recover variable names that are as close as possible to what the user
+originally used.
+
+\subsubsection{Context}
+
+% TODO finish
\subsection{Type hierarchy}
\label{sec:hier-impl}
-\subsection{Elaboration}
+As a breath of air amongst the type gas, we will explain how to
+implement the typical ambiguity we have spoken about in
+\ref{sec:term-hierarchy}. As mentioned, we have to verify a the
+consistency of a set of constraints each time we add a new one. The
+constraints range over some set of variables whose members we will
+denote with $x, y, z, \dots$. and are of two kinds:
+\begin{center}
+ \begin{tabular}{cc}
+ $x \le y$ & $x < y$
+ \end{tabular}
+\end{center}
+
+Predictably, $\le$ expresses a reflexive order, and $<$ expresses an
+irreflexive order, both working with the same notion of equality, where
+$x < y$ implies $x \le y$---they behave like $\le$ and $<$ do on natural
+numbers (or in our case, levels in a type hierarchy). We also need an
+equality constraint ($x = y$), which can be reduced to two constraints
+$x \le y$ and $y \le x$.
+
+Given this specification, we have implemented a standalone Haskell
+module---that we plan to release as a library---to efficiently store and
+check the consistency of constraints. Its interface is shown in Figure
+\ref{fig:constraint}. The problem unpredictably reduces to a graph
+algorithm. If we
+
+\begin{figure}[t]
+{\small\begin{verbatim}module Data.Constraint where
+
+-- | Data type holding the set of constraints, parametrised over the
+-- type of the variables.
+data Constrs a
+
+-- | A representation of the constraints that we can add.
+data Constr a = a :<=: a | a :<: a | a :==: a
+
+-- | An empty set of constraints.
+empty :: Ord a => Constrs a
+
+-- | Adds one constraint to the set, returns the new set of constraints
+-- if consistent.
+addConstr :: Ord a => Constr a -> Constrs a -> Maybe (Constrs a)\end{verbatim}
+}
+
+ \caption{Interface for the module handling the constraints.}
+ \label{fig:constraint}
+\end{figure}
+
+
+\subsection{Type holes}
+
+When building up programs interactively, it is useful to leave parts
+unfinished while exploring the current context. This is what type holes
+are for.
\section{Evaluation}
\UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mytyb}$}
\end{prooftree}
-I will often present `definition' in the described calculi and in
+I will often present `definitions' in the described calculi and in
$\mykant$\ itself, like so:
-{\mysmall\[
+\[
\begin{array}{@{}l}
\myfun{name} : \mytysyn \\
\myfun{name} \myappsp \myb{arg_1} \myappsp \myb{arg_2} \myappsp \cdots \mapsto \mytmsyn
\end{array}
-\]}
+\]
To define operators, I use a mixfix notation similar
-to Agda, where $\myarg$s denote arguments, for example
-{\mysmall\[
+to Agda, where $\myarg$s denote arguments:
+\[
\begin{array}{@{}l}
\myarg \mathrel{\myfun{$\wedge$}} \myarg : \mybool \myarr \mybool \myarr \mybool \\
\myb{b_1} \mathrel{\myfun{$\wedge$}} \myb{b_2} \mapsto \cdots
\end{array}
-\]}
+\]
In explicitly typed systems, I will also omit type annotations when they
are obvious, e.g. by not annotating the type of parameters of
abstractions or of dependent pairs.
+I will also introduce multiple arguments in one go in arrow types:
+\[
+ (\myb{x}\, \myb{y} {:} \mytya) \myarr \cdots = (\myb{x} {:} \mytya) \myarr (\myb{y} {:} \mytya) \myarr \cdots
+\]
+and in abstractions:
+\[
+\myabs{\myb{x}\myappsp\myb{y}}{\cdots} = \myabs{\myb{x}}{\myabs{\myb{y}}{\cdots}}
+\]
+
\section{Code}
\subsection{ITT renditions}
then (λ _ f → (suc (f tt))) else (λ _ _ → y))
x
- List : (A : Set) → Set
- List A = W (A ∨ Unit) (λ s → Tr (fst s))
-
- [] : ∀ {A} → List A
- [] = (false , tt) ◁ absurd
-
- _∷_ : ∀ {A} → A → List A → List A
- x ∷ l = (true , x) ◁ (λ _ → l)
-
module Equality where
open ITT
}
\subsection{\mykant's hierachy}
+\label{sec:hurkens}
This rendition of the Hurken's paradox does not type check with the
hierachy enabled, type checks and loops without it. Adapted from an
projects / bitonic-mengthesis.git / commitdiff