diff --git a/thesis.bib b/thesis.bib index de66362..07a1950 100644 --- a/thesis.bib +++ b/thesis.bib @@ -1884,4 +1884,29 @@ title = {MLton Documentation}, year = 2014, month = jan -} \ No newline at end of file +} + +# Comparison of control operators via double barrelled CPS +@article{Thielecke02, + author = {Hayo Thielecke}, + title = {Comparing Control Constructs by Double-Barrelled {CPS}}, + journal = {High. Order Symb. Comput.}, + volume = {15}, + number = {2-3}, + pages = {141--160}, + year = {2002} +} + +# Comparison of effect handlers and shift/reset in a polymorphic type system +@inproceedings{PirogPS19, + author = {Maciej Pir{\'{o}}g and + Piotr Polesiuk and + Filip Sieczkowski}, + title = {Typed Equivalence of Effect Handlers and Delimited Control}, + booktitle = {{FSCD}}, + series = {LIPIcs}, + volume = {131}, + pages = {30:1--30:16}, + publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, + year = {2019} +} diff --git a/thesis.tex b/thesis.tex index 2c72b28..c264be3 100644 --- a/thesis.tex +++ b/thesis.tex @@ -542,6 +542,26 @@ wide range of control operators from the literature. % callcc is a procedural variation of catch. It was invented in % 1982~\cite{AbelsonHAKBOBPCRFRHSHW85}. +A full formal comparison of the control operators is out of scope of +this chapter. The literature contains comparisons of various control +operators along various dimensions, e.g. +% +\citet{Thielecke02} studies a handful of operators via double +barrelled continuation passing style. \citet{ForsterKLP19} compare the +relative expressiveness of untyped and simply-typed variations of +effect handlers, shift/reset, and monadic reflection by means of +whether they are macro-expressible. Their work demonstrates that in an +untyped setting each operator is macro-expressible, but in most cases +the macro-translations do not preserve typeability, for instance the +simple type structure is insufficient to type the image of +macro-translation between effect handlers and shift/reset. +% +However, \citet{PirogPS19} show that with a polymorphic type system +the translation preserve typeability. +% +\citet{Shan04} shows that dynamic delimited control and static +delimited control is macro-expressible in an untyped setting. + \section{Notions of continuations} % \citeauthor{Reynolds93} has written a historical account of the @@ -712,6 +732,46 @@ and callcc turned out to be essentially the same operator. statement-oriented control mechanisms such as jumps and labels programmable in an expression-oriented language. % +The operator introduces a new computation form. +% +\[ + M, N \in \CompCat ::= \cdots \mid \Escape\;k\;\In\;M +\] +% +The variable $k$ is called the \emph{escape variable} and it is bound +in $M$. The escape variable exposes the current continuation of the +$\Escape$-expression to the programmer. The captured continuation is +abortive, thus an invocation of the escape variable in the body $M$ +has the effect of performing a non-local exit. +% + +In terms of jumps and labels the $\Escape$-expression can be +understood as corresponding to a kind of label and an application of +the escape variable $k$ can be understood as corresponding to a jump +to the label. + +\citeauthor{Reynolds98a}' original treatise of escape was untyped, and +as such, the escape variable could escape its captor, e.g. +% +\[ + \Let\;k \revto (\Escape\;k\;\In\;k)\;\In\; N +\] +% +Here the current continuation, $N$, gets bound to $k$ in the +$\Escape$-expression, which returns $k$ as-is, and thus becomes +available for use within $N$. \citeauthor{Reynolds98a} recognised the +power of this idiom and noted that it could be used to implement +coroutines and backtracking~\cite{Reynolds98a}. +% +In our simply-typed setting it is not possible for the continuation to +propagate outside its binding $\Escape$-expression as it would require +the addition of either recursive types or some other escape hatch like +mutable reference cells. +% + +The typing of $\Escape$ and $\Continue$ reflects that the captured +continuation is abortive. +% \begin{mathpar} \inferrule* {\typ{\Gamma,k : \Cont\,\Record{A;\Zero}}{M : A}} @@ -722,11 +782,23 @@ programmable in an expression-oriented language. {\typ{\Gamma}{\Continue~W~V : \Zero}} \end{mathpar} % +The return type of the continuation object can be taken as a telltale +sign that an invocation of this object never returns, since there are +no inhabitants of the empty type. +% +An invocation of the continuation discards the invocation context and +plugs the argument into the captured context. +% \begin{reductions} \slab{Capture} & \EC[\Escape\;k\;\In\;M] &\reducesto& \EC[M[\cont_{\EC}/k]]\\ \slab{Resume} & \EC[\Continue~\cont_{\EC'}~V] &\reducesto& \EC'[V] \end{reductions} % +The \slab{Capture} rule leaves the context intact such that if the +body $M$ does not invoke $k$ then whatever value $M$ reduces is +plugged into the context. The \slab{Resume} discards the current +context $\EC$ and installs the captured context $\EC'$ with the +argument $V$ plugged in. \paragraph{Sussman and Steele's catch} % @@ -852,7 +924,7 @@ the correspondence between labels and J. \[ \ba{@{}l@{~}l} &\sembr{\keyw{begin}\;s_1;\;\keyw{goto}\;L;\;L:\,s_2\;\keyw{end}}\\ - =& \lambda\Unit.\Let\;L \revto \J\,\sembr{s_2}\;\In\;\Let\;\Unit \revto \sembr{s_1}\,\Unit\;\In\;L\,\Unit + =& \lambda\Unit.\Let\;L \revto \J\,\sembr{s_2}\;\In\;\Let\;\Unit \revto \sembr{s_1}\,\Unit\;\In\;\Continue~L\,\Unit \ea \] % @@ -894,7 +966,7 @@ However, if $g$ does apply its argument, then the value provided to the application becomes the return value of $\dec{f}$, e.g. % \[ - \dec{f}~(\lambda return.return~\False) \reducesto^+ \False + \dec{f}~(\lambda return.\Continue~return~\False) \reducesto^+ \False \] % The function argument provided to $\J$ can intuitively be thought of @@ -945,9 +1017,12 @@ instead with the $\J$-argument $W$ applied to the value $V$. Let us end by remarking that the J operator is expressive enough to encode a familiar control operator like $\Callcc$. +% \[ \Callcc \defas \lambda f. f\,(\J\,(\lambda x.x)) \] +% + \subsection{Delimited operators} Delimited control: Control delimiters form the basis for delimited