公称軸ごとの幅部分型付けが再利用と混同防止を両立する

確認済み 出典: explorations/2026-06-10-carina-type-system-type-theory/type-system-analysis.md §5 2026-06-10 作成

列挙やカスタム文字列型にはTypeIdentity { provider, segments, kind }という公称的な識別が付く(providerは省略可能)。注目すべきはその等価性・代入可能性の定義で、単純な全フィールド一致ではない。

• 等価性(same_type)は「両者が値を持っている軸だけ」を比較する。 provider無指定の型は、provider軸について「より広い型」として振る舞う。
• 代入可能性(assignable_to)は方向付きで、受け側が特定している軸は送り側も一致しなければならないが、受け側が特定していない軸は問わない。

これは公称型に幅部分型付け(width subtyping)を一軸ずつ載せた構造である。aws.iam.Role.Arn <: Arn(provider非依存のArn)のような包摂が成り立ち、provider無指定のbare identityは実質的にそのkindの上限(top)として機能する。

二つの要求を一つの機構で

一方でaws.Regionとgcp.Regionのように両軸が特定されていれば別型であり、provider越しの混同は型として弾かれる。

「公称的な核(kind)+ 省略可能な公称軸による包摂」というこの設計は、完全公称型と完全構造型の中間にある。完全公称型ならaws.iam.Role.Arnと汎用Arnは無関係な別型になり、共通のArn型を書けない。完全構造型ならどちらも単なる文字列になり、aws.Regionとgcp.Regionの混同を弾けない。軸ごとの部分型付けは、マルチプロバイダ環境での型再利用とプロバイダ間の混同防止を一つの機構で両立させている。

表記と正規形

DSL上の列挙値の表記(aws.s3.Bucket.VersioningStatus.enabledのような名前空間付き識別子)は、この公称識別への構文的な参照であり、静的段階で「identity + プロバイダAPI値」という正規形へ解決される。比較・直列化は解決済みの形でのみ行われる。

この公称軸の包摂は、値が未解決の参照に対する宣言型検査でも使われる。値なしでもrole_arn = role.role_nameのような型違いを弾けるのは、この方向付きの代入可能性判定があるからである。

#型システム #部分型 #公称型