Capture Checking / Separation Checking 入門

Scala わいわい勉強会 #6 (2025-11-27)

- Capture Checkinga | Scala 3 Reference https://docs.scala-lang.org/scala3/reference/experimental/cc.html
- Separation Checking | Scala 3 Reference https://dotty.epfl.ch/docs/reference/experimental/capture-checking/separation-checking.html
- System Capybara: Capture Tracking for Ownership and Borrowing | ICFP/SPLASH'25
- https://2025.workshop.scala-lang.org/details/scala-2025/6/System-Capybara-Capture-Tracking-for-Ownership-and-Borrowing
- https://www.youtube.com/live/D4uQiayHmv0?si=Hbfv_ZVvWGo3TcF-&t=4036
- Capture Checking project page https://capless.cc/

実行例: https://github.com/tanishiking/kitchensink/tree/main/scala3-cc

Transcript

1. Capture Checking / Separation Checking 入門 Scala わいわい勉強会 #6 (2025-11-27) @tanishiking Scala わいわい勉強会主催 Scala Compiler Engineer @ VirtusLab
2. Capture って何? class Counter extends Capability: def inc(): Counter = ??? def main(): val c = new Counter val increment = () => { c.inc() } increment() 一旦無視して Closure外で定義された値 (c)を参照している。 Increment は c を capture
3. Capturing Types T^{ x 1 ,⋯, x n } Capture Set: この型の値が キャプチャできる値の上限 Shape Type: 普通の型 val c = new Counter val increment: (() -> Unit)^{c} = () => { c.inc() } () => Unit な関数型で c をキャプチャする。() ->{c} Unit とも書ける
4. Capture Checking val c1: Counter^ = new Counter val c2: Counter^ = new Counter val increment: (() -> Unit)^{c1} = () => { c1.inc() c2.inc() } (c2 : Counter^) cannot be referenced here; it is not included in the allowed capture set {c1} of an enclosing function literal with expected type () ->{c1} Unit Error! increment がキャプチャ 可能な値の集合 Capture set はその値がアクセス可能な capabilities という捉え方もできる
5. val c: Counter^ = new Counter val ls: MyList[Int] = ??? Ls.map { x => c.inc(); x + c.get() } 例: 参照透過なクロージャ enum MyList[+A]: def map[B](f: A ->{} B): MyList[B] = ??? map の引数である関数f は値を キャプチャすることを拒否 Error! c は f: A ->{} B の capture set に 含まれないのでエラー 公式サイトに他にも例あり
6. Alias Tracking val a: Counter^{c} = c val increment: (() -> Unit)^{c} = () => { a.inc() } a は c への alias をもつことが型レベルで分かる キャプチャしているのは a だが、 a は c の alias だとわかっているので、 capturing型は (() -> Unit)^{c}
7. 発展: Separation Checking class Ref(init: Int) extends Mutable: private var current = init def get: Int = current update def set(x: Int): Unit = current = x def read(r: Ref): Int = { r.set(0); r.get } def update(r: Ref^, value: Int): Unit = r.set(value) Cannot call update method set of r since its capture set {r} is read-only. Error! Ref = Ref^{cap.rd}: 読み取り専用のcapabilityのみをもつ Ref^: 任意のcapabilityを持つ(書き込み可能)
8. 発展: Separation Checking def par[A, B](f: () => A, g: () => B): (A, B) par( () => r.set(2), () => r.set(3) ) Error! 2つの引数が同じ値をcaptureすることを 禁止 () -> {r} Unit par( () => println(r.get), () => println(r.get) ) OK 読み取り専用同士ならOK () -> {cap.rd} Unit
9. 発展: 所有権っぽいやつ def inplaceUpdate(consume a: Ref^, value: Int): Ref^ = a.set(value) a val r = Ref(0) val newRef = inplaceUpdate(r, 100) read(r) Error! r へのアクセス capability は inplaceUpdate に移ったので ここで r を参照できない
10. 参考資料など 1. Capture Checkinga | Scala 3 Reference a. https://docs.scala-lang.org/scala3/reference/experimental/cc.html 2. Separation Checking | Scala 3 Reference a. https://dotty.epfl.ch/docs/reference/experimental/capture-checking/separation-checking.html 3. System Capybara: Capture Tracking for Ownership and Borrowing | ICFP/SPLASH'25 a. https://2025.workshop.scala-lang.org/details/scala-2025/6/System-Capybara-Capture-Trac king-for-Ownership-and-Borrowing b. https://www.youtube.com/live/D4uQiayHmv0?si=Hbfv_ZVvWGo3TcF-&t=4036 4. Capture Checking project page a. https://capless.cc/ 実行例: https://github.com/tanishiking/kitchensink/tree/main/scala3-cc