Remove space

macros.tex

@@ -330,7 +330,10 @@
 
 % UNIX example
 \newcommand{\OSname}[0]{Tiny UNIX}
-\newcommand{\Uexit}{\dec{exit}}
+\newcommand{\exit}{\dec{exit}}
+\newcommand{\Exit}{\dec{Exit}}
+\newcommand{\Status}{\dec{Status}}
+\newcommand{\status}{\dec{status}}
 \newcommand{\basicIO}{\dec{basicIO}}
 \newcommand{\Putc}{\dec{Putc}}
 \newcommand{\putc}{\dec{putc}}
@@ -339,4 +342,15 @@
 \newcommand{\fwrite}{\dec{fwrite}}
 \newcommand{\iter}{\dec{iter}}
 \newcommand{\stdout}{\dec{stdout}}
-\newcommand{\IO}{\dec{IO}}
+\newcommand{\IO}{\dec{IO}}
+\newcommand{\Alice}{\dec{Alice}}
+\newcommand{\Bob}{\dec{Bob}}
+\newcommand{\Root}{\dec{Root}}
+\newcommand{\User}{\dec{User}}
+\newcommand{\environment}{\dec{env}}
+\newcommand{\EnvE}{\dec{Session}}
+\newcommand{\Ask}{\dec{Ask}}
+\newcommand{\whoami}{\dec{whoami}}
+\newcommand{\Su}{\dec{Su}}
+\newcommand{\su}{\dec{su}}
+\newcommand{\sessionmgr}{\dec{sessionmgr}}

thesis.bib

@@ -1025,3 +1025,19 @@
   publisher = {Pearson Education}
 }
 
+# GNU coreutils
+@book{MacKenzieMPPBYS20,
+  author = {David MacKenzie
+            and Jim Meyering
+            and Ross Paterson
+            and François Pinard
+            and Karl Berry
+            and Brian Youmans
+            and Richard Stallman},
+  title  = {{GNU} {Coreutils}},
+  note   = {For version 8.32},
+  month  = feb,
+  year   = 2020,
+  publisher = {Free Software Foundation},
+  address = {Boston, MA, USA}
+}

thesis.tex

@@ -2004,7 +2004,7 @@ operation invocations.
 This reading was suggested to me by James McKinna (personal
 communication). In this section I will take this reading literally,
 and demonstrate how we can use the power of (deep) effect handlers to
-implement a small operating system that supports multiple users,
+implement a tiny operating system that supports multiple users,
 time-sharing, and file i/o.
 %
 The operating system will be a variation of UNIX~\cite{RitchieT74},
@@ -2121,9 +2121,172 @@ We can now write some contents to the file and observe the effects.
 \subsection{Exceptions: non-local exits}
 \label{sec:tiny-unix-exit}
 
-\subsection{Dynamic binding: the environment}
+\[
+  \Status \defas \{\Exit : \Int \opto \Zero\}
+\]
+
+\[
+  \bl
+    \exit : \Int \to \alpha \eff \Status\\
+    \exit~n \defas \Absurd\;(\Do\;\Exit~n)
+  \el
+\]
+
+\[
+  \bl
+    \status : (\UnitType \to \alpha \eff \Status) \to \Int\\
+    \status~m \defas
+       \ba[t]{@{~}l}
+         \Handle\;m\,\Unit\;\With\\
+           ~\ba{@{~}l@{~}c@{~}l}
+              \Return\;\_ &\mapsto& 0\\
+              \Exit~n~\_ &\mapsto& n
+           \ea
+       \ea
+  \el
+\]
+
+\[
+  \ba{@{~}l@{~}l}
+    &\bl
+      \basicIO\,(\lambda\Unit.
+         \status\,(\lambda\Unit.
+            \fwrite\,\Record{\stdout;\texttt{"dead"}};\exit~1;\fwrite\,\Record{\stdout;\texttt{"code"}}))
+     \el\\
+    \reducesto^+& \Record{1;\texttt{"dead"}} : \Record{\Int;\UFile}
+  \ea
+\]
+
+\subsection{Dynamic binding: user-specific environments}
 \label{sec:tiny-unix-env}
 
+In UNIX an environment maps keys to string-values. A key-value pair is
+referred to as an \emph{environment variable}. Each user gets their
+own environment with their own set of environment variables. Some
+environment variable names are common to all environments, but their
+valuation may depend on the particular user session. For example, the
+environment variable \texttt{USER} is bound to the (string) name of
+the user; the result of querying the environment for the value of
+\texttt{USER} depends on which user session it is executed under.
+%
+\dhil{The value of an environment variable may also change during execution.}
+
+An environment variable is an instance of dynamic binding. The idea of
+dynamic binding as a programming notion dates back as far as the
+original implementation of Lisp~\cite{McCarthy60}.
+%
+We will use dynamic binding to implement user-specific environments.
+
+For simplicity we will fix the users to be root, Alice, and Bob.
+%
+\[
+  \User \defas [\Alice;\Bob;\Root]
+\]
+
+Our environment will only support a single environment variable
+intended to store the name of the current user. The value of this
+variable can be accessed via an operation $\Ask : \UnitType \opto \String$.
+%
+% \[
+%   \EnvE \defas \{\Ask : \UnitType \opto \String\}
+% \]
+%
+Using this operation we can readily implement the \emph{whoami}
+utility from the GNU coreutils~\cite[Section~20.3]{MacKenzieMPPBYS20},
+which returns the name of the current user.
+%
+\[
+  \bl
+    \whoami : \UnitType \to \String \eff \{\Ask : \UnitType \opto \String\}\\
+    \whoami~\Unit \defas \Do\;\Ask~\Unit
+  \el
+\]
+%
+The following handler implements the environment.
+%
+\[
+  \bl
+    \environment : \Record{\User;\UnitType \to \alpha \eff \{\Ask : \UnitType \opto \String\}} \to \alpha\\
+    \environment~\Record{user;m} \defas
+       \ba[t]{@{~}l}
+         \Handle\;m\,\Unit\;\With\\
+           ~\ba{@{~}l@{~}c@{~}l}
+              \Return\;res &\mapsto& res\\
+              \Ask~\Unit~resume &\mapsto&
+                \bl
+                  \Case\;user\,\{
+                  \ba[t]{@{}l@{~}c@{~}l}
+                    \Alice &\mapsto& resume~\texttt{"alice"}\\
+                    \Bob   &\mapsto& resume~\texttt{"bob"}\\
+                    \Root  &\mapsto& resume~\texttt{"root"}\}
+                   \ea
+                \el
+           \ea
+       \ea
+  \el
+\]
+%
+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
+interpret an application of $\whoami$.
+%
+\[
+  \environment~\Record{\Root;\whoami} \reducesto^+ \texttt{"root"} : \String
+\]
+%
+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 handler can
+embrace UNIX's laissez-faire attitude and resume with the empty
+string.
+
+\paragraph{Session management}
+%
+\[
+  \EnvE \defas \{\Ask : \UnitType \opto \String;\Su : \User \opto \UnitType\}
+\]
+
+\[
+  \bl
+    \su : \User \to \UnitType \eff \{\Su : \User \opto \UnitType\}\\
+    \su~user \defas \Do\;\Su~user
+  \el
+\]
+
+\[
+  \bl
+    \sessionmgr : \Record{\User; \UnitType \to \alpha \eff \EnvE} \to \alpha\\
+    \sessionmgr~\Record{user;m} \defas
+      \environment\,\langle{}user;(\lambda\Unit.
+         \ba[t]{@{}l}
+           \Handle\;m\,\Unit\;\With\\
+             ~\ba{@{~}l@{~}c@{~}l}
+                \Return\;res &\mapsto& res\\
+                \Su~user'~resume &\mapsto& \environment\,\Record{user';resume})\rangle
+              \ea
+         \ea
+  \el
+\]
+
+\[
+  \ba{@{~}l@{~}l}
+    &\bl
+      \basicIO\,(\lambda\Unit.\\
+         \qquad\sessionmgr\,\Record{\Root;\lambda\Unit.\\
+           \qquad\qquad\status\,(\lambda\Unit.
+            \ba[t]{@{}l@{~}l}
+              \su~\Alice;&\fwrite\,\Record{\stdout;\whoami\,\Unit};~\fwrite\,\Record{\stdout;\texttt{" "}};\\
+              \su~\Bob;&\fwrite\,\Record{\stdout;\whoami\,\Unit};~\fwrite\,\Record{\stdout;\texttt{" "}};\\
+              \su~\Root;&\fwrite\,\Record{\stdout;\whoami\,\Unit})})
+            \ea
+     \el \smallskip\\
+   \reducesto^+& \Record{0;\texttt{"alice bob root"}} : \Record{\Int;\UFile}
+ \ea
+\]
 \subsection{Nondeterminism: time sharing}
 \label{sec:tiny-unix-time}