X-Git-Url: https://git.enpas.org/?a=blobdiff_plain;f=presentation.tex;h=2184ae49c31d3e0d65748257619744bf7538f3c5;hb=HEAD;hp=a1b2419ca7bc50da5bb4739d1f0d54e704a1d8a5;hpb=ec1119dffc5801526058a816d498b58e3c8f9e7f;p=bitonic-mengthesis.git

diff --git a/presentation.tex b/presentation.tex
index a1b2419..2184ae4 100644
--- a/presentation.tex
+++ b/presentation.tex
@@ -12,6 +12,13 @@
 
 \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}
@@ -228,11 +235,14 @@
 \begin{frame}
   \frametitle{\mykant?}
 
-  \mykant\ is an \emph{interactive theorem prover}, implemented in
-  Haskell.
+  \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}.
 
-  It is similar in scope to Agda or 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}
@@ -287,15 +297,13 @@
 \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}
     \mysyn{data}\ \myempty & \text{No members.} \\
     \mysyn{data}\ \myunit \mapsto \mytt & \text{One member.}
   \end{array}
   \]
-  $\myempty : \mytyp$, $\myunit : \mytyp$.
 
   $\myunit$ is trivially inhabitable: it corresponds to $\top$ in
   logic.
@@ -306,6 +314,9 @@
   \[
   \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}
@@ -363,15 +374,15 @@
 
 \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)
+  Yes: to typecheck, we reduce terms fully (to their \emph{normal form})
   before comparing:
   \[
   \begin{array}{@{}r@{\ }c@{\ }c@{\ }c@{\ }c@{\ }c@{\ }l}
@@ -440,10 +451,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}
@@ -474,7 +481,7 @@ Without the $\myb{l}$ we cannot compute, so we are stuck with
   \[
   \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}
@@ -512,6 +519,8 @@ Without the $\myb{l}$ we cannot compute, so we are stuck with
   % TODO fix
   \[
   \begin{array}{@{}l}
+    \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 \\
@@ -532,7 +541,7 @@ Without the $\myb{l}$ we cannot compute, so we are stuck with
   \[
   \cancel{\mytyp : \mytyp}\ \ \ \text{\textbf{inconsistent}}
   \]
-  Much like na{\"i}ve set theory is (Girard's paradox).
+  Similar to Russel's paradox in na{\"i}ve set theory.
 
   Instead, we have a hierarchy:
   \[
@@ -553,6 +562,33 @@ Without the $\myb{l}$ we cannot compute, so we are stuck with
   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}
@@ -579,16 +615,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}
 
@@ -617,9 +643,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}
   \]
 
@@ -627,12 +653,32 @@ 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 Type holes;
+    \item Observational equality---coming soon to the implementation.
+  \end{itemize}
+\end{frame}
+
 \begin{frame}
   \frametitle{Further work}