Continuing with Continuations

6.S050

Jack Feser

Created: 2023-05-11 Thu 11:06

Fibonacci revisited

function fib(n) {
  if (n == 0) { return 0; }
  if (n == 1) { return 1; }
  return fib(n - 1) + fib(n - 2);
}

Fibonacci revisited

function fib(n) {
  if (n == 0) { return 0; }
  if (n == 1) { return 1; }
  return fib(n - 1) + fib(n - 2);
}


function fib_let(n) {
  if (n == 0) { return 0; }
  else if (n == 1) { return 1; }
  else {
    let a = fib_let(n - 1);
    let b = fib_let(n - 2);
    return a + b;
  }
}

Fibonacci revisited

function fib_let(n) {
  if (n == 0) { return 0; }
  else if (n == 1) { return 1; }
  else {
    let a = fib_let(n - 1);
    let b = fib_let(n - 2);
    return a + b;
  }
}


function fib_cps (n, k) {
  if (n == 0) { k(0); }
  else if (n == 1) { k(1); }
  else {
    fib_cps(n - 1, function(a) {
    fib_cps(n - 2, function(b) {
      k(a + b);
    })
    });
  }
}

Fibonacci revisited

function fib_cps (n, k) {
  if (n == 0) { k(0); }
  else if (n == 1) { k(1); }
  else {
    fib_cps(n - 1, function(a) {
    fib_cps(n - 2, function(b) {
      k(a + b);
    })
    });
  }
}

fib_cps(8, function(x) { console.log(x); });

21

Back to while and break

Evaluation relations:

  • \(\langle \text{Statement}, \text{Store} \rangle \Downarrow \text{Store}\)
  • \(\langle \text{Expression}, \text{Store} \rangle \Downarrow_e \text{Value}\)
\begin{gather*} \frac{ \langle e, \sigma \rangle \Downarrow_e \texttt{true} \quad \langle s, \sigma \rangle \Downarrow \sigma' \quad \langle \texttt{while}\ e\ \texttt{do}\ s, \sigma' \rangle \Downarrow \sigma'' \quad }{ \langle \texttt{while}\ e\ \texttt{do}\ s, \sigma \rangle \Downarrow \sigma'' } \\\\ \frac{ \langle e, \sigma \rangle \Downarrow_e \texttt{false} }{ \langle \texttt{while}\ e\ \texttt{do}\ s, \sigma \rangle \Downarrow \sigma } \end{gather*}

Adding break to IMP

Evaluation relations:

  • \(\langle \text{Statement}, \text{Store} \rangle \Downarrow \langle \text{DidBreak?}, \text{Store} \rangle\)
\begin{gather*} \langle \texttt{break}, \sigma \rangle \Downarrow \langle \texttt{true}, \sigma \rangle \end{gather*}

Adding break to IMP

\begin{gather*} \frac{ \langle e, \sigma \rangle \Downarrow_e \texttt{true} \quad \langle s, \sigma \rangle \Downarrow \langle \texttt{false}, \sigma' \rangle \quad \langle \texttt{while}\ e\ \texttt{do}\ s, \sigma' \rangle \Downarrow c \quad }{ \langle \texttt{while}\ e\ \texttt{do}\ s, \sigma \rangle \Downarrow c } \\\\ \frac{ \langle e, \sigma \rangle \Downarrow_e \texttt{true} \quad \langle s, \sigma \rangle \Downarrow \langle \texttt{true}, \sigma' \rangle }{ \langle \texttt{while}\ e\ \texttt{do}\ s, \sigma \rangle \Downarrow \langle \texttt{false}, \sigma' \rangle } \\\\ \frac{ \langle e, \sigma \rangle \Downarrow_e \texttt{false} }{ \langle \texttt{while}\ e\ \texttt{do}\ s, \sigma \rangle \Downarrow \langle \texttt{false}, \sigma \rangle } \end{gather*}

Adding break to IMP

\begin{gather*} \frac{ \langle s, \sigma \rangle \Downarrow \langle \texttt{false}, \sigma' \rangle \quad \langle s', \sigma' \rangle \Downarrow c }{ \langle s; s', \sigma \rangle \Downarrow c } \\\\ \frac{ \langle s, \sigma \rangle \Downarrow \langle \texttt{true}, \sigma' \rangle }{ \langle s; s', \sigma \rangle \Downarrow \langle \texttt{true}, \sigma' \rangle } \end{gather*}

First-class continuations: The functional goto

  • We've seen "continuation passing style"
    • Manual, can be difficult to write & maintain
  • Can we do better?
    • Can we get access to the "current continuation"? What could we do then?

call/cc

call-with-current-continuation or call/cc

call/cc by example

1 + (call/cc
       (fun k -> 2 + (k 3))

call/cc is a bit weird:

  • k isn't really a function—it doesn't return!
  • call/cc is "unbounded": it captures the whole program as a continuation

Delimited control

What if we could capture only part of the continuation? Enter shift and reset. 

2 * (reset (1 + (shift k (k 5))))

What is k here? The continuation up to the first reset. 

1 + []

So, computation is then: 

2 * (1 + 5)

Delimited control

What about the following? 

2 * (reset (1 + (shift k (k 5 + k 6))))

Semantics of delimited control

\begin{align*} &\texttt{reset}\ v \rightarrow v \\ &\texttt{reset}\ C[\texttt{shift}\ k\ body] \rightarrow \\ &\quad \texttt{reset}\ ((\lambda k.\ body) (\lambda x.\ \texttt{reset}\ E[x])) \end{align*}

Can write the second rule as:

\begin{align*} &\texttt{reset}\ C[\texttt{shift}\ k\ body] \rightarrow \\ &\quad\texttt{reset}\ (\texttt{let}\ k = \lambda x.\ \texttt{reset}\ E[x]\ \texttt{in}\ body) \end{align*}

First-class continuations: control not state

Say you're in the kitchen in front of the refrigerator, thinking about a sandwich. You take a continuation right there and stick it in your pocket. Then you get some turkey and bread out of the refrigerator and make yourself a sandwich, which is now sitting on the counter. You invoke the continuation in your pocket, and you find yourself standing in front of the refrigerator again, thinking about a sandwich. But fortunately, there's a sandwich on the counter, and all the materials used to make it are gone. So you eat it. :-)

Source