notes mizzy.org

デプロイ計画がモノイドかモナドかで見通しが決まる

解釈 出典: explorations/2026-06-10-carina-type-system-type-theory/totality-comparison.md §4後半 作成

未知値をめぐる三すくみは、構造の言葉で言い直せる。鍵になる区別は、デプロイ計画が「平らな宣言の集まり」か「継続のつながり」かである。

前者はリストの連結だけでできた構造(モノイド)で、実行前に全要素を列挙・検査できる。後者はPromiseのthenと同じ構造(モナド)で、後続の処理が関数の中に隠れているため、実行するまで中身を見られない。

モノイド — 平らな宣言の集まり Effect Effect Effect Effect …連結だけ 実行前に全要素を列挙・検査できる — 表示されたものが実行されるものの全部 モナド — 継続のつながり Effect λ(値) → 次の計画 ? 継続が関数の中に隠れる — 実行するまで先が見えず、previewは原理的に近似になる
モノイド性が効くのは、それが「成果物が全情報を含む」ことの保証だからである。継続が残る成果物では、表示されたものが実行されるものの全部だと言えなくなる。

リトマス試験

判定は一つの問いで済む。「デプロイ時に決まる値を受けて、次に何を作るかを決めるコールバックを書けるか」

Lambda-backedカスタムリソースはデプロイ中に任意コードを走らせる脱出口だが、CloudFormationから見ても不透明な箱であり、言語構造というより「モノイドの1要素として埋め込まれた別プログラム」である。

なぜこの軸が効くか

CDKとPulumiの違いはこのモナド/モノイドの軸にある。CDKは成果物をモノイドに保った代わりに穴をstring型のまま放置し(Tokenの誤用が無音で壊れる)、Pulumiは穴をOutput<T>という型付きの容器で守った代わりに、その容器がモナドなので継続の中身がpreviewから見えない。

モノイド性が効くのは、それが「成果物が全情報を含む」ことの保証だからである。planという中間表現をユーザーがレビューして承認するワークフローが成立するのは、IRに継続が残らないからにほかならない。継続が残る成果物では、表示されたものが実行されるものの全部だと言えなくなる。

CDKとCarinaの違いは、この軸ではなく全域性の軸にある。成果物は同じモノイドでも、CDKのそれはチューリング完全な任意プログラムが組み立てるので、生成の停止と再現性が言語の保証にならない。

#モナド #構造 #plan