WIP

thesis.bib

@@ -1413,6 +1413,13 @@
   year      = {2010}
 }
 
+@book{Dybvig03,
+  author    = {R. Kent Dybvig},
+  title     = {The {Scheme} Programming Language, Third Edition},
+  publisher = {{MIT} Press},
+  year      = {2003}
+}
+
 # Haskell
 @misc{JonesABBBFHHHHJJLMPRRW99,
   author = {Simon Peyton Jones
@@ -3267,3 +3274,58 @@
   pages     = {1--32},
   year      = {2003}
 }
+
+# Undelimited control is insufficient to express mutable state
+@techreport{FriedmanS00,
+  author = {Daniel P. Friedman and Amr Sabry},
+  title = {Recursion is a Computational Effect},
+  institution = {Computer Science Department, Indiana University},
+  address   = {Bloomington, Indiana 47405, USA},
+  type = {Technical report},
+  number = {546},
+  year = {200},
+}
+
+# Fortran
+@inproceedings{BackusBBGHHNSSS57,
+  author    = {John W. Backus and
+               Robert J. Beeber and
+               Sheldon Best and
+               Richard Goldberg and
+               Lois M. Haibt and
+               Harlan L. Herrick and
+               Robert A. Nelson and
+               David Sayre and
+               Peter B. Sheridan and
+               H. Stern and
+               Irving Ziller and
+               Robert A. Hughes and
+               R. Nutt},
+  title     = {The {FORTRAN} automatic coding system},
+  booktitle = {{IRE-AIEE-ACM} Computer Conference (Western)},
+  pages     = {188--198},
+  publisher = {{ACM}},
+  year      = {1957}
+}
+
+# Algol
+@article{BackusBGKMPRSVWWW60,
+  author    = {John W. Backus and
+               Friedrich L. Bauer and
+               Julien Green and
+               C. Katz and
+               John McCarthy and
+               Alan J. Perlis and
+               Heinz Rutishauser and
+               Klaus Samelson and
+               Bernard Vauquois and
+               Joseph Henry Wegstein and
+               Adriaan van Wijngaarden and
+               Michael Woodger},
+  title     = {Report on the algorithmic language {ALGOL} 60},
+  journal   = {Commun. {ACM}},
+  volume    = {3},
+  number    = {5},
+  pages     = {299--314},
+  year      = {1960}
+}

thesis.tex

@@ -426,20 +426,88 @@ language.
 
 \section{State of effectful programming}
 
-The evolution of effectful programming has gone through several
+Programming with effects can be done in basically three different
-characteristic time periods. In this section I will provide a brief
+ways: 1) usage of builtin effects, 2) simulation via global program
-programming perspective on how effectful programming has evolved as
+transformations, or 3) simulation via control effects.
-well as providing an informal introduction to the core concepts
+%
-concerned with each time period.
+In this section I will provide a brief programming perspective on the
+various approaches to programming with effects. We will look at each
+approach through the lens of a singular effect, namely, global mutable
+state.
 
-\subsection{Early days of direct-style}
+% how
+% effectful programming has evolved as well as providing an informal
+% introduction to the involved core concepts. We will look at the
+% evolution of effectful programming through the lens of a singular
+% effect, namely, global mutable state.
 
-It is well-known that $\Callcc$ exhibits both time and space
+% The evolution of effectful programming has gone through several
-performance problems for various implementing various
+% characteristic time periods. In this section I will provide a brief
-effects~\cite{Kiselyov12}.
+% programming perspective on how effectful programming has evolved as
+% well as providing an informal introduction to the core concepts
+% concerned with each time period. We will look at the evolution of
+% effectful programming through the lens of a singular effect, namely,
+% global mutable state.
+
+\subsection{Direct-style state}
+%
+We can realise stateful behaviour by either using language-supported
+state primitives, globally structure our program to follow a certain
+style, or use first-class control in the form of delimited control to
+simulate state. As for simulating state with control effects we
+consider only delimited control, because undelimited control is
+insufficient to express mutable state~\cite{FriedmanS00}.
+% Programming in its infancy was effectful as the idea of first-class
+% control was conceived already during the design of the programming
+% language Algol~\cite{BackusBGKMPRSVWWW60} -- one of the early
+% high-level programming languages along with
+% Fortran~\cite{BackusBBGHHNSSS57} and Lisp~\cite{McCarthy60} -- when
+% \citet{Landin98} sought to model unrestricted goto-style jumps using
+% an extended $\lambda$-calculus. The power of \citeauthor{Landin98}'s
+% control facility was recognised early by \citet{Burstall69}, who used
+% it to implement a control abstraction for tree-based search.
+% %
+% % \citeauthor{Landin98}'s control facility did not gain popularity as a
+% % practical programming abstraction~\cite{Felleisen87b}.
+% \citeauthor{Landin98}'s control facility is a precursor to the
+% undelimited control operator $\Callcc$ (short for call with current
+% continuation), which first appeared in the programming language
+% Scheme~\cite{AbelsonHAKBOBPCRFRHSHW85}.
+
+%
+% The power of \citeauthor{Landin98}'s control facility was recognised early The nature of the first-class control introduced by
+% \citeauthor{Landin98} was undelimited. However, 
+
+% The early high-level programming languages
+% Fortran~\cite{BackusBBGHHNSSS57}, Algol~\cite{BackusBGKMPRSVWWW60},
+% and Lisp~\cite{McCarthy60} all hard-wire a particular set of effects
+% into their semantics. The usage of effects in these languages is
+% completely untracked, although, the languages belonging to the Lisp
+% family have adopted a naming convention to suffix names of
+% side-effecting operations with exclamation points, e.g. the state
+% modification operation is named $\keyw{set!}$~\cite{Dybvig03}.
+
+% The idea of undelimited first-class control was conceived during the
+% development of Algol~\cite{Landin65,Landin65a,Landin98}. The probably
+% most famous form of undelimited control, $\Callcc$, appeared
+% later~\cite{AbelsonHAKBOBPCRFRHSHW85}.
+
+% 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.
+It is common to find mutable state builtin into the semantics of
+mainstream programming languages. However, different languages vary in
+their approach to mutable state. For instance, state mutation
+underpins the foundations of imperative programming languages
+belonging to the C family of languages. They do typically not
+distinguish between mutable and immutable values at the level of
+types. Contrary, programming languages belonging to the ML family of
+languages use types to differentiate between mutable and immutable
+values. They reflect mutable values in types by using a special unary
+type constructor $\PCFRef^{\Type \to \Type}$. Furthermore, ML
+languages equip the $\PCFRef$ constructor with three operations.
 %
 \[
   \refv : S \to \PCFRef~S \qquad\quad
@@ -447,12 +515,12 @@ Builtin mutable state comes with three operations.
   \defnas~ : \PCFRef \to S \to \Unit
 \]
 %
-The first operation \emph{initialises} a new mutable state cell; the
+The first operation \emph{initialises} a new mutable state cell of
-second operation \emph{gets} the value of a given state cell; and the
+type $S$; the second operation \emph{gets} the value of a given state
-third operation \emph{puts} a new value into a given state cell. It is
+cell; and the third operation \emph{puts} a new value into a given
-important to note here retrieving contents of the state cell is an
+state cell. It is important to note that retrieving contents of the
-idempotent action, whilst modifying the contents is a destructive
+state cell is an idempotent action, whilst modifying the contents is a
-action.
+destructive action.
 
 The following function illustrates a use of the get and put primitives
 to manipulate the contents of some global state cell $st$.
@@ -460,13 +528,19 @@ 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
+    \incrEven\,\Unit \defas \Let\;v \revto !st\;\In\;st \defnas 1 + v;\,\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.
 %
+The body of the function first retrieves the current value of the
+state cell and binds it to $st$. Subsequently, it destructively
+increments the value of the state cell. Finally, it applies the
+predicate $\even : \Int \to \Bool$ to the original state value to test
+whether its parity is even.
+%
 We can run this computation as a subcomputation in the context of
 global state cell $st$.
 %
@@ -482,6 +556,29 @@ computation returns the boolean value paired with the final value of
 the state cell.
 
 \subsubsection{Transparent state-passing purely functionally}
+It is possible to implement stateful behaviour in a language without
+any computational effects, e.g. simply typed $\lambda$-calculus, by
+following a particular design pattern known as
+\emph{state-passing}. The principal idea is to parameterise stateful
+functions by the current state and make them return whatever result
+they compute along with the updated state value. More precisely, in
+order to endow some $n$-ary function with argument types $A_i$ and
+return type $R$ with state of type $S$, we transform the function
+signature as follows.
+%
+\[
+    \val{A_1 \to \cdots \to A_n \to R}_S
+  \defas A_1 \to \cdots \to A_n \to S \to R \times S
+\]
+%
+By convention we always insert the state parameter at the tail end of
+the parameter list. We may read the suffix $S \to R \times S$ as a
+sort of effect annotation indicating that a particular function
+utilises state. The downside of state-passing is that it is a global
+technique which requires us to rewrite the signatures (and their
+implementations) of all functions that makes use of state.
+
+We can reimplement the $\incrEven$ in state-passing style as follows.
 %
 \[
   \bl
@@ -490,17 +587,21 @@ the state cell.
   \el
 \]
 %
-State-passing is a global phenomenon that requires us to rewrite the
+State initialisation is simply function application.
-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
+  \incrEven~\Unit~4 \reducesto^+ \Record{\True;5} : \Bool \times \Int
-  = A_0 \to \cdots \to A_n \to S \to R \times S
 \]
 %
+Programming in state-passing style is laborious and no fun as it is
+anti-modular, because effect-free higher-order functions to work with
+stateful functions they too must be transformed or at the very least
+be duplicated to be compatible with stateful function arguments.
+%
+Nevertheless, state-passing is an important technique as it is the
+secret sauce that enables us to simulate mutable state with other
+programming techniques.
+
 \subsubsection{Opaque state-passing with delimited control}
 %
 Delimited control appears during the late 80s in different
@@ -623,7 +724,8 @@ $\runState$ function to apply the $\incrEven$ function.
   \runState~\incrEven~4~ \reducesto^+ \Record{\True;5} : \Bool \times \Int
 \]
 
-\subsection{Monadic epoch}
+% \subsection{Monadic epoch}
+\subsection{Monadic state}
 During the late 80s and early 90s monads rose to prominence as a
 practical programming idiom for structuring effectful
 programming~\cite{Moggi89,Moggi91,Wadler92,Wadler92b,JonesW93,Wadler95,JonesABBBFHHHHJJLMPRRW99}.
@@ -683,7 +785,16 @@ Haskell~\cite{JonesABBBFHHHHJJLMPRRW99}.
   \end{reductions}
 \end{definition}
 %
-The monad laws ensure that monads have some algebraic structure.
+\dhil{Remark that the monad type $T~A$ may be read as a tainted value}
+The monad interface may be instantiated in different ways to realise
+different computational effects. In the following subsections we will
+see three different instantiations with which we will implement global
+mutable state.
+
+The monad laws ensure that monads have some algebraic structure, which
+programmers can use when reasoning about their monadic programs, and
+optimising compilers may take advantage of the structure to emit more
+efficient code for monadic programs.
 
 The success of monads as a programming idiom is difficult to
 understate as monads have given rise to several popular
@@ -821,12 +932,11 @@ monad $T$~\cite{Moggi91,Wadler92}, i.e. $\getF$ and
 $\putF$. Operationally, the function retrieves the current value of
 the state cell via the invocation of $\getF$. The bind operator passes
 this value onto the continuation, which increments the value and
-invokes $\putF$. The continuation applies a predicate
+invokes $\putF$. The continuation applies a predicate the $\even$
-$\even : \Int \to \Bool$ to the original state value to test whether
+predicate to the original state value. The structure of the monad
-its parity is even. The structure of the monad means that the result
+means that the result of running this computation gives us a pair
-of running this computation gives us a pair consisting of boolean
+consisting of boolean value indicating whether the initial state was
-value indicating whether the initial state was even and the final
+even and the final state value.
-state value.
 
 The state initialiser and monad runner is simply thunk forcing and
 function application combined.
@@ -854,6 +964,8 @@ 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}\label{def:cont-monad}
   The continuation monad is defined over some fixed return type
@@ -915,16 +1027,27 @@ of the state cell; instead it returns simply the unit value $\Unit$.
 One can show that this implementation of $\getF$ and $\putF$ abides by
 the same equations as the implementation given in
 Definition~\ref{def:state-monad}.
-%
+
-By fixing $S = \Int$ we can use this particular continuation monad
+The state initialiser and runner for the monad supplies the initial
-instance to interpret $\incrEven$.
+continuation.
 %
 \[
-  \incrEven~\Unit~(\lambda x.\lambda st. \Record{x;st})~4 \reducesto^+ \Record{\True;5}
+  \bl
+    \runState : (\UnitType \to T~A) \to S \to A \times S\\
+    \runState~m~st_0 \defas m~\Unit~(\lambda x.\lambda st. \Record{x;st})~st_0
+  \el
 \]
 %
 The initial continuation $(\lambda x.\lambda st. \Record{x;st})$
 corresponds to the $\Return$ of the state monad.
+%
+As usual by fixing $S = \Int$ and $A = \Bool$, we can use this
+particular continuation monad instance to interpret $\incrEven$.
+%
+\[
+  \runState~\incrEven~4 \reducesto^+ \Record{\True;5} : \Bool \times \Int
+\]
+%
 
 % Scheme's undelimited control operator $\Callcc$ is definable as a
 % monadic operation on the continuation monad~\cite{Wadler92}.