-\documentclass[report]{article}
+\documentclass[report, 11pt]{article}
\usepackage{etex}
+\usepackage[sc,slantedGreek]{mathpazo}
+\linespread{1.05}
+% \usepackage{times}
+
+\oddsidemargin 0in
+\evensidemargin 0in
+\textheight 9.5in
+\textwidth 6.2in
+\topmargin -7mm
+\parindent 10pt
+
+
%% Narrow margins
% \usepackage{fullpage}
\newcommand{\mydesc}[3]{
\noindent
\mbox{
- \vspace{0.1cm}
\parbox{\textwidth}{
{\small
+ \vspace{0.2cm}
\hfill \textbf{#1} $#2$
\framebox[\textwidth]{
\parbox{\textwidth}{
\centering{
#3
}
- \vspace{0.1cm}
+ \vspace{0.2cm}
}
}
}
(\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
let us represent inductive data in a general (but clumsy) way. The core
idea is to
+% TODO finish
+
\section{The struggle for equality}
\label{sec:equality}
$
\myjeq{\myse{P}}{(\myapp{\myrefl}{\mytmm})}{\mytmn} \myred \mytmn
$
- \vspace{0.87cm}
+ \vspace{0.9cm}
}
\end{minipage}
\DisplayProof
}
-% \mydesc{definitional equality:}{\mytmsyn \mydefeq \mytmsyn}{
-% \begin{tabular}{cc}
-% \AxiomC{}
-% &
-% foo
-% \end{tabular}
-% }
-% \end{description}
+% TODO finish
\subsubsection{Uniqueness of identity proofs}
+% TODO finish
% TODO reference the fact that J does not imply J
% TODO mention univalence
\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.
- Consider for example
- {\small\[
- \myabss{\myb{q}}{\mytya \mypeq{\mytyp} (\mytya \myarr \mytya)}{\myhole{?}}
+ 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.
+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
\end{itemize}
Given these facts theories employing equality reflection, like NuPRL
\subsection{Some alternatives}
+% TODO finish
% TODO add `extentional axioms' (Hoffman), setoid models (Thorsten)
\section{Observational equality}
}
\mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
- \begin{tabular}{cc}
+ \begin{tabular}{ccc}
\AxiomC{\phantom{$\myjud{\myse{P}}{\myprop}$}}
\UnaryInfC{$\myjud{\mytop}{\myprop}$}
\noLine
\noLine
\UnaryInfC{\phantom{$\myjud{\mybot}{\myprop}$}}
\DisplayProof
- \end{tabular}
-
- \myderivsp
-
+ &
\AxiomC{$\myjud{\myse{A}}{\mytyp}$}
\AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\myse{P}}{\myprop}$}
\BinaryInfC{$\myjud{\myprfora{\myb{x}}{\mytya}{\myse{P}}}{\myprop}$}
+ \noLine
+ \UnaryInfC{\phantom{$\myjud{\mybot}{\myprop}$}}
\DisplayProof
+ \end{tabular}
}
Our foundation will be a type theory like the one of section
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}}}}$}
\DisplayProof
-
- \myderivsp
-
+ &
\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
frequently make use what de Bruijn called \emph{telescopes}
\citep{Bruijn91}, a construct that will prove useful when dealing with
the types of type and data constructors. A telescope is a series of
-nested typed bindings, such as $(\myb{x} {:} \mynat); (\myb{p} :
+nested typed bindings, such as $(\myb{x} {:} \mynat); (\myb{p} {:}
\myapp{\myfun{even}}{\myb{x}})$. Consistently with the notation for
contexts and term vectors, we use $\myemptyctx$ to denote an empty
telescope and $\myarg ; \myarg$ to add a new binding to an existing
\item[Ordered lists] Up to this point, the examples shown are nothing
new to the \{Haskell, SML, OCaml, functional\} programmer. However
- dependent types let us express much more than
+ dependent types let us express much more than that. A useful example
+ is the type of ordered lists. There are many ways to define such a
+ thing, we will define our type to store the bounds of the list, making
+ sure that $\mydc{cons}$ing respects that.
+
+ First, using $\myunit$ and $\myempty$, we define a type expressing the
+ ordering on natural numbers, $\myfun{le}$---`less or equal'.
+ $\myfun{le}\myappsp \mytmm \myappsp \mytmn$ will be inhabited only if
+ $\mytmm \le \mytmn$:
+ {\small\[
+ \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}}{
+ \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
+ 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
+ `open' bounds, for example for empty lists, we create a type for
+ `lifted' naturals with a bottom (less than everything) and top
+ (greater than everything) elements, along with an associated comparison
+ function:
+ {\small\[
+ \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 \\
+ \end{array}
+ \]} 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:
+ {\small\[
+ \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})
+ }
+ \end{array}
+ \]} 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}.}.
+
% TODO
\item[Dependent products] Apart from $\mysyn{data}$, $\mykant$\ offers
\section{Future work}
+\subsection{Coinduction}
+
+\subsection{Quotient types}
+
+\subsection{Partiality}
+
+\subsection{Pattern matching}
+
+\subsection{Pattern unification}
+
% TODO coinduction (obscoin, gimenez), pattern unification (miller,
% gundry), partiality monad (NAD)
projects / bitonic-mengthesis.git / commitdiff