notes mizzy.org

Effect systemと「副作用を値にする」は別の軸である

解釈 出典: Koka公式ドキュメント、Effect-TS公式ドキュメント、carina-rs/carina main 2e75b9d2のソース、既存ノート群 作成

CarinaのEffectは名前のせいでEffect systemと取り違えられやすい。だが二つは答えている問いが違う。Effect systemは「この関数は何を起こしうるか」を型で追跡してコンパイル時に検査する仕組みで、「副作用を値にする」は副作用の記述をデータとして作り、実行を後に回す設計である。前者は型の話、後者は実行時の表現の話で、片方だけを持つ言語もライブラリも普通にある。

Effect system — 起こしうることを型に書く

普通の型は戻り値の形しか言わない。fn load(path: &str) -> Configからは、ファイルを読むのか、ネットワークに出るのか、途中で止まらないのかは分からない。Effect systemはこれを関数型の一部にする。

Kokaはこれを中心に据えた言語で、関数型は引数・効果・戻り値の3つで書かれる。公式ドキュメントの例:

fun square1( x : int ) : total int   { x*x }
fun square2( x : int ) : console int { println( "a not so secret side-effect" ); x*x }
fun square3( x : int ) : div int     { x * square3( x ) }
fun square4( x : int ) : exn int     { throw( "oops" ); x*x }

totalは効果なし、consoleは出力、divは停止しないかもしれない、exnは例外。Kokaはすべての関数の効果を推論して追跡するので、totalと宣言した関数の中でprintlnを呼べば型エラーになる。呼んだ関数の効果は呼び出し元へ伝わる。

対象を1種類に絞った小さなEffect systemなら身近にある。Javaの検査例外(throws IOException)は例外だけを追跡するEffect systemで、Rustのasyncは「中断しうる」という効果を印として持ち、呼び出し側に.awaitを要求する。Rustにはasync / constを効果として統一的に扱う議論(Keyword Generics Initiative)がある。

エフェクトハンドラはEffect systemとは別物である。ハンドラは「効果をどう処理するか」を呼び出し側が与える実行時の仕組みで、型で追跡するかどうかとは独立している。OCaml 5はエフェクトハンドラを持つが、どの関数がどの効果を起こすかを型で追跡しない。追跡がなければEffect systemとは呼ばない。

副作用を値にする — 記述と実行を分ける

こちらは副作用をその場で起こさず、「何をするか」をデータとして作っておく。実行は解釈器が後で与える。HaskellのIO、Effect-TSのEffect、Carinaのplanがこの形をしている。Effect-TSの説明ではEffectは遅延実行されるワークフローの記述で、不変な値である。

二つの軸に並べる

型で追跡しない 型で追跡する 値にする 値にしない Carina planは継続を持たない列。開いて読める HaskellのIO IOか否かの1ビットだけ追跡 Effect-TS 失敗Eと依存Rを型で追跡 OCaml 5 ハンドラはあるが型に出ない Koka 全効果を推論。直接実行しハンドラで解釈 Javaの検査例外 例外だけ追跡
二つの軸は独立していて、4つの象限すべてに実例がある。

境界がぼやけて見えるのは右上の象限のせいである。HaskellのIOもEffect-TSも値でありながら型に効果の情報を載せているので、二つの軸が同じものに見える。Effect-TSのEffect<Success, Error, Requirements>は、値化と型による追跡を一つの型に同居させた設計である。

「IOモナドと同じ」と言えるのはどこまでか

CarinaのEffectを「IOモナドと同じく副作用を値として扱う」と説明できるのは、記述と実行を分けるところまでである。そこから先は違う。

HaskellのIO

IOはモナドで、>>=の右側は関数である。「前の結果を受けて次に何をするか」が関数の中に隠れるので、IOの値は実行するまで中を開けない。表示も保存もできない。

Carinaのplan

継続を持たない効果の並びで、全要素を列挙し、表示し、ファイルに書き出せる。applyの前に人が全部を読める。

同じ「副作用の値化」でも、IOは合成の力を取って検査可能性を捨て、Carinaは検査可能性を取って合成の力を捨てている。planを人が承認してからapplyするワークフローは後者でしか成り立たない。この差はモノイドとモナドを分けるのは継続を持てるかどうかであるとモナドは箱ではなく合成戦略であるで書いたものそのもので、planの側の構造は効果の具体化 — planは効果の自由モノイドであるにある。

Carinaの位置

Carinaは左上の象限で、値化はするが型で追跡しない。DSLの型が見ているのは属性値とスキーマで、どの式がどの効果を起こすかは型に現れない。「型安全」と「Effect」が同じ製品の説明に並ぶので、合わせて型レベルのEffect systemだと読まれやすいが、二つの語は別の軸を指している。Carinaの型システムは値を検査する篩型の体系で、穴は段階と境界の継ぎ目にある

根拠の確度

Kokaのコード例と「すべての関数の効果を推論して追跡する」という説明は、公式ドキュメントのEffect typesの節から写した。Effect-TSの型パラメータ名と「遅延実行されるワークフローの記述」「不変」という説明は公式ドキュメントによる。OCaml 5が効果を型で追跡しないことは、漸進的エフェクト型付けの論文の記述による。リリース済みのOCamlに効果の型付けが入っていないことは、最新のリリースノートでは確認していない(要確認: 最新版でも未導入か)。Keyword Generics Initiativeは2022年の発表を見たが、現状どこまで進んでいるかは確認していない。

CarinaのEffectがRead / Create / Update / Delete / Import / Remove / Move / Wait / DeferredCreateなどの変種を持つenumで、Planがeffects: Vec<Effect>を持つことは、carina main 2e75b9d2のcarina-core/src/effect.rsとplan.rsで確認した。図の分類(とくにHaskellのIOを「1ビットのEffect system」と読むこと)と、IOとplanの対比は解釈である。

#効果 #型システム #比較