paper: more progress

paper/main.tex

-\documentclass[12pt]{article}
+\documentclass[11pt]{article}
 
 \usepackage{amssymb, amsmath, amsthm, amsrefs}
 
@@ -12,12 +12,12 @@
 
 %% better code font
 % https://tex.stackexchange.com/q/88001/5764
-\usepackage{listings, plex-mono, letltxmacro}
+\usepackage{listings, inconsolata, letltxmacro}
 \lstset{basicstyle=\ttfamily\footnotesize, breaklines=true}
 \LetLtxMacro\oldttfamily\ttfamily
 \DeclareRobustCommand{\ttfamily}{\oldttfamily\csname ttsize\endcsname}
 \newcommand{\setttsize}[1]{\def\ttsize{#1}}%
-\setttsize{\footnotesize}
+\setttsize{\small}
 
 % ONE MOTHERFUCKING SPACE AFTER EACH MOTHERFUCKING SENTENCE
 \frenchspacing
@@ -34,6 +34,13 @@
 % backslash alias
 \newcommand{\bs}{\, \backslash \,}
 
+% teletype alias
+\renewcommand{\tt}{\texttt}
+
+
+\usepackage{multicol}
+\setlength\columnsep{33pt}
+
 \title{Iterative Programming in ML Languages with Type Classes and Associated Types}
 \author{
   Mark Cohen\\
@@ -56,7 +63,73 @@
 
 % gobble page number for title
 \thispagestyle{empty}
-\newpage
+\clearpage
+
+\begin{multicols*}{2}
+
+\section{Introduction}
+Iterative programming is second-to-none in terms of being powerful, highly intuitive, and having a
+low cognitive load. Other disciplines of programming with collections come with substantial
+tradeoffs. Using purely functional \tt{map}, \tt{filter}, and \tt{fold} is substantially less
+powerful, as there's no mechanism for reusing code across different types of collections. And using
+monadic sequencing operators is highly powerful and has a low cognitive load once the programmer
+clears the bar for understanding this discipline; unfortunately, that bar is very high.
+
+Consider the following Python program:
+\begin{lstlisting}
+for (k, v) in db:
+    if query(k):
+        res.append((k, v))
+return dict(res)
+\end{lstlisting}
+This is highly intuitive: the gap between one's mental model and the actual program is minimal. This
+particular snippet iterates over all key-value pairs in a dictionary, performs some query on each
+one, and appends all keys that pass the query to some response list. Then, it converts that response
+list to a dictionary with blank values.
+
+Contrast the above with the following equivalent Standard ML (SML) program:
+\begin{lstlisting}
+let
+  fun arrToDict' d [] = d
+    | arrToDict' d ((k, v) :: xs) =
+        arrToDict' (dictAdd d (k, v)) xs
+  fun arrToDict xs = arrToDict' {} xs
+in
+  arrToDict (filter (fn (k, _) => query k) d)
+end
+\end{lstlisting}
+This is, in contrast, highly unintuitive: it requires one to think inside-out. To be sure, this
+discipline of programming has many benefits, chiefly that it is purely functional. An additional
+benefit is that languages in this discipline tend to be type-sound, where languages in the iterative
+discipline tend to be either untyped (Python, Javascript, etc) or weakly typed (C, Java, etc). These
+tendencies are purely correlative, but nonetheless represent real-world constraints.
+
+One notable exception to this rule is Rust, which provides iteration based on traits ((TODO: cite
+Scharli, also maybe some Rust papers?)). Below is a Rust program equivalent to the two discussed
+above:
+\begin{lstlisting}
+for (k, v) in db.iter() {
+    if query(k) {
+        res.push(v);
+    }
+};
+res.collect::<HashMap<K, V>>()
+\end{lstlisting}
+
+
+\end{multicols*}
+
+
+
+
+
+
+
+
+
+
+
+\clearpage
 
 \begin{table}
   \renewcommand{\arraystretch}{3.5}

presentation/main.tex

@@ -15,7 +15,7 @@
 \LetLtxMacro\oldttfamily\ttfamily
 \DeclareRobustCommand{\ttfamily}{\oldttfamily\csname ttsize\endcsname}
 \newcommand{\setttsize}[1]{\def\ttsize{#1}}%
-\setttsize{\footnotesize}
+\setttsize{\small}
 
 % ONE MOTHERFUCKING SPACE AFTER EACH MOTHERFUCKING SENTENCE
 \frenchspacing
@@ -593,7 +593,7 @@ eq?$_{\alpha * \beta}$ eq?$_\tt{int}$ eq?$_\tt{char}$ (1, #"a") (1, #"a")
       \infer[no rule] 3{A, (x' :: \tau' \bs x_{\tau'}) \proves e :: \sigma \bar{\rho} \; \tau \bs \bar{e}}
       \infer[no rule] 1 {A, (x' :: \tau' \bs x_{\tau'}) \proves e' :: \sigma'' \rho'' \tau'' \bs \bar{e}'}
       \infer 1 {
-        A \proves (\tt{inst } x :: \sigma \rho \, \tau = e \tt{ in } e') ::
+        A \proves (\tt{inst } x :: \sigma \rho \tau = e \tt{ in } e') ::
         \sigma'' \rho'' \tau'' \bs (\tt{inst } x ::
       \sigma \bar{\rho} \tau = \lambda x'_{\tau'} . \bar{e} \tt{ in } \bar{e}')}
     \end{prooftree}