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.
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.
Chung-chieh Shan. Slides of the ICFP 2006 Presentation, Sep 18, 2006.
< http://www.cs.rutgers.edu/~ccshan/dynscope/talk.pdf >
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.
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.
Mechanising dynamic binding
A message posted on the POPLmark mailing list on Wed Sep 20 14:43:52 EDT 2006
< http://lists.seas.upenn.edu/pipermail/poplmark/2006-September/000368.html >
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
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.
DB calculus, simply typed lambda-calculus with dynamic binding.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.
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.
oleg-at-okmij.org
Your comments, problem reports, questions are very welcome!
Converted from HSXML by HSXML->HTML