Lecture 18: Explaining letcc and error

Explaining letcc and error

Our goal is to produce a tail-recursive interpreter, which we will use to understand the meaning of error and letcc.

To recap our previous lecture, during its evaluation, every phrase will be surrounded by some computation that is waiting to be performed (and, typically, that depends on the value of this phrase). This remaining computation is known as an evaluation context. Turning this evaluation context into a function is the act of making the continuation explicit.

For instance, in

(+ (* 12 3) (- 2 23))

the evaluation context of the first sub-expression (assuming it is evaluated first) is

(+ _ (- 2 23))

(where we pronounce _ as ``hole''), so the reified version of this context is

(lambda (x) (+ x (- 2 23)))

Puzzle: Can (lambda (x) ... _ ...) be a valid evaluation context?

Modeling error

Let us consider an interpreter for LC:

(define Eval
  (lambda (M env)
    (cond
      ((var? M)
	(lookup M env))
      ((lam? M)
	(make-closure M env))
      ((app? M)
	(Apply (Eval (app-rator M) env) (Eval (app-rand M) env)))
      ((add? M)
	...)
      ...)))

In this interpreter, we see both the creation of new continuations and the use of the (implicit) continuation. New continuations are created in the code for applications, at the evaluation of the sub-expressions and again in the call to Apply. The other two clauses shown use the current continuation by passing it a value.

We now use the standard technique for transforming Scheme code to transform the interpreter into CPS:

(define Eval/k
  (lambda (M env k)
    (cond
      ((var? M) (k (lookup M env)))
      ((lam? M) (k (make-closure M env)))
      ((app? M) (Eval/k (app-rator M) env
		  (lambda (rator-v)
		    (Eval/k (app-rand M) env
		      (lambda (rand-v)
			(Apply/k rator-v rand-v k))))))
      ...)))

We need to similarly transform Apply. Whereas before we had

(define Apply
  (lambda (f a)
    (cond
      ((closure? f)
	(Eval (body-of f)
          (extend (env-of f) (param-of f) a)))
      (else ...))))

we now have

(define Apply/k
  (lambda (f a k)
    (cond
      ((closure? f)
	(Eval/k (body-of f)
	  (extend (env-of f) (param-of f) a) 
	  k))
      (else ...))))

Historical Note:

None of the Apply procedures take an environment as an argument; instead, they choose to use the one stored in the closure. However, it is possible to imagine a different semantics that passes on the current environment to Apply, which then passes it on for the remainder of the evaluation. Such a system is said to have dynamic binding, as opposed to the static binding used here.

Exercise:

Implement dynamic binding.

We have intentionally left the fall-through case of the cond expressions in the Apply procedures empty. However, we know from before that there should be a call to error in that slot. Since we want to explain error, we need to determine how to signal an erroneous application.

Since the k argument always represents the entire evaluation context, there is no additional computation awaiting the value returned by the interpreter. Therefore, to ignore the pending computations and return a value directly, all that error needs to do in this interpreter is to return a value. This value is then returned to the user. (Note that this crucially depends on the fact that the interpreter is fully tail-recursive.) Therefore, the code for Apply/k could be written as

(define Apply/k
  (lambda (f a k)
    (cond
      ((closure? f)
	(Eval/k (body-of f)
	  (extend (env-of f) (param-of f) a) 
	  k))
      (else 'ouch!))))

Note that the else clause above is ``returning'' at the meta-level, not at the level of LC. A function return in LC is modeled by passing the result of evaluating the function call to the appropriate continuation.

We have teased out control entirely and made it a distinct entity in the interpreter. Thus, we can use it as before, we can ignore it, or we can harness it in new ways, as we will see below.

Puzzle: What value would we use as the initial continuation?

Modeling letcc

In our earlier interpreters, we modeled letcc by appealing to the letcc form at the meta-level:

(cond
  ...
  ((letcc? M)
    (letcc k (Eval (body-of M)
               (extend env (label-of M) k))))
  ...)

Since we want letcc to bind a program variable to the rest of the computation, we could instead write, in Eval/k,

(cond
  ...
  ((letcc? M)
    (Eval/k (body-of M)
      (extend env
	(label-of M) k)
	k))
  ...)

This rewrite makes manifest an interesting feature of control. Just as stores were duplicated when we made them explicit, here we have two uses of k. In the case of stores, we hypothesized that we could have an operator that ``forgot'' the side-effects performed in the evaluation of an expression, but we found no use for such an operator. Now, however, we can save the evaluation context, and return to it -- ignoring any intermediate context -- if we wish. Furthermore, since this evaluation context is bound in the environment, we can return to it whenever we choose to, even outside the lexical context of the letcc expression. One example of where this might be useful is in the implementation of context switches during multitasking, where we periodically store the current context and return to it later.

Hence, whereas before control was single-threaded, and could be implemented as a stack, it is now tree-shaped and cannot be implemented in that manner.

Eliminating Closures

Earlier, we decided to eliminate meta-language closures from our interpreter. Now, we have reintroduced them in the process of CPSing our interpreter, ie, in the action for applications. As before, we shall model this process of closure creation abstractly by using the procedure Push. Similarly, we will abstract over the use of the continuation -- to ``return'' values -- as the procedure Pop.

(define Eval*/k
  (lambda (M env k)
    (cond
      ((var? M) (Pop k (lookup M env)))
      ((lam? M) (Pop ...))
      ((app? M)
	(Eval (app-rator M) env
	  (Push 1 M env k)))
      ...)))

To begin with, these abstractions can map to the current implementation method:

(define Push
  (lambda (name M env k)
    (lambda (x)
      (Eval/k (app-rand M) env
	(lambda (y)
	  (Apply/k x y k))))))

(define Pop
  (lambda (k v)
    (k v)))

Note, further, that Push has a call to Eval/k; we rewrite this as

(Eval/k (app-rand M) env (Push 2 x k))

In all, there is a finite number of locations that create continuations in the interpreter, so we can write a procedure that creates each one of these. Thus, Push can be rewritten as

(define Push
  (lambda (name . pv)
    (cond
      ((= name 1)
	(let ((M ...pv...) (env ...pv...) (k ...pv...))
	  (lambda (x) (Eval/k (app-rand M) env
			(Push 2 x k)))))
      ((= name 2)
	(let ((x ...pv...) (k ...pv...))
	  (lambda (y) (Apply/k x y k)))))))

Finally, the remaining reliance on lambda can be removed by replacing it with a call to list instead. In the process, Pop has to become more elaborate: in particular, it needs to dispatch on the ``name'' of the current continuation. This is analogous to the change made in Apply when we moved from a meta-level to a structure-based representation of closures in our original interpreters.