From df78daffd508f40f39777d37db16562007b2ed12 Mon Sep 17 00:00:00 2001
From: Francesco Mazzoli <f@mazzo.li>
Date: Thu, 27 Jun 2013 00:02:00 +0100
Subject: [PATCH] ...

---
 final.lagda      |  4 ++--
 presentation.tex | 47 ++++++++++++++++++++++++++---------------------
 2 files changed, 28 insertions(+), 23 deletions(-)

diff --git a/final.lagda b/final.lagda
index 8928ec7..4b7484a 100644
--- a/final.lagda
+++ b/final.lagda
@@ -4357,11 +4357,11 @@ Tokenisation is performed by a simple hand written lexer.
     \multicolumn{3}{@{}l}{\text{Abstracted variables.}} \\
     \mysee{abstract} & ::= & \mytermi{postulate}\ \mysee{typed} \\
     \multicolumn{3}{@{}l}{\text{Data types, and their constructors.}} \\
-    \mysee{data} & ::= & \mytermi{data}\ \mysee{name}\ \mysee{telescope}\ \mytermi{->}\ \mytermi{*}\ \mytermi{=>}\ \mytermi{\{}\ \mysee{constrs}\ \mytermi{\}} \\
+    \mysee{data} & ::= & \mytermi{data}\ \mysee{name}\ \mytermi{:}\ \mysee{telescope}\ \mytermi{->}\ \mytermi{*}\ \mytermi{=>}\ \mytermi{\{}\ \mysee{constrs}\ \mytermi{\}} \\
     \mysee{constrs} & ::= & \mysee{typed} \\
                    &  |  & \mysee{typed}\ \mytermi{|}\ \mysee{constrs} \\
     \multicolumn{3}{@{}l}{\text{Records, and their projections.  The $\mysee{name}$ before the projections is the constructor name.}} \\
-    \mysee{record} & ::= & \mytermi{record}\ \mysee{name}\ \mysee{telescope}\ \mytermi{->}\ \mytermi{*}\ \mytermi{=>}\ \mysee{name}\ \mytermi{\{}\ \mysee{projs}\ \mytermi{\}} \\
+    \mysee{record} & ::= & \mytermi{record}\ \mysee{name}\ \mytermi{:}\ \mysee{telescope}\ \mytermi{->}\ \mytermi{*}\ \mytermi{=>}\ \mysee{name}\ \mytermi{\{}\ \mysee{projs}\ \mytermi{\}} \\
     \mysee{projs} & ::= & \mysee{typed} \\
                    &  |  & \mysee{typed}\ \mytermi{,}\ \mysee{projs}
   \end{array}
diff --git a/presentation.tex b/presentation.tex
index 3728511..1089ae6 100644
--- a/presentation.tex
+++ b/presentation.tex
@@ -366,13 +366,13 @@
 
 \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 (3 \mycons \mynil) : \myfun{non-empty}\myappsp(3 \mycons \mynil) \myarr \mynat
   \]
-  Is it the case that
-  \[ \mytt : \myfun{non-empty}\myappsp(3 \mycons \mynil) \]
-  Or
-  \[ \myfun{head} \myappsp (3 \mycons \mynil) : \myunit \myarr \mynat \]
 
   Yes: to typecheck, we reduce terms fully (to their \emph{normal form})
   before comparing:
@@ -443,10 +443,6 @@ Without the $\myb{l}$ we cannot compute, so we are stuck with
   \]
   Which is what we want.  The interesting part is how to make the system
   compute nicely.
-  
-  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.
 \end{frame}
 
 \begin{frame}
@@ -584,16 +580,6 @@ Without the $\myb{l}$ we cannot compute, so we are stuck with
   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}
   \frametitle{OTT + user defined types}
 
@@ -622,9 +608,9 @@ Without the $\myb{l}$ we cannot compute, so we are stuck with
   For example we have that
   \[
   \begin{array}{@{}l}
-    (\myb{x_1} {:} \mytya_1) \myarr \mytyb_1 \myeq (\myb{x_2} {:} \mytya_2) \myarr \mytyb_2 \myred \\
-    \myind{2} \mytya_1 \myeq \mytya_2 \myand 
-    ((\myb{x_1} : \mytya_1) \myarr (\myb{x_2} : \mytya_2) \myarr \mytyb_1[\myb{x_1}] \myeq \mytyb_2[\myb{x_2}])
+    \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}
   \]
 
@@ -632,12 +618,31 @@ Without the $\myb{l}$ we cannot compute, so we are stuck with
   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 Observational equality---coming soon to the implementation.
+  \end{itemize}
+\end{frame}
+
 \begin{frame}
   \frametitle{Further work}
 
-- 
2.30.2