How shall I understand the undesirable consequences of dynamic scoping?

Question

In Practical Foundation of Programming Languages by Harper

8.4 Dynamic Scope

Another approach, called dynamic scoping, or dynamic binding, is sometimes advocated as an alternative to static binding. The crucial difference is that with dynamic scoping the principle of identification of abt’s up to renaming of bound variables is denied. Consequently, capture-avoiding substitution is not available. Instead, evaluation is defined for open terms, with the bindings of free variables provided by an environment mapping variable names to (possibly open) values. The binding of a variable is determined as late as possible, at the point where the variable is evaluated, rather than where it is bound. If the environment does not provide a binding for a variable, evaluation is aborted with a run-time error.

In the higher-order case, the equivalence of static and dynamic scope breaks down. For example, consider the expression

 e = (λ (x : num) λ (y : num) x + y)(42).

With static scoping e evaluates to the closed value v = λ (y : num) 42 + y, which, if applied, would add 42 to its argument. It makes no difference how the bound variable x is chosen, the outcome will always be the same. With dynamic scoping, e evaluates to the open value v' = λ (y : num) x + y in which the variable x occurs free. When this expression is evaluated, the variable x is bound to 42, but this is irrelevant because the binding is not needed to evaluate the λ-abstraction. The binding of x is not retrieved until such time as v' is applied to an argument, at which point the binding for x in force at that time is retrieved,and not the one in force at the point where e is evaluated.

Therein lies the difference. For example, consider the expression

e' = (λ (f : num → num) (λ (x : num) f (0))(7))(e)`.

When evaluated using dynamic scope, the value of e' is 7, whereas its value is 42 under static scope. The discrepancy can be traced to the rebinding of x to 7 before the value of e, namely v', is applied to 0, altering the outcome.

Dynamic scope violates the basic principle that variables are given meaning by capture-avoiding substitution as defined in Chapter 1. Violating this principle has at least two undesirable consequences.

One is that the names of bound variables matter, in contrast to static scope which obeys the identification principle. For example, had the innermost λ-abstraction of e' bound the variable y, rather than x, then its value would have been 42, rather than 7. Thus, one component of a program may be sensitive to the names of bound variables chosen in another component, a clear violation of modular decomposition.

Another problem is that dynamic scope is not, in general, type-safe. For example, consider the expression

e' = (λ (f : num → num) (λ (x : str) f ("zero"))(7))(e)

Under dynamic scoping this expression gets stuck attempting to evaluate x + y with x bound to the string “zero”, and no further progress can be made.

What does it mean by "with dynamic scoping the principle of identification of abt’s up to renaming of bound variables is denied" and "consequently, capture-avoiding substitution is not available"?

Why under dynamic scoping, "had the innermost λ-abstraction of e' bound the variable y, rather than x, then its value would have been 42, rather than 7"? How does "static scope obey the identification principle" here?

How "Under dynamic scoping this expression gets stuck attempting to evaluate x + y with x bound to the string “zero”"? Isn't it that x in e' is bound to 7?

Thanks.

Answer 1

I think you're right that that example is a bit confused. I believe the fix is the following, if I got my parantheses right.

e' = (λ (f : num → num) (λ (x : str) f ("zero"))(7))(e)

should instead be

e' = (λ (f : num → num) (λ (x : str) f) ("zero"))(e)(7)

If we evaluate e first we'll get:

(λ (x : num) λ (y : num) x + y)(42).

x = 42
(λ (y : num) x + y).

We've finished evaluating e, since we got to a lambda. But evaluating it in the above expression will cause the bad addition "zero" + 42, since, regardless of what we do with the environment, the x="zero" binding will be the closest. The immediate reduction of the above gives: