WIP

thesis.bib

@@ -651,7 +651,8 @@
                Tom Schrijvers},
   title     = {Fusion for Free - Efficient Algebraic Effect Handlers},
   booktitle = {{MPC}},
-  series    = {Lecture Notes in Computer Science},
+  OPTseries    = {Lecture Notes in Computer Science},
+  series    = {LNCS},
   volume    = {9129},
   pages     = {302--322},
   publisher = {Springer},
@@ -874,7 +875,7 @@
                Mitchell Wand},
   title     = {Continuation Semantics in Typed Lambda-Calculi (Summary)},
   booktitle = {Logic of Programs},
-  series    = {Lecture Notes in Computer Science},
+  series    = {LNCS},
   volume    = {193},
   pages     = {219--224},
   publisher = {Springer},
@@ -992,6 +993,41 @@
   howpublished = {{ML Workshop}}
 }
 
+@article{DanvyH92,
+  author    = {Olivier Danvy and
+               John Hatcliff},
+  title     = {CPS-Transformation After Strictness Analysis},
+  journal   = {{LOPLAS}},
+  volume    = {1},
+  number    = {3},
+  pages     = {195--212},
+  year      = {1992}
+}
+
+@inproceedings{DanvyH93,
+  author    = {Olivier Danvy and
+               John Hatcliff},
+  title     = {On the Transformation between Direct and Continuation Semantics},
+  booktitle = {{MFPS}},
+  series    = {{LNCS}},
+  volume    = {802},
+  pages     = {627--648},
+  publisher = {Springer},
+  year      = {1993}
+}
+
+@article{Nielsen01,
+  author = {Lasse R. Nielsen},
+  title = {A Selective CPS Transformation},
+  journal   = {Electr. Notes Theor. Comput. Sci.},
+  volume = {45},
+  pages = {311-331},
+  year = {2001},
+  OPTnote = {MFPS 2001,Seventeenth Conference on the Mathematical Foundations of Programming Semantics},
+  OPTissn = {1571-0661},
+  OPTdoi = {https://doi.org/10.1016/S1571-0661(04)80969-1}
+}
+
 # Dynamic binding
 @inproceedings{KiselyovSS06,
   author    = {Oleg Kiselyov and
@@ -1891,7 +1927,7 @@
   author    = {John Longley},
   title     = {Some Programming Languages Suggested by Game Models (Extended Abstract)},
   booktitle = {{MFPS}},
-  series    = {Electronic Notes in Theoretical Computer Science},
+  journal   = {Electr. Notes Theor. Comput. Sci.},
   volume    = {249},
   pages     = {117--134},
   publisher = {Elsevier},
@@ -2185,7 +2221,7 @@
                David B. MacQueen},
   title     = {Standard {ML} of New Jersey},
   booktitle = {{PLILP}},
-  series    = {Lecture Notes in Computer Science},
+  series    = {{LNCS}},
   volume    = {528},
   pages     = {1--13},
   publisher = {Springer},
@@ -2198,7 +2234,7 @@
                David B. MacQueen},
   title     = {A Standard {ML} compiler},
   booktitle = {{FPCA}},
-  series    = {Lecture Notes in Computer Science},
+  series    = {{LNCS}},
   volume    = {274},
   pages     = {301--324},
   publisher = {Springer},
@@ -2209,7 +2245,7 @@
 # MLton
 @misc{Fluet20,
   author = {Matthew Fluet and others},
-  title  = {MLton Documentation},
+  title  = {{MLton} Documentation},
   year   = 2014,
   month  = jan
 }
@@ -2289,7 +2325,7 @@
   author    = {Olivier Danvy},
   title     = {A Rational Deconstruction of Landin's {SECD} Machine},
   booktitle = {{IFL}},
-  series    = {Lecture Notes in Computer Science},
+  series    = {{LNCS}},
   volume    = {3474},
   pages     = {52--71},
   publisher = {Springer},
@@ -2368,7 +2404,7 @@
                Yukiyoshi Kameyama},
   title     = {Polymorphic Delimited Continuations},
   booktitle = {{APLAS}},
-  series    = {Lecture Notes in Computer Science},
+  series    = {{LNCS}},
   volume    = {4807},
   pages     = {239--254},
   publisher = {Springer},
@@ -2489,7 +2525,7 @@
                Chung{-}chieh Shan},
   title     = {A Substructural Type System for Delimited Continuations},
   booktitle = {{TLCA}},
-  series    = {Lecture Notes in Computer Science},
+  series    = {{LNCS}},
   volume    = {4583},
   pages     = {223--239},
   publisher = {Springer},
@@ -2553,7 +2589,7 @@
                Chung{-}chieh Shan},
   title     = {Embedded Probabilistic Programming},
   booktitle = {{DSL}},
-  series    = {Lecture Notes in Computer Science},
+  series    = {{LNCS}},
   volume    = {5658},
   pages     = {360--384},
   publisher = {Springer},
@@ -2583,7 +2619,7 @@
                Chung{-}chieh Shan},
   title     = {Delimited Continuations in Operating Systems},
   booktitle = {{CONTEXT}},
-  series    = {Lecture Notes in Computer Science},
+  series    = {{LNCS}},
   volume    = {4635},
   pages     = {291--302},
   publisher = {Springer},
@@ -2675,7 +2711,7 @@
   title     = {Functional Programming with Bananas, Lenses, Envelopes and Barbed
                Wire},
   booktitle = {{FPCA}},
-  series    = {Lecture Notes in Computer Science},
+  series    = {{LNCS}},
   volume    = {523},
   pages     = {124--144},
   publisher = {Springer},

thesis.tex

@@ -2686,7 +2686,8 @@ continuations to represent strands of computation and timer interrupts
 to suspend continuations.
 %
 \citet{KiselyovS07a} used delimited continuations to explain various
-phenomena of operating systems, including multi-tasking.
+phenomena of operating systems, including multi-tasking and file
+systems.
 %
 On the web, \citet{Queinnec04} used continuations to model the
 client-server interactions. This model was adapted by
@@ -2696,6 +2697,12 @@ concurrency model~\cite{ArmstrongVW93}.
 \citet{Leijen17a} and \citet{DolanEHMSW17} gave two different ways of
 implementing the asynchronous programming operator async/await as a
 user-definable library.
+%
+In the setting of distributed programming, \citet{BracevacASEEM18}
+describe a modular event correlation system that makes crucial use of
+effect handlers.  \citeauthor{Bracevec19}'s PhD dissertation
+explicates the theory, design, and implementation of event correlation
+by way of effect handlers~\cite{Bracevec19}.
 
 Continuations have also been used in meta-programming to speed up
 partial evaluation and
@@ -3022,22 +3029,22 @@ Section~\ref{sec:base-language-type-rules}.
 % %\slab{Type variables} &\alpha, \rho, \theta& \\
 % \slab{Type environments} &\Gamma &::=& \cdot \mid \Gamma, x:A \\
 % \slab{Kind environments} &\Delta &::=& \cdot \mid \Delta, \alpha:K
-\slab{Value types}    &A,B \in \ValTypeCat  &::= & A \to C
+\slab{Value\mathrm{~}types}    &A,B \in \ValTypeCat  &::= & A \to C
                              \mid  \forall \alpha^K.C
                              \mid   \Record{R} \mid [R]
                              \mid  \alpha \\
-\slab{Computation types\!\!}
+\slab{Computation\mathrm{~}types\!\!}
                       &C,D \in \CompTypeCat   &::= & A \eff E \\
-\slab{Effect types}   &E \in \EffectCat   &::= & \{R\}\\
+\slab{Effect\mathrm{~}types}   &E \in \EffectCat   &::= & \{R\}\\
-\slab{Row types}      &R \in \RowCat      &::= & \ell : P;R \mid \rho \mid \cdot \\
+\slab{Row\mathrm{~}types}      &R \in \RowCat      &::= & \ell : P;R \mid \rho \mid \cdot \\
-\slab{Presence types\!\!\!\!\!} &P \in \PresenceCat  &::= & \Pre{A} \mid \Abs \mid \theta\\
+\slab{Presence\mathrm{~}types\!\!\!\!\!} &P \in \PresenceCat  &::= & \Pre{A} \mid \Abs \mid \theta\\
 \\
 \slab{Types}          &T \in \TypeCat    &::= & A \mid C \mid E \mid R \mid P \\
 \slab{Kinds}          &K \in \KindCat    &::= & \Type \mid \Comp \mid \Effect \mid \Row_\mathcal{L} \mid \Presence \\
-\slab{Label sets}     &\mathcal{L} \in \LabelCat &::=& \emptyset \mid \{\ell\} \uplus \mathcal{L}\\\\
+\slab{Label\mathrm{~}sets}     &\mathcal{L} \in \LabelCat &::=& \emptyset \mid \{\ell\} \uplus \mathcal{L}\\\\
 
-\slab{Type environments} &\Gamma \in \TyEnvCat   &::=& \cdot \mid \Gamma, x:A \\
+\slab{Type\mathrm{~}environments} &\Gamma \in \TyEnvCat   &::=& \cdot \mid \Gamma, x:A \\
-\slab{Kind environments} &\Delta \in \KindEnvCat &::=& \cdot \mid \Delta, \alpha:K \\
+\slab{Kind\mathrm{~}environments} &\Delta \in \KindEnvCat &::=& \cdot \mid \Delta, \alpha:K \\
 \end{syntax}
   \caption{Syntax of types, kinds, and their environments.}
   \label{fig:base-language-types}
@@ -4763,7 +4770,7 @@ computation normal forms as there are now two ways in which a
 computation term can terminate: successfully returning a value or
 getting stuck on an unhandled operation.
 %
-\begin{definition}[Computation normal forms]\ref{def:comp-normal-form}
+\begin{definition}[Computation normal forms]\label{def:comp-normal-form}
   We say that a computation term $N$ is normal with respect to an
   effect signature $E$, if $N$ is either of the form $\Return\;V$, or
   $\EC[\Do\;\ell\,W]$ where $\ell \in E$ and $\ell \notin \BL(\EC)$.
@@ -10649,11 +10656,12 @@ continuation argument per handler in scope~\cite{SchusterBO20}. The
 idea of iterated CPS is due to \citet{DanvyF90}, who used it to give
 develop a CPS transform for shift and reset.
 %
-\citet{XieBHSL20} has devised an \emph{evidence-passing translation}
+\citet{XieBHSL20} have devised an \emph{evidence-passing translation}
 for deep effect handlers. The basic idea is similar to
 capability-passing style as evidence for handlers are passed downwards
 to their operations in shape of a vector containing the handlers in
-scope through computations.
+scope through computations. \citet{XieL20} have realised handlers by
+evidence-passing style as a Haskell library.
 
 There are clear connections between the CPS translations presented in
 this chapter and the continuation monad implementation of
@@ -10730,7 +10738,10 @@ then in the image $\cps{M}\,k \reducesto^\ast k\,\cps{V}$.
 
 % \paragraph{Partial evaluation}
 
+\paragraph{ANF vs CPS}
+
 \paragraph{Selective CPS transforms}
+\citet{Nielsen01} \citet{DanvyH92} \citet{DanvyH93} \citet{Leijen17}
 
 \chapter{Abstract machine semantics}
 \label{ch:abstract-machine}
@@ -11349,7 +11360,7 @@ If $\typc{}{M : A}{E}$ and $M \reducesto^+ N \not\reducesto$, then $M
 
 
 \part{Expressiveness}
-\chapter{Interdefinability of deep and shallow handlers}
+\chapter{Interdefinability of effect handlers}
 \label{ch:deep-vs-shallow}
 
 In this section we show that shallow handlers and general recursion
@@ -11359,6 +11370,18 @@ latter construction generalises the example of pipes implemented using
 deep handlers that we gave in
 Section~\ref{sec:pipes}.
 %
+\paragraph{Relation to prior work} The results in this chapter has
+been published previously in the following papers.
+%
+\begin{enumerate}[i]
+    \item \bibentry{HillerstromL18}  \label{en:ch-def-HL18}
+    \item \bibentry{HillerstromLA20} \label{en:ch-def-HLA20}
+\end{enumerate}
+%
+The results of Sections~\ref{sec:deep-as-shallow} and
+\ref{sec:shallow-as-deep} appear in item \ref{en:ch-def-HL18}, whilst
+the result of Section~\ref{sec:param-desugaring} appear in item
+\ref{en:ch-def-HLA20}.
 
 \section{Deep as shallow}
 \label{sec:deep-as-shallow}
@@ -11373,18 +11396,34 @@ 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}) \\
+\bl
-\dstrans{H}h &=& \dstrans{\hret}h \uplus \dstrans{\hops}h \\
+  \dstrans{-} : \CompCat \to \CompCat\\
-\dstrans{\{ \Return \; x \mapsto N\}} h &=&
+  \dstrans{\Handle \; M \; \With \; H} \defas
+      (\Rec~h~f.\ShallowHandle\; f\,\Unit \; \With \; \dstrans{H}_h)\,(\lambda \Unit{}.\dstrans{M}) \medskip\\
+    % \dstrans{H}h &=& \dstrans{\hret}h \uplus \dstrans{\hops}h \\
+  \dstrans{-} : \HandlerCat \times \ValCat \to \HandlerCat\\
+  \ba{@{}l@{~}c@{~}l}
+    \dstrans{\{ \Return \; x \mapsto N\}}_h &\defas&
       \{ \Return \; x \mapsto \dstrans{N} \}\\
-\dstrans{\{ \ell \; p \; r \mapsto N_\ell \}_{\ell \in \mathcal{L}}} h &=&
+    \dstrans{\{ \OpCase{\ell}{p}{r} \mapsto N_\ell \}_{\ell \in \mathcal{L}}}_h &\defas&
-  \{ \ell \; p \; r \mapsto
+      \{ \OpCase{\ell}{p}{r} \mapsto
-      \Let \; r \revto \Return \; \lambda x.h\,(\lambda \Unit{}.r\,x) \; \In \;
+           \bl
-         \dstrans{N_\ell} \}_{\ell \in \mathcal{L}}
+             \Let \; r \revto \Return \; \lambda x.h\,(\lambda \Unit{}.r\,x)\\
-\end{equations}
+             \In\;\dstrans{N_\ell} \}_{\ell \in \mathcal{L}}
-
+           \el
+  \ea
+\el
+\]
+%
+The translation of $\Handle$ uses a $\Rec$-abstraction to introduce a
+fresh name $h$ for the handler $H$. This name is used by the
+translation of the handler definitions. The translation of
+$\Return$-clauses is the identity, and thus ignores the handler
+name. However, the translation of operation clauses uses the name to
+simulate a deep resumption by guarding invocations of the shallow
+resumption $r$ with $h$.
 % \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
@@ -11424,9 +11463,13 @@ extension of the following equations to all terms.
 % \]\\
 
 \begin{theorem}
-If $\Delta; \Gamma \vdash M : C$ then $\Delta; \Gamma \vdash
+If $\Delta; \Gamma \vdash M : C$ then $\dstrans{\Delta}; \dstrans{\Gamma} \vdash
-\dstrans{M} : C$.
+\dstrans{M} : \dstrans{C}$.
 \end{theorem}
+%
+\begin{proof}
+  By induction on typing derivations.
+\end{proof}
 
 In order to obtain a simulation result, we allow reduction in the
 simulated term to be performed under lambda abstractions (and indeed
@@ -11455,7 +11498,7 @@ If $M \reducesto N$ then $\dstrans{M} \reducesto_{\mathrm{cong}}^+
 \end{proof}
 
 \section{Shallow as deep}
-
+\label{sec:shallow-as-deep}
 \newcommand{\sdtrans}[1]{\mathcal{D}\llbracket #1 \rrbracket}
 
 Implementing shallow handlers in terms of deep handlers is slightly
@@ -11467,28 +11510,36 @@ 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 \\
+  \bl
-  \sdtrans{\ShallowHandle \; M \; \With \; H} &=&
+  \sdtrans{-} : \TypeCat \to \TypeCat\\
+  \sdtrans{C \Rightarrow D} \defas
+  \sdtrans{C} \Rightarrow \Record{\UnitType \to \sdtrans{C}; \UnitType \to \sdtrans{D}} \medskip \medskip\\
+  \sdtrans{-} : \CompCat \to \CompCat\\
+  \sdtrans{\ShallowHandle \; M \; \With \; H} \defas
       \ba[t]{@{}l}
       \Let\;z \revto \Handle \; \sdtrans{M} \; \With \; \sdtrans{H} \; \In\\
       \Let\;\Record{f; g} = z \;\In\;
       g\,\Unit
-      \ea \\
+      \ea \medskip\\
-  \sdtrans{H} &=& \sdtrans{\hret} \uplus \sdtrans{\hops} \\
+  \sdtrans{-} : \HandlerCat \to \HandlerCat\\
-  \sdtrans{\{\Return \; x \mapsto N\}} &=&
+  % \sdtrans{H} &=& \sdtrans{\hret} \uplus \sdtrans{\hops} \\
+  \ba{@{}l@{~}c@{~}l}
+    \sdtrans{\{\Return \; x \mapsto N\}} &\defas&
       \{\Return \; x \mapsto \Return\; \Record{\lambda \Unit.\Return\; x; \lambda \Unit.\sdtrans{N}}\} \\
-  \sdtrans{\{\ell\; p\; r \mapsto N\}_{\ell \in \mathcal{L}}} &=& \{
+      \sdtrans{\{\OpCase{\ell}{p}{r} \mapsto N\}_{\ell \in \mathcal{L}}} &\defas& \{
     \bl
-    \ell\; p\; r \mapsto \\
+    \OpCase{\ell}{p}{r} \mapsto\\
-    \quad \Let \;r \revto
+    \qquad\bl\Let \;r \revto
-       \lambda x. \Let\; z \revto r\,x\; \In\;
+       \lambda x. \Let\; z \revto r~x\;\In\;
-                  \Let\; \Record{f; g} = z\; \In\; f\,\Unit
+                  \Let\; \Record{f; g} = z\; \In\; f\,\Unit\;\In\\
-    \; \In\\
+       \Return\;\Record{\lambda \Unit.\Let\; x \revto \Do\;\ell~p\; \In\; r~x; \lambda \Unit.\sdtrans{N}}\}_{\ell \in \mathcal{L}}
-    \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}
+    \el
+    \ea
+    \el
+\]
 %
 Each shallow handler is encoded as a deep handler that returns a pair
 of thunks. The first forwards all operations, acting as the identity
@@ -11540,7 +11591,10 @@ reverting to forwarding.
 If $\Delta; \Gamma \vdash M : C$ then $\sdtrans{\Delta};
 \sdtrans{\Gamma} \vdash \sdtrans{M} : \sdtrans{C}$.
 \end{theorem}
-
+%
+\begin{proof}
+  By induction on typing derivations.
+\end{proof}
 
 \newcommand{\admin}{admin}
 \newcommand{\approxa}{\gtrsim}
@@ -11626,6 +11680,71 @@ $\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 as ordinary deep handlers}
+\label{sec:param-desugaring}
+\newcommand{\PD}[1]{\mathcal{P}\cps{#1}}
+%
+As mentioned in Section~\ref{sec:unary-parameterised-handlers},
+parameterised handlers codify the parameter-passing idiom. They may be
+seen as an optimised form of parameter-passing deep handlers. We now
+show formally that parameterised handlers are special instances of
+ordinary deep handlers.
+%
+We define a local transformation $\PD{-}$ which translates
+parameterised handlers into ordinary deep handlers. We omit the
+homomorphic cases and show only the interesting cases.
+%
+\[
+  \bl
+  \PD{-} : \TypeCat \to \TypeCat\\
+  \PD{\Record{C, A} \Rightarrow^\param B \eff E} \defas \PD{C} \Rightarrow (\PD{A} \to \PD{B \eff E})\eff \PD{E} \medskip\\
+  \PD{-} : \CompCat \to \CompCat\\
+  \PD{\ParamHandle\;M\;\With\;(q.\,H)(W)} \defas \left(\Handle\; \PD{M}\; \With\; \PD{H}_q\right)~\PD{W} \medskip\\
+  \PD{-} : \HandlerCat \times \ValCat \to \HandlerCat\\
+  \ba{@{}l@{~}c@{~}l}
+  \PD{\{\Return\;x \mapsto M\}}_q &\defas& \{\Return\;x \mapsto \lambda q. \PD{M}\}\\
+  \PD{\{\OpCase{\ell}{p}{r} \mapsto M\}}_q &\defas&
+      \{\OpCase{\ell}{p}{r} \mapsto \lambda q.
+        \Let\; r \revto \Return\;\lambda \Record{x,q'}. r~x~q'\;
+        \In\; \PD{M}\}
+  \ea
+ \el
+\]
+%
+The parameterised $\ParamHandle$ construct becomes an application of a
+$\Handle$ construct to the translation of the parameter. The bodies of
+return and operation clauses are each enclosed in a lambda abstraction
+whose formal parameter is the handler parameter $q$. As a result the
+ordinary deep resumption $r$ is a curried function. However, the uses
+of $r$ in $M$ expects a binary function. To repair this discrepancy,
+we construct an uncurried interface of $r$ via the function $r'$.
+
+\begin{theorem}
+If $\Delta; \Gamma \vdash M : C$ then $\PD{\Delta};
+\sdtrans{\Gamma} \vdash \PD{M} : \PD{C}$.
+\end{theorem}
+%
+\begin{proof}
+  By induction on typing derivations.
+\end{proof}
+
+This translation of parameterised handlers simulates the native
+semantics. As with the simulation of deep handlers via shallow
+handlers in Section~\ref{sec:deep-as-shallow}, this simulation is only up
+to congruence due to the need for an application of a pure function to
+a variable to be reduced. The interesting cases of the proof appear in
+Appendix~\ref{sec:param-proof}.
+
+\begin{theorem}[Simulation of parameterised handlers by deep
+  handlers]
+  \label{thm:param-simulation}
+  If $M \reducesto N$ then $\PD{M} \reducesto^+_{\mathrm{cong}} \PD{N}$.
+\end{theorem}
+
+\section{Related work}
+
+\citet{ForsterKLP17,ForsterKLP19} \citet{PirogPS19}, \citet{Shan04}
+
 % \chapter{Computability, complexity, and expressivness}
 % \label{ch:expressiveness}
 % \section{Notions of expressiveness}