Home

Delimited Control in OCaml, Abstractly and Concretely, System Description

Delimited Control in OCaml, Abstractly and Concretely, System Description

We describe the first implementation of multi-prompt delimited control operators in OCaml that is direct in that it captures only the needed part of the control stack. The implementation is a library that requires no changes to the OCaml compiler or run-time, so it is perfectly compatible with existing OCaml source code and byte-code. The library has been in fruitful practical use for four years.

We present the library as an implementation of an abstract machine derived by elaborating the definitional machine. The abstract view lets us distill a minimalistic API, scAPI, sufficient for implementing multi-prompt delimited control. We argue that a language system that supports exception and stack-overflow handling supports scAPI. Our library illustrates how to use scAPI to implement multi-prompt delimited control in a typed language. The approach is general and can be used to add multi-prompt delimited control to other existing language systems.

Oleg was kind enough to send me an e-mail letting me know of this paper's existence (it appears not yet to be linked from the "Computation" page under which it is stored) and to include me in the acknowledgements. Since the paper in its current form has been accepted for publication, he indicated that it can be made more widely available, so here it is. In typical Oleg fashion, it offers insights at both the theoretical and implementation levels.

By Paul Snively at 2010-01-25 17:27 | Cross language runtimes | Functional | Implementation | Semantics | Type Theory | other blogs | 8570 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Relation to Flatt 07?

I'm rather surprised that this paper doesn't even discuss Flatt et al's ICFP 07 paper, which also provides a production implementation of multi-prompt delimited control, in PLT Scheme.

By Sam Tobin-Hochstadt at Mon, 2010-01-25 18:51 | login or register to post comments

Different Issues

Off the cuff, it seems that [Flatt et al. 2007] treats a different set of issues, such as how to cleanly integrate delimited continuations with call/cc, dynamic-wind, dynamic binding, and PLT Scheme's exceptions, and specifically in the untyped realm of Scheme. While the PLT team is absolutely to be commended for making all that happen and giving it a formal treatment, it's not clear that there that much overlap with Oleg's approach that originated with OCaml, which lacks call/cc, dynamic-wind, and dynamic binding but is statically typed. The fact that the derived API was also implemented in R5RS Scheme is, IMHO, intriguing, and it would be informative to compare the results to PLT Scheme's. But it's still derived from the distinct approach taken with OCaml rather than other Scheme implementations.

All of this is, of course, only my educated guess. Oleg participates here himself, so he could, of course, provide direct information.

By Paul Snively at Tue, 2010-01-26 14:22 | login or register to post comments