18.11 Open Recursion and Evaluation Order

< Free Open Study >

There is one problem with our definition of instrCounterClass—we cannot use it to build instances! If we write newInstrCounter in the usual way

   newInstrCounter =     λ_:Unit. let r = {x=ref 1, a=ref 0} in                 fix (instrCounterClass r); ▸ newInstrCounter : Unit → InstrCounter

and then attempt to create an instrumented counter by applying it to unit,

   ic = newInstrCounter unit;

the evaluator will diverge. To see how this happens, consider the sequence of evaluation steps that ensue when we start from this term.

We first apply newInstrCounter to unit, yielding

   let r = {x=ref 1, a=ref 0} in fix (instrCounterClass r)

We next allocate two ref cells, package them into a record—let's call it <ivars>—and substitute <ivars> for r in the rest.
```
   fix (instrCounterClass <ivars>) 
```
We pass <ivars> to instrCounterClass. Since instrCounterClass begins with two lambda-abstractions, we immediately get back a function that is waiting for self,
```
   fix (λself:InstrCounter.          let super = setCounterClass <ivars> self in <imethods>) 
```
where <imethods> is the record of instrumented-counter methods. Let's call this function <f> and write the current state (fix <f>).
We apply the evaluation rule for fix (E-FIX in Figure 11-12, page 144), which "unfolds" fix <f> by substituting (fix <f>) for self in the body of <f>, yielding
```
   let super = setCounterClass <ivars> (fix <f>) in <imethods> 
```
We now reduce the application of setCounterClass to <ivars>, yielding:
```
   let super = (λself:SetCounter. <smethods>) (fix <f>)               in <imethods> 
```
where <smethods> is the record of set-counter methods.
By the evaluation rules for applications, we cannot reduce the application of (λself:SetCounter. <smethods>) to (fix <f>) until the latter has been reduced to a value. So the next step of evaluation again unfolds fix <f>, yielding:
```
   let super = (λself:SetCounter. <smethods>)                  (let super = setCounterClass <ivars> (fix <f>)                   in <imethods>)   in <imethods> 
```

Since the argument to the outer lambda-abstraction is still not a value, we must continue to work on evaluating the inner one. We perform the application of setCounterClass to <ivars>, yielding

   let super = (λself:SetCounter. <smethods>)                  (let super = (λself:SetCounter. <smethods>)                                  (fix <f>)                   in <imethods>)   in <imethods>

Now we have created an inner application similar in form to the outer one. Just as before, this inner application cannot be reduced until its argument, fix <f>, has been fully evaluated. So our next step is again to unfold fix <f>, yielding a yet more deeply nested expression of the same form as in step 6. It should be clear at this point that we are never going to get around to evaluating the outer application.

Intuitively, the problem here is that the argument to the fix operator is using its own argument, self, too early. The operational semantics of fix is defined with the expectation that, when we apply fix to some function λx.t, the body t should refer to x only in "protected" positions, such as the bodies of inner lambda-abstractions. For example, we defined iseven on page 143 by applying fix to a function of the form λie. λx. ..., where the recursive reference to ie in the body was protected by the abstraction on x. By contrast, the definition of instrCounterClass tries to use self right away in calculating the value of super.

At this point, we can proceed in several ways:

We can protect the reference to self in instrCounterClass to prevent it from being evaluated too early, for example by inserting dummy lambda-abstractions. We develop this solution below. We will see that it is not completely satisfactory, but it is straightforward to describe and understand using the mechanisms we have already seen. We will also find it useful later, when we consider purely functional object encodings in Chapter 32.
We can look for different ways of using low-level language features to model the semantics of classes. For example, instead of using fix to build the method table of a class, we could build it more explicitly using references. We develop this idea in §18.12 and further refine it in Chapter 27.
We can forget about encoding objects and classes in terms of lambda-abstraction, records, and fix, and instead take them as language primitives, with their own evaluation (and typing) rules. Then we can simply choose evaluation rules that match our intentions about how objects and classes should behave, rather than trying to work around the problems with the given rules for application and fix. This approach will be developed in Chapter 19.

Using dummy lambda-abstractions to control evaluation order is a well-known trick in the functional programming community. The idea is that an arbitrary expression t can be turned into a function λ_:Unit.t, called a thunk. This "thunked form" of t is a syntactic value; all the computation involved in evaluating t is postponed until the thunk is applied to unit. This gives us a way to pass t around in unevaluated form and, later, ask for its result.

What we want to do at the moment is to delay the evaluation of self. We can do this by changing its type from an object (e.g. SetCounter) to an object thunk (Unit→SetCounter). This involves (1) changing the type of the self parameter to the class, (2) adding a dummy abstraction before we construct the result object, and (3) changing every occurrence of self in the method bodies to (self unit).

   setCounterClass =     λr:CounterRep.     λself: Unit→SetCounter.       λ_:Unit.         {get = λ_:Unit. !(r.x),          set = λi:Nat.  r.x:=i,          inc = λ_:Unit. (self unit).set(succ((self unit).get unit))}; ▸ setCounterClass : CounterRep →                     (Unit→SetCounter) → Unit → SetCounter

Since we do not want the type of newSetCounter to change (it should still return an object), we also need to modify its definition slightly so that it passes a unit argument to the thunk that results when we form the fixed point of setCounterClass.

   newSetCounter =     λ_:Unit. let r = {x=ref 1} in                 fix (setCounterClass r) unit; ▸ newSetCounter : Unit → SetCounter

Similar changes are needed in the definition of instrCounterClass. Note that none of these modifications actually require any thinking: once we have changed the type of self, every other change is dictated by the typing rules.

   instrCounterClass =     λr:InstrCounterRep.     λself: Unit→InstrCounter.       λ_:Unit.         let super = setCounterClass r self unit in            {get = super.get,             set = λi:Nat. (r.a:=succ(!(r.a)); super.set i),             inc = super.inc,             accesses = λ_:Unit. !(r.a)}; ▸ instrCounterClass : InstrCounterRep →                       (Unit→InstrCounter) → Unit → InstrCounter

Finally, we change newInstrCounter so that it supplies a dummy argument to the thunk constructed by fix.

   newInstrCounter =     λ_:Unit. let r = {x=ref 1, a=ref 0} in                 fix (instrCounterClass r) unit; ▸ newInstrCounter : Unit → InstrCounter

We can now use newInstrCounter to actually build an object.

   ic = newInstrCounter unit; ▸ ic : InstrCounter

Recall that this was the step that diverged before we added thunks.

The following tests demonstrate how the accesses method counts calls to both set and inc, as we intended.

   (ic.set 5; ic.accesses unit); ▸ 1 : Nat   (ic.inc unit; ic.get unit); ▸ 6 : Nat   ic.accesses unit; ▸ 2 : Nat

18.11.1 Exercise [Recommended, ⋆⋆⋆]

Use the fullref checker to implement the following extensions to the classes above:

Rewrite instrCounterClass so that it also counts calls to get.
Extend your modified instrCounterClass with a subclass that adds a reset method, as in §18.4.
Add another subclass that also supports backups, as in §18.7.

< Free Open Study >