Which simplest evaluation model explains call/cc?

Question

TL;DR: What does call/cc do, (semi-)formally speaking?

The long version: I'm vaguely familiar with continuations and call/cc, but I don't have a strong formal understanding. I would like one.

In the SICP video lectures we are presented with the substitution model and a metacircular interpreter. In Shriram Krishnamurti's programming language course we are shown an environment-and-store-passing style. In the compiler course I took in uni I evaluated Java expressions by manipulating a stack.

What's the simplest evaluation model in which call/cc can be expressed, and how do you express call/cc in it?

Answer 1

I found this excellent presentation (in German), which answered my question: https://www.youtube.com/watch?v=iuaM9-PX1ls

To evaluate the lambda calculus with call/CC, you pass around an evaluation context consisting of an environment (as usual) and a call stack. A call to call/cc creates a special function-like continuation object which stores the evaluation context. The result of applying the special object to an expression expr is the result of interpreting expr in the evaluation context captured in the continuation object.

TL;DR: you can implement call/cc with an environment-and-call-stack-passing interpreter.

If you want to also thread around a mutable store the continuation objects should not capture it. Rather, when invoking a continuation you pass the store as an argument to the interpretation in the restored evaluation context. (The store can be of a linear type.)

Here is one such implementation in Haskell. Here's a sample expression you may want to evaluate: interpret 0 (Application (Lambda (1, (CallCC (Lambda (2, (Application (Variable 2) (Lambda (3, (Variable 4))))))))) (Lambda (4, (Variable 5)))).

(The numbers are just plain old names, not (e.g.) De Bruijn indices. If you wish to use characters or strings, change type Name = Integer to type Name = Char.)

Note especially interp applied to CallCC and InvokeContinuation as well as continue applied to ContinuationArgument.

import qualified Data.Map as Map

type Name = Integer
type NameAndBody = (Name, LambdaCallCC)
data LambdaCallCC
  = Lambda NameAndBody
  | Variable Name
  | InvokeContinuation EvaluationContext LambdaCallCC
  | CallCC LambdaCallCC
  | Application LambdaCallCC LambdaCallCC
  deriving Show

type Environment = Map.Map Name NameAndBody

type EvaluationContext = (CallStack, Environment)
type CallStack = [Frame]

data Frame
  = FunctionPosition LambdaCallCC
  | ArgumentPosition NameAndBody
  | ContinuationArgument EvaluationContext
  deriving Show

type Fail = (Name, EvaluationContext)
interpret :: Name -> LambdaCallCC -> Either Fail NameAndBody
interpret thunkVarName expression = interp [] Map.empty expression
  where interp stk env (Lambda nameAndBody)
          = continue stk env nameAndBody
        interp stk env (Variable name)
          = case Map.lookup name env of
              Nothing -> Left (name, (stk, env))
              Just e -> continue stk env e
        interp stk env (Application e1 e2)
          = interp (FunctionPosition e2 : stk) env e1
        interp stk env (CallCC expr)
          = interp stk env (Application expr
                              (Lambda (thunkVarName,
                                        (InvokeContinuation
                                          (stk, env)
                                          (Variable thunkVarName)))))
        interp stk env (InvokeContinuation capturedContext expr)
          = interp [ContinuationArgument capturedContext] env expr

        continue [] env value
          = Right value
        continue ((FunctionPosition expr) : frames) env value
          = interp ((ArgumentPosition value) : frames) env expr
        continue ((ArgumentPosition (name, body)) : frames) env value
          = interp frames (Map.insert name value env) body
        continue ((ContinuationArgument (stk, env)) : nil) _ value
          = interp stk env (Lambda value)

Answer 2

TL;DR call/cc lets you tap into Schemes internal code so that you can use continuations without writing your code in continuation passing style. The best evaluation model is the substitution model given that you don't use set and view it from CPS code

Imagine this little program.

(define (sum-list lst)
  (cond ((null? lst) 0)
        ((number? (car lst)) (+ (car lst) (sum-list (cdr lsr))))
        (else (sum-list (cdr lsr)))))

(display (sum-list '(1 2 3 4))) ; displays 10

Imagine you want the result to be 1337 if you hit the else term. How would you go about that without rewriting the whole thing? You can't. However most Scheme implementation does CPS conversion to your code where changing it is trivial:

(define (sum-list& lst k)
  (null?& lst
          (lambda (nlst?)
            (if& nlst?
                 (lambda ()
                   (k 0))
                 (lambda ()
                   (car& lst
                         (lambda (car-lst)
                           (number?& car-lst
                                     (lambda (ncl?)
                                       (if& ncl?
                                            (lambda ()
                                              (cdr& lst
                                                    (lambda (clst)
                                                      (sum-list& clst
                                                                 (lambda (sclst)
                                                                   (+& car-lst sclst k))))))
                                            (lambda ()
                                              (cdr& lst
                                                    (lambda (clst)
                                                      (sum-list& clst k))))))))))))))
(sum-list& '(1 2 3 4)
           (lambda (sum)
             (display& sum halt)))

cond is a macro so it is the if& calls you see. I know what you're thinking. Why not tell the programmers to do it like this in the first place? Just kidding!

If you change the second continuation in the second if& to (lambda () (k 1337)) you're done. As beautiful as CPS is it is horrible to read and write, but since the compiler does this anyway couldn't there be a way to be able to write your code in the first way and still get to code control flow? The best of two worlds is enabled with call/cc. call/cc is this in CPS:

(define (call/cc& f& continuation)
  (define (exit& value actual-continuation)
    (continuation value))
  (f& exit& continuation))

It doesn't do much at all. It passes exit& which ignores the real continuation of the program when called and calls the value with the original continuation of the call/cc& call. With the list '(1 2 3 #f) you'd have 3 nested continuations waiting to add with the result but all of that needs to be cancelled. If you get to choose the value of the continuation before that calculation it automatically is cancelled. And that is it. When you write your code with it you don't need to do full CPS, only the continuation you want thought call/cc like this:

(define (sum-list lst)
  (call/cc
   (lambda (k)
     (define (helper lst)
       (cond ((null? lst) 0)
             ((number? (car lst))
              (+ (car lst) (helper (cdr lst))))
             (else (k 1337))))
     (helper lst))))

This gets transformed to this in CPS:

(define (sum-list& lst k)
  (call/cc&
   (lambda (k& real-k)
     (define (helper& lst k)
       (null?& lst
               (lambda (nlst?)
                 (if& nlst?
                      (lambda ()
                        (k 0))
                      (lambda ()
                        (car& lst
                              (lambda (car-lst)
                                (number?& car-lst
                                          (lambda (ncl?)
                                            (if& ncl?
                                                 (lambda ()
                                                   (cdr& lst
                                                         (lambda (clst)
                                                           (helper& clst
                                                                    (lambda (sclst)
                                                                      (+& car-lst sclst k))))))
                                                 (lambda ()
                                                   (k& 1337 real-k))))))))))))
     (helper& lst real-k))
     k))


(sum-list& '(1 2 3 4)
           (lambda (sum)
             (display& sum halt)))

call/cc can always be avoided. Our example could have been rewritten to return 1337 like this:

(define (sum-list lst)
  (define (helper lst sum)
    (cond ((null? lst) sum)
          ((number? (car lst)) (helper (cdr lst) (+ sum (car lst))))
          (else 1337)))
  (helper lst 0))

This is tail recursive and instead of creating continuations it accumulates. For completeness here is the CPS version of it:

(define (helper& lst sum k)
  (null?& lst
          (lambda (nlst)
            (if& nlst
                 (lambda () (k sum))
                 (lambda ()
                   (car& lst
                       (lambda (cl)
                         (number?& cl
                                 (lambda (ncl?)
                                   (if& ncl?
                                        (lambda ()
                                          (cdr& lst
                                                (lambda (cdrl)
                                                  (+& sum
                                                      cl
                                                      (lambda (scl)
                                                        (helper& cdrl
                                                                 scl
                                                                 k))))))
                                        (lambda () (k 1337))))))))))))


(define (sum-list& lst k)
  (helper& lst 0 k))