Conclusions notes [WIP]

thesis.tex

@@ -2948,6 +2948,7 @@ readily be implemented with a trampoline~\cite{GanzFW99}. Alas, at the
 cost of the indirection induced by the trampoline.
 
 \part{Design}
+\label{p:design}
 
 \chapter{An ML-flavoured programming language based on rows}
 \label{ch:base-language}
@@ -8289,6 +8290,7 @@ domain of processes~\cite{Milner75,Plotkin76}.
 \dhil{Briefly mention \citet{AtkeyJ15}}
 
 \part{Implementation}
+\label{p:implementation}
 
 \chapter{Continuation-passing style}
 \label{ch:cps}
@@ -11425,8 +11427,9 @@ implementation based on stack manipulations.
 \begin{equations}
 \inv{\{\Return\;x \mapsto M\}}\env
   &\defas& \{\Return\;x \mapsto \inv{M}(\env \res \{x\})\} \\
-\inv{\{\ell\;x\;k \mapsto M\} \uplus H^\depth}\env
+\inv{\{\OpCase{\ell}{p}{r} \mapsto M\} \uplus H^\depth}\env
   &\defas& \{\OpCase{\ell}{p}{r} \mapsto \inv{M}(\env \res \{p, r\}\} \uplus \inv{H^\depth}\env \\
+\inv{(q.\,H)}\env &\defas& \inv{H}(\env \res \{q\})
 \end{equations}
 
 \textbf{Value terms and values}
@@ -11460,58 +11463,98 @@ implementation based on stack manipulations.
 \label{fig:config-to-term}
 \end{figure}
 %
-Figure~\ref{fig:config-to-term} defines an inverse mapping $\inv{-}$
+We now show that the base abstract machine is correct with respect to
-from configurations to computation terms via a collection of mutually
+the combined context-based small-step semantics of $\HCalc$, $\SCalc$,
-recursive functions defined on configurations, continuations,
+and $\HPCalc$ via a simulation result.
-computation terms, handler definitions, value terms, and values.
+
+Initial states provide a canonical way to map a computation term onto
+the abstract machine.
 %
-We write $\dom(\gamma)$ for the domain of $\gamma$ and $\gamma \res
+A more interesting question is how to map an arbitrary configuration
-\{x_1, \dots, x_n\}$ for the restriction of environment $\gamma$ to
+to a computation term.
-$\dom(\gamma) \res \{x_1, \dots, x_n\}$.
+%
+Figure~\ref{fig:config-to-term} describes such a mapping $\inv{-}$
+from configurations to terms via a collection of mutually recursive
+functions defined on configurations, continuations, handler closures,
+computation terms, handler definitions, value terms, and machine
+values. The mapping makes use of a domain operation and a restriction
+operation on environments.
+%
+\begin{definition}
+  The domain of an environment is defined recursively as follows.
+  %
+  \[
+    \bl
+    \dom : \MEnvCat \to \VarCat\\
+    \ba{@{}l@{~}c@{~}l}
+      \dom(\emptyset) &\defas& \emptyset\\
+      \dom(\env[x \mapsto v]) &\defas& \{x\} \cup \dom(\env)
+    \ea
+    \el
+  \]
+  %
+  We write $\env \res \{x_1, \dots, x_n\}$ for the restriction of
+  environment $\env$ to $\dom(\env) \res \{x_1, \dots, x_n\}$.
+\end{definition}
 %
 The $\inv{-}$ function enables us to classify the abstract machine
-reduction rules by how they relate to the operational
+reduction rules according to how they relate to the context-based
-semantics.
+small-step semantics.
 %
-The rules \mlab{Init} and \mlab{Halt} concern only initial input and
+Both the rules \mlab{Let} and \mlab{Forward} are administrative in the
-final output, neither a feature of the operational semantics.
+sense that $\inv{-}$ is invariant under either rule.
 %
-The rules \mlab{Resume^\depth}, \mlab{Resume^\param}, \mlab{Let},
+This leaves the $\beta$-rules \mlab{App}, \mlab{AppRec}, \mlab{TyApp},
-\mlab{Handle^\depth}, \mlab{Handle^\param}, and \mlab{Forward} are
+\mlab{Resume^\delta}, \mlab{Split}, \mlab{Case}, \mlab{PureCont}, and
-administrative in that $\inv{-}$ is invariant under them.
+\mlab{GenCont}. Each of these corresponds directly with performing a
+reduction in the small-step semantics. We extend the notion of
+transition to account for administrative steps.
 %
-This leaves $\beta$-rules \mlab{App}, \mlab{AppRec}, \mlab{AppType},
+\begin{definition}[Auxiliary reduction relations]
-\mlab{Split}, \mlab{Case}, \mlab{PureCont}, \mlab{GenCont},
+  We write $\stepsto_{\textrm{a}}$ for administrative steps and
-\mlab{Do^\depth}, and \mlab{Do^\dagger}, each of which corresponds
+  $\simeq_{\textrm{a}}$ for the symmetric closure of
-directly to performing a reduction in the operational semantics.
+  $\stepsto_{\textrm{a}}^*$. We write $\stepsto_\beta$ for
+  $\beta$-steps and $\Stepsto$ for a sequence of steps of the form
+  $\stepsto_{\textrm{a}}^\ast \stepsto_\beta$.
+\end{definition}
 %
-We write $\stepsto_a$ for administrative steps, $\stepsto_\beta$ for
+The following lemma describes how we can simulate each reduction in
-$\beta$-steps, and $\Stepsto$ for a sequence of steps of the form
+the small-step reduction semantics by a sequence of administrative
-$\stepsto_a^* \stepsto_\beta$.
+steps followed by one $\beta$-step in the abstract machine.
-
-Each reduction in the operational semantics is simulated by a sequence
-of administrative steps followed by a single $\beta$-step in the
-abstract machine. The $Id$ handler (Section~\ref{subsec:terms})
-implements the top-level identity continuation.
 %
-\begin{theorem}[Simulation]
+\begin{lemma}
-\label{lem:simulation}
+\label{lem:machine-simulation}
-If $M \reducesto N$, then for any $\conf$ such that $\inv{\conf} =
+Suppose $M$ is a computation and $\conf$ is configuration such that
-Id(M)$ there exists $\conf'$ such that $\conf \Stepsto \conf'$ and
+$\inv{\conf} = M$, then if $M \reducesto N$ there exists $\conf'$ such
-$\inv{\conf'} = Id(N)$.
+that $\conf \Stepsto \conf'$ and $\inv{\conf'} = N$, or if
-%% If $M \reducesto N$, then for any $\conf$ such that $\inv{\conf} = M$
+$M \not\reducesto$ then $\conf \not\Stepsto$.
-%% there exists $\conf'$ such that $\conf \Stepsto \conf'$ and
+\end{lemma}
-%% $\inv{\conf'} = N$.
-\end{theorem}
 %
 \begin{proof}
 By induction on the derivation of $M \reducesto N$.
 \end{proof}
-
+%
-\begin{corollary}
+The correspondence here is rather strong: there is a one-to-one
-If $\typc{}{M : A}{E}$ and $M \reducesto^+ N \not\reducesto$, then $M
+mapping between $\reducesto$ and the quotient relation of $\Stepsto$
-\stepsto^+ \conf$ with $\inv{\conf} = N$.
+and $\simeq_{\textrm{a}}$. % The inverse of the lemma is straightforward
-\end{corollary}
+% as the semantics is deterministic.
+%
+Notice that Lemma~\ref{lem:machine-simulation} does not require that
+$M$ be well-typed. This is mostly a convenience to simplify the
+lemma. The lemma is used in the following theorem where it is being
+applied only on well-typed terms.
+%
+\begin{theorem}[Simulation]\label{thm:handler-simulation}
+  If $\typc{}{M : A}{E}$ and $M \reducesto^+ N$ such that $N$ is
+  normal with respect to $E$, then
+  $\cek{M \mid \emptyset \mid \kappa_0} \stepsto^+ \conf$ such that
+  $\inv{\conf} = N$, or $M \not\reducesto$ then
+  $\cek{M \mid \emptyset \mid \kappa_0} \not\stepsto$.
+\end{theorem}
+%
+\begin{proof}
+By repeated application of Lemma~\ref{lem:machine-simulation}.
+\end{proof}
 
 \section{Related work}
 The literature on abstract machines is vast and rich. I describe here
@@ -11631,7 +11674,7 @@ than right-to-left evaluation order is now considered a bug (subject
 to some exceptions, notably short-circuiting logical and/or
 functions).
 
-\paragraph{Mechanic machine derivations}
+\paragraph{Mechanical machine derivations}
 %
 There are deep mathematical connections between environment-based
 abstract machine semantics and standard reduction semantics with
@@ -11649,14 +11692,15 @@ programming language Agda.
 %
 \citet{HuttonW04} demonstrate how to calculate a
 correct-by-construction abstract machine from a given specification
-using structural induction. Notably, their example machine supports a
+using structural induction. Notably, their example machine supports
-basic notion of exceptions.
+basic computational effects in the form of exceptions.
 %
-Derivations of abstract machines for languages with computational
+\citet{AgerDM05} also extended their technique to derive abstract
-effects were also explored by \citet{AgerDM05}.
+machines from monadic-style effectful evaluators.
 
 
 \part{Expressiveness}
+\label{p:expressiveness}
 \chapter{Interdefinability of effect handlers}
 \label{ch:deep-vs-shallow}
 
@@ -12508,13 +12552,93 @@ Describe the methodology\dots
 % \section{Effect system}
 
 \part{Conclusions}
+\label{p:conclusions}
 
-\chapter{Conclusions}
+\chapter{Conclusions and future work}
 \label{ch:conclusions}
-Some profound conclusions\dots
+%
+I will begin this chapter with a brief summary of this
+dissertation. The following sections each elaborates and spells out
+directions for future work.
 
-\chapter{Future Work}
+In Part~\ref{p:background} of this dissertation I have compiled an
-\label{ch:future-work}
+extensive survey of first-class control. In this survey I characterise
+the various kinds of control phenomena that appear in the literature
+as well as providing an overview of the operational characteristics of
+control operators appearing in the literature. To the best of my
+knowledge this survey is the only of its kind in the present
+literature.
+
+In Part~\ref{p:design} I have presented the design of a ML-like
+programming language equipped an effect-and-type system and a
+structural notion of effectful operations and effect handlers. In this
+language I have demonstrated how to implement the essence of a
+\UNIX{}-like operating system by making, almost, zealous use of deep,
+shallow, and parameterised effect handlers.
+
+In Part~\ref{p:implementation} I have devised two canonical
+implementation strategies for the language, one based an
+transformation into continuation passing style, and another based on
+abstract machine semantics. Both strategies make key use of the notion
+of generalised continuations, which
+
+In Part~\ref{p:expressiveness} I have explored how effect handlers fit
+into the wider landscape of programming abstractions.
+
+\section{Effect handler-oriented programming}
+In Chapters~\ref{ch:base-language} and \ref{ch:unary-handlers} I
+explored the design space of programming languages with effect
+handlers. My design differentiates itself from others in the literature
+with respect to the kind of programming language considered. I have
+focused a language with structural data and effects, whereas others
+have focused on nominal data and effects. An effect system is
+necessary to ensure safety and soundness in a structural
+setting. Although, an effect system is informative, it is not strictly
+necessary in a nominal setting.
+%
+Another point of emphasis is that my design incorporates deep,
+shallow, and parameterised variations of effect handlers into a single
+programming language. I have demonstrated applications that each kind
+of handler is uniquely suited for by way of the case study of
+Section~\ref{sec:deep-handlers-in-action}.
+
+
+\subsection{Future work}
+\begin{itemize}
+  \item Efficiency of nested handlers.
+  \item Effect-based optimisations.
+  \item Equational theories.
+  \item Signal handling.
+  \item Implement an actual operation system using handlers.
+  \item Re-implement the case study in other programming languages.
+  \item Parallel and distributed programming with effect handlers.
+  \item Multi-handlers.
+\end{itemize}
+
+\section{Implementation strategies for effect handlers}
+
+\subsection{Future work}
+\begin{itemize}
+  \item Formally relate the CPS translation and the abstract machine.
+  \item Type the CPS translation.
+  \item Simulate generalised continuations with other programming facilities.
+  \item Abstracting continuations.
+  \item Multi-handlers.
+\end{itemize}
+
+\section{On the expressive power of effect handlers}
+
+\subsection{Future work}
+\begin{itemize}
+  \item Investigate whether there exists efficient encodings of shallow
+    handlers in terms of deep handlers.
+  \item Establish a hierarchy of asymptotic efficiency for control
+    structures (iteration, recursion, backtracking, first-class
+    control).
+  \item Investigate how to adapt the asymptotic result to a setting
+    with effect tracking.
+  \item Extend the result to linear effect handlers.
+\end{itemize}
 
 %%
 %% Appendices