notes mizzy.org

全域性は後付けできない

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

静的段階の全域性は、実装を頑張れば手に入る種類の性質ではない。言語設計の選択そのものに由来するため、汎用言語に埋め込む方式を選んだ時点で原理的に取れなくなる。

PulumiとCDKは逆の取引をしている。リソースグラフを構築する段階(Pulumiのプログラム実行、CDKのsynth)は、TypeScript / Python / Goといったチューリング完全な汎用言語の任意のプログラム実行である。無限ループも、ネットワークI/Oも、環境変数や現在時刻への依存も書ける。したがって「グラフ構築は必ず停止する」「同じソースから必ず同じグラフが出る」は言語の定理としては成立せず、プログラマとライブラリの行儀に依存する経験則になる。

失われるのは停止性だけではない。Carinaのplanがソースとstateの純関数であるのに対し、synthの出力は外界に依存しうる。CDKのcontext lookupのように、synthの過程でAWSアカウントの現在の状態を取り込む仕組みは公式機能ですらある。

正確には、AWSを呼ぶのはsynth中のプログラム自身ではない。値が足りないとき、appはCDK Toolkitにその旨を通知し、CLIが問い合わせてcdk.context.jsonに書き、その値を渡してappを再実行する(公式ドキュメント)。純関数でなくなるという結論は変わらず、依存先が「呼び出し時のAWS」から「cdk.context.jsonに凍結された、ある時点のAWS」に変わるだけである。公式ドキュメントがこのファイルを「アプリケーションの状態の一部」としてソース管理へのコミットを求めているのは、まさにそれが入力だからである。

そして後付けの道が塞がっている理由がここにある。これを言語保証に戻すには汎用言語をサブセット化するしかなく、それはもう別言語を作ることと同じである。全域性は「構文制限 + 参照グラフの非循環性強制」の合わせ技であり、既存のホスト言語に対して外から課せるものではない。

この構図は設計空間の象限としても現れる。「汎用言語埋め込みかつ全域的」という象限が空なのは偶然ではなく、ホスト言語をサブセット化しない限り埋まらない。

#全域性 #言語設計 #iac