[SOLVED] Which simplest evaluation model explains call/cc?

Which simplest evaluation model explains call/cc?

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?

Solution

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)