%% -----------------------------------------------------------------------------
%% Commands
+\newcommand{\mysmall}{}
\newcommand{\mysyn}{\AgdaKeyword}
\newcommand{\mytyc}{\AgdaDatatype}
\newcommand{\mydc}{\AgdaInductiveConstructor}
\newcommand{\myapp}[2]{#1 \myappsp #2}
\newcommand{\mysynsep}{\ \ |\ \ }
\newcommand{\myITE}[3]{\myfun{If}\, #1\, \myfun{Then}\, #2\, \myfun{Else}\, #3}
+\newcommand{\mycumul}{\preceq}
\FrameSep0.2cm
\newcommand{\mydesc}[3]{
\noindent
\mbox{
\parbox{\textwidth}{
- {\small
+ {\mysmall
\vspace{0.2cm}
\hfill \textbf{#1} $#2$
\framebox[\textwidth]{
\vspace{0.2cm}
}
}
+ \vspace{0.2cm}
}
}
}
\newcommand{\mycase}[2]{\mathopen{\myfun{[}}#1\mathpunct{\myfun{,}} #2 \mathclose{\myfun{]}}}
\newcommand{\myabsurd}[1]{\myfun{absurd}_{#1}}
\newcommand{\myarg}{\_}
-\newcommand{\myderivsp}{\vspace{0.3cm}}
+\newcommand{\myderivsp}{}
+\newcommand{\myderivspp}{\vspace{0.3cm}}
\newcommand{\mytyp}{\mytyc{Type}}
\newcommand{\myneg}{\myfun{$\neg$}}
\newcommand{\myar}{\,}
\newcommand{\mydefeq}{\cong}
\newcommand{\myrefl}{\mydc{refl}}
\newcommand{\mypeq}[1]{\mathrel{\mytyc{=}_{#1}}}
-\newcommand{\myjeqq}{\myfun{=-elim}}
+\newcommand{\myjeqq}{\myfun{$=$-elim}}
\newcommand{\myjeq}[3]{\myapp{\myapp{\myapp{\myjeqq}{#1}}{#2}}{#3}}
\newcommand{\mysubst}{\myfun{subst}}
\newcommand{\myprsyn}{\myse{prop}}
-\newcommand{\myprdec}[1]{\mathopen{\mytyc{$\llbracket$}} #1 \mathopen{\mytyc{$\rrbracket$}}}
+\newcommand{\myprdec}[1]{\mathopen{\mytyc{$\llbracket$}} #1 \mathclose{\mytyc{$\rrbracket$}}}
\newcommand{\myand}{\mathrel{\mytyc{$\wedge$}}}
\newcommand{\mybigand}{\mathrel{\mytyc{$\bigwedge$}}}
\newcommand{\myprfora}[3]{\forall #1 {:} #2. #3}
\newcommand{\mytree}{\mytyc{Tree}}
\newcommand{\myproj}[1]{\myfun{$\pi_{#1}$}}
\newcommand{\mysigma}{\mytyc{$\Sigma$}}
+\newcommand{\mynegder}{\vspace{-0.3cm}}
+\newcommand{\myquot}{\Downarrow}
%% -----------------------------------------------------------------------------
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):
-{\small
+{\mysmall
\[
(\myapp{\omega}{\omega}) \myred (\myapp{\omega}{\omega}) \myred \cdots \text{, with $\omega = \myabs{x}{\myapp{x}{x}}$}
\]
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:
-{\small\[
+{\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
\DisplayProof
\end{tabular}
- \myderivsp
+ \myderivspp
\begin{tabular}{cc}
\AxiomC{$\myjud{\mytmt}{\mytya}$}
\end{tabular}
- \myderivsp
+ \myderivspp
\begin{tabular}{cc}
\AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$}
\DisplayProof
\end{tabular}
- \myderivsp
+ \myderivspp
\begin{tabular}{ccc}
\AxiomC{$\myjud{\mytmm}{\mytya}$}
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
+normalising.
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:
-{\small\[
+{\mysmall\[
(\myfix{\myb{x}}{\mytya}{\myb{x}}) : \mytya
\]}
\BinaryInfC{$\myjud{\mytmm \mycons \mytmn}{\myapp{\mylist}{\mytya}}$}
\DisplayProof
\end{tabular}
- \myderivsp
+ \myderivspp
\AxiomC{$\myjud{\mysynel{f}}{\mytya \myarr \mytyb \myarr \mytyb}$}
\AxiomC{$\myjud{\mytmm}{\mytyb}$}
\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?
+inductive data.
\section{Intuitionistic Type Theory}
\label{sec:itt}
\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:
- {\small\[\displaystyle
+ {\mysmall\[\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
\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: {\small\[\displaystyle(\myabss{\myb{A} \myar \myb{R}}{\mytyp}{(\myb{A}
+ 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\]}
\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:
- {\small\[\displaystyle(\myabss{\myb{x}}{\mybool}{\myite{\myb{x}}{\mynat}{\myrat}}) : \mybool
+ {\mysmall\[\displaystyle(\myabss{\myb{x}}{\mybool}{\myite{\myb{x}}{\mynat}{\myrat}}) : \mybool
\myarr \mytyp\]}
\end{description}
include Agda \citep{Norell2007, Bove2009}, Coq \citep{Coq}, and Epigram
\citep{McBride2004, EpigramTut}.
-\subsection{A note on inference}
-
-% TODO do this, adding links to the sections about bidi type checking and
-% implicit universes.
-In the following text I will often omit explicit typing for abstractions or
-
-Moreover, I will use $\mytyp$ without bothering to specify a
-universe, with the silent assumption that the definition is consistent
-regarding to the hierarchy.
-
\subsection{A simple type theory}
\label{sec:core-tt}
$
\end{tabular}
- \myderivsp
+ \myderivspp
$
\myrec{(\myse{s} \mynode{\myb{x}}{\myse{T}} \myse{f})}{\myb{y}}{\myse{P}}{\myse{p}} \myred
$\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
-{\small\[
+{\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
reducing terms to their normal forms before comparing them, so that a
-separate conversion rule is not needed. % TODO add section
+separate conversion rule is not needed.
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.
\UnaryInfC{$\myjud{\myfalse}{\mybool}$}
\DisplayProof
\end{tabular}
- \myderivsp
+ \myderivspp
\AxiomC{$\myjud{\mytmt}{\mybool}$}
\AxiomC{$\myjudd{\myctx : \mybool}{\mytya}{\mytyp_l}$}
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
-{\small\[\text{\texttt{if null xs then head xs else 0}}\]}
+{\mysmall\[\text{\texttt{if null xs then head xs else 0}}\]}
are a necessary, well typed, danger.
However, in a more expressive system, we can do better: the branches' type can
\BinaryInfC{$\myjud{\myfora{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
\DisplayProof
- \myderivsp
+ \myderivspp
\begin{tabular}{cc}
\AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytmt}{\mytyb}$}
For example, assuming that we have lists and natural numbers in our
language, using dependent functions we would be able to
write:
-{\small\[
+{\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 \\
\myfun{head} : (\myb{A} {:} \mytyp_0) \myarr (\myb{l} {:} \myapp{\mylist}{\myb{A}})
- \myarr \myapp{\myapp{\myfun{length}}{\myb{A}}}{\myb{l}} \mathrel{\myfun{>}} 0 \myarr
+ \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. $\myfun{>}$ is
-a function that takes two naturals and returns a type: if the lhs is
-greater then the rhs, $\myunit$ is returned, $\myempty$ otherwise. This
-way, we can express a `non-emptyness' condition in $\myfun{head}$, by
-including a proof that the length of the list argument is non-zero.
-This allows us to rule out the `empty list' case, so that we can safely
-return the first element.
+\myfun{length} is the usual polymorphic length
+function. $\myarg\myfun{$>$}\myarg$ is a function that takes two naturals
+and returns a type: if the lhs is greater then the rhs, $\myunit$ is
+returned, $\myempty$ otherwise. This way, we can express a
+`non-emptyness' condition in $\myfun{head}$, by including a proof that
+the length of the list argument is non-zero. This allows us to rule out
+the `empty list' case, so that we can safely return the first element.
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
\BinaryInfC{$\myjud{\myexi{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
\DisplayProof
- \myderivsp
+ \myderivspp
\begin{tabular}{cc}
\AxiomC{$\myjud{\mytmm}{\mytya}$}
Another perhaps more `dependent' application of products, paired with
$\mybool$, is to offer choice between different types. For example we
can easily recover disjunctions:
-{\small\[
+{\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}}} \\ \ \\
\label{sec:well-order}
\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
+ \begin{tabular}{cc}
\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
+ \end{tabular}
- \myderivsp
+ \myderivspp
\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}$}
}
Finally, the well-order type, or in short $\mytyc{W}$-type, which will
-let us represent inductive data in a general (but clumsy) way. The core
-idea is to
-
-% TODO finish
-
+let us represent inductive data in a general (but clumsy) way. We can
+form `nodes' of the shape $\mytmt \mynode{\myb{x}}{\mytyb} \myse{f} :
+\myw{\myb{x}}{\mytya}{\mytyb}$ that contain data ($\mytmt$) of type and
+one `child' for each member of $\mysub{\mytyb}{\myb{x}}{\mytmt}$. The
+$\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}.
+
+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\[
+ \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} \myfun{rec}\, \myb{x} / \myb{b}.\mynat \, \\
+ \myind{2} \myfun{with}\, \myabs{\myb{b}}{\\
+ \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
+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.
\section{The struggle for equality}
\label{sec:equality}
$
\myjeq{\myse{P}}{(\myapp{\myrefl}{\mytmm})}{\mytmn} \myred \mytmn
$
- \vspace{0.9cm}
+ \vspace{1.1cm}
}
\end{minipage}
-
+\mynegder
\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
\AxiomC{$\myjud{\mytya}{\mytyp_l}$}
\AxiomC{$\myjud{\mytmm}{\mytya}$}
\TrinaryInfC{$\myjud{\mytmm \mypeq{\mytya} \mytmn}{\mytyp_l}$}
\DisplayProof
- \myderivsp
+ \myderivspp
\begin{tabular}{cc}
\AxiomC{$\begin{array}{c}\ \\\myjud{\mytmm}{\mytya}\hspace{1.1cm}\mytmm \mydefeq \mytmn\end{array}$}
$\mytya$) and a proof of their equality
\item $\myse{q}$, a proof that two terms in $\mytya$ (say $\myse{m}$ and
$\myse{n}$) are equal
-\item and $\myse{p}$, an inhabitant of $\myse{P}$ applied to $\myse{m}$, plus
- the trivial proof by reflexivity showing that $\myse{m}$ is equal to itself
+\item and $\myse{p}$, an inhabitant of $\myse{P}$ applied to $\myse{m}$
+ twice, plus the trivial proof by reflexivity showing that $\myse{m}$
+ is equal to itself
\end{itemize}
Given these ingredients, $\myjeqq$ retuns a member of $\myse{P}$ applied to
$\mytmm$, $\mytmn$, and $\myse{q}$. In other words $\myjeqq$ takes a
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:
-{\small\[
+{\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
\end{array}
\]}
Once we have $\myfun{subst}$, we can easily prove more familiar laws regarding
-equality, such as symmetry, transitivity, and a congruence law.
-
-% TODO finish this
+equality, such as symmetry, transitivity, congruence laws, etc.
\subsection{Common extensions}
-Our definitional equality can be made larger in various ways, here we
-review some common extensions.
-
-\subsubsection{Congruence laws and $\eta$-expansion}
-
-A simple type-directed check that we can do on functions and records is
-$\eta$-expansion. We can then have
+Our definitional and propositional equalities can be enhanced in various
+ways. Obviously if we extend the definitional equality we are also
+automatically extend propositional equality, given how $\myrefl$ works.
+
+\subsubsection{$\eta$-expansion}
+\label{sec:eta-expand}
+
+A simple extension to our definitional equality is $\eta$-expansion.
+Given an abstract variable $\myb{f} : \mytya \myarr \mytyb$ the aim is
+to have that $\myb{f} \mydefeq
+\myabss{\myb{x}}{\mytya}{\myapp{\myb{f}}{\myb{x}}}$. We can achieve
+this by `expanding' terms based on their types, a process also known as
+\emph{quotation}---a term borrowed from the practice of
+\emph{normalisation by evaluation}, where we embed terms in some host
+language with an existing notion of computation, and then reify them
+back into terms, which will `smooth out' differences like the one above
+\citep{Abel2007}.
+
+The same concept applies to $\myprod$, where we expand each inhabitant
+by reconstructing it by getting its projections, so that $\myb{x}
+\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}.
+
+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
+elements of $\myunit$ or $\myempty$ are equal.
\mydesc{definitional equality:}{\myjud{\mytmm \mydefeq \mytmn}{\mytmsyn}}{
\begin{tabular}{cc}
- \AxiomC{$\myjud{f \mydefeq (\myabss{\myb{x}}{\mytya}{\myapp{\myse{g}}{\myb{x}}})}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
+ \AxiomC{$\myjudd{\myctx; \myb{y} : \mytya}{\myapp{\myse{f}}{\myb{x}} \mydefeq \myapp{\myse{g}}{\myb{x}}}{\mysub{\mytyb}{\myb{x}}{\myb{y}}}$}
\UnaryInfC{$\myjud{\myse{f} \mydefeq \myse{g}}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
\DisplayProof
&
- \AxiomC{$\myjud{\mytmm \mydefeq \mypair{\myapp{\myfst}{\mytmn}}{\myapp{\mysnd}{\mytmn}}}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
+ \AxiomC{$\myjud{\mypair{\myapp{\myfst}{\mytmm}}{\myapp{\mysnd}{\mytmm}} \mydefeq \mypair{\myapp{\myfst}{\mytmn}}{\myapp{\mysnd}{\mytmn}}}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
\UnaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\myexi{\myb{x}}{\mytya}{\mytyb}}$}
\DisplayProof
\end{tabular}
- \myderivsp
+ \myderivspp
+ \begin{tabular}{cc}
\AxiomC{$\myjud{\mytmm}{\myunit}$}
\AxiomC{$\myjud{\mytmn}{\myunit}$}
\BinaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\myunit}$}
\DisplayProof
+ &
+ \AxiomC{$\myjud{\mytmm}{\myempty}$}
+ \AxiomC{$\myjud{\mytmn}{\myempty}$}
+ \BinaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\myempty}$}
+ \DisplayProof
+ \end{tabular}
}
-% TODO finish
-
\subsubsection{Uniqueness of identity proofs}
-% TODO finish
-% TODO reference the fact that J does not imply J
-% TODO mention univalence
-
+Another common but controversial addition to propositional equality is
+the $\myfun{K}$ axiom, which essentially states that all equality proofs
+are by reflexivity.
-\mydesc{definitional equality:}{\myjud{\mytmm \mydefeq \mytmn}{\mytmsyn}}{
+\mydesc{typing:}{\myjud{\mytmm \mydefeq \mytmn}{\mytmsyn}}{
\AxiomC{$
\begin{array}{@{}c}
\myjud{\myse{P}}{\myfora{\myb{x}}{\mytya}{\myb{x} \mypeq{\mytya} \myb{x} \myarr \mytyp}} \\\
- \myjud{\myse{p}}{\myfora{\myb{x}}{\mytya}{\myse{P} \myappsp \myb{x} \myappsp \myb{x} \myappsp (\myrefl \myapp \myb{x})}} \hspace{1cm}
\myjud{\mytmt}{\mytya} \hspace{1cm}
+ \myjud{\myse{p}}{\myse{P} \myappsp \mytmt \myappsp (\myrefl \myappsp \mytmt)} \hspace{1cm}
\myjud{\myse{q}}{\mytmt \mypeq{\mytya} \mytmt}
\end{array}
$}
- \UnaryInfC{$\myjud{\myfun{K} \myappsp \myse{P} \myappsp \myse{p} \myappsp \myse{t} \myappsp \myse{q}}{\myse{P} \myappsp \mytmt \myappsp \myse{q}}$}
+ \UnaryInfC{$\myjud{\myfun{K} \myappsp \myse{P} \myappsp \myse{t} \myappsp \myse{p} \myappsp \myse{q}}{\myse{P} \myappsp \mytmt \myappsp \myse{q}}$}
\DisplayProof
}
+\cite{Hofmann1994} showed that $\myfun{K}$ is not derivable from the
+$\myjeqq$ axiom that we presented, and \cite{McBride2004} showed that it is
+needed to implement `dependent pattern matching', as first proposed by
+\cite{Coquand1992}. Thus, $\myfun{K}$ is derivable in the systems that
+implement dependent pattern matching, such as Epigram and Agda; but for
+example not in Coq.
+
+$\myfun{K}$ is controversial mainly because it is at odds with
+equalities that include computational behaviour, most notably
+Voevodsky's `Univalent Foundations', which includes a \emph{univalence}
+axiom that identifies isomorphisms between types with propositional
+equality. For example we would have two isomorphisms, and thus two
+equalities, between $\mybool$ and $\mybool$, corresponding to the two
+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}.}.
+
\subsection{Limitations}
\epigraph{\emph{Half of my time spent doing research involves thinking up clever
However this is not the case, or in other words with the tools we have we have
no term of type
-{\small\[
+{\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
}
\]}
To see why this is the case, consider the functions
-{\small\[\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,
+{\mysmall\[\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
-{\small\[
-\myfora{\myb{x}}{\mynat}{(0 \mathrel{\myfun{+}} \myb{x}) \mypeq{\mynat} (\myb{x} \mathrel{\myfun{+}} 0)}
+{\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
\item The rule is syntax directed, and the type checker is presumably expected
to come up with equality proofs when needed.
\item More worryingly, type checking becomes undecidable also because
- computing under false assumptions becomes unsafe, since we can use
- equality reflection and the conversion rule to have terms of any
- type.
- Consider for example {\small\[ \myabss{\myb{q}}{\mytya
- \mypeq{\mytyp} (\mytya \myarr \mytya)}{\myhole{?}}
- \]}
-Using the assumed proof in tandem with equality reflection we
-could easily write a classic Y combinator, sending the compiler into a
-loop. In general, we using the conversion rule
-% TODO check that this makes sense
+ computing under false assumptions becomes unsafe, since we derive any
+ equality proof and then use equality reflection and the conversion
+ rule to have terms of any type.
\end{itemize}
Given these facts theories employing equality reflection, like NuPRL
\citep{NuPRL}, carry the derivations that gave rise to each typing judgement
-to keep the systems manageable. % TODO more info, problems with that.
+to keep the systems manageable.
For all its faults, equality reflection does allow us to prove extensionality,
using the extensions we gave above. Assuming that $\myctx$ contains
-{\small\[\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}}}\]}
+{\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}}}\]}
We can then derive
\begin{prooftree}
- \small
+ \mysmall
\AxiomC{$\hspace{1.1cm}\myjudd{\myctx; \myb{x} : \myb{A}}{\myapp{\myb{q}}{\myb{x}}}{\myapp{\myb{f}}{\myb{x}} \mypeq{} \myapp{\myb{g}}{\myb{x}}}\hspace{1.1cm}$}
\RightLabel{equality reflection}
\UnaryInfC{$\myjudd{\myctx; \myb{x} : \myb{A}}{\myapp{\myb{f}}{\myb{x}} \mydefeq \myapp{\myb{g}}{\myb{x}}}{\myb{B}}$}
$
\begin{array}[t]{@{}l@{\ }l@{\ }l@{\ }l@{\ }l@{\ }c@{\ }l@{\ }}
\mycoe & \myempty & \myempty & \myse{Q} & \myse{t} & \myred & \myse{t} \\
- \mycoe & \myunit & \myunit & \myse{Q} & \mytt & \myred & \mytt \\
+ \mycoe & \myunit & \myunit & \myse{Q} & \myse{t} & \myred & \mytt \\
\mycoe & \mybool & \mybool & \myse{Q} & \mytrue & \myred & \mytrue \\
\mycoe & \mybool & \mybool & \myse{Q} & \myfalse & \myred & \myfalse \\
\mycoe & (\myexi{\myb{x_1}}{\mytya_1}{\mytyb_1}) &
& \myb{\mytmn_1} & \mapsto & \myapp{\mysnd}{\mytmt_1} : \mysub{\mytyb_1}{\myb{x_1}}{\myb{\mytmm_1}} \\
& \myb{Q_A} & \mapsto & \myapp{\myfst}{\myse{Q}} : \mytya_1 \myeq \mytya_2 \\
& \myb{\mytmm_2} & \mapsto & \mycoee{\mytya_1}{\mytya_2}{\myb{Q_A}}{\myb{\mytmm_1}} : \mytya_2 \\
- & \myb{Q_B} & \mapsto & (\myapp{\mysnd}{\myse{Q}}) \myappsp \myb{\mytmm_1} \myappsp \myb{\mytmm_2} \myappsp (\mycohh{\mytya_1}{\mytya_2}{\myb{Q_A}}{\myb{\mytmm_1}}) : \\ & & & \myprdec{\mysub{\mytyb_1}{\myb{x_1}}{\myb{\mytmm_1}} \myeq \mysub{\mytyb_2}{\myb{x_2}}{\myb{\mytmm_2}}} \\
+ & \myb{Q_B} & \mapsto & (\myapp{\mysnd}{\myse{Q}}) \myappsp \myb{\mytmm_1} \myappsp \myb{\mytmm_2} \myappsp (\mycohh{\mytya_1}{\mytya_2}{\myb{Q_A}}{\myb{\mytmm_1}}) : \myprdec{\mysub{\mytyb_1}{\myb{x_1}}{\myb{\mytmm_1}} \myeq \mysub{\mytyb_2}{\myb{x_2}}{\myb{\mytmm_2}}} \\
& \myb{\mytmn_2} & \mapsto & \mycoee{\mysub{\mytyb_1}{\myb{x_1}}{\myb{\mytmm_1}}}{\mysub{\mytyb_2}{\myb{x_2}}{\myb{\mytmm_2}}}{\myb{Q_B}}{\myb{\mytmn_1}} : \mysub{\mytyb_2}{\myb{x_2}}{\myb{\mytmm_2}} \\
\mysyn{in} & \multicolumn{3}{@{}l}{\mypair{\myb{\mytmm_2}}{\myb{\mytmn_2}}}
\end{array}} \\
\mytmt & \myred &
\cdots \\
- \mycoe & \mytya & \mytyb & \myse{Q} & \mytmt & \myred & \\
- \multicolumn{7}{l}{
- \myind{2}\myapp{\myabsurd{\mytyb}}{\myse{Q}}\ \text{if $\mytya$ and $\mytyb$ are canonical.}
- }
+ \mycoe & \mytya & \mytyb & \myse{Q} & \mytmt & \myred & \myapp{\myabsurd{\mytyb}}{\myse{Q}}\ \text{if $\mytya$ and $\mytyb$ are canonical.}
\end{array}
$
}
Figure \ref{fig:eqred} illustrates this idea in practice. For ground
types, the proof is the trivial element, and \myfun{coe} is the
-identity. For the three type binders, things are similar but subtly
-different---the choices we make in the type equality are dictated by
-the desire of writing the $\myfun{coe}$ in a natural way.
+identity. For $\myunit$, we can do better: we return its only member
+without matching on the term. For the three type binders, things are
+similar but subtly different---the choices we make in the type equality
+are dictated by the desire of writing the $\myfun{coe}$ in a natural
+way.
$\myprod$ is the easiest case: we decompose the proof into proofs that
the first element's types are equal ($\mytya_1 \myeq \mytya_2$), and a
described above. Thus, we can immediately coerce the first element of
the pair using the first element of the proof, and then instantiate the
second element with the two first elements and a proof by coherence of
-their equality, since we know that the types are equal. The cases for
-the other binders are omitted for brevity, but they follow the same
-principle.
+their equality, since we know that the types are equal.
+
+The cases for the other binders are omitted for brevity, but they follow
+the same principle with some twists to make $\myfun{coe}$ work with the
+generated proofs; the reader can refer to the paper for details.
\subsubsection{$\myfun{coe}$, laziness, and $\myfun{coh}$erence}
It is important to notice that in the reduction rules for $\myfun{coe}$
are never obstructed by the proofs: with the exception of comparisons
-between different canonical types we never pattern match on the pairs,
-but always look at the projections. This means that, as long as we are
-consistent, and thus as long as we don't have $\mybot$-inducing proofs,
-we can add propositional axioms for equality and $\myfun{coe}$ will
-still compute. Thus, we can take $\myfun{coh}$ as axiomatic, and we can
-add back familiar useful equality rules:
+between different canonical types we never `pattern match' on the proof
+pairs, but always look at the projections. This means that, as long as
+we are consistent, and thus as long as we don't have $\mybot$-inducing
+proofs, we can add propositional axioms for equality and $\myfun{coe}$
+will still compute. Thus, we can take $\myfun{coh}$ as axiomatic, and
+we can add back familiar useful equality rules:
\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
- \begin{tabular}{cc}
\AxiomC{$\myjud{\mytmt}{\mytya}$}
- \UnaryInfC{$\myjud{\myapp{\myrefl}{\mytmt}}{\myprdec{\myjm{\myb{x}}{\myb{\mytya}}{\myb{x}}{\myb{\mytya}}}}$}
+ \UnaryInfC{$\myjud{\myapp{\myrefl}{\mytmt}}{\myprdec{\myjm{\mytmt}{\mytya}{\mytmt}{\mytya}}}$}
\DisplayProof
- &
+
+ \myderivspp
+
\AxiomC{$\myjud{\mytya}{\mytyp}$}
\AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytyb}{\mytyp}$}
\BinaryInfC{$\myjud{\mytyc{R} \myappsp (\myb{x} {:} \mytya) \myappsp \mytyb}{\myfora{\myb{y}\, \myb{z}}{\mytya}{\myprdec{\myjm{\myb{y}}{\mytya}{\myb{z}}{\mytya} \myimpl \mysub{\mytyb}{\myb{x}}{\myb{y}} \myeq \mysub{\mytyb}{\myb{x}}{\myb{z}}}}}$}
\DisplayProof
- \end{tabular}
}
$\myrefl$ is the equivalent of the reflexivity rule in propositional
$
\begin{array}{r@{ }c@{\ }c@{\ }c@{}l@{\ }c@{\ }r@{}c@{\ }c@{\ }c@{}l@{\ }l}
(&\mytmt_1 & : & \myempty&) & \myeq & (&\mytmt_2 & : & \myempty &) & \myred \mytop \\
- (&\mytmt_1 & : & \myempty&) & \myeq & (&\mytmt_2 & : & \myempty&) & \myred \mytop \\
+ (&\mytmt_1 & : & \myunit&) & \myeq & (&\mytmt_2 & : & \myunit&) & \myred \mytop \\
(&\mytrue & : & \mybool&) & \myeq & (&\mytrue & : & \mybool&) & \myred \mytop \\
(&\myfalse & : & \mybool&) & \myeq & (&\myfalse & : & \mybool&) & \myred \mytop \\
- (&\mytmt_1 & : & \mybool&) & \myeq & (&\mytmt_1 & : & \mybool&) & \myred \mybot \\
+ (&\mytrue & : & \mybool&) & \myeq & (&\myfalse & : & \mybool&) & \myred \mybot \\
+ (&\myfalse & : & \mybool&) & \myeq & (&\mytrue & : & \mybool&) & \myred \mybot \\
(&\mytmt_1 & : & \myexi{\mytya_1}{\myb{x_1}}{\mytyb_1}&) & \myeq & (&\mytmt_2 & : & \myexi{\mytya_2}{\myb{x_2}}{\mytyb_2}&) & \myred \\
& \multicolumn{11}{@{}l}{
\myind{2} \myjm{\myapp{\myfst}{\mytmt_1}}{\mytya_1}{\myapp{\myfst}{\mytmt_2}}{\mytya_2} \myand
}}
} \\
(&\mytmt_1 \mynodee \myse{f}_1 & : & \myw{\mytya_1}{\myb{x_1}}{\mytyb_1}&) & \myeq & (&\mytmt_1 \mynodee \myse{f}_1 & : & \myw{\mytya_2}{\myb{x_2}}{\mytyb_2}&) & \myred \cdots \\
- (&\mytmt_1 & : & \mytya_1&) & \myeq & (&\mytmt_2 & : & \mytya_2 &) & \myred \\
- & \multicolumn{11}{@{}l}{
- \myind{2} \mybot\ \text{if $\mytya_1$ and $\mytya_2$ are canonical.}
- }
+ (&\mytmt_1 & : & \mytya_1&) & \myeq & (&\mytmt_2 & : & \mytya_2 &) & \myred \mybot\ \text{if $\mytya_1$ and $\mytya_2$ are canonical.}
\end{array}
$
}
As with type-level equality, we want value-level equality to reduce
-based on the structure of the compared terms.
-
-\subsection{Proof irrelevance}
-
-% \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}
+based on the structure of the compared terms. When matching
+propositional data, such as $\myempty$ and $\myunit$, we automatically
+return the trivial type, since if a type has zero one members, all
+members will be equal. When matching on data-bearing types, such as
+$\mybool$, we check that such data matches, and return bottom otherwise.
+
+\subsection{Proof irrelevance and stuck coercions}
+
+The last effort is required to make sure that proofs (members of
+$\myprop$) are \emph{irrelevant}. Since they are devoid of
+computational content, we would like to identify all equivalent
+propositions as the same, in a similar way as we identified all
+$\myempty$ and all $\myunit$ as the same in section
+\ref{sec:eta-expand}.
+
+Thus we will have a quotation that will not only perform
+$\eta$-expansion, but will also identify and mark proofs that could not
+be decoded (that is, equalities on neutral types). Then, when
+comparing terms, marked proofs will be considered equal without
+analysing their contents, thus gaining irrelevance.
+
+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
+$\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.
+
+This process of identifying every proof as equivalent and removing
+$\myfun{coe}$rcions is known as \emph{quotation}.
\section{\mykant : the theory}
\label{sec:kant-theory}
the basis for a more featureful system, while still presenting interesting
features and more importantly observational equality.
-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, observational
-equality is not currently implemented. However, a detailed plan on how to add
-it this functionality is provided, and should not prove to be too much work.
+We will first present the features of the system, and then describe the
+implementation we have developed in section \ref{sec:kant-practice}.
-The features currently implemented in \mykant\ are:
+The defining features of \mykant\ are:
\begin{description}
\item[Full dependent types] As we would expect, we have dependent a system
with associated primitive recursion operators; or records, with associated
projections for each field.
-\item[Bidirectional type checking] While no `fancy' inference via unification
- is present, we take advantage of an type synthesis system in the style of
- \cite{Pierce2000}, extending the concept for user defined data types.
+\item[Bidirectional type checking] While no `fancy' inference via
+ unification is present, we take advantage of a type synthesis system
+ 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.
-\end{description}
-
-The planned features are:
-\begin{description}
\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.
-
-\item[Coinductive data] ...
\end{description}
-We will analyse the features one by one, along with motivations and tradeoffs
-for the design decisions made.
+We will analyse the features one by one, along with motivations and
+tradeoffs for the design decisions made.
\subsection{Bidirectional type checking}
-We start by describing bidirectional type checking since it calls for fairly
-different typing rules that what we have seen up to now. The idea is to have
-two kind of terms: terms for which a type can always be inferred, and terms
-that need to be checked against a type. A nice observation is that this
-duality runs through the semantics of the terms: data destructors (function
-application, record projections, primitive re cursors) \emph{infer} types,
-while data constructors (abstractions, record/data types data constructors)
-need to be checked. In the literature these terms are respectively known as
+We start by describing bidirectional type checking since it calls for
+fairly different typing rules that what we have seen up to now. The
+idea is to have two kinds of terms: terms for which a type can always be
+inferred, and terms that need to be checked against a type. A nice
+observation is that this duality runs through the semantics of the
+terms: neutral terms (abstracted or defined variables, function
+application, record projections, primitive recursors, etc.) \emph{infer}
+types, canonical terms (abstractions, record/data types data
+constructors, etc.) need to be \emph{checked}.
To introduce the concept and notation, we will revisit the STLC in a
-bidirectional style. The presentation follows \cite{Loh2010}.
+bidirectional style. The presentation follows \cite{Loh2010}. The
+syntax for our bidirectional STLC is the same as the untyped
+$\lambda$-calculus, but with an extra construct to annotate terms
+explicitly---this will be necessary when having top-level canonical
+terms. The types are the same as those found in the normal STLC.
+
+\mydesc{syntax}{ }{
+ $
+ \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
+\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,
+and so are annotate terms. The type of applications is inferred too,
+propagating types down the applied term. Abstractions are checked.
+Finally, we have a rule to check the type of an inferrable term.
+
+\mydesc{typing:}{\myctx \vdash \mytmsyn \Leftrightarrow \mytmsyn}{
+ \begin{tabular}{ccc}
+ \AxiomC{$\myctx(x) = A$}
+ \UnaryInfC{$\myinf{\myb{x}}{A}$}
+ \DisplayProof
+ &
+ \AxiomC{$\myjudd{\myctx;\myb{x} : A}{\mytmt}{\mytyb}$}
+ \UnaryInfC{$\mychk{\myabs{x}{\mytmt}}{\mytyb}$}
+ \DisplayProof
+ &
+ \AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$}
+ \AxiomC{$\myjud{\mytmn}{\mytya}$}
+ \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mytyb}$}
+ \DisplayProof
+ \end{tabular}
-% TODO do this --- is it even necessary
+ \myderivspp
-% The syntax of
+ \begin{tabular}{cc}
+ \AxiomC{$\mychk{\mytmt}{\mytya}$}
+ \UnaryInfC{$\myinf{\myann{\mytmt}{\mytya}}{\mytya}$}
+ \DisplayProof
+ &
+ \AxiomC{$\myinf{\mytmt}{\mytya}$}
+ \UnaryInfC{$\mychk{\mytmt}{\mytya}$}
+ \DisplayProof
+ \end{tabular}
+}
\subsection{Base terms and types}
abstractions and $\mytyp$s. Everything else will be provided by
user-definable constructs. Since we let the user define values, we will
need a context capable of carrying the body of variables along with
-their type. Bound names and defined names are treated separately in the
-syntax, and while both can be associated to a type in the context, only
-defined names can be associated with a body:
+their type.
+
+Bound names and defined names are treated separately in the syntax, and
+while both can be associated to a type in the context, only defined
+names can be associated with a body:
\mydesc{context validity:}{\myvalid{\myctx}}{
\begin{tabular}{ccc}
\end{tabular}
}
-We can now give types to our terms. The type of names, both defined and
-abstract, is inferred. The type of applications is inferred too,
-propagating types down the applied term. Abstractions are checked.
-Finally, we have a rule to check the type of an inferrable term. We
-defer the question of term equality (which is needed for type checking)
-to section \label{sec:kant-irr}.
+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}.
\mydesc{typing:}{\myctx \vdash \mytmsyn \Leftrightarrow \mytmsyn}{
- \begin{tabular}{ccc}
+ \begin{tabular}{cccc}
\AxiomC{$\myse{name} : A \in \myctx$}
\UnaryInfC{$\myinf{\myse{name}}{A}$}
\DisplayProof
\UnaryInfC{$\myinf{\myfun{f}}{A}$}
\DisplayProof
&
+ \AxiomC{$\mychk{\mytmt}{\mytya}$}
+ \UnaryInfC{$\myinf{\myann{\mytmt}{\mytya}}{\mytya}$}
+ \DisplayProof
+ &
\AxiomC{$\myinf{\mytmt}{\mytya}$}
- \UnaryInfC{$\mychk{\myann{\mytmt}{\mytya}}{\mytya}$}
+ \UnaryInfC{$\mychk{\mytmt}{\mytya}$}
\DisplayProof
\end{tabular}
- \myderivsp
+ \myderivspp
\begin{tabular}{ccc}
\AxiomC{$\myinf{\mytmm}{\myfora{\myb{x}}{\mytya}{\mytyb}}$}
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
-{\small\[
+{\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
\]}
\myapp{\myfun{even}}{42})$.
\end{itemize}
+Additionally, when presenting syntax elaboration, I'll use $\mytmsyn^n$
+to indicate a term vector composed of $n$ elements, or
+$\mytmsyn^{\mytele}$ for one composed by as many elements as the
+telescope.
+
\subsubsection{Declarations syntax}
\mydesc{syntax}{ }{
\begin{array}{r@{\ }c@{\ }l}
\mydeclsyn & ::= & \myval{\myb{x}}{\mytmsyn}{\mytmsyn} \\
& | & \mypost{\myb{x}}{\mytmsyn} \\
- & | & \myadt{\mytyc{D}}{\mytelesyn}{}{\mydc{c} : \mytelesyn\ |\ \cdots } \\
- & | & \myreco{\mytyc{D}}{\mytelesyn}{}{\myfun{f} : \mytmsyn,\ \cdots } \\
+ & | & \myadt{\mytyc{D}}{\myappsp \mytelesyn}{}{\mydc{c} : \mytelesyn\ |\ \cdots } \\
+ & | & \myreco{\mytyc{D}}{\myappsp \mytelesyn}{}{\myfun{f} : \mytmsyn,\ \cdots } \\
\mytelesyn & ::= & \myemptytele \mysynsep \mytelesyn \mycc (\myb{x} {:} \mytmsyn) \\
\mynamesyn & ::= & \cdots \mysynsep \mytyc{D} \mysynsep \mytyc{D}.\mydc{c} \mysynsep \mytyc{D}.\myfun{f}
\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}$):
- {\small\[
+ {\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:
- {\small\[\text{\texttt{data Nat = Zero | Suc Nat}}\]}
+ {\mysmall\[\text{\texttt{data Nat = Zero | Suc Nat}}\]}
Once the data type is defined, $\mykant$\ will generate syntactic
constructs for the type and data constructors, so that we will have
\begin{center}
- \small
+ \mysmall
\begin{tabular}{ccc}
\AxiomC{\phantom{$\mychk{\mytmt}{\mynat}$}}
\UnaryInfC{$\myinf{\mynat}{\mytyp}$}
natural numbers: If we have $\mytmt : \mynat$, we can destruct
$\mytmt$ using the generated eliminator `$\mynat.\myfun{elim}$':
\begin{prooftree}
- \small
+ \mysmall
\AxiomC{$\mychk{\mytmt}{\mynat}$}
\UnaryInfC{$
\myinf{\mytyc{\mynat}.\myfun{elim} \myappsp \mytmt}{
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:
- {\small\[
+ {\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
- {\small\[
+ {\mysmall\[
\begin{array}{@{}l}
\text{\texttt{elim :: Nat -> a -> (Nat -> a -> a) -> a}}\\
\text{\texttt{elim Zero pz ps = pz}}\\
\end{array}
\]}
Which buys us the computational behaviour, but not the reasoning power.
- % TODO maybe more examples, e.g. Haskell eliminator and fibonacci
\item[Binary trees] Now for a polymorphic data type: binary trees, since
lists are too similar to natural numbers to be interesting.
- {\small\[
+ {\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}})
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:
- {\small\[
+ {\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}}}
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
- {\small\[
+ {\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
parameter from the type that the term gets checked against, much like
we get the type of abstraction arguments:
\begin{center}
- \small
+ \mysmall
\begin{tabular}{cc}
\AxiomC{$\mychk{\mytya}{\mytyp}$}
\UnaryInfC{$\mychk{\mydc{leaf}}{\myapp{\mytree}{\mytya}}$}
\end{tabular}
\end{center}
Which enables us to write, much more concisely
- {\small\[
+ {\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:
\begin{prooftree}
- \footnotesize
+ \small
\AxiomC{$\myinf{\mytmt}{\myapp{\mytree}{\mytya}}$}
\UnaryInfC{$
\myinf{\mytree.\myfun{elim} \myappsp \mytmt}{
\item[Empty type] We have presented types that have at least one
constructors, but nothing prevents us from defining types with
\emph{no} constructors:
- {\small\[
+ {\mysmall\[
\myadt{\mytyc{Empty}}{ }{ }{ }
\]}
What shall the `induction principle' on $\mytyc{Empty}$ be? Does it
$\mykant$\ does not care, and generates an eliminator with no `cases',
and thus corresponding to the $\myfun{absurd}$ that we know and love:
\begin{prooftree}
- \small
+ \mysmall
\AxiomC{$\myinf{\mytmt}{\mytyc{Empty}}$}
\UnaryInfC{$\myinf{\myempty.\myfun{elim} \myappsp \mytmt}{(\myb{P} {:} \mytmt \myarr \mytyp) \myarr \myapp{\myb{P}}{\mytmt}}$}
\end{prooftree}
ordering on natural numbers, $\myfun{le}$---`less or equal'.
$\myfun{le}\myappsp \mytmm \myappsp \mytmn$ will be inhabited only if
$\mytmm \le \mytmn$:
- {\small\[
+ {\mysmall\[
\begin{array}{@{}l}
- \myfun{le} : \mynat \myarr \mynat \myarr \mytyp \mapsto \\
- \myind{2} \myabs{\myb{n}}{\\
- \myind{2}\myind{2} \mynat.\myfun{elim} \\
- \myind{2}\myind{2}\myind{2} \myb{n} \\
- \myind{2}\myind{2}\myind{2} (\myabs{\myarg}{\mynat \myarr \mytyp}) \\
- \myind{2}\myind{2}\myind{2} (\myabs{\myarg}{\myunit}) \\
- \myind{2}\myind{2}\myind{2} (\myabs{\myb{n}\, \myb{f}\, \myb{m}}{
+ \myfun{le} : \mynat \myarr \mynat \myarr \mytyp \\
+ \myfun{le} \myappsp \myb{n} \mapsto \\
+ \myind{2} \mynat.\myfun{elim} \\
+ \myind{2}\myind{2} \myb{n} \\
+ \myind{2}\myind{2} (\myabs{\myarg}{\mynat \myarr \mytyp}) \\
+ \myind{2}\myind{2} (\myabs{\myarg}{\myunit}) \\
+ \myind{2}\myind{2} (\myabs{\myb{n}\, \myb{f}\, \myb{m}}{
\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
number in less or equal than zero), $\myempty$ if the first number is
`lifted' naturals with a bottom (less than everything) and top
(greater than everything) elements, along with an associated comparison
function:
- {\small\[
+ {\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 \mapsto \cdots \\
+ \myfun{le'} : \mytyc{Lift} \myarr \mytyc{Lift} \myarr \mytyp\\
+ \myfun{le'} \myappsp \myb{l_1} \mapsto \\
+ \myind{2} \mytyc{Lift}.\myfun{elim} \\
+ \myind{2}\myind{2} \myb{l_1} \\
+ \myind{2}\myind{2} (\myabs{\myarg}{\mytyc{Lift} \myarr \mytyp}) \\
+ \myind{2}\myind{2} (\myabs{\myarg}{\myunit}) \\
+ \myind{2}\myind{2} (\myabs{\myb{n_1}\, \myb{n_2}}{
+ \mytyc{Lift}.\myfun{elim} \myappsp \myb{l_2} \myappsp (\myabs{\myarg}{\mytyp}) \myappsp \myempty \myappsp (\myabs{\myb{n_2}}{\myfun{le} \myappsp \myb{n_1} \myappsp \myb{n_2}}) \myappsp \myunit
+ }) \\
+ \myind{2}\myind{2} (\myabs{\myb{n_1}\, \myb{n_2}}{
+ \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
parametrised over two values representing the lower and upper bounds
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:
- {\small\[
+ {\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 (\myfun{le'} \myappsp \myb{low} \myappsp (\myfun{lift} \myappsp \myb{n})
+ \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
\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}.}.
-
- % TODO
\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:
- {\small\[
+ {\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}
(the destructors of the record) infer the type, while the constructor
gets checked:
\begin{center}
- \small
+ \mysmall
\begin{tabular}{cc}
\AxiomC{$\mychk{\mytmm}{\mytya}$}
\AxiomC{$\mychk{\mytmn}{\myapp{\mytyb}{\mytmm}}$}
\end{description}
\begin{figure}[p]
- \begin{subfigure}[b]{\textwidth}
- \vspace{-1cm}
\mydesc{syntax}{ }{
\footnotesize
$
$
}
+ \mynegder
+
\mydesc{syntax elaboration:}{\mydeclsyn \myelabf \mytmsyn ::= \cdots}{
\footnotesize
$
$
}
+ \mynegder
+
\mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
\footnotesize
}
+ \mynegder
+
\mydesc{reduction elaboration:}{\mydeclsyn \myelabf \myctx \vdash \mytmsyn \myred \mytmsyn}{
\footnotesize
$\myadt{\mytyc{D}}{\mytele}{}{ \cdots \ |\ \mydc{c}_n : \mytele_n } \ \ \myelabf$
\end{array}
$
}
- \end{subfigure}
- \begin{subfigure}[b]{\textwidth}
+ \mynegder
+
\mydesc{syntax elaboration:}{\myelab{\mydeclsyn}{\mytmsyn ::= \cdots}}{
\footnotesize
$
$
}
+ \mynegder
\mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
\footnotesize
\DisplayProof
}
+ \mynegder
+
\mydesc{reduction elaboration:}{\mydeclsyn \myelabf \myctx \vdash \mytmsyn \myred \mytmsyn}{
\footnotesize
$\myreco{\mytyc{D}}{\mytele}{}{ \cdots, \myfun{f}_n : \myse{F}_n } \ \ \myelabf$
\DisplayProof
}
- \end{subfigure}
\caption{Elaboration for data types and records.}
\label{fig:elab}
\end{figure}
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 % TODO add section
+$\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.
destructors, we store their types in full in the context, and then
instantiate when due:
-\mydesc{typing:}{ }{
+\mydesc{typing:}{\myctx \vdash \mytmsyn \Leftrightarrow \mytmsyn}{
\AxiomC{$
\begin{array}{c}
\mytyc{D} : \mytele \myarr \mytyp \in \myctx \hspace{1cm}
\UnaryInfC{$\mychk{\myapp{\mytyc{D}.\mydc{c}}{\vec{t}}}{\myapp{\mytyc{D}}{\vec{A}}}$}
\DisplayProof
- \myderivsp
+ \myderivspp
\AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
\AxiomC{$\mytyc{D}.\myfun{f} : \mytele \mycc (\myb{x} {:}
considerable burden on the user, on various levels. Consider for
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 two $\mytyp_0$, or
-$\mytyp_{42}$? Our definition would fail us, since $\mytyp_0 :
-\mytyp_1$.
+What if we wanted to form a disjunction containing something a
+$\mytyp_1$, or $\mytyp_{42}$? Our definition would fail us, since
+$\mytyp_1 : \mytyp_2$.
+
+\begin{figure}[b!]
+
+ % 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$}
+ \DisplayProof
+ &
+ \AxiomC{\phantom{$\myctx \vdash \mytya \mydefeq \mytyb$}}
+ \UnaryInfC{$\myctx \vdash \mytyp_l \mycumul \mytyp_{l+1}$}
+ \DisplayProof
+ &
+ \AxiomC{$\myctx \vdash \mytya \mycumul \mytyb$}
+ \AxiomC{$\myctx \vdash \mytyb \mycumul \myse{C}$}
+ \BinaryInfC{$\myctx \vdash \mytya \mycumul \myse{C}$}
+ \DisplayProof
+ \end{tabular}
+
+ \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}$}
+ \DisplayProof
+ &
+ \AxiomC{$\myctx \vdash \mytya \mycumul \mytyb$}
+ \AxiomC{$\myctx \vdash \mytyb \mycumul \myse{C}$}
+ \BinaryInfC{$\myctx \vdash \mytya \mycumul \myse{C}$}
+ \DisplayProof
+ \end{tabular}
+}
+\caption{Cumulativity rules for \mykant, plus a `conversion' rule for
+ cumulative types.}
+ \label{fig:cumulativity}
+\end{figure}
One way to solve this issue is a \emph{cumulative} hierarchy, where
$\mytyp_{l_1} : \mytyp_{l_2}$ iff $l_1 < l_2$. This way we retain
consistency, while allowing for `large' definitions that work on small
-types too. For example we might define our disjunction to be
-{\small\[
+types too. Figure \ref{fig:cumulativity} gives a formal definition of
+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
chosen by Agda, where levels can be quantified so that the relationship
between arguments and result in type formers can be explicitly
expressed:
-{\small\[
+{\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.
+% \begin{figure}[t]
+% % TODO do this
+% \caption{Constraints generated by the typical ambiguity engine. We
+% assume some global set of constraints with the ability of generating
+% fresh references.}
+% \label{fig:hierarchy}
+% \end{figure}
+
\subsection{Observational equality, \mykant\ style}
There are two correlated differences between $\mykant$\ and the theory
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
-follow his footsteps. Most of the work, as an extension of elaboration,
-is to generate reduction rules and coercions.
+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
+constructors.
\subsubsection{The \mykant\ prelude, and $\myprop$ositions}
Before defining $\myprop$, we define some basic types inside $\mykant$,
as the target for the $\myprop$ decoder:
-\begin{framed}
-\small
-$
+{\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}
-$
-\end{framed}
+\]}
When using $\mytyc{Prod}$, we shall use $\myprod$ to define `nested'
products, and $\myproj{n}$ to project elements from them, so that
-{\small
+{\mysmall
\[
\begin{array}{@{}l}
\mytya \myprod \mytyb = \mytyc{Prod} \myappsp \mytya \myappsp (\mytyc{Prod} \myappsp \mytyb \myappsp \myunit) \\
\end{tabular}
}
-\subsubsection{Why $\myprop$?}
+Adopting the same convention as with $\mytyp$-level products, we will
+nest $\myand$ in the same way.
-It is worth to ask if $\myprop$ is needed at all. It is perfectly
-possible to have the type checker identify propositional types
-automatically, and in fact that is what The author initially planned to
-identify the propositional fragment internally \cite{Jacobs1994}.
-
-% TODO finish
-
-\subsubsection{OTT constructs}
+\subsubsection{Some OTT examples}
Before presenting the direction that $\mykant$\ takes, let's consider
some examples of use-defined data types, and the result we would expect,
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: {\small\[
+ avoid confusion with the $\mytyc{Prod}$ in the prelude: {\mysmall\[
\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
- {\small\[
+ {\mysmall\[
\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}}}
provides the solution to simplify the equality above.
If we take, just like we saw previously in OTT
- {\small\[
+ {\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}{
}}
\end{array}
\]} Then we can simply take
- {\small\[
+ {\mysmall\[
\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}
\item[Lists] Now for finite lists, which will give us a taste for data
constructors:
- {\small\[
+ {\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:
- {\small\[
+ {\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: {\small\[
+ the proof for the inductive occurrence: {\mysmall\[
\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 & \\
\end{array}
\]} Value equality is unsurprising---we match the constructors, and
return bottom for mismatches. However, we also need to equate the
- parameter in $\mydc{nil}$: {\small\[
+ parameter in $\mydc{nil}$: {\mysmall\[
\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 \\
Finally, quotation
% TODO quotation
-
-
+\item[Evil type]
+ Now for something useless but complicated.
\end{description}
-
+\subsubsection{Only one equality}
+
+Given the examples above, a more `flexible' heterogeneous emerged, since
+of the fact that in $\mykant$ we re-gain the possibility of abstracting
+and in general handling sets in a way that was not possible in the
+original OTT presentation. Moreover, we found that the rules for value
+equality work very well if used with user defined type
+abstractions---for example in the case of dependent products we recover
+the original definition with explicit binders, in a very simple manner.
+
+In fact, we can drop a separate notion of type-equality, which will
+simply be served by $\myjm{\mytya}{\mytyp}{\mytyb}{\mytyp}$, from now on
+abbreviated as $\mytya \myeq \mytyb$. We shall still distinguish
+equalities relating types for hierarchical purposes. The full rules for
+equality reductions, along with the syntax for propositions, are given
+in figure \ref{fig:kant-eq-red}. We exploit record to perform
+$\eta$-expansion. Moreover, given the nested $\myand$s, values of data
+types with zero constructors (such as $\myempty$) and records with zero
+destructors (such as $\myunit$) will be automatically always identified
+as equal.
+
+\begin{figure}[p]
\mydesc{syntax}{ }{
+ \small
$
\begin{array}{r@{\ }c@{\ }l}
- \mytmsyn & ::= & \cdots \mysynsep \mycoee{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \mysynsep
- \mycohh{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
\myprsyn & ::= & \cdots \mysynsep \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
\end{array}
$
}
-\begin{figure}[p]
-\mydesc{typing:}{\myctx \vdash \myprsyn \myred \myprsyn}{
- \footnotesize
- \begin{tabular}{cc}
- \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
- \AxiomC{$\myjud{\mytmt}{\mytya}$}
- \BinaryInfC{$\myjud{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}$}
- \DisplayProof
- &
- \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
- \AxiomC{$\myjud{\mytmt}{\mytya}$}
- \BinaryInfC{$\myjud{\mycohh{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\myprdec{\myjm{\mytmt}{\mytya}{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}}}$}
- \DisplayProof
- \end{tabular}
-}
+ % \mytmsyn & ::= & \cdots \mysynsep \mycoee{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \mysynsep
+ % \mycohh{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
+ % \myprsyn & ::= & \cdots \mysynsep \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
+
+% \mynegder
+
+% \mydesc{typing:}{\myctx \vdash \mytmsyn \Leftrightarrow \mytmsyn}{
+% \small
+% \begin{tabular}{cc}
+% \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
+% \AxiomC{$\myjud{\mytmt}{\mytya}$}
+% \BinaryInfC{$\myinf{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}$}
+% \DisplayProof
+% &
+% \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
+% \AxiomC{$\myjud{\mytmt}{\mytya}$}
+% \BinaryInfC{$\myinf{\mycohh{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\myprdec{\myjm{\mytmt}{\mytya}{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}}}$}
+% \DisplayProof
+% \end{tabular}
+% }
+
+\mynegder
+
\mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
- \footnotesize
+ \small
\begin{tabular}{cc}
\AxiomC{\phantom{$\myjud{\myse{P}}{\myprop}$}}
\UnaryInfC{$\myjud{\mytop}{\myprop}$}
\DisplayProof
\end{tabular}
- \myderivsp
+ \myderivspp
\begin{tabular}{cc}
\AxiomC{$
\DisplayProof
\end{tabular}
}
+
+\mynegder
% TODO equality for decodings
\mydesc{equality reduction:}{\myctx \vdash \myprsyn \myred \myprsyn}{
- \footnotesize
+ \small
+ \begin{tabular}{cc}
\AxiomC{}
\UnaryInfC{$\myctx \vdash \myjm{\mytyp}{\mytyp}{\mytyp}{\mytyp} \myred \mytop$}
\DisplayProof
+ &
+ \AxiomC{}
+ \UnaryInfC{$\myctx \vdash \myjm{\myprdec{\myse{P}}}{\mytyp}{\myprdec{\myse{Q}}}{\mytyp} \myred \mytop$}
+ \DisplayProof
+ \end{tabular}
- \myderivsp
+ \myderivspp
\AxiomC{}
\UnaryInfC{$
\myctx \vdash &
\myjm{\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}}{\mytyp}{\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}}{\mytyp} \myred \\
& \myind{2} \mytya_2 \myeq \mytya_1 \myand \myprfora{\myb{x_2}}{\mytya_2}{\myprfora{\myb{x_1}}{\mytya_1}{
- \myjm{\myb{x_2}}{\mytya_2}{\myb{x_1}}{\mytya_1} \myimpl \mytyb_1 \myeq \mytyb_2
+ \myjm{\myb{x_2}}{\mytya_2}{\myb{x_1}}{\mytya_1} \myimpl \mytyb_1[\myb{x_1}] \myeq \mytyb_2[\myb{x_2}]
}}
\end{array}
$}
\DisplayProof
- \myderivsp
+ \myderivspp
\AxiomC{}
\UnaryInfC{$
\DisplayProof
- \myderivsp
+ \myderivspp
\AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
\UnaryInfC{$
$}
\DisplayProof
- \myderivsp
+ \myderivspp
\AxiomC{$
\begin{array}{@{}c}
\mydataty(\mytyc{D}, \myctx)\hspace{0.8cm}
- \mytyc{D}.\mydc{c} : \mytele;\mytele' \myarr \mytyc{D} \myappsp \mytelee \in \myctx \\
+ \mytyc{D}.\mydc{c} : \mytele;\mytele' \myarr \mytyc{D} \myappsp \mytelee \in \myctx \hspace{0.8cm}
\mytele_A = (\mytele;\mytele')\vec{A}\hspace{0.8cm}
\mytele_B = (\mytele;\mytele')\vec{B}
\end{array}
$}
\DisplayProof
- \myderivsp
+ \myderivspp
\AxiomC{$\mydataty(\mytyc{D}, \myctx)$}
\UnaryInfC{$
$}
\DisplayProof
- \myderivsp
+ \myderivspp
\AxiomC{$
\begin{array}{@{}c}
$}
\DisplayProof
- \myderivsp
+ \myderivspp
\AxiomC{}
\UnaryInfC{$\myjm{\mytmm}{\mytya}{\mytmn}{\mytyb} \myred \mybot\ \text{if $\mytya$ and $\mytyb$ are canonical types.}$}
\DisplayProof
}
- \caption{Equality reduction for $\mykant$.}
+\caption{Propositions and equality reduction in $\mykant$. We assume
+ the presence of $\mydataty$ and $\myisreco$ as operations on the
+ context to recognise whether a user defined type is a data type or a
+ record.}
\label{fig:kant-eq-red}
\end{figure}
+\subsubsection{Coercions}
+
+% \begin{figure}[t]
+% \mydesc{reduction}{\mytmsyn \myred \mytmsyn}{
+
+% }
+% \caption{Coercions in \mykant.}
+% \label{fig:kant-coe}
+% \end{figure}
+
+% TODO finish
+
\subsubsection{$\myprop$ and the hierarchy}
-Where is $\myprop$ placed in the $\mytyp$ hierarchy? At each universe
-level, we will have that
+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\[
+ \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
+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
+that we had explicit, non cumulative levels, it would be tempting to have
+\begin{center}
+\begin{tabular}{cc}
+ \AxiomC{$\myjud{\myse{Q}}{\myprop_l}$}
+ \UnaryInfC{$\myjud{\myprdec{\myse{Q}}}{\mytyp_l}$}
+ \DisplayProof
+&
+ \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
+ \AxiomC{$\myjud{\mytyb}{\mytyp_l}$}
+ \BinaryInfC{$\myjud{\myjm{\mytya}{\mytyp_{l}}{\mytyb}{\mytyp_{l}}}{\myprop_l}$}
+ \DisplayProof
+\end{tabular}
+\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\[
+ \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:
+\begin{prooftree}
+ \AxiomC{$\myjud{\mytmm}{\mytya}$}
+ \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
+ \AxiomC{$\myjud{\mytmn}{\mytyb}$}
+ \AxiomC{$\myjud{\mytyb}{\mytyp_l}$}
+ \QuaternaryInfC{$\myjud{\myjm{\mytmm}{\mytya}{\mytmm}{\mytya}}{\myprop_l}$}
+\end{prooftree}
+This is disappointing, since type equalities will be needlessly large:
+$\myprdec{\myjm{\mytya}{\mytyp_l}{\mytyb}{\mytyp_l}} : \mytyp_{l + 1}$.
+
+However, considering that our theory is cumulative, we can do better.
+Assuming rules for $\myprop$ cumulativity similar to the ones for
+$\mytyp$, we will have (with the conversion rule reproduced as a
+reminder):
+\begin{center}
+ \begin{tabular}{cc}
+ \AxiomC{$\myctx \vdash \mytya \mycumul \mytyb$}
+ \AxiomC{$\myjud{\mytmt}{\mytya}$}
+ \BinaryInfC{$\myjud{\mytmt}{\mytyb}$}
+ \DisplayProof
+ &
+ \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
+ \AxiomC{$\myjud{\mytyb}{\mytyp_l}$}
+ \BinaryInfC{$\myjud{\myjm{\mytya}{\mytyp_{l}}{\mytyb}{\mytyp_{l}}}{\myprop_l}$}
+ \DisplayProof
+ \end{tabular}
+
+ \myderivspp
+
+ \AxiomC{$\myjud{\mytmm}{\mytya}$}
+ \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
+ \AxiomC{$\myjud{\mytmn}{\mytyb}$}
+ \AxiomC{$\myjud{\mytyb}{\mytyp_l}$}
+ \AxiomC{$\mytya$ and $\mytyb$ are not $\mytyp_{l'}$}
+ \QuinaryInfC{$\myjud{\myjm{\mytmm}{\mytya}{\mytmm}{\mytya}}{\myprop_l}$}
+ \DisplayProof
+\end{center}
+
+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\[
+ \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}
+\label{sec:kant-irr}
+
+% \begin{figure}[t]
+% \mydesc{reduction}{\mytmsyn \myred \mytmsyn}{
+
+% }
+% \caption{Quotation in \mykant.}
+% \label{fig:kant-quot}
+% \end{figure}
-\subsubsection{Quotation and irrelevance}
-\ref{sec:kant-irr}
+% TODO finish
+
+\subsubsection{Why $\myprop$?}
+
+It is worth to ask if $\myprop$ is needed at all. It is perfectly
+possible to have the type checker identify propositional types
+automatically, and in fact in some sense we already do during equality
+reduction and quotation. However, this has the considerable
+disadvantage that we can never identify abstracted
+variables\footnote{And in general neutral terms, although we currently
+ don't have neutral propositions.} of type $\mytyp$ as $\myprop$, thus
+forbidding the user to talk about $\myprop$ explicitly.
+
+This is a considerable impediment, for example when implementing
+\emph{quotient types}. With quotients, we let the user specify an
+equivalence class over a certain type, and then exploit this in various
+way---crucially, we need to be sure that the equivalence given is
+propositional, a fact which prevented the use of quotients in dependent
+type theories \citep{Jacobs1994}.
-foo
+% TODO finish
+
+\subsection{Type holes}
\section{\mykant : The practice}
\label{sec:kant-practice}
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
+should not prove to be too much work.
+
The interaction happens in a read-eval-print loop (REPL). The REPL is a
available both as a commandline application and in a web interface,
which is available at \url{kant.mazzo.li} and presents itself as in
\end{description}
\begin{figure}
- \centering{\small
+ \centering{\mysmall
\tikzstyle{block} = [rectangle, draw, text width=5em, text centered, rounded
corners, minimum height=2.5em, node distance=0.7cm]
\subsection{Pattern unification}
-% TODO coinduction (obscoin, gimenez), pattern unification (miller,
+% TODO coinduction (obscoin, gimenez, jacobs), pattern unification (miller,
% gundry), partiality monad (NAD)
\appendix
I will often present `definition' in the described calculi and in
$\mykant$\ itself, like so:
-{\small\[
+{\mysmall\[
\begin{array}{@{}l}
\myfun{name} : \mytysyn \\
\myfun{name} \myappsp \myb{arg_1} \myappsp \myb{arg_2} \myappsp \cdots \mapsto \mytmsyn
\]}
To define operators, I use a mixfix notation similar
to Agda, where $\myarg$s denote arguments, for example
-{\small\[
+{\mysmall\[
\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.
+
\section{Code}
\subsection{ITT renditions}
_∷_ : ∀ {A} → A → List A → List A
x ∷ l = (true , x) ◁ (λ _ → l)
- _++_ : ∀ {A} → List A → List A → List A
- l₁ ++ l₂ = rec
- (λ _ → List _ → List _)
- (λ s f c l → {!!})
- l₁ l₂
-
module Equality where
open ITT
projects / bitonic-mengthesis.git / commitdiff