Continuations (= Stacks) Stacks record what we should continue doing after we're done evaluating the current expression. So, they're sometimes referred to as a "continuation". If we have a stack in the language, then we might consider making it a first-class thing that the programmer can manipulate, just like functions or integers. In other words, we might add stacks to the class of values: v ::= ... | S In addition, we might add mechanisms for getting our current stack/continuation (letcc) and for installing a given stack as the current continuation (throwcc): e ::= ... | letcc x in e | throwcc e1 e2 For throwcc, we'll also need two new stack frames to allow us to evaluate the nested subexpressions: F ::= ... | throwcc [] e | throwcc v [] The rewriting rules for these two new mechanisms are: (S, letcc x in e) => (S, e[S/x]) (S, throwcc S' v) => (S', v) (S, throwcc v e) => ((throwcc v [])::S, e) (e not a value) (S, throwcc e1 e2) => ((throwcc [] e2)::S, e1) (e1 not a value) Notice that letcc makes a copy of the current stack and substitutes it for x within the body of the letcc. The throwcc operation throws away the current stack and installs its first argument as the current continuation/stack. If we have letcc and throwcc, then we can (more or less) code up exceptions: try/catch corresponds to doing a letcc, and throw corresponds to doing a throwcc to that continuation. ------------------------------------------------------------------------- Homework: due Wed, 26 Nov before class. 1. Implement an interpreter for a language with continuations. You should use the following datatype definitions: type var = string datatype opn = Plus | Times | Minus datatype value = Int of int | Fn of var * exp | Stack of stack and exp = Var of var | Val of value | Opn of exp * opn * exp | App of exp * exp | Letcc of var * exp | Throw of exp * exp and frame = ... (* to be filled in by you *) withtype stack = frame list Note that you'll need to fill in appropriate constructors for the definition of the frame datatype. You should write two functions for your interpreter: val step : stack * exp -> stack * exp val evaluate : exp -> value Evaluate will call step until a terminal configuration is achieved. 2. SML/NJ doesn't provide letcc and throwcc, but it does provide two closely related constructs in the SMLofNJ.Cont library: callcc : ('a cont -> 'a) -> 'a throw : 'a cont -> 'a -> 'b An "T cont" is a continuation/stack that expects to be thrown a T value. You can encode "letcc x in e" as "callcc (fn x => e)". Suppose you have the following datatype: datatype 'a tree = Leaf of 'a | Node of {left:'a tree,right:'a tree} Your goal is to write a function: val exists : ('a -> bool) -> 'a tree -> bool with the propery that (exists p t) should return true iff t has a Leaf(v) such that p(v) returns true. Furthermore, and this is the interesting part, assuming that throw is a constant time operation, your function should return its answer within a constant number of steps of finding the first leaf value that satisfies the given predicate. Your function should require no auxiliary data structures, nor should it require multiple passes over the tree. Note that a standard recursive procedure does not have this property, as you'll end up "unwinding" the stack when you have a deeply nested Leaf that satisfies the predicate. Extra Credit: Write exists2 so that it has the same type, does not use exceptions, callcc, or an auxilliary data structure, but performs the same task in the same number of steps. 3. Suppose we wish to model a multi-threaded programming language such as Java. In particular, suppose we have a new expression form "fork e1 e2" which starts a new thread running the function e1 applied to the argument e2. That is, suppose we have the following expressions: e ::= x | i | \x.e | e1 e2 | fork e1 e2 Give a small-step, call-by-value operational semantics for this language. This means definining configurations and transition rules for the expression forms.