🌌

Heftiaエフェクトシステムライブラリ入門 Part 3 - 限定継続

2024/09/01に公開

ここでは、Heftiaにおける一階及び高階エフェクトを用いた限定継続の操作について説明します。

ここまでで出てきた使い方は、既存のエフェクトシステムライブラリで実現可能な部分と被るところがありました。しかし本パートで説明すること[1]は、既存のものでは実現が困難であり、完全に新規な技術です。

以降、常体で解説を行います。

Forkエフェクト

以下で定義するForkエフェクトは、制御構造を非決定性計算的に分枝させるものだ。

非決定性計算と言えば、リストモナドだ。リストモナドでdo { x <- [1..4]; ... }とやるように、このエフェクトは制御の流れを分枝させ、あたかもパラレルワールドでプログラムが並行に動いているように見える。

Posixプログラミングに詳しい読者は、これはプロセスを分裂させるいわゆるfork()関数と同じものだと思ってもらって良い。ただし、Posixのfork関数は制御構造を2つに分裂させるが、こちらは任意の個数だけ分裂させる。

type ForkID = Int

data Fork a where
    Fork :: Fork ForkID
makeEffectF [''Fork]

runForkSingle :: ForallHFunctor eh => eh :!! LFork ': r ~> eh :!! r
runForkSingle = interpretRec \Fork -> pure 0

戻り値のForkIDは、分裂後に自分がどの分枝世界にいるかを表すIDだ。runForkSingleは単純に、forkエフェクトが投げられても分枝せず、戻り値は0のみを返すインタプリタだ。

ResetForkエフェクト

以下のResetForkエフェクトは、分枝の範囲をスコープで区切って限定するための高階エフェクトだ。

data ResetFork f a where
    ResetFork :: Monoid w => f w -> ResetFork f w
makeEffectH [''ResetFork]

Posixのfork()との違いは、あちらはプロセス終了まで永遠と分枝したままだが、こちらは分枝の範囲が限定されているということだ。

RestForkが導入するスコープを抜けるタイミングで、スコープ内で発生したForkによる分枝はすべて収束し、戻り値はMonoidに沿って合成される。

さて、ここで限定継続の出番だ。「限定」というのはつまり分枝がスコープ内の中で収まっていて、その外側では分枝は継続しないということだ。

以下のelaboration射は、Forkエフェクトが投げられたタイミングにおける限定継続resumeを取り出し、それをnumberOfFork回呼び出すことで、実際に制御構造をnumberOfFork個に分枝させる。forkが実行された瞬間に制御がエフェクトフルプログラム側からインタプリタ側に移行され、そのときresumeがインタプリタ側に渡ってくる。このresumeを実行すると、エフェクトフルプログラム側の一時停止した処理を再開し制御を戻すことができる。これを複数回呼ぶと、再開処理が多重で実行される。これがすなわち、制御が分枝するということだ。

applyResetFork :: Fork <| r => Int -> Elab ResetFork ('[] :!! r)
applyResetFork numberOfFork (ResetFork m) =
    m & interposeK pure \resume Fork -> do
        r <- mapM resume [1 .. numberOfFork]
        pure $ mconcat r

限定継続の取り出しにはinterposeK関数を使う。他にもK系統の関数はいくつかあるので、用途に応じて使い分けよう。ここでは取り出された限定継続resume1からnumberOfForkにかけて呼び出し、最後に各々の継続の結果をmconcatで集計している。

実行例を見てみよう。

main :: IO ()
main =
    runEff
        . runForkSingle
        . interpretRecH (applyResetFork 4)
        $ do
            liftIO . putStrLn . (("[out of scope] " ++) . show) =<< fork
            s <- resetFork do
                fid1 <- fork
                fid2 <- fork
                liftIO $ putStrLn $ "[delimited continuation of `fork`] Fork ID: " ++ show (fid1, fid2)
                pure $ show (fid1, fid2)
            liftIO $ putStrLn $ "scope exited. result: " ++ s

実行結果:

[out of scope] 0
[delimited continuation of `fork`] Fork ID: (1,1)
[delimited continuation of `fork`] Fork ID: (1,2)
[delimited continuation of `fork`] Fork ID: (1,3)
[delimited continuation of `fork`] Fork ID: (1,4)
[delimited continuation of `fork`] Fork ID: (2,1)
[delimited continuation of `fork`] Fork ID: (2,2)
[delimited continuation of `fork`] Fork ID: (2,3)
[delimited continuation of `fork`] Fork ID: (2,4)
[delimited continuation of `fork`] Fork ID: (3,1)
[delimited continuation of `fork`] Fork ID: (3,2)
[delimited continuation of `fork`] Fork ID: (3,3)
[delimited continuation of `fork`] Fork ID: (3,4)
[delimited continuation of `fork`] Fork ID: (4,1)
[delimited continuation of `fork`] Fork ID: (4,2)
[delimited continuation of `fork`] Fork ID: (4,3)
[delimited continuation of `fork`] Fork ID: (4,4)
scope exited. result: (1,1)(1,2)(1,3)(1,4)(2,1)(2,2)(2,3)(2,4)(3,1)(3,2)(3,3)(3,4)(4,1)(4,2)(4,3)(4,4)

まず、resetForkのスコープの外ではapplyResetForkの影響を受けず、単にrunForkSingleの挙動が反映される。resetForkのスコープ内ではリストモナドの要領で、おのおののforkについて1から4のすべてのパターンが戻ってきて、計算が分枝して進んでいる。resetForkのスコープを抜けると分枝は収束し、スコープから返却された(fid1,fid2)という形式の文字列がすべてMonoidにより結合されて結果として得られている。

単にこれと同じ動作をするfork関数を作るだけなら、リストモナドや継続モナドを使うことで今までも可能であった。本ライブラリが真に可能にするのは、例えばapplyResetForkとは別のfork戦略をelaboratorとして実装するなどして、どのようにforkするかを差し替えできるということだ。例えば、スレッドを使って並行に実行するようなapplyResetForkByThreadなるelaboratorを実装できるはずだ。さらにPart 2で説明したようにして、高階なフックを用いて挙動をモジュラーに変更することができ、それらは合成可能だ。

おわりに

このように、Heftiaでは限定継続を容易に扱うことができる。その上で、どのように限定継続を使うか(あるいは使わないか)をelaborationにより柔軟に(モジュラーに)変更することができる。これにより、非決定性計算はもちろん、非同期バックエンドを変更可能なAsyncエフェクトといった並行計算への応用など、色々と面白いエフェクト・DSLを作ることが可能になるだろう。

Haskell上でEffect Systemを実現するライブラリは数多くあるが、いわゆる「Algebraic Effects and Handlers」で可能なこと(限定継続の取り出しとそれを用いたモジュラーな高階エフェクトのハンドリング)をほぼフルでエミュレートできるのは、Hefty Algebrasに基づくElaboration方式のみのようだ。

以上で、本ライブラリの入門編は終わりになる。本ライブラリの"感覚"を掴むための最低限の説明をしたつもりだ。まだまだ説明できなかった事柄がたくさんあるので、各自Haddockを辿るか、次のシリーズである応用編が書かれるのを待ってほしい!Haddockに関してはほとんどドキュメントは書けていない。ドキュメントの整備を手伝ってくれる人は大歓迎だ!

本シリーズを英訳してくれる人を募集中です。


本パートの例で使用したコードの全体はGitHubにある。

脚注
  1. 高階エフェクトを組み合わせたモジュラーな限定継続の制御 ↩︎

GitHubで編集を提案

Discussion