変性は書かれていないだけで、既に決まっている
List<T>やMap<K,V>のような型構成子を持つ型システムには、必ず変性(variance)の問いが付いてくる。T <: UのときList<T> <: List<U>は成り立つか(共変)、逆向きになるか(反変)、どちらでもないか(不変)である(この三択がなぜ三択で、何が答えを決めるのかは変性は選ぶものではなく、位置が決めるものであるに書いた)。
Carinaはこの問いに答えを持っている。ただしその答えはコードのどこにも書かれておらず、代入可能性判定の再帰の向きから読み取るしかない。「変性が未定義」なのではなく、未文書のまま確定しているというのが正確な状態である。
しかも確定したのは、変性を決めるための検討によってではない。別の目的の修正が判定の形を変えた結果、副作用として決まった。決定と、決定するはずだった議論が、別の場所で進んでいる。
実装が選んでいる答え
代入可能性判定のコンテナのアームは、要素型を送り側から受け側の向きにそのまま再帰する。
// List: 要素型を source → sink の向きで再帰
(List { element_type: source_element, .. },
List { element_type: sink_element, .. })
=> source_element.is_assignable_to(sink_element)
// Map: キーも値も source → sink の向きで再帰
(Map { key: source_key, value: source_value },
Map { key: sink_key, value: sink_value })
=> source_key.is_assignable_to(sink_key)
&& source_value.is_assignable_to(sink_value)外側の向きと内側の向きが一致している。つまりリストは要素について共変、マップはキーについても値についても共変である。反変の位置は型システム全体に一つも無い。
注意すべきは、Mapのキーが共変であることが値の共変以上に強い主張である点である。キーはAttributeTypeをまるごと取れるので、篩型で絞ったキー型(ARNの形をした文字列など)を持つマップが書ける。「キーがARNのマップ」を「キーが任意文字列のマップ」として渡せる、という包摂がここで成立している。
構造再帰になって初めて変性が問題になった
この読み取りが意味を持つようになったのは最近である。以前はList<T>の代入可能性が型名の文字列比較で、型名を文字列連結して比較していた。文字列一致は要素型の包摂を一切見ないので、変性以前に共変も不変も表現されていなかった — 実質的に「名前が同じときだけ通す」という不変に近い挙動である。
2026-08-15の修正でコンテナが構造再帰になり(d15d8ce8、スキーマを跨いだRef名の偽の受理を塞ぐのが主目的)、そこで初めて要素型の包摂が判定に効くようになった。共変はその修正の副産物として入っている。 コミットメッセージが明示的に固定した差分は「識別付きの要素が匿名の受け側へ広がる」ことと「要素の区間包含が効くようになる」ことの二点で、変性そのものには触れていない。
ここが本ノートの要点である。変性を決めるための議論は3か月前からissueとして存在していた(carina#3210、2026-05-23)。にもかかわらず、実際に変性を確定させた変更はそのissueを参照せず、別の目的の修正のついでに起きた。決定が議論の外側で行われたというのが正確な構図で、「まだ決めていない」でも「決めて書いていない」でもない。
負債の順序としては筋が通っている — 文字列比較という粗い近似を構造再帰に直したのは正しい方向で、その結果として変性という次の問いが初めて意味を持つようになった。文字列を比較している間は、変性を議論しても答えようがなかった。
なお文字列比較を潰すためのissue carina#3209はまだopenである。コンテナは構造再帰になったが、判定の最終アームにはself.attr.type_name() == sink.attr.type_name()が残っており、文字列比較のノートが指摘する網羅性の問題はそこで生きている。部分的に直った、というのが正確な状態である。
共変が今のところ安全な理由と、その境界
共変な可変コンテナは古典的な不健全性の源である。Javaの配列共変が教科書例で、Object[] a = new String[1]; a[0] = 1; が型検査を通って実行時に落ちる。共変が安全なのは読み出し専用のときだけで、書き戻しが入ると壊れる。
IaCの値は基本的には読み出し専用なので、現状この罠は踏んでいない。プロバイダのスキーマから来た値を読み、比較し、直列化するのが主な流れである。
ただし「基本的に」が効いている。issue carina#3210はplan/applyの経路について、「読み出し方向が支配的だが、純粋な読み出し専用ではない」と書いている — stateからコンテナの値を読んでプロバイダのビルダに渡す流れが主で、state v3経由の書き戻しが時折ある、という整理である。つまり不健全性の前提条件は「存在しない」のではなく「まだ点検されていない」。
そして問題の核心はそこにある。「読み出し専用だから共変で安全」という条件が、どこにも書かれていないだけでなく、成り立っているかを確かめてもいない。これは言語の不変条件ではなく、現在の使われ方についての未検証の観察である。同issueが最初の作業として挙げているのも、リスト・マップの要素を読む位置と書き戻す位置を全て洗い出し、各位置を共変/反変/不変に分類することである。書き戻しを伴う機能 — 属性の部分更新、リストへの要素追加を型の上で表す構文、可変な参照 — を一つ入れた時点で、共変は不健全になる。そのとき壊れるのは新機能ではなく、既存の代入可能性判定である。
これは部分型関係が公理化されていないのと同じ形をしている。規則の集合が満たすべき性質が、人間の注意にだけ載っていて機械には載っていない。反射性・推移性・反対称性が試験に書かれていないのと同様、「共変が許されるのは読み出し専用だから」という前提も、破ったときに誰も教えてくれない場所にある。
直す方向
変性を型の側に書くことである。List<T>のTが共変であることを型構成子の定義に注記し、その注記に沿って再帰の向きを決めるようにすれば、新しい構成子を足すときに変性を決めることが強制される。今は再帰を素直に書けば共変になってしまうので、既定値が暗黙に選ばれる構造になっている。
issue #3210はこの方向をほぼそのまま提案している — 位置ごとに変性を分類し、構成子ごとの既定を文書に固定し、選んだ変性に沿った性質試験を置く。不健全な経路が見つかった場合の手当てとしてその経路だけ不変にする(安い)か、可変コンテナを別の構成子(MutList<T> / MutMap<K,V>)として分ける(重い)かの二案まで書かれている。後者はtypestateで壊れた状態を書けなくするの適用そのもので、「今は書き戻しが無いから大丈夫」を「書き戻せるコンテナは別の型だから大丈夫」に変えることである。
issueは2026-05-23に立って今もopenであり、着手されていない。 変性が未文書のままなのは見落としではなく、優先度が付かないまま3か月弱が経っているという状態である。実害が出ていないので急がない、という判断としては筋が通るが、その「実害が出ていない」の根拠自体が未点検であることは上に書いたとおりである。
根拠の確度
再帰の向きとMapのキーが共変であることは2026-08-16時点のソース(carina-core/src/schema/mod.rsのis_assignable_to_resolved)で確認済み。構造再帰になった日付とその主目的はコミットd15d8ce8(2026-08-15)による。issue #3210 / #3209がopenであること、および#3210の本文(「読み出し方向が支配的だが純粋な読み出し専用ではない」、位置ごとの分類、MutList案)はGitHub APIで確認済み。
「変性が選択として議論された形跡がない」は、コードとコミットの範囲に限った話である。 carina-core/src/とnotes/のどちらにもvariance/covariant/contravariantの語が現れないこと、d15d8ce8のコミットメッセージが変性に触れていないことは確認したが、issue #3210の存在は「議論が無い」わけではないことを示している。正確には「変性を決める議論はissueとして立っているが、コードに反映されておらず、コンテナを構造再帰にした変更もその議論を参照していない」ということになる。
Mapのキーが共変であることの実害は未確認。AttributeTypeをキーに取れる以上、篩型で絞ったキーを持つマップは表現可能だが、それがプロバイダのスキーマに実際に現れるか、共変が問題を起こす組み合わせが存在するかは調べていない。
「書き戻しが入れば不健全になる」はJava配列共変からの類推である。#3210が言う「state v3経由の書き戻し」が具体的にどの経路で、それが部分型付けされた位置に当たるかどうかは、issue本文の記述をそのまま引いただけで自分では追っていない。