WIP

macros.tex

@@ -77,7 +77,8 @@
 \newcommand{\Inl}{\keyw{inl}}
 \newcommand{\Inr}{\keyw{inr}}
 \newcommand{\Thunk}{\lambda \Unit.}
-\newcommand{\PCFRef}{\keyw{ref}}
+\newcommand{\PCFRef}{\dec{Ref}}
+\newcommand{\refv}{\keyw{ref}}
 
 \newcommand{\Pre}[1]{\mathsf{Pre}(#1)}
 \newcommand{\Abs}{\mathsf{Abs}}

thesis.bib

@@ -822,6 +822,18 @@
   year      = {2012}
 }
 
+@inproceedings{VazouL16,
+  author    = {Niki Vazou and
+               Daan Leijen},
+  title     = {From Monads to Effects and Back},
+  booktitle = {{PADL}},
+  series    = {{LNCS}},
+  volume    = {9585},
+  pages     = {169--186},
+  publisher = {Springer},
+  year      = {2016}
+}
+
 @inproceedings{PauwelsSM19,
   author    = {Koen Pauwels and
                Tom Schrijvers and
@@ -1517,7 +1529,7 @@
   year      = {1994}
 }
 
-# Simulation of delimited control using undelimited control
+# Simulation of delimited control using undelimited control & monadic reflection
 @inproceedings{Filinski94,
   author    = {Andrzej Filinski},
   title     = {Representing Monads},
@@ -1527,6 +1539,13 @@
   year      = {1994}
 }
 
+@phdthesis{Filinski96,
+  author    = {Andrzej Filinski},
+  title     = {Controlling Effects},
+  school    = {Carnegie Mellon University},
+  year      = {1996}
+}
+
 # Landin's J operator
 @article{Landin65,
   author    = {Peter J. Landin},
@@ -3247,4 +3266,4 @@
   number    = {1},
   pages     = {1--32},
   year      = {2003}
-}
+}

thesis.tex

@@ -434,6 +434,195 @@ concerned with each time period.
 
 \subsection{Early days of direct-style}
 
+It is well-known that $\Callcc$ exhibits both time and space
+performance problems for various implementing various
+effects~\cite{Kiselyov12}.
+%
+\subsubsection{Builtin mutable state}
+Builtin mutable state comes with three operations.
+%
+\[
+  \refv : S \to \PCFRef~S \qquad\quad
+  ! : \PCFRef~S \to S     \qquad\quad
+  \defnas~ : \PCFRef \to S \to \Unit
+\]
+%
+The first operation \emph{initialises} a new mutable state cell; the
+second operation \emph{gets} the value of a given state cell; and the
+third operation \emph{puts} a new value into a given state cell. It is
+important to note here retrieving contents of the state cell is an
+idempotent action, whilst modifying the contents is a destructive
+action.
+
+The following function illustrates a use of the get and put primitives
+to manipulate the contents of some global state cell $st$.
+%
+\[
+  \bl
+    \incrEven : \UnitType \to \Bool\\
+    \incrEven\,\Unit \defas \Let\;v \revto !st\;\In\;st \defnas 1 + v\;\In\;\even~st
+  \el
+\]
+%
+The type signature is oblivious to the fact that the function
+internally makes use of the state effect to compute its return value.
+%
+We can run this computation as a subcomputation in the context of
+global state cell $st$.
+%
+\[
+  \Let\;st \revto \refv~4\;\In\;\Record{\incrEven\,\Unit;!st} \reducesto^+ \Record{\True;5} : \Bool \times \Int
+\]
+%
+Operationally, the whole computation initialises the state cell $st$
+to contain the integer value $4$. Subsequently it runs the $\incrEven$
+computation, which returns the boolean value $\True$ and as a
+side-effect increments the value of $st$ to be $5$. The whole
+computation returns the boolean value paired with the final value of
+the state cell.
+
+\subsubsection{Transparent state-passing purely functionally}
+%
+\[
+  \bl
+    \incrEven : \UnitType \to \Int \to \Bool \times \Int\\
+    \incrEven\,\Unit \defas \lambda st. \Record{\even~st; 1 + st}
+  \el
+\]
+%
+State-passing is a global phenomenon that requires us to rewrite the
+signatures (and their implementations) of all functions that makes use
+of state, i.e. in order to endow an $n$-ary function that returns some
+value of type $R$ with state $S$ we have to transform its type as
+follows.
+%
+\[
+    \val{A_1 \to \cdots \to A_n \to R}_S
+  = A_0 \to \cdots \to A_n \to S \to R \times S
+\]
+%
+\subsubsection{Opaque state-passing with delimited control}
+%
+Delimited control appears during the late 80s in different
+forms~\cite{SitaramF90,DanvyF89}.
+%
+There are several different forms of delimited control.  The
+particular form of delimited control that I will use here is due to
+\citet{DanvyF89}.
+%
+Nevertheless, the secret sauce of all forms of delimited control is
+that a delimited control operator makes it possible to pry open
+function boundaries as control may transfer out of an arbitrary
+evaluation context, leaving behind a hole that can later be filled by
+some value supplied externally.
+
+\citeauthor{DanvyF89}'s formulation of delimited control introduces
+the following two primitives.
+%
+\[
+  \reset{-} : (\UnitType \to R) \to R \qquad\quad
+  \shift : ((A \to R) \to R) \to A
+\]
+%
+The first primitive $\reset{-}$ (pronounced `reset') is a control
+delimiter. Operationally, reset evaluates a given thunk in an empty
+evaluation context and returns the final result of that evaluation.
+%
+The second primitive $\shift$ is a control reifier. An application
+$\shift$ reifies and erases the control state up to (but not
+including) the nearest enclosing reset. The reified control state
+represents the continuation of the invocation of $\shift$ (up to the
+innermost reset); it gets passed as a function to the argument of
+$\shift$.
+
+Both primitives are defined over some (globally) fixed result type
+$R$.
+%
+By instantiating $R = S \to A \times S$, where $S$ is the type of
+state and $A$ is the type of return values, then we can use shift and
+reset to simulate mutable state using state-passing in way that is
+opaque to the rest of the program.
+%
+Let us first define operations for accessing and modifying the state
+cell.
+%
+\[
+  \ba{@{~}l@{\qquad\quad}@{~}r}
+  \multirow{2}{*}{
+    \bl
+      \getF : \UnitType \to S\\
+      \getF~\Unit \defas \shift\,(\lambda k.\lambda st. k~st~st)
+    \el} &
+  \multirow{2}{*}{
+    \bl
+      \putF : S \to \UnitType\\
+      \putF~st \defas \shift\,(\lambda k.\lambda st'.k~\Unit~st)
+    \el} \\ & % space hack to avoid the next paragraph from
+                % floating into the math environment.
+  \ea
+\]
+%
+The body of $\getF$ applies $\shift$ to capture the current
+continuation, which gets supplied to the anonymous function
+$(\lambda k.\lambda st. k~st~st)$. The continuation parameter $k$ has
+type $S \to S \to A \times S$. The continuation is applied to two
+instances of the current state value $st$. The instance the value
+returned to the caller of $\getF$, whilst the second instance is the
+state value available during the next invocation of either $\getF$ or
+$\putF$. This aligns with the intuition that accessing a state cell
+does not modify its contents. The implementation of $\putF$ is
+similar, except that the first argument to $k$ is the unit value,
+because the caller of $\putF$ expects a unit in return. Also, it
+ignores the current state value $st'$ and instead passes the state
+argument $st$ onto the activation of the next state operation. Again,
+this aligns with the intuition that modifying a state cell destroys
+its previous contents.
+
+Using these two operations we can implement a version of $\incrEven$
+that takes advantage of delimited control to simulate global state.
+%
+\[
+  \bl
+    \incrEven : \UnitType \to \Bool\\
+    \incrEven\,\Unit \defas \Let\;st \revto \getF\,\Unit\;\In\;\putF\,(1 + st);\,\even~st
+  \el
+\]
+%
+Modulo naming of operations, this version is similar to the version
+that uses builtin state. The type signature of the function is even
+the same.
+%
+Before we can apply this function we must first a state initialiser.
+%
+\[
+  \bl
+    \runState : (\UnitType \to A) \to S \to A \times S\\
+    \runState~m~st_0 \defas \reset{\lambda\Unit.\Let\;x \revto m\,\Unit\;\In\;\lambda st. \Record{x;st}}\,st_0
+      \bl
+      \el
+  \el
+\]
+%
+The function $\runState$ acts as both the state cell initialiser and
+runner of the stateful computation. The first parameter $m$ is a thunk
+that may perform stateful operations and the second parameter $st_0$
+is the initial value of the state cell. The implementation wraps an
+instance of reset around the application of $m$ in order to delimit
+the extent of applications of $\shift$ within $m$. It is important to
+note that each invocation of $\getF$ and $\putF$ gives rise to a
+state-accepting function, thus when $m$ is applied a chain of
+state-accepting functions gets constructed lazily. The chain ends in
+the state-accepting function returned by the reset instance. The
+application of the reset instance to $st_0$ effectively causes
+evaluation of each function in this chain to start.
+
+After instantiating $A = \Bool$ and $S = \Int$ we can use the
+$\runState$ function to apply the $\incrEven$ function.
+%
+\[
+  \runState~\incrEven~4~ \reducesto^+ \Record{\True;5} : \Bool \times \Int
+\]
+
 \subsection{Monadic epoch}
 During the late 80s and early 90s monads rose to prominence as a
 practical programming idiom for structuring effectful
@@ -454,10 +643,22 @@ In practical programming terms, monads may be thought of as
 constituting a family of design patterns, where each pattern gives
 rise to a distinct effect with its own operations.
 %
+The part of the appeal of monads is that they provide a structured
+interface for programming with effects such as state, exceptions,
+nondeterminism, and so forth, whilst preserving the equational style
+of reasoning about pure functional
+programs~\cite{GibbonsH11,Gibbons12}.
+%
 % Notably, they form the foundations for effectful programming in
 % Haskell, which adds special language-level support for programming
 % with monads~\cite{JonesABBBFHHHHJJLMPRRW99}.
 %
+
+The presentation of monads here is inspired by \citeauthor{Wadler92}'s
+presentation of monads for functional programming~\cite{Wadler92}, and
+it should be familiar to users of
+Haskell~\cite{JonesABBBFHHHHJJLMPRRW99}.
+
 \begin{definition}
   A monad is a triple $(T^{\TypeCat \to \TypeCat}, \Return, \bind)$
   where $T$ is some unary type constructor, $\Return$ is an operation
@@ -482,11 +683,12 @@ rise to a distinct effect with its own operations.
   \end{reductions}
 \end{definition}
 %
-Monads have a proven track record of successful applications.
+The monad laws ensure that monads have some algebraic structure.
 
-Monads have also given rise to various popular control-oriented
+The success of monads as a programming idiom is difficult to
-programming abstractions, e.g. the asynchronous programming idiom
+understate as monads have given rise to several popular
-async/await has its origins in monadic
+control-oriented programming abstractions including the asynchronous
+programming idiom async/await has its origins in monadic
 programming~\cite{Claessen99,LiZ07,SymePL11}.
 
 % \subsection{Option monad}
@@ -521,9 +723,10 @@ programming~\cite{Claessen99,LiZ07,SymePL11}.
 
 \subsubsection{State monad}
 %
-The state monad encapsulates mutable state by using the state-passing
+The state monad is an instantiation of the monad interface that
-technique internally. It provides two operations for manipulating the
+encapsulates mutable state by using the state-passing technique
-state cell.
+internally. In addition it equip the monad with two operations for
+manipulating the state cell.
 %
 \begin{definition}\label{def:state-monad}
   The state monad is defined over some fixed state type $S$.
@@ -595,8 +798,9 @@ The literature often presents the state monad with a fourth equation,
 which states that $\getF$ is idempotent. However, this equation is
 redundant as it is derivable from the first and third equations.
 
-The following bit toggling function illustrates a use of the state
+We can implement a monadic variation of the $\incrEven$ function that
-monad.
+uses the state monad to emulate manipulations of the state cell as
+follows.
 %
 \[
   \bl
@@ -622,15 +826,28 @@ $\even : \Int \to \Bool$ to the original state value to test whether
 its parity is even. The structure of the monad means that the result
 of running this computation gives us a pair consisting of boolean
 value indicating whether the initial state was even and the final
-state value. For instance, if the initial state value is $\True$, then
+state value.
-the computation yields
+
+The state initialiser and monad runner is simply thunk forcing and
+function application combined.
 %
 \[
-  \incrEven~\Unit~4 \reducesto^+ \Record{\True;5},
+  \bl
+    \runState : (\UnitType \to T~A) \to S \to A \to S\\
+    \runState~m~st_0 \defas m~\Unit~st_0\\
+   \el
 \]
 %
-where the first component contains the initial state value and the
+By instantiating $S = \Int$ and $A = \Bool$ we can obtain the same
-second component contains the final state value.
+result as before.
+%
+\[
+  \runState~\incrEven~4 \reducesto^+ \Record{\True;5} : \Bool \times \Int
+\]
+%
+We can instantiate the monad structure in a similar way to simulate
+other computational effects such as exceptions, nondeterminism,
+concurrency, and so forth~\cite{Moggi91,Wadler92}.
 
 \subsubsection{Continuation monad}
 As in J.R.R. Tolkien's fictitious Middle-earth~\cite{Tolkien54} there
@@ -812,11 +1029,11 @@ operation is another computation tree node.
 \[
   \bl
     \dec{FreeState}~S~R \defas [\Get:S \to R|\Put:\Record{S;R}] \smallskip\\
-    \fmap~f~x \defas \Case\;x\;\{
+    \fmap~f~op \defas \Case\;op\;\{
-    \bl
+    \ba[t]{@{}l@{~}c@{~}l}
-       \Get~k \mapsto \Get\,(\lambda st.f\,(k~st));\\
+       \Get~k    &\mapsto& \Get\,(\lambda st.f\,(k~st));\\
-       \Put~st'~k \mapsto \Put\,\Record{st';f~k}\}
+       \Put~st~k &\mapsto& \Put\,\Record{st;f~k}\}
-    \el
+    \ea
   \el
 \]
 %
@@ -838,8 +1055,8 @@ operation is another computation tree node.
 %
 \[
   \bl
-    \runState : S \to \Free\,(\dec{FreeState}~S)\,A \to A \times S\\
+    \runState : \Free\,(\dec{FreeState}~S)\,A \to S \to A \times S\\
-    \runState~st~m \defas
+    \runState~m~st \defas
       \Case\;m\;\{
       \ba[t]{@{~}l@{~}c@{~}l}
          \return~x      &\mapsto& (x, st);\\
@@ -854,7 +1071,7 @@ operation is another computation tree node.
 \]
 
 \subsection{Back to direct-style}
-
+Combining monadic effects~\cite{VazouL16}\dots
 
 \subsubsection{Effect tracking}
 
@@ -1320,13 +1537,13 @@ distinct notions of continuations. It is common in the literature to
 find the word `continuation' accompanied by a qualifier such as full,
 partial, abortive, escape, undelimited, delimited, composable, or
 functional (in Chapter~\ref{ch:cps} I will extend this list by three
-new ones). Some of these notions of continuations synonyms, whereas
+new ones). Some of these notions of continuations are synonymous,
-others have distinct meaning. Common to all notions of continuations
+whereas others have distinct meanings. Common to all notions of
-is that in essence they represent the control state. However, the
+continuations is that they represent the control state. However, the
 extent and behaviour of continuations differ widely from notion to
 notion. The essential notions of continuations are
 undelimited/delimited and abortive/composable. To tell them apart, we
-will classify them by their operational behaviour.
+will classify them according to their operational behaviour.
 
 The extent and behaviour of a continuation in programming are
 determined by its introduction and elimination forms,