diff --git a/thesis.tex b/thesis.tex index 9592e24..72a2348 100644 --- a/thesis.tex +++ b/thesis.tex @@ -4226,20 +4226,51 @@ The term `pure' is heavily overloaded in the programming literature. \chapter{Programming with control via effect handlers} \label{ch:unary-handlers} % -In this chapter we study various flavours of unary effect -handlers~\cite{PlotkinP13}, that is handlers of a single -computation. Concretely, we shall study four variations of effect -handlers: in Section~\ref{sec:unary-deep-handlers} we augment the base -calculus \BCalc{} with \emph{deep} effect handlers yielding the -calculus \HCalc{}; subsequently in -Sections~\ref{sec:unary-parameterised-handlers} and -\ref{sec:unary-default-handlers} we refine \HCalc{} with two practical -relevant kinds of handlers, namely, \emph{parameterised} and -\emph{default} handlers. The former is a specialisation of a -particular class of deep handlers, whilst the latter is important for -programming at large. Finally in -Section~\ref{sec:unary-shallow-handlers} we study \emph{shallow} -effect handlers which are an alternative to deep effect handlers. +Programming with effect handlers is a dichotomy of \emph{performing} +and \emph{handling} of effectful operations -- or alternatively a +dichotomy of \emph{constructing} and \emph{deconstructing} effects. An +operation is a constructor of an effect. By itself an operation has no +predefined semantics. A handler deconstructs effects by +pattern-matching on their operations. By matching on a particular +operation, a handler instantiates the said operation with a particular +semantics of its own choosing. The key ingredient to make this work in +practice is \emph{delimited control}. Performing an operation reifies +the remainder of the computation up to the nearest enclosing handler +of the said operation as a continuation. The continuation is provided +to the programmer via the handler, and it may be manipulated like any +other first-class value. + +Effect handlers provide a structured interface for programming with +delimited continuations. They are structured in the sense that an +invocation site of an operation is decoupled from the use site of its +continuation. A continuation is exposed in the corresponding operation +cases inside the handler of its operation of provenance. + +I will make a slight change of terminology to disambiguate +programmatic continuations, i.e. continuations exposed to the +programmer, from continuations in continuation passing style +(Chapter~\ref{ch:cps}) and machine continuations +(Chapter~\ref{ch:abstract-machine}). In the remainder of this +dissertation I refer to programmatic continuations as `resumptions', +and reserve the term `continuation' for continuations concerning the +implementation details. + + + +% In this chapter we study various flavours of unary effect +% handlers~\cite{PlotkinP13}, that is handlers of a single +% computation. Concretely, we shall study four variations of effect +% handlers: in Section~\ref{sec:unary-deep-handlers} we augment the base +% calculus \BCalc{} with \emph{deep} effect handlers yielding the +% calculus \HCalc{}; subsequently in +% Sections~\ref{sec:unary-parameterised-handlers} and +% \ref{sec:unary-default-handlers} we refine \HCalc{} with two practical +% relevant kinds of handlers, namely, \emph{parameterised} and +% \emph{default} handlers. The former is a specialisation of a +% particular class of deep handlers, whilst the latter is important for +% programming at large. Finally in +% Section~\ref{sec:unary-shallow-handlers} we study \emph{shallow} +% effect handlers which are an alternative to deep effect handlers. % , First we endow \BCalc{} @@ -4257,17 +4288,17 @@ effect handlers which are an alternative to deep effect handlers. \section{Deep handlers} \label{sec:unary-deep-handlers} % -Programming with effect handlers is a dichotomy of \emph{performing} -and \emph{handling} of effectful operations -- or alternatively a -dichotomy of \emph{constructing} and \emph{deconstructing}. An operation -is a constructor of an effect without a predefined semantics. A -handler deconstructs effects by pattern-matching on their operations. By -matching on a particular operation, a handler instantiates the said -operation with a particular semantics of its own choosing. The key -ingredient to make this work in practice is \emph{delimited - control}~\cite{Landin65,Landin65a,Landin98,FelleisenF86,DanvyF90}. Performing -an operation reifies the remainder of the computation up to the -nearest enclosing handler of the said operation. +% Programming with effect handlers is a dichotomy of \emph{performing} +% and \emph{handling} of effectful operations -- or alternatively a +% dichotomy of \emph{constructing} and \emph{deconstructing}. An operation +% is a constructor of an effect without a predefined semantics. A +% handler deconstructs effects by pattern-matching on their operations. By +% matching on a particular operation, a handler instantiates the said +% operation with a particular semantics of its own choosing. The key +% ingredient to make this work in practice is \emph{delimited +% control}~\cite{Landin65,Landin65a,Landin98,FelleisenF86,DanvyF90}. Performing +% an operation reifies the remainder of the computation up to the +% nearest enclosing handler of the said operation. As our starting point we take the regular base calculus, \BCalc{}, without the recursion operator. We elect to do so to understand @@ -4291,7 +4322,7 @@ no predefined dynamic semantics. The introduction form for effectful operations is a computation term. % \begin{syntax} - \slab{Value types} &A,B \in \ValTypeCat &::=& \cdots \mid~ \tikzmarkin{optype} A \opto B \tikzmarkend{optype}\\ + \slab{Value\textrm{ }types} &A,B \in \ValTypeCat &::=& \cdots \mid~ \tikzmarkin{optype} A \opto B \tikzmarkend{optype}\\ \slab{Computations} &M,N \in \CompCat &::=& \cdots \mid~ \tikzmarkin{do1} (\Do \; \ell~V)^E \tikzmarkend{do1} \end{syntax} % @@ -4339,7 +4370,7 @@ First we define notation for handler kinds and types. % \begin{syntax} \slab{Kinds} &K \in \KindCat &::=& \cdots \mid~ \tikzmarkin{handlerkinds1} \Handler \tikzmarkend{handlerkinds1}\\ -\slab{Handler types} &F \in \HandlerTypeCat &::=& C \Harrow D\\ +\slab{Handler\textrm{ }types} &F \in \HandlerTypeCat &::=& C \Harrow D\\ \slab{Types} &T \in \TypeCat &::=& \cdots \mid~ \tikzmarkin{typeswithhandler} F \tikzmarkend{typeswithhandler} \end{syntax} % @@ -6013,12 +6044,12 @@ We can now plug everything together. \Record{2; \ba[t]{@{}l@{}l} \texttt{"}&\texttt{To be, or not to be,\nl{}that is the question:\nl{}}\\ - &\texttt{Whether 'tis nobler in the mind to suffer\nl{}}}; + &\texttt{Whether 'tis nobler in the mind to suffer\nl{}"}}; \ea\\ \Record{1; \ba[t]{@{}l@{}l} \texttt{"}&\texttt{UNIX is basically a simple operating system, }\\ - &\texttt{but you have to be a genius to understand the simplicity.\nl{}}}; + &\texttt{but you have to be a genius to understand the simplicity.\nl{"}}}; \ea\\ \Record{0; \strlit{}}]}} \ea @@ -6397,440 +6428,163 @@ applies the consumer's resumption to the yielded value. bar \end{example} -\section{Interdefinability of deep and shallow handlers} -\label{sec:deep-vs-shallow} +\section{Parameterised handlers} +\label{sec:unary-parameterised-handlers} -In this section we show that shallow handlers and general recursion -can simulate deep handlers up to congruence, and that deep handlers -can simulate shallow handlers up to administrative reductions. The -latter construction generalises the example of pipes implemented using -deep handlers that we gave in -Section~\ref{sec:pipes}. -% +Parameterised handlers are a useful idiom for handling stateful +computations. -\subsection{Deep as shallow} -\label{sec:deep-as-shallow} +\subsection{Syntax and static semantics} +% +\begin{figure} + \begin{syntax} + & F &::=& \cdots \mid \Record{C; A} \Rightarrow^\param D\\ + & \delta &::=& \cdots \mid \param\\ + & M,N &::=& \cdots \mid \ParamHandle\; M \;\With\; H^\param(W)\\ + & H^\param &::=& q^A.~H + \end{syntax} + \caption{Syntax extensions for parameterised handlers.}\label{fig:param-syntax} +\end{figure} +% +Figure~\ref{fig:param-syntax} extends the syntax of +$\HCalc$ with parameterised handlers. Syntactically a parameterised +handler is new binding form $(q^A.~H)$, where $q$ is the name of the +parameter, whose type is $A$. The name is bound in the ordinary +handler definition $H$. The elimination form +($\ParamHandle\; M\;\With\;H^\param(W)$) is similar to the form for +ordinary deep handlers, except that the parameterised handler +definition is applied to a value $W$, which is the initial value of +the parameter $q$. -\newcommand{\dstrans}[1]{\mathcal{S}\llbracket #1 \rrbracket} +% +\begin{figure} +\begin{mathpar} + % Handle + \inferrule*[Lab=\tylab{Param-Handle}] + { + % \typ{\Gamma}{V : A} \\ + \typ{\Gamma}{M : C} \\ + \typ{\Gamma}{W : A} \\ + \typ{\Gamma}{H^\param : \Record{C; A} \Harrow D} + } + {\Gamma \vdash \ParamHandle \; M \; \With\; H^\param(W) : D} +\end{mathpar} +~ +\begin{mathpar} +% Parameterised handler + \inferrule*[Lab=\tylab{Handler^\param}] + {{\bl + C = A \eff \{(\ell_i : A_i \to B_i)_i; R\} \\ + D = B \eff \{(\ell_i : P)_i; R\} \\ + H = \{\Return\;x \mapsto M\} \uplus \{ \OpCase{\ell_i}{p_i}{r_i} \mapsto N_i \}_i + \el}\\\\ + \typ{\Delta;\Gamma, q : A', x : A}{M : D}\\\\ + [\typ{\Delta;\Gamma,q : A', p_i : A_i, r_i : B_i \to D}{N_i : D}]_i + } + {\typ{\Delta;\Gamma}{(q^{A'} . H) : \Record{C;A'} \Harrow^\param D}} +\end{mathpar} +%% + \caption{Typing rules for parameterised handlers.}\label{fig:param-static-semantics} +\end{figure} +% +We require two additional rules to type parameterised handlers. The +rules are given in Figure~\ref{fig:param-static-semantics}. The main +differences between the \tylab{Handler} and \tylab{Handler^\param} are +that in the latter the return and operation cases are typed with +respect to the parameter $q$, and that resumptions $r$ have type +$\Record{B_\ell;A'} \to D$, that is they accept a pair as +input. -The implementation of deep handlers using shallow handlers (and -recursive functions) is by a direct local translation, similar to how -one would implement a fold (catamorphism) in terms of general -recursion. Each handler is wrapped in a recursive function and each -resumption has its body wrapped in a call to this recursive function. +\subsection{Dynamic semantics} +Operationally, a parameterised resumption uses the first component as +the return value of the operation, and the second component as the +updated value of the handler parameter $q$. % -Formally, the translation $\dstrans{-}$ is defined as the homomorphic -extension of the following equations to all terms. -\begin{equations} -\dstrans{\Handle \; M \; \With \; H} &=& - (\Rec~h~f.\ShallowHandle\; f\,\Unit \; \With \; \dstrans{H} h)\,(\lambda \Unit{}.\dstrans{M}) \\ -\dstrans{H}h &=& \dstrans{\hret}h \uplus \dstrans{\hops}h \\ -\dstrans{\{ \Return \; x \mapsto N\}} h &=& - \{ \Return \; x \mapsto \dstrans{N} \}\\ -\dstrans{\{ \ell \; p \; r \mapsto N_\ell \}_{\ell \in \mathcal{L}}} h &=& - \{ \ell \; p \; r \mapsto - \Let \; r \revto \Return \; \lambda x.h\,(\lambda \Unit{}.r\,x) \; \In \; - \dstrans{N_\ell} \}_{\ell \in \mathcal{L}} -\end{equations} +This operational behaviour is formalised by following reduction rule +$\semlab{Op^\param}$. +% +\[ +\ba{@{~}l@{~}l} + &\ParamHandle \; \EC[\Do \; \ell \; V] \; \With \; (q.~H)(W)\\ + \reducesto& + N[V/p,W/q,\lambda \Record{y;q'}.\Handle \; \EC[\Return \; y] \; \With \; (q.~H)(q')/r]\\ + & \text{ where } \ell \notin BL(\EC) \text{ and } \hell = \{ \OpCase{\ell}{p}{r} \mapsto N \} +\ea +\] +% +The parameter value $W$ is substituted for the parameter name $q$ into +the operation case body $N$. As with ordinary deep handlers, the +resumption rewraps its handler, but with the slight twist that the +parameterised handler definition is applied to the updated parameter +value $q'$ rather than the original value $W$. The reduction rule for +handling the return of a computation is as follows. +% +\[ + \ParamHandle \, (\Return \; V) \; \With \; (q.~H)(W) \reducesto N[V/x,W/q], \text{where } \hret = \{ \Return \; x \mapsto N \} +\] +% +Both the return value $V$ and the parameter value $W$ are substituted +into the return case body $N$ for their respective binders. -% \paragraph{Example} We illustrate the translation $\dstrans{-}$ on the -% EXAMPLE handler from Section~\ref{sec:strategies} (recall that the -% variable $m$ is bound to the input computation). The example here is -% reproduced in ANF notation. -% \[ -% \ba{@{~}l@{~}l@{}l} -% &\mathcal{S}&\left\llbracket -% \ba[m]{@{~}l} -% \Handle\; m~\Unit\; \With\\ -% \quad -% \ba{@{}l@{~}c@{~}l} -% \Return~x &\mapsto& \Return\;x\\ -% \Move~\Record{\_;n}~resume &\mapsto& \Let\;y \revto ps~n\;\In\; resume~y -% \ea -% \ea\right\rrbracket =\\\\ -% & -% &\ba[m]{@{}l} -% \hspace{-1ex} -% \left( -% \ba[m]{@{~}l} -% \Rec~h~f. -% \ba[t]{@{~}l} -% \ShallowHandle\; f~\Unit\; \With\\ -% \quad -% \ba{@{}l@{~}c@{~}l} -% \Return~x &\mapsto& \Return\; x\\ -% \Move~\Record{\_;n}~resume &\mapsto&\\ -% \quad\ba[t]{@{~}l@{}} -% \Let\; r \revto \Return\; \lambda x. h (\lambda\Unit.resume~x)\;\In\\ -% \Let\; y \revto ps~n\; \In\; r~y -% \ea -% \ea -% \ea -% \ea\right)~(\lambda \Unit. m~\Unit) -% \ea -% \ea -% \]\\ +\subsection{Lightweight concurrency} -\begin{theorem} -If $\Delta; \Gamma \vdash M : C$ then $\Delta; \Gamma \vdash -\dstrans{M} : C$. -\end{theorem} +\begin{example}[Green threads] + \dhil{Example: Lightweight threads} +\end{example} -In order to obtain a simulation result, we allow reduction in the -simulated term to be performed under lambda abstractions (and indeed -anywhere in a term), which is necessary because of the redefinition of -the resumption to wrap the handler around its body. -% -Nevertheless, the simulation proof makes minimal use of this power, -merely using it to rename a single variable. -% -We write $R_{\mathrm{cong}}$ for the compatible closure of relation -$R$, that is the smallest relation including $R$ and closed under term -constructors for $\SCalc$. -%% , otherwise known as \emph{reduction up to -%% congruence}. +% \section{Default handlers} +% \label{sec:unary-default-handlers} -\begin{theorem}[Simulation up to congruence] -If $M \reducesto N$ then $\dstrans{M} \reducesto_{\mathrm{cong}}^+ -\dstrans{N}$. -\end{theorem} +% \chapter{N-ary handlers} +% \label{ch:multi-handlers} -\begin{proof} - By induction on $\reducesto$ using a substitution lemma. The - interesting case is $\semlab{Op}$, which is where we apply a single - $\beta$-reduction, renaming a variable, under the lambda abstraction - representing the resumption. -\end{proof} +% \section{Syntax and Static Semantics} +% \section{Dynamic Semantics} +% \section{Unifying deep and shallow handlers} + +\section{Related work} +\label{sec:unix-related-work} -\subsection{Shallow as deep} +\subsection{Interleaving computation} -\newcommand{\sdtrans}[1]{\mathcal{D}\llbracket #1 \rrbracket} +\paragraph{The resumption monad} \citet{Milner75}, +\citet{Plotkin76}, \citet{Moggi90}, \citet{Papaspyrou01}, \citet{Harrison06}, \citet{AtkeyJ15} -Implementing shallow handlers in terms of deep handlers is slightly -more involved than the other way round. +\paragraph{Continuation-based interleaving} +First implementation of `threads' is due to \citet{Burstall69}. \citet{Wand80} \citet{HaynesF84} \citet{GanzFW99} \citet{HiebD90} + +\subsection{Effect-driven concurrency} +\citet{BauerP15}, \citet{DolanWSYM15}, \citet{Hillerstrom16}, \citet{DolanEHMSW17}, \citet{Convent17}, \citet{Poulson20} + +\part{Implementation} + +\chapter{Continuation-passing style} +\label{ch:cps} + +Continuation-passing style (CPS) is a \emph{canonical} program +notation that makes every facet of control flow and data flow +explicit. In CPS every function takes an additional function-argument +called the \emph{continuation}, which represents the next computation +in evaluation position. CPS is canonical in the sense that it is +definable in pure $\lambda$-calculus without any further +primitives. As an informal illustration of CPS consider again the +rudimentary factorial function from Section~\ref{sec:tracking-div}. % -It amounts to the encoding of a case split by a fold and involves a -translation on handler types as well as handler terms. -% -Formally, the translation $\sdtrans{-}$ is defined as the homomorphic -extension of the following equations to all types, terms, and type -environments. -\begin{equations} - \sdtrans{C \Rightarrow D} &=& - \sdtrans{C} \Rightarrow \Record{\UnitType \to \sdtrans{C}; \UnitType \to \sdtrans{D}} \medskip \\ - \sdtrans{\ShallowHandle \; M \; \With \; H} &=& - \ba[t]{@{}l} - \Let\;z \revto \Handle \; \sdtrans{M} \; \With \; \sdtrans{H} \; \In\\ - \Let\;\Record{f; g} = z \;\In\; - g\,\Unit - \ea \\ - \sdtrans{H} &=& \sdtrans{\hret} \uplus \sdtrans{\hops} \\ - \sdtrans{\{\Return \; x \mapsto N\}} &=& - \{\Return \; x \mapsto \Return\; \Record{\lambda \Unit.\Return\; x; \lambda \Unit.\sdtrans{N}}\} \\ - \sdtrans{\{\ell\; p\; r \mapsto N\}_{\ell \in \mathcal{L}}} &=& \{ - \bl - \ell\; p\; r \mapsto \\ - \quad \Let \;r \revto - \lambda x. \Let\; z \revto r\,x\; \In\; - \Let\; \Record{f; g} = z\; \In\; f\,\Unit - \; \In\\ - \quad \Return\;\Record{\lambda \Unit.\Let\; x \revto \Do\;\ell\,p\; \In\; r\,x; \lambda \Unit.\sdtrans{N}}\}_{\ell \in \mathcal{L}} - \el -\end{equations} -% -Each shallow handler is encoded as a deep handler that returns a pair -of thunks. The first forwards all operations, acting as the identity -on computations. The second interprets a single operation before -reverting to forwarding. - -% \paragraph{Example} We demonstrate the translation $\sdtrans{-}$ on -% the $\Pipe$ handler from Section~\ref{sec:shallow-handlers-tutorial} -% (recall that the variables $c$ and $p$ are bound to the consumer and -% producer functions respectively). The example is reproduced in ANF -% notation. -% % -% \[ -% \ba{@{~}l@{~}l@{}l} -% &\mathcal{D}&\left\llbracket -% \ba[m]{@{~}l} -% \ShallowHandle\; c\,\Unit \;\With\; \\ -% \quad -% \ba[m]{@{}l@{~}c@{~}l@{}} -% \Return~x &\mapsto& \Return\; x \\ -% \Await~\Unit~resume &\mapsto& \Copipe\; \Record{resume; p} \\ -% \ea \\ -% \ea\right\rrbracket = \\ -% & -% &\ba[t]{@{~}l} -% \Let\; z \revto -% \ba[t]{@{~}l} -% \Handle\; c~\Unit \; \With\\ -% \quad \ba[m]{@{~}l} -% \ba[m]{@{~}l@{~}l} -% \Return~x &\mapsto \Return\; \Record{\lambda\Unit. \Return\; x; \lambda\Unit. \Return\;x}\\ -% \Await~\Unit~resume &\mapsto -% \ea\\ -% \qquad\ba[t]{@{~}l} -% \Let\;r \revto \lambda x.\Let\; z \revto resume~x\; -% \In\; \Let\; \Record{f; g} = z \;\In\; f~\Unit\; \In\\ -% \Return\;\Record{\lambda \Unit. \Let\; x \revto \Do\; \ell~p \;\In\; r~x; -% \lambda\Unit.\sdtrans{\Copipe}\Record{r; p}} -% \ea -% \ea -% \ea\\ -% \In\;\Let\;\Record{f; g} = z\; \In\; g~\Unit -% \ea -% \ea -% \] -% - -\begin{theorem} -If $\Delta; \Gamma \vdash M : C$ then $\sdtrans{\Delta}; -\sdtrans{\Gamma} \vdash \sdtrans{M} : \sdtrans{C}$. -\end{theorem} - - -\newcommand{\admin}{admin} -\newcommand{\approxa}{\gtrsim} - -As with the implementation of deep handlers as shallow handlers, the -implementation is again given by a local translation. However, this -time the administrative overhead is more significant. Reduction up to -congruence is insufficient and we require a more semantic notion of -administrative reduction. - -\begin{definition}[Administrative evaluation contexts] -An evaluation context $\EC$ is administrative, $\admin(\EC)$, iff -\begin{enumerate} -\item For all values $V$, we have: $\EC[\Return\;V] \reducesto^\ast - \Return\;V$ -\item For all evaluation contexts $\EC'$, operations $\ell \in BL(\EC) - \backslash BL(\EC')$, values $V$: -% -\[ - \EC[\EC'[\Do\;\ell\;V]] \reducesto^\ast \Let\; x \revto \Do\;\ell\;V \;\In\; \EC[\EC'[\Return\;x]]. -\] -\end{enumerate} -\end{definition} -% -The intuition is that an administrative evaluation context behaves -like the empty evaluation context up to some amount of administrative -reduction, which can only proceed once the term in the context becomes -sufficiently evaluated. -% -Values annihilate the evaluation context and handled operations are -forwarded. -% -%% The forwarding handler is a technical device which allows us to state -%% the second property in a uniform way by ensuring that the operation is -%% handled at least once. - -\begin{definition}[Approximation up to administrative reduction] -Define $\approxa$ as the compatible closure of the following inference -rules. -% -\begin{mathpar} - \inferrule* - { } - {M \approxa M} - - \inferrule* - {M \reducesto M' \\ M' \approxa N} - {M \approxa N} - - \inferrule* - {\admin(\EC) \\ M \approxa N} - {\EC[M] \approxa N} -\end{mathpar} -% -We say that $M$ approximates $N$ up to administrative reduction if $M -\approxa N$. -\end{definition} -% -Approximation up to administrative reduction captures the property -that administrative reduction may occur anywhere within a term. -% -The following lemma states that the forwarding component of the -translation is administrative. -\begin{lemma}\label{lem:sdtrans-admin} -For all shallow handlers $H$, the following context is administrative: -\begin{displaymath} -\Let\; z \revto - \Handle\; [~] \;\With\; \sdtrans{H}\; - \In\; - \Let\; \Record{f;\_} = z\; \In\; f\,\Unit. -\end{displaymath} -\end{lemma} - -\begin{theorem}[Simulation up to administrative reduction] -If $M' \approxa \sdtrans{M}$ and $M \reducesto N$ then there exists -$N'$ such that $N' \approxa \sdtrans{N}$ and $M' \reducesto^+ N'$. -\end{theorem} -% -\begin{proof} -By induction on $\reducesto$ using a substitution lemma and -Lemma~\ref{lem:sdtrans-admin}. The interesting case is -$\semlab{Op^\dagger}$, which uses Lemma~\ref{lem:sdtrans-admin} to -approximate the body of the resumption up to administrative reduction. -\end{proof} - -\section{Parameterised handlers} -\label{sec:unary-parameterised-handlers} - -Parameterised handlers are a useful idiom for handling stateful -computations. - -\subsection{Syntax and static semantics} -% -\begin{figure} - \begin{syntax} - & F &::=& \cdots \mid \Record{C; A} \Rightarrow^\param D\\ - & \delta &::=& \cdots \mid \param\\ - & M,N &::=& \cdots \mid \ParamHandle\; M \;\With\; H^\param(W)\\ - & H^\param &::=& q^A.~H - \end{syntax} - \caption{Syntax extensions for parameterised handlers.}\label{fig:param-syntax} -\end{figure} -% -Figure~\ref{fig:param-syntax} extends the syntax of -$\HCalc$ with parameterised handlers. Syntactically a parameterised -handler is new binding form $(q^A.~H)$, where $q$ is the name of the -parameter, whose type is $A$. The name is bound in the ordinary -handler definition $H$. The elimination form -($\ParamHandle\; M\;\With\;H^\param(W)$) is similar to the form for -ordinary deep handlers, except that the parameterised handler -definition is applied to a value $W$, which is the initial value of -the parameter $q$. - -% -\begin{figure} -\begin{mathpar} - % Handle - \inferrule*[Lab=\tylab{Param-Handle}] - { - % \typ{\Gamma}{V : A} \\ - \typ{\Gamma}{M : C} \\ - \typ{\Gamma}{W : A} \\ - \typ{\Gamma}{H^\param : \Record{C; A} \Harrow D} - } - {\Gamma \vdash \ParamHandle \; M \; \With\; H^\param(W) : D} -\end{mathpar} -~ -\begin{mathpar} -% Parameterised handler - \inferrule*[Lab=\tylab{Handler^\param}] - {{\bl - C = A \eff \{(\ell_i : A_i \to B_i)_i; R\} \\ - D = B \eff \{(\ell_i : P)_i; R\} \\ - H = \{\Return\;x \mapsto M\} \uplus \{ \OpCase{\ell_i}{p_i}{r_i} \mapsto N_i \}_i - \el}\\\\ - \typ{\Delta;\Gamma, q : A', x : A}{M : D}\\\\ - [\typ{\Delta;\Gamma,q : A', p_i : A_i, r_i : B_i \to D}{N_i : D}]_i - } - {\typ{\Delta;\Gamma}{(q^{A'} . H) : \Record{C;A'} \Harrow^\param D}} -\end{mathpar} -%% - \caption{Typing rules for parameterised handlers.}\label{fig:param-static-semantics} -\end{figure} -% -We require two additional rules to type parameterised handlers. The -rules are given in Figure~\ref{fig:param-static-semantics}. The main -differences between the \tylab{Handler} and \tylab{Handler^\param} are -that in the latter the return and operation cases are typed with -respect to the parameter $q$, and that resumptions $r$ have type -$\Record{B_\ell;A'} \to D$, that is they accept a pair as -input. - -\subsection{Dynamic semantics} -Operationally, a parameterised resumption uses the first component as -the return value of the operation, and the second component as the -updated value of the handler parameter $q$. -% -This operational behaviour is formalised by following reduction rule -$\semlab{Op^\param}$. -% -\[ -\ba{@{~}l@{~}l} - &\ParamHandle \; \EC[\Do \; \ell \; V] \; \With \; (q.~H)(W)\\ - \reducesto& - N[V/p,W/q,\lambda \Record{y;q'}.\Handle \; \EC[\Return \; y] \; \With \; (q.~H)(q')/r]\\ - & \text{ where } \ell \notin BL(\EC) \text{ and } \hell = \{ \OpCase{\ell}{p}{r} \mapsto N \} -\ea -\] -% -The parameter value $W$ is substituted for the parameter name $q$ into -the operation case body $N$. As with ordinary deep handlers, the -resumption rewraps its handler, but with the slight twist that the -parameterised handler definition is applied to the updated parameter -value $q'$ rather than the original value $W$. The reduction rule for -handling the return of a computation is as follows. -% -\[ - \ParamHandle \, (\Return \; V) \; \With \; (q.~H)(W) \reducesto N[V/x,W/q], \text{where } \hret = \{ \Return \; x \mapsto N \} -\] -% -Both the return value $V$ and the parameter value $W$ are substituted -into the return case body $N$ for their respective binders. - -\subsection{Lightweight concurrency} - -\begin{example}[Green threads] - \dhil{Example: Lightweight threads} -\end{example} - -% \section{Default handlers} -% \label{sec:unary-default-handlers} - -% \chapter{N-ary handlers} -% \label{ch:multi-handlers} - -% \section{Syntax and Static Semantics} -% \section{Dynamic Semantics} -% \section{Unifying deep and shallow handlers} - -\section{Related work} -\label{sec:unix-related-work} - -\subsection{Interleaving computation} - -\paragraph{The resumption monad} \citet{Milner75}, -\citet{Plotkin76}, \citet{Moggi90}, \citet{Papaspyrou01}, \citet{Harrison06}, \citet{AtkeyJ15} - -\paragraph{Continuation-based interleaving} -First implementation of `threads' is due to \citet{Burstall69}. \citet{Wand80} \citet{HaynesF84} \citet{GanzFW99} \citet{HiebD90} - -\subsection{Effect-driven concurrency} -\citet{BauerP15}, \citet{DolanWSYM15}, \citet{Hillerstrom16}, \citet{DolanEHMSW17}, \citet{Convent17}, \citet{Poulson20} - -\part{Implementation} - -\chapter{Continuation-passing style} -\label{ch:cps} - -Continuation-passing style (CPS) is a \emph{canonical} program -notation that makes every facet of control flow and data flow -explicit. In CPS every function takes an additional function-argument -called the \emph{continuation}, which represents the next computation -in evaluation position. CPS is canonical in the sense that it is -definable in pure $\lambda$-calculus without any further -primitives. As an informal illustration of CPS consider again the -rudimentary factorial function from Section~\ref{sec:tracking-div}. -% -\[ - \bl - \dec{fac} : \Int \to \Int\\ - \dec{fac} \defas \lambda n. - \ba[t]{@{}l} - \Let\;is\_zero \revto n = 0\;\In\\ - \If\;is\_zero\;\Then\; \Return\;1\\ - \Else\;\ba[t]{@{~}l} - \Let\; n' \revto n - 1 \;\In\\ - \Let\; m \revto f~n' \;\In\\ - n * m - \ea - \ea - \el -\] +\[ + \bl + \dec{fac} : \Int \to \Int\\ + \dec{fac} \defas \lambda n. + \ba[t]{@{}l} + \Let\;is\_zero \revto n = 0\;\In\\ + \If\;is\_zero\;\Then\; \Return\;1\\ + \Else\;\ba[t]{@{~}l} + \Let\; n' \revto n - 1 \;\In\\ + \Let\; m \revto f~n' \;\In\\ + n * m + \ea + \ea + \el +\] % The above implementation of the function $\dec{fac}$ is given in direct-style fine-grain call-by-value. In CPS notation the @@ -9370,118 +9124,395 @@ Computation terms &=& \Handle^\depth\;\inv{M}\env\;\With\;\inv{H}\env \\ \end{equations} -Handler definitions +Handler definitions +\begin{equations} +\inv{\{\Return\;x \mapsto M\}}\env + &=& \{\Return\;x \mapsto \inv{M}(\env \res \{x\})\} \\ +\inv{\{\ell\;x\;k \mapsto M\} \uplus H}\env + &=& \{\ell\;x\;k \mapsto \inv{M}(\env \res \{x, k\}\} \uplus \inv{H}\env \\ +\end{equations} + +Value terms and values +\begin{displaymath} +\ba{@{}c@{}} +\begin{eqs} +\inv{x}\env &=& \inv{v}, \quad \text{ if }\env(x) = v \\ +\inv{x}\env &=& x, \quad \text{ if }x \notin dom(\env) \\ +\inv{\lambda x^A.M}\env &=& \lambda x^A.\inv{M}(\env \res \{x\}) \\ +\inv{\Lambda \alpha^K.M}\env &=& \Lambda \alpha^K.\inv{M}\env \\ +\inv{\Record{}}\env &=& \Record{} \\ +\inv{\Record{\ell=V; W}}\env &=& \Record{\ell=\inv{V}\env; \inv{W}\env} \\ +\inv{(\ell\;V)^R}\env &=& (\ell\;\inv{V}\env)^R \\ +\end{eqs} +\quad +\begin{eqs} +\inv{\shk^A} &=& \lambda x^A.\inv{\shk}(\Return\;x) \\ +\inv{(\shk, \slk)^A} &=& \lambda x^A.\inv{\slk}(\inv{\shk}(\Return\;x)) \\ +\inv{(\env, \lambda x^A.M)} &=& \lambda x^A.\inv{M}(\env \res \{x\}) \\ +\inv{(\env, \Lambda \alpha^K.M)} &=& \Lambda \alpha^K.\inv{M}\env \\ +\inv{\Record{}} &=& \Record{} \\ +\inv{\Record{\ell=v; w}} &=& \Record{\ell=\inv{v}; \inv{w}} \\ +\inv{(\ell\;v)^R} &=& (\ell\;\inv{v})^R \\ +\end{eqs} \smallskip\\ +\inv{\Rec\,g^{A \to C}\,x.M}\env = \Rec\,g^{A \to C}\,x.\inv{M}(\env \res \{g, x\}) + = \inv{(\env, \Rec\,g^{A \to C}\,x.M)} \\ +\ea +\end{displaymath} + +\caption{Mapping from abstract machine configurations to terms.} +\label{fig:config-to-term} +\end{figure} + + +\paragraph{Remark} If the main continuation is empty then the machine gets +stuck. This occurs when an operation is unhandled, and the forwarding +continuation describes the succession of handlers that have failed to +handle the operation along with any pure continuations that were +encountered along the way. +% +Assuming the input is a well-typed closed computation term $\typc{}{M + : A}{E}$, the machine will either not terminate, return a value of +type $A$, or get stuck failing to handle an operation appearing in +$E$. We now make the correspondence between the operational semantics +and the abstract machine more precise. + +\section{Correctness} +\label{subsec:machine-correctness} + +Fig.~\ref{fig:config-to-term} defines an inverse mapping $\inv{-}$ +from configurations to computation terms via a collection of mutually +recursive functions defined on configurations, continuations, +computation terms, handler definitions, value terms, and values. +% +We write $dom(\gamma)$ for the domain of $\gamma$ and $\gamma \res +\{x_1, \dots, x_n\}$ for the restriction of environment $\gamma$ to +$dom(\gamma) \res \{x_1, \dots, x_n\}$. +% +The $\inv{-}$ function enables us to classify the abstract machine +reduction rules by how they relate to the operational +semantics. +% +The rules (\mlab{Init}) and (\mlab{RetTop}) concern only initial +input and final output, neither a feature of the operational +semantics. +% +The rules (\mlab{AppCont^\depth}), (\mlab{Let}), (\mlab{Handle}), +and (\mlab{Forward}) are administrative in that $\inv{-}$ is invariant +under them. +% +This leaves $\beta$-rules (\mlab{AppClosure}), (\mlab{AppRec}), +(\mlab{AppType}), (\mlab{Split}), (\mlab{Case}), (\mlab{RetCont}), +(\mlab{RetHandler}), (\mlab{Do}), and (\mlab{Do^\dagger}), +each of which corresponds directly to performing a reduction in the +operational semantics. +% +We write $\stepsto_a$ for administrative steps, $\stepsto_\beta$ for +$\beta$-steps, and $\Stepsto$ for a sequence of steps of the form +$\stepsto_a^* \stepsto_\beta$. + +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 (\S\ref{subsec:terms}) +implements the top-level identity continuation. +\\ +\begin{theorem}[Simulation] +\label{lem:simulation} +If $M \reducesto N$, then for any $\conf$ such that $\inv{\conf} = +Id(M)$ there exists $\conf'$ such that $\conf \Stepsto \conf'$ and +$\inv{\conf'} = Id(N)$. +%% If $M \reducesto N$, then for any $\conf$ such that $\inv{\conf} = M$ +%% there exists $\conf'$ such that $\conf \Stepsto \conf'$ and +%% $\inv{\conf'} = N$. +\end{theorem} + +\begin{proof} +By induction on the derivation of $M \reducesto N$. +\end{proof} + +\begin{corollary} +If $\typc{}{M : A}{E}$ and $M \reducesto^+ N \not\reducesto$, then $M +\stepsto^+ \conf$ with $\inv{\conf} = N$. +\end{corollary} + + +\part{Expressiveness} +\chapter{Interdefinability of deep and shallow handlers} +\label{ch:deep-vs-shallow} + +In this section we show that shallow handlers and general recursion +can simulate deep handlers up to congruence, and that deep handlers +can simulate shallow handlers up to administrative reductions. The +latter construction generalises the example of pipes implemented using +deep handlers that we gave in +Section~\ref{sec:pipes}. +% + +\section{Deep as shallow} +\label{sec:deep-as-shallow} + +\newcommand{\dstrans}[1]{\mathcal{S}\llbracket #1 \rrbracket} + +The implementation of deep handlers using shallow handlers (and +recursive functions) is by a direct local translation, similar to how +one would implement a fold (catamorphism) in terms of general +recursion. Each handler is wrapped in a recursive function and each +resumption has its body wrapped in a call to this recursive function. +% +Formally, the translation $\dstrans{-}$ is defined as the homomorphic +extension of the following equations to all terms. +\begin{equations} +\dstrans{\Handle \; M \; \With \; H} &=& + (\Rec~h~f.\ShallowHandle\; f\,\Unit \; \With \; \dstrans{H} h)\,(\lambda \Unit{}.\dstrans{M}) \\ +\dstrans{H}h &=& \dstrans{\hret}h \uplus \dstrans{\hops}h \\ +\dstrans{\{ \Return \; x \mapsto N\}} h &=& + \{ \Return \; x \mapsto \dstrans{N} \}\\ +\dstrans{\{ \ell \; p \; r \mapsto N_\ell \}_{\ell \in \mathcal{L}}} h &=& + \{ \ell \; p \; r \mapsto + \Let \; r \revto \Return \; \lambda x.h\,(\lambda \Unit{}.r\,x) \; \In \; + \dstrans{N_\ell} \}_{\ell \in \mathcal{L}} +\end{equations} + +% \paragraph{Example} We illustrate the translation $\dstrans{-}$ on the +% EXAMPLE handler from Section~\ref{sec:strategies} (recall that the +% variable $m$ is bound to the input computation). The example here is +% reproduced in ANF notation. +% \[ +% \ba{@{~}l@{~}l@{}l} +% &\mathcal{S}&\left\llbracket +% \ba[m]{@{~}l} +% \Handle\; m~\Unit\; \With\\ +% \quad +% \ba{@{}l@{~}c@{~}l} +% \Return~x &\mapsto& \Return\;x\\ +% \Move~\Record{\_;n}~resume &\mapsto& \Let\;y \revto ps~n\;\In\; resume~y +% \ea +% \ea\right\rrbracket =\\\\ +% & +% &\ba[m]{@{}l} +% \hspace{-1ex} +% \left( +% \ba[m]{@{~}l} +% \Rec~h~f. +% \ba[t]{@{~}l} +% \ShallowHandle\; f~\Unit\; \With\\ +% \quad +% \ba{@{}l@{~}c@{~}l} +% \Return~x &\mapsto& \Return\; x\\ +% \Move~\Record{\_;n}~resume &\mapsto&\\ +% \quad\ba[t]{@{~}l@{}} +% \Let\; r \revto \Return\; \lambda x. h (\lambda\Unit.resume~x)\;\In\\ +% \Let\; y \revto ps~n\; \In\; r~y +% \ea +% \ea +% \ea +% \ea\right)~(\lambda \Unit. m~\Unit) +% \ea +% \ea +% \]\\ + +\begin{theorem} +If $\Delta; \Gamma \vdash M : C$ then $\Delta; \Gamma \vdash +\dstrans{M} : C$. +\end{theorem} + +In order to obtain a simulation result, we allow reduction in the +simulated term to be performed under lambda abstractions (and indeed +anywhere in a term), which is necessary because of the redefinition of +the resumption to wrap the handler around its body. +% +Nevertheless, the simulation proof makes minimal use of this power, +merely using it to rename a single variable. +% +We write $R_{\mathrm{cong}}$ for the compatible closure of relation +$R$, that is the smallest relation including $R$ and closed under term +constructors for $\SCalc$. +%% , otherwise known as \emph{reduction up to +%% congruence}. + +\begin{theorem}[Simulation up to congruence] +If $M \reducesto N$ then $\dstrans{M} \reducesto_{\mathrm{cong}}^+ +\dstrans{N}$. +\end{theorem} + +\begin{proof} + By induction on $\reducesto$ using a substitution lemma. The + interesting case is $\semlab{Op}$, which is where we apply a single + $\beta$-reduction, renaming a variable, under the lambda abstraction + representing the resumption. +\end{proof} + +\section{Shallow as deep} + +\newcommand{\sdtrans}[1]{\mathcal{D}\llbracket #1 \rrbracket} + +Implementing shallow handlers in terms of deep handlers is slightly +more involved than the other way round. +% +It amounts to the encoding of a case split by a fold and involves a +translation on handler types as well as handler terms. +% +Formally, the translation $\sdtrans{-}$ is defined as the homomorphic +extension of the following equations to all types, terms, and type +environments. \begin{equations} -\inv{\{\Return\;x \mapsto M\}}\env - &=& \{\Return\;x \mapsto \inv{M}(\env \res \{x\})\} \\ -\inv{\{\ell\;x\;k \mapsto M\} \uplus H}\env - &=& \{\ell\;x\;k \mapsto \inv{M}(\env \res \{x, k\}\} \uplus \inv{H}\env \\ + \sdtrans{C \Rightarrow D} &=& + \sdtrans{C} \Rightarrow \Record{\UnitType \to \sdtrans{C}; \UnitType \to \sdtrans{D}} \medskip \\ + \sdtrans{\ShallowHandle \; M \; \With \; H} &=& + \ba[t]{@{}l} + \Let\;z \revto \Handle \; \sdtrans{M} \; \With \; \sdtrans{H} \; \In\\ + \Let\;\Record{f; g} = z \;\In\; + g\,\Unit + \ea \\ + \sdtrans{H} &=& \sdtrans{\hret} \uplus \sdtrans{\hops} \\ + \sdtrans{\{\Return \; x \mapsto N\}} &=& + \{\Return \; x \mapsto \Return\; \Record{\lambda \Unit.\Return\; x; \lambda \Unit.\sdtrans{N}}\} \\ + \sdtrans{\{\ell\; p\; r \mapsto N\}_{\ell \in \mathcal{L}}} &=& \{ + \bl + \ell\; p\; r \mapsto \\ + \quad \Let \;r \revto + \lambda x. \Let\; z \revto r\,x\; \In\; + \Let\; \Record{f; g} = z\; \In\; f\,\Unit + \; \In\\ + \quad \Return\;\Record{\lambda \Unit.\Let\; x \revto \Do\;\ell\,p\; \In\; r\,x; \lambda \Unit.\sdtrans{N}}\}_{\ell \in \mathcal{L}} + \el \end{equations} +% +Each shallow handler is encoded as a deep handler that returns a pair +of thunks. The first forwards all operations, acting as the identity +on computations. The second interprets a single operation before +reverting to forwarding. -Value terms and values -\begin{displaymath} -\ba{@{}c@{}} -\begin{eqs} -\inv{x}\env &=& \inv{v}, \quad \text{ if }\env(x) = v \\ -\inv{x}\env &=& x, \quad \text{ if }x \notin dom(\env) \\ -\inv{\lambda x^A.M}\env &=& \lambda x^A.\inv{M}(\env \res \{x\}) \\ -\inv{\Lambda \alpha^K.M}\env &=& \Lambda \alpha^K.\inv{M}\env \\ -\inv{\Record{}}\env &=& \Record{} \\ -\inv{\Record{\ell=V; W}}\env &=& \Record{\ell=\inv{V}\env; \inv{W}\env} \\ -\inv{(\ell\;V)^R}\env &=& (\ell\;\inv{V}\env)^R \\ -\end{eqs} -\quad -\begin{eqs} -\inv{\shk^A} &=& \lambda x^A.\inv{\shk}(\Return\;x) \\ -\inv{(\shk, \slk)^A} &=& \lambda x^A.\inv{\slk}(\inv{\shk}(\Return\;x)) \\ -\inv{(\env, \lambda x^A.M)} &=& \lambda x^A.\inv{M}(\env \res \{x\}) \\ -\inv{(\env, \Lambda \alpha^K.M)} &=& \Lambda \alpha^K.\inv{M}\env \\ -\inv{\Record{}} &=& \Record{} \\ -\inv{\Record{\ell=v; w}} &=& \Record{\ell=\inv{v}; \inv{w}} \\ -\inv{(\ell\;v)^R} &=& (\ell\;\inv{v})^R \\ -\end{eqs} \smallskip\\ -\inv{\Rec\,g^{A \to C}\,x.M}\env = \Rec\,g^{A \to C}\,x.\inv{M}(\env \res \{g, x\}) - = \inv{(\env, \Rec\,g^{A \to C}\,x.M)} \\ -\ea -\end{displaymath} +% \paragraph{Example} We demonstrate the translation $\sdtrans{-}$ on +% the $\Pipe$ handler from Section~\ref{sec:shallow-handlers-tutorial} +% (recall that the variables $c$ and $p$ are bound to the consumer and +% producer functions respectively). The example is reproduced in ANF +% notation. +% % +% \[ +% \ba{@{~}l@{~}l@{}l} +% &\mathcal{D}&\left\llbracket +% \ba[m]{@{~}l} +% \ShallowHandle\; c\,\Unit \;\With\; \\ +% \quad +% \ba[m]{@{}l@{~}c@{~}l@{}} +% \Return~x &\mapsto& \Return\; x \\ +% \Await~\Unit~resume &\mapsto& \Copipe\; \Record{resume; p} \\ +% \ea \\ +% \ea\right\rrbracket = \\ +% & +% &\ba[t]{@{~}l} +% \Let\; z \revto +% \ba[t]{@{~}l} +% \Handle\; c~\Unit \; \With\\ +% \quad \ba[m]{@{~}l} +% \ba[m]{@{~}l@{~}l} +% \Return~x &\mapsto \Return\; \Record{\lambda\Unit. \Return\; x; \lambda\Unit. \Return\;x}\\ +% \Await~\Unit~resume &\mapsto +% \ea\\ +% \qquad\ba[t]{@{~}l} +% \Let\;r \revto \lambda x.\Let\; z \revto resume~x\; +% \In\; \Let\; \Record{f; g} = z \;\In\; f~\Unit\; \In\\ +% \Return\;\Record{\lambda \Unit. \Let\; x \revto \Do\; \ell~p \;\In\; r~x; +% \lambda\Unit.\sdtrans{\Copipe}\Record{r; p}} +% \ea +% \ea +% \ea\\ +% \In\;\Let\;\Record{f; g} = z\; \In\; g~\Unit +% \ea +% \ea +% \] +% -\caption{Mapping from abstract machine configurations to terms.} -\label{fig:config-to-term} -\end{figure} +\begin{theorem} +If $\Delta; \Gamma \vdash M : C$ then $\sdtrans{\Delta}; +\sdtrans{\Gamma} \vdash \sdtrans{M} : \sdtrans{C}$. +\end{theorem} -\paragraph{Remark} If the main continuation is empty then the machine gets -stuck. This occurs when an operation is unhandled, and the forwarding -continuation describes the succession of handlers that have failed to -handle the operation along with any pure continuations that were -encountered along the way. -% -Assuming the input is a well-typed closed computation term $\typc{}{M - : A}{E}$, the machine will either not terminate, return a value of -type $A$, or get stuck failing to handle an operation appearing in -$E$. We now make the correspondence between the operational semantics -and the abstract machine more precise. +\newcommand{\admin}{admin} +\newcommand{\approxa}{\gtrsim} -\section{Correctness} -\label{subsec:machine-correctness} +As with the implementation of deep handlers as shallow handlers, the +implementation is again given by a local translation. However, this +time the administrative overhead is more significant. Reduction up to +congruence is insufficient and we require a more semantic notion of +administrative reduction. -Fig.~\ref{fig:config-to-term} defines an inverse mapping $\inv{-}$ -from configurations to computation terms via a collection of mutually -recursive functions defined on configurations, continuations, -computation terms, handler definitions, value terms, and values. +\begin{definition}[Administrative evaluation contexts] +An evaluation context $\EC$ is administrative, $\admin(\EC)$, iff +\begin{enumerate} +\item For all values $V$, we have: $\EC[\Return\;V] \reducesto^\ast + \Return\;V$ +\item For all evaluation contexts $\EC'$, operations $\ell \in BL(\EC) + \backslash BL(\EC')$, values $V$: % -We write $dom(\gamma)$ for the domain of $\gamma$ and $\gamma \res -\{x_1, \dots, x_n\}$ for the restriction of environment $\gamma$ to -$dom(\gamma) \res \{x_1, \dots, x_n\}$. +\[ + \EC[\EC'[\Do\;\ell\;V]] \reducesto^\ast \Let\; x \revto \Do\;\ell\;V \;\In\; \EC[\EC'[\Return\;x]]. +\] +\end{enumerate} +\end{definition} % -The $\inv{-}$ function enables us to classify the abstract machine -reduction rules by how they relate to the operational -semantics. +The intuition is that an administrative evaluation context behaves +like the empty evaluation context up to some amount of administrative +reduction, which can only proceed once the term in the context becomes +sufficiently evaluated. % -The rules (\mlab{Init}) and (\mlab{RetTop}) concern only initial -input and final output, neither a feature of the operational -semantics. +Values annihilate the evaluation context and handled operations are +forwarded. % -The rules (\mlab{AppCont^\depth}), (\mlab{Let}), (\mlab{Handle}), -and (\mlab{Forward}) are administrative in that $\inv{-}$ is invariant -under them. +%% The forwarding handler is a technical device which allows us to state +%% the second property in a uniform way by ensuring that the operation is +%% handled at least once. + +\begin{definition}[Approximation up to administrative reduction] +Define $\approxa$ as the compatible closure of the following inference +rules. % -This leaves $\beta$-rules (\mlab{AppClosure}), (\mlab{AppRec}), -(\mlab{AppType}), (\mlab{Split}), (\mlab{Case}), (\mlab{RetCont}), -(\mlab{RetHandler}), (\mlab{Do}), and (\mlab{Do^\dagger}), -each of which corresponds directly to performing a reduction in the -operational semantics. +\begin{mathpar} + \inferrule* + { } + {M \approxa M} + + \inferrule* + {M \reducesto M' \\ M' \approxa N} + {M \approxa N} + + \inferrule* + {\admin(\EC) \\ M \approxa N} + {\EC[M] \approxa N} +\end{mathpar} % -We write $\stepsto_a$ for administrative steps, $\stepsto_\beta$ for -$\beta$-steps, and $\Stepsto$ for a sequence of steps of the form -$\stepsto_a^* \stepsto_\beta$. +We say that $M$ approximates $N$ up to administrative reduction if $M +\approxa N$. +\end{definition} +% +Approximation up to administrative reduction captures the property +that administrative reduction may occur anywhere within a term. +% +The following lemma states that the forwarding component of the +translation is administrative. +\begin{lemma}\label{lem:sdtrans-admin} +For all shallow handlers $H$, the following context is administrative: +\begin{displaymath} +\Let\; z \revto + \Handle\; [~] \;\With\; \sdtrans{H}\; + \In\; + \Let\; \Record{f;\_} = z\; \In\; f\,\Unit. +\end{displaymath} +\end{lemma} -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 (\S\ref{subsec:terms}) -implements the top-level identity continuation. -\\ -\begin{theorem}[Simulation] -\label{lem:simulation} -If $M \reducesto N$, then for any $\conf$ such that $\inv{\conf} = -Id(M)$ there exists $\conf'$ such that $\conf \Stepsto \conf'$ and -$\inv{\conf'} = Id(N)$. -%% If $M \reducesto N$, then for any $\conf$ such that $\inv{\conf} = M$ -%% there exists $\conf'$ such that $\conf \Stepsto \conf'$ and -%% $\inv{\conf'} = N$. +\begin{theorem}[Simulation up to administrative reduction] +If $M' \approxa \sdtrans{M}$ and $M \reducesto N$ then there exists +$N'$ such that $N' \approxa \sdtrans{N}$ and $M' \reducesto^+ N'$. \end{theorem} - +% \begin{proof} -By induction on the derivation of $M \reducesto N$. +By induction on $\reducesto$ using a substitution lemma and +Lemma~\ref{lem:sdtrans-admin}. The interesting case is +$\semlab{Op^\dagger}$, which uses Lemma~\ref{lem:sdtrans-admin} to +approximate the body of the resumption up to administrative reduction. \end{proof} -\begin{corollary} -If $\typc{}{M : A}{E}$ and $M \reducesto^+ N \not\reducesto$, then $M -\stepsto^+ \conf$ with $\inv{\conf} = N$. -\end{corollary} - - -\part{Expressiveness} % \chapter{Computability, complexity, and expressivness} % \label{ch:expressiveness} % \section{Notions of expressiveness}