Shallow handlers intro

thesis.bib

@@ -1248,6 +1248,14 @@
   volume    = {33}
 }
 
+@book{Church41,
+  author = {Alonzo Church},
+  title = {The Calculi of Lambda Conversion. (AM-6) (Annals of Mathematics Studies)},
+  year = {1941},
+  publisher = {Princeton University Press},
+  address = {USA}
+}
+
 # Termination analysis.
 @article{Walther94,
   author    = {Christoph Walther},
@@ -2502,3 +2510,10 @@
   pages     = {106--142},
   year      = {1963}
 }
+
+# Scott encoding
+@unpublished{Scott62,
+  author    = {Dana Scott},
+  title     = {A system of functional abstraction},
+  note      = {Lectures delivered at University of California, Berkeley, California, USA, 1962/63}
+}

thesis.tex

@@ -4944,7 +4944,7 @@ The $\Absurd$ computation term is used to coerce the return type
 $\ZeroType$ of $\Fail$ into $\alpha$. This coercion is safe, because
 $\ZeroType$ is an uninhabited type.
 %
-An interpretation of $\Fail$ amounts to implementing an exception
+An interpretation of $\Exit$ amounts to implementing an exception
 handler.
 %
 \[
@@ -6644,11 +6644,34 @@ We can now plug it all together.
   \ea
 \]
 %
-Alice makes a hard copy of the file \texttt{ritchie.txt} as
-\texttt{ritchie}, and subsequently removes the original file, which
-effectively amounts to a roundabout way of renaming a file. Bob makes
-a soft copy of the file \texttt{hamlet} as \texttt{act3}, meaning
-both names share the same i-node with index $2$.
+Alice copies the file \texttt{ritchie.txt} as \texttt{ritchie}, and
+subsequently removes the original file, which effectively amounts to a
+roundabout way of renaming a file. It is evident from the file system
+state that the file is a hard copy as the contents of
+\texttt{ritchie.txt} now reside in location $3$ rather than location
+$1$ in the data region. Bob makes a soft copy of the file
+\texttt{hamlet} as \texttt{act3}, which is evident by looking at the
+directory where the two filenames point to the same i-node (with index
+$2$), whose link counter has value $2$.
+
+\paragraph{Summary} Throughout this section we have used effect
+handlers to give a semantics to a \UNIX{}-style operating system by
+treating system calls as effectful operations, whose semantics are
+given by handlers, acting as composable micro-kernels. Starting from a
+simple bare minimum file I/O model we seen how the modularity of
+effect handlers enable us to develop a feature-rich operating system
+in an incremental way by composing several handlers to implement a
+basic file system, multi-user environments, and multi-tasking
+support. Each incremental change to the system has been backwards
+compatible with previous changes in the sense that we have not
+modified any previously defined interfaces in order to support a new
+feature. It serves as a testament to demonstrate the versatility of
+effect handlers, and it suggests that handlers can be a viable option
+to use with legacy code bases to retrofit functionality. The operating
+system makes use of fourteen operations, which are being handled by
+twelve handlers, some of which are used multiple times, e.g. the
+$\environment$ and $\redirect$ handlers.
+
 
 % \begin{figure}[t]
 %   \centering
@@ -6944,9 +6967,86 @@ both names share the same i-node with index $2$.
 \section{Shallow handlers}
 \label{sec:unary-shallow-handlers}
 
+Shallow handlers are an alternative to deep handlers. Shallow handlers
+are defined as case-splits over computation trees, whereas deep
+handlers are defined as folds. Consequently, a shallow handler
+application unfolds only a single layer of the computation tree.
+%
+Semantically, the difference between deep and shallow handlers is
+similar to the difference between \citet{Church41} and \citet{Scott62}
+encoding techniques for data types in the sense that the recursion is
+intrinsic to the former, whilst recursion is extrinsic to the latter.
+%
+Often deep handlers are attractive because they are semantically
+well-behaved and provide appropriate structure for efficient
+implementations using optimisations such as fusion~\cite{WuS15}, and
+as we saw in the previous they codify a wide variety of applications.
+%
+However, they are not always convenient for implementing other
+structural recursion schemes such as mutual recursion.
+
 \subsection{Syntax and static semantics}
+\begin{syntax}
+\slab{Computations} &M,N \in \CompCat    &::=& \cdots \mid \ShallowHandle \; M \; \With \; H\\[1ex]
+\end{syntax}
+%
+%
+\begin{mathpar}
+  \inferrule*[Lab=\tylab{Handle}]
+  {
+    \typ{\Gamma}{M : C} \\
+    \typ{\Gamma}{H : C \Harrow D}
+  }
+  {\Gamma \vdash \ShallowHandle \; M \; \With\; H : D}
+
+
+%\mprset{flushleft}
+  \inferrule*[Lab=\tylab{Handler}]
+    {{\bl
+       C = A \eff \{(\ell_i : A_i \opto B_i)_i; R\} \\
+       D = B \eff \{(\ell_i : P_i)_i;           R\}\\
+       H = \{\Return\;x \mapsto M\} \uplus \{ \OpCase{\ell_i}{p_i}{r_i} \mapsto N_i \}_i
+       \el}\\\\
+       \typ{\Delta;\Gamma, x : A}{M : D}\\\\
+       [\typ{\Delta;\Gamma,p_i : A_i, r_i : B_i \to C}{N_i : D}]_i
+    }
+    {\typ{\Delta;\Gamma}{H : C \Harrow D}}
+\end{mathpar}
+%
+The \tylab{Handle} rule is simply the application rule for handlers.
+%
+The \tylab{Handler} rule is where most of the work happens. The effect
+rows on the input computation type $C$ and the output computation type
+$D$ must mention every operation in the domain of the handler. In the
+output row those operations may be either present ($\Pre{A}$), absent
+($\Abs$), or polymorphic in their presence ($\theta$), whilst in the
+input row they must be mentioned with a present type as those types
+are used to type operation clauses.
+%
+In each operation clause the resumption $r_i$ must have the same
+return type, $D$, as its handler. In the return clause the binder $x$
+has the same type, $C$, as the result of the input computation.
+
+
 \subsection{Dynamic semantics}
 
+We augment the operational semantics with two new reduction rules: one
+for handling return values and another for handling operations.
+%{\small{
+\begin{reductions}
+\semlab{Ret} &
+  \ShallowHandle \; (\Return \; V) \; \With \; H &\reducesto& N[V/x],  \hfill\text{where } \hret = \{ \Return \; x \mapsto N \} \\
+\semlab{Op} &
+  \ShallowHandle \; \EC[\Do \; \ell \, V] \; \With \; H
+    &\reducesto& N[V/p, \lambda y . \, \EC[\Return \; y]/r], \\
+\multicolumn{4}{@{}r@{}}{
+       \hfill\ba[t]{@{~}r@{~}l}
+                   \text{where}& \hell = \{ \OpCase{\ell}{p}{r} \mapsto N \}\\
+                   \text{and}  & \ell \notin \BL(\EC)
+              \ea
+}
+\end{reductions}%}}%
+
 \subsection{\UNIX{}-style pipes}
 \label{sec:pipes}
 
@@ -7011,14 +7111,6 @@ If the producer performs the $\Yield$ operation, then $\Pipe$ is
 invoked with the resumption of the producer along with a thunk that
 applies the consumer's resumption to the yielded value.
 
-\begin{example}[Inversion of control]
-  foo
-\end{example}
-
-\begin{example}[Communicating pipes]
-  bar
-\end{example}
-
 \section{Parameterised handlers}
 \label{sec:unary-parameterised-handlers}