notes mizzy.org

型名の文字列比較で代入可能性を決めるのは構造を捨てている

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

代入可能性判定の最終アームは、二つの型の表示用の名前を文字列として比較するものになっている。

(a, b) => a.type_name() == b.type_name()

構造体のtype_name()"Struct(名前)"であり、フィールド集合の比較ではなく名前の一致である。値の検証側にも、分岐が型名の文字列を経由する箇所がある。

コンテナについても当初は同じ形だった。List<T>type_name()"List<" + T.type_name() + ">"という文字列連結で、一見構造を見ているようだが、実態は入れ子の公称名を文字列に潰したものでしかなかった。この部分は2026-08-15に構造再帰へ直っている(コミットd15d8ce8)。ただし直った動機は文字列化そのものではなく、スキーマを跨いだRef名の偽の受理を塞ぐことだった。副産物としてコンテナの変性が初めて判定に効くようになっている(変性は書かれていないだけで、既に決まっている)。

つまり本ノートが指す負債は部分的に解消されている。最終アームのa.type_name() == b.type_name()は今も残っており(carina#3209はopen)、下に書く三つの理由のうち網羅性と表示名との結合はそこで生きている。コンテナに関する第二の理由 — 型引数を持つ構成子で破綻する — だけが、先に手当てされた形になる。

構造体の代入可能性が公称であること自体は意図した設計判断である(プロバイダを跨いだ同名構造体の取り違えを防ぐ)。問題はその公称性を文字列化で実現していることにある。

なぜ文字列が問題なのか

三つの理由がある。

第一に、網羅性検査が効かない。実装言語の代数的データ型に対する分岐なら、構成子を足したときに未処理の枝がコンパイルエラーになる。文字列に潰した時点でその保護は消え、新しいプリミティブや構成子を足しても静かに素通りする。

第二に、型引数を持つ構成子を足した瞬間に破綻する。ジェネリクスや高階の型構成子を導入すれば、名前の文字列一致では表せない関係(変性、束縛変数の名前替え)が必要になる。文字列連結は構造を保存しない符号化なので、そこで作り直しになる。

第三に、文字列化は本来ハッシュと表示のための機能である。判定に流用したことで、表示名を変えると型の意味が変わるという結合が生まれている。表示の都合で名前を整えたら代入可能性が変わる、という事故の可能性が構造として残る。

直す方向

修正は素直で、最終アームを構成子ごとの構造再帰に置き換えることである。公称性を捨てる必要はない — 構造体は名前で比較し、List<T>は構成子が一致することを確かめてから要素型を再帰する、という形に書き直せば、公称の意味論は保ったまま網羅性が実装言語の型に戻る。

コンテナについては、上に書いたとおりこの形に直っている。List同士・Map同士のアームが構成子で照合してから要素型・キー型・値型に再帰する、という書き方になった。残っているのは最終アームの落ち穂拾いで、そこに落ちる組を構成子ごとに列挙し切れば、matchの網羅性が判定全体に戻る。

これは「区別を型に昇格させる」という、この型システムの負債群に共通する解の形の一例である。文字列は最も情報の少ない表現であり、そこへ潰した時点で実装言語の型システムが持っていた保護をすべて手放している。

根拠の確度

最終アームにtype_name()の文字列比較が残っていること、コンテナが構造再帰になっていることは2026-08-16時点のソース(carina-core/src/schema/mod.rsis_assignable_to_resolved)で確認済み。#3209がopenであることはGitHub APIで確認済み。

値の検証側の文字列経由の分岐は再確認していない。 評価メモ §3.3 (m) の記述を引き継いだままで、コンテナと同時に直っている可能性は追っていない。

#型システム #設計負債 #部分型