notes mizzy.org

同値関係を方向付き判定に流用すると抽象から具体への代入が漏れる

確認済み 出典: audits/2026-05-23-type-system-evaluation.md §3.3 (n), §5 / carina-core/src/schema/type_identity.rs (2026-08-16時点) 作成/ 更新

公称識別の軸ごとの包摂は、設計としては方向付きである。受け側が特定している軸は送り側も一致していなければならず、受け側が特定していない軸は問わない。ところがその判定に使われている関数は対称な同値関係として書かれている

TypeIdentity::same_typeの規則は「各軸について、両方が値を持っているときだけ一致を要求し、片方が空なら通す」である。この規則は左右を入れ替えても成り立つ。にもかかわらず代入可能性判定のカスタム型どうしのアームは、これを送り側から受け側への片方向の包摂判定として呼んでいる。

抽象 — aws.Arn segments未指定 具体 — aws.iam.Role.Arn segments指定 具体→抽象: 通る(正しい) 抽象→具体: 通ってしまう(漏れ) 対称なsame_typeを片方向の判定位置に置いたため、 出元不明の汎用ARNが具体型だけを受けるべき属性に流れる。
同値関係は左右対称なので、片方向の包摂判定の位置に置くと逆向きの矢も同時に通る。設計として通したいのは片方だけである。

何が漏れるか

結果として、本来拒否すべき抽象から具体への代入が通る

generic  = aws.Arn                 // segments 未指定
role_arn = aws.iam.Role.Arn        // segments 指定

generic.is_assignable_to(&role_arn)   // 通ってしまう ✗
role_arn.is_assignable_to(&generic)   // 通る (これは正しい)

出元不明の汎用ARN — 実体はaws.acm.Certificate.Arnかもしれない値 — を、aws.iam.Role.Arnだけを受けるべき属性に渡せてしまう。プロバイダ軸ではクラウド跨ぎの混同を型で弾けているのに、セグメント軸では同じ設計目標が達成されていない(carina#3218)。

同じアームの中に正しい形がある

この漏れが際立つのは、同じ判定アームの中で他の制約は方向付きに書かれているからである。パターンは受け側が持っていて送り側が持たなければ拒否し、区間は送り側が受け側に包含されることを要求する。方向を持つのが当然という前提で書かれた規則の列に、identityだけが対称な関係として混じっている。

さらに同じ判定関数の中には「識別を持たない送り側から識別を持つ受け側への代入は拒否する」という規則があり、コメントに「送り側は識別の証明を持たない」と明記されている。その精神をTypeIdentity内部の軸にも適用すれば直る — 対称なsame_typeと方向付きのassignable_toを別の関数に分離し、具体から抽象は通し、抽象から具体は拒否する。

バグクラスとしての形

これは単発の実装ミスではなく、名前の付くバグクラスである。同値関係と半順序は別物であり、前者を後者の位置に置いても型検査は通ってしまう。どちらも二引数の真偽値関数で、シグネチャが同じだからである。区別は名前と使われ方にしかなく、実装言語の型は何も守ってくれない。

だから検出は性質側からしか来ない。反対称性の性質試験があれば、a ≤ b かつ b ≤ a なのに a ≠ b という組を機械的に見つけられた。設計意図と実装挙動のずれが試験の欠落によって見えていなかった、という構図そのものである。

現状(2026-08-16)

この漏れは塞がれている。 上に書いた方向 — 対称なsame_typeと方向付きのassignable_toを別の関数に分離する — がそのまま実装され、TypeIdentity::assignable_toは「受け側がsegmentsを持つなら送り側も同じsegmentsを持たねばならない」という非対称な規則になった。方向性を確かめる単体試験も入っている(assignable_to_is_directional_on_segments)。

ただし直ったのはこの一件だけである。修正の要点だった「区別を型に昇格させる」は起きていない — 対称な関係と方向付きの関係は今も同じ&self, &TypeIdentity -> boolというシグネチャを持ち、判定の位置に取り違えて置いても実装言語の型は何も言わない。上の「バグクラスとしての形」はそのまま残っている。部分型関係の公理化が求める反対称性の性質試験も入っていないので、同じクラスの次の一件を機械的に捕まえる網はまだ無い

同じ構図は「未確定」を表す表現が四つあるノートにも記録がある。そちらはidentity: Noneの三つの意味を分けないまま判定側だけを直した点を指摘していて、表現を変えずに症状を消したという評価が本ノートと一致する。

#型システム #バグクラス #部分型