\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}
\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.
\[
\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}
\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:
\]
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}
% 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 \\
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}
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}
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}
\]
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}