循環スキーマは名前付きμ型で明示展開する
CloudFormationのWAFv2 Statement → AndStatement → List<Statement>のような循環スキーマを表すため、スキーマは
Schema = { root: 型, defs: 名前 → 型 }という形を取り、型の中にRef(名前)(defsへの参照)が現れる。これはμ型を名前付き定義の組で表す、iso-recursiveな流儀に相当する。展開(unfold)を暗黙の同一視ではなく明示的な操作として扱う、という選択である。
展開が明示操作であることの効果
型の意味を消費する操作(検証・差分・補完)は、参照をdefsに対して一段展開してから進む。展開にはホップ数の上限があるため、壊れた定義に対しても停止する。
equi-recursive的に「参照と展開後を暗黙に同一視する」扱いを避けたのは意図的な設計である。過去には暗黙展開に相当する処理が循環スキーマ上で無限再帰した事故があり(carina#3340系)、その根治として展開を明示操作に一本化した経緯がある。
型でも固定されている
この不変条件は規約ではなく実装言語の型で固定されている。μ型の参照を展開した後の型ビューには参照変種が存在せず、未展開のまま照合する状態がそもそも書けない(carina#3349)。「展開を忘れないこと」を各消費地点が覚えている必要がない形になっている、というのがこの根治の要点である。
equi-recursiveの暗黙同一視は書き手にとって楽だが、無限再帰の可能性を型システムの外に置く。iso-recursiveは展開を一度書かせる代わりに、停止性を構造として担保する。全域性を土台に置く言語では後者が整合する。