notes mizzy.org

汎用言語埋め込みとの取引は構造的に対称、価値づけは非対称

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

汎用言語埋め込みと専用全域言語の取引は、構造としてはきれいに相補的である。

メタプログラムの項ベース型付け静的段階の全域性・値の全数検査
Pulumi / CDK強い(ホスト言語の型システム)持てない
Carinaほぼ持たない持つ

TypeScriptの型検査は、グラフを組み立てるメタプログラムに対する本物の項ベース静的型付けであり、関数・クラス・パッケージエコシステム(npm / PyPI)による抽象化もそのまま使える。専用言語側が構造として失うのは言語が小さいこと自体で、高階関数・再帰的なデータ変換・外部ライブラリがなく、表現力の上限は言語設計者が用意した構成子で決まる。

しかしドメインに照らした価値づけは対称ではない。表の左列は「持てない」ではなく「要らない」というのが設計上の立場である。IaC言語の意味的本体はリソース定義と依存関係グラフだけであり、その本体に対して項ベース型付けとエコシステムは必要な道具ではない。

この非対称な価値づけこそが設計上の賭けであり、検査様式の全体(意味論的型付け、篩の任意述語、型主導の等価性、Unknownの一貫した意味論)はこの賭けの配当として読める。構造の整理(どちらを取ればどちらを失うか)は客観的に書けるが、どちらを取るかの判断はドメインの性質についての規範的な主張に依存する。

#トレードオフ #設計判断 #比較