等価判定は正規形へ簡約してから型ごとに行う
差分計算の中核にあるのは、等価性が型ごとに定義される(type-directed equality) という原則である。同じ値の組でも、期待される型によって判定が変わる。
- 順序付きリストは列として位置比較、順序なしリストは多重集合として比較(
Listのorderedフラグが「列(sequence)」と「多重集合(multiset)」を同じ構成子で表し分けている) - 列挙はプロバイダAPI値の正規形で比較し、公称識別が両側にあればidentityも厳密に比較
- 合併型はメンバを順に試す(合併の等価性はメンバ等価性の存在量化)
- 秘匿値はハッシュ経由で比較し、平文を状態に残さない
正規化が先に来る
比較の前には正規化が入る。Union[String, List<String>]の標準形化、DSL綴りの列挙値からAPI正規形への解決などを型に導かれて行い、正規形(canonical form)同士でのみ等価性を判定する。
型理論の言葉では、値の同値関係を型ごとの定義的等価(definitional equality)として与え、判定は正規形への簡約を経てから行う、という型付き等価性の標準的な構成である。
正規化を飛ばすと壊れる
この構成には理論側からの予言が付いてくる。正規形を経ない等価判定は不健全である。
そして実際にその形の事故が起きている。state中の列挙値が永遠に変更扱いされ続ける現象は、正規化を経ない比較経路が残っていたことが原因だった。DSL綴りのまま保存された値とAPI正規形の値を直接比較すれば、意味的に同じ値が毎回「変わった」と判定され続ける。差分が中心機能であるツールにおいて、これは機能が静かに無意味になる種類のバグである。
裏返せば、等価性・正規化が型主導で一元化されていること自体がCarinaの強みである。差分という中心機能が「正規形に簡約してから型ごとの同値関係で比較」という単一の原則に載っており、比較経路が増えるたびに個別対処するのではなく、原則から外れた経路を潰す形で議論できる。