Delimited Continuations

In this essay, I will examine three different approaches to delimited continuations in three different languages: Rompf et al. [6] (Scala), Kiselyov [3] (OCaml), and Phipps-Costin et al. [5] (Wasm). By comparing and contrasting their designs and then implementations, I will consider two questions:

1. What factors influence design decisions?
2. How should we evaluate the quality of an implementation?

Designing an Interface

First, I consider the design of delimited continuations in each of the three papers. I argue that interface design is affected by (at least) three stakeholders – end-users, designers, and implementers – whose interests may not always align.

The interface for delimited continuations presented by Rompf et al. is similar to that in lecture. The key difference is that they are typed. The type of \(\mathcal{S} k. e\) is \((A \rightarrow B) \rightarrow C\). \(A \rightarrow B\) is the type of the continuation, and \(C\) the type returned by \(e\). Concretely, in the following example, \(A = \texttt{int}\), \(B = \texttt{int}\), and \(C = \texttt{int list}\).

\[ \langle (\mathcal{S} k: \texttt{int} \rightarrow \texttt{int}. (k \, 0) :: []) + 1\rangle: \texttt{int list} \]

Notice that \(B = \texttt{int} \neq \texttt{int list} = C\). Evaluating \(e\) changes the answer type of the entire expression. This answer-type modification complicates type-checking. As an additional source of complexity, many use-cases require answer-type polymorphism. Consider:

\[ \lambda x: \alpha. \langle \mathcal{S} k. (k \, x) :: (k \, [x]) \rangle \]

Answer type modification is a relative notion. The first application (\(k \, x\)) modifies the original answer type of the (identity) continuation from \(\alpha\) to \(\alpha \texttt{ list}\). However, the second application does not modify the original answer type of the continuation \(\beta (= \alpha \texttt{ list})\). This is answer-type polymorphism.

The interfaces presented by Kiselyov and Phipps-Costin et al. are not so familiar. Kiselyov’s [3] interface differs from the traditional \(\mathcal{S}\) and \(\langle \rangle\) operators in three key ways:

First, rather than having a single \(\mathcal{S}\) (correspondingly \(\langle \rangle\)), Kiselyov introduces multiple “colours” of \(\mathcal{S}\), dynamically generated via new_prompt. A coloured \(\mathcal{S}\) thus captures the continuation up to the nearest delimiter of the same colour. In the following example, the captured continuation \(k\) is \(\ca{\langle} \cdot + 1\ca{\rangle} + 1\):

\[ \cb{\langle} \ca{\langle} (\cb{\mathcal{S}} k. (k \; 0)) + 1 \ca{\rangle} + 1 \cb{\rangle} \]

These control delimiters are not allowed to modify their answer type. In OCaml, the syntax for \(\langle e \rangle\) is push_prompt \(p\) \(e\) where \(p\) is a coloured \(\langle \rangle\).

The second difference is that we can implement multiple control reifiers (\(\mathcal{S}, \mathcal{F}_0\), etc). Control reifiers are implemented by two operations: take_subcont and push_subcont. To implement \(\mathcal{F}_0 k. k \; 0\), we write

take_subcont p (fun k -> push_subcont k (fun () -> 0))

To implement \(\mathcal{S} k. e\), we write

let shift e = take_subcont p (fun cont () ->
  push_prompt p (fun () ->
    e (fun v ->
      push_prompt p (fun () ->
        push_subcont cont (fun () -> v)))))

A final difference is in spirit. Throughout the paper, Kiselyov separates the control reifier from its handler. That is, rather than writing

let e = take_subcont p (fun k () ->
  push_subcont k (fun () -> 0))

we instead write

let e' = take_subcont p (fun k () -> HandleMe(k)) in
match push_prompt p (Done(fun () -> e')) with
 | Done -> 1
 | HandleMe(k) -> push_subcont k (fun () -> 0)

This associates the handler with the delimiter (push_prompt), rather than the control reifier (take_subcont), thus more closely resembling algebraic effects.

Phipps-Costin et al., in contrast, force handlers to be associated with delimiters rather than reifiers. Apart from this change, their design corresponds closely to Kiselyov’s.

The WasmFX explainer [8] motivates their design by appealing to human-centric factors. Each “colour” of handler can be assigned a different purpose, creating loci on which to attach semantic meaning. By associating the handler with the delimiter, they further claim to create a “separation of concerns” [8]. Extending this argument, I note that if there is only a single handler instance for each colour, as is the case for many of the “key use cases” [5], then the design coincides with named handlers [10].

In contrast, Kiselyov and Rompf et al. do not justify their designs from a user-centric perspective. Kiselyov seems to suggest that his design is usable, pointing to “fruitful practical use”. Conversely, the usability of Rompf’s approach has been subjected to retrospective criticism. Rompf’s implementation relies on a source-to-source transform, which Pham and Odersky [4] critique as being “unfriendly” to debugging.

Beyond the end-user, designs are additionally shaped by language designers. Existing language designs may aid, or hinder, particular modifications. The designs of both Kiselyov and Phipps-Costin et al. avoid answer-type polymorphism. Scala accommodates answer-type polymorphism by offering a “pluggable” type system, where separate type systems may be substituted into the compiler. In addition, its object-oriented sub-typing seems to naturally lend itself to checking the “compatibility” of answer types. OCaml and Wasm are not so accommodating. Designers of Wasm would also have to modify the formal specification, and the formal proofs [9] (though it is unclear how significant the modifications need be).

The implementers of the language also shape language design. Their influence is visible in WasmFX’s lack of support for multi-shot continuations.^[1] Many different engines run Wasm. These present a barrier to change for WasmFX. For example, multi-shot continuations necessitate some form of stack copying. However, some engines mix Wasm and C++ stack frames, and only the Wasm frames should be copied. Similarly, multi-shot continuations can create heap cycles, but some engines do not have garbage collectors [5].

Do the demands of implementers conflict with the demands of users? Phipps-Costin et al. argue that, at present, they are aligned. While applications like “probabilistic programming” cannot be supported, these are not “key use cases”. This statement deserves further scrutiny. Phipps-Costin et al. never clarify how these key use cases were determined (by users, or implementers?). Further, even if the statement is currently valid, this may be a poor predictor for future needs of users: the “next 700” features which WasmFX tries to anticipate. One might argue that the lack of named handlers is similarly myopic. Indeed, probabilistic programming is the second use case mentioned by Kiselyov. The question of how WasmFX will navigate competing demands remains, to me, unanswered.

Implementing Delimited Continuations

I now pivot from the design to the implementation of delimited continuations, focusing on OCaml and Scala.

The heart of Rompf’s [6] Scala implementation is a static type-system that supports answer-type modification and polymorphism. Such support requires static identification of the continuation \(k\), which in turn depends on an explicit notion of the evaluation order.

Implementation is aided by the choice of \(\mathcal{S}\) and \(\langle \rangle\), since they give us strong guarantees over behaviour under composition. Consider

\[ \langle e_1 \rangle + \langle e_2 \rangle \]

Since \(\mathcal{S}\) always retains its enclosing \(\langle \rangle\), no \(\mathcal{S}\) in \(e_1\) can capture any sub-continuation of \(\cdot + \langle e_2 \rangle\). Additionally, consider

\[ \langle \mathcal{S} k. (k v) + 1\rangle \]

Since \(\mathcal{S}\) always installs a new delimiter when applying \(k\), any \(\mathcal{S}\) arising from the evaluation of \((k v)\) will never capture the \(\cdot+1\).

In effect, we can analyse \(\mathcal{S}\) statically, within local sub-expressions. This allows a simple translation into continuation-passing style, where delimiters translate into applications of identity continuations [1]. When written in this style, the evaluation order is explicit. This makes it easier to identify the captured continuation \(k\), and check the compatibility of answer-types.

As formulated, this approach requires either user re-writes or source-to-source translation of the program into CPS. The former places too much burden on the user. The latter might not be performant: bypassing the stack leads to a run-time cost [6]. To address the first concern, Rompf et al. automatically perform CPS-conversion. To assuage the second, a type-and-effect system leverages the static characteristics of \(\mathcal{S}\) and \(\langle \rangle\) to precisely detect the need for CPS-conversion. This CPS-converts a minimal amount of code, reducing overheads. Rompf et al. subject their implementation to three benchmarks, illustrating that it can outperform efficient contemporaries on a range of “representative” tasks.

Two critiques can be levelled. First, we should be careful not to over-generalise their Scala-centric assessment. Different languages have different contexts-of-use, which could result in very different “representative” benchmarks and/or evaluation criteria. For example, WasmFX has a different set of use cases, and thus a different set of benchmarks [5]. Further, the WasmFX designers are willing to trade longer run times for smaller binary sizes [5]. Second, the authors should perhaps have been more concerned with maintainability: “The plugin was […] discontinued because nobody was volunteering to maintain it” [7]. Its longevity relied, perhaps unrealistically, on a separate type system being evolved and maintained parallel to Scala.

Rather than modifying the existing language, Kiselyov’s OCaml implementation conforms to it. Built as a library, it requires no changes to the run-time, and is compatible with existing OCaml code. Kiselyov claims that Delimcc is both popular and long-lived.

To make this work, Kiselyov’s implementation appropriates existing OCaml machinery. Examples include

1. Leveraging OCaml’s exception-handling for delimiters and control reifiers, and
2. Using existing run-time mechanisms for coping with stack overflow, accessed via the foreign function interface, for copying sub-stacks.

To what extent was this retro-fitting successful? I argue that it is tremendously so, though with a wart: building \(\mathcal{S}\) (or \(\mathcal{S}_0\)) out of the given primitives triggers a memory leak!

The problem is that before a stack fragment can be copied, dirty registers must be flushed to it. Kiselyov achieves this by sandwiching stack fragments between two anonymous delimiters. Since delimiters are exception frames at the low-level, this has the desired behaviour. Consequently, composing push_prompt and take_subcont results in an unnecessary accumulation of anonymous delimiters. Users are thus advised to use push_delim_subcont. Implementation details have leaked out of the clean abstraction [3].

Perhaps unsurprisingly, I find Kiselyov’s techniques more ad-hoc and less principled than Rompf’s. The results are also less elegant, and less robustly defended. However, given the constraints, it is arguably more surprising that the quality of implementation is even comparable. Further, Kiselyov’s implementation continues to serve users today. On this basis, I rank Kiselyov’s implementation above Rompf’s.

Longevity is not our only metric. Kiselyov invites us to critique his implementation on its transferability: as a scheme for retro-fitting delimited continuations onto languages. This claim is supported by implementations in Scheme and Haskell [2].

I find two reasons to be sceptical. First, it is unclear if all languages supporting exceptions and recovery from stack overflow support his approach. Phipps-Costin et al. argue that “most languages, like [C, C++, and Wasm]”, do not. Second, even if Kiselyov’s approach is possible, might the outcomes be drastically different? Beyond implementation, Kiselyov’s design decisions are also shaped by OCaml. For example, \(\mathcal{S}k.e\) inherits the typing rules for exceptions. Would another language that types exceptions differently force (or allow) an alternate design? To facilitate detailed description of his implementation, Kiselyov pays little attention to different design decisions. It is unclear how far one can, or needs to, deviate from his recipe.

Rompf et al. and Kiselyov’s [3] implementations raise questions about how an implementation should be evaluated. Performance is tied to the context-of-use, and secondary to factors like longevity. If the techniques used are transferable, an implementation gains additional value: but it is difficult to provide a recipe that is both detailed yet flexible.

References

1. [1] O. Danvy and A. Filinski. Abstracting control. In Proceedings of the 1990 ACM Conference on LISP and Functional Programming, pages 151–160. 1990. doi.org/10.1145/91556.91622
2. [2] O. Kiselyov. Implementing delimited control. okmij.org/ftp/continuations/implementations.html
3. [3] O. Kiselyov. Delimited control in OCaml, abstractly and concretely. Theoretical Computer Science, 435, pages 56–76. 2012. doi.org/10.1016/j.tcs.2012.02.025
4. [4] C. N. Pham and M. Odersky. Stack-Copying Delimited Continuations for Scala Native. In Proceedings of the 19th ACM International Workshop on Implementation, Compilation, Optimization of OO Languages, Programs and Systems, pages 2–13. 2024. doi.org/10.1145/3679005.3685979
5. [5] L. Phipps-Costin, A. Rossberg, A. Guha, D. Leijen, D. Hillerström, K. C. Sivaramakrishnan, M. Pretnar, and S. Lindley. Continuing WebAssembly with Effect Handlers. arXiv:2308.08347. 2023. arxiv.org/abs/2308.08347
6. [6] T. Rompf, I. Maier, and M. Odersky. Implementing first-class polymorphic delimited continuations by a type-directed selective CPS-transform. SIGPLAN Not., 44(9), pages 317–328. 2009. doi.org/10.1145/1631687.1596596
7. [7] Delimited continuations. 2019. contributors.scala-lang.org/t/delimited-continuations/3485
8. [8] Explainer document | WasmFX: Effect Handlers for WebAssembly. wasmfx.dev/specs/explainer/
9. [9] C. Watt. Mechanising and verifying the WebAssembly specification. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 53–65. 2018. doi.org/10.1145/3167082
10. [10] N. Xie, Y. Cong, K. Ikemori, and D. Leijen. First-class names for effect handlers. Proc. ACM Program. Lang., 6(OOPSLA2). 2022. doi.org/10.1145/3563289