属性の出所は型に昇格させるべきモダリティである
「この属性は誰が書くのか」— ユーザー指定か、プロバイダ算出か、サーバ既定か — という区別が、Carinaでは型に乗っていない。フラグと投影で表現されている。これが理論的な負債になっている。
症状の出方
出所が型の外にあると、差分計算のたびに個別対処が要る。代表例が「見かけの削除」問題である。ユーザーが書いていない属性にサーバが既定値を入れた場合、次の差分計算でその属性が「消える」ように見える。実際には誰も消そうとしていないが、比較の両側で出所が違うことを型が知らないため、差分器はそれを検出できない。
この種の症状はひとつではない。出所の区別が必要になる場面が増えるたびにフラグと投影の処理が足され、症状が出るたびに個別対処になりやすい構造ができている。
型に昇格させると何が変わるか
属性の出所を型上のモダリティとして昇格させれば、現在フラグと投影で行っている差分の補正が型主導の操作になる。
差分計算は既に型主導である。等価性は型ごとに定義され、正規化は型に導かれて走る。出所が型に乗れば、出所ごとの比較規則もその枠組みに載る — 「ユーザー指定でない属性はユーザー側の欠落を差分としない」といった規則が、個別の補正処理ではなく型ごとの同値関係の一部になる。
これは「区別を型に昇格させる」という、この型システムの負債群に共通する解の形でもある。検査器の二重実装、二つの型言語の非対称、タグなし合併の曖昧さも含め、負債はいずれも「定義を一つにし、区別を型に昇格させる」方向に解がある。