タグなし合併の判別はヒューリスティックに頼るしかない
CarinaのUnion(Vec<AttributeType>)はタグなし合併(untagged union) である。「いずれかのメンバが受理すれば妥当」という集合論的合併の意味論を持つ。これには理論的な代償がある。
直和型(tagged sum)と違い、値がどのメンバに属するかを判別子なしに構造照合で推定する必要がある。実装は「最良スコアのメンバを選ぶ」ヒューリスティックに頼っている。
どこまで吸収できるか
メンバ同士が重なる場合(例: Int | Float)は、数値の包摂(Int→Float昇格)で吸収している。しかし重なりの大きい合併を定義すると、正規化先が曖昧になる余地は残る。スコアリングによるメンバ選択は原理的に曖昧であり、判別子付き合併を言語に持たない限り根本解消はしない。
この曖昧さは等価性にも波及する。合併型の等価判定はメンバを順に試す(メンバ等価性の存在量化)構成であり、正規化がどのメンバに寄せるかで結果が変わりうる。差分計算が型主導の正規化に載っている以上、正規化先の曖昧さは差分の曖昧さになる。
発展方向
理論的な解は明快で、合併への判別子導入(またはDSL構文でのtagged union) である。値のどこかにメンバを一意に決めるタグがあれば、判別は推定ではなく参照になる。
なおユーザーが書く型注釈の言語にはStringLiteral(値ひとつだけを持つシングルトン型)があり、Unionと組み合わせると'dev' | 'prod'のようなリテラル合併型が書ける。TypeScriptのリテラル型と同じ構図であり、ユーザー定義の列挙を公称的なEnumを経由せず構造的に表現する手段になっている。リテラル合併に限れば判別は曖昧にならないが、これは注釈側にしかない機能である。