..>

1 files changed, 176 insertions, 90 deletions

diff --git a/presentation.tex b/presentation.tex
index f3381bc..3492be8 100644
--- a/presentation.tex
+++ b/presentation.tex
@@ -10,6 +10,9 @@
 \AtBeginSubsubsection{\frame{\subsubsectionpage}}
 \beamertemplatenavigationsymbolsempty
 
+\usepackage{centernot}
+\usepackage{cancel}
+
 \setlength{\parindent}{0pt}
 \setlength{\parskip}{6pt plus 2pt minus 1pt}
 \setlength{\emergencystretch}{3em}  % prevent overfull lines
@@ -39,7 +42,7 @@
 \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}
@@ -204,10 +207,12 @@
 \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*}}
@@ -221,6 +226,19 @@
 \frame{\titlepage}
 
 \begin{frame}
+  \frametitle{\mykant?}
+
+  \mykant\ is an \emph{interactive theorem prover}, implemented in
+  Haskell.
+
+  It is similar in scope to Agda or Coq, but with a more powerful notion
+  of \emph{equality}.
+
+  We figured out its theory, but do not have a complete
+  implementation---although most of the work is done.
+\end{frame}
+
+\begin{frame}
   \frametitle{Theorem provers are short-sighted}
 
   Two functions dear to the Haskell practitioner:
@@ -253,14 +271,12 @@
 \end{frame}
 
 \begin{frame}
-  \frametitle{Observational equality and \mykant}
-
-  \emph{Observational equality} is a solution to this and other equality
-  annoyances.
+  \frametitle{\mykant\ and observational equality}
 
-  \mykant\ is a system making observational equality more usable.
+  \emph{Observational} equality solves this and other annoyances.
 
-  The theory of \mykant\ is complete, the practice, not quite.
+  \mykant\ is a system aiming at making observational equality more
+  usable.
 \end{frame}
 
 \begin{frame}
@@ -279,11 +295,14 @@
   logic.
 
   $\myempty$ is \emph{not} inhabitable: it corresponds to $\bot$.
-
+  \[
+  \myfun{absurd} : \myempty \myarr \myb{A}
+  \]
 \end{frame}
 
 \begin{frame}
   \frametitle{Theorem provers, dependent types}
+  % TODO examples first
 
   We can express relations:
   \[
@@ -298,7 +317,7 @@
   \]
 
   A term of type $\myb{m} \mathrel{\myfun{$>$}} \myb{n}$ represents a
-  \emph{proof} that $\myb{n}$ is indeed greater than $\myb{n}$.
+  \emph{proof} that $\myb{m}$ is indeed greater than $\myb{n}$.
   \[
   \begin{array}{@{}l}
     3 \mathrel{\myfun{$>$}} 1 \myred \myunit \\
@@ -306,9 +325,6 @@
     0 \mathrel{\myfun{$>$}} \myb{m} \myred \myempty
   \end{array}
   \]
-
-  Thus, proving that $2 \mathrel{\myfun{$>$}} 2$ corresponds to proving
-  falsity, while $3 \mathrel{\myfun{$>$}} 1$ is fine.
 \end{frame}
 
 \begin{frame}
@@ -316,53 +332,32 @@
 
   \[
   \begin{array}{@{}l}
-    \mysyn{data}\ \mylistt{\myb{A}} = \mynil \mydcsep \myb{A} \mycons \mylistt{\myb{A}} \\
+    \mysyn{data}\ \mylist{\myb{A}} = \mynil \mydcsep \myb{A} \mycons \mylist{\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})
+      \myfun{length} & \mynil & \mapsto & \mydc{zero} \\
+      \myfun{length} & (\myb{x} \mycons \myb{xs}) & \mapsto & \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} & = & \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{length}\myappsp\myb{l} \mathrel{\myfun{$>$}} 0 \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{length} \myappsp \mynil \mathrel{\myfun{$>$}} 0 \myred 0 \mathrel{\myfun{$>$}} 0 \myred \myempty \]}
 \end{frame}
 
 \begin{frame}
@@ -370,6 +365,10 @@
   \[
   \myfun{head} \myappsp \mylistt{3} : \myfun{length} \myappsp \mylistt{3} \mathrel{\myfun{$>$}} 0 \myarr \mynat
   \]
+  Is it the case that
+  \[ \mytt : \myfun{length} \myappsp \mylistt{3} \mathrel{\myfun{$>$}} 0 \]
+  Or
+  \[ \myfun{head} \myappsp \mylistt{3} : \myunit \myarr \mynat \]
 
   Will $\mytt : \myunit$ do as an argument?  In other words, when type
   checking, do we have that
@@ -401,6 +400,7 @@
   \]
 
   This equality, $\mydefeq$, takes the name of \emph{definitional} equality.
+  % TODO add break
 \end{frame}
 
 \begin{frame}
@@ -424,7 +424,7 @@
 \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}    \]
+\[    \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.
 
 But without the $\myb{l}$, we cannot compute, so we are stuck with
@@ -434,15 +434,15 @@ But without the $\myb{l}$, we cannot compute, so we are stuck with
 \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:
   \[
   \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}})
+    (\myfun{map}\myappsp \myse{f} \mycomp \myfun{map}\myappsp \myse{g} : \mylistt{\myse{A_1}} \myarr \mylistt{\myse{C_1}}) \myeq (\myfun{map}\myappsp (\myse{f} \mycomp \myse{g}) : \mylistt{\myse{A_2}} \myarr \mylistt{\myse{C_2}}) \myred \\
+    \myind{2} (\myse{l_1} : \mylistt{\myse{A_1}}) \myarr (\myse{l_2} : \mylistt{\myse{A_2}}) \myarr (\myse{l_1} : \mylistt{\myse{A_1}}) \myeq (\myse{l_2} : \mylistt{\myse{A_2}}) \myarr \\
+    \myind{2} ((\myfun{map}\myappsp \myse{f} \mycomp \myfun{map}\myappsp \myse{g}) \myappsp \myse{l} : \mylistt{\myse{C_1}}) \myeq (\myfun{map}\myappsp (\myse{f} \mycomp \myse{g}) \myappsp \myse{l} : \mylistt{\myse{C_2}})
   \end{array}
   \]
   This extends to other structures (tuples, inductive types, \dots).
@@ -451,37 +451,30 @@ But without the $\myb{l}$, we cannot compute, so we are stuck with
 \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} \\
@@ -494,7 +487,7 @@ But without the $\myb{l}$, we cannot compute, so we are stuck with
   \frametitle{Records}
   But also records:
   \[
-  \mysyn{record}\ \mytyc{Tuple}\myappsp\myb{A}\myappsp\myb{B} = \mydc{tuple}\ \{ \myfun{fst} : \myb{A}, \myfun{snd} : \myb{B} \}
+  \mysyn{record}\ \mytyc{Tuple}\myappsp(\myb{A} : \mytyp)\myappsp(\myb{B} : \mytyp) \mapsto \mydc{tuple}\ \{ \myfun{fst} : \myb{A}, \myfun{snd} : \myb{B} \}
   \]
   Where each field defines a projection from instances of the record:
   \[
@@ -513,19 +506,17 @@ But without the $\myb{l}$, we cannot compute, so we are stuck with
 \end{frame}
 
 \begin{frame}
-  \frametitle{Dependend defined types} \emph{Unlike} Haskell, we can
+  \frametitle{Dependent defined types} \emph{Unlike} Haskell, we can
   have fields of a data constructor to depend on earlier fields:
   \[
   \begin{array}{@{}l}
-    \mysyn{record}\ \mytyc{Tuple}\myappsp(\myb{A} : \mytyp)\myappsp(\myb{B} : \myb{A} \myarr \mytyp) = \\
+    \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}
   \]
-  $\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:
+  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} \\
@@ -535,17 +526,34 @@ But without the $\myb{l}$, we cannot compute, so we are stuck with
 \end{frame}
 
 \begin{frame}
-  \frametitle{Type hierarchy}
-  Up to now, we have thrown $\mytyp$ around, as `the type of types'.
+  \frametitle{Example: the type of even numbers}
+  For example we can define the type of even numbers:
+  % TODO fix
+  \[
+  \begin{array}{@{}l}
+    \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}
 
-  But what is the type of $\mytyp$ itself?  The simple way out is
+\begin{frame}
+  \frametitle{Type hierarchy}
+  \[\{\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.
+  Much like na{\"i}ve set theory is (Girard's paradox).
 
-  Instead, following Russell, we shall have
+  Instead, we have a hierarchy:
   \[
   \{\mynat, \mybool, \mytyc{List}\myappsp\mynat, \cdots\} : \mytyp_0 : \mytyp_1 : \cdots
   \]
@@ -554,9 +562,87 @@ But without the $\myb{l}$, we cannot compute, so we are stuck with
 
 \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}.
+\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;
+  \item Describe when two values of the defined type are equal;
+  \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}
+    ((\myb{x_1} {:} \mytya_1) \myarr \mytyb_1 : \mytyp) \myeq ((\myb{x_2} {:} \mytya_2) \myarr \mytyb_2 : \mytyp) \myred \\
+    \myind{2} (\mytya_1 : \mytyp) \myeq (\mytya_2 : \mytyp) \myand \\
+    \myind{2} (\myb{x_1} : \mytya_1) \myarr (\myb{x_2} : \mytya_2) \myarr (\mytyb_1 : \mytyp) \myeq (\mytyb_2 : \mytyp)
+  \end{array}
+  \]
+
+  Subtle point---I discovered a problem in the theory after
+  submitting... but I have a fix.
+\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{Bidirectional type checking}
+
+  This technique is known as \emph{bidirectional} type checking---some
+  terms get \emph{checked}, some terms \emph{infer} types.
+
+  Usually used for pre-defined types or core calculi, \mykant\ extends
+  to user-defined types.
+\end{frame}
+
+\begin{frame}
+\begin{center}
+{\Huge Demo}
+\end{center}
 \end{frame}
 
 \begin{frame}