presentation: more progress

final/main.tex

@@ -132,4 +132,32 @@
 %         \Phi((x :: \tau) . \tau') &= ((x :: \tau), \tau') \\
 % \end{align*}
 
+
+% TODO: type this up in non-beamer form
+% \begin{frame}{A new type grammar}
+%   Wadler \& Blott write type schemes as follows:
+
+%   \begin{align*}
+%     \tau &::= (\tau \arrow \tau') \mid \alpha \mid \chi (\tau_1 \ldots \tau_n) \\
+%     \rho &::= (x :: \tau).\rho \mid \tau \\
+%     \sigma &::= \forall \alpha . \sigma \mid \rho
+%   \end{align*}
+
+%   Then, types are written simply $x :: \sigma$.
+% \end{frame}
+
+
+% \begin{frame}{A new type grammar}
+%   We propose the following modification:
+
+%   \begin{align*}
+%     \tau &::= (\tau \arrow \tau') \mid \alpha \mid \chi (\tau_1 \ldots \tau_n) \\
+%     \rho &::= (x :: \tau).\rho \mid \; \varnothing \\
+%     \sigma &::= \forall \alpha . \sigma \mid \; \varnothing
+%   \end{align*}
+
+%   Then, types are written $x :: \sigma \rho \, \tau$.
+% \end{frame}
+
+
 \end{document}