Home

Delimited dynamic binding

We are seeking comments on the final draft of our ICFP 2006 paper: Delimited dynamic binding, by Oleg Kiselyov, Chung-chieh Shan, and Amr Sabry.

Dynamic binding and delimited control are useful together in many settings, including Web applications, database cursors, and mobile code. We examine this pair of language features to show that the semantics of their interaction is ill-defined yet not expressive enough for these uses.

We solve this open and subtle problem. We formalise a typed language DB+DC that combines a calculus DB of dynamic binding and a calculus DC of delimited control. We argue from theoretical and practical points of view that its semantics should be based on delimited dynamic binding: capturing a delimited continuation closes over part of the dynamic environment, rather than all or none of it; reinstating the captured continuation supplements the dynamic environment, rather than replacing or inheriting it. We introduce a type- and reduction-preserving translation from DB+DC to DC, which proves that delimited control macro-expresses dynamic binding. We use this translation to implement DB+DC in Scheme, OCaml, and Haskell.

We extend DB+DC with mutable dynamic variables and a facility to obtain not only the latest binding of a dynamic variable but also older bindings. This facility provides for stack inspection and (more generally) folding over the execution context as an inductive data structure.

The paper comes with a large amount of accompanying code—in Scheme, OCaml, SML, and Haskell. The code (described in the paper's appendix) uses realistic examples to show how the joint behavior of delimited continuations and dynamic binding is ill-defined in various PL systems, and solves the problem by a full-fledged implementation of dynamic binding in all these systems. Any comments or suggestions would be very welcome!
By Chung-chieh Shan at 2006-06-22 22:15 | Functional | Semantics | other blogs | 14274 reads

Comment viewing options

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

Um...

<neo>Whoa.</neo>

By Paul Snively at Fri, 2006-06-23 03:08 | login or register to post comments

Is the code available?

The current paper refers to source code on the web, but the address it gives is for the paper itself. I think I've put together a working Haskell version, based on the O'Caml in the paper and the delimited continuations library, but I haven't managed to implement the 'dupp' operator properly.

It's interesting how close dnew, dref, and dset are to newIORef, readIORef, and writeIORef.

How much trouble would it cause Haskell if delimited continuations were useable in pure code? I'm guessing there would be order-of-evaluation concerns, but I don't grasp the issues well enough to say for certain.

By Dave Menendez at Fri, 2006-06-23 20:37 | login or register to post comments

Quite a lot, I suspect

I saw that delimited continuation break referential transparency by recalling that they can be used to express state. If anything, I think the trend in Haskell goes the other way, with work on dependent types and Curry-Howard suggesting that even nontermination should be excluded from pure code.

Trying to integrate continuations into a language without a deterministic evaluation order seems very tricky. You might be able to salvage things with some kind of nondeterministic semantics, like exceptions in Haskell, or with coherence conditions.

I've suspected for a while it was impossible to build a monad offering mutable references at arbitrary types on pure Haskell. I'm impressed to see it done. Is there a simpler implementation if you just want to provide variables?

By Brandon Moore at Fri, 2006-06-23 22:25 | login or register to post comments

Ref. transparency, delim. cont., capabilities

Referential transparency, in a nutshell, says that a `meaning' (e.g.,
reductions) of a term does not depend on its context. 0+42 reduced to 42
no matter where in the large computation that expression appears.

Capturing a first-class continuation, OTH, lets an expression get
hold of its context. That offers a general way to implement
context-sensitive reductions and terms with context-sensitive meaning.
An example of such terms in a natural language are the phrases with
pronouns or quantifiers like `everyone'. Chung-chieh Shan's thesis
elucidates these connections and discusses them in great detail.


http://www.eecs.harvard.edu/~ccshan/dissertation/book.pdf

Multi-prompt delimited continuation add a greatly important
restriction on the free-wheeling call/cc. An expression may capture its
delimited continuation only if it possesses the corresponding
prompt. The prompts are unforgeable -- and act as
capabilities.

By Oleg at Sat, 2006-06-24 00:05 | login or register to post comments

Mutable references and multiple prompts

I've suspected for a while it was impossible to build a monad offering mutable references at arbitrary types on pure Haskell. I'm impressed to see it done.
Actually, we didn't do it—The implementation of multi-prompt delimited control in Haskell uses ST internally. Oh well!
By Chung-chieh Shan at Sat, 2006-06-24 19:46 | login or register to post comments

Open unions and multiple prompts

Thanks for everyone's comments. We have posted the final version of the paper at the same address.

Oleg and I would like to clarify the comment above a bit. Storage cells for mutable state, prompts for delimited control, and variants of a union data-type are profoundly related. Thus it is no accident that delimited control with an arbitrary number of prompts can be implemented in terms of mutable state with an arbitrary number of storage cells, as well as vice versa as our paper shows, be it in Haskell or in OCaml. Gunter et al implement multiprompt delimited control using ML's extensible datatype of exceptions.

By Chung-chieh Shan at Tue, 2006-06-27 19:02 | login or register to post comments

Code is available

Yes, all of the code is available online:


http://pobox.com/~oleg/ftp/packages/DBplusDC.tar.gz

The OCaml and Haskell code needs delimited continuations libraries,
which are available from the same site. They are excluded from
DBplusDC.tar.gz for the sake of avoiding code duplication. OTH, the
Scheme implementation of Dybvig, Sabry, Peyton-Jones framework, with
an additional twist, is included in the code. It is R5RS plus
SRFI-9-like records. That implementation is the base for parameter
objects -- with exactly the same interface as Petite Chez's native
facility.

By Oleg at Sat, 2006-06-24 00:03 | login or register to post comments

Presentation and formalization

Chung-chieh Shan's ICFP06 talk gives a gentler introduction to both
dynamic binding and delimited continuations, along with their
surprising interactions. The talk contains many pictures of the
(delimited) `stack':


http://www.eecs.harvard.edu/~ccshan/dynscope/talk.pdf

The slides also hint at applications of delimited continuations in
linguistics.

One of the languages of the paper -- simply-typed lambda-calculus with
(mutable) dynamic binding (language DB) -- has been formalized in Twelf,
with its type safety formally proven:


http://pobox.com/~oleg/ftp/Computation/dynamic-binding.html#DB-formalization

This is a rare formalization of mutable variables that uses
no explicit state.

By Oleg at Mon, 2006-10-09 01:31 | login or register to post comments

Linkrot

The talk is now at a different location: http://www.cs.rutgers.edu/~ccshan/dynscope/talk.pdf

By Manuel J. Simoni at Wed, 2011-08-03 11:51 | login or register to post comments