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
eevaluates to the closed valuev = λ (y : num) 42 + y, which, if applied, would add42to its argument. It makes no difference how the bound variablexis chosen, the outcome will always be the same. With dynamic scoping,eevaluates to the open valuev' = λ (y : num) x + yin which the variablexoccurs free. When this expression is evaluated, the variablexis bound to42, but this is irrelevant because the binding is not needed to evaluate the λ-abstraction. The binding ofxis not retrieved until such time asv'is applied to an argument, at which point the binding forxin force at that time is retrieved,and not the one in force at the point whereeis 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'is7, whereas its value is42under static scope. The discrepancy can be traced to the rebinding ofxto7before the value ofe, namelyv', is applied to0, 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 variabley, rather thanx, then its value would have been42, rather than7. 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 + ywithxbound 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.