部分型関係が公理化されていないと性質の破れを検出できない
代入可能性の判定は、手書きの分岐の集合として書かれている。個々のアームは妥当だが、それらが全体として部分型関係の性質を満たすかはコードでも試験でも保証されていない。反射性・推移性・反対称性のいずれもである。
これは学術的な体系との差がそのまま出ている箇所である。System F<: やDOT calculusでは部分型は判断規則(judgement rules)として記述され、推移性は公理か導出可能な定理として最初から手に入る。手書きの分岐の集合では、規則を一つ足すたびに全体の性質が保たれているかを人間が確かめ直すしかない。
破れは実際に起きている
性質の欠落は抽象的なリスクではない。公称識別の軸で反対称性が破れている実例が既に見つかっている(抽象型から具体型への代入が通る)。反対称性の性質試験があれば機械的に検出できた種類の破れである。
同型の未形式化はもう一箇所ある。変性(共変・反変)がコード上に明示されていない。List<T>やMap<K,V>の変性がどうなっているかは代入可能性判定の再帰の向きから読み取るしかない。読み取れば答えは出る — 全て共変である — が、それは決定が書かれていることを意味しない(変性は書かれていないだけで、既に決まっている)。IaCの値は基本的に読み出し専用なので実害は出ていないものの、Java配列の共変性と同じ不健全性の罠が置かれた状態であり、読むだけなら安全・書き戻しがあれば危険という境界がどこにも書かれていない。
公理化が回帰ネットになる
だから改善の順序が決まる。個々の破れを直すことと、性質を試験で担保することは別の作業であり、後者は前者の再発を防ぐネットになる。反射性・推移性・反対称性を性質試験(property test)として書けば、既知の破れを検出するだけでなく、将来アームを足したときの破れも自動的に捕まる。
これは他の負債と同じ形の解でもある。「一箇所の破れを直す」のは症状への対処で、「性質を機械的に検査する仕組みを置く」のが根の側にある。呼び出し側が覚えていることに依存する不変条件を型の形に作り直すのと同様、規則の集合が満たすべき性質は、人間の注意ではなく試験の形に置き直すまで守られていない。