型注釈の言語とスキーマ型は別の言語である
Carinaには型を表す言語が二つある。ユーザーが書く型注釈の言語(TypeExpr)と、プロバイダのスキーマが表すスキーマ型(AttributeType)である。両者は別の言語であり、前者から後者への対応付け(解決)を静的段階の一部として行う。
問題はこの対応付けが部分写像であることにある。両側の表現力が対称ではない。
- リテラル型・構造的合併は注釈側にしかない。
StringLiteralとUnionを組み合わせた'dev' | 'prod'のようなリテラル合併型は注釈側の機能である。 - 篩の制約はスキーマ側にしかない。 パターン・区間・検証関数という篩型の装備はスキーマ型が持つ。
何が帰結するか
対応付けが部分写像であることは、表現できる型の集合が経路によって違うことを意味する。ユーザーが注釈で書ける型と、プロバイダのスキーマが表せる型が一致しない。ある制約は書けるが運べない、ある型は運ばれてくるが書けない、という非対称が構造的に残る。
これは単なる機能不足ではなく、二つの型言語を別々に育てたことの負債である。一方に機能を足すたびに、他方との対応表に穴が増えるか、対応付けの実装が複雑になる。
同種の負債は検査器にもある。plan/validate経路とLSP経路は同じ検査の二重実装であり、意味論の一致(パリティ)を規約と試験で維持している。検査器を一つの定義から導出できていないことのコストである。型言語が二つあることと検査器が二系統あることは、どちらも「定義を一つにできていない」という同じ形の問題であり、解の方向も同じ側にある。