notes mizzy.org

未知値の規律と段階分離は三すくみである

解釈 出典: explorations/2026-06-10-carina-type-system-type-theory/totality-comparison.md §4 / 2026-04-26-cdk-pulumi-terraform-carina-comparison/chapter-3-types-schema-and-unknown.md 作成

段階を跨ぐ値(applyまで決まらない値)の扱いに、IaCツールの設計差が最も鮮明に現れる。CDKは段階の分離を保って未知値の規律を失い、Pulumiは未知値の規律を強めて段階の分離を失い、Carinaは言語を小さくすることで両方を同時に手にしている、という三すくみになる。

三つの性質 モノイドの成果物(平らなplan) 型と意味論で守られた穴 全域的な生成器 CDK 段階の分離は保つ 穴の規律を失う(Token = string) Pulumi 穴は型で守る 段階の分離を失う(モナド) Carina 言語を小さくすることで 三つを同時に持つ CDKとPulumiは「穴を型で守ること」と「成果物を平らに保つこと」を片方ずつしか取れていない。
三つの性質を同時に持つのがCarinaの位置である。CDKとPulumiが片方ずつしか取れないのは、どちらもチューリング完全な汎用言語を生成器に選んだことの帰結である。

三者の未知値

CarinaのUnknown は定義された意味論を持つ一級の値である。値の所属検査は葉の位置で素通しし(周囲の構造検査は続く)、等価性は何とも成立せず、未解決参照には宣言型ベースの代入可能性検査が別経路で走る。未知値をどう扱うかが言語の意味論として固定されている

CDKのToken は未解決値のプレースホルダだが、型上はただのstringである。Token.asString()等で生成され、内部にプレースホルダ文字列(${Token[Bucket.Arn.0]}のような形)を持ち、synth時にCloudFormationテンプレートのFn::GetAttFn::Joinへ変換される。ところがif (vpcId === "...")のような分岐や比較に使ってもコンパイルも実行も通り、bucket.bucketArn.split(':')[5]のような文字列操作も呼べてしまう。プレースホルダ文字列への操作として黙って間違った結果を返すのがCDKの有名な落とし穴で、汎用言語に埋め込むと未知値の意味論をホスト言語の制御フローに守らせる手段がない、ということの帰結である。

PulumiのOutput<T> はCDKより規律が強い。型付きのコンテナなので、TypeScript上でOutput<string>を素のstringとして使えば型エラーになり、値に触るにはapply()を経由するしかない。thenを持たないことでawaitが不可能になる。文字列補間もpulumi.interpolateを経由する必要がある。ただしtoStringは既定では例外を投げず、エラー文言を文字列として返す(投げるのはutils.errorOutputString設定時のみ) — つまり `${output}` は既定ではエラーメッセージを黙って埋め込む。previewはapplyのコールバックを近似しない、実行しない未知値の型レベルの規律という一点では三者で最も明示的とも言える。

規律の代価

ただしそのapply()こそが、依存リソースが実体化した後 — つまりdeployの最中 — に実行されるコールバックである。プログラムの一部が動的段階で走るので、pulumi previewは構造的に近似でしかなく、コールバック内の分岐でリソースを作るようなコードはpreviewに現れないことがある。Carinaの「planは動的段階の静的近似であり、近似誤差はUnknownとして明示される」という性質に対して、Pulumiは近似誤差の所在がプログラム中の任意のクロージャに分散する

成果物の構造穴(未知値)の扱い成果物を作る言語
Carinaモノイド(plan + DAG)一級のUnknown(意味論が定義済み)全域的なDSL
CDKモノイド(テンプレート + DAG)Token = ただのstring(誤用が無音)チューリング完全な汎用言語
Pulumiモナド(継続がデプロイ中に走る)Output<T>(型で守られた継続)チューリング完全な汎用言語

「穴を型で守ること」と「成果物を平らに保つこと」を、CDKとPulumiは片方ずつしか取れていない。三つの性質 — モノイドの成果物・型と意味論で守られた穴・全域的な生成器 — を同時に持つのがCarinaの位置である。

なおTerraformは1.6以降refinementsを持ち、「unknownだがnonnull」「unknownだが長さ既知」「unknownだがprefix既知」といった部分情報をunknownフラグの拡張として保持する。依存グラフベースの実行モデルの制約を型システム側で緩和する方向である。

根拠の確度

CDKのTokenが文字列操作で無音に壊れることは、公式ドキュメントと複数の日本語記事で確認済み。

Pulumi Output.applyのデプロイ中実行とpreviewの近似性も、公式のapplyページで一次ソース確認済み。「pulumi upでプログラムが実行されるとき、apply関数はリソースが作られてプロパティが解決するまで待つ」「applyの中で作られたリソースは、outputの値が既にわかっている場合を除きpulumi previewに現れない」「applyの中でリソースを作ることは可能な限り避けるべきで、preview出力が実際のpulumi upの変更と一致しないことがある」と明記されている。SDK側の裏付けは出典ポインタ集にある — applyHelperAsyncがpreview時にfuncを実行せずisKnown: falseのOutputを返す。

CDKのcontext lookupも公式のcontextページで確認済み。ただし挙動は当初の理解より一段細かい。synth中のプログラム自身がAWSを呼ぶのではない — 値が無いとき、appはCDK Toolkitに「contextが足りない」と通知し、CLIがAWSアカウントに問い合わせてcdk.context.jsonに保存し、その値を渡してappを再実行する。結果はキャッシュされ、以降のsynthは同じ値を使う(cdk context --reset / --clearで明示的に捨てるまで)。Vpc.fromLookupのAPI docも「このメソッドを呼ぶとCDK CLI実行時にlookupが起きる」「VPC情報はcdk.context.jsonにキャッシュされ、以降の実行でも同じVPCが使われる」としている。

初稿はOutput<T>toStringが「例外を投げる」としていたが、これは誤り。既定では投げず、エラー文言を文字列として返す(sdk/nodejs/output.ts L23-54、投げるのはutils.errorOutputString設定時のみ)。規律の強さの評価としてはむしろ弱くなる方向の訂正で、既定では `${output}` が黙って通る。2026-08-16に本文を直した。previewはapplyのコールバックを近似しない、実行しない

CDKのcontext lookupの訂正はこのノートの主張を弱めない。むしろ経路が具体化する — キャッシュがある以上、synthの出力は「ソースの純関数」ではなくソースとcdk.context.jsonの関数であり、そのcdk.context.jsonはある時点の外界の写しである。だから公式ドキュメント自身が「アプリケーションの状態の一部なので、ソース管理にコミットせよ」と言っている。全域性は後付けできないの「synthの出力は外界に依存しうる」はこの経路を指す。

#unknown #比較 #iac