「副作用が型シグネチャに現れる」という説明だけでは、型が何を保証するのかは決まらない。 型で区別できるのは、副作用の有無か、起こし得る効果の種類か、効果を起こせる具体的な権限か、その権限を保持できる期間かもしれない。 いずれも実際に起きた操作の記録ではなく、プログラムが起こし得ることの安全な上界を表す。
計算全体を純粋な値として包む
Haskell は副作用を起こす計算を IO 型の値として表す。 通常の関数はすべて純粋であり、Int から Int を返す関数は入出力を実行できない。 入出力の結果として String を得る計算は String ではなく IO String になるため、純粋な値と副作用を伴う計算を型で混同できない。
square :: Int -> Int
getLine :: IO Stringこの方式は副作用の有無を強い境界として示す一方、IO だけではファイル、ネットワーク、時刻のどれを使うかまでは区別しない。
起こし得る効果の種類を列挙する
Koka は関数型を引数型、効果型、結果型の三つで構成し、console、exn、div、ndet のような効果を推論する。 関数が受け取った別の関数と同じ効果を持つことも、効果変数によって表せる。
fun print : (string) -> console ()
fun divide : (int, int) -> exn int
fun map : (list<a>, a -> e b) -> e list<b>このような効果行は「どの種類の操作を起こし得るか」を直接表す。 局所的な変更可能状態が外へ漏れないと証明できれば、その状態効果を外側の関数型から消せるため、内部実装の命令的な書き方と外から観測できる純粋性も分けられる。
https://koka-lang.github.io/koka/doc/book.html
Flix も原始効果、代数的効果、ヒープ効果を型で追跡し、局所的な変更可能状態が関数の外へ出なければ純粋な関数として扱う。 この方式では「純粋」を構文上の書き方ではなく、外から観測できる効果の不在として検査できる。
https://doc.flix.dev/effect-system.html
効果ハンドラがあっても効果安全とは限らない
代数的効果とハンドラは、効果の型付けとは別の仕組みである。 前者は処理を中断して操作の意味を外側のハンドラへ委ねる実行機構であり、後者は未処理の効果が残らないことを静的に検査する仕組みである。
OCaml 5 は効果ハンドラを備えるが、関数型に発生し得る効果の集合を載せない。 コンパイラはすべての効果が処理されたことを保証せず、対応するハンドラがなければ実行時に Effect.Unhandled 例外が発生する。 この例は「効果を組み合わせられる」と「効果が型に現れる」を同一視できないことを示す。
https://ocaml.org/manual/5.1/effects.html
効果を起こす権限と生存期間を追跡する
Scala 3 の実験的な Capture Checking が直接追跡するのは効果名ではなく、関数値や遅延値が保持するケイパビリティへの参照である。 次の型はログ書き込みという効果を必ず起こすことではなく、この関数値が logger を保持して使えることを表す。
() ->{logger} Unitこの捕捉集合は、関数値が保持してよいケイパビリティの許可リストに近い。 ただし、関数が使える権限の全体を捕捉集合だけで表すわけではない。 関数は、呼び出し時に引数として渡されたケイパビリティも、関数値の中へ保持せずにその場で使える。
Logger^ -> Unitこの型の関数は特定の Logger を保持しないため純粋な関数型だが、Logger を引数として受け取った呼び出しではログを書ける。 したがって、許可される権限は、引数から持ち込まれるケイパビリティと、捕捉集合により関数値から持ち出されるケイパビリティの両方で決まる。
具体的な参照が型に現れるため、ファイルやデータベース接続のような権限が許されたスコープより長く残らないかを検査できる。 一方、読み取りと書き込みをケイパビリティの型で分けなければ両者は区別できず、追跡されない大域的な操作まで Capture Checking 単体で禁止できるわけでもない。
Koka や Flix の効果型が起こし得る操作の種類を列挙するのに対し、Capture Checking はその操作を可能にする具体的な権限の持ち込みと持ち出しを制限する。
https://docs.scala-lang.org/scala3/reference/experimental/capture-checking/overview.html
Rust の所有権と借用も、一般的な効果の種類ではなく、具体的な値へアクセスする権限とその有効期間を型で制約する。 共有参照は読み取りを許し、可変参照は変更を許すが、同じ値への競合する参照を同時に持てない。 Rust はこれによって変更と別名参照の安全性を検査するが、関数がファイルやネットワークを使うかを関数型へ列挙するわけではない。
https://doc.rust-lang.org/book/ch04-02-references-and-borrowing.html
副作用という一語を分解する
副作用について型で知りたいことは一つではない。 純粋な計算と外界を操作する計算を分けたいなら IO 型が答えになり、起こし得る操作の種類を合成したいなら効果行が答えになる。 特定の資源を誰が使えていつまで保持できるかを制約したいなら、ケイパビリティ追跡や所有権と借用が答えになる。
したがって、副作用の型付けを比較するときは「純粋か不純か」だけを見るのでは足りない。 型が効果の種類、具体的な権限、生存期間のどれを追跡し、どの操作がその追跡を迂回できるのかまで確認して、初めて保証の違いが分かる。
#effect-system #type-system #capability #functional-programming