Notes on escape

thesis.bib

@@ -1798,6 +1798,36 @@
   year   = 2020
 }
 
+# Gauche
+@misc{Kawai20,
+  author = {Shiro Kawai},
+  title  = {{Gauche} Users' Reference (version 0.9.9)},
+  year   = 2019
+}
+
+# OchaCaml
+@inproceedings{MasukoA11,
+  author    = {Moe Masuko and Kenchi Asai},
+  title     = {{Caml} {Light} + shift/reset = {Caml} {Shift}},
+  booktitle = {Theory and Practice of Delimited Continuations ({TPDC})},
+  year      = 2011,
+  pages     = {33--46}
+}
+
+# Shift/reset in Scala
+@inproceedings{RompfMO09,
+  author    = {Tiark Rompf and
+               Ingo Maier and
+               Martin Odersky},
+  title     = {Implementing first-class polymorphic delimited continuations by a
+               type-directed selective CPS-transform},
+  booktitle = {{ICFP}},
+  pages     = {317--328},
+  publisher = {{ACM}},
+  year      = {2009}
+}
+
+
 # First implementation of threads using continuations
 @InProceedings{Burstall69,
   author    = {Rod M. Burstall},
@@ -1854,4 +1884,29 @@
   title  = {MLton Documentation},
   year   = 2014,
   month  = jan
-}
+}
+
+# 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}
+}

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
@@ -1088,21 +1163,39 @@ implementation strategies.
 
 \begin{table}
   \centering
-  \begin{tabular}{| l | >{\raggedright}p{4.5cm} | l |}
+  \begin{tabular}{| l | >{\raggedright}p{4.3cm} | l |}
     \hline
     \multicolumn{1}{|c|}{\textbf{Language}} & \multicolumn{1}{c |}{\textbf{Control operators}} & \multicolumn{1}{c|}{\textbf{Implementation strategies}}\\
     \hline
+    Eff      & Effect handlers & Virtual machine, interpreter \\
+    \hline
+    Effekt   & Lexical effect handlers & ??\\
+    \hline
+    Frank    & N-ary effect handlers & Abstract machine \\
+    \hline
+    Gauche   & callcc, shift/reset & Virtual machine \\
+    \hline
+    Helium   & Effect handlers & CEK machine \\
+    \hline
+    Koka     & Effect handlers & Continuation monad\\
+    \hline
     Links    & Effect handlers, escape & CEK machine, CPS\\
     \hline
     MLton    & callcc & Stack copying\\
     \hline
-    Multicore OCaml  & Effect handlers & Segmented stacks\\
+    Multicore OCaml  & Affine effect handlers & Segmented stacks\\
     \hline
-    Racket & callcc, callcc$^{\ast}$, fcontrol, prompt/control, shift/reset, splitter, spawn & Continuation marks\\
+    OchaCaml & shift/reset & Virtual machine\\
     \hline
-    Rhino JavaScript      & A variation of J  & Interpreter \\
+    Racket & callcc, callcc$^{\ast}$, cupto, fcontrol, prompt/control, shift/reset, splitter, spawn & Continuation marks\\
     \hline
-    SML/NJ                & callcc       & CPS\\
+    Rhino JavaScript      & JI                & Interpreter \\
+    \hline
+    Scala                 & shift/reset       & CPS\\
+    \hline
+    SML/NJ                & callcc            & CPS\\
+    \hline
+    Wasm/k                & prompt/control    & ?? \\
     \hline
   \end{tabular}
   \caption{Some languages and  their implementation strategies for first-class control.}\label{tbl:ctrl-operators-impls}