動的段階の効果の閉包性はP1完全性とP2帰属性に分解できる
「動的段階では、コードに書いたこと以外の副作用が発生しない」という性質を動的段階の効果の閉包性と呼ぶと、これは二つの独立した命題に分解できる。
- P1(完全性):動的段階で起きる効果はすべて実行前の成果物に列挙されている。エンジンが勝手に足さず、ユーザーコードが途中で混ざらない。
- P2(帰属性):成果物の各効果はユーザーが書いたコードに遡れる。ライブラリが黙って注入しない。
モノイド性が「成果物に継続が残らない」という静的側の性質だとすれば、閉包性はその実行時側の対偶である。
Carinaは両方を構造的に満たす
applyが実行するのはplanに列挙されたEffectだけで、apply中にユーザーコードが走る仕組み(フック、プロビジョナ、コールバック)はない。失敗時の自動ロールバックもなく、途中失敗は中途状態で止まるだけで、誰も書いていない削除をエンジンが自律的に実行することはない。モジュールやforは展開結果がそのままplanに見える糖衣で、書いていないリソースを注入する層がない。
ただし条件が二つある。第一に、性質が成り立つのはEffectの粒度である。1効果の実装としてプロバイダは複数のAPI呼び出しを行い、クラウド側が付随リソースを暗黙に作ることもある。第二に、プロバイダは効果を忠実に実装すると信頼されたコードである。ただしWASMサンドボックス内で動きI/Oがホスト経由なので、この信頼を機構で縛る余地が構造的にある。
CDKとPulumiの破れ方は違う
CDKはP1にもP2にも破れがある。CloudFormationは失敗時に自動ロールバックする — 作ったものを勝手に消すという、誰も書いていない効果をエンジンが自律的に実行する。カスタムリソース(Lambda-backed)はデプロイ中に任意コードを走らせ、その副作用はテンプレートから不透明である。そしてP2の破れは日常的で、constructライブラリは利用者が書いていないリソース(補助Lambda、IAMロール)をスタックに注入する。成果物には載るので「テンプレートに対する完全性」は保たれるが、「コードに書いたこと」への帰属は薄れる。
PulumiはP1が言語構造として成立しない。Output.applyのコールバックとdynamic providerはデプロイ中に任意のユーザーコードを実行し、そのコードはリソースとして表現されない副作用を自由に持てて、previewには現れない。行儀よく書けば満たせるが、言語は保証しない — モナド的という構造の帰結である。
| P1:効果は成果物に閉じる | P2:効果はユーザーコードに遡れる | |
|---|---|---|
| Carina | 成り立つ(Effect粒度、プロバイダを信頼の根として) | 成り立つ |
| CDK | 破れ(自動ロールバック、カスタムリソース) | 破れ(constructの暗黙注入) |
| Pulumi | 構造的に不成立(デプロイ中の任意コード) | CDKと同様の注入あり |
P1とP2に分けることの利点は、破れ方の質が区別できる点にある。P1の破れは「見えない効果が起きる」、P2の破れは「見える効果の出所が辿れない」であり、前者はレビューを無効化し、後者はレビューを重くする。