scala/Capture Checking

#scala #scala3

! このページの記述はたぶん間違えています。著者もぜんぜん分かっていないのを調べながら書いているページです

Scala 3.2.1あたりからexperimentalで導入された機能。

Scalaの型システムに修正を加え、ある種の操作を不可能にすることで安全性を高めるという機構が追加される。

例1

Scala 3のCapture Checkingでローンを確実に返済！ - xuwei-k's blogを改変した例

一時ファイルを作ってその上で作業できる関数withTempFileがあるとする

code:scala

//> using scala 3.5.1

//> using dep "com.lihaoyi::os-lib:0.11.3"

def withTempFileA(body: os.Path => A): A =

val tempFile = os.temp()

try

body(tempFile)

finally

os.remove(tempFile)

withTempFile(f => println(s"I have $f"))

実行すると・・・

code:sh

I have /tmp/8906984965225497605.tmp

ところで、この↓コードって意味ある？

code:scala

val p = withTempFile(identity)

identityはあらゆる型Aを受け取り、それをそのまま返すだけの関数

つまり、内部のtempFileがそのまま取り出される

しかし、withTempFileが完了したタイミングでこのファイルはfinally節によって削除されている

code:scala

//> using scala 3.5.1

//> using dep "com.lihaoyi::os-lib:0.11.3"

def withTempFileA(body: os.Path => A): A =

val tempFile = os.temp()

try

body(tempFile)

finally

os.remove(tempFile)

val p = withTempFile(identity)

val crash = os.read(p)

実際、これを実行するとクラッシュする

code:sh

Exception in thread "main" java.nio.file.NoSuchFileException: /tmp/16212483105167079882.tmp

at java.base/sun.nio.fs.UnixException.translateToIOException(UnixException.java:92)

at java.base/sun.nio.fs.UnixException.rethrowAsIOException(UnixException.java:106)

at java.base/sun.nio.fs.UnixException.rethrowAsIOException(UnixException.java:111)

at java.base/sun.nio.fs.UnixFileSystemProvider.newByteChannel(UnixFileSystemProvider.java:219)

内部のなんらかの値が外側に返されるのを防ぐことは、現行のScalaの型システムでは不可能

Capture Checkingでは、型に^をつけることで、その値を返せなくできる

code:scala

//> using scala 3.5.1

//> using dep "com.lihaoyi::os-lib:0.11.3"

// 通常のScalaファイルでは↓をimportすればよいが、scala scriptなのでうまくいかない。

// ファイル名を.scala.scから.scalaにすることで解消した

import language.experimental.captureChecking

def withTempFileA(body: os.Path^ => A): A = // os.Path^になっている

val tempFile = os.temp()

try

body(tempFile)

finally

os.remove(tempFile)

def main() =

val p = withTempFile(identity)

val crash = os.read(p)

実行するとコンパイルを拒否される

code:sh

error ./script.scala:16:24

error Found: (x: os.Path^?) ->? box os.Path^?

error Required: (x: os.Path^) => box os.Path^?

error

error Note that the universal capability cap

error cannot be included in capture set ?

error val p = withTempFile(identity)

error ^^^^^^^^

Error compiling project (Scala 3.5.1, JVM (17))

Compilation failed

どう考えたらいい？

いったん意味の話は棄てて、こういう基本ルールがありますという話をします

Capture Checkingの登場人物: capturing types(捕捉型), capture set(捕捉セット), capability(能力)

定訳はなさそうなので適当に訳している

capturing types

文法上: A^{x, ...}の形になっている型

A^はA^{cap}のエイリアスである

A^{}は何もcapabilityを持たない

capture set

文法上: A^{x, y, z}における、{x, y, z}の部分

setという名前の通り、集合のように振る舞う

capability

文法上: A^{x, y, z}における、x、y、zのこと

ここには型ではなく値が入る

capabilityになれるのは、ローカル変数、パラメータ、thisのみ

capabilityになれるのは、capturing typesであるような値のみ

?capturing typesがなければ、capabilityを作れず、capture setも作れず、capturing typesが作れないのでは？

!A^とA^{}はcapabilityを示さずに作れる

型が値の情報を持っていて、値もまたcapturing typesなので、また別の値を追跡する、という構造になっている

Capturing typesも通常の型システム同様にチェックされる

Capturing typesが要求されている場所で、適合しないcapturing typesがやってきた場合はコンパイルエラーにする

capture setには大小関係があり、これが型チェックに援用される

ここでは普通の型と同じように、capture set aが capture set bより小さいことをa <: bと書きます

A^a型が求められているとき、B^b型があり、B <: Aでないとき

そもそも別の型なので失敗する

A^a型が求められているとき、B^b型があり、B <: Aであるとき

b <: aのとき

Capture checking成功!!

そうではないとき

Capture checking失敗!!

大小関係どう決めるの？

{cap}: 一番デカいcapture set。全てのcapabilityを詰めたcapture setとみなす

通常の型でいうとAnyみたいなやつや

{}: 一番小さいcapture set。一切のcapabilityを持っていないcapture set。

通常の型でいうとNothingみたいなやつや

例えば{} <: {x} <: {x, y} <: {x, y, z}: <: {cap}みたいな感じ

基本ルールを覚えたところで、実用の話に戻ります

Capture Checkingはcapturing typesに対してしかチェックされない

JavaScriptのawaitみたいに、後付けでメリットだけ享受できるということ

capturing typesでない型がcapturing typesとかかわった場合、一般に安全な方向に倒される

値 x: A^{cap}があるとき、これはB^{x}か、これよりも大きなcapture setの型にしか入らない

値 x: A^{}があるとき、これはA^{...}を求めている型のどこにでも入れる

呼び出したcapturing typesに対して何も影響を与えない

このようなcapturing typesはPure(純粋)である、と呼ばれる

この基本的な制約をもとに応用的なユースケースが開発される

応用: リソース管理

以下のようなメソッドを考える

入口で引数にcapturing typeを設定する

出口ではその引数をcapturing typeに含めない

コードでは以下のような形:

code:scala

def useFooA(x: A^) = {

}

こうするとuseFooの返り値の型は通常通りAに推論される

A^{}と同じにされる

しかし返されているxの型A^はcapture set{cap}を持っている

{cap} <: {}は成り立たないのでコンパイル失敗する

これにより、特定の型がスコープの外に脱出してしまうことを絶対に回避できる

もうちょっと複雑な例として冒頭の例が出てくる

code:scala

def withTempFileA(body: os.Path^ => A): A =

val tempFile = os.temp()

try body(tempFile)

finally os.remove(tempFile)

val p = withTempFile(identity) // コンパイルしない

withTempFileは、一時ファイルを作ってbodyにそれを渡し、bodyの実行が終了したら一時ファイルを破壊する

がしかし、identityを渡すことで一時ファイルを向いたos.Pathを取り出せてしまう

ここでos.Pathをcapturing typeにし(os.Path^とし)、返り値の型をAのままにすることで、os.Pathをそのまま返そうとしたときにcapture checkingの検査が失敗するように仕向けられる

応用: ライフタイム管理

直接参照していなくても、型レベルで互いの値を依存させることができる

foo: Bar^{buzz}: fooのライフタイムはbuzzと一致しなければならない

ライフタイムが一致しているということは利用できる(capable)なので、{}の中身に入れられるやつはケイパビリティ(capability)と呼ばれる

また、このときfooもcapabilityになる

A^{x, y}のようになっているとき、xもyもcapabilityである必要あある

A^はA^{cap}の略記

capは「他のあらゆる値」なので、あらゆる値をキャプチャできる

事実上、「プログラム全体」のライフタイムと同期する、ということを言っているのと同じなので、何も制約を受けない

何の制約もなくAに対してA^できるので、追跡の起点として使われる

なにも^をつけない型はそもそも最初からCapture Checkerの検査対象にならない

^をつけることで、Capture Checkerを起動する

A^{}、つまりケイパビリティを一切持たない型は純粋(pure)であると呼ばれる。

ケイパビリティを一切持たない関数も考えられる。これはすなわち純粋な関数とみなせる。これをA -> Bのように書く。

関数にケイパビリティを持たせるにはA ->{foo} Bのように書ける。

より厳密にA{foo} -> BとかA -> B{foo}のようにも書ける。

ケイパビリティは型のように大小関係を持つので、純粋な関数はどこに入れてもよい

code:scala

//> using scala 3.5.1

import language.experimental.captureChecking

val double: Int -> Int = _ * 2

def makePairA(a: A^): (A^{a}, A^{a}) = (a, a)

def applyA, B(a: A^)(f: A^ ->{a} B) = f(a)

def pureApplyA, B(a: A)(f: A -> B): B^{} = f(a)

object Main extends App:

println(apply(42)(double))

println(pureApply(42)(double))

println(apply("foo")(makePair))

println(pureApply("foo")(makePair))

検査例外への転用

https://dotty.epfl.ch/docs/reference/experimental/cc#checked-exceptions-1

Capture Checkingがもたらす制約は検査例外にも転用できる

In the effects as capabilities model, an effect is expressed as an (implicit) parameter of a certain type. For exceptions we would expect parameters of type CanThrowE where E stands for the exception that can be thrown.

throws Eで定義された関数は、CanThrow[E]をcontext parameterとして受け取る形に展開される

code:scala

import language.experimental.saferExceptions

class NegativeParameterException extends Exception

def repeat(s: String, n: Int): String throws NegativeParameterException =

n match {

case n if n < 0 => throw NegativeParameterException()

case n => s.repeat(n)

}

ここでrepeatの型は(String, Int) => CanThrow[NegativeParameterException] ?=> Stringになる

つまりdef repeat(s: String, n: Int)(using CanThrow[NegativeParameterException]): Stringしたのと同じ

じゃあCanThrowは誰が供給するのかというと、catchすると供給されるようになる

Scalaではusingでコンテキストが得られなかった場合のエラーメッセージもカスタマイズできるので、これを利用して「ちゃんとハンドルしてね」というメッセージを出せる

それはそうと、例外を引き起こす能力がtry節から漏れ出してはいけない

code:scala

def repeat1(s: String, n: Int): () => String throws NegativeParameterException =

try () => repeat(s, n)

catch

case e: NegativeParameterException =>

() => throw NegativeParameterException() // これ自体は throws ...でエラーにならない

上掲のコードでは例外を起こす能力が漏れてしまう

repeat1("42", -1)()すると例外ハンドリングできていないのでクラッシュする

そこで、Capture Checkingがこれを追跡してエラーにする

CanThrow型はcapabilityとして定義される

tryの返り値の型がCanThrow型をcaptureすることを禁止する

エフェクトとしてのcapability