From e52bd8867fb64511b25815fe03dd4b2770108de3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Fri, 14 Feb 2020 17:33:44 +0000 Subject: [PATCH] Spell out bound labels. --- macros.tex | 1 + thesis.tex | 116 ++++++++++++++++++++++++++++++++++++++--------------- 2 files changed, 85 insertions(+), 32 deletions(-) diff --git a/macros.tex b/macros.tex index 84eab82..150f3c5 100644 --- a/macros.tex +++ b/macros.tex @@ -157,6 +157,7 @@ %% Defined-as equality %% \newcommand{\defas}[0]{\mathrel{\overset{\makebox[0pt]{\mbox{\normalfont\tiny\text{def}}}}{=}}} +\newcommand{\defnas}[0]{\mathrel{:=}} %% %% Partiality diff --git a/thesis.tex b/thesis.tex index 4c86b7b..81e4bc7 100644 --- a/thesis.tex +++ b/thesis.tex @@ -1553,9 +1553,9 @@ for handling return values and another for handling operations. \Handle \; \EC[\Do \; \ell \, V] \; \With \; H &\reducesto& N[V/p, \lambda y . \, \Handle \; \EC[\Return \; y] \; \With \; H/r], \\ \multicolumn{4}{@{}r@{}}{ - \hfill\ba[t]{@{~}r@{~}l} - \text{where}& \hell = \{ \ell \; p \; r \mapsto N \}\\ - \text{and} & \ell \notin \BL(\EC) + \hfill\ba[t]{@{~}r@{~}l} + \text{where}& \hell = \{ \ell \; p \; r \mapsto N \}\\ + \text{and} & \ell \notin \BL(\EC) \ea } \end{reductions}%}}% @@ -1565,40 +1565,83 @@ $H$ and substitutes $V$ for $x$ in the body $N$. % The rule \semlab{Op} handles an operation $\ell$, provided that the handler definition $H$ contains a corresponding operation clause for -$\ell$ and that $\ell$ does not appear in the bound labels of the -inner context $\EC$. The latter condition enforces that an operation -is always handled by the innermost suitable handler. To illustrate the -condition at work consider the following example. +$\ell$ and that $\ell$ does not appear in the \emph{bound labels} +($\BL$) of the inner context $\EC$. The bound label condition enforces +that an operation is always handled by the nearest enclosing suitable +handler. +% +Formally, we define the notion of bound labels, +$\BL : \EvalCat \to \LabelCat$, inductively over the structure of +evaluation contexts. +% +\begin{equations} +\BL([~]) &=& \emptyset \\ +\BL(\Let\;x \revto \EC\;\In\;N) &=& \BL(\EC) \\ +\BL(\Handle\;\EC\;\With\;H) &=& \BL(\EC) \cup \dom(H) \\ +\end{equations} +% +To illustrate the necessity of this condition consider the following +example with two nested handlers which both handle the same operation +$\ell$. % \[ \bl \ba{@{~}r@{~}c@{~}l} - H_{\mathsf{inner}} &\defas& \{\ell\;p\;r \mapsto r~42, \Return\;x \mapsto \Return~x\}\\ - H_{\mathsf{outer}} &\defas& \{\ell\;p\;r \mapsto r~0,\Return\;x \mapsto \Return~x \} + H_{\mathsf{inner}} &\defas& \{\ell\;p\;r \mapsto r~42; \Return\;x \mapsto \Return~x\}\\ + H_{\mathsf{outer}} &\defas& \{\ell\;p\;r \mapsto r~0;\Return\;x \mapsto \Return~x \} \ea\medskip\\ \Handle \; - \Handle\; \Do\;\ell~\Record{}\;\With\; H_{\mathsf{inner}}\; + \left(\Handle\; \Do\;\ell~\Record{}\;\With\; H_{\mathsf{inner}}\right)\; \With\; H_{\mathsf{outer}} - \reducesto^+ \Return\;42 + \reducesto^+ \begin{cases} + \Return\;42 & \text{Innermost}\\ + \Return\;0 & \text{Outermost} + \end{cases} \el \] % -Both handlers handle the operation $\ell$, however, due to the side -condition gets handled by $H_{\mathsf{inner}}$ rather than -$H_{\mathsf{outer}}$. Without the side condition reduction would have -been ambiguous. Thus the condition is necessary to ensure -deterministic reduction. +Without the bound label condition there are two possible results as +the choice of which handler to pick for $\ell$ is ambiguous, meaning +reduction would be nondeterministic. Conversely, with the bound label +condition we obtain that the above term reduces to $\Return\;42$, +because $\ell$ is bound in the computation term of the outermost +$\Handle$. +% -Formally, we define the notion of bound labels, -$\BL : \EvalCat \to \LabelCat$, inductively over the structure of -evaluation contexts. +We have made a conscious design decision by always selecting nearest +enclosing suitable handler for any operation. In fact, we have made +the \emph{only} natural and sensible choice as picking any other +handler than the nearest enclosing renders programming with effect +handlers anti-modular. Consider always selecting the outermost +suitable handler, then the meaning of closed program composition +cannot be derived from its immediate constituents. For example, +consider using integer addition as the composition operator to compose +the inner handle expression from above with a copy of itself. % -\begin{equations} -\BL([~]) &=& \emptyset \\ -\BL(\Let\;x \revto \EC\;\In\;N) &=& \BL(\EC) \\ -\BL(\Handle\;\EC\;\With\;H) &=& \BL(\EC) \cup \dom(H) \\ -\end{equations} +\[ + \bl + \dec{fortytwo} \defas \Handle\;\Do\;\ell~\Unit\;\With\;H_{\mathsf{inner}} \medskip\\ + \EC[\dec{fortytwo} + \dec{fortytwo}] \reducesto^+ \begin{cases} + \Return\; 84 & \text{when $\EC$ is empty}\\ + ?? & \text{otherwise} + \end{cases} + \el +\] +% +Clearly, if the ambient context $\EC$ is empty, then we can derive the +result by reasoning locally about each constituent separately and +subsequently add their results together to obtain the computation term +$\Return\;84$. However, if the ambient context is nonempty, then we +need to account for the possibility that some handler for $\ell$ could +occur in the context. For instance if +$\EC = \Handle\;[~]\;\With\;H_{\mathsf{outer}}$ then the result would +be $\Return\;0$, which we cannot derive locally from looking at the +constituents. Thus we argue that if we want programming to remain +modular and compositional, then we must necessarily always select the +nearest enclosing suitable handler to handle an operation invocation. % +\dhil{Effect forwarding (the first condition)} + The metatheoretic properties of $\BCalc$ transfer to $\HCalc$ with little extra effort, although we must amend the definition of @@ -1613,21 +1656,30 @@ getting stuck on an unhandled operation. \end{definition} % -% -\begin{theorem}[Subject Reduction] -If $\typ{\Gamma}{M : C}$ and $M \reducesto M'$, then -$\typ{\Gamma}{M' : C}$. +\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{theorem}[Type Soundness] - If $\typ{}{M : C}$, then either there exists $\typ{}{N : C}$ such - that $M \reducesto^+ N$ and $N$ is normal, or $M$ diverges. +% +\begin{theorem}[Preservation] + Suppose $\typ{\Gamma}{M : C}$ and $M \reducesto M'$, then + $\typ{\Gamma}{M' : C}$. \end{theorem} +\subsection{Coding nontermination} + +\subsection{Programming with deep handlers} +\dhil{Exceptions} +\dhil{Reader} +\dhil{State} +\dhil{Nondeterminism} + \section{Parameterised handlers} \label{sec:unary-parameterised-handlers} +\dhil{Example: Lightweight threads} + \section{Default handlers} \label{sec:unary-default-handlers}