CS 312 Recitation 5
Scope, Evaluation with Substitutions

Identifiers

The ability to define new identifiers is central to every high-level programming language. Identifiers are the way that programmers refer to constructs they create; different uses of identifiers correspond to the different abstraction mechanisms provided by the programming language. Let's take a closer look at the way that identifiers are used in ML.

In ML, identifiers may refer to variables, functions (which are really just variables), datatypes, datatype constructors, field names, type names introduced using type, type variables (if preceded by ') and to some other things we  haven't seen yet: modules and signatures. SML lets you use the same identifiers to refer to some of these things. For example, you can have a type named foo and a variable named foo at the same time. When an expression contains the identifier foo, what it refers to depends on how it is used. In the following code, the occurrences of "foo" that refer to a type are shown in green, the occurrences that are variables are shown in red and magenta. In this example there are actually two different variables named foo; the second one (in green) shadows the first one.

let type foo = int
    val foo: foo = 2
    val foo: {foo: foo} = {foo = foo}
in
  #foo foo
end

Clearly the ability to use names to refer to different kinds of things at the same time can be abused. Try avoid writing code that looks like this example!

Binding

There are three different ways that one can use an identifier:

1. A binding occurrence, which binds the identifier to a particular value or type. For example, in the expression let val x:int = 1 in x end, the first occurrence is a binding occurrence that binds x to 1. Each binding occurrence introduces a new variable, and this new variable has a scope: a part of the program in which uses of that identifier refer to the variable. In this case the scope of the variable x is the body of the let expression.
2. A bound occurrence is a use of a variable in the scope of a variable binding. For each bound occurrence of a variable, there is a single corresponding binding of that variable. For example, in the expression (fn(x:int)=>x),  the second occurrence of x is a bound occurrence; its corresponding binding occurrence is the first occurrence. At run time this variable will be bound to whatever value is passed to the function when it is invoked.
3. An unbound or free occurrence is a use of an identifier with no corresponding binding occurrence in whose scope. For example, in the expression let val y:foo = x+1 in y end, the use of x is an unbound occurrence because there is no containing binding of x. The identifier foo is also an unbound occurrence of a type identifier. A legal SML program cannot contain an unbound occurrence of an identifier. However, for the purpose of understanding how SML works, sometimes it is useful to write down syntactically legal fragments of SML programs and talk about the unbound variables that occur in them.

Given an occurrence of an identifier that is not a binding occurrence, there is a simple way to figure out whether it is bound or unbound, and if the former, to which binding occurrence the identifier is bound. An identifier is bound if it is in the scope of a binding occurrence. For ML programs, the scope of a variable can be seen by simply looking at the program text. If the variable lies within the scope of more than one binding occurrence, then one of those bindings shadows the rest. It will be the binding occurrence whose scope most tightly encloses the use of the identifier.

In SML it is possible to figure out just by looking at the program code which occurrence binds each use of a variable. A language with this property is said to have lexical (or static) scoping : the scope of each variable is apparent from the lexical form of the program, without knowing anything about how the program runs. The alternative to lexical scoping is dynamic scoping, in which a given variable occurrence may have different binding occurrences depending on how the program runs. In most modern languages, such as Java or C, variable have lexical scope. However, Perl and Python are examples of languages with dynamic variable scoping. Dynamic scope is harder to implement efficiently, and can lead to unpleasant surprises for programmers because variables don't always mean what they expect.

Substitution

Earlier we saw some rewriting rules that explained how to evaluate terms of the SML language. For example, we said that a simple expression evaluates according to the following rewrite rule:

let val x:t = v in e end  -->  e (with occurrences of x replaced by v)

Remember that we use e to stand for an arbitrary expression (term), x to stand for an arbitrary identifier, and v to stand for a value -- that is, a fully evaluated term.

We now know this cannot be the full story, because e2 may contain occurrences of x whose binding occurrence is not this binding x:t = v1.  It doesn't make sense to substitute v for these occurrences. For example, consider evaluation of the expression:

let val x:int = 1
    fun f(x:int) = x
    val y:int = x+1
in
  fn(a:string) => x*2
end

The next step of evaluation replaces the green occurrences of x with 1, because these occurrences have the first declaration as their binding occurrence. Notice that the two occurrences of x inside the function f, which are respectively a binding and a bound occurrence, are not replaced. Thus, the result of this rewriting step is

let fun f(x:int) = x
    val y:int = 1+1
in
  fn(a:string) => 1*2
end

Let's write the substitution e{v/x} to mean the expression e with all unbound occurrences of x replaced by the value v. Then we can restate the rule for evaluating let more simply:

let val x:t = v in e end --> e{v/x}

This works because any occurrence of x in e must be bound by exactly this declaration val x:t = v. Here are some examples of substitution:

x{2/x}  =  2
x{2/y}  =  x
(fn(y:int)=>x) {"hi"/x}  =  (fn(y:int)=>"hi")
f(x) { fn(y:int)=>y / f } =  (fn(y:int)=>y)(x)

One of the features that makes ML fairly unique is the ability to write complex patterns containing binding occurrences of variables. Pattern matching in ML causes these variables to be bound in such a way that the pattern matches the supplied value. This is can be a very concise and convenient way of binding variables. We can generalize the notation used above by writing e{v/p} to mean the expression e with all unbound occurrences of variables appearing in the pattern p replaced by the values obtained when p is matched against v. Using this notation, we can express the let rule simply:

let val p = v in e end --> e{v/p}

What if a let expression introduces multiple declarations? Such an expression is identical in effect to a series of nested let expressions. Thus, we can use the following rewrite that pulls out the first declaration so the rules above apply. 

let d1...dn  in e end  -->
  let d1 in let d2...dn in e end end

We can use the same substitution operator to give a more precise rule for what happens when a function is called. Consider a function declared as fun f(p) = e, where f is the identifier naming the function. Then the expression for a function call whose argument has been evaluated, f(v), is rewritten as follows:

f(v)  -->  e{v/p}

Similarly, consider a call to an anonymous function:

(fn( p )=> e )( v )  -->  e{v/p}

We have seen a model of how programs evaluate in SML. It is important to realize that this is just a model. The actual implementation of SML evaluation is quite different (and much more complex to explain). This model is an abstraction that hides the complexity you don't need to know about. Some aspects of the model should not be taken too literally. For example, you might think that function calls take longer if an argument variable appears many times in the body of the function. It might seem that calls to function f are faster if it is defined as fun f(x) = x*3 rather than as fun f(x) = x+x+x because the latter requires three substitutions. Actually the time required to pass arguments to a function typically depends only on the number of arguments. Chances are the definition on the right is at least as fast as that on the left.

Evaluating functions

We have not yet discussed how to model the evaluation of a function declaration. Consider the expression let fun f p : t = e in e' end. This declaration creates a new function and binds the function to the identifier f. However, it is important to avoid confusing the function f with other possible functions named  f (perhaps created by evaluating the same expression earlier in the program). Therefore we model this binding process as follows. A fresh identifier f ' is selected (a fresh identifier is one that occurs nowhere else in the program). This fresh identifier is used to define a new  function of the form fun  f ' p = e{f '/f }. In other words f ' looks just like f except that any recursive references it contains are replaced by f '. This function is added to a special top-level environment that is accessible anywhere in the program text. Since f ' is fresh we do not need to worry that it might be shadowed.

The let expression is then rewritten to use f ' in place of f :

let fun f p : t =
e in e' end  -->  e' { f ' / f }

Here,  f '  is unbound in the current program expression, but it is bound in the top-level environment.

Consider an example:

let val s = "hi"
    fun g(n:int):string = if n=0 then s else g(n-1) ^ s in
  g(2)
end
-->
let fun g(n:int):string = if n=0 then "hi" else g(n-1) ^ "hi" in
  g(2)
end

--> g1(2) --> if 2=0 then "hi" else g1(2-1) ^ "hi" -->
if false then "hi" else g1(2-1) ^ "hi" -->
g1(2-1) ^ "hi" -->  g1(1) ^ "hi"  -->  (if 1=0 then "hi" else g1(1-1) ^ "hi") ^ "hi" -->
... --> (if 0=0 then "hi" else g1(0-1) ^ "hi") ^ "hi" ^ "hi" -->
"hi" ^ "hi" ^ "hi"  -->  "hihihi"

It is also possible to define several mutually recursive functions using the and keyword to separate them. For example, here are two functions that determine whether a number is even or odd:

fun even(n:int): bool =
  case n of
    0 => true
  | _ => odd(n-1)
and odd(n:int): bool = not (even(n))

If functions like these are evaluated inside a let statement, they are all evaluated and lifted to the top level together, resulting in top-level functions like the following for some fresh identifiers E and O.

fun E(n:int): bool =
  case n of
    0 => true
  | _ => O(n-1)
fun O(n:int): bool = not (E(n))

Note that the names of all the mutually recursive functions are consistently replaced in all their bodies.

Here is a more elaborate example. This is about as complicated as it gets.

let fun f(x: int, g1: unit->int): int = 
  let fun g(): int = x + 10
  in
    if x = 0 then g() + g1()
    else f(0, g)
  end
in
  f(1, fn()=> 0)
end

fun f'(x: int, g1: unit->int): int = 
  let fun g(): int = x + 10
  in
    if x = 0 then g() + g1()
    else f'(0, g)
  end

--> f'(1, fn()=> 0)

fun g'(): int = 0

--> f'(1, g')

--> let fun g(): int = 1 + 10
    in
      if 1 = 0 then g() + g'()
      else f'(0, g)
    end

fun g''(): int = 1 + 10

--> if 1 = 0 then g''() + g'()
    else f'(0, g'')

--> if false then g''() + g'()
    else f'(0, g'')

--> f'(0, g'')

--> let fun g(): int = 0 + 10
    in
      if 0 = 0 then g() + g''()
      else f'(0, g)
    end

fun g'''(): int = 0 + 10

--> if 0 = 0 then g'''() + g''()
    else f'(0, g''')

--> if true then g'''() + g''()
    else f'(0, g''')

--> g'''() + g''()

--> 0 + 10 + g''() --> 10 + g''() --> 10 + (1 + 10) --> 10 + 11 --> 10 + 21 = 21   

 Note that if ML had dynamic scoping, the result of this example would be 20!