Control

Motivating Questions

• What kind of control constructs should we use?
  • Seen while, for, if, function calls
• Are our control constructs sufficiently expressive?
  • Why not use goto?
• How should we think about non-local control?
  • Exceptions, co-routines, concurrency, backtracking

Adding break to IMP: Original (big-step) semantics

Evaluation relations:

• \(\langle \text{Statement}, \text{Store} \rangle \Downarrow \text{Store}\)
• \(\langle \text{Expression}, \text{Store} \rangle \Downarrow_e \text{Value}\)

Adding break to IMP

Adding break to IMP

Evaluation relations:

• \(\langle \text{Statement}, \text{Store} \rangle \Downarrow \langle \text{DidBreak?}, \text{Store} \rangle\)

Adding break to IMP

Adding break to IMP: What about the other rules?

Everything else needs to change…

Now try adding continue…

Non-local control flow

• Early exit from procedures, loops
• Nonlocal exits (i.e setjmp=/=longjmp)
• goto
• Exceptions
• Coroutines (i.e. Python's generators)
• Backtracking

Control transfers to something other than the next statement

Continuations

Explicit representation of the "rest" of a computation

Continuations: Example

• \(E = (1 * 2) + 5\)
• \(E = C[1 * 2]\), where \(C = □ + 5\)
• Continuation, or "rest of computation", for \(1 * 2\): \(\lambda x.\ x + 5\)
• Model continuations as procedures
• Take evaluation context and abstract over the hole

Continuation-passing style (CPS)

Represent continuation explicitly as parameter \(k\)

let rec fact n =
  if n = 0 then 1 else n * (fact (n - 1))

let rec fact_cps n k =
  if n = 0
  then k 1
  else fact_cps (n - 1) (fun x -> k (n * x))

What is CPS good for?

• Can implement more sophisticated control flow patterns
• And we can do it in the language!

Example: Multi-value returns

type tree = Leaf of int | Node of tree * tree

let rec sum = function
  | Leaf x -> x
  | Node (t, t') -> sum t + sum t'

let rec height = function
  | Leaf _ -> 0
  | Node (t, t') -> 1 + (max (height t) + (height t'))

let rec sum_times_height t = sum t * height t

Can we do this in one pass over the tree?

Example: Multi-value returns

type tree = Leaf of int | Node of tree * tree

let sum_times_height t =
  let rec inner t = match t with
    | Leaf x -> (0, x)
    | Node (t, t') ->
       let (s, h) = inner t in
       let (s', h') = inner t' in
       (s + s', 1 + (max h h'))
  in
  let (s, h) = inner t in
  s * h

What if the tree is very tall? Should we worry about overflowing the stack?

Example: Multi-value returns

type tree = Leaf of int | Node of tree * tree

let sum_times_height t =
  let rec inner t k = match t with
    | Leaf x -> k 0 x
    | Node (t, t') ->
       inner t (fun s h ->
	   inner t' (fun s' h' ->
	       k (s + s') (1 + (max h h'))))
  in
  inner t (fun s h -> s * h)

Practice: Fibonacci

Translate this function to CPS

let rec fib n = match n with
  | 0 -> 0
  | 1 -> 1
  | n -> fib (n - 1) + fib (n - 2)

Practice: Fibonacci

Solution:

let rec fib n = match n with
  | 0 -> 0
  | 1 -> 1
  | n -> fib (n - 1) + fib (n - 2)

let rec fib_cps n k = match n with
  | 0 -> k 0
  | 1 -> k 1
  | n -> fib (n - 1) (fun x ->
	     fib (n - 2) (fun x' ->
		 k (x + x')))

Example: Non-local exits

(Similar to early returns in imperative languages.)

type tree = Leaf of int | Node of tree * tree

let rec tree_product t = match t with
  | Leaf x -> x
  | Node (t, t') -> (tree_product t) * (tree_product t')

What if a leaf is zero? Can we avoid doing the rest of the work?

Example: Non-local exits

First translate to CPS

type tree = Leaf of int | Node of tree * tree

let rec tree_product t k = match t with
  | Leaf x -> k x
  | Node (t, t') ->
     tree_product t (fun x ->
	 tree_product t' (fun x' -> k (x * x')))

Example: Non-local exits

Separate the "early return" continuation from "keep processing" continuation

type tree = Leaf of int | Node of tree * tree

let tree_product t k_early_return =
  let rec prod t k =
    match t with
    | Leaf 0 -> k_early_return 0
    | Leaf x -> k x
    | Node (t, t') ->
       tree_product t (fun x ->
	   tree_product t' (fun x' -> k (x * x')))
  in
  prod t k_early_return

Note that this will "return" from multiple nested calls

Mechanization

CPS conversion can be done automatically:

Source

Mechanization example