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), algebraic effects, 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)
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.
This is joint work with Chung-chieh Shan and Amr Sabry.
DDBinding.pdf [269K]
Delimited Dynamic Binding.
Proceedings of the ICFP 2006, pp. 26-37.
Dynamic variables plus Delimited Control: ill-defined and unexpected
(Delimited) Dynamically scoped variables in OCaml post 5.0
in terms of algebraic effects
cc-ref.scm [6K]
cc-ref-tests.scm [5K]
Delimited continuation interface
of Dybvig, Sabry, Peyton-Jones, realized in R5RS + records
Only Scheme48 so far provides the necessary operations (capturing and splicing) on its native dynamic environment.
new-shift.scm [10K]
Scheme48-specific code. It implements
shift/reset that now behaves as expected in DB+DC, with respect to
Scheme48's native dynamic variables and dynamic-wind.
The extension can be implemented specifically: for example, if dynamic binding is realized by the environment-passing translation, the capturing and restoring is straightforward. If dynamic binding is done in terms delimited control or algebraic effects, effects can also be used to capture the environment. Capturing and re-instating can also be implemented using the ordinary dynamic binding, generically.
Applications:
dynvar_ext.mli [<1K]
dynvar_ext.ml [2K]
Capturing and re-instating the dynamic environment, generically.
vdynvar_ext.ml [4K]
The test code, which also
demonstrates a sample application: implementing lexical binding
in terms of dynamic binding.
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.
pruned-tree-outline.ml [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.
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.
Joint work with Chung-chieh Shan.
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
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.
Reader. We illustrate various interactions of the monad transformer
ReaderT with the (delimited) continuation monad transformer. We
observe that certain frequently occurring code patterns cannot be
expressed at all with the monad transformer mechanism because no
(static) combination of ReaderT and CC layers does the job.
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.
Delimited Dynamic Binding
The paper that introduced the DB
calculus, simply typed lambda-calculus with dynamic binding.