We demonstrate how lexical binding can be realized in terms of
dynamic binding. Therefore, higher-order lexically scoped functions
can be introduced into an existing first-order language as is, without
re-writing its compiler/interpreter to deal with the variable binding
environment. The approach works for strict and lazy evaluation, and is
particularly instructive for delimited dynamic binding. Applications
involve extensible interpreters and compilers, and staging.

- Introduction
- Sample languages
- Implementation: first-order fragment
- Dynamic binding
- Pure let-binding is dynamic binding
- Higher-order functions: variable capture
- Capturing dynamic environment
- Call-by-name and call-by-need
- Call-by-need via delimited continuations
- Conclusions
- Free Variables and Free Effects

- The most familiar, explained in any textbook approach to dealing with
variable references in higher-order programs is variable binding
environment: an association of variable names with their bound
values. In an interpreter (the
`eval`

function), the environment is one of its arguments. Compiled functions receive the environment as an extra argument. Terms with variables are commonly thought to mean functions from the environment to the value domain.This article demonstrates a different, unconventional approach to variable references, coming from the observation that a (let-)bound variable can only be used while the control remains within the corresponding let-expression body. In interpreter terms, a variable may be accessed only while the interpreter is still handling the let-form, which remains on the interpreter stack. Therefore, to find the value associated with the bound variable we search the stack -- or, better, just point to the right place on the stack that stores that value.

That is a very attractive idea, which seems first to come to mind when implementing higher-order languages. It was indeed first that came to mind to J. McCarthy and A. Turing. Alas, the idea -- now called dynamic binding -- is flawed (as Turing soon realized). To regard functions as first-class, to be able to pass them as arguments and return as results, lexical binding is indispensable.

This article demonstrates that, perhaps surprisingly, lexical binding can be implemented via dynamic binding, in strict and lazy settings.

The main advantage of this alternative approach is making variables a

*modular*feature: variables and (first-class) functions can be introduced to a first-order language without any changes to the latter, without any need to re-write the interpretation of the first-order fragment (numbers, strings, etc.) to pass the environment. We may write extensible interpreters and compilers. Another application is the surprisingly simple implementation of staging.Dynamic binding can be implemented in many ways. One particular implementation, in terms of delimited control, turns out particularly insightful. Incidentally, it demonstrates the need for multi-shot (non-affine) delimited continuations -- perhaps the first non-trivial use of such delimited continuations aside from non-determinism.

Another insight is that a let-expression -- often considered a mere syntax sugar in lambda calculus -- turns out more fundamental than the lambda abstraction.

**References**- lexdyn.ml [20K]

The complete code accompanying the article, with many tests and examples

- To make the point we introduce a progression of (simply typed)
languages, starting from the basic and adding more and more features. We shall
see that their implementations are just as extensible.
We implement the languages by writing their interpreters -- several, in fact, for various evaluation strategies -- in OCaml. It helps therefore to embed the languages in OCaml as DSLs. We will be using tagless-final embedding, as more illuminating and easier to extend. The latter is particularly important: the extensibility of implementations is one of the main points.

The base language is the simplest first-order language with integers and integer operations, as well as applications (of built-in functions, since there is no way to define functions yet.) As a tagless-final DSL, the language (its operations -- syntax -- and the types) are described by the following OCaml signature.

module type fo = sig type 'a exp (* expressions *) val int : int -> int exp (* integer literals *) val ( + ) : int exp -> int exp -> int exp val ( - ) : int exp -> int exp -> int exp val (//) : ('a -> 'b) exp -> 'a exp -> 'b exp (* application, left-assoc *) end

A DSL expression of type

`t`

is represented by an OCaml expression of (an abstract) type`t exp`

. For example, an OCaml expression`int 1`

represents DSL's integer literal`1`

. Here is a (OCaml representation) of a more elaborate DSL expression:let exfo = int 1 + int 2 - int 3 - int 4

Applications are denoted by the (left-associative) operator`//`

. Built-in functions are easy to add but they will not be needed for our examples.The second language,

`fol`

, extends`fo`

with definitions: let-expressions and variables:module type fol = sig include fo type 'a var val newvar : string -> 'a var val var : 'a var -> 'a exp val let_ : 'a var -> 'a exp -> (unit -> 'b exp) -> 'b exp end

The type`'a var`

describes variables, created by`newvar`

from an unlimited supply. The first argument of`var`

is the name, used only for tracing, which is quite useful especially for call-by-need later on. Variables per se are*not*expressions: use`var`

to reference them (which may, and actually will be, an effectful operation). The body of a let-expression is a thunk: the timing of its evaluation is controlled by`let_`

.A sample

`fol`

term may look as follows:let x = newvar "x" let y = newvar "y" let exfol = let_ x (int 10 - int 5) @@ fun () -> let_ y (int 1 + var x) @@ fun () -> let_ x (var x + var y) @@ fun () -> var x + var y

The first two lines create the variables for use in`exfol`

. (Hereafter we assume that all variables appearing in examples have been created similarly).Finally, we make the language higher-order by adding first-class functions, built by lambda-expressions:

module type ho = sig include fol val lam : 'a var -> (unit -> 'b exp) -> ('a -> 'b) exp end

For example, an anonymous function of adding two to its argument is represented as`lam x (fun () -> x + int 2)`

.Here are a few sample expressions using all

`ho`

facilities, including those inherited from`fo`

and`fol`

:let ex0 = (lam x @@ fun () -> let_ y (var x + var x) @@ fun () -> var y + var y) // int 10 let ex1 = (lam x @@ fun () -> let_ y (var x + var x) @@ fun () -> lam z @@ fun () -> var z + (var z + (var y + var y))) // (int 10 - int 5) // (int 20 - int 10) let exd = let_ h (lam f @@ fun () -> let_ x (int 10) @@ fun () -> var f // var x) @@ fun () -> let_ x (int 1) @@ fun () -> var h // (lam y (fun () -> var x + var y))

The last example,`exd`

, deliberately uses the same variable`x`

in different contexts, to highlight the difference between lexical and dynamic bindings.

- We will be writing many interpreters of our DSLs, starting with
`fo`

in this section. For a tagless-final DSL, an interpreter is not a single (`eval`

) function; rather, it is a realization of the`fo`

signature, showing the implementation (interpretation, or, denotation) of each expression form of the DSL.We chose the simplest, meta-circular interpreter, which interprets the

`fo`

DSL as a subset of OCaml. Therefore, the type`t exp`

is realized as`t`

, DSL integer literals are OCaml integers, DSL addition and subtraction are OCaml addition and subtraction (modulo printing the trace), DSL application is the OCaml application. Other interpreters are possible: pretty-printer or code generator.module FO = struct type 'a exp = 'a let int : int -> int exp = Fun.id let ( + ) : int exp -> int exp -> int exp = fun x y -> Printf.printf "Adding %d and %d\n" x y; x + y let ( - ) : int exp -> int exp -> int exp = fun x y -> Printf.printf "Subtracting %d and %d\n" x y; x - y let (//) : ('a -> 'b) exp -> 'a exp -> 'b exp = (@@) end

Thus defined

`FO`

can be immediately used to evaluate the sample term`exfo`

, producing`-4`

and printing the trace of additions and subtractions.

- As remarked earlier, dynamic binding is first to come to mind when
thinking of variables. It can be described by the following operations:
module type dynbind = sig type 'a dynvar val dnew : ?init:'a -> unit -> 'a dynvar val dlet : 'a dynvar -> 'a -> (unit -> 'w) -> 'w val dref : 'a dynvar -> 'a end

The operation`dnew`

creates a new dynvar: dynamically-bound variable, possibly with the default value. The operation`dlet`

, having received a dynvar, a value and a thunk, evaluates the thunk in the dynamic environment extended with the binding of the given value to the given dynvar. Finally,`dref`

obtains the value associated with the dynvar by the closest dynamically-enclosing dlet (or the default value, if it was specified and the variable is not bound).There are several implementations of this signature. The simplest uses reference cells: so-called `shallow binding'.

module DBShallow = struct type 'a dynvar = 'a option ref let dnew : ?init:'a -> unit -> 'a dynvar = fun ?init () -> ref init let dlet : 'a dynvar -> 'a -> (unit -> 'w) -> 'w = fun dv e body -> let vold = !dv in dv := Some e; match body () with | r -> dv := vold; r | exception e -> dv := vold; raise e let dref : 'a dynvar -> 'a = function | {contents = Some x} -> x | _ -> failwith "unbound dynamic variable" end

One may also implement dynamic binding via delimited control -- so-called delimited dynamic binding (

`DDB`

). In this implementation, dereferencing a dynvar is literally reaching back to the place on the evaluation stack that stores the bound value (as part of the`dlet`

stack frame). Finally, dynamic binding is what's called a `reader effect', and may be implemented with any algebraic effect facility (e.g., `one-shot' algebraic effects of OCaml 5). **References**- Delimited Dynamic Binding

- Let us turn to the language
`fol`

, which extends`fo`

with variables and let-expressions. A variable may only be accessed while in scope of the let-expression that bound it. In`fol`

, the scope of a let-expression -- when control remains within its body -- cannot be interrupted, captured or resumed. Therefore, lexical scope and dynamic scope coincide, and we may use dynamic binding to implement let-expressions and variables. The advantage of dynamic binding is that it may added modularly to an existing language without any changes to the latter -- as we now demonstrate.The interpreter of

`fol`

is a proper extension of`FO`

, including it as is and adding the interpretation of the new facilities: variables and binding:module FOL(D:dynbind) = struct include FO type 'a var = string * 'a D.dynvar (* name for tracing *) let newvar : string -> 'a var = fun name -> (name, D.dnew ()) let var : 'a var -> 'a exp = fun (name,dv) -> Printf.printf "Needing %s...\n" name; D.dref dv let let_ : 'a var -> 'a exp -> (unit -> 'b exp) -> 'b exp = fun (name,dv) e body -> Printf.printf "Binding %s...\n" name; D.dlet dv e body end

Essentially, DSL variables are realized as dynvar,`var`

is`dref`

and`let_`

is`dlet`

. In particular, accessing a variable is a (reader) effect.The

`FOL`

interpreter is parameterized by the implementation of dynamic binding. See the accompanying code for tests, using`DBShallow`

and`DDB`

implementations of dynamic binding.We must stress again the absence of any explicit environment, and that the first-order fragment

`FO`

is used as is, without any modification. The first-order fragment remains unaware of any variables.

- It may be tempting to add higher-order functions similarly, as a
simple generalization of
`let`

:module HODB(D:dynbind) = struct include FOL(D) let lam : 'a var -> (unit -> 'b exp) -> ('a -> 'b) exp = fun v body -> fun e -> let_ v e body end

which is what the original Lisp did. It is indeed very intuitive and elegant -- in fact, too intuitive. Trying to interpret our examples shows the problem: whereas

`ex0`

runs and gives the expected result, interpreting`ex1`

, repeated belowlet ex1 = (lam x @@ fun () -> let_ y (var x + var x) @@ fun () -> lam z @@ fun () -> var z + (var z + (var y + var y))) // (int 10 - int 5) // (int 20 - int 10)

ends in a ``unbound dynamic variable'' when accessing`y`

, according to the trace. Looking closely, we see that although`lam z`

is defined within the scope of`let_ y`

, it is applied outside the dynamic scope of that let-expression. The example`exd`

shows a more insidious error:let exd = let_ h (lam f @@ fun () -> let_ x (int 10) @@ fun () -> var f // var x) @@ fun () -> let_ x (int 1) @@ fun () -> var h // (lam y (fun () -> var x + var y))

Interpreting it with`HODB`

finishes without problems; the result,`20`

, is probably not what one may have expected. In the presence of first-class functions, lexical binding no longer coincides with dynamic binding.The solution is also old, proposed by Landin back in 1960s: closures, which carry the variable environment at the point of function definition. When the function is later applied, its body is evaluated within the environment of its definition rather than the environment of the application. We can implement this standard, textbook solution literally, if we use an extended dynamic binding facility that permits capturing and restoring of the dynamic environment:

module type db_capture = sig include dynbind type env val current_env : unit -> env val with_env : env -> (unit -> 'w) -> 'w end

The operation`current_env`

captures the current environment and returns it as an opaque value (of an abstract type`env`

). The operation`with_env`

receives an`env`

and a`thunk`

and evaluates the thunk in the given dynamic environment`env`

rather than the current one.Given an implementation of

`db_capture`

, lexical first-class functions are implemented*literally*as the textbooks say:module HO(D:db_capture) = struct include FOL(D) let lam : 'a var -> (unit -> 'b exp) -> ('a -> 'b) exp = fun v body -> let env = D.current_env () in (* env of the lam definition *) fun e -> D.with_env env @@ fun () -> let_ v e body end

The body of the lambda-expression is evaluated in the environment of its definition.

- We have thus seen that lexical scope is characterized by an extended
dynamic binding
`db_capture`

-- extended with the operations for capturing and restoring of the dynamic environment. We now demonstrate that these operations are realizable in terms of the ordinary dynamic binding (plus the facility to build sequences, or at least something like function compositions).The proof is constructive: the following functor delivers an implementation of

`db_capture`

given an implementation of`dynbind`

:module DBCapture(D:dynbind) = struct include D type env = {k: 'w. (unit -> 'w) -> 'w} let with_env : env -> (unit -> 'w) -> 'w = fun {k} body -> k body let env_acc = dnew ~init:{k=fun b -> b ()} () let current_env : unit -> env = fun () -> dref env_acc let dlet : 'a dynvar -> 'a -> (unit -> 'w) -> 'w = fun dv e body -> let env = current_env () in D.dlet env_acc {k = fun b -> env.k (fun () -> D.dlet dv e b)} @@ fun () -> D.dlet dv e body end

The trick is the dynamic variable`env_acc`

, to accumulate the current dynamic environment. A`dlet`

expression records in`env_acc`

the binding it is about to make.The functor

`DBCapture`

builds the implementation of`db_capture`

generically, given any implementation of`dynbind`

. For a particular implementation of`dynbind`

, however, there may be a more efficient realization of`db_capture`

. For example, the accompanying code shows such efficient implementation of`db_capture`

it terms of`DDB`

, using multiprompt delimited control (supported in OCaml as the library`delimcc`

). Incidentally, capturing of the environment requires multi-shot delimited control, which is*not*supported by OCaml 5 algebraic effects. It turns out that multi-shot delimited control is needed not just to implement non-determinism. **References**- lexdyn.ml [20K]

The complete code accompanying the article

- In the call-by-name evaluation strategy, variables are bound to
expressions rather than values; the evaluation occurs when the value
is required, to return the overall result or perform an arithmetic
operation. Making our DSLs call-by-name is
messier, because the the evaluation strategy of the DSL differs from
that of the host language, and we may no longer piggy-back on the
latter: straightforward meta-circular interpretation is no longer
possible. Still, we may introduce variables and variable binding
modularly, as described earlier. A complication is that we
need to capture the environment already in the
`fol`

interpreter: in call-by-name, lexical and dynamic scope differ even without first-class functions.Call-by-need, or lazy, evaluation is call-by-name with the memoization of the result. A lazy expression is not evaluated until its result is needed. At that point, the expression is evaluated and the result is memoized. Thus a lazy

*argument*expression is evaluated at most once. Dynamic binding often includes the operation`dset`

to change the binding of a dynamic variable in scope (in particular,`DDB`

supports such an operation; it is easy to add to`DBShallow`

). Using`dset`

in the implementation of the`var`

operation is all that is needed to make call-by-name into call-by-need. **References**- lexdyn.ml [20K]

The complete code accompanying the article

- The two old pieces of code, mostly of historical interest by now,
implement lazy evaluation in a call-by-value lambda-calculus with
shift and reset. The first code was written in 2005 in Scheme. An
improved version, in OCaml and using delimcc, was implemented in July
2017 over discussions with Petros Barbagiannis. That version has
eventually lead to the present article.
The goal at that time was to related call-by-need with delimited control. I have eventually realized that it is not about delimited control but about dynamic binding (which may be implemented via delimited control, among other things).

**References**- cbn_delimcc1.ml [8K]

The OCaml implementation, July 7, 2017. It uses a more conventional representation of an embedded DSL as an algebraic data type (deep embedding). The interpreter (`eval`

) is the fold over that data type.lazy-eval.scm [6K]

The complete implementation and several illustrative examples, including the recursively-defined Fibonacci stream. The code was originally written on Feb 21, 2005. The version as of Dec 28, 2008 adds a convenient automatic identification of lazy expressions and more examples.Ronald Garcia, Andrew Lumsdaine and Amr Sabry: Lazy Evaluation and Delimited Control. Logical Methods in Computer Science, July 11, 2010, Volume 6, Issue 3

- We have thus seen that
- Variables and variable binding, and even lexically-bound higher-order functions may be added to a first-order language modularly, without rewriting its interpretation to pass the variable environment.
- The interpreter stack may serve as the variable binding environment.
- The let-form is more fundamental than lambda: lambda-form is sort of a `truncated' let-form, with the captured environment