\AtBeginSubsubsection{\frame{\subsubsectionpage}}
\beamertemplatenavigationsymbolsempty
+\usepackage{centernot}
+\usepackage{cancel}
+\usepackage{tikz}
+\usetikzlibrary{shapes,arrows,positioning}
+\usetikzlibrary{intersections}
+\pgfdeclarelayer{background}
+\pgfdeclarelayer{foreground}
+\pgfsetlayers{background,main,foreground}
+
+
\setlength{\parindent}{0pt}
\setlength{\parskip}{6pt plus 2pt minus 1pt}
\setlength{\emergencystretch}{3em} % prevent overfull lines
\newcommand{\myb}[1]{\AgdaBound{$#1$}}
\newcommand{\myfield}{\AgdaField}
\newcommand{\myind}{\AgdaIndent}
-\newcommand{\mykant}{\textmd{\textsc{Bertus}}}
+\newcommand{\mykant}{{\rmfamily\scshape Bertus}}
\newcommand{\mysynel}[1]{#1}
\newcommand{\myse}{\mysynel}
\newcommand{\mytmsyn}{\langle t \rangle}
\newcommand{\mytermi}[1]{\text{\texttt{#1}}}
\newcommand{\mysee}[1]{\langle\myse{#1}\rangle}
\newcommand{\mycomp}{\mathbin{\myfun{$\circ$}}}
-\newcommand{\mylist}[1]{\mathopen{\mytyc{$[$}} #1 \mathclose{\mytyc{$]$}}}
+\newcommand{\mylist}[1]{\mytyc{List}\myappsp #1}
\newcommand{\mylistt}[1]{\mathopen{\mydc{$[$}} #1 \mathclose{\mydc{$]$}}}
\newcommand{\myplus}{\mathbin{\myfun{$+$}}}
\newcommand{\mytimes}{\mathbin{\myfun{$*$}}}
+\newcommand{\mysuc}{\mydc{suc}}
+\newcommand{\myzero}{\mydc{zero}}
\renewcommand{\[}{\begin{equation*}}
\renewcommand{\]}{\end{equation*}}
\begin{document}
\frame{\titlepage}
+\begin{frame}
+ \frametitle{\mykant?}
+
+ \mykant\ is an \emph{interactive theorem prover}/\emph{functional
+ programming language}, implemented in Haskell.
+
+ It is in the tradition of Agda and Epigram (and to a lesser extent
+ Coq), but with a more powerful notion of \emph{equality}.
+
+ We have figured out theory of \mykant, and have a near-complete
+ implementation.
+\end{frame}
+
\begin{frame}
\frametitle{Theorem provers are short-sighted}
\end{frame}
\begin{frame}
- \frametitle{Observational equality and \mykant}
+ \frametitle{\mykant\ and observational equality}
+
+ \emph{Observational} equality solves this and other annoyances.
- \emph{Observational equality} is a solution to this and other equality
- annoyances.
+ \mykant\ is a system aiming at making observational equality more
+ usable.
+\end{frame}
- \mykant\ is a system making observational equality more usable.
+\begin{frame}
+ \frametitle{Theorem provers, dependent types}
+ \begin{center}
+ \Huge
+ types $\leftrightarrow$ propositions
- The theory of \mykant\ is complete, the practice, not quite.
+ programs $\leftrightarrow$ proofs
+ \end{center}
\end{frame}
\begin{frame}
- \frametitle{Theorem provers, dependent types} First class types: we
- can return them, have them as arguments, etc.
+ \frametitle{Theorem provers, dependent types}
\[
- \begin{array}{@{}l@{\ }l@{\ \ \ }l}
- \mysyn{data}\ \myempty & & \text{No members.} \\
- \mysyn{data}\ \myunit & = \mytt & \text{One member.} \\
- \mysyn{data}\ \mynat & = \mydc{zero} \mydcsep \mydc{suc}\myappsp\mynat & \text{Natural numbers.}
+ \begin{array}{@{}l@{\ \ \ }l}
+ \mysyn{data}\ \myempty & \text{No members.} \\
+ \mysyn{data}\ \myunit \mapsto \mytt & \text{One member.}
\end{array}
\]
- $\myempty : \mytyp$, $\myunit : \mytyp$, $\mynat : \mytyp$.
$\myunit$ is trivially inhabitable: it corresponds to $\top$ in
logic.
-
+ \[
+ \mytt : \myunit
+ \]
$\myempty$ is \emph{not} inhabitable: it corresponds to $\bot$.
+ \[
+ \myfun{absurd} : \myempty \myarr \myb{A}
+ \]
+ First class types: we can return them, have them as arguments, etc:
+ $\myempty : \mytyp$, $\myunit : \mytyp$.
\end{frame}
\begin{frame}
\frametitle{Theorem provers, dependent types}
-
- We can express relations:
+ \[ \mysyn{data}\ \mylist{\myb{A}} \mapsto \mynil \mydcsep \myb{A} \mycons \mylist{\myb{A}} \]
+ We want to express a `non-emptiness' property for lists:
\[
\begin{array}{@{}l}
- (\myfun{${>}$}) : \mynat \myarr \mynat \myarr \mytyp \\
- \begin{array}{@{}c@{\,}c@{\,}c@{\ }l}
- \mydc{zero} & \mathrel{\myfun{$>$}} & \myb{m} & = \myempty \\
- \myb{n} & \mathrel{\myfun{$>$}} & \mydc{zero} & = \myunit \\
- (\mydc{suc} \myappsp \myb{n}) & \mathrel{\myfun{$>$}} & (\mydc{suc} \myappsp \myb{m}) & = \myb{n} \mathrel{\myfun{$>$}} \myb{m}
+ \myfun{non-empty} : \mylist{\myb{A}} \myarr \mytyp \\
+ \begin{array}{@{}l@{\myappsp}c@{\ }l}
+ \myfun{non-empty} & \mynil & \mapsto \myempty \\
+ \myfun{non-empty} & (\myb{x} \mycons \myb{l}) & \mapsto \myunit
\end{array}
\end{array}
\]
- A term of type $\myb{m} \mathrel{\myfun{$>$}} \myb{n}$ represents a
- \emph{proof} that $\myb{n}$ is indeed greater than $\myb{n}$.
+ A term of type $\myfun{non-empty} \myappsp \myb{l}$ represents a
+ \emph{proof} that $\myb{l}$ is indeed not empty.
\[
- \begin{array}{@{}l}
- 3 \mathrel{\myfun{$>$}} 1 \myred \myunit \\
- 2 \mathrel{\myfun{$>$}} 2 \myred \myempty \\
- 0 \mathrel{\myfun{$>$}} \myb{m} \myred \myempty
+ \begin{array}{@{}l@{\ \ \ }l}
+ \text{Can't prove} & \myfun{non-empty}\myappsp \mynil \myred \myempty \\
+ \text{Trivial to prove} & \myfun{non-empty}\myappsp(2 \mycons \mynil) \myred \myunit
\end{array}
\]
-
- Thus, proving that $2 \mathrel{\myfun{$>$}} 2$ corresponds to proving
- falsity, while $3 \mathrel{\myfun{$>$}} 1$ is fine.
\end{frame}
\begin{frame}
\frametitle{Example: safe $\myfun{head}$ function}
-
+ \only<3>{We can eliminate the `empty list' case:}
\[
\begin{array}{@{}l}
- \mysyn{data}\ \mylistt{\myb{A}} = \mynil \mydcsep \myb{A} \mycons \mylistt{\myb{A}} \\
- \ \\
- \myfun{length} : \mylistt{\myb{A}} \myarr \mynat \\
- \begin{array}{@{}l@{\myappsp}c@{\ }c@{\ }l}
- \myfun{length} & \mynil & = & \mydc{zero} \\
- \myfun{length} & (\myb{x} \mycons \myb{xs}) & = & \mydc{suc} \myappsp (\myfun{length} \myappsp \myb{xs})
- \end{array} \\
- \ \\
- \myfun{head} : \myfora{\myb{l}}{\mytyc{List}\myappsp\myb{A}}{ \myfun{length}\myappsp\myb{l} \mathrel{\myfun{$>$}} 0 \myarr \myb{A}} \\
+ \myfun{head} : \myfora{\myb{l}}{\mytyc{List}\myappsp\myb{A}}{ \myfun{non-empty}\myappsp\myb{l} \myarr \myb{A}} \\
\begin{array}{@{}l@{\myappsp}c@{\myappsp}c@{\ }c@{\ }l}
- \myfun{head} & \mynil & \myb{p} & = & \myhole{?} \\
- \myfun{head} & (\myb{x} \mycons \myb{xs}) & \myb{p} & = & \myb{x}
+ \myfun{head} & \mynil & \myb{p} & \mapsto & \only<1,2>{\myhole{?}}\only<3>{\myabsurd\myappsp\myb{p}} \\
+ \myfun{head} & (\myb{x} \mycons \myb{xs}) & \myb{p} & \mapsto & \myb{x}
\end{array}
\end{array}
\]
+ \only<1>{
+ The logic equivalent would be
+ \[
+ \forall \myb{l} {:} \mylist{\myb{A}}.\ \myfun{non-empty}\myappsp\myb{l} \myarr \myb{A}
+ \]
+ `For all non-empty lists of type $\myb{A}$, we can get an element of $\myb{A}$.'
+ }
+ \only<2>{
The type of $\myb{p}$ in the $\myhole{?}$ is $\myempty$, since
- \[\myfun{length} \myappsp \mynil \mathrel{\myfun{$>$}} 0 \myred 0 \mathrel{\myfun{$>$}} 0 \myred \myempty \]
-\end{frame}
-
-
-\begin{frame}
- \frametitle{Example: safe $\myfun{head}$ function}
-
- \[
- \begin{array}{@{}l}
- \mysyn{data}\ \mylistt{\myb{A}} = \mynil \mydcsep \myb{A} \mycons \mylistt{\myb{A}} \\
- \ \\
- \myfun{length} : \mytyc{List}\myappsp\myb{A} \myarr \mynat \\
- \begin{array}{@{}l@{\myappsp}c@{\ }c@{\ }l}
- \myfun{length} & \mynil & = & \mydc{zero} \\
- \myfun{length} & (\myb{x} \mycons \myb{xs}) & = & \mydc{suc} \myappsp (\myfun{length} \myappsp \myb{xs})
- \end{array} \\
- \ \\
- \myfun{head} : \myfora{\myb{l}}{\mytyc{List}\myappsp\myb{A}}{ \myfun{length}\myappsp\myb{l} \mathrel{\myfun{$>$}} 0 \myarr \myb{A}} \\
- \begin{array}{@{}l@{\myappsp}c@{\myappsp}c@{\ }c@{\ }l}
- \myfun{head} & \mynil & \myb{p} & = & \myabsurd \myappsp \myb{p} \\
- \myfun{head} & (\myb{x} \mycons \myb{xs}) & \myb{p} & = & \myb{x}
- \end{array}
- \end{array}
- \]
-
- Where $\myfun{absurd}$ corresponds to the logical \emph{ex falso
- quodlibet}---given $\myempty$, we can get anything:
- \[
- \myfun{absurd} : \myempty \myarr \myb{A}
- \]
+ \[\myfun{non-empty}\myappsp\mynil \myred \myempty \]}
+ \only<3>{
+ Remember:
+ \[ \myfun{absurd} : \myempty \myarr \myb{A} \]
+ }
\end{frame}
\begin{frame}
\frametitle{How do we type check this thing?}
+ \[\text{Is\ } \myfun{non-empty}\myappsp(3 \mycons \mynil) \text{\ the same as\ } \myunit\text{?}\]
+ Or in other words, is
+ \[ \mytt : \myunit \]
+ A valid argument to
\[
- \myfun{head} \myappsp \mylistt{3} : \myfun{length} \myappsp \mylistt{3} \mathrel{\myfun{$>$}} 0 \myarr \mynat
+ \myfun{head} \myappsp (3 \mycons \mynil) : \myfun{non-empty}\myappsp(3 \mycons \mynil) \myarr \mynat
\]
- Will $\mytt : \myunit$ do as an argument? In other words, when type
- checking, do we have that
- \[
- \begin{array}{@{}c@{\ }c@{\ }c}
- \myunit & \mydefeq & \myfun{length} \myappsp \mylistt{3} \mathrel{\myfun{$>$}} 0 \\
- \myfun{length} \myappsp \mynil \mathrel{\myfun{$>$}} 0 & \mydefeq & \myempty \\
- (\myabs{\myb{x}\, \myb{y}}{\myb{y}}) \myappsp \myunit \myappsp \myappsp \mynat & \mydefeq & (\myabs{\myb{x}\, \myb{y}}{\myb{x}}) \myappsp \mynat \myappsp \myunit \\
- & \vdots &
- \end{array}
- \]
- ?
-\end{frame}
-
-\begin{frame}
- \frametitle{Definitional equality}
-
- The type checker needs a notion of equality between types.
-
- We reduce terms `as far as possible' (to their \emph{normal form}) and
- then compare them syntactically:
+ Yes: to typecheck, we reduce terms fully (to their \emph{normal form})
+ before comparing:
\[
\begin{array}{@{}r@{\ }c@{\ }c@{\ }c@{\ }c@{\ }c@{\ }l}
- \myunit & \myredd & \myunit & \mydefeq & \myunit & \myreddd & \myfun{length} \myappsp \mylistt{3} \mathrel{\myfun{$>$}} 0 \\
- \myfun{length} \myappsp \mynil \mathrel{\myfun{$>$}} 0 & \myredd & \myempty & \mydefeq & \myempty & \myreddd & \myempty \\
+ \myunit & \myredd & \myunit & \mydefeq & \myunit & \myreddd & \myfun{non-empty}\myappsp(3 \mycons \mynil) \\
(\myabs{\myb{x}\, \myb{y}}{\myb{y}}) \myappsp \myunit \myappsp \myappsp \mynat & \myredd & \mynat & \mydefeq & \mynat & \myreddd & (\myabs{\myb{x}\, \myb{y}}{\myb{x}}) \myappsp \mynat \myappsp \myunit \\
& & & \vdots & & &
\end{array}
\]
-
- This equality, $\mydefeq$, takes the name of \emph{definitional} equality.
+ \[
+ \mydefeq\ \text{takes the name of \textbf{definitional equality}.}
+ \]
\end{frame}
\begin{frame}
\frametitle{Propositional equality} Using definitional equality, we
can give the user a type-level notion of term equality.
\[
- (\myeq) : \myb{A} \myarr \myb{A} \myarr \mytyp
+ (\myeq) : \myb{A} \myarr \myb{A} \myarr \mytyp\ \ \ \text{internalises equality \textbf{as a type}}
\]
- We introduce members of $\myeq$ by reflexivity:
+ We introduce members of $\myeq$ by reflexivity, for example
\[
- \myrefl\myappsp\mytmt : \mytmt \myeq \mytmt
+ \myrefl\myappsp5 : 5 \myeq 5
\]
- So that $\myrefl$ will relate definitionally equal terms:
+ But also
\[
- \myrefl\myappsp 5 : (3 + 2) \myeq (1 + 4)\ \text{since}\ (3 + 2) \myeq (1 + 4) \myredd 5 \myeq 5
+ \begin{array}{@{}l}
+ \myrefl\myappsp 5 : (3 + 2) \myeq (1 + 4)\text{, since}\\
+ (3 + 2) \myeq (1 + 4) \myredd 5 \myeq 5
+ \end{array}
\]
Then we can use a substitution law to derive other
laws---transitivity, congruence, etc.
+ \[ \myeq\ \text{takes the name of \textbf{propositional equality}} \]
\end{frame}
\begin{frame}
\frametitle{The problem with prop. equality}
Going back to $\myfun{map}$, we can prove that
-\[ \forall \myb{f} {:} (\myb{b} \myarr \myb{c}), \myb{g} {:} (\myb{a} \myarr \myb{b}), \myb{l} {:} \mylist{\myb{a}}. (\myfun{map}\myappsp \myb{f} \mycomp \myfun{map}\myappsp \myb{g}) \myappsp \myb{l} \myeq \myfun{map}\myappsp (\myb{f} \mycomp \myb{g}) \myappsp \myb{l} \]
-Because we can prove, by induction on $\myb{l}$, that we will always get definitionally equal lists.
+\[ \forall \myb{f} {:} (\myb{b} \myarr \myb{c}), \myb{g} {:} (\myb{a} \myarr \myb{b}), \myb{l} {:} \mylist{\myb{a}}.\ (\myfun{map}\myappsp \myb{f} \mycomp \myfun{map}\myappsp \myb{g}) \myappsp \myb{l} \myeq \myfun{map}\myappsp (\myb{f} \mycomp \myb{g}) \myappsp \myb{l} \]
+Because
+\[
+(\myfun{map}\myappsp \myb{f} \mycomp \myfun{map}\myappsp \myb{g})\myappsp \myb{l} \mydefeq \myfun{map}\myappsp (\myb{f} \mycomp \myb{g}) \myappsp \myb{l}
+\]
+By induction on $\myb{l}$.
-But without the $\myb{l}$, we cannot compute, so we are stuck with
+Without the $\myb{l}$ we cannot compute, so we are stuck with
\[
\myfun{map}\myappsp \myb{f} \mycomp \myfun{map}\myappsp \myb{g} \not\mydefeq \myfun{map}\myappsp (\myb{f} \mycomp \myb{g})
\]
\end{frame}
\begin{frame}
- \frametitle{The solution}
+ \frametitle{Observational equality}
- \emph{Observational} equality, instead of basing its equality on
- definitional equality, looks at the structure of the type to decide:
+ Instead of basing its equality on definitional equality, look at the
+ structure of the type to decide.
+
+ For functions this will mean that proving
\[
- \begin{array}{@{}l}
- (\myfun{map}\myappsp \myb{f} \mycomp \myfun{map}\myappsp \myb{g} : \mylistt{\myb{A_1}} \myarr \mylistt{\myb{C_1}}) \myeq (\myfun{map}\myappsp (\myb{f} \mycomp \myb{g}) : \mylistt{\myb{A_2}} \myarr \mylistt{\myb{C_2}}) \myred \\
- \myind{2} (\myb{l_1} : \myb{A_1}) \myarr (\myb{l_2} : \myb{A_2}) \myarr (\myb{l_1} : \myb{A_1}) \myeq (\myb{l_2} : \myb{A_2}) \myarr \\
- \myind{2} ((\myfun{map}\myappsp \myb{f} \mycomp \myfun{map}\myappsp \myb{g}) \myappsp \myb{l} : \mylistt{\myb{C_1}}) \myeq (\myfun{map}\myappsp (\myb{f} \mycomp \myb{g}) \myappsp \myb{l} : \mylistt{\myb{C_2}})
- \end{array}
+ \myfun{map}\myappsp \myse{f} \mycomp \myfun{map}\myappsp \myse{g} \myeq \myfun{map}\myappsp (\myse{f} \mycomp \myse{g})
+ \]
+ Will reduce to proving that
+ \[
+ (\myb{l} : \mylist{\myb{A}}) \myarr
+ (\myfun{map}\myappsp \myse{f} \mycomp \myfun{map}\myappsp \myse{g})\myappsp\myb{l} \myeq \myfun{map}\myappsp (\myse{f} \mycomp \myse{g})\myappsp \myb{l}
\]
- This extends to other structures (tuples, inductive types, \dots).
- Moreover, if we can deem two \emph{types} equal, we can \emph{coerce}
- values from one to the other.
+ Which is what we want. The interesting part is how to make the system
+ compute nicely.
\end{frame}
\begin{frame}
- \frametitle{\mykant}
-
- Observational equality was described in a very restricted theory.
-
- \mykant\ aims to incorporate it in a more `practical' environment,
- where we have:
- \begin{itemize}
- \item User defined data types (inductive data and records).
- \item A type hierarchy.
- \item Partial type inference (bidirectional type checking).
- \item Type holes.
- \end{itemize}
+ \begin{center}
+ {\huge \mykant' features}
+ \end{center}
\end{frame}
\begin{frame}
\frametitle{Inductive data}
- Good old Haskell data types:
\[
- \mysyn{data}\ \mytyc{List}\myappsp \myb{A} = \mynil \mydcsep \myb{A} \mycons \mytyc{List}\myappsp\myb{A}
+ \mysyn{data}\ \mytyc{List}\myappsp (\myb{A} : \mytyp) \mapsto \mynil \mydcsep \myb{A} \mycons \mytyc{List}\myappsp\myb{A}
\]
- But instead of general recursion and pattern matching, we have
- structural induction:
+ Each with an induction principle:
\[
\begin{array}{@{}l@{\ }l}
- \mytyc{List}.\myfun{elim} : & (\myb{P} : \mytyc{List}\myappsp\myb{A} \myarr \mytyp) \myarr \\
+ \mytyc{List}.\myfun{elim} : & \AgdaComment{-{}- The property that we want to prove:} \\
+ & (\myb{P} : \mytyc{List}\myappsp\myb{A} \myarr \mytyp) \myarr \\
+ & \AgdaComment{-{}- If it holds for the base case:} \\
& \myb{P} \myappsp \mynil \myarr \\
+ & \AgdaComment{-{}- And for the inductive step:} \\
& ((\myb{x} : \myb{A}) \myarr (\myb{l} : \mytyc{List}\myappsp \myb{A}) \myarr \myb{P} \myappsp \myb{l} \myarr \myb{P} \myappsp (\myb{x} \mycons \myb{l})) \myarr \\
+ & \AgdaComment{-{}- Then it holds for every list:} \\
& (\myb{l} : \mytyc{List}\myappsp\myb{A}) \myarr \myb{P} \myappsp \myb{l}
\end{array}
\]
- Reduction:
+ Induction is also computation, via structural recursion:
\[
\begin{array}{@{}l@{\ }l}
\mytyc{List}.\myfun{elim} \myappsp \myse{P} \myappsp \myse{pn} \myappsp \myse{pc} \myappsp \mynil & \myred \myse{pn} \\
- \mytyc{List}.\myfun{elim} \myappsp \myse{P} \myappsp \myse{pn} \myappsp \myse{pc} \myappsp (\mytmm \mycons \mytmn) & \myred \myse{pc} \myappsp \mytmm \myappsp \mytmn \myappsp (\mytyc{List}.\myfun{elim} \myappsp \myse{P} \myappsp \myse{pn} \myappsp \myse{ps} \myappsp \mytmt )
+ \mytyc{List}.\myfun{elim} \myappsp \myse{P} \myappsp \myse{pn} \myappsp \myse{pc} \myappsp (\mytmm \mycons \mytmn) & \myred \myse{pc} \myappsp \mytmm \myappsp \mytmn \myappsp (\mytyc{List}.\myfun{elim} \myappsp \myse{P} \myappsp \myse{pn} \myappsp \myse{ps} \myappsp \mytmn )
\end{array}
\]
\end{frame}
\begin{frame}
- \frametitle{Records}
- But also records:
+ \frametitle{Dependent defined types} \emph{Unlike} Haskell, we can
+ have fields of a data constructor to depend on earlier fields:
\[
- \mysyn{record}\ \mytyc{Tuple}\myappsp\myb{A}\myappsp\myb{B} = \mydc{tuple}\ \{ \myfun{fst} : \myb{A}, \myfun{snd} : \myb{B} \}
+ \begin{array}{@{}l}
+ \mysyn{record}\ \mytyc{Tuple}\myappsp(\myb{A} : \mytyp)\myappsp\myhole{$(\myb{B} : \myb{A} \myarr \mytyp)$} \mapsto \\
+ \myind{2}\mydc{tuple}\ \{ \myfun{fst} : \myb{A}, \myfun{snd} : \myb{B}\myappsp\myb{fst} \}
+ \end{array}
\]
- Where each field defines a projection from instances of the record:
+
+ The \emph{type} of the second element depends on the \emph{value} of
+ the first:
\[
- \begin{array}{@{}l@{\ }c@{\ }l}
- \myfun{fst} & : & \mytyc{Tuple}\myappsp\myb{A}\myappsp\myb{B} \myarr \myb{A} \\
- \myfun{snd} & : & \mytyc{Tuple}\myappsp\myb{A}\myappsp\myb{B} \myarr \myb{B}
+ \begin{array}{@{}l@{\ }l}
+ \myfun{fst} & : \mytyc{Tuple}\myappsp\myb{A}\myappsp\myb{B} \myarr \myb{A} \\
+ \myfun{snd} & : (\myb{x} : \mytyc{Tuple}\myappsp\myb{A}\myappsp\myb{B}) \myarr \myb{B} \myappsp (\myfun{fst} \myappsp \myb{x})
\end{array}
\]
Where the projection's reduction rules are predictably
\end{frame}
\begin{frame}
- \frametitle{Dependend defined types} \emph{Unlike} Haskell, we can
- have fields of a data constructor to depend on earlier fields:
+ \frametitle{Example: the type of even numbers}
+ For example we can define the type of even numbers:
+ % TODO fix
\[
\begin{array}{@{}l}
- \mysyn{record}\ \mytyc{Tuple}\myappsp(\myb{A} : \mytyp)\myappsp(\myb{B} : \myb{A} \myarr \mytyp) = \\
- \myind{2}\mydc{tuple}\ \{ \myfun{fst} : \myb{A}, \myfun{snd} : \myb{B}\myappsp\myb{fst} \}
- \end{array}
- \]
- $\mytyc{Tuple}$ takes a $\mytyp$, $\myb{A}$, and a predicate from
- elements of $\myb{A}$ to types, $\myb{B}$.
-
- This way, the \emph{type} of the second element depends on the
- \emph{value} of the first:
- \[
- \begin{array}{@{}l@{\ }l}
- \myfun{fst} & : \mytyc{Tuple}\myappsp\myb{A}\myappsp\myb{B} \myarr \myb{A} \\
- \myfun{snd} & : (\myb{x} : \mytyc{Tuple}\myappsp\myb{A}\myappsp\myb{B}) \myarr \myb{B} \myappsp (\myfun{fst} \myappsp \myb{x})
+ \mysyn{data}\ \mynat \mapsto \mydc{zero} \mydcsep \mydc{suc}\myappsp\mynat \\
+ \ \\
+ \myfun{even} : \mynat \myarr \mytyp \\
+ \begin{array}{@{}l@{\myappsp}c@{\ }l}
+ \myfun{even} & \myzero & \mapsto \myunit \\
+ \myfun{even} & (\mysuc \myappsp \myzero) & \mapsto \myempty \\
+ \myfun{even} & (\mysuc \myappsp (\mysuc \myappsp \myb{n})) & \mapsto \myfun{even} \myappsp \myb{n}
+ \end{array} \\
+ \ \\
+ \mytyc{Even} : \mytyp \\
+ \mytyc{Even} \mapsto \mytyc{Tuple}\ \mynat\ \myfun{even}
\end{array}
\]
\end{frame}
\begin{frame}
\frametitle{Type hierarchy}
- Up to now, we have thrown $\mytyp$ around, as `the type of types'.
-
- But what is the type of $\mytyp$ itself? The simple way out is
+ \[\{\mynat, \mybool, \mytyc{List}\myappsp\mynat, \cdots\} : \mytyp\]
+ What is the type of $\mytyp$?
\[
- \mytyp : \mytyp
+ \cancel{\mytyp : \mytyp}\ \ \ \text{\textbf{inconsistent}}
\]
- This solution is not only simple, but inconsistent, for the same
- reason that the notion of a `powerset' in na{\"i}ve set theory is.
+ Similar to Russel's paradox in na{\"i}ve set theory.
- Instead, following Russell, we shall have
+ Instead, we have a hierarchy:
\[
\{\mynat, \mybool, \mytyc{List}\myappsp\mynat, \cdots\} : \mytyp_0 : \mytyp_1 : \cdots
\]
\begin{frame}
\frametitle{Cumulativity and typical ambiguity}
- Is it OK to take
- \[ \mytyp_0 : \mytyp_2 \]
- ?
+ Instead of:
+ \[ \mytyp_0 : \mytyp_1 \ \ \ \text{but}\ \ \ \mytyp_0 \centernot{:} \mytyp_2\]
+ We have a cumulative hierarchy, so that
+ \[ \mytyp_n : \mytyp_m \ \ \ \text{iff}\ \ \ n < m \]
+ For example
+ \[ \mynat : \mytyp_0\ \ \ \text{and}\ \ \ \mynat : \mytyp_1\ \ \ \text{and}\ \ \ \mynat : \mytyp_{50} \]
+
+ But in \mykant, you can forget about levels: the consistency is
+ checked automatically---a mechanised version of what Russell called
+ \emph{typical ambiguity}.
+
+ \begin{center}
+ \begin{tikzpicture}[remember picture, node distance=1.5cm]
+ \begin{pgfonlayer}{foreground}
+ % Place nodes
+ \node (x) {$x$};
+ \node [right of=x] (y) {$y$};
+ \node [right of=y] (z) {$z$};
+ \node [below of=z] (k) {$k$};
+ \node [left of=k] (j) {$j$};
+ %% Lines
+ \path[->]
+ (x) edge node [above] {$<$} (y)
+ (y) edge node [above] {$\le$} (z)
+ (z) edge node [right] {$<$} (k)
+ (k) edge node [below] {$\le$} (j)
+ (j) edge node [left ] {$\le$} (y);
+ \end{pgfonlayer}{foreground}
+ \end{tikzpicture}
+ \begin{tikzpicture}[remember picture, overlay]
+ \begin{pgfonlayer}{background}
+ \fill [red, opacity=0.3, rounded corners]
+ (-2.7,2.6) rectangle (-0.2,0.05)
+ (-4.1,2.4) rectangle (-3.3,1.6);
+ \end{pgfonlayer}{background}
+ \end{tikzpicture}
+ \end{center}
+\end{frame}
+
+\begin{frame}
+ \frametitle{Bidirectional type checking}
+ \[
+ \mysyn{data}\ \mytyc{List}\myappsp (\myb{A} : \mytyp) \mapsto \mydc{nil} \mydcsep \mydc{cons} \myappsp \myb{A}\myappsp (\mytyc{List}\myappsp\myb{A})
+ \]
+
+ With no type inference, we have explicit types for the constructors:
+ \[
+ \begin{array}{@{}l@{\ }l}
+ \mydc{nil} & : (\myb{A} : \mytyp) \myarr \mytyc{List}\myappsp\myb{A} \\
+ \mydc{cons} &: (\myb{A} : \mytyp) \myarr \myb{A} \myarr \mytyc{List}\myappsp\myb{A} \myarr \mytyc{List}\myappsp\myb{A}\\
+ \end{array}
+ \]
+ ...ugh:
+ \[
+ \mydc{cons}\myappsp \mynat\myappsp 1 \myappsp (\mydc{cons}\myappsp \mynat \myappsp 2 \myappsp (\mydc{cons}\myappsp \mynat \myappsp 3 \myappsp (\mydc{nil}\myappsp \mynat)))
+ \]
+ Instead, annotate terms and propagate the type:
+ \[
+ \mydc{cons}\myappsp 1 \myappsp (\mydc{cons}\myappsp 2 \myappsp (\mydc{cons} \myappsp 3 \myappsp \mydc{nil})) : \mytyc{List}\myappsp\mynat
+ \]
+ Conversely, when we use eliminators the type can be inferred.
+\end{frame}
+
+\begin{frame}
+ \frametitle{OTT + user defined types}
+
+ For each type, we need to:
+ \begin{itemize}
+ \item Describe when two types formed by the defined type constructors
+ are equal;
+ \[ \mylist{\mytya_1} \myeq \mylist{\mytya_2} \]
+ \item Describe when two values of the defined type are equal;
+ \[
+ \begin{array}{@{}c@{\ \ \ \ \ \ }c}
+ \mynil \myeq \mynil & \mynil \myeq \mytmm \mycons \mytmn \\
+ \mytmm \mycons \mytmn \myeq \mynil & \mytmm_1 \mycons \mytmn_1 \myeq \mytmm_2 \mycons \mytmn_2
+ \end{array}
+ \]
+ \item Describe how to transport values of the defined type.
+ \end{itemize}
+\end{frame}
+
+\begin{frame}
+ \frametitle{OTT + hierarchy}
+
+ Since equalities reduce to functions abstracting over various things,
+ we need to make sure that the hierarchy is respected.
+
+ For example we have that
+ \[
+ \begin{array}{@{}l}
+ \myjm{(\myb{x_1} {:} \mytya_1) \myarr \mytyb_1}{\mytyp}{(\myb{x_2} {:} \mytya_2) \myarr \mytyb_2}{\mytyp} \myred \\
+ \myind{2} \myjm{\mytya_1}{\mytyp}{\mytya_2}{\mytyp} \myand \\
+ \myind{2} ((\myb{x_1} : \mytya_1) \myarr (\myb{x_2} : \mytya_2) \myarr \myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2} \myarr \mytyb_1[\myb{x_1}] \myeq \mytyb_2[\myb{x_2}])
+ \end{array}
+ \]
+
+ Subtle point---I discovered a problem in the theory after
+ submitting... but I have a fix.
+\end{frame}
+
+\begin{frame}
+ \frametitle{Bonus! WebSocket prompt}
+ \url{http://bertus.mazzo.li}, go DDOS it!
+
+ \includegraphics[width=\textwidth]{web-prompt.png}
+\end{frame}
+
+\begin{frame}
+\begin{center}
+{\Huge Demo}
+\end{center}
+\end{frame}
+
+\begin{frame}
+ \frametitle{What have we done?}
+
+ \begin{itemize}
+ \item A small theorem prover for intuitionistic logic, featuring:
+ \item Inductive data and record types;
+ \item A cumulative, implicit type hierarchy;
+ \item Partial type inference---bidirectional type checking;
+ \item Type holes;
+ \item Observational equality---coming soon to the implementation.
+ \end{itemize}
+\end{frame}
+
+\begin{frame}
+ \frametitle{Further work}
+
+ \begin{itemize}
+ \item Pattern matching and explicit recursion
+ \item More expressive data types
+ \item Inference via unification
+ \item Codata
+ \end{itemize}
\end{frame}
\begin{frame}