More presentation progress

presentation/main.tex

-\documentclass{beamer}
+\documentclass[10pt]{beamer}
 
 \usetheme{default}
 
 
-\usepackage{amssymb, amsmath, amsthm, amsrefs}
+\usepackage{amssymb, amsmath, amsthm, amsrefs, mathtools}
 
 \usepackage[english = american]{csquotes}
 \MakeOuterQuote{"}
@@ -32,6 +32,9 @@
 % backslash alias
 \newcommand{\bs}{\, \backslash \,}
 
+% teletype alias
+\renewcommand{\tt}{\texttt}
+
 
 \title{Typeclasses with Associated Types for ML Languages}
 \subtitle{Bachelors' Thesis}
@@ -88,8 +91,8 @@ impl Iterator for Fibonacci {
 \begin{frame}{Motivations}
   \begin{itemize}
     \item<1-> But there are drawbacks to each of these schemes.
-    \item<2-> Python: not type-sound
-    \item<2-> Rust: trait-based % can only impl traits for types you "own"
+    \item<2-> Python: impure, not type-sound
+    \item<2-> Rust: impure, trait-based % can only impl traits for types you "own"
   \end{itemize}
 \end{frame}
 
@@ -99,7 +102,79 @@ impl Iterator for Fibonacci {
 \end{frame}
 
 
-\begin{frame}{Beginnings: polymorphic type inference}
+\begin{frame}[fragile]{Beginnings: polymorphic type inference}
+  \begin{onlyenv}<1->
+    \begin{lstlisting}
+let
+  id = fn x => x
+in
+  (id 4, id true)
+    \end{lstlisting}
+  \end{onlyenv}
+
+  \begin{onlyenv}<2->
+    \begin{itemize}
+      \item Need to be able to assign type $\forall \alpha . \alpha \arrow \alpha$ to \tt{id}
+      \item Need to be able to instantiate \tt{id} twice
+    \end{itemize}
+  \end{onlyenv}
+\end{frame}
+
+
+\begin{frame}[fragile]{Adding in typeclasses}
+  \begin{itemize}
+    \item<1-> Work at the level of \tt{over} and \tt{inst} declarations
+    \item<2-> {
+      Example:
+      \begin{align*}
+        \tt{over eq?} &:: \forall \alpha . \alpha \arrow \alpha \arrow \tt{bool in}\\
+        \tt{inst eq?} &:: \tt{int} \arrow \tt{int} \arrow \tt{bool} \tt{ = } \lambda \tt{x} .
+          \lambda \tt{y} \ldots \tt{in}\\
+        \tt{inst eq?} &:: \tt{char} \arrow \tt{char} \arrow \tt{bool} \tt{ = } \lambda \tt{x} .
+          \lambda \tt{y} \ldots \tt{in}\\
+        &\tt{((eq? 5 10), (eq? \#"a" \#"a"))}\\
+      \end{align*}
+    }
+  \end{itemize}
+\end{frame}
+
+
+\begin{frame}{Typeclasses: translation to Hindley-Milner}
+  % Inference and translation rules from Wadler and Blott
+\end{frame}
+
+
+\begin{frame}[fragile]{Correcting a translation error}
+  Consider the following program:
+  \begin{lstlisting}[mathescape=true]
+over eq? :: $\forall \alpha .$ $\alpha$ $\arrow$ $\alpha$ $\arrow$ bool in
+inst eq? :: int $\arrow$ int $\arrow$ bool = $\lambda$x.$\lambda$y. $\ldots$ in
+inst eq? :: char $\arrow$ char $\arrow$ bool = $\lambda$x.$\lambda$y. $\ldots$ in
+inst eq? :: $\forall \alpha . \forall \beta .$
+                 (eq? :: $\alpha$ $\arrow$ $\alpha$ $\arrow$ bool).
+                 (eq? :: $\beta$ $\arrow$ $\beta$ $\arrow$ bool).
+                 ($\alpha$ * $\beta$ $\arrow$ $\alpha$ * $\beta$ $\arrow$ bool)
+                 = $\lambda$x.$\lambda$y. $\ldots$ in
+eq? (1, #"a") (2, #"b")
+  \end{lstlisting}
+\end{frame}
+
+
+\begin{frame}[fragile]{Correcting a translation error}
+  Per Wadler and Blott, the translation should be:
+  \begin{lstlisting}[mathescape=true]
+let eq?$_\tt{int}$ = $\lambda$x.$\lambda$y. $\ldots$ in
+let eq?$_\tt{char}$ = $\lambda$x.$\lambda$y. $\ldots$ in
+let eq?$_{\alpha * \beta}$ = $\lambda$eq?$_\alpha$.$\lambda$eq?$_\beta$.$\lambda$x.$\lambda$y. $\ldots$ in
+eq?$_{\alpha * \beta}$ eq?$_\tt{int}$ eq?$_\tt{char}$ (1, #"a") (2, #"b")
+  \end{lstlisting}
+\end{frame}
+
+
+\begin{frame}{Associated types}
+  \begin{itemize}
+    \item New \tt{assoc} declaration
+  \end{itemize}
 \end{frame}
 
 % TODO: why not Haskell?