Exceptions example and figures.

macros.tex

@@ -348,6 +348,7 @@
 \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.tex

@@ -2051,10 +2051,10 @@ 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
@@ -2067,51 +2067,52 @@ 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,6 +2198,8 @@ 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}
@@ -2315,6 +2355,8 @@ string.
   \el
 \]
 
+\dhil{This is an instance of non-blind backtracking}
+
 \[
   \bl
     \interrupt : \UnitType \to \UnitType \eff \{\Interrupt : \UnitType \opto \UnitType\}\\
@@ -2377,15 +2419,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 +2435,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 +2449,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 +2516,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}