From: Francesco Mazzoli <f@mazzo.li>
Date: Thu, 27 Jun 2013 09:15:06 +0000 (+0100)
Subject: ...
X-Git-Url: https://git.enpas.org/?p=bitonic-mengthesis.git;a=commitdiff_plain;h=HEAD

...
---

diff --git a/presentation.tex b/presentation.tex
index 1089ae6..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}
@@ -290,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.
@@ -309,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}
@@ -554,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}
@@ -639,6 +674,7 @@ Without the $\myb{l}$ we cannot compute, so we are stuck with
     \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}