Fix typo

macros.tex

@@ -377,4 +377,5 @@
 \newcommand{\State}{\dec{State}}
 \newcommand{\runState}{\dec{runState}}
 \newcommand{\Uget}{\dec{get}}
-\newcommand{\Uput}{\dec{put}}
+\newcommand{\Uput}{\dec{put}}
+\newcommand{\nl}{\textbackslash{}n}

thesis.bib

@@ -1298,4 +1298,11 @@
   number    = {4},
   pages     = {343--355},
   year      = {1995}
+}
+
+# Shakespeare's Hamlet
+@misc{Shakespeare6416,
+  author = {William Shakespeare},
+  title  = {The {Tragedy} of {Hamlet}, {Prince} of {Denmark}},
+  year   = {1564-1616}
 }

thesis.tex

@@ -28,7 +28,7 @@
 %\usepackage{lmodern}
 %\usepackage{palatino}
 % \usepackage{newpxtext,newpxmath}
-\usepackage[scaled=0.85]{beramono}
+\usepackage[scaled=0.80]{beramono}
 \usepackage[activate=true,
     final,
     tracking=true,
@@ -1663,7 +1663,7 @@ The term `pure' is heavily overloaded in the programming literature.
 %   back to 2016 when Richard Eisenberg asked me about how we do effect
 %   inference in Links.}
 
-\chapter{Unary handlers}
+\chapter{Programming with control via effect handlers}
 \label{ch:unary-handlers}
 %
 In this chapter we study various flavours of unary effect
@@ -2507,7 +2507,109 @@ The following handler implements this behaviour.
   \el
 \]
 %
-\dhil{This is an instance of non-blind backtracking}
+The $\Return$-case returns a singleton list containing a result of
+running $m$.
+%
+The $\Fork$-case invokes the provided resumption $resume$ twice. Each
+invocation of $resume$ effectively copies $m$ and runs each copy to
+completion. Each copy returns through the $\Return$-case, hence each
+invocation of $resume$ returns a list of the possible results obtained
+by interpreting $\Fork$ first as $\True$ and subsequently as
+$\False$. The results are joined by list concatenation ($\concat$).
+%
+Thus the handler returns a list of all the possible results of $m$.
+%
+In fact, this handler is exactly the handler for nondeterministic
+choice, and it satisfies the standard semi-lattice
+equations~\cite{PlotkinP09,PlotkinP13}.
+% \dhil{This is an instance of non-blind backtracking~\cite{FriedmanHK84}}
+
+Let us consider $\nondet$ together with the previously defined
+handlers. But first, let us define two computations.
+%
+\[
+  \bl
+    \quoteRitchie,\;\quoteHamlet : \UnitType \to \UnitType \eff \{\Write: \Record{\UFD;\String} \opto \UnitType\} \smallskip\\
+    \quoteRitchie\,\Unit \defas
+      \ba[t]{@{~}l}
+        \echo~\strlit{UNIX is basically };\\
+        \echo~\strlit{a simple operating system, };\\
+        \echo~\strlit{but };\\
+        \echo~\texttt{"}
+          \ba[t]{@{}l}
+             \texttt{you have to be a genius }\\
+             \texttt{to understand the simplicity.\nl{}"}
+          \ea
+      \ea \smallskip\\
+    \quoteHamlet\,\Unit \defas
+      \ba[t]{@{}l}
+        \echo~\strlit{To be, or not to be, };\\
+        \echo~\strlit{that is the question:\nl};\\
+        \echo~\strlit{Whether 'tis nobler in the mind to suffer\nl}
+      \ea
+  \el
+\]
+%
+The computation $\quoteRitchie$ writes a quote by Dennis Ritchie to
+the file, whilst the computation $\quoteHamlet$ writes a few lines of
+William Shakespeare's \emph{The Tragedy of Hamlet, Prince of Denmark},
+Act III, Scene I~\cite{Shakespeare6416} to the file.
+%
+Using $\nondet$ and $\fork$ together with the previously defined
+infrastructure, we can fork the initial process such that both of the
+above computations are run concurrently.
+%
+\[
+  \ba{@{~}l@{~}l}
+    &\bl
+    \basicIO\,(\lambda\Unit.\\
+         \qquad\nondet\,(\lambda\Unit.\\
+           \qquad\qquad\sessionmgr\,\Record{\Root;\lambda\Unit.\\
+             \qquad\qquad\qquad\status\,(\lambda\Unit.
+                 \ba[t]{@{}l}
+                   \If\;\fork~\Unit\;\Then\;
+                       \su~\Alice;\,
+                       \quoteRitchie~\Unit\\
+                   \Else\;
+                       \su~\Bob;\,
+                       \quoteHamlet~\Unit)}))
+                 \ea
+     \el \smallskip\\
+     \reducesto^+&
+     \Record{
+       \ba[t]{@{}l}
+         [0, 0];
+         \texttt{"}\ba[t]{@{}l}
+           \texttt{UNIX is basically a simple operating system, but }\\
+           \texttt{you have to be a genius to understand the simplicity.\nl}\\
+           \texttt{To be, or not to be, that is the question:\nl}\\
+           \texttt{Whether 'tis nobler in the mind to suffer\nl"}} : \Record{\List~\Int; \UFile}
+         \ea
+       \ea
+  \ea
+\]
+%
+The computation running under the $\status$ handler immediately
+performs an invocation of fork, causing $\nondet$ to explore both the
+$\Then$-branch and the $\Else$-branch. In the former, $\Alice$ signs
+in and quotes Ritchie, whilst in the latter Bob signs in and quotes a
+Hamlet.
+%
+Looking at the output there is supposedly no interleaving of
+computation, since the individual writes have not been
+interleaved. From the stack of handlers, we \emph{know} that there has
+been no interleaving of computation, because no handler in the stack
+handles interleaving. Thus, our system only supports time sharing in
+the extreme sense: we know from the $\nondet$ handler that every
+effect of the parent process will be performed and handled before the
+child process gets to run. In order to be able to share time properly
+amongst processes, we must be able to interrupt them.
+
+\paragraph{Interleaving computation}
+%
+We need an operation for interruptions and corresponding handler to
+handle interrupts in order for the system to support interleaving of
+processes.
 %
 \[
   \bl
@@ -2516,20 +2618,42 @@ The following handler implements this behaviour.
   \el
 \]
 %
+The intended behaviour of an invocation of $\Interrupt$ is to suspend
+the invoking computation in order to yield time for another
+computation to run.
+%
+We can achieve this behaviour by reifying the process state. For the
+purpose of interleaving processes via interruptions it suffices to
+view a process as being in either of two states: 1) it is done, that
+is it has run to completion, or 2) it is paused, meaning it has
+yielded to provide room for another process to run.
+%
+We can model the state using a recursive variant type parameterised by
+some return value $\alpha$ and a set of effects $\varepsilon$ that the
+process may perform.
 %
 \[
   \Pstate~\alpha~\varepsilon \defas \forall \theta.
      \ba[t]{@{}l@{}l}
        [&\Done:\alpha;\\
-        &\Suspended:\UnitType \to \Pstate~\alpha~\varepsilon \eff \{\Interrupt:\theta';\varepsilon\} ]
+        &\Suspended:\UnitType \to \Pstate~\alpha~\varepsilon \eff \{\Interrupt:\theta;\varepsilon\} ]
      \ea
 \]
 %
+The $\Done$-tag simply carries the return value of type $\alpha$. The
+$\Suspended$-tag carries a suspended computation, which returns
+another instance of $\Pstate$, and may or may not perform any further
+invocations of $\Interrupt$. Note that, the presence variable $\theta$
+in the effect row is universally quantified in the type alias
+definition. The reason for this particular definition is that the type
+of a value carried by $\Suspended$ is precisely the type of a
+resumption originating from a handler that handles only the operation
+$\Interrupt$ such as the following handler.
 %
 \[
   \bl
-    \slice : (\UnitType \to \alpha \eff \{\Interrupt:\UnitType \opto \UnitType;\varepsilon\}) \to \Pstate~\alpha~\varepsilon\\
-    \slice~m \defas
+    \reifyP : (\UnitType \to \alpha \eff \{\Interrupt: \UnitType \opto \UnitType;\varepsilon\}) \to \Pstate~\alpha~\varepsilon\\
+    \reifyP~m \defas
          \ba[t]{@{}l}
            \Handle\;m\,\Unit\;\With\\
              ~\ba{@{~}l@{~}c@{~}l}
@@ -2540,6 +2664,36 @@ The following handler implements this behaviour.
   \el
 \]
 %
+This handler tags and returns values with $\Done$. It also tags and
+returns the resumption provided by the $\Interrupt$-case with
+$\Suspended$. If we compose this handler with the nondeterminism
+handler, then we obtain a term with the following type.
+%
+\[
+  \nondet\,(\lambda\Unit.\reifyP~m) : \List~(\Pstate~\alpha~\{\Fork: \UnitType \opto \Bool;\varepsilon\})
+\]
+%
+for some $m : \UnitType \to \{\Proc;\varepsilon\}$ where
+$\Proc \defas \{\Fork: \UnitType \opto \Bool;\Interrupt: \UnitType
+\opto \UnitType\}$.
+%
+The composition yields a list of process states, some of which may be
+in suspended state. In particular, the suspended computations may have
+unhandled instances of $\Fork$ as signified by it being present in the
+effect row. The reason for this is that in the above composition when
+$\reifyP$ produces a $\Suspended$-tagged resumption, it immediately
+returns through the $\Return$-case of $\nondet$, meaning that the
+resumption escapes the $\nondet$. Recall that a resumption is a
+delimited continuation that captures the extent from the operation
+invocation up to and including the nearest enclosing suitable
+handler. In this particular instance, it means that the $\nondet$
+handler is part of the extent.
+%
+We ultimately want to return just a list of $\alpha$s to ensure every
+process has run to completion. To achieve this, we define an auxiliary
+function which accepts as list of process states as input and
+recursively runs any suspended computations under the $\nondet$
+handler.
 %
 \[
   \bl
@@ -2556,13 +2710,40 @@ The following handler implements this behaviour.
   \el
 \]
 %
+The function $\runNext$ inspects each process in the input list $ps$
+to see whether it done or paused. It translates a $\Done$-tagged value
+into a singleton list, whereas if it is a $\Suspended$-tagged
+computation, then the computation is run under the $\nondet$ handler
+to in order to handle invocations of $\Fork$, and $\runNext$ is
+recursively applied to the result.
+%
+The function
+$\concatMap : (\alpha \to \List~\beta) \to \List~\alpha \to
+\List~\beta$ maps a function that produces a list of $\beta$s from an
+$\alpha$ over a list of $\alpha$s, thus producing a list of list of
+$\beta$s. The resulting list is flatten by using list concatenation to
+combine the list members.
+%
+Using the above machinery, we can define a function which adds
+time-sharing capabilities to the system.
 %
 \[
   \bl
-     \timeshare : (\UnitType \to \alpha \eff \{\Fork:\UnitType \opto \Bool;\Interrupt:\UnitType \opto \UnitType;\epsilon\}) \to (\List~\alpha) \eff \epsilon\\
-     \timeshare~m \defas \runNext\,[\Suspended\,(\lambda\Unit.\slice~m)]
+     \timeshare : (\UnitType \to \alpha \eff \Proc) \to \List~\alpha\\
+     \timeshare~m \defas \runNext\,[\Suspended\,(\lambda\Unit.\reifyP~m)]
   \el
 \]
+%
+The function $\timeshare$ handles the invocations of $\Fork$ and
+$\Interrupt$ in some computation $m$ by starting it in suspended state
+under the $\reifyP$ handler. The $\runNext$ actually starts the
+computation, when it runs the computation under the $\nondet$ handler.
+%
+
+It remains to inject invocations of $\Interrupt$ to cause computation
+to be interleaved.
+
+\paragraph{Interruption via interception}
 
 \subsection{State: file i/o}
 \label{sec:tiny-unix-io}