previous  next  contents  top

Dynamic binding, binding evaluation contexts, and (delimited) control effects


Following Moreau (HOSC 1998), we call a dynamic variable a variable whose association with a value exists only within the dynamic extent of an expression, that is, while control remains within that expression. If several associations exist for the same variable at the same time, the latest one takes effect. Such association is called a dynamic binding. The expression dynamic scope is convenient to refer to the indefinite scope of a variable with a dynamic extent. Examples of dynamic variables include exception handlers, stdin, and hostname (for mobile code). Given this abstract specification, dynamic binding can be implemented in many ways: by adding an environment argument to each function (so-called environment-passing style), using global mutable cells (shallow binding), and so on.

Dynamic variables are also called `fluid variables' or `parameters'. For history, terminology, and thorough motivation of dynamic binding, please see
   Luc Moreau: A Syntactic Theory of Dynamic Binding. Higher-Order and Symbolic Computation, 11, 233-279 (1998).

This is joint work with Chung-chieh Shan and Amr Sabry.


Delimited Dynamic Binding

[The Abstract of the paper]

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 formalize 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:

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.

This paper answers Moreau's call for ``a single framework integrating continuations, side-effects, and dynamic binding''. Our delimited dynamic binding is a new and useful form of abstraction -- over parts of the dynamic environment, just as lambda lets us abstract over parts of the lexical environment.

The current version is 1.1, Jul 2006.
DDBinding.pdf [269K]
``Delimited Dynamic Binding.'' Proceedings of the ICFP 2006, pp. 26-37.

Chung-chieh Shan. Slides of the ICFP 2006 Presentation, Sep 18, 2006.
< >

DBplusDC.tar.gz [25K]
DBplusDC-README.txt [5K]
The code accompanying the paper
The archive includes numerous examples (in various Scheme systems and SML) illustrating the ill-defined interaction between dynamic variables and shift/reset. The code includes implementations -- in OCaml, Scheme and Haskell -- of dynamic binding in terms of delimited continuations, which is consistent with the combined context-reduction semantics of DB+DC . A separate, Scheme48-specific code implements delimited continuations (shift/reset) that are aware of dynamic-wind and dynamic-environment.
Please see the README file for the full description.


Mutable bindings in evaluation contexts: formalization of dynamic binding

We demonstrate a mechanized formalization of mutable dynamic binding in a direct-style semantics, without environment- or state-passing but relying instead on the evaluation context to play the prominent double role of the dynamic environment.

Our language is DB (as defined in Figure 1 and Section 2 of the `Delimited Dynamic Binding' paper), which is a simply-typed lambda-calculus with mutable dynamically-scoped variables. The language is based on Moreau's syntactic theory of dynamic binding, to which we added a sound type system. Our formalization of type safety uses the reduction semantics exactly as published by Moreau, Figure 6 of his paper. Our type system is conventional, except that judgments are parameterized by a signature Sigma, which associates every dynamic variable with its type. This type system does not prevent access to an unbound dynamic variable, which matches the existing practice.

Our Twelf code closely follows the small-step approach of `Syntactic Approach to Type Soundness' with contexts, focusing and redexing. Evaluation contexts are modeled as meta-level functions. The notable complication is that contexts and pre-values are mutually dependent, and so the pre-val and focus functions are mutually recursive. Another complication is that our type system specifically lets a well-typed expression try to access an unbound dynamic variable, resulting in an error. This reflects the behavior of most real systems that use dynamic variables. We have to model this error behavior and account for it in our progress proofs.

Our formalization points out a deep similarity between lexical variables in the typing context and dynamic (mutable) variables in the evaluation context.

The current version is 1.2, Sep 20, 2006.
db-lang.elf [23K]
The commented Twelf code

Mechanising dynamic binding
A message posted on the POPLmark mailing list on Wed Sep 20 14:43:52 EDT 2006
< >


Haskell's `implicit parameters' are not dynamically scoped

Implicit parameters of Haskell are often regarded as similar to dynamically scoped variables, such as `special' variables of Common Lisp, current-input-port of Scheme, stdin, and exception handlers in many languages. It is important to realize however that implicit parameters lack truly dynamic scope, as the following code illustrates.
     (let ((p (make-parameter #f)))
       (let ((x
               (parameterize ((p 1))
                 (lambda () (+ (p) 1)))))
         (parameterize ((p 2)) (x))))
This scheme code uses parameter objects, SRFI-39, which are natively implemented in some Scheme systems. The code evaluates to 3. The equivalent Haskell code
     let x = (let ?p = 1 in (\ () -> ?p + 1)) in let ?p = 2 in x()
yields the value 2
The current version is Spring 2005.


Simply typed lambda-calculus with dynamic binding is not strongly normalizing

Simply typed lambda-calculus has strong normalization property: the sequence of reductions of any term terminates. If we add (typed) dynamic variables, however, as in the language DB above, the strong normalization property no longer holds. Indeed, the following term (written with OCaml dynamic binding library) is essentially fun () -> Omega: its inferred type is unit -> 'a, and consequently, the evaluation of loop () loops forever.

     let loop () =
       let p = dnew () in
       let delta () = dref p () in
       dlet p delta delta

This term constitutes probably the simplest proof of the result, shown in a different setting by Moreau, that dynamic binding brings new expressiveness to the language.

The current version is September 29, 2006.
Delimited Dynamic Binding
The paper that introduced the DB calculus, simply typed lambda-calculus with dynamic binding.


Printing the outline of a pruned tree

This practical problem has been posed by the LtU user `rici' as follows: ``You have a labeled tree

     type 'a tree = 
        Leaf of string * 'a | Branch of string * 'a tree list
that might correspond to a normal file system... where the leaves are files and the branches are directories. You are to produce an outline view of this tree, showing only those leaves which satisfy some predicate function and the branches necessary to reach those leaves.... I find this problem interesting, in part because it is practical (my original implementation was to produce a view of an Apache configuration file showing only directives which pertained to a given module)...''

We show the solution to this problem in Theta(tree-depth) space using dynamic binding with the extension to access the previous binding of a dynamic variable. This extension dupp is the part of our dynamic binding library for OCaml, Haskell, and Scheme. It lets us fold over the execution context as an inductive data structure.

The current version is December 6, 2006.
References [5K]
The commented OCaml code, with examples and the test run output at the end.

Delimited Dynamic Binding
The description of our extended dynamic binding library, and its source code. The dupp extension is described in Section 6.2 of the paper and illustrated in the `nub' example.

Last updated January 1, 2007

This site's top page is
Your comments, problem reports, questions are very welcome!

Converted from HSXML by HSXML->HTML