Resumption Counts and Ownership

Combine multi-shot continuations with affine and linear resources.

10.1 Four resumption quantities

An effect declaration determines how often the handler may call the continuation k.

The default is <=1. Write resume ω only when repeated resumption is needed. The quantity follows the result type in an effect's signature.

effect ask(q: Text): i64                 // resume <=1 (default)
effect choose(): Bool resume ω           // multi-shot
effect fail(msg: Text): Never resume 0   // never resume
effect step(): () resume 1               // resume exactly once

10.2 Express nondeterminism

effect choose(): i64 resume ω

fn pair_sum(): i64 {
  let a := perform choose()
  let b := perform choose()
  a * 10 + b
}

let total := handle { pair_sum() } with {
  choose(), k => k(1) + k(2)
  return v => v
}
perform show("total", total)

// Explore both choices at each operation and add all four outcomes.

・ pair_sum

total = 66

total = 66

The first choose receives both 1 and 2, and the second receives both values in each branch. This produces 11, 12, 21, and 22, whose sum is 66. Unlike an ordinary if, this executes the remaining computation itself several times.

10.3 Why resumption interacts with ownership

If a continuation that runs twice owned an affine file handle, it would use the same resource twice. Tauto restricts nonduplicable values that remain alive across effects permitting repeated resumption.

import std::prelude::Affine

effect choose(): Bool resume ω

let c := handle {
  var w := Vec::new()
  Vec::push(&mut w, 1)
  if perform choose() { Vec::len(&w) } else { 0 }
} with {
  choose(), k => k(true) + k(false)
}
perform show("c", c)

// This deliberately keeps an affine vector alive across multi-shot resumption.

error 8:6: w is live across choose, which resumes ω

ch10-live-across.taut:8:6: use error: w is live across choose, which resumes ω

The vector w remains alive across choose, whose quantity is ω, so the checker rejects the program. Move w's declaration outside handle and use only &w in its body to make it acceptable.

Similarly, placing a linear value in a continuation that may be discarded breaks the requirement to use it exactly once. A resumption quantity describes control flow in a form ownership checking can understand.

The combinations of live values and quantities are:

Think about it: Which is harder to combine with a linear resource: a handler that discards its continuation on failure, or one that resumes twice? Use the table to explain your answer.