Zenn
⚙️

Higher-Order Effects Done Right: Heftia Extensible Effectsライブラリの仕組み

2024/09/05に公開
Haskell
monad
effect
extensibleeffects
代数的エフェクト
tech

はじめに

本記事はHaskellのExtensible Effectsのコミュニティ向けに、特に「高階エフェクト」と「限定継続」にフォーカスして、筆者の実装したEEライブラリ「Heftia」の仕組みを解説するものだ。本記事がEEコミュニティに届いて反響を呼んでくれることを祈る。

https://github.com/sayo-hs/heftia

なお、おそらくEEコミュニティは英語圏にあるので、本記事は最終的に英訳する目的で書かれた。英訳後の記事はこちら。

https://sayo-hs.github.io/jekyll/update/2024/09/04/how-the-heftia-extensible-effects-library-works.html

背景

知られている通り、既存のEEライブラリの高階エフェクトの扱いは完璧とは言い難い。

まず、fused-effectsはその名の通りエフェクトがfuseされている。厳密に言うとこれはEEと言えるのかどうかよくわからない（少なくともFreerベースじゃないのでFreer Effectsじゃないと思う）。たぶん言えないんじゃないだろうか。fuseされているというのはつまり、パフォーマンスに原理的な優位性があるということだが、その代償としてエフェクトの動的な変換（いわゆるinterpose系の操作）が困難になっている。あとインタプリタを読み書きするのが大変だ（<$ ctxまみれになるし、threadを扱うのはとても難しく感じる）。

polysemyは惜しい所まで行っている。一階エフェクトはとても簡単に扱えて、便利だ。一方で高階エフェクトの扱いは依然として難しい。Strategy、Finalなどは頭が痛くなってくる。あと、NonDet系の非決定性計算やコルーチンを正しく扱うことができない[1]。これはつまるところ、限定継続を操作できないことに起因するものだ。

そこでeffの登場だ。これはIOモナドレベルで限定継続を扱うプリミティブなオペレーターをGHCに追加することで、continuation-based semanticsという高階エフェクトの意味論を提供するようだ。もし仮にこれが動くようになるとしたら、同じIOモナドベースでシンプルゆえ現在主流のeffectfulの実質的な上位互換になるのではないかと思う。しかしながら、現行のGHCでは動作しないようだ。

また、in-other-wordsというのもある。これもfused-effectsと同様、おそらくEEではないライブラリだ。fused-effectsにおいて挙げたような問題点は解決されている。インタプリタのコードは簡潔で、あとNonDetなども扱えるようだ。しかしながら、解釈の順番によって高階エフェクトが絡んだ挙動がトランザクショナルになったりそうじゃなくなったりと、この辺はmtlの特徴を引き継いでいる。いわゆるAlgebraic Effects and Handlersの意味論のエミュレーションを高階エフェクトに期待する場合、これはちょっと扱いづらい。mtlをモダンにしたものが欲しいというニーズには合致するだろう。

高階エフェクトが問題

さて、なぜこのような面倒なことになっているのだろうか？何か、筋の良い、すべてがうまく行くような方法はないだろうか？

まず、パフォーマンスのことは忘れ、セマンティクスに集中しよう。第一に良いセマンティクス、第二にパフォーマンスだ。

答えへのヒント

ここで、重要なヒントが2つある。

第一に、freer-simpleだ。これは高階エフェクトを完全にスルーして、一階エフェクトのみをサポートするものだ。高階エフェクトが使えないという代償と引き換えに、ここでは完璧なセマンティクスが実現されている。まず、ここではcontinuation-based semanticsという、いわゆるAlgebraic Effects and Handlersに等しい、予測しやすく筋の良い素直な挙動が実現される。このセマンティクスについての詳細はAlexis King氏のThe effect semantics zooを見てほしい。限定継続が自由に扱えるので、コルーチンも非決定性計算もなんでもござれだ。

ここから得られることは、高階エフェクトが厄介者ということだ。高階エフェクトさえないなら、単にFreeにCoyonedaを合成するだけで話は終わりなのだ。

そして第二のヒントが、Polysemyの開発初期のアイデアだ。以下は開発者のSandy Maguire氏のブログで2019年3月ごろに書かれたものだ。引用しよう:

...

newtype Freer f a = Freer
  { runFreer
        :: forall m
         . Monad m
        => (forall x. f (Freer f) x -> m x)
        -> m a
  }

I have no idea if this is right, but at least it gives a Monad instance for free. One limitation you’ll notice is that the continuation in runFreer is a natural transformation, and thus it’s unable to change its return type.

That means interpretations like runError :: Eff (Error e ': r) a -> Eff r (Either e a) are surprisingly difficult to implement. More on this later—I just wanted to point out this flaw.

...

Freer, yet Too Costly Higher-order Effects - Freeing the Higher Orders - REASONABLY POLYMORPHICより。

この後、引用元ではPolysemyのweaving方式版のCoyonedaとしてYoという構造を合成しようと試みている。おそらく現在のPolysemyの内部実装はこれが合成されたものそのものか、それに近いものになっていると思う。

ここで、weaving方式を取らず、単にこのままこれをEffの内部データ構造としたらどうなるだろうか？runErrorは書けなくなる、だろうか？

ここが分岐点だ。

そう、まさにこの高階版FreerであるFreer f aの定義、ここまでは確かに正しかったようなのだ！

では、我々はどのようにrunErrorを書いたらよいのだろうか？

一階と高階を分離する

ここで一つ、新規なアイデアを投入する。
一階のエフェクトと高階のエフェクトを型として分離するというものだ。

例えば、Errorエフェクトは、以下の2つのデータ型に分解されて定義される。

data Throw e (a :: Type) where
    Throw :: e -> Throw e a

data Catch e f (a :: Type) where
    Catch :: f a -> (e -> f a) -> Catch e f a

そして、エフェクトフルプログラムを表現するモナド上では、高階エフェクトの型レベルリストと一階エフェクトの型レベルリストを2つの型引数として分けて取るようにする:

program :: Eff '[Catch Int] '[Throw Int] Int
program = catch (throw 42) \a -> pure a

ここで、Effは内部的には先程のPolysemyのFreerで定義される。これについては後述する。

そして、runErrorのように一括で両者を解釈してしまうのではなく、代わりに以下のように一階用のインタプリタと高階用のインタプリタとに分けるのだ:

runThrow :: Eff '[] (Throw e ': ef) a -> Eff '[] ef (Either e a)
runCatch :: Throw e <| ef => Eff (Catch e ': eh) ef a -> Eff eh ef a

ここで、runThrowの方は高階エフェクトのリストが空になっていることに注意してほしい。実は、このようにするとrunThrowと、そしてなんと runCatchが書けるようになる[2]。こうすれば、高階エフェクトが扱えるのだ。

runThrowについては、少なくともいま議論しているこの方式においては、限定継続を扱うような解釈をするときは、高階エフェクトはリスト内に残しておけないということだ。runThrowの中では、Throwが投げられたらそこからの限定継続を捨てて大域脱出をする必要がある。

本質的構造

この話のオチは、Polysemy、そして既存のEEの高階エフェクトにまつわる困難の元凶は、一階エフェクトと高階エフェクトという本質的に構造も性質も可能な操作も異なる対象を、まぜこぜにして扱っていたことにある、ということだ。これが、筆者の本記事での最も強調したい主張だ。

このようにエフェクトの型もリストも一階と高階で分けることで、どういう局面でどういう操作が可能かが型レベルで分けられるので、より厳密に制約が表現されるようになり、書けないと思われていた操作が実際には条件分けすれば書けることが分かった。

これが、Heftiaが一階エフェクトと高階エフェクトを同時に扱うための方法だ。前述した通り、これには限定継続を取り出して呼び出したり、捨てて大域脱出をしようとするときは、高階エフェクトがすべて解釈済みでリストから消えていなければならないという制限が付く。

筆者の考えでは、この制限は代数的エフェクトを高階エフェクトに拡張したときにその数学的構造に本質的に現れるもので、拡張の理論的限界なのではないか、と現時点では思っている。一応そう考える理由として、実際、この制限はセマンティクスの正常性を保護するためのものとして解釈できる。

例えば、エラー時にリソース開放等を安全に行うための高階エフェクトであるいわゆるonExceptionと、先程のthrow一階エフェクトを使った、次のようなプログラムを考えてみよう:

prog :: ... => Eff (OnException ': eh) (Throw Int ': ef) ()
prog =
    ( do
        allocateResource
        throw 42
        freeResourceOnSuccess
    ) `onException` freeResourceOnError

そして、仮にrunThrowが高階エフェクトがリストに残っていても使えると考えてみよう。つまり

runThrow' :: Eff eh (Throw e ': ef) a -> Eff eh ef (Either e a)

が書けると仮定するということだ。

すると、次のようなことができることになる。

runThrow' prog :: Eff (OnException ': eh) ef (Either Int ())

さて、このようになったとすると、次にOnExceptionはどうしたらよいだろうか？Effは内部的には単なるFreerなので、もはやリストから消えてしまったThrowの情報はどこにも保持されていない。throw 42はもはやonExceptionをすり抜けてEither Intになってしまった。こうなってしまっては、もはやonExceptionの解釈においてスコープ内でエラーが発生したかどうかの情報を取得することは不可能だ。つまり、freeResourceOnErrorを呼ぶべきかどうかの判断ができない。呼ばないとすれば、失敗時にリソース開放がされなくなるし、呼ぶとすれば、freeResourceOnSuccessとfreeResourceOnErrorで二重に開放処理が走ることになる。とても嫌な感じだ。

高階エフェクトが残っていると限定継続が扱えないというのはつまり、こういう「スコープから勝手に飛び出してしまう」ような非安全性を防ぐための型による"ガードレール"だと解釈することができる。型がこうなっていれば、限定継続を扱う解釈をするためにはまず先に高階エフェクトを解釈しなければならない。必ずこの順番が守ることが型で保証される。予測の難しい変な挙動とはおさらばというわけだ。

さらにこの話は、Resource（いわゆるbracketやonException）やUnliftIO系の高階エフェクトは、NonDetやThrowやStateなどの限定継続操作系エフェクトと競合するという話に繋がる[3]。この場合、実はrunNonDetByThreadやrunThrowByIOやrunStateByIORefのように、IOモナドの操作に依存した解釈のみしか不可能になる。つまり、型の導きによって、どのように頑張ってもbracketから漏れる例外はありえないのだ。このように構造から導出される型に従うと、すべてが整合的で、安全に保たれるようになっている。これはかなり、Heftiaが提供する構造とその制限の筋の良さ、本質的構造への近さを示していると言えるのではないだろうか。少なくとも筆者はそう考えている。

Continuation-based Semantics

この方法で各種一階・高階エフェクトとインタプリタを定義すると、自然に前述のcontinuation-based semanticsが実現される。詳細は本ライブラリのREADMEのGetting Startedを見てほしい。端的に言えば、Algebraic Effects and HandlersやAlexis King氏のeffと同じ結果になるということだ。

実際のところの筋道、そしてHefty Algebra

もちろん、筆者は無からこのアイデアに至ったわけではない。筆者は一年半ほど前、ちょうどHeftiaの初期バージョンにおいて設計に悩んでいた頃、以下の論文を見つけた:

Casper Bach Poulsen and Cas van der Rest. 2023. Hefty Algebras: Modular Elaboration of Higher-Order Algebraic Effects. Proc. ACM Program. Lang. 7, POPL, Article 62 (January 2023), 31 pages.

どうやら悩んでいる事柄についての答えを与えている何かであるような感じがしたので、書かれていたHeftyのAgdaによる定義コードと、アーティファクトのリポジトリにあったHaskellコードを参考に型を弄っていた所、Heftyが以下のデータ構造であるらしいことはわかった[4]:

data Hefty h a =
      Pure a
    | forall x. Impure (h (Hefty h) x) (x -> Hefty h a)

そしてこれは、どうもHCoyonedaというCoyonedaの高階版のようなものが合成された形になっているらしい。
HCoyonedaを分解すると:

type Hefty h = Hefty' (HCoyoneda h)

data Hefty' h a =
      Pure a
    | Impure (h (Hefty h) (Hefty h a))

data HCoyoneda h f a
    = forall x. HCoyoneda (h f x) (x -> a)
    = HCoyoneda (Coyoneda (h f) a)

そしてさらに、Hefty'というのはFreeの高階版のようだ:

data Hefty' h a = Hefty' ( Free (h (Hefty' h)) a )

そう、HeftyというのはFreeの高階版とCoyonedaの高階版の合成、つまり高階版のFreerなのだ。

また、Hefty AlgebraではHeftyデータ構造上で高階エフェクトを扱うためにElaborationという仕組みを使う。これは前述の制限のさらに強いようなバージョンで、限定継続操作をするかどうかに関わらず、すべての一階エフェクトの解釈の前にまずすべての高階エフェクトの解釈を終えなければならない、という枠組みだ。つまり、高階エフェクトの解釈ステージ（これをElaborationと呼んでいる）と一階エフェクトの解釈ステージが完全に分離されている。

なんか、行けそうだ。そういうわけでこれらの考えをベースにライブラリを設計し直した。途中で、解釈のステージを完全に分離しなくても、どうもエフェクトリストを分けるだけで、ある程度一階と高階は共存できるらしいということに気付いた。そういうわけで、一階エフェクトと高階エフェクトのリストを分離するというアイデアはこのElaborationの方式にインスパイアされたものだ。

そして、さらにしばらく経ってから見つけたのが、あのPolysemyの記事だ。
先程の高階版Freerの定義を再掲しよう。

newtype Freer f a = Freer
  { runFreer
        :: forall m
         . Monad m
        => (forall x. f (Freer f) x -> m x)
        -> m a
  }

これを変形してみよう。まず、従来の一階のFreerと混ざってややこしいので、この高階版のFreerはFreerHと仮に置く。fはhと改名する。そして、FreerHを従来の一階のFreerであるFreer1を使って書き直す。ここで、Freer1は等価なエンコーディングとしてFree (Coyoneda f)があるのだった[5]。

data FreerH h a = FreerH (Freer1 (h (FreerH h)) a)

data Freer1 f a
    = Freer1 (forall m. Monad m => (forall x. f x -> m x) -> m a)
    = Freer1 (Free (Coyoneda f) a)

Freer1のエンコーディングをFree (Coyoneda f)の方に置き換えてFreerHに代入してみると

data FreerH h a
    = FreerH (Free (Coyoneda (h (FreerH h))) a)
    = FreerH (Free (HCoyoneda h (FreerH h)) a)

HCoyonedaを分解すると

type FreerH h = FreerH' (HCoyoneda h)
data FreerH' h a = FreerH' ( Free (h (FreerH' h)) a )

あれ？これって…

type Hefty h = Hefty' (HCoyoneda h)
data Hefty' h a = Hefty' ( Free (h (Hefty' h)) a )

…同じだ。

というわけで、 このHeftyと等価なものは、既に2019年の時点でPolysemy内で出ていたというわけだ。そういう意味で、非常に惜しい所まで来ていた。この高階版Freerの能力を真に引き出すために登場を待つ必要があったものこそつまり、高階エフェクトのみを一階エフェクトと分離して解釈するというelaborationの枠組みだろう。

というわけで、だいぶ元の論文からは変質したが、Heftiaは基本的にはこの論文の考え方がベースになっている。

今後について

本ライブラリは、単にAlexis King氏のeffを先取りして動くようにした、というようなものではない。

Haskellのエフェクトシステムライブラリを分類するとしたら、非IOベースとIOベースに分けられるだろう。

本ライブラリは非IOベースの、純粋側に分類される。これはつまり、IOモナドに依存せずともエフェクトの動作が可能ということである。IOモナド以外をベースのモナドにすることができるし、さらにはモナドでなくアプリカティブなエフェクトフルプログラムすらも扱うことが可能だ。

なぜ純粋性にこだわるかというと、これはSafe Haskell言語拡張を意識している。IOモナドに依存せず、内部でunsafeな関数を一切使用しなければ、Safe Haskellと組み合わせて、エフェクトシステムを静的な権限管理・アクセス制御のためのセキュリティ機能として使うことができるようになる。いまのところはおそらくSafe Haskellと同時に使用することはできないと思うが、将来的にはこれに対応したいと考えている。純粋性は、そのための布石だ。

脚注

  1. https://github.com/polysemy-research/polysemy/issues/246 ↩︎

  2. 実はehにHFunctor（Polysemyの古いバージョンで言うところのMFunctorに相当する）の制約が必要だ。これについても実は色々と説明できることがあるのだが、今回は割愛。 ↩︎

  3. Effectful等でお馴染みの話だが、唯一性質のいいReaderだけが、競合なしにIOに依存せず解釈できる。 ↩︎

  4. 日本語だが、そのときの思考の書き散らしがここにある:https://gist.github.com/ymdryo/e8af81d454371c719c289eba1418e573 ↩︎

  5. https://stackoverflow.com/questions/71562355/did-this-construction-of-freefreer-monad-works ↩︎

GitHubで編集を提案

Discussion