15-312 Foundations of Programming LanguagesContinuationsDaniel Spoonhower (spoons+@cs)Edited by Jason Reed (jcreed+@cs)October 6, 20041 ContinuationsWe began discussion of continuations last week in lecture; we will continue todaywith a pair of more detailed examples, both borrowed from Harper’s notes.1.1 ReviewRecall the static semantics of our constructs for manipulating continuations.Γ, x:τ cont ` e : τΓ ` callcc x => e : τΓ ` e1: τ1Γ ` e2: τ1contΓ ` throw[τ] e1to e2: τRemember that callcc binds the current continuation to a variable and thencontinues evaluation, while throw evaluations an expression and then continuesat the point of evaluation marked by the second expression.1.2 Short Circuiting EvaluationConsider the following function that computes the product of the elements inan integer list.fun mul(l : int list) : int =>case lof nil => 1| x::l => x * mul lNote that if the list contains the element 0, this function might perform asignificant amount of extra work, particularly if the 0 appears near the beginningof the list. We might consider a short-circuited version of multiplication, onewhere we stop inspecting the remainder of the list once we encounter a 0.1fun mul(l : int list) : int =>case lof nil => 1| x::l => if x = 0 then 0else x * mul l fiIf we expect a list of length n to have exactly one 0 (distributed uniformly),we’ve reduced the (expected) number of recursive calls by n/2. We are still,however, performing n/2 multiplications (again, expected case), each of whoseresult will be 0. We’d like to jump out the entire sequence of recursive calls,not just the current one.For reasons that will become clear in a moment, we first transform thefunction by η-expansion:fn l : int list =>let mul = fun mul(l : int list) : int =>case lof nil => 1| x::l => if x = 0 then 0else x * mul l fiinmul lendNow, using the callcc and throw constructs from above, we can writefn l : int list =>callcc ret =>let mul = fun mul(l : int list) : int =>case lof nil => 1| x::l => if x = 0 then throw 0 to retelse x * mul l fiinmul lendendIn this example, we are throwing a value backward to a previous point inevaluation, and moreover, we don’t really use ret for anything particularlyinteresting. We could have easily written a similar short-circuiting functionusing exceptions. Next, we’ll see an example where that is definitely not thecase.21.3 CompositionRemember that continuations are values: even though we can’t write a value oftype τ cont in the concrete syntax, they may be manipulated just like any othervalue.We’d like to write a function compose that combines a function with a con-tinuation, resulting in a new continuation. Specifically, a function with thefollowing type. (Why does this make sense?)compose : (τ0-> τ) -> τ cont -> τ0contWe begin as follows:fn f : τ0-> τ => fn k : τ cont =>Now what do we do? Let’s inspect the types and see what we can do.throw[τ0] (something of type τ ) to k (...this will have type τ0...)f (applied to something of type τ0) (...this will have type τ ...)Finally, we know we want to return a value of type τ0cont, and there is onlyone way to create such a value:callcc k’ => (something of type τ0) endLet’s start from the end and work backwards. The k’ above holds the valuewe’d like to return, but we can’t simply writecallcc k’ => k’ end(Remember from lecture that such an expression is not well-typed.)So how else can we save the continuation (and return it later)? Well, theonly other thing we can do with a continuation is to throw it!callcc k’ => throw[τ0] k’ to ? end(Why do we give the throw expression type τ0?) Of course, we need somewhereto throw this continuation, so let’s use another callcc.callcc ret => ... callcc k’ => throw[τ0] k’ to ret end endNow that we have captured the continuation we want, let’s go back and considerwhat we’d do if someone actually threw to it. First we’d apply f:callcc ret => ... f (callcc k’ => throw[τ0] k’ to ret end) endWhat remains? We have only to throw some value of type τ to k. The resultof the application of f is just such value.3fn f : τ0-> τ => fn k : τ cont =>callcc ret =>throw[τ0cont] (f (callcc k’ => throw[τ0] k’ to ret end))to kend(Convince yourself that this function typechecks. What’s the type of ret?(τ0cont cont) Finally, does compose ever return? Did we ever expect it to?)Clearly, we could not accomplish a feat such as compose with exceptions!1.4 ThreadsYou saw briefly in lecture how to make a ‘cooperative’ threading library usingcallcc. We’ll review it.The primitives we want are described by the signaturesigval fork : (unit -> unit) -> unitval yield : unit -> unitval exit : unit -> ’aendfork takes a function and starts executing it in a new thread, putting the currentthread to sleep. When it wakes up, it will continue executing from where thefork ended. yield simply puts the current thread to sleep, which will continueexecuting from after the yield when it wakes back up again. exit terminatesthe current thread.What callcc is used for is to express the idea of ‘where I should startexecuting again once I’m woken up’. throw is used to actually wake up athread.The signature of the queue that holds all our threads looks like this:sigtype ’a queueval new : unit -> ’a queueval enqueue : ’a queue * ’a -> unitval dequeue : ’a queue -> ’aval clear : ’a queue -> unitendPretty straightforward.Now we can start coding up the thread library itself. What a thread is goingto be is a continuation that receives no data in particular, i.e. unit:structure T :> THREADS =struct4type thread = unit cont...Initializing the queue is trivial:...val readyQueue : thread Q.queue = Q.new ()...Now we’re going to need a pair of functions that accomplishe ‘start runningthe next runnable thread.’ and ‘make the following a runnable thread’. Thefirst means waking it up by throwing it a value of the type of continuation thatit is, which is unit, so we throw it (). The second is simply enqueueing thegiven thread, which is a unit continuation: it must have come from a callccsomewhere....fun dispatch () =letval t = Q.dequeue readyQueuehandle Q.Dequeue => raise NoRunnableThreadsinthrow t ()endfun enq t = Q.enqueue (readyQueue, t)...Now here comes the actual guts of the thread library. Look how simple theyare! Notice how yield is a special case of fork: It’s the forking-off of the emptyjob....fun exit () = dispatch ()fun fork f