citet => cite

thesis.bib

@@ -319,6 +319,13 @@
   year      = {2020}
 }
 
+@phdthesis{Geron19,
+  author = {Bram Geron},
+  title  = {Defined Algebraic Operations},
+  school = {University of Birmingham, England, {UK}},
+  year   = 2019
+}
+
 # Asynchronous effects
 @article{AhmanP21,
   author    = {Danel Ahman and
@@ -509,6 +516,59 @@
   year      = {2017}
 }
 
+@inproceedings{Leijen05,
+  author    = {Daan Leijen},
+  title     = {Extensible records with scoped labels},
+  booktitle = {Trends in Functional Programming},
+  series    = {Trends in Functional Programming},
+  volume    = {6},
+  pages     = {179--194},
+  publisher = {Intellect},
+  year      = {2005}
+}
+
+# Helium
+@article{BiernackiPPS18,
+  author    = {Dariusz Biernacki and
+               Maciej Pir{\'{o}}g and
+               Piotr Polesiuk and
+               Filip Sieczkowski},
+  title     = {Handle with care: relational interpretation of algebraic effects and
+               handlers},
+  journal   = {Proc. {ACM} Program. Lang.},
+  volume    = {2},
+  number    = {{POPL}},
+  pages     = {8:1--8:30},
+  year      = {2018}
+}
+
+@article{BiernackiPPS19,
+  author    = {Dariusz Biernacki and
+               Maciej Pir{\'{o}}g and
+               Piotr Polesiuk and
+               Filip Sieczkowski},
+  title     = {Abstracting algebraic effects},
+  journal   = {Proc. {ACM} Program. Lang.},
+  volume    = {3},
+  number    = {{POPL}},
+  pages     = {6:1--6:28},
+  year      = {2019}
+}
+
+@article{BiernackiPPS20,
+  author    = {Dariusz Biernacki and
+               Maciej Pir{\'{o}}g and
+               Piotr Polesiuk and
+               Filip Sieczkowski},
+  title     = {Binders by day, labels by night: effect instances via lexically scoped
+               handlers},
+  journal   = {Proc. {ACM} Program. Lang.},
+  volume    = {4},
+  number    = {{POPL}},
+  pages     = {48:1--48:29},
+  year      = {2020}
+}
+
 # Haskell implementations
 @inproceedings{KiselyovSS13,
   author    = {Oleg Kiselyov and
@@ -1014,20 +1074,6 @@
   year      = {1986}
 }
 
-@article{BiernackiPPS18,
-  author    = {Dariusz Biernacki and
-               Maciej Pir{\'{o}}g and
-               Piotr Polesiuk and
-               Filip Sieczkowski},
-  title     = {Handle with care: relational interpretation of algebraic effects and
-               handlers},
-  journal   = {{PACMPL}},
-  volume    = {2},
-  number    = {{POPL}},
-  pages     = {8:1--8:30},
-  year      = {2018}
-}
-
 # Capability passing style
 @phdthesis{Brachthauser20,
   author    = {Jonathan Immanuel Brachth{\"{a}}user},
@@ -1073,18 +1119,6 @@
   year      = {2020}
 }
 
-@article{BrachthauserSO18,
-  author    = {Jonathan Immanuel Brachth{\"{a}}user and
-               Philipp Schuster and
-               Klaus Ostermann},
-  title     = {Effect handlers for the masses},
-  journal   = {Proc. {ACM} Program. Lang.},
-  volume    = {2},
-  number    = {{OOPSLA}},
-  pages     = {111:1--111:27},
-  year      = {2018}
-}
-
 # explicit effect subtyping
 @inproceedings{SalehKPS18,
   author    = {Amr Hany Saleh and

thesis.tex

@@ -166,15 +166,25 @@
   programming with first-class control by separating control reifying
   operations from their handling.
 
-  In this thesis I develop operational foundations for programming and
+  This thesis is composed of three strands in which I develop
-  implementing effect handlers.
+  operational foundations for programming and implementing effect
+  handlers as well as investigating the expressive power of effect
+  handlers.
 
-  The first strand develops the core calculus of a programming
+  The first strand develops the core calculus of a statically typed
-  language with a \emph{structural} notion of effects, as opposed to
+  programming language a \emph{structural} notion of effects, as
-  the dominant \emph{nominal} notion of effects.
+  opposed to the dominant \emph{nominal} notion of effects.
-
+  %
-  By making crucial use of \emph{row polymorphism} to build and track
+  With the structural approach, effects need not be declared before
-  effect signatures.
+  use. The usual safety properties of statically typed programming are
+  retained by making crucial use of \emph{row polymorphism} to build
+  and track effect signatures.
+  %
+  The calculus features three forms of handlers: deep, shallow, and
+  parameterised. They each offer a different approach to manipulate
+  the control state of programs.
+  %
+  To demonstrate the usefulness of effect\dots
 
   The second strand studies \emph{continuation passing style} and
   \emph{abstract machine semantics}, which are foundational techniques
@@ -4717,7 +4727,7 @@ computation normal forms as there are now two ways in which a
 computation term can terminate: successfully returning a value or
 getting stuck on an unhandled operation.
 %
-\begin{definition}[Computation normal forms]
+\begin{definition}[Computation normal forms]\ref{def:comp-normal-form}
   We say that a computation term $N$ is normal with respect to an
   effect signature $E$, if $N$ is either of the form $\Return\;V$, or
   $\EC[\Do\;\ell\,W]$ where $\ell \in E$ and $\ell \notin \BL(\EC)$.
@@ -4728,12 +4738,19 @@ getting stuck on an unhandled operation.
   Suppose $\typ{}{M : C}$, then either there exists $\typ{}{N : C}$
   such that $M \reducesto^+ N$ and $N$ is normal, or $M$ diverges.
 \end{theorem}
-
 %
-\begin{theorem}[Preservation]
+\begin{proof}
+  By induction on typing derivations.
+\end{proof}
+%
+\begin{theorem}[Subject reduction]
   Suppose $\typ{\Gamma}{M : C}$ and $M \reducesto M'$, then
   $\typ{\Gamma}{M' : C}$.
 \end{theorem}
+%
+\begin{proof}
+  By induction on typing derivations.
+\end{proof}
 
 \section{Composing \UNIX{} with effect handlers}
 \label{sec:deep-handlers-in-action}
@@ -5466,7 +5483,7 @@ handled recursively.
 %
 \[
   \bl
-    \schedule : \List~(\Pstate~\alpha~\{\Fork:\Bool;\varepsilon\}) \to \List~\alpha \eff \varepsilon\\
+    \schedule : \List~(\Pstate~\alpha~\{\Fork:\Bool;\varepsilon\}~\theta) \to \List~\alpha \eff \varepsilon\\
     \schedule~ps \defas
        \ba[t]{@{}l}
          \Let\;run \revto
@@ -7083,6 +7100,27 @@ handler as in the setting of deep handlers, meaning is up to the
 programmer to supply the handler the next invocation of $\ell$ inside
 $\EC$. This handler may be different from $H$.
 
+The basic metatheoretic properties of $\SCalc$ are a carbon copy of
+the basic properties of $\HCalc$.
+%
+\begin{theorem}[Progress]
+  Suppose $\typ{}{M : C}$, then either there exists $\typ{}{N : C}$
+  such that $M \reducesto^+ N$ and $N$ is normal, or $M$ diverges.
+\end{theorem}
+%
+\begin{proof}
+  By induction on typing derivations.
+\end{proof}
+%
+\begin{theorem}[Subject reduction]
+  Suppose $\typ{\Gamma}{M : C}$ and $M \reducesto M'$, then
+  $\typ{\Gamma}{M' : C}$.
+\end{theorem}
+%
+\begin{proof}
+  By induction on typing derivations.
+\end{proof}
+
 \subsection{\UNIX{}-style pipes}
 \label{sec:pipes}
 
@@ -7621,6 +7659,25 @@ rather than the original value $W$. This achieves the effect of state
 passing as the value of $q'$ becomes available upon the next
 activation of the handler.
 
+The metatheoretic properties of $\HCalc$ carries over to $\HPCalc$.
+\begin{theorem}[Progress]
+  Suppose $\typ{}{M : C}$, then either there exists $\typ{}{N : C}$
+  such that $M \reducesto^+ N$ and $N$ is normal, or $M$ diverges.
+\end{theorem}
+%
+\begin{proof}
+  By induction on typing derivations.
+\end{proof}
+%
+\begin{theorem}[Subject reduction]
+  Suppose $\typ{\Gamma}{M : C}$ and $M \reducesto M'$, then
+  $\typ{\Gamma}{M' : C}$.
+\end{theorem}
+%
+\begin{proof}
+  By induction on typing derivations.
+\end{proof}
+
 \subsection{Process synchronisation}
 %
 In Section~\ref{sec:tiny-unix-time} we implemented a time-sharing
@@ -7937,10 +7994,116 @@ status list that Alice's process is the first to complete, and the
 second to complete is Bob's process, whilst the last process to
 complete is the $\init$ process.
 
+\paragraph{Retrofitting fork} In the previous program we replaced the
+original implementation of $\timeshare$
+(Section~\ref{sec:tiny-unix-time}), which handles invocations of
+$\Fork : \UnitType \opto \Bool$, by $\timesharee$, which handles the
+more general operation $\UFork : \UnitType \opto \Int$. In practice,
+we may be unable to dispense of the old interface so easily, meaning
+we have to retain support for, say, legacy reasons. As we have seen
+previously we can an operation in terms of another operation. Thus to
+retain support for $\Fork$ we simply have to insert a handler under
+$\timesharee$ which interprets $\Fork$ in terms of $\UFork$. The
+operation case of this handler would be akin to the following.
+%
+\[
+  \OpCase{\Fork}{\Unit}{resume} \mapsto
+    \bl
+      \Let\;pid \revto \Do\;\UFork~\Unit\;\In\\
+      resume\,(pid \neq 0)
+    \el
+\]
+%
+The interpretation of $\Fork$ inspects the process identifier returned
+by the $\UFork$ to determine the role of the current process in the
+parent-child relationship. If the identifier is nonzero, then the
+process is a parent, hence $\Fork$ should return $\True$ to its
+caller. Otherwise it should return $\False$. This preserves the
+functionality of the legacy code.
+
 \section{Related work}
 \label{sec:unix-related-work}
 
-\paragraph{Programming languages with handlers}
+\paragraph{Programming languages with handlers} The work presented in
+this chapter has been retrofitted on to the programming language
+Links~\cite{HillerstromL16,HillerstromL18}. A closely related
+programming language with handlers is \citeauthor{Leijen17}'s Koka,
+which has been retrofitted with ordinary deep and parameterised effect
+handlers~\cite{Leijen17}. In Koka effects are nominal, meaning an
+effect and its constructors must be declared before use, which is
+unlike the structural approach taken in this chapter. Koka also tracks
+effects via an effect system based on \citeauthor{Leijen05}-style row
+polymorphism~\cite{Leijen05,Leijen14}, where rows are interpreted as
+multisets which means an effect can occur multiple times in an effect
+row. The ability to repeat effects provide a form for effect scoping
+in the sense that an effect instance can shadow another. A handler
+handles only the first instance of a repeated effect, leaving the
+remaining instances for another handler. Consequently, the order of
+repeated effect instances matter and it can therefore be situational
+useful to manipulate the order of repeated instances by way of
+so-called \emph{effect masking}.
+%
+The notion of effect masking was formalised by \citet{BiernackiPPS18}
+and generalised by \citet{ConventLMM20}.
+%
+
+\citet{BiernackiPPS18} designed Helium, which is a programming
+language that features a rich module system, deep handlers, and
+\emph{lexical} handlers~\cite{BiernackiPPS20}. Lexical handlers
+\emph{bind} effectful operations to specific handler
+instances. Operations remain bound for the duration of
+computation. This makes the nature of lexical handlers more static
+than ordinary deep handlers, as for example it is not possible to
+dynamically overload the interpretation of residual effects of a
+resumption invocation as in Section~\ref{sec:tiny-unix-env}.
+%
+The mathematical foundations for lexical handlers has been developed
+by \citet{Geron19}.
+
+The design of the Effekt language by \citet{BrachthauserSO20b}
+resolves around the idea of lexical handlers for efficiency. Effekt
+takes advantage of the static nature of lexical handlers to eliminate
+the dynamic handler lookup at runtime by tying the correct handler
+instance directly to an operation
+invocation~\cite{BrachthauserS17,SchusterBO20}. The effect system of
+Effekt is based on intersection types, which provides a limited form
+of effect polymorphism~\cite{BrachthauserSO20b}. A design choice that
+means it does not feature first-class functions.
+
+The Frank language by \citet{LindleyMM17} is born and bred on shallow
+effect handlers. One of the key novelties of Frank is $n$-ary shallow
+handlers, which generalise ordinary unary shallow handlers to be able
+to handle multiple computations simultaneously. Another novelty is the
+effect system, which is based on a variation of
+\citeauthor{Leijen05}-style row polymorphism, where the programmer
+rarely needs to mention effect variables. This is achieved by
+insisting that the programmer annotates each input argument with the
+particular effects handled at the particular argument position as well
+as declaring what effects needs to be handled by the ambient
+context. Each annotation is essentially an incomplete row. They are
+made complete by concatenating them and inserting a fresh effect
+variable.
+
+\citeauthor{BauerP15}'s Eff language was the first programming
+language designed from the ground up with effect handlers in mind. It
+features only deep handlers~\cite{BauerP15}. A previous iteration of
+the language featured an explicit \emph{effect instance} system. An
+effect instance is a sort of generative interface, where the
+operations are unique to each instance. As a result it is possible to
+handle two distinct instances of the same effect differently in a
+single computation. Their system featured a type-and-effect system
+with support for effect inference~\cite{Pretnar13,BauerP13}, however,
+the effect instance system was later dropped to in favour of a vanilla
+nominal approach to effects and handlers.
+
+Multicore OCaml is, at the time of writing, an experimental branch of
+the OCaml programming language, which aims to extend OCaml with effect
+handlers for multicore and concurrent
+programming~\cite{DolanWM14,DolanWSYM15}. The current incarnation
+features untracked nominal effects and deep handlers with single-use
+resumptions.
+
+\dhil{Possibly move to the introduction or background}
 
 \paragraph{Effect-driven concurrency}
 In their tutorial of the Eff programming language \citet{BauerP15}
@@ -7957,7 +8120,7 @@ fork operation invocation site and the scheduler handler needs to be
 manually reinstalled when the computation argument is
 run. Nevertheless, this is the approach to concurrency that
 \citet{DolanWSYM15} have adopted for Multicore
-OCaml~\citet{DolanWSYM15}.
+OCaml~\cite{DolanWSYM15}.
 %
 In my MSc(R) dissertation I used a similar approach to implement a
 cooperative version of the actor concurrency model of Links with