Prism: 型付きエフェクトを備えた非純粋関数型言語

 (stephendiehl.com)
1 ポイント 投稿者 GN⁺ 2 시간 전 | 1件のコメント | WhatsAppで共有
  • Prismは、可変変数・例外・ストリームのようなエフェクトを隠さず型に表しつつ、外部から観測できない局所的な変更は Int -> Int のような純粋な型のまま保つ実験的コンパイラ
  • 中核は 代数的エフェクトハンドラ と row polymorphism で、エフェクトは関数型の row に統合され、ハンドラは必要なラベルだけを処理して残りを渡す
  • 同じエフェクトシステムで例外、ジェネレータ/ストリーム、レンズ、var 状態、fail/guard フローを表現でき、一部の経路は中間リストやランタイム合成なしに lower される
  • 性能面では evidence passing と Perceus 参照カウントを組み合わせ、エフェクト呼び出しごとの割り当てを避け、固有所有値の関数型更新をインプレース変更に最適化する
  • Prism は LLVM IR、MLIR、C ランタイム、Rust インタプリタ、Lean 4 モデル、WASM playground を提供し、型推論と lowering の結果を直接確認できる

外部から見えない変更と型付きエフェクト

  • Prism の出発点は、内部で var と代入を使う fib 関数でも、外部の観測者には純粋関数のように見えるという点にある
    • 例の fib は 2 つの変数をインプレース更新するが、関数の外へ状態を露出しない
    • 型は Int -> Int で、エフェクトは型に現れない
  • Prism は過去 3 年にわたって開発された 概念実証の関数型コンパイラ で、OCaml 5、Haskell、Koka 系の現代的な型のアイデアを土台にエフェクトをモデル化している
  • 中心的な方向性は、エフェクトを避けることではなく、エフェクトを型システムに入れ、コンパイラがそのコストを消すよう最適化することにある

エフェクトはインターフェースのように振る舞う

  • Prism のエフェクトは演算を宣言し、ハンドラがその演算に意味を与える 代数的エフェクトハンドラ 方式である
    • effect Gen { ctl yield(Int) : Unit } は yield 演算を宣言する
    • fn produce(n) : !{Gen} Unit の !{Gen} は、関数が yield を実行することを型に示す
  • 同じ producer でも continuation である k をどう扱うかによって異なる意味に解釈される
    • total は yield の値を足し合わせる
    • count は yield の回数を数える
    • k を捨てれば例外、1 回呼べば状態やジェネレータ、複数回呼べば探索の動作になる
  • Amb エフェクトの例では、choose と reject でピタゴラス数探索を表現する
    • choose(n) は 0..n-1 範囲の値を提供する
    • ハンドラは候補ごとに同じ continuation を再開し、探索木を作る
  • OCaml 5 と異なり、Prism はエフェクトを型に含め、Haskell のモナドトランスフォーマースタックのように階層を手動で積み上げる必要がない
    • エフェクト row は呼び出しをまたいで構造的に統合される
    • スタックではなくラベルの集合のように動作する

1 つのメカニズムで表現される機能群

  • 例外

    • Prism では例外は continuation を捨てるハンドラ である
    • final ctl 節は k を破棄し、その本体の値をハンドラ結果とする
    • Result を伝播させたり、呼び出しスタックに ? を散りばめたりする方式ではない
    • 例外はエフェクト row のラベルなので、拡張可能な例外 として合成される
    • 各失敗は個別の演算であり、関数型の row は外へ出る可能性のある例外を示す
    • Abort と Timeout の例では、fetch は !{Abort, Timeout} を持つ
    • with_default は Timeout だけを処理して fallback の "cached" を返し、処理後の型には !{Abort} だけが残る
    • Java の checked exception と違って、クラス階層に縛られず開いた構造的集合として動作する

  • ジェネレータとストリーム

    • ストリームは emit を実行する producer、それを捕まえて再度流す transformer、fold する consumer で構成される
    • パイプラインは 1 つの producer を囲むようにハンドラを入れ子にした形なので、中間リスト が構造的に生じない
    • 例: srange(1, n).smap(square).skeep(even).stake(5).ssum()
    • stake(5) のような早期終了は、必要な値を得た後で continuation を捨てるハンドラである
    • ストリームライブラリは Haskell の pipes と conduit から影響を受けている

  • レンズ

    • Prism のレンズは別ライブラリではなく、レコード更新パス とメモリモデルの組み合わせである
    • ネストしたレコードで、1 つのパス式により深いフィールドを複数更新できる
    • 例: { g | player.pos.x = 30, player.hp = 95, score = 110 }
    • ネストしたレコードの spine を作り直しつつ、値が固有所有されている場合は分解したセルを再利用する
    • この構造により、関数型更新をポインタ書き込みへコンパイルできる
    • ランタイムで optic 型を割り当てたり合成したりはしない
    • deriving (Lens) は score_of、with_score のような通常の関数アクセサを生成する

  • 可変状態

    • var は private effect の get/set 演算へ desugar される
    • ブロック末尾に設置されたハンドラがこのエフェクトを処理する
    • クロージャ脱出解析は、状態が外へ逃げる場合を拒否する
    • 外側の関数は空のエフェクト row を維持できる

  • 失敗

    • 失敗は匿名の Fail エフェクトで表され、「この式は値を生成できないかもしれない」ということを型システムが扱う
    • fail() は失敗を実行し、guard(cond) は条件が偽のとき失敗する
    • ?? は左辺が失敗したとき fallback を使う
    • ?. は option チェーンをたどりながら短絡する
    • comprehension guard は失敗した要素を crash させる代わりに枝刈りする
    • var もハンドラ sugar なので、transact ブロックは live 変数をスナップショットし、失敗時にロールバックできる

現代的な型機能

  • Prism は大半のコードで型注釈を書かなくて済むよう、Dunfield-Krishnaswami 系の双方向 higher-rank 型推論を使う
  • 高階多相性が必要な境界では forall で binder を明示する
    • pick(g : forall a. (a) -> a) は g を Bool と Int の両方に適用できる
    • Damas-Milner core なら最初の呼び出しで a が Bool に単一化され、2 回目の呼び出しは拒否される状況である
  • アドホック多相性は Lean スタイルの型クラスで表現される
    • インスタンスは名前付きの値である
    • given Ord(a) は辞書を要求する
    • 複数のインスタンスがあるときは 1 つを canonical として印を付け、他は using で明示する
  • deriving は Eq、Ord、Show、Lens のような反復的インスタンスとフィールドアクセサを生成する
  • パターンマッチもクラスと結び付けられている
    • pattern First(n) for Peek = view peek はクラスメソッドを view として使うパターンである
    • head_or は Peek インスタンスを持つ複数の型に対して同じパターンを使える
  • show は別クラスなしで 型指向 に動作する
    • コンパイラが静的型から構造的 printer を合成する
    • ランタイム型タグを読んで出力方法を決めるわけではない
  • エフェクト row も多相的である
    • fn twice(f : (Unit) -> Int ! {| e}) は、引数として受け取った関数のエフェクト row e が何であっても結果を足し合わせる
    • 純粋な thunk では e は空 row {} と単一化される
    • Tick や Say のようなエフェクトを実行する thunk では、その row をそのまま伝播する

エフェクトコストを下げるコンパイル方式

  • 教科書的な代数的エフェクト実装では、計算を free monad 形式の木に再構成し、演算ごとに小さなセルを割り当てることがある
  • Prism の高速経路は Koka 系の evidence passing である
    • 計算を再構成してハンドラを探す代わりに、アクティブなハンドラ節を通常の引数のように各演算地点へ渡す
    • do op は直接呼び出しへ lower される
    • ハンドラ設置時にクロージャを 1 つ割り当てるだけなので、コストは O(handlers) であり、演算回数には比例しない
  • free monad エンコーディングは fallback として残されている
    • データ構造として外へ出る計算
    • 真の multishot resumption
    • masked handler のようなパターンが対象である
  • ストリームパイプラインでは interprocedural flow analysis により、必要な effect evidence を関数境界の向こうまで計算する
    • producer と transformer に evidence をスレッディングする
    • 全体のチェーンは単一ループへ lower される
    • 中間リストも演算ごとのセル割り当てもない
  • この方式は、Haskell の stream fusion や Rust の iterator adapter の単一化に近い結果を、エフェクトコンパイラで得る構造である

メモリモデルとランタイム

  • Prism は Perceus 参照カウント を使う
    • ヒープセルは静的に既知の地点で決定的に解放される
    • pause も tracing もない
  • frame-limited reuse は、パターンマッチでたった今分解したセルをコンストラクタ側へ再び渡す
    • 固有所有されたリストに対する map は、新しいリストを返す純粋関数のように見えるが、実際にはインプレース変更されうる
    • レンズ更新がポインタ書き込みへコンパイルされるのも同じメカニズムである
  • ランタイム構造は Lean 4 のメモリ規律に似ているが、Prism は LLVM IR を出力する
    • LLVM IR は inkwell を通じて生成される
    • 同じプログラムに対してテキスト MLIR モジュールも生成する
    • 結果は clang で手書きの C ランタイム prism_rt.c とリンクされる
  • prism_rt.c は約 2,000 行規模の小さなランタイムである
    • ヒープセルは { refcount, tag, arity, fields... } 形式の 4 word 以上の構造を持つ
    • allocator、rc_inc/rc_dec、インプレース再利用 allocator、bignum と文字列 primitive を含む
    • collector thread、card table、safepoint はない
  • 既定の allocator は libc の malloc で、ベンチマーク用に opt-in の mimalloc 設定がある
  • live-cell oracle は終了時に heap balance が 0 であることを assert し、テストスイートが garbage-free 特性を確認する

Lean モデルとバックエンド検証

  • Prism インタプリタは CEK machine 系であり、この machine は Lean 4 モデル models/Prism.lean に反映されている
  • Lean 4 モデルは、small-step relation が決定的であることを示す 機械検証済み定理 を持つ
    • プログラムは常にただ 1 つの次状態へ進む
  • Rust 実装のインタプリタは differential oracle としても使われる
    • corpus 内のすべてのプログラムは、インタプリタと LLVM、MLIR、C-linked binary の各バックエンドをすべて通過する
    • 4 つの結果の出力が byte-identical でなければビルドは通らない
  • 決定性は replayable durable execution の基盤になる
    • 入力を固定して実行を記録すれば、bit-for-bit の再生が可能になるという構想である
    • 将来のバージョンでは、クラッシュ後の replay 安全性を型特性として検査する Prism が描かれている

WASM playground とソース

  • 同じインタプリタは WASM にコンパイルされており、playground でインストールなしに Prism コードを実行できる
  • playground は worker 上でプログラムを実行する
  • ボタンで推論された型注釈、effect row、lower された core IR をダンプできる
    • var ループやストリームパイプラインが実際にどのような形に lower されるかを見られる
  • 本文の例は dropdown に含まれている
  • 全ソース、Lean モデル、C ランタイムは prism repository on GitHub にある

実装の系譜とプロジェクトの性格

関連記事

1件のコメント

 
GN⁺ 2 시간 전
Lobste.rs のコメント

  • レンズがエフェクトと何の関係があるのか分からない。記事でレンズに触れるたびに、「1つのトリックを5通りに」の下にまとめられていること以外、互いに無関係に見える。
    それに tick_use() がそもそも何をしようとしているのかも分からない。読者が説明なしでこんな入り組んだ例を理解することを期待しているのだろうか？ 型注釈があれば助けになったと思う。

    • レンズについてはこちらでさらに説明されている: https://sdiehl.github.io/prism/spec.html#86-optic-paths
      それでも、比喩的なレベルを超えてレンズがエフェクトと何の関係があるのかはよく見えない。著者はこう書いている:

      This is the language’s “effects instead of monads” stance applied to optics, paths instead of optic combinators.
      つまり比喩としてはこういうことだと思う。モナドは値だが、エフェクトは値ではなく一種の制御構造である。同様にレンズは値だが、Prism の optic paths は値ではなく、ハードコードされた構文を持つ制御構造に近い。

  • もっと時間をかけて理解する必要があるが、本当に美しく見える。

  • 本当に印象的だ。むしろそのために、Diehl が記事の最後でコンパイラをおもちゃと呼んでいる理由が気になる。新しいレベルの優雅さを示す、成功した概念実証のように見える。

  • call-by-push-value の中間表現が実際にどのような形なのか、もっと詳しく見てみたい。特に合流点（join point）をどう扱うのかが気になる。
    CBPV にエフェクトを付ける理論を扱った論文はいくつかあった。計算にはエフェクト型があり、値にはないと言うのはかなり自然だが、Koka の証拠渡しにそのまま適用できるほど具体化されたものは見たことがないので興味深い。
    全体として Koka と比べてどういう位置づけなのか知りたい。FBIP、Perceus、証拠渡しを見ると、Koka の研究から強く影響を受けているのは明らかで、同時に中間表現に CBPV を使っているので確かに異なってもいる。ただ、どのくらい違うのかはよく見えない。

  • 自分がずっと時間を作って作ろうとしていたものにかなり似ている。いいね！

  • 話題から少し外れるが、Stephen の「write you a haskell」プロジェクトが数年前に止まってしまったのは、いつも少し残念に思っていた。Prism についてはチュートリアル級の実装解説が出るといいな。

  • この言語で何が「不純」なのか気になる。その単語はタイトルにだけ出てきて、本文では二度と出てこない。
    すべてのエフェクトが追跡されるように見えるので、エフェクトのない関数は依然として数学的な関数だ。何か見落としているのだろうか？

    • 提示されている fib 定義のように、関数定義内でローカルな可変変数を使うことに関係しているように見える。var x は不純な可変変数で、let x は純粋な不変変数だ。

  • 通常は言語の機能として扱われていたもの、たとえば X 言語の yield や Y 言語の throw のようなものを、もう1つのインターフェースとして実装している点が本当に素晴らしい。
    副作用、例外、継続のような複数の制御フローを1つの抽象化の上に構築できるというのは、設計上の問い全体を新たに捉える興味深い方法であり、さらなる探求と革新を助けたり刺激したりしてくれることを期待している。今後何年も、インスピレーションを得るためにまた見返すことになりそうだ。