notes mizzy.org

効果の具体化 — planは効果の自由モノイドである

解釈 出典: explorations/2026-06-10-carina-type-system-type-theory/type-system-analysis.md §7 作成/ 更新

静的段階の出力であるplanは、Read / Create / Update / Delete / Import / Remove / Move / Wait / DeferredCreate / DeferredReplaceの10種のEffect値の列である。効果は純粋な値であり、実行は解釈器(Provider)が動的段階で与える。Planeffects: Vec<Effect>を持つserde直列化可能な構造体で、dyn Fnの類を一切抱えていない。

置換(Replace)がこの列に無いことは、この読みにとって偶然ではない。置換は命令ではなく、差分エンジンがCreateとDeleteの対に展開する複合命令である。差分計算は命令選択である

これは副作用の具体化(reification)であり、構造としては「プログラム = 効果の自由構造、意味 = 解釈器」というfree monad / algebraic effectsの発想の初等形に当たる。

free monadではなく自由モノイド

正確にはfree monadではない。ほとんどの効果が継続を持たないからである。効果の結果に依存して次の効果を構成する部分は、大半が静的段階で済ませてある。したがって構造は効果の自由モノイド(列)+ 複数解釈器(実プロバイダ、mock、表示)である — ただしこの呼び方には後述の留保が要る。

効果の並び — Deferred系を除けば継続を持たない Create Update Delete Move … 全10種のEffect値 全要素を列挙・検査・表示・保存できる 解釈器を差し替える 実プロバイダ 世界に作用する mock エミュレートする 表示器 人間に読ませる 効果が値であって手続きでないから、意味を後から与えられる
継続がないからこそ、効果の並びは全要素を並べて読める。同じ並びに対して解釈器を差し替えられることも、この構造の配当である。

この区別は装飾ではない。継続がないからこそplanは全要素を列挙・検査・表示・保存できる。free monadなら「次に何をするか」が関数の中に隠れ、実行するまで中身を見られない。「planは検査可能・表示可能・保存可能であり、applyだけが世界に触る」というCarinaの中心的性質は、自由モノイドであることに直接由来している。

自由モノイドと呼ぶには二点の留保が要る

順序に意味がない。PlanVec<Effect>だが、このVecの順序は実行順ではない。実行順はapply時にapply_edges / destroy_edgesからDAGとして導出される。モノイドの積は連接だが、連接の順序が意味を持たないなら、構造としてはむしろ多重集合 + 導出可能なエッジである。「列」と呼ぶのは実装の格納形式に引きずられた言い方になっている。

Deferred系は脱関数化された継続である。DeferredCreateはtemplateとしてAST片を抱えており、apply後の上流stateに対して再展開されて新しいCreateを生む。関数ではないので「純粋な値」は保てるが、「効果の結果に依存して次の効果を構成する部分は静的段階で済ませてある」は、この2変種については成り立たない。実装はis_scheduler_meta()という述語でこれらを他と区別している。

したがって正確には、Deferred系を除いた部分について、順序を捨てた自由構造である。その上でなら、planが検査可能・表示可能・保存可能であることの説明としては今も効く。

複数解釈器という帰結

同じ効果の列に対して解釈器を差し替えられることも、この構造の配当である。実プロバイダは世界に作用し、mockはエミュレートし、表示器は人間に読ませる。効果が値であって手続きでないから、意味を後から与えられる。

型システムから見た意味

型システムの観点では、静的段階の成果物が「型検査済みの効果プログラム」という明確な中間言語になっていることが重要である。検査と実行の境界がplanという具体的なデータに一致している。抽象的な「検査は実行前に終わる」という主張が、ファイルに書き出して持ち運べる具体物として存在する、ということでもある。

根拠の確度

Effectが10変種であること、Replaceが変種として存在しないこと、PlanVec<Effect>を持つserde直列化可能な構造体でdyn Fnを含まないこと、実行順がapply_edges / destroy_edgesから導出されること、DeferredCreatetemplateにAST片を持ちis_scheduler_meta()で区別されることは、2026-08-16時点のソースで確認済み(carina-core/src/effect.rsplan.rs)。自由モノイド / free monadとの対応づけは解釈である。

初稿は8種としてReadとDeferredCreate / DeferredReplaceを落とし、実装に無いReplaceを含めていた。落としていたDeferred系がまさに継続に当たるものだったので、「継続を持たない」という初稿の主張は、抜けていた変種を入れると弱まる。留保付きで残した。

#効果 #代数 #plan