WIP

macros.tex

@@ -351,8 +351,14 @@
 \newcommand{\fail}{\dec{fail}}
 \newcommand{\optionalise}{\dec{optionalise}}
 \newcommand{\bind}{\ensuremath{\gg\!=}}
-\newcommand{\return}{\dec{return}}
+\newcommand{\return}{\dec{Return}}
 \newcommand{\faild}{\dec{withDefault}}
+\newcommand{\Free}{\dec{Free}}
+\newcommand{\OpF}{\dec{Op}}
+\newcommand{\DoF}{\dec{do}}
+\newcommand{\getF}{\dec{get}}
+\newcommand{\putF}{\dec{put}}
+\newcommand{\fmap}{\dec{fmap}}
 
 % Abstract machine
 \newcommand{\cek}[1]{\ensuremath{\langle #1 \rangle}}

thesis.bib

@@ -768,6 +768,26 @@
   year      = {1992}
 }
 
+@article{Wadler92b,
+  author    = {Philip Wadler},
+  title     = {Comprehending Monads},
+  journal   = {Math. Struct. Comput. Sci.},
+  volume    = {2},
+  number    = {4},
+  pages     = {461--493},
+  year      = {1992}
+}
+
+@inproceedings{JonesW93,
+  author    = {Simon L. Peyton Jones and
+               Philip Wadler},
+  title     = {Imperative Functional Programming},
+  booktitle = {{POPL}},
+  pages     = {71--84},
+  publisher = {{ACM} Press},
+  year      = {1993}
+}
+
 @inproceedings{Wadler95,
   author    = {Philip Wadler},
   title     = {Monads for Functional Programming},
@@ -3168,3 +3188,13 @@
   year  = {2011},
   booktitle = {{TPDC}}
 }
+
+# Fellowship of the Ring reference
+@book{Tolkien54,
+  title = {The lord of the rings: Part 1: The fellowship of the ring},
+  author    = {John Ronald Reuel Tolkien},
+  publisher = {Allen and Unwin},
+  year      = 1954,
+  language = {eng},
+  keywords = {Fiction},
+}

thesis.tex

@@ -398,11 +398,196 @@ expressiveness.
 \subsection{Why effect handlers matter}
 
 \section{State of effectful programming}
-\subsection{Monadic programming}
+
+\subsection{Dark age of impurity}
+
+\subsection{Monadic enlightenment}
+During the late 80s and early 90s monads rose to prominence as a
+practical program structuring idiom for effectful
+programming. Notably, they form the foundations for effectful
+programming in Haskell, which adds special language-level support for
+programming with monads~\cite{JonesABBBFHHHHJJLMPRRW99}.
+%
+\begin{definition}
+  A monad is a triple $(T, \Return, \bind)$ where $T$ is some unary
+  type constructor, $\Return$ is an operation that lifts an arbitrary
+  value into the monad (sometimes this operation is called `the unit
+  operation'), and $\bind$ is an application operator the monad (this
+  operator is pronounced `bind'). Implementations of $\Return$ and
+  $\bind$ must conform to the following interface.
+  %
+  \[
+    \bl
+      \Return : A \to T~A \qquad\quad \bind ~: T~A \to (A \to T~B) \to T~B
+    \el
+  \]
+  %
+  Interactions between $\Return$ and $\bind$ are governed by the
+  so-called `monad laws'.
+  \begin{reductions}
+    \slab{Left\textrm{ }identity} & \Return\;x \bind k &=& k~x\\
+    \slab{Right\textrm{ }identity} & m \bind \Return &=& m\\
+    \slab{Associativity} & (m \bind k) \bind f &=& m \bind (\lambda x. k~x \bind f)
+  \end{reductions}
+\end{definition}
+%
 Monads have given rise to various popular control-oriented programming
-abstractions, e.g. async/await originates from monadic
+abstractions, e.g. the async/await idiom has its origins in monadic
 programming~\cite{Claessen99,LiZ07,SymePL11}.
 
+\subsection{Option monad}
+The $\Option$ type is a unary type constructor with two data
+constructors, i.e.  $\Option~A \defas [\Some:A|\None]$.
+
+\begin{definition} The option monad is a monad equipped with a single
+  failure operation.
+  %
+  \[
+    \ba{@{~}l@{\qquad}@{~}r}
+      \multicolumn{2}{l}{T~A \defas \Option~A} \smallskip\\
+      \multirow{2}{*}{
+        \bl
+         \Return : A \to T~A\\
+         \Return \defas \lambda x.\Some~x
+        \el} &
+      \multirow{2}{*}{
+        \bl
+          \bind ~: T~A \to (A \to T~B) \to T~B\\
+          \bind ~\defas \lambda m.\lambda k.\Case\;m\;\{\None \mapsto \None;\Some~x \mapsto k~x\}
+          \el}\\ & \smallskip\\
+      \multicolumn{2}{l}{
+        \bl
+          \fail : A \to T~A\\
+          \fail \defas \lambda x.\None
+        \el}
+    \ea
+  \]
+  %
+\end{definition}
+
+\subsection{State monad}
+
+\subsection{Continuation monad}
+As in J.R.R. Tolkien's fictitious Middle-earth~\cite{Tolkien54} there
+exists one monad to rule them all, one monad to realise them, one
+monad to subsume them all, and in the term language bind them. This
+powerful monad is the \emph{continuation monad}.
+
+\begin{definition}
+  The continuation monad is defined over some fixed return type
+  $R$~\cite{Wadler92}.
+  %
+  \[
+    \ba{@{~}l@{\qquad\quad}@{~}r}
+      \multicolumn{2}{l}{T~A \defas (A \to R) \to R} \smallskip\\
+      \multirow{2}{*}{
+        \bl
+         \Return : A \to T~A\\
+         \Return \defas \lambda x.\lambda k.k~x
+        \el} &
+      \multirow{2}{*}{
+        \bl
+          \bind ~: T~A \to (A \to T~B) \to T~B\\
+          \bind ~\defas \lambda m.\lambda k.\lambda f.m~(\lambda x.k~x~f)
+          \el} \\ & % space hack to avoid the next paragraph from
+                    % floating into the math environment.
+    \ea
+  \]
+  %
+\end{definition}
+%
+The $\Return$ operation lifts a value into the monad by using it as an
+argument to the continuation $k$. The bind operator applies the monad
+$m$ to an anonymous function that accepts a value $x$ of type
+$A$. This value $x$ is supplied to the immediate continuation $k$
+alongside the current continuation $f$.
+
+Scheme's undelimited control operator $\Callcc$ is definable as a
+monadic operation on the continuation monad~\cite{Wadler92}.
+%
+\[
+  \bl
+    \Callcc : ((A \to T~B) \to T~A) \to T~A\\
+    \Callcc \defas \lambda f.\lambda k. f\,(\lambda x.\lambda.k'.k~x)~k
+  \el
+\]
+
+\subsection{Free monad}
+Just like other monads the free monad satisfies the monad laws,
+however, unlike other monads the free monad does not perform any
+computation \emph{per se}. Instead the free monad builds an abstract
+representation of the computation in form of a computation tree, whose
+interior nodes correspond to an invocation of some operation on the
+monad, where each outgoing edge correspond to a possible continuation
+of the operation; the leaves correspond to return values. The meaning
+of a free monadic computation is ascribed by a separate function, or
+interpreter, that traverses the computation tree.
+
+The shape of computation trees is captured by the following generic
+type definition.
+%
+\[
+  \Free~F~A \defas [\return:A|\OpF:F\,(\Free~F~A)]
+\]
+%
+The type constructor $\Free$ takes two type arguments. The first
+parameter $F$ is itself a type constructor of kind
+$\TypeCat \to \TypeCat$. The second parameter is the usual type of
+values computed by the monad. The $\Return$ tag creates a leaf of the
+computation tree, whilst the $\OpF$ tag creates an interior node. In
+the type signature for $\OpF$ the type variable $F$ is applied to the
+$\Free$ type. The idea is that $F~K$ computes an enumeration of the
+signatures of the possible operations on the monad, where $K$ is the
+type of continuation for each operation. Thus the continuation of an
+operation is another computation tree node.
+%
+\begin{definition} The free monad is a triple
+  $(F^{\TypeCat \to \TypeCat}, \Return, \bind)$ which forms a monad
+  with respect to $F$. In addition an adequate instance of $F$ must
+  supply a map, $\dec{fmap} : (A \to B) \to F~A \to F~B$, over its
+  structure.
+  %
+  \[
+   \bl
+     T~A \defas \Free~F~A \smallskip\\
+     \Return : A \to T~A\\
+     \Return \defas \lambda x.\return~x\\
+     \bind ~: T~A \to (A \to T~B) \to T~B\\
+     \bind ~\defas \lambda m.\lambda k.\Case\;m\;\{\return~x \mapsto k~x;\OpF~y \mapsto \OpF\,(\fmap\,(\lambda m'. m' \bind k)\,y)\}
+     \el
+   \]
+   %
+   We define an auxiliary function to alleviate some of the
+   boilerplate involved with performing operations on the monad.
+   %
+   \[
+     \bl
+       \DoF : F~A \to \Free~F~A\\
+       \DoF \defas \lambda op.\OpF\,(\fmap\,(\lambda x.\return~x)\,op)
+     \el
+  \]
+  %
+\end{definition}
+
+\[
+  \bl
+    \dec{FreeState}~S~R \defas [\Get:S \to R|\Put:\Record{S;R}|\Done] \smallskip\\
+    \fmap~f~x \defas \Case\;x\;\{
+    \bl
+       \Get~k \mapsto \Get\,(\lambda st.f\,(k~st));\\
+       \Put~st'~k \mapsto \Put\,\Record{st';f~k};\\
+       \Done \mapsto \Done\}
+    \el \smallskip\\
+    \getF : \UnitType \to T~S\\
+    \getF~\Unit \defas \DoF~(\Get\,(\lambda x.x)))\\
+    \putF : S \to T~\UnitType\\
+    \putF~st \defas \DoF~(\Put\,\Record{st;\Unit})
+  \el
+\]
+
+\subsection{Direct-style revolution}
+
+
 \section{Contributions}
 The key contributions of this dissertation are the following:
 \begin{itemize}
@@ -432,7 +617,7 @@ The key contributions of this dissertation are the following:
     notions of continuations and first-class control phenomena.
 \end{itemize}
 
-\section{Thesis outline}
+\section{Structure of this dissertation}
 Chapter~\ref{ch:maths-prep} defines some basic mathematical
 notation and constructions that are they pervasively throughout this
 dissertation.
@@ -8063,7 +8248,7 @@ $\Co$-operations have been handled.
 %
 In the definition the scheduler state is bound by the name $st$.
 
-The $\return$ case is invoked when a process completes. The return
+The $\Return$ case is invoked when a process completes. The return
 value $x$ is paired with the identifier of the currently executing
 process and consed onto the list $done$. Subsequently, the function
 $\runNext$ is invoked in order to the next ready process.
@@ -16288,19 +16473,22 @@ handlers only get amplified in the setting of multi handlers.
 
 \paragraph{Handling linear resources} The implementation of effect
 handlers in Links makes the language unsound, because the \naive{}
-combination of effect handlers and session typing is unsound. For
-instance, it is possible to break session fidelity by twice resuming
-some resumption that closes over a receive operation. Similarly, it is
-possible to break type safety by using a combination of exceptions and
-multi-shot resumptions, e.g. suppose some channel first expects an
-integer followed by a boolean, then the running the program
+combination of effect handlers and session typing is unsound. The
+combined power of being able to discard some resumptions and resume
+others multiple times can make for bad interactions with sessions. For
+instance, suppose some channel supplies only one value, then it is
+possible to break session fidelity by twice resuming some resumption
+that closes over a receive operation. Similarly, it is possible to
+break type safety by using a combination of exceptions and multi-shot
+resumptions, e.g. suppose some channel first expects an integer
+followed by a boolean, then the running the program
 $\Do\;\Fork\,\Unit;\keyw{send}~42;\Absurd\;\Do\;\Fail\,\Unit$ under
 the composition of the nondeterminism handler and default failure
 handler from Chapter~\ref{ch:unary-handlers} will cause the primitive
 $\keyw{send}$ operation to supply two integers in succession, thus
 breaking the session protocol. Figuring out how to safely combine
-linear resources, such as channels, and effect handlers with
-multi-shot resumptions is an interesting unsolved problem.
+linear resources, such as channels, and handlers with multi-shot
+resumptions is an interesting unsolved problem.
 
 \section{Canonical implementation strategies for handlers}
 Chapter~\ref{ch:cps} carries out a comprehensive study of CPS