scala/Capture Checking

Capture Checking 何

型システムにもう一つ便利な機能つけたぞー

👓😫💥👊😡

Capture 何

スコープにないのに、後から使っているなら、captureしているといってよい

例

code:scala

case class TaxInfo(rate: Double)

val taxInfo = TaxInfo(0.1)

def calculateTax(x: Double): Double = x * taxInfo.rate

// calculateTax は taxInfo を capture している!!!

クロージャ(関数閉包)じゃん

クロージャがやっていることのうち、参照を持っていってしまうことをcaptureといっている

なんでCaptureをCheckしたいのか

リソース管理に有益だから

リソース管理でCapture Checkしたい

code:scala

//> using scala 3.5.1

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

val tempFile = os.temp()

try

body(tempFile)

finally

os.remove(tempFile)

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

よくある、acquire-use-releaseパターンを実現した便利なやつ

やった！安全だ！型システム最高だな〜

code:scala

val invalidFile = withTempFile(identity)

// => /tmp/8906984965225497605.tmp

ヨシ！

安全ちゃうやん！

何がいけなかったのか？

意図しない形で参照が逃げ出した(escape)のを防げなかった

なぜ参照が逃げてほしくないのか？

即座に無効になるから

セキュリティ的に機微だから

副作用の制御の観点から隔離したいから

実行時に分かってもしょうがないので、型レベルでなんとかチェックできないか〜

参照を逃がさない

参照が逃げないようにするためには、従来の型情報だけでは不十分

先程の例を再掲する

code:scala

case class TaxInfo(rate: Double)

val taxInfo = TaxInfo(0.1)

def calculateTax(x: Double): Double = x * taxInfo.rate

追加でいくつかの概念を導入するぞい

その型がcaptureしているべきもの(ローカル変数、パラメータ、this)は何？

e.g. calculateTax は taxInfo を capture している

複数の値をcaptureしていることがあるぞ

意味合い

ナニコレ？

後述

こうすると関数などの戻り値が何をcaptureしているかが型に載るようになる

Capture Checking

さて、(Capture Checkingが有効化された)コンパイラは、従来のサブタイピングに加えて以下のようにcapture setについてもサブタイプを判定するようになる

{} <: {x} <: {x, y} <: {x, y, z}: <: {cap}

また再掲

code:scala

val tempFile = os.temp()

try

body(tempFile)

finally

os.remove(tempFile)

すると、以下のような制御ができるようになるね

ただし:

どこからか、「ここからcapture checking有効です」と示す必要がある

例

https://scrapbox.io/files/68d501121283e39a4b3a7a61.png

https://scrapbox.io/files/68d50aa1fe4a7195f28a5b5c.png

https://scrapbox.io/files/68d50ac5bbe3e8d97ed871e5.png

------ ここから古い記述

hr.icon

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

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

例1

code:scala

//> using scala 3.5.1

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

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)

code:scala

//> using scala 3.5.1

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

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の型システムでは不可能

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

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 compiling project (Scala 3.5.1, JVM (17))

Compilation failed

どう考えたらいい？

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

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

capturing types

capture set

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

capability

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

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

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

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

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

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

Capture checking成功!!

そうではないとき

Capture checking失敗!!

大小関係どう決めるの？

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

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

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

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

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

応用: リソース管理

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

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

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

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

code:scala

x

}

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

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

code:scala

val tempFile = os.temp()

try body(tempFile)

finally os.remove(tempFile)

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

応用: ライフタイム管理

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

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

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

code:scala

//> using scala 3.5.1

import language.experimental.captureChecking

val double: Int -> Int = _ * 2

object Main extends App:

println(apply(42)(double))

println(pureApply(42)(double))

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

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

検査例外への転用

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

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)

}

code:scala

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

try () => repeat(s, n)

catch

case e: NegativeParameterException =>

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

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

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

エフェクトとしてのcapability