継続の回数と所有権

継続を何度も再開すること（multi-shot）と、affine / linear な資源を両立させます。

10.1 再開量は四種類

ハンドラに渡される継続 k を何回呼んでよいかは、effect の宣言が決めます。

書かなかったときの既定は <=1 です。何度でも再開する必要があるときだけ、resume ω と書きます。再開量は、署名の結果型のあとに書きます。

effect ask(q: Text): i64                 // resume <=1（既定）
effect choose(): Bool resume ω           // multi-shot
effect fail(msg: Text): Never resume 0   // 再開しない
effect step(): () resume 1               // ちょうど一度再開する

10.2 非決定性を表現する

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)

・ pair_sum

total = 66

total = 66

一度目の choose に 1 と 2 を与え、二度目にもそれぞれ 1 と 2 を与えるので、組み合わせは 11、12、21、22 の四つで、合計は 66 です。普通の if とは違って、残りの計算そのものを複数回走らせる表現です。

10.3 なぜ所有権と衝突するのか

もし affine なファイルハンドルを、二度実行される継続が所有していたら、同じ資源を二回使ってしまいます。Tauto は、多重に再開できる効果をまたいで生きている、複製できない値を制限します。

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)

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 ω

Vec の w が、choose（ω）をまたいで生きているので、検査が止めます。w の宣言を handle の外に出して、本体では &w だけを使えば通ります。

同様に、linear な値を、捨てられるかもしれない継続の中に置くと、「ちょうど一度使う」という約束を破ります。resume は、制御フローを、所有権の型が理解できる形にするための情報でもあります。

生きている値と再開量の組み合わせは、次のとおりです。

考えてみよう：失敗時に継続を捨てるハンドラと、継続を二回再開するハンドラでは、どちらが linear な資源と両立しにくいでしょうか。表を見て答えてください。