Putc => Write. Don't mention file descriptors.

macros.tex

@@ -343,11 +343,12 @@
 \newcommand{\Putc}{\dec{Putc}}
 \newcommand{\putc}{\dec{putc}}
 \newcommand{\UFile}{\dec{File}}
-\newcommand{\UFD}{\dec{FileDescr}}
+\newcommand{\UFD}{\dec{INumber}}
 \newcommand{\fwrite}{\dec{fwrite}}
 \newcommand{\iter}{\dec{iter}}
 \newcommand{\stdout}{\dec{stdout}}
 \newcommand{\IO}{\dec{IO}}
+\newcommand{\BIO}{\dec{BIO}}
 \newcommand{\Alice}{\dec{Alice}}
 \newcommand{\Bob}{\dec{Bob}}
 \newcommand{\Root}{\dec{Root}}

thesis.bib

@@ -460,30 +460,6 @@
   year      = {2008}
 }
 
-# WebAssembly
-@misc{HaasRSTGWBH17,
-  author = {Andreas Haas and Andreas Rossberg and Ben L. Titzer and Dan Gohman and Luke Wagner and JF Bastien and Michael Holman},
-  title  = {Bringing the {Web} up to Speed with {WebAssembly}},
-  year   = 2017,
-  note   = {Draft},
-  howpublished = {\url{https://people.mpi-sws.org/~rossberg/papers/Haas, Rossberg, Schuff, Titzer, Gohman, Wagner, Bastien, Holman - Bringing the Web up to Speed with WebAssembly [Draft].pdf}}
-}
-
-# ECMAScript
-@misc{EMCA15,
-  author = {{Ecma International}},
-  title  = {{ECMAScript} 2015 Language Specification},
-  year = 2015,
-  url = {http://www.ecma-international.org/ecma-262/6.0/index.html}
-}
-
-@misc{EMCA17,
-  author = {{Emca International}},
-  title  = {{ECMAScript} 2017 Language Specification},
-  year = 2017,
-  url = {https://tc39.github.io/ecma262/}
-}
-
 # Hop.js
 @inproceedings{SerranoP16,
   author    = {Manuel Serrano and
@@ -646,7 +622,19 @@
   howpublished = {{ML Workshop}}
 }
 
-% fancy row typing systems that support shapes
+# Delimited Control
+@inproceedings{KiselyovSS06,
+  author    = {Oleg Kiselyov and
+               Chung{-}chieh Shan and
+               Amr Sabry},
+  title     = {Delimited dynamic binding},
+  booktitle = {{ICFP}},
+  pages     = {26--37},
+  publisher = {{ACM}},
+  year      = {2006}
+}
+
+# fancy row typing systems that support shapes
 @inproceedings{BerthomieuS95,
   author = {Bernard Berthomieu and Camille le Moniès de Sagazan},
   title = {A Calculus of Tagged Types, with applications to process languages},
@@ -663,7 +651,7 @@
 }
 
 
-
+# Zipper data structure.
 @article{Huet97,
   author    = {G{\'{e}}rard P. Huet},
   title     = {The Zipper},

thesis.tex

@@ -22,11 +22,11 @@
 \DeclareCaptionFormat{underlinedfigure}{#1#2#3\hrulefill}
 \captionsetup[figure]{format=underlinedfigure}
 \usepackage[T1]{fontenc}      % Fixes issues with accented characters
-\usepackage[scaled=0.85]{beramono}
 %\usepackage{libertine}
 %\usepackage{lmodern}
 %\usepackage{palatino}
 % \usepackage{newpxtext,newpxmath}
+\usepackage[scaled=0.85]{beramono}
 \usepackage[activate=true,
     final,
     tracking=true,
@@ -2051,67 +2051,68 @@ model for strings, $\String \defas \List~\Char$, such that we can use
 string literal notation to denote the $\strlit{contents of a file}$.
 %
 The signature of the basic file system will consist of a single
-operation $\Putc$ for writing a single character to the file.
+operation $\Write$ for writing a list of characters to the file.
 %
 \[
-  \IO \defas \{\Putc : \Record{\UFD;\Char} \opto \UnitType\}
+  \BIO \defas \{\Write : \Record{\UFD;\String} \opto \UnitType\}
 \]
 %
-The operation is parameterised by a file descriptor ($\UFD$) and a
-character. We will leave the file descriptor type abstract until
+The operation is parameterised by an $\UFD$ and a character
+sequence. We will leave the $\UFD$ type abstract until
 Section~\ref{sec:tiny-unix-io}, however, we will assume the existence
 of a term $\stdout : \UFD$ such that we perform invocations of
-$\Putc$.
+$\Write$.
 %
 Let us define a suitable handler for this operation.
 %
 \[
   \bl
-    \basicIO : (\UnitType \to \alpha \eff \IO) \to \Record{\alpha; \UFile}\\
+    \basicIO : (\UnitType \to \alpha \eff \BIO) \to \Record{\alpha; \UFile}\\
     \basicIO~m \defas
        \ba[t]{@{~}l}
          \Handle\;m\,\Unit\;\With\\
            ~\ba{@{~}l@{~}c@{~}l}
               \Return\;res &\mapsto& \Record{res;\nil}\\
-              \OpCase{\Putc}{\Record{\_;c}}{resume} &\mapsto&
-                  \Let\; \Record{res;file} = resume\,\Unit\;\In\;
-                  \Record{res; c \cons file}
+              \OpCase{\Write}{\Record{\_;cs}}{resume} &\mapsto&
+                 \ba[t]{@{}l}
+                   \Let\; \Record{res;file} = resume\,\Unit\;\In\\
+                   \Record{res; cs \concat file}
+                 \ea
            \ea
        \ea
   \el
 \]
 %
 The handler takes as input a computation that produces some value
-$\alpha$, and in doing so may perform the $\IO$ effect.
+$\alpha$, and in doing so may perform the $\BIO$ effect.
 %
 The handler ultimately returns a pair consisting of the return value
 $\alpha$ and the final state of the file.
 %
 The $\Return$-case pairs the result $res$ with the empty file $\nil$
 which models the scenario where the computation $m$ performed no
-$\Putc$-operations, e.g.
+$\Write$-operations, e.g.
 $\basicIO\,(\lambda\Unit.\Unit) \reducesto^+
 \Record{\Unit;\strlit{}}$.
 %
-The $\Putc$-case extends the file by first invoking the resumption,
+The $\Write$-case extends the file by first invoking the resumption,
 whose return type is the same as the handler's return type, thus it
 returns a pair containing the result of $m$ and the file state. The
-file gets extended with the character $c$ before it is returned along
-with the original result of $m$. The file is effectively built bottom
-up starting with the last character.
+file gets extended with the character sequence $cs$ before it is
+returned along with the original result of $m$.%  The file is
+% effectively built bottom up starting with the last character.
 
-Let us define an auxiliary function that writes a string to a given
-file.
+Let us define an auxiliary function that writes a string to the $\stdout$ file.
 %
 \[
   \bl
-    \echo : \String \to \UnitType \eff \{\Putc : \Record{\UFD;\Char} \opto \UnitType\}\\
-    \echo~cs \defas \iter\,(\lambda c.\Do\;\Putc\,\Record{\stdout;c})\,cs
+    \echo : \String \to \UnitType \eff\, \BIO\\%\{\Write : \Record{\UFD;\String} \opto \UnitType\}\\
+    \echo~cs \defas \Do\;\Write\,\Record{\stdout;cs}
   \el
 \]
 %
-The function $\echo$ invokes the operation $\Putc$ point-wise on the
-list of characters $cs$ by using the list iteration function $\iter$.
+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.
 %
@@ -2125,17 +2126,44 @@ We can now write some contents to the file and observe the effects.
 \subsection{Exceptions: non-local exits}
 \label{sec:tiny-unix-exit}
 
+A process may terminate successfully by running to completion, or it
+may terminate with success or failure in the middle of some
+computation by performing an \emph{exit} system call. The exit system
+call is typically parameterised by an integer value intended to
+indicate whether the exit was due to success or failure. By
+convention, \UNIX{} interprets the integer zero as success and any
+nonzero integer as failure, where the specific value is supposed to
+correspond to some known error code.
+%
+
+We can model the exit system call by way of a single operation
+$\Exit$.
+%
 \[
   \Status \defas \{\Exit : \Int \opto \Zero\}
 \]
-
+%
+The operation is parameterised by an integer value, however, an
+invocation of $\Exit$ can never return, because the type $\Zero$ is
+uninhabited. Thus $\Exit$ acts like an exception.
+%
+It is convenient to abstract invocations of $\Exit$ to make it
+possible to invoke the operation in any context.
+%
 \[
   \bl
     \exit : \Int \to \alpha \eff \Status\\
     \exit~n \defas \Absurd\;(\Do\;\Exit~n)
   \el
 \]
-
+%
+The $\Absurd$ computation term is used to coerce the return type
+$\Zero$ of $\Fail$ into $\alpha$. This coercion is safe, because
+$\Zero$ is an uninhabited type.
+%
+An interpretation of $\Fail$ amounts to implementing an exception
+handler.
+%
 \[
   \bl
     \status : (\UnitType \to \alpha \eff \Status) \to \Int\\
@@ -2149,7 +2177,17 @@ We can now write some contents to the file and observe the effects.
        \ea
   \el
 \]
+%
+Following the \UNIX{} convention, the $\Return$-case interprets a
+successful completion of $m$ as the integer $0$. The operation case
+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)$.
 
+To illustrate $\status$ and $\exit$ in action consider the following
+example, where the computation gets terminated mid-way.
+%
 \[
   \ba{@{~}l@{~}l}
     &\bl
@@ -2160,28 +2198,42 @@ We can now write some contents to the file and observe the effects.
     \reducesto^+& \Record{1;\strlit{dead}} : \Record{\Int;\UFile}
   \ea
 \]
+%
+The (delimited) continuation of $\exit~1$ is effectively dead code.
 
 \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.
+When a process is run in \UNIX{}, the operating system makes available
+to the process a collection of name-value pairs called the
+\emph{environment}.
 %
-\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}.
+The name of a name-value pair is known as an \emph{environment
+  variable}.
 %
-We will use dynamic binding to implement user-specific environments.
+During execution the process may perform a system call to ask the
+operating system for the value of some environment variable.
+%
+The value of environment variables may change throughout process
+execution, moreover, the value of some environment variables may vary
+according to which user asks the environment.
+%
+For example, an environment may contain the environment variable
+\texttt{USER} that is bound to the name of the inquiring user.
 
-For simplicity we will fix the users to be root, Alice, and Bob.
+An environment variable can be viewed as an instance of dynamic
+binding. The idea of dynamic binding as a binding form in programming
+dates back as far as the original implementation of
+Lisp~\cite{McCarthy60}, and still finds uses in successors such as
+Emacs Lisp~\cite{LewisLSG20}. It is well-known that dynamic binding
+can be encoded as a computational effect by using delimited
+control~\cite{KiselyovSS06}.
+%
+Unsurprisingly, we will use this insight to simulate user-specific
+environments using effect handlers.
+
+For simplicity we fix the users of the operating system to be root,
+Alice, and Bob.
 %
 \[
   \User \defas [\Alice;\Bob;\Root]
@@ -2315,6 +2367,8 @@ string.
   \el
 \]
 
+\dhil{This is an instance of non-blind backtracking}
+
 \[
   \bl
     \interrupt : \UnitType \to \UnitType \eff \{\Interrupt : \UnitType \opto \UnitType\}\\
@@ -2377,15 +2431,15 @@ string.
     \hline
     \strlit{hamlet}\tikzmark{hamlet}\\
     \hline
-    \strlit{ritchie.txt}\\
+    \strlit{ritchie.txt}\tikzmark{ritchie}\\
     \hline
     \multicolumn{1}{| c |}{$\cdots$}\\
     \hline
-    \strlit{act3}\\
+    \strlit{stdout}\tikzmark{stdout}\\
     \hline
     \multicolumn{1}{| c |}{$\cdots$}\\
     \hline
-    \strlit{stdout}\\
+    \strlit{act3}\tikzmark{act3}\\
     \hline
   \end{tabular}
   \hspace{1.5cm}
@@ -2393,13 +2447,13 @@ string.
     \hline
     \multicolumn{1}{| c |}{\textbf{I-List}} \\
     \hline
-    2\\
+    1\tikzmark{ritchieino}\\
     \hline
-    1\tikzmark{hamletino}\\
+    2\tikzmark{hamletino}\\
     \hline
     \multicolumn{1}{| c |}{$\cdots$}\\
     \hline
-    1\\
+    1\tikzmark{stdoutino}\\
     \hline
   \end{tabular}
   \hspace{1.5cm}
@@ -2407,18 +2461,27 @@ string.
     \hline
     \multicolumn{1}{| c |}{\textbf{Data region}} \\
     \hline
-    \strlit{UNIX is basically...}\\
+    \tikzmark{stdoutdr}\strlit{}\\
     \hline
     \tikzmark{hamletdr}\strlit{To be, or not to be...}\\
     \hline
     \multicolumn{1}{| c |}{$\cdots$}\\
     \hline
-    \strlit{}\\
+    \tikzmark{ritchiedr}\strlit{UNIX is basically...}\\
     \hline
   \end{tabular}
-  \tikz[remember picture,overlay]\draw[->,thick] ([xshift=1.3cm,yshift=0.1cm]pic cs:hamlet) -- ([xshift=-0.85cm,yshift=0.1cm]pic cs:hamletino) node[] {};
-  \tikz[remember picture,overlay]\draw[->,thick] ([xshift=0.62cm,yshift=0.1cm]pic cs:hamletino) -- ([xshift=-0.23cm,yshift=0.1cm]pic cs:hamletdr) node[] {};
-  \caption{\UNIX{} directory, i-list, and data region mappings}\label{fig:unix-mappings}
+  %% Hamlet arrows.
+  \tikz[remember picture,overlay]\draw[->,thick,out=30,in=160] ([xshift=1.3cm,yshift=0.1cm]pic cs:hamlet) to ([xshift=-0.85cm,yshift=0.1cm]pic cs:hamletino) node[] {};
+  \tikz[remember picture,overlay]\draw[->,thick,out=30,in=180] ([xshift=0.62cm,yshift=0.1cm]pic cs:hamletino) to ([xshift=-0.23cm,yshift=0.1cm]pic cs:hamletdr) node[] {};
+  %% Ritchie arrows.
+  \tikz[remember picture,overlay]\draw[->,thick,out=-30,in=180] ([xshift=0.22cm,yshift=0.1cm]pic cs:ritchie) to ([xshift=-0.85cm,yshift=0.1cm]pic cs:ritchieino) node[] {};
+  \tikz[remember picture,overlay]\draw[->,thick,out=30,in=180] ([xshift=0.62cm,yshift=0.1cm]pic cs:ritchieino) to ([xshift=-0.23cm,yshift=0.1cm]pic cs:ritchiedr) node[] {};
+  %% Act3 arrow.
+  \tikz[remember picture,overlay]\draw[->,thick,out=10,in=210] ([xshift=1.73cm,yshift=0.1cm]pic cs:act3) to ([xshift=-0.85cm,yshift=-0.5mm]pic cs:hamletino) node[] {};
+  %% Stdout arrows.
+  \tikz[remember picture,overlay]\draw[->,thick,out=30,in=180] ([xshift=1.3cm,yshift=0.1cm]pic cs:stdout) to ([xshift=-0.85cm,yshift=0.1cm]pic cs:stdoutino) node[] {};
+  \tikz[remember picture,overlay]\draw[->,thick,out=30,in=180] ([xshift=0.62cm,yshift=0.1cm]pic cs:stdoutino) to ([xshift=-0.23cm,yshift=0.1cm]pic cs:stdoutdr) node[] {};
+  \caption{\UNIX{} directory, i-list, and data region mappings.}\label{fig:unix-mappings}
 \end{figure}
 
 
@@ -2465,9 +2528,9 @@ string.
     %
     \draw (client) -- (client_ground);
     \draw (server) -- (server_ground);
-    \draw[->] ($(client)!0.25!(client_ground)$) -- node[rotate=-6,above,scale=0.7,midway]{SYN 42} ($(server)!0.40!(server_ground)$);
-    \draw[<-] ($(client)!0.56!(client_ground)$) -- node[rotate=6,above,scale=0.7,midway]{SYN 84;ACK 43} ($(server)!0.41!(server_ground)$);
-    \draw[->] ($(client)!0.57!(client_ground)$) -- node[rotate=-6,above,scale=0.7,midway]{ACK 44} ($(server)!0.72!(server_ground)$);
+    \draw[->,thick] ($(client)!0.25!(client_ground)$) -- node[rotate=-6,above,scale=0.7,midway]{SYN 42} ($(server)!0.40!(server_ground)$);
+    \draw[<-,thick] ($(client)!0.56!(client_ground)$) -- node[rotate=6,above,scale=0.7,midway]{SYN 84;ACK 43} ($(server)!0.41!(server_ground)$);
+    \draw[->,thick] ($(client)!0.57!(client_ground)$) -- node[rotate=-6,above,scale=0.7,midway]{ACK 85} ($(server)!0.72!(server_ground)$);
   \end{tikzpicture}
   \caption{Sequence diagram for the TCP handshake example.}\label{fig:tcp-handshake}
 \end{figure}