第 6 課: 回復可能なエフェクト: インストールできて、アンインストールもできる

一言でいうと: 回復可能なエフェクトは「副作用」を「変換 + 逆変換」に作り替えます——環境を変更するたびに自動的に「逆の鍵」が用意され、インストール時に帳簿に記録され、アンインストール時に逆順で自動的に元に戻されます。これ以降、「アンインストールしても痕跡を残さない」は手書きのクリーンアップコードを必要とせず、構造そのものによって保証されます。

ステップ 1: 復習——時間合成可能性は「取り外せること」を要求する

前の課では「箱(モナド)」を使って副作用を明示的で制御可能なものにしました。しかし明示的にすることは第一歩にすぎません。この論文が本当に求めているのは動的な合成です: 実行時にコンポーネントをインストールし、使い終わったら取り外す——まるで OS がドライバをロードしたり、DSH がプラグインをマウントしたりするように。

論文はこの能力に正式な名前をつけています: 時間合成可能性(time composability)。それは次のことを要求します:

• コンポーネントは実行時にロードできる;
• コンポーネントは実行時にアンロードできる;
• アンロード時には、共有環境が合成前の状態に復元されなければならない——インストール前がどんな状態だったなら、取り外した後も同じ状態でなければなりません。

🏠 たとえ話: 寮に新しいルームメイトが引っ越してきて、壁に釘を打って装飾画を掛けました。ルームメイトが出て行くとき、壁は元通りにしなければなりません——さもないと次に入ってくるルームメイトは、穴だらけの壁を見ることになります。

ここから一つの厳しい要求が導かれます: コンポーネントが環境に加えるすべての変更は、追跡可能かつ可逆でなければなりません。

• 追跡可能(trackable): システムは何を変更したかを把握していなければならない;
• 可逆(invertible): システムはすべての変更を正確に取り消せなければならない。

この 2 つを満たさないとどうなるでしょうか? 最も典型的な結果はクリーンアップロジックの手書きです: 各コンポーネントがアンロード時に自分で「復元コード」を書きます。たくさん書けば漏れやミス、忘れが発生します——一か所でも忘れれば環境はこっそり汚染され、積み重なるほど追跡不能になります。論文の答えは: プログラマに手書きでクリーンアップさせるな、「取り消し」をエフェクト自体の構造的性質にせよ。

ステップ 2: 核心となる考え——すべての変換に「逆の鍵」を備える

どうすれば「手書きのクリーンアップ」を不要にできるでしょうか? 論文の発想はとても素朴です: エフェクトを「変換 + 逆変換」の関数としてモデル化する。

純粋関数の形をしたエフェクトは次のようになります:

f : Γ × X → Γ × Y

読めなくても大丈夫です。平易な言葉に翻訳すると: 環境 Γ と入力 X を受け取り、変更後の環境と戻り値 Y を出力する。 そして重要なアップグレードがこの行です:

エフェクト : Γ → Γ × (Γ → Γ)

意味はこうです: エフェクトを現在の環境に適用すると、変更後の環境に加えて、追加で明示的な逆関数(Γ から Γ への関数)が返されます。この逆関数こそが「逆の鍵」です:

• インストール時: 環境は γ から f(γ) に変わる;
• 取り外し時: 逆関数 f⁻¹ を取り出し、環境は f(γ) から γ に戻る。

🚿 たとえ話(キッチン編): 食器洗い機を設置するとします。設置時に水道管をつなぎ替え、電気回路をいじりました——一つ一つの変更を記録します: 「給水管をここにつないだ」「回路をそこからここに移した」と。後で食器洗い機を外すとき、思い出す必要はありません。メモに従って一歩ずつ復元すれば、キッチンは元通りです。

🧳 たとえ話(荷物編): 出張でホテルに泊まり、部屋を好きなように模様替えしました(スタンドを枕元に移動し、本を本棚に並べる)。チェックアウト時に元の位置をすべて覚えている必要はありません——「復元チェックリスト」さえあれば、それに従って戻すだけです。逆変換はまさにこのチェックリストです。

逆関数をランタイムに返すことで、一石二鳥になります:

• 可逆: f⁻¹ があれば、どんな変更でも取り消せる;
• 追跡可能: ランタイムはすべての f⁻¹ を集めるので、コンポーネントが何を変更したかが分かる。

論文はこの種のエフェクトを**回復可能なエフェクト(revertible effect)**と呼んでいます: 実行中にこれらの逆関数を記録・合成すれば、環境の完全な復元はもはやプログラマの義務ではなく、構造的な保証になります。

図は 3 つの部分からなります: コンポーネントのインストール時に変換 f が実行され、引き出しに f⁻¹ が自動的に保存されます; アンロード時に f⁻¹ が適用され、環境が復元されます——インストール時に記録し、取り外し時に復元する——その間に手書きのクリーンアップコードは一行もありません。

ステップ 3: エフェクトコンテキスト ∂Γ = Γ × 𝔉Γ——「状態 + 帳簿」

逆の鍵はできました。それをどこに保存するのでしょうか? 論文は新しいものを発明しました: エフェクトコンテキスト(effect context)。

まず記法を導入します: 𝔉Γ をすべての「許容可能なエフェクト」の集合とします(𝔉 は筆記体の F)。これらのエフェクトは 3 つの公理を満たします:

この 3 つを合わせると、𝔉Γ は合成演算 ∘ の下で群を構成します——「どうインストールしても、どうアンインストールできる」ことが数学的に保証されます。一つのスコープ上の制約に注意してください: Γ がモデル化するのはシステムが完全に掌握する内部状態だけです。ネットワークリクエストやファイル I/O のようなシステム外部に向かう操作は Γ を変更しないため、𝔉Γ の観点からは何もしていない(idΓ)のと同じで、ドメイン固有のポリシー(補償トランザクションなど)が別途処理します。

次に本節で最も重要な定義です:

定義 1(エフェクトコンテキスト): コンテキスト Γ が与えられたとき、エフェクトコンテキストは次のように定義されます。 ∂Γ = Γ × 𝔉Γ

これは 2 つの組 (γ, φ) として理解できます:

• γ ∈ Γ: 現在のコンテキスト状態;
• φ ∈ 𝔉Γ: コンテキストを初期状態に復元する変換(累積された逆変換の帳簿)。

特に、初期状態は (γ₀, idΓ) です——状態は最初の γ₀ で、帳簿はまだ空(恒等変換)です。

🧳 荷物編: ∂Γ は「スーツケース + 復元チェックリスト」です。γ はスーツケースの現在の姿、φ はチェックリストに累積された復元手順です。出発直後、スーツケースは元のままの γ₀ で、チェックリストは空っぽ(idΓ)です。

この 2 つの組があれば、インストール/取り外しは 2 つの自動化された操作——track と recover——になります。

track: インストール時の自動記帳

定義 2(trackΓ): trackΓ = f ↦ (γ, φ) ↦ (f(γ), φ ∘ f⁻¹)

読み方: 通常の変換 f を「実行しながら逆を記録する」バージョンに変える。trackΓ(f) を実行すると:

• 状態部分: f を適用し、γ は f(γ) になる;
• 帳簿部分: f の逆 f⁻¹ を φ に追加(∘ で合成)し、φ は φ ∘ f⁻¹ になる。

コンポーネントのインストール = 環境の変更 + 逆変換の自動記帳。 コンポーネントは記帳について一切気にする必要がありません。

論文はさらに 2 つの保証(定理 3、定理 4)を示しています。直感的に理解できれば十分です:

• 定理 3(追跡は振る舞いを変えない): pr1 ∘ trackΓ(f) = f ∘ pr1——track 版は「状態成分」での振る舞いが元の変換とまったく同じ。帳簿は追加されるが、通常の使用には影響しない;
• 定理 4(追跡は合成を保つ): trackΓ(f ∘ g) = trackΓ(f) ∘ trackΓ(g)——先に合成してから追跡することは、先に追跡してから合成することと等しい。つまり逆変換の記帳は安心して積み重ねられます: 10 個のコンポーネントをインストールすれば、帳簿には 10 個の逆変換があり、構造は乱れません。

recover: 取り外し時の自動復元

定義 5(recoverΓ): recoverΓ = (γ, φ) ↦ (φ(γ), idΓ)

読み方: 帳簿 φ を全体として現在の状態 γ に適用し、復元された環境 φ(γ) を得る。そして帳簿を空にし、φ を恒等変換 idΓ にリセットする。

φ には逆変換が累積されており、新しい逆変換が後ろに並び、先に適用されるため、復元はちょうど後にインストールしたものから先に外す、逆順の取り消しになります——自動再生される一連の取り消し操作のように、環境を一歩ずつ最初の γ₀ へと押し戻します。

ステップ 4: インストール時に自動記帳、取り外し時に自動復元

track と recover を組み合わせると、完全な「インストール → 取り外し」サイクルになります:

初期           (γ₀, idΓ)
f₁ をインストール  →  (f₁(γ₀), idΓ ∘ f₁⁻¹)
f₂ をインストール  →  (f₂(f₁(γ₀)), f₁⁻¹ ∘ f₂⁻¹)
f₃ をインストール  →  (f₃(f₂(f₁(γ₀))), f₁⁻¹ ∘ f₂⁻¹ ∘ f₃⁻¹)
recover で取り外し →  (γ₀, idΓ)

最後の行を見てください: recover は 3 つの逆変換を逆順に順次適用し、環境は正確に γ₀ に戻り、帳簿は空になります——サイクル全体が閉じています。

🎮 日常版: ゲームで、キャラクターに 3 つのバフ(力、速度、シールド)を連続して付与する場面を想像してください。システムはバフを付与したその瞬間に、対応する「取り消しカード」を自動的に記録します。バフを間違えた? 「復元」をタップすれば、システムは後に付与したものから先に順にバフを取り消し、キャラクターはバフ前の状態に戻ります——カードを 1 枚も漏らしません——あなたは「取り消しロジック」を一行も書いていません。それは仕組みそのものによって保証されます。

なぜこれが「構造的保証」であり、また別の「自動でクリーンアップしてくれる」魔法ではないのでしょうか? 保証が構造そのものから来ているからです:

1. 𝔉Γ の逆元公理: すべての変換には逆変換があるため、すべての変更は取り消し可能;
2. 定理 4 の合成保持: 逆変換を任意に合成しても取り消し可能なので、どれだけコンポーネントをインストールしても、1 回の recover ですべて復元できる;
3. track は記帳をエフェクト自体に組み込むため、プログラマには記録を漏らす機会がない——記録漏れは手書き方式にしか存在しないバグです。

言い換えれば: コンポーネントが track を通じて変換を適用し、アンロード時に recover で締めくくる限り、環境の復元は数学的に保証が成立する事柄であり、プログラマが覚えているかどうかとは無関係です。

💡 本線に戻る: これこそが DSH の「インストールしたものは取り外せ、取り外しても痕跡を残さない」という理論的な出所です——エージェントが実行時にプラグインを安全にマウント/アンマウントできるのは、基盤となるすべてのエフェクトが逆変換を持ち歩いているからであり、アンロード = 逆変換の再生なのです。

重要ポイントの振り返り

1. 時間合成可能性 = 実行時にコンポーネントをロード/アンロードでき、アンロード時に共有環境が元の状態に復元される。すべての変更は追跡可能かつ可逆でなければなりません。
2. 回復可能なエフェクト = エフェクトを「変換 + 逆変換」としてモデル化する: Γ → Γ × (Γ → Γ)。逆関数をランタイムに返すことで、取り消しは構造的保証になります。
3. エフェクトコンテキスト ∂Γ = Γ × 𝔉Γ: 2 つの組 (γ, φ)——γ は現在の状態、φ は累積された復元変換(逆変換の帳簿)で、初期値は (γ₀, idΓ)。
4. trackΓ は通常の変換を「実行しながら逆を記録する」バージョンに変えます: (γ, φ) ↦ (f(γ), φ ∘ f⁻¹)。recoverΓ は φ を全体として適用した後、idΓ にリセットします: (γ, φ) ↦ (φ(γ), idΓ)。
5. 構造的保証: 逆元公理が取り消し可能性を保証し、定理 4 が任意の合成のワンクリック取り消しを保証し、track が記帳をエフェクトに組み込みます——だから手書きのクリーンアップロジックは不要です。

🚀 次の課「第 7 課: エフェクト関数と合成: 逆変換の自動合成」では、逆変換がどのように自動合成されるかを詳しく見ていきます——定理 4 が一体何を保証しているのか、複数のエフェクトが重なっても「ワンクリック取り消し」がなぜ依然として成立するのかを。