カスタム型は独立の構成子ではなく篩型である
Carinaに「カスタム型」という独立した型構成子はない。代わりにString / Int / Floatの各変種が制約を持ち運ぶ。つまりカスタム型の正体は基底型を述語で絞り込んだ篩型(refinement types)である。
持ち運ばれる制約は三種類ある。
- 正規表現パターン(
pattern) - 長さ・値域の区間(
length/range、両端の省略で開区間を表現) - 任意の検証関数
これは型理論でいう篩型 — { x: String | P(x) }のように基底型を述語で絞り込んだ型 — に相当する。
任意述語を許せる理由
検査はすべて静的段階で評価済みの値に対して行われるため、篩の述語は決定可能性の心配なしに任意の計算を含められる。項レベルで含意を証明する型システムでは述語の表現力に決定可能性の上限がかかるが、値に適用するだけなら走らせれば済む。完全評価できる言語の利点である。
述語の二系統という代償
一方で、述語のうち構造的な表現を持つのは区間とパターンだけで、それを超える部分は不透明な関数に逃がしている。この非対称は二つの帰結を生む。
第一に、篩の不透明部分(検証関数)は合成も直列化も比較もできない。 構造的な制約(パターン・区間)への寄せが進むほどこの問題は縮むが、現状は二系統の併存であり、どちらで検証されるかが型から読めない。
第二に、述語が一階の表現を持つか否かは、型を直列化してプラグイン境界を越えられるかを分ける線でもある。 構造的な制約は境界の向こうへ運べるが、関数は運べない。実際、篩のパターンがプラグイン境界で脱落する事故(carina#3364)が起きている。
なお値が未解決の参照に対しては、区間の包含までは宣言レベルで照合される。篩型のうち決定可能な断片については、値なしでも含意(部分型)検査が成立しているということでもある。