霧の中の代数的エフェクト

関数型まつり2026で発表した資料です。
代数的エフェクトの「代数的」が何を意味するのかを説明します。

Transcript

1. 霧の中の代数的エフェクト ～代数的とは何なのか～
2. 自己紹介 名前： funnycat やってること： PureScriptやHaskellでモックライブラリを作ったり、zenn.devで記事を書いたりし てます。 この発表までの変遷： 1. 関数型言語でフロントエンドをやりたくてElmを学ぶ。 2. PureScriptを始める。モナドの理解以前にExtensible Effectsに突っ込み撃沈。 　諦めてモナド→MTL→Extensible Effectsと進む。 3. 他言語のExtensible Effectsを知るためHaskellを始める。 4. 代数的エフェクトの存在を知る。色々言語を触る。 5. 代数的ってなんだ？という記事を書こうと思って真面目に調べ始めて撃沈。霧の中。 6. 多少見えてきたものがあるので話してみようと思う。
3. ご注意 • 理論的な内容に触れますが、私自身にアカデミックなバックグラウンドはない。 厳密性を欠いている可能性があります。 • 人物名は敬称略とさせていただきます。 • 代数的エフェクトは今も進化を続けていますが、この発表では提唱者による限定的 な範囲の代数的エフェクトについて話します。
4. はじめに
5. 代数的エフェクトとハンドラー の ざっくりとした説明 （あとで厳密な説明を書きます）
6. ラベルづけ この発表は、異なる複数のレイヤーの話が混在しており、話している内容の属するレイヤーが切 り替わりながら進行します。 現在どのレイヤーの話をしているかを視覚的にぱっと把握できるようにするため、スライド右上 に以下のラベルを付けています。 [理論] 数学的な構造の話 [橋渡し] 理論とプログラムの見え方をつなぐ話 [プログラム] Koka / Haskell 上での見え方 [注意] 誤解しやすいズレや境界線 [整理] まとめ・地図・章の接続
7. 代数的エフェクトとは？ 今の段階では、代数的エフェクトを 　　　『operation によって計算エフェクトを表現したもの』 としておきます。 （operation の例: ask, get, set, choose） operation は具体的な処理を行いません。 計算エフェクトを表現するものとしては、他には『モナド』がありますね。 【橋渡し】
8. ハンドラーとは エフェクトの operation を利用する関数を書いたとします。 しかし operation とは具体的な処理を行わないものでした。 その operation に対して具体的な処理を与えるものがハンドラーです。 つまり実際のプログラミングにおいては、代数的エフェクトとハンドラーは一緒に扱われ ます。 同じ operation の組み合わせに対し、ハンドラーを差し替えることで別々の処理を行うこ とができます（本番とテストで処理を切り替えるとか）。 【橋渡し】
9. 具体的なコードを用いたサンプル
10. 扱うサンプルコード • 状態を表現するエフェクト State • State が持つ operation ◦ 値を取得する ◦ 値を書き換える • Stateエフェクトを使うサンプル関数の内容 ◦ 数値を扱う State とする。 ◦ 処理内容は以下とする。 1. 数値を取得する。 2. 取得した数値を加算して値を書き換える。 3. 再度数値を取得する。 4. 1と3で取得した値のタプルを返す。 • State のハンドラー ◦ 極力余計なことをしないシンプルなものとする ※後ほど別の言語の例も示しますが、表現する内容はまったく同じものとします。 【プログラム】
11. Koka のコード
12. State エフェクトの宣言 任意の型sを扱えるエフェクトとし、 get,set の operation を宣言している。 【プログラム】
13. サンプル関数 【プログラム】
14. ハンドラー 【プログラム】
15. 実行例 【プログラム】
16. ここまではざっくり ここからはガチ
17. コードを見てきたわけですが
18. コードのどこに『代数』がありましたか？
19. まだ見えていない
20. ということで・・・・・・
21. 提唱者による説明を見てみよう 代数的エフェクトの論文の内容で、代数的エフェクトについて 説明されている箇所をいくつかピックアップしてわっと見ていき ます。 ここは登場する概念をさらうためのセクションであり、すべての 理解は目指しません。
22. 代数的エフェクトとは [GORDON D. PLOTKIN AND MATIJA PRETNAR 2013] HANDLING ALGEBRAIC EFFECTS 代数的エフェクトとは、対象としているエフェクトを生み出す operation をもつ等式理論によって表現できる計算 エフェクトである。この理論の自由モデルは、対応するエフェクトに期待される計算モナドを誘導する。 【理論】
23. 代数的エフェクトとは 集合 A から値を返す計算は、等式理論によって生成される自由モデル F A の要素としてモデル化される。非 決 定性の場合、これらの等式は choose が半束演算であることを述べる。忘却関手を別にすれば、自由モデル関 手は、対応する効果をモデル化するために Moggi が提案したモナドそのものである。そのような等式的提示に よってモナドが得られる効果を algebraic と呼ぶ。対応するモナドはちょうど ranked monads である。 [GORDON D. PLOTKIN AND MATIJA PRETNAR 2013] HANDLING ALGEBRAIC EFFECTS 【理論】
24. 代数的エフェクトとは [Gordon Plotkin and John Power 2002] Notions of Computation Determine Monads この論文の立場は、計算エフェクトはモナドを決定するが、モナドと同一視されるものではない、というものであ る。われわれは、計算エフェクトは演算の族によって実現され、その等式理論によってモナドが生成されると考 える。 【理論】
25. 代数的エフェクトとは [Gordon Plotkin and John Power 2002] Notions of Computation Determine Monads 【理論】
26. 代数的エフェクトとは 【理論】 [Gordon Plotkin and John Power 2002] Notions of Computation Determine Monads
27. 代数的エフェクトとは [Gordon Plotkin and John Power 2003] Algebraic Operations and Generic Effects 【理論】
28. 代数的エフェクトとは 【理論】
29. まとめてみると 代数的エフェクトは、計算エフェクトの一種である。 Plotkin–Power の見方では、計算エフェクトは次の二つによって表現される。 ・効果の発生源を表す operation の集合 ・それらの operation の性質を記述する等式理論 この等式理論から、値集合 A 上の自由モデル F A が構成される。 A の値を返す計算は、この自由モデル F A の要素としてモデル化される。 さらに、自由モデル関手 F と忘却関手 U から得られるモナド U F が、対応するエフェクトを表す計算モナドになる。 このように、等式的提示から計算モナドが得られるエフェクトを algebraic と呼ぶ。 ただし、この立場では、計算エフェクトはモナドを決定するが、計算エフェクトそのものをモナドと同一視するわけではない。 【理論】【補足】
30. 「代数的」には、もう一つの使い方がある ここまで見ているのは、 計算エフェクトが 代数的 である という話です。 一方、文献では、 operation そのものが 代数的 である という別の使い方もあります。 この二つは関係していますが、同じ定義ではありません。 operation が代数的であるとはどういうことかは、本発表では割愛します。 【理論】【補足】
31. 計算エフェクト ・代数的エフェクト 代数的エフェクトを表すもの ・operation ・等式 ・等式理論 / 等式的提示 等式理論から作られるもの ・モデル ・自由モデル ・自由モデル関手 F ・忘却関手 U ・モナド UF 意味論上の対応 ・値を返す計算 = 自由モデルの要素 ・計算モナド = UF 登場した要素の整理 馴染みのない言葉が並んでいるかもしれません が、前述の通り今回完全理解は目指しません。 【整理】
32. なぜ代数的エフェクトが考えられたのか 登場の流れ
33. Moggi
34. Moggi はどう考えたか [EUGENIO MOGGI] Notions of Computation and Monads 【理論】
35. Plotkin, Power
36. Plotkin, Power [Gordon Plotkin and John Power 2002] Notions of Computation Determine Monads Moggiのモデル化への統一的なアプローチは、例えば関数型プログラミングにおいて有用であることが証明さ れています。 しかし、様々なエフェクトを比較し対照するための精密な数学的基礎がありませんでした。 【理論】
37. Plotkin, Power [Gordon Plotkin and John Power 2003] Algebraic Operations and Generic Effects 【理論】
38. Plotkin, Power [Gordon Plotkin and John Power 2003] Algebraic Operations and Generic Effects 【理論】
39. まとめ 計算エフェクトの表現方法 • Moggi は、計算エフェクトを対応するモナドによってモデル化した。 • Plotkin–Power らは、計算エフェクトを operation と等式から見る。 両者は対立しているわけではない。 • Moggi の見方では、計算エフェクトに対応するモナドを考える。 • Plotkin–Power らの見方では、まず計算エフェクトを実現する operation と、その 性質を表す等式を考える。 そして、その等式理論からモナドが生成される。 つまり、どちらもモナドに到達するが、代数的エフェクトの見方では、モナドは operation と等式から結果として現れる。 【整理】
40. 計算エフェクトを operation と等式で見る、という方向 が代数的エフェクトの理論につながる。 ということで、operation を持つという等式理論などを 見ていく。 【整理】
41. 等式理論とは 【理論】
42. 等式理論とは 【Adámek, J., Rosicky, J. and Vitale, E. M. (draft) Algebraic Theories による等式理論の定義】 　※書籍のドラフト版（以前無料で公開されていた） 【代数的エフェクトの説明】 代数的エフェクトとは、対象としているエフェクトを生み出す operation をもつ等式理論 によって表現できる計算 エフェクトである。この理論の自由モデルは、対応するエフェクトに期待される計算モナドを誘導する。 専門性の高い用語のオンパレードになっているので、ざっくり説明していきます。 【理論】
43. これを軸に 説明します 【理論】
44. いくぞ！
45. まずは です 【理論】
46. Σ 【余談】 テキストの流れでは、プログラムでいう単一の型のみを考え るところから定義して、後から複数の型を扱えるように拡張し ていきます。 【理論】
47. get / set は木の中でどう見えるか Koka のコード上では、 get と set は次のように見えます。 get: 値を渡さずに呼び出す。 結果として、現在の状態値を受け取る。 set(s): 新しい状態値 s を渡して呼び出す。 結果として、特に意味のある値は返さない。 しかし、木として見ると、注目する場所が少し変わります。 get は、結果として得られる状態値によって、次の計算が分かれます。 たとえば状態が整数なら、 ・0 が得られた場合の次の計算 ・1 が得られた場合の次の計算 ・2 が得られた場合の次の計算 ・… という枝を持つように見えます。 一方、set(s) は、状態値 s を記録したあと、次の計算へ一本道で進むように見えます。 【理論】
48. Σ-項、Σ-木 【理論】
49. コードとΣ-木のイメージ get / set という operation 記号に注目して描いた Σ-木。 get は状態値ごとに分岐するため、 state<int> では int の値 の数だけ枝がある。 ここではまだ具体的な state の意味は考えず、operation の つながりだけを描いている。 【橋渡し】
50. 次は です 【理論】
51. E は、Σ-項同士の等式の集合です。 【理論】
52. 等式を書いてみる（ここでの記法） ここでの `return a` は、Koka の構文そのものではなく、 Σ-木の葉を表すための記法です。 `return a` 値 `a` を返して計算が終わる葉を表す。 `get(s -> T_s)` `get` によって得られる状態値を `s` とし、その値に応じて次の項 `T_s` へ進む。 `set(s); T` `set(s)` を行い、その後に項 `T` へ進む。 【理論】
53. State effect は get / set という operation だけ でなく、それらが満たすべき law によって特徴づ けられる。 【理論】
54. KokaのStateでの等式（擬似コード） この記法で、State の代表的な law は次のように書けます。 1. get した値をそのまま set し直すなら、何もしないのと同じ。 `get(s -> set(s); return ()) = return ()` 2. set を二回続けると、最後の set だけが残る。 `set(s); set(t); return v = set(t); return v` 3. set の直後に get すると、set した値が得られる。 `set(s); get(x -> return x) = set(s); return s` 4. 状態を変えずに get を二回行うと、同じ値が得られる。 `get(s -> get(t -> return (s,t))) = get(s -> return (s,s))` 5. 4 の具体例として、2回 get した値を使って set する場合。 `get(s -> get(t -> set(s + t); return (s,t))) = get(s -> set(s + s); return (s,s))` 【橋渡し】 ※これは厳密な公理リストではなく、直感を掴むための代表例です
55. 実際のプログラミング言語における等式 等式理論としては等式が求められるが、これらの等式が必ずしもそのままプログラミング言語の機能 として要求されるわけではない。 Koka では get / set という operation と、それを解釈する handler は書ける。 しかし、その handler が State law を満たすかどうかは、処理系が一般に証明してくれるわけではな い。 必要なら、仕様やテストとして確認することになる。 【橋渡し】
56. KokaのStateでの等式（テスト） 【プログラム】
57. KokaのStateでの等式（テスト） これらのテストは、 run-state handler が State law に沿って振る舞っているかを確認している。 ただし、これは言語が等式を強制しているという意味ではない。 ここで確認しているのは、あくまでこの handler 実装が、期待される State の振る舞いを満たしているかどうかである。 【プログラム】
58. Σ-木と等式 等式を入れると、別々の Σ-木を「同じ計算」とみなせるようになる。 ただし今回は、この商構成の詳細には踏み込まない。 【橋渡し】
59. 理論側： operation + 等式でエフェクトを特徴づける 実用言語側： operation + handler は書ける 等式は多くの場合、処理系が直接扱わない ここでのまとめ 【整理】
60. ここまできた 代数的エフェクトとは、対象としているエフェクトを生み出す operation をもつ等式理論 によって表現できる計算 エフェクトである。この理論の自由モデルは、対応するエフェクトに期待される計算モナドを誘導する。 次は「この理論の自由モデルは、対応するエフェクトに期待される計算モナドを誘導する。 」 【整理】
61. この理論の自由モデルは、対応するエフェクトに 期待される計算モナドを誘導する。 【理論】
62. 自由モデル⇛モナドまでの道のり この対応について簡単に説明するのは困難なため、以下の道筋で説明します。 1. ゴールの確認 どういう条件を満たせばモナドが誘導できたといえるのか 2. スタートの確認 そもそも自由モデルとは何なのか 3. スタートからゴールまで 自由モデルから出発して、どのようにモナドが誘導されるか 【整理】
63. ここでお詫び
64. 圏論の話をまったく出さないで説明をした かったけど無理でした。。。 よって圏論の話を頑張ってします。
65. 予備知識
66. ここで説明する基本的な概念 • 圏 • 関手 • 自然変換 • 随伴 • モナド ※主目的から外れるため、あまり厳密には説明しません。 　ざっくりな説明になることをご容赦ください。 　深い意味を考えず記号の形を視覚的に見ていくのがよいかもしれません。 【整理】
67. 圏は、対象と射からなり、射の合成と恒等射を備えた構造である。 ただし、射の合成について結合則と単位則が成り立つ。 圏 圏の例 【理論】 【ざっくり説明】 圏は、対象と、その対象どうしを結ぶ射を集めたも のです。 射は続けて合成できます。
68. 圏　 圏 　 は、集合を対象とし、集合間の写像を射とする圏である。 の中の一部の例 ※恒等射は省略 【理論】
69. 関手 関手の例 ※恒等射やその対応および合成などは省略 【理論】 【ざっくり説明】 関手は、ある圏の対象と射を、別の圏の 対象と射へ対応させるものです。
70. 関手 Maybe 先ほどのSetの例の一部を再利用し、Haskellなどで馴染みのある Maybe を関手とした 例。 【理論】
71. 自然変換 ※このような図式を可換図式という 【理論】 【ざっくり説明】 自然変換は、二つの関手の間の対応です。 各対象について、一方の関手で写した結果から、 もう一方の関手で写した結果への射を与えます。
72. 自然変換の例 以下の図は、先ほどのSetの例と関手の例を再利用し、List関手とMaybe関手の間の自 然変換の例としたもの。 【理論】
73. モナド ※可換図式 【理論】 【ざっくり説明】 モナドは、一つの圏から同じ圏への関手に、 値をその構造へ入れる自然変換と、二重になった構造 を一重にする自然変換を備えたものです。
74. 随伴にあらわれる単位・余単位 単位・余単位の形 【理論】 【ざっくり説明】 単位：元の対象を、二つの関手を順に適 用した対象へ入れるもの。 余単位：二つの関手を逆の順に適用し た対象を、元の対象へ戻すもの。
75. 随伴 【理論】 【ざっくり説明】 二つの関手が、 単位と余単位を通して うまく対応している関係。
76. 随伴からモナドが得られる 【理論】
77. 随伴からモナドが得られる 【理論】
78. 随伴からモナドが得られる 【理論】
79. 「随伴からモナドが得られる」のまとめ図 【理論】 ※T=GFとしている
80. 関係しそうな箇所を抽出 [GORDON D. PLOTKIN AND MATIJA PRETNAR 2013] HANDLING ALGEBRAIC EFFECTS 【理論】
81. モナドを誘導する箇所の説明で登場した要素たち 【理論】
82. 関手が二つ （自由モデル関手と忘却関手）
83. ひょっとして随伴？💡 ・・・・・・そうです。随伴です。
84. 答えは書いてあった [Gordon Plotkin and John Power 2002] Notions of Computation Determine Monads 【理論】
85. 忘却関手と自由関手とは 【理論】
86. 随伴とモナドの図に当てはめてみる 【理論】
87. 2013年論文では Set で見る 【理論】
88. エフェクト理論 【理論】
89. モデルの圏 【理論】
90. 自由モデルの随伴から計算モナドへ 【理論】
91. State の自由モデル 　　 の中身 【橋渡し】
92. 注釈を加えたもの 【橋渡し】
93. プログラムとの対応 【橋渡し】
94. ここで大事なこと ここで大事なのは、Moggi の モナド を最初から仮定するのではなく、operation / 等式 から モナド が現れるということ。 ※ 厳密には、自由モデル関手と忘却関手からモナドが得られる（圏論的な話）。 【理論】
95. ここまでで省略したもの 【注意】
96. 代数的ではないエフェクト：継続 【注意】
97. operation の木をデータ型として露出させる：フ リーモナド on Haskell 【プログラム】
98. 素朴なフリーモナド 【プログラム】
99. State エフェクト これらは、最初のKokaのサンプルと同じ ことをするコードです。 【プログラム】
100. example の get, set を展開すると・・・・・・ このような入れ子構造になる 【プログラム】
101. 木構造として見ると 【橋渡し】
102. ちょっと加工してやると Op を消し、Pure を return に読み替えた木 Koka の例の木 Haskellの方はデータ構造で表すために Op が存在していたが、消してやり、Pure を return に読み替えると、Koka の場合の木と同じ構造になった。 【橋渡し】
103. 同じ operation 木に見えるが、少し違う フリーモナドでは、operation の木をそのままデータとして持ちます。 そのため、形の違う二つの木は、別のデータです。 一方、自由モデルでは、 operation 木を等式まで含めて見ます。 そのため、等式によって同じとされる木は、区別されません。 たとえば State の等式により、 　set(s₁); set(s₂); return a と 　set(s₂); return a が同じとされるなら、 Free monad では形の違う二つの木ですが、 自由モデルでは同じ計算として扱われます。 【注意】【橋渡し】
104. handler 【理論】
105. ハンドラーの説明 等式理論のモデルとは、解釈、すなわち、等式を満たす一つの集合と、各演算に一つずつ対応する写像 の集合である。ハンドラーは、そのような解釈の定義を与える。 【理論】 主な考えは、次の二点である。（1）ハンドラーは、等式理論の、必ずしも自由ではないモデルに対応す る。そして（2）ハンドリングの意味論は、そのようなモデルを対象とし、自由モデルの普遍性によって誘導 される一意な準同型を用いて与えられる。
106. 未処理計算をどう実行するのか 【整理】
107. コードとΣ-木のイメージ handler は、この operation 木を評価するものとして見られます。 【橋渡し】
108. 論文の答え：handler はモデル、handling は準同型 主な考えは、次の二点である。 （1）ハンドラーは、等式理論の、必ずしも自由ではないモデルに対応する。そして （2）ハンドリングの意味論は、そのようなモデルを対象とし、自由モデルの普遍性によって誘導される一意な準同型を用いて 与えられる。 つまり 未処理計算： 自由モデルの側にある handler： 別のモデルを与える handling： handling とは、自由モデルの計算を、 　　　　　 handler が与えるモデルの世界へ移して評価することだと見られる。 です。 ここで、さきほど出てきた自由モデル F(A) が再び効いてきます。 【理論】【橋渡し】
109. handler は、どうモデルに対応するのか 【理論】【橋渡し】
110. 同じ operation、異なる解釈 【理論】【橋渡し】
111. operation だけでは、木全体はまだ読めない 自由モデルの計算は、 operation 木として見ていました。 operation 木には、二種類の部分があります。 • 内部のノード： get や set • 葉： return a 前のスライドでは、 handler に書かれた get と set の処理が、 各 operation の解釈を与えると見ました。 しかし、それだけでは operation 木全体を処理できません。 return a という葉に到達したとき、そこにある値 a を、handler でどのように扱うかも決める必要があります。 したがって、handling には次の二つが必要です。 • get と set のノードをどう処理するか • return a の葉にある値をどう扱うか この二つが決まることで、 operation 木全体の処理が決まります。 【理論】【橋渡し】
112. 葉の値をどう扱うか 【理論】【橋渡し】
113. get のノードをどう扱うか 【理論】【橋渡し】
114. set(s) のノードをどう扱うか 【理論】【橋渡し】
115. 葉とノードの処理を、木全体へ広げる 【理論】【橋渡し】
116. 木全体の処理を、一つの写像として表す 【理論】【橋渡し】
117. handling は operation の解釈を保つ 【理論】【橋渡し】
118. 葉の扱いは、木全体の handling に一意に延長される 【理論】【橋渡し】
119. 図解
120. Koka の handler と対応させる 【橋渡し】
121. example を処理してみる 【橋渡し】
122. ただし：handler が常に正しいとは限らない 【橋渡し】
123. ここまでのまとめ 【注意】
124. 実用言語では 等式 がどこへ行ったのか
125. 実用言語では 等式 はどこへ行ったのか 理論上は、operation だけでなく 等式 まで含めて エフェクト理論 を見る。 しかし実用言語では、多くの場合、operation と handler は書けても、 等式 は言語機能として直接は書かない。 そのため、handler が期待する law を満たすかどうかは、 型システムではなく、仕様・設計・テスト・証明の側に残る。 【整理】
126. エフェクトの合成
127. エフェクトの合成 実用言語では、複数のエフェクトを同時に扱えることが重要です。 State Exception Nondeterminism I/O などを組み合わせて使いたくなりますし、Kokaなども実際そのように使えます。 以下は ask エフェクトを定義し、同時に扱う例 【整理】
128. エフェクトの合成 Koka に限らず、代数的エフェクトを扱えるとされている言語は大抵エフェクトを合成できるため、 　代数的エフェクト = effect を簡単に合成する仕組み という印象を持つかもしれません。 しかし、今回見てきた提唱者側の基本構図は、一つのエフェクト理論についての話でした。 つまり、 　一つの エフェクト を operation / 等式 から見る という構図であって、合成は中心には出てきませんでした。 複数のエフェクトをどう組み合わせるかは、この基本構図の外側にある話です。 【整理】
129. 実用する上では合成は不可欠 前述の通り実用上はエフェクトの合成は避けて通れません。 たとえば、実際のプログラムでは、 状態を読み書きしながら 例外を投げ ログを書き 外部 I/O も行う ということが普通に起きます。 そのため、実用言語では複数のエフェクトを扱える仕組みが重要になります。 合成は、代数的エフェクトの出発点ではありません。 しかし、実用上はすぐに必要になるテーマです。 【整理】
130. operation / 等式で見ると、合成も見えてくる operation / 等式 でエフェクトを見ると、複数のエフェクトを組み合わせる問題も、同じ言葉で考えられます。 たとえば直感的には、 　State の operation / 等式 　Exception の operation / 等式 を合わせて、一つのエフェクト理論として見る、という方向があります。 つまり、 　get, set 　raise を同じ計算の中に持つエフェクト理論を考える、ということです。 【整理】
131. ただし、組み合わせ方は一つではない 複数のエフェクトを合わせるとき、単に operation を並べればすべてが決まるわけではありません。 問題になるのは、たとえば次のようなことです。 • それぞれの等式をどう保つか • エフェクト同士の相互作用をどう扱うか • handler の順序で意味が変わる場合をどう見るか つまり、合成は単なる機能追加ではなく、意味の問題でもあります。 このため、合成は大きな理論的テーマになります。 【整理】
132. 理論側の流れ実装側の流れ ここで、話を「理論側」と「実装側」の二つの流れに分けておきます。 理論側の例： ・複数のエフェクト理論をどう組み合わせるか ・エフェクト同士の相互作用をどう記述するか ・エフェクトシステム や graded monad とどう接続するか 実装側の例： ・Monad transformers ・Free monad ・Coproduct / Data types à la carte ・Extensible Effects ・ 実用言語の effect handlers 【整理】
133. 実装側の問題意識 実装側では、主に次のような問題がありました。 ・複数のエフェクトをどう扱うか ・monad transformer の lift をどう減らすか ・エフェクトを後から追加しやすくできるか ・handler / interpreter を差し替えられるか この流れの中で、 ・Free monad ・Freer monad ・Extensible Effects などの実装技法が発展しました。 ([Oleg Kiselyov, Hiromi Ishii. 2015] Freer Monads, More Extensible Effects [Oleg Kiselyov, Amr Sabry, Cameron Swords. 2013] Extensible Effects: An Alternative to Monad Transformers) これらは、代数的エフェクトの理論から派生して出てきたものではありません。 しかし、後から見ると、 operation 木と handler の考え方で代数的エフェクトに近い構造が見えてきます。 【整理】
134. 理論側の発展 理論側でも、合成やエフェクトの追跡は大きなテーマになります。 複数のエフェクトを扱うと、 ・どのエフェクトを使ったか ・どの範囲でエフェクトが現れるか ・どのリソースに触れる可能性があるか といった情報も問題になります。 この方向で出てくるのが、 Parametric effect monads ※や、その後の Graded Monad の流れです。 (※ [Shin-ya Katsumata 2014] Parametric effect monads and semantics of effect systems) 【理論】
135. Graded Algebraic Theories さらに Graded Monad に対応する operation / 等式 側の理論も整理されています。 （[Satoshi Kura. 2020] Graded Algebraic Theories） 今回見た基本構図では、 　operation / 等式 　自由モデル 　計算モナド という流れを見ました。 Graded の方向では、この対応を Grade つきの世界へ広げます。 また、エフェクトを組み合わせるための sums や tensor products も扱われます。 ここでは深入りしません。 大事なのは、operation / 等式 で エフェクトを見る考え方が、さらに先の理論へ拡張されている、ということです。 【理論】
136. 合成についてのまとめ 代数的エフェクトは、 effect を簡単に合成するための機能 として出発したわけではありません。 出発点は、 計算エフェクトを operation と等式から見ること でした。 しかし、実用上は合成が重要です。 そのため、理論側では合成や Graded Monad の方向へ発展し、実装側では Free monad や Extensible Effects などの流れが発展しまし た。 これらは別々の動機から出てきましたが、後から operation 木、handler、モナドという観点で接続して見えてきます。 【整理】
137. 発展
138. 代数的エフェクトの枠組みは、さまざまな方向へ拡張されています。 （以下はその例の一部です） ・一つの sort だけを見る話 　 → 多ソート / S-ソートへ ・圏 Set 上で考える話 　 → Poset, ω-Cpo, presheaf category などの圏へ ・単純な operation を扱う話 → scope を持つ operation / 計算を引数に取る operation (higher-order operation) へ ・operation と等式で理論を作る話 → enriched / graded な理論へ ・通常の monad で エフェクト を表す話 → Graded Monad へ ・一つの エフェクト を見る話 → 複数の エフェクト を組み合わせる話へ ・通常の handler で処理する話 → scoped / higher-order effects を扱う handler へ 拡張 【整理】
139. おわり