Environments and let

Through Part II an expression meant one value wherever it stood: 2 + 2 is 4 in every context, and the evaluator needed nothing but the expression itself to find it. A variable is the first form whose value the expression does not settle on its own. x stands for 3 where a binding says so, for "hi" where another one does, and for nothing at all where none does. The structure that supplies each name’s value is the environment, and this chapter describes what an environment is and how it came to be.

Algol 60 made where does a name refer? a question with a principled answer — a name introduced in a region of a program means something inside that region and not outside it — but left open what such a region is made of once the program runs. The environment is the answer: a map from the names in scope to the values they currently denote. In Bridger, we use let x = e to update the environment to say that the name x now refers to the value e evaluates to.

A name has a value only in context

The evaluation judgment has carried an environment $\rho$ since Part I, and every rule threaded the same $\rho$ through its premises. Until now nothing read or modified the environment. The arithmetic, boolean, string, and list forms have no variable to look up, so each rule passed $\rho$ along untouched and the derivations dropped it, writing $e\Downarrow v$; the starter’s eval_expr did the same, taking an env parameter that no arm consulted. A variable changes that. Its rule reads the environment and nothing else:

$$\frac{\rho (x)=v}{\rho ⊢x\Downarrow v}(\text{E-Var})$$

$\rho$ is a finite map from variables in scope to values, $\rho :Var\rightharpoonup v$; $\rho (x)$ is the value it binds to $x$. When $\rho$ has no binding for $x$, the premise $\rho (x)=v$ cannot be met, no rule applies, and the expression is stuck — the same absence of a derivation that a type mismatch produces, reported as the runtime error UnboundVariable. An unbound name is the failure this chapter adds to the list; every other stuck case so far came from a value of the wrong shape, and this one comes from a name with no value at all.

The environment as an explicit part of an evaluator goes back to Peter Landin’s SECD machine, whose four components — stack, environment, control, dump — evaluate an expression by looking each variable up in the environment component, the E (Landin, 1964). Two years later the same author’s ISWIM gave the notation let x = e (and its mirror, the where clause) for naming a value over a region of an expression (Landin, 1966); the keyword has since landed in languages far from ISWIM, Bridger among them.

The let operator

A block is a sequence of items evaluated top to bottom, and its value is its final expression. A let is one kind of item: it evaluates its right-hand side and binds the name over the rest of the block. Writing $\{rest\}$ for the block that remains after the first item, the rule extends the environment for that remainder and for nothing else:

$$\frac{\rho ⊢e_1\Downarrow v_1\rho [x\mapsto v_1]⊢\{rest\}\Downarrow v}{\rho ⊢\{\text{let}x=e_1;rest\}\Downarrow v}(\text{E-Let})$$

The notation $\rho [x\mapsto v_1]$ is the environment $\rho$ with $x$ bound to $v_1$ added: it agrees with $\rho$ on every other name and answers $v_1$ for $x$. The right-hand side $e_1$ is evaluated in $\rho$ — the environment before the binding is added — so the name being bound is not yet in scope while its own value is computed. The rest of the block is evaluated in the extended environment, which is where the new name can be read.

An item that is a bare expression is evaluated for whatever it does and its value discarded; the block carries on in the same environment. The final expression is the block’s value, and an empty block is unit:

$$\frac{\rho ⊢e_1\Downarrow v_1\rho ⊢\{rest\}\Downarrow v}{\rho ⊢\{e_1;rest\}\Downarrow v}(\text{E-Seq})$$

$$\frac{\rho ⊢e\Downarrow v}{\rho ⊢\{e\}\Downarrow v}(\text{E-Block})\frac{}{\rho ⊢\{\}\Downarrow ()}(\text{E-Empty})$$

Because $\text{E-Let}$ extends the environment only over the block’s remainder, a binding reaches from its let to the end of the enclosing block and no further. A name bound inside a block is not in scope after the block ends, and a name bound in an outer block is in scope within an inner one unless the inner block binds the same name again.

A binding is confined to its block even when that block is nested inside another. Take a block whose first item is itself a block:

{
    { let x = 1; x + 1 };   // inner block; x is bound only within it
    x                       // UnboundVariable: x's scope ended at the }
}

The outer block evaluates its first item — the inner block — by $\text{E-Seq}$, which evaluates it in the current environment and discards the result. Inside, $\text{E-Let}$ extends the environment with $x\mapsto 1$ for the inner block’s remainder alone, yielding 2. $\text{E-Seq}$ then evaluates the rest of the outer block in the same environment it began with — the one with no x — so the final x is unbound. A block produces a value, not an environment: the binding made inside the inner block never leaves it.

Binding a name a second time is shadowing: the new binding $\rho [x\mapsto v]$ answers for $x$ from that point on, and the earlier value is unreachable through the name for the rest of that region though it is not destroyed. Since the right-hand side is evaluated before the binding is added, a let may define a name in terms of the value the same name held before it:

let x = 1;
let x = x + 1;   // the x on the right is the old 1; x is now 2
x                // 2

Building it

The environment now reaches the evaluator’s signature. The provided method is

fn eval_expr(&mut self, e: &Expr, env: &Env) -> Result<Value, Control>

and the env parameter, carried unused since Milestone M1, is what the new arms read. An Env offers two operations: lookup, which returns the value a name is bound to or None, and extend, which returns a new environment with one more binding and leaves the one it was called on untouched. $\text{E-Var}$ needs only the first: look the name up, and a miss is UnboundVariable. A block threads the second — it walks its items carrying an environment that grows as each let is met — and because every extension produces a fresh scope, that growth reaches the rest of the block and stops at its closing brace.

// M2: read a variable, and evaluate a block by threading a
// scope that each `let` extends — scope = scope.extend(x, v)
Expr::Var(..)   => todo_m2!("look up a variable"),
Expr::Block(..) => todo_m2!("evaluate a block"),

That the environment is never rewritten is the rule the whole chapter turns on. $\rho$ is read-only: a let adds a binding, and rebinding a name is a new binding that shadows the old, not a change to it. Making a name’s value change over time — a counter that counts — is a separate mechanism, a mutable cell held in the store, and it arrives in Part IV. How an Env is represented, and what lookup costs as scopes nest, is the next chapter; how a name’s binding is fixed by where it is written rather than by where it is used — the property that makes scope decidable before the program runs — is the chapter after. Reading variables and evaluating blocks completes the evaluator’s work for Milestone M2.

The design space

let need not be a form of its own. Landin’s observation was that a block beginning let x = e_1; computes what applying the function $\lambda x.e$ — whose body $e$ is the rest of the block — to the argument $e_1$ computes: both evaluate $e_1$, bind the result to $x$, and evaluate that body in the extended environment. A language with functions can treat let as sugar for that application and carry one rule instead of two. Bridger keeps let a form in its own right — functions arrive in Part V, and let is available from the first block a program writes — but the two describe the same binding, and the closure rule in Part V will extend the environment the same way $\text{E-Let}$ does.

Whether a name is in scope within its own right-hand side is a genuine fork, and $\text{E-Let}$ takes a side: it evaluates $e_1$ in the environment before the binding is added, so x is bound after its definition, not during it. A definition may therefore use the earlier meaning of a name it rebinds, and a let-bound function cannot call itself, since the name is not in scope while the function value is being built. Languages that want a let to bind a recursive function offer a separate recursive-binding form — let rec, or a letrec that binds the name over its own right-hand side — that closes exactly this gap. In Bridger, self-reference goes through a top-level fn, where every top-level name is in scope in every definition, so functions may call themselves and each other regardless of order.

Rebinding a name that is already in scope is a choice too. Bridger allows it — shadowing is ordinary — where some languages reject a second binding of a name in the same scope and require the programmer to choose a fresh one. Allowing it lets a block reuse a name for a series of related values; rejecting it turns an accidental reuse into an error the compiler catches. The tradeoff is between a convenience and a class of mistake, and Bridger takes the convenience.

Further reading

The environment and let: Peter Landin’s The Mechanical Evaluation of Expressions (The Computer Journal, 1964) introduces the SECD machine, whose environment component is the structure a variable is resolved against, and The Next 700 Programming Languages (Communications of the ACM, 1966) introduces ISWIM and its let and where notations for naming a value over a region of an expression, together with the reading of a local definition as a function applied to its right-hand side.

The environment model of evaluation: Abelson and Sussman’s Structure and Interpretation of Computer Programs (MIT Press, free online) develops evaluation as the extension of environments in its chapter of that name, working through how a binding form adds to the environment and how a name is looked up in it.

Concept checks