diff --git a/macros.tex b/macros.tex index cf51537..d0968ed 100644 --- a/macros.tex +++ b/macros.tex @@ -27,6 +27,7 @@ \newcommand{\HSCalc}{\ensuremath{\lambda_{\mathsf{h^\delta}}}\xspace} \newcommand{\EffCalc}{\ensuremath{\lambda_{\mathsf{eff}}}\xspace} \newcommand{\UCalc}{\ensuremath{\lambda_{\mathsf{u}}}\xspace} +\newcommand{\param}{\ensuremath{\ddagger}} %% %% Calculi terms and types type-setting. @@ -36,6 +37,7 @@ \newcommand{\dec}[1]{\mathsf{#1}} \newcommand{\keyw}[1]{\mathbf{#1}} \newcommand{\Handle}{\keyw{handle}} +\newcommand{\ParamHandle}{\Handle^\param} \newcommand{\ShallowHandle}{\ensuremath{\keyw{handle}^\dagger}} \newcommand{\With}{\keyw{with}} \newcommand{\Let}{\keyw{let}} diff --git a/thesis.tex b/thesis.tex index 13ed26c..4a0d1bb 100644 --- a/thesis.tex +++ b/thesis.tex @@ -2997,7 +2997,7 @@ evaluation of the stateful fragment of $m$ to continue. \subsubsection{Basic sequential file system} % -\begin{figure} +\begin{figure}[t] \centering \begin{tabular}[t]{| l |} \hline @@ -3007,11 +3007,11 @@ evaluation of the stateful fragment of $m$ to continue. \hline \strlit{ritchie.txt}\tikzmark{ritchie}\\ \hline - \multicolumn{1}{| c |}{$\cdots$}\\ + \multicolumn{1}{| c |}{$\vdots$}\\ \hline \strlit{stdout}\tikzmark{stdout}\\ \hline - \multicolumn{1}{| c |}{$\cdots$}\\ + \multicolumn{1}{| c |}{$\vdots$}\\ \hline \strlit{act3}\tikzmark{act3}\\ \hline @@ -3025,7 +3025,7 @@ evaluation of the stateful fragment of $m$ to continue. \hline 2\tikzmark{hamletino}\\ \hline - \multicolumn{1}{| c |}{$\cdots$}\\ + \multicolumn{1}{| c |}{$\vdots$}\\ \hline 1\tikzmark{stdoutino}\\ \hline @@ -3039,7 +3039,7 @@ evaluation of the stateful fragment of $m$ to continue. \hline \tikzmark{hamletdr}\strlit{To be, or not to be...}\\ \hline - \multicolumn{1}{| c |}{$\cdots$}\\ + \multicolumn{1}{| c |}{$\vdots$}\\ \hline \tikzmark{ritchiedr}\strlit{UNIX is basically...}\\ \hline @@ -3057,9 +3057,50 @@ evaluation of the stateful fragment of $m$ to continue. \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} +% +A file system provide an abstraction over primary storage in a +computer system. This abstraction facilities allocation, deletion, +storage, and access of files. +% +A typical \UNIX{} file system is hierarchical and +distinguishes between ordinary files, directories, and special +files~\cite{RitchieT74}. To simplify matters, our file system will be +entirely flat and only contain ordinary files. Although, the system +can readily be extended to be hierarchical, it comes at the expense of +extra complexity, that blurs rather than illuminates the model. +% +An ordinary file is a sequence of characters, or a simply a string in +our setting. +% -\begin{figure} +Figure~\ref{fig:unix-mappings} depicts some example mappings from the +directory into the i-list, and from there into the data region. + +Mathematically, the mapping from i-list to the data region is a +partial bijection. + +% +\[ + \ba{@{~}l@{\qquad}c@{~}l} + \dec{Directory} \defas \List~\Record{\String;\Int} &&% + \dec{DataRegion} \defas \List~\Record{\Int;\UFile} \smallskip\\ + \dec{INode} \defas \Record{loc:\Int;lno:\Int} &&% + \dec{IList} \defas \List~\Record{\Int;\dec{INode}} + \ea +\] +% +\[ + \dec{FileSystem} \defas \Record{ + \ba[t]{@{}l} + dir:\dec{Directory},ilist:\dec{IList},dreg:\dec{DataRegion},\\ + dnext:\Int,inext:\Int} + \ea +\] + + + +\begin{figure}[t] \centering \begin{tikzpicture}[node distance=4cm,auto,>=stealth'] \node[] (server) {\bfseries Bob (server)}; @@ -3350,21 +3391,6 @@ evaluation of the stateful fragment of $m$ to continue. % \subsection{Coding nontermination} -\section{Parameterised handlers} -\label{sec:unary-parameterised-handlers} - -\subsection{Syntax and static semantics} -\subsection{Dynamic semantics} - -\subsection{Lightweight concurrency} - -\begin{example}[Green threads] - \dhil{Example: Lightweight threads} -\end{example} - -% \section{Default handlers} -% \label{sec:unary-default-handlers} - \section{Shallow handlers} \label{sec:unary-shallow-handlers} @@ -3381,6 +3407,394 @@ evaluation of the stateful fragment of $m$ to continue. bar \end{example} +\section{Interdefinability of deep and shallow handlers} +\label{sec: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:shallow-handlers-tutorial}. +% + +\subsection{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} + +\subsection{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} + \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} + +In Section~\ref{sec:state} we informally presented parameterised +handlers as a useful idiom for handling stateful computations. We now +consider parameterised handlers as a primitive in $\HCalc$, and show +how to extend the CPS and abstract machine implementations to support +them. We also show that parameterised handlers can always be simulated +by deep handlers. + +\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 \{ \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 = \{ \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}