Section 2.3

thesis.tex

@@ -2667,7 +2667,7 @@ as well as implementation strategies for first-class control.
 
 There are several analogies for understanding effect handlers as a
 programming abstraction, e.g. as interpreters for effects, folds over
-computation trees (as in Section~\ref{sec:sec:state-of-effprog}),
+computation trees (as in Section~\ref{sec:state-of-effprog}),
 resumable exceptions. A particularly compelling programmatic analogy
 is \emph{effect handlers as composable operating systems}. Effect
 handlers and operating systems share operational characteristics: an
@@ -2705,6 +2705,10 @@ handlers, that each handles a particular set of system commands. In
 this respect, we will truly realise \OSname{} in the spirit of the
 \UNIX{} philosophy~\cite[Section~1.6]{Raymond03}.
 
+The source calculus underpinning the language used to implement
+\OSname{} will be introduced informally on-the-fly. The formal syntax
+and semantics will be introduced in Chapter~\ref{ch:handler-calculi}
+
 \paragraph{Terminology}
 In the remainder of this dissertation, I will make a slight change of
 terminology to disambiguate programmatic continuations,
@@ -2720,29 +2724,37 @@ handlers} to model file i/o, user environments, process termination,
 process duplication, and process interruption.
 %
 \begin{description}
-\item[Section~\ref{sec:tiny-unix-bio}] This section implements a basic
+\item[Section~\ref{sec:tiny-unix-bio}] implements a basic
   mechanism which facilities writing to a global file. This mechanism
   is used as a stepping stone for building a more feature rich model.
 \item[Section~\ref{sec:tiny-unix-exit}] This section demonstrates a
   use of effect handlers as exception handlers, as we use \emph{exceptions}
   to implement process termination.
-\item[Section~\ref{sec:tiny-unix-env}] This section exemplifies
+\item[Section~\ref{sec:tiny-unix-env}] exemplifies
   user-specific environments as an instance of \emph{dynamic binding},
   as we use the environment, or reader, effect to implement user
   environments. The section also contains an instance of a
   \emph{tail-resumptive} handler as well as demonstrates an
   application of dynamic overloading of interpretation of residual
   effectful operations in resumptions.
-\item[Section~\ref{sec:tiny-unix-time}] This section models \UNIX{}'s
+\item[Section~\ref{sec:tiny-unix-time}] models \UNIX{}'s
   process duplicating primitive `fork' by making use of the
   \emph{nondeterminism} effect. Furthermore, in this section we also
   implement a simple time-sharing facility that is capable of
   interleaving user processes.
-\item[Section~\ref{sec:tiny-unix-io}] This section replaces the basic
+\item[Section~\ref{sec:tiny-unix-io}] replaces the basic
   i/o model of Section~\ref{sec:tiny-unix-bio} by a full-fledged i/o
   model supporting file creation, opening, reading, writing, and
   linking. This model is realised by making use of the \emph{state}
   effect.
+\item[Section~\ref{sec:pipes}] demonstrates an application of
+  \emph{shallow handlers} to implement parts of the \UNIX{}
+  programming environment by simulating composable \UNIX{}-style
+  \emph{pipes} for data stream processing.
+\item[Section~\ref{sec:tiny-unix-proc-sync}] implements a variation of
+  the time-sharing system from Section~\ref{sec:tiny-unix-time} with
+  process synchronisation by taking advantage of the ability to
+  internalise computation state with \emph{parameterised handlers}.
 \end{description}
 
 \paragraph{Relation to prior work}
@@ -2818,27 +2830,66 @@ Let us define a suitable handler for this operation.
   \el
 \]
 %
-The handler takes as input a computation that produces some value
+The type signature
-$\alpha$, and in doing so may perform the $\BIO$ effect.
+$(\UnitType \to \alpha \eff \BIO) \to \Record{\alpha;\UFile}$
+classifies a second-order function that takes as input a computation
+that produces some value $\alpha$, and in doing so may perform the
+$\BIO$ effect. As we program in a call-by-value setting the input
+computation is represented as a suspended computation, or thunk. Thus
+the type $\UnitType \to \alpha \eff \BIO$ classifies a thunk, that
+when forced may perform the $\BIO$ effect, i.e. the $\Write$
+operation, to produce a value of type $\alpha$.
 %
-The handler ultimately returns a pair consisting of the return value
+The second-order function ultimately returns a pair consisting of the
-$\alpha$ and the final state of the file.
+return value $\alpha$ and the final state of the file. The return type
+of the second-order function is `pure' in the sense that the function
+does not perform any effectful operations itself to produce its
+result.
 %
-The $\Return$-case pairs the result $res$ with the empty file $\nil$
+
-which models the scenario where the computation $m$ performed no
+In the implementation the input computation is bound by the name $m$,
+which is applied to a $\Unit$ (pronounced `unit'; as we will see in
+Chapter~\ref{ch:handler-calculi} it happens to be the empty record)
+under a $\Handle\;\cdots\;\With\cdots$ construct which is the term
+syntax for effect handler application. Occurrences of the $\Write$
+operation inside $m$ are handled with respect to the given handler, whose
+definition consists of two cases: a $\Return$-case and a
+$\Write$-case.
+%
+The $\Return$-case runs when $m\,\Unit$ reduces to a value. The
+resulting value gets bound to the name $res$. The body of the
+$\Return$-case pairs the result $res$ with the empty file $\nil$ which
+models the scenario where the computation $m$ performed no
 $\Write$-operations, e.g.
 $\basicIO\,(\lambda\Unit.\Unit) \reducesto^+
 \Record{\Unit;\strlit{}}$.
 %
-The $\Write$-case extends the file by first invoking the resumption,
+The $\Write$-case runs when $\Write$ is invoked inside of $m$. The
-whose return type is the same as the handler's return type, thus it
+payload of the operation along with its resumption gets bound on the
-returns a pair containing the result of $m$ and the file state. The
+left hand side of $\mapsto$. We use deep pattern matching to ignore
-file gets extended with the character sequence $cs$ before it is
+the first element of the payload and to bind the second element of the
-returned along with the original result of $m$.
+payload to $cs$. The resumption gets bound to the name $resume$. It is
+worth noting that at this point, the type of $resume$ is
+$\UnitType \to \Record{\alpha;\UFile}$, where the domain type matches
+the codomain type of the operation $\Write$ and the codomain type
+matches the expected type of the current context. This latter fact is
+due to the deep semantics of $\Handle$-construct, which means that an
+invocation of $resume$ implicitly installs another $\Handle$-construct
+with the same handler around the residual evaluation context embodied
+in $resume$.
+%
+The body of the $\Write$-case extends the file by first invoking the
+resumption, which returns a pair containing the result of $m$ and the
+file state. This pair is deconstructed using the $\Let$-pair
+deconstruction construct, which projects and binds the result
+component to $res$ and the file state component to $file$. The file
+gets extended with the character sequence $cs$ before it is returned
+along with the original result of $m$.
 %
 Intuitively, we may think of this implementation of $\Write$ as a
-peculiar instance of buffered writing, where the contents of the
+peculiar instance of buffered writing, where we temporarily store the
-operation are committed to the file when the computation $m$ finishes.
+contents of each $\Write$ operation on call stack and commit them to
+the file as we unwind the stack after the computation $m$ finishes.
 
 Let us define an auxiliary function that writes a string to the
 $\stdout$ file.
@@ -2850,8 +2901,9 @@ $\stdout$ file.
   \el
 \]
 %
-The function $\echo$ is a simple wrapper around an invocation of
+The $\Do$-construct is the invocation construct, or introduction form,
-$\Write$.
+for effectful operations. The function $\echo$ is a simple wrapper
+around an invocation of $\Write$.
 %
 We can now write some contents to the file and observe the effects.
 %
@@ -2862,7 +2914,7 @@ We can now write some contents to the file and observe the effects.
   \ea
 \]
 
-\section{Exceptions: non-local exits}
+\section{Exceptions: process termination}
 \label{sec:tiny-unix-exit}
 
 A process may terminate successfully by running to completion, or it
@@ -2923,6 +2975,12 @@ returns whatever payload the $\Exit$ operation was carrying. As a
 consequence, outside of $\status$, an invocation of $\Exit~0$ in $m$
 is indistinguishable from $m$ returning normally, e.g.
 $\status\,(\lambda\Unit.\exit~0) = \status\,(\lambda\Unit.\Unit)$.
+%
+Technically, the $\Exit$-case provides access to the resumption of
+$\Exit$ in $m$, however, we do not write this resumption here, because
+it is useless as its type is $\ZeroType \to \Int$. It expects as
+argument an element of the empty type, which is of course impossible
+to provide, hence we can never invoke it.
 
 To illustrate $\status$ and $\exit$ in action consider the following
 example, where the computation gets terminated mid-way.
@@ -3036,8 +3094,12 @@ The following handler implements the environment.
 The handler takes as input the current $user$ and a computation that
 may perform the $\Ask$ operation. When an invocation of $\Ask$ occurs
 the handler pattern matches on the $user$ parameter and resumes with a
-string representation of the user. With this implementation we can
+string representation of the user. This handler is an instance of a
-interpret an application of $\whoami$.
+so-called \emph{tail-resumptive} handler~\cite{Leijen17b,XieBHSL20} as
+each resumption invocation appears in tail position within in the
+operation clause.
+%
+With this implementation we can interpret an application of $\whoami$.
 %
 \[
   \environment~\Record{\Root;\whoami} \reducesto^+ \strlit{root} : \String
@@ -3047,8 +3109,8 @@ It is not difficult to extend this basic environment model to support
 an arbitrary number of variables. This can be done by parameterising
 the $\Ask$ operation by some name representation (e.g. a string),
 which the environment handler can use to index into a list of string
-values. In case the name is unbound the environment, the handler can
+values. In case the name is not bound in the environment, the handler
-embrace the laissez-faire attitude of \UNIX{} and resume with the
+can embrace the laissez-faire attitude of \UNIX{} and resume with the
 empty string.
 
 \paragraph{User session management}
@@ -5075,6 +5137,7 @@ words ``to'', ``be'', and the newline character ``$\nl$'' appear two
 times each, whilst the other words appear once each.
 
 \section{Process synchronisation}
+\label{sec:tiny-unix-proc-sync}
 %
 In Section~\ref{sec:tiny-unix-time} we implemented a time-sharing
 system on top of a simple process model. However, the model lacks a
@@ -5639,7 +5702,7 @@ domain of processes~\cite{Milner75,Plotkin76}.
 
 % \chapter{An ML-flavoured programming language based on rows}
 \chapter{ML-flavoured calculi for effect handler oriented programming}
-\label{ch:base-language}
+\label{ch:handler-calculi}
 
 \dhil{TODO merge this chapter with ``Effect handler calculi''}