Carinaの型システムは値を検査する篩型の体系で、穴は段階と境界の継ぎ目にある

解釈 出典: carina-rs/carina main 0fb456c1(2026-09-30)のソースとissue、同日のレポート「Carinaの型システムを型理論から読む」(main d0445d0b)、既存ノート群 2026-09-30 作成

Carinaの型システムについて個別のノートがかなり溜まったので、型理論の地図の上でどこにいるのか、何が強くて何が弱いのかを一枚にまとめる。細部は各ノートにあり、ここは索引を兼ねた見取り図である。

一言でいえば、プロバイダのスキーマが供給する型(篩型+公称軸)に、評価し切った値を照らして所属を判定する検査系である。ユーザーが型を定義する言語ではなく、型の大半はcodegenが作ったスキーマから来る。値が無いところだけ、宣言型どうしの代入可能性で補う。

規則そのものはおおむね正しい。穴は規則ではなく継ぎ目 — 段階の継ぎ目、二つの型言語の継ぎ目、プラグイン境界、同じ関係の複数の実装 — に集まっている。とくに大きいのは、漸進的型付けの静的な半分だけがあって、動的な半分が無いことである。

ポジション — 軸ごとに見る

近い言語と並べると、検査の様式はPklやNickelの契約、型の語彙はCUE寄り、全域性はDhall・CUE・HCLの系譜という混合になる。Dhallのような構文的な型体系(判断規則と推論、多相)は持たず、Terraformのようにstring+検証述語に落とすのでもない。他と一番違うのは、「このARNはIAMロールのARNか」という出所を公称軸で型に持たせていることである。PulumiのTypeScript型はstringとstringを区別しない。→ 「専用言語か」と「全域か」は独立した二軸である / プロトコルで型が潰れるのは共通で、差はschemaの型語彙にある

強さの源は全域性にある

値で検査できるのは、静的段階が必ず停止し、結果がソースとstateだけで決まるからである。そのおかげで篩の述語に任意の計算を置いても決定可能性の問題が起きない。項レベルで含意を証明する篩型システムが、述語をSMTで決定可能な論理に絞る(Liquid Haskellなど)のと対照的で、Carinaは証明の代わりに実行する。

逆にいえば、この様式は値が手に入る場所でしか働かない。弱みのほとんどはここから出る。→ 型は値の分類器である(意味論的型付け) / 値ベースの全数検査は停止性の配当である / カスタム型は独立の構成子ではなく篩型である

型は三つの層にある

「Carinaの型」と言うとき、性格の違う三つの層がある。

• DSL層(TypeExpr) — ユーザーが書く注釈。arguments・attributes・exports・fnで使える。letには書けない
• スキーマ層(AttributeType) — プロバイダがWASM越しに渡すスキーマ。部分型関係is_assignable_toと値検査器を持つ
• 実装層 — 処理系自身の不変条件をRustのnewtype/typestateで封じる層

弱点の多くは層と層のつなぎ目にある。

部分型の規則

is_assignable_toの手書きの分岐を判断規則の形に直すと、おおむね次のとおりになる。A <: Bは「A型の値をB型の受け手に渡してよい」。

Rule 10があるので推移律が崩れる。pattern=alpha → String → pattern=digitsは一段ずつなら通るが、直接は拒否される。試験(carina-core/src/schema/tests.rs)は有限個の型を総当たりして反射律と推移律を確かめており、推移律の試験は「Rule 10を中継したときだけ崩れてよい」と例外を明示し、その例外が少なくとも1件あることまで確かめている。非推移性を意図として宣言しているのは誠実である。

強み

1. 段階が明確。型検査はどの効果よりも先に終わり、planが検査と実行の境界そのものになっている。(IaC言語は二段階の言語である)
2. 篩の述語に制限が無い。上の全域性の配当。
3. 出所を運ぶ公称軸。共通型の再利用(aws.iam.Role.Arn <: aws.Arn)とプロバイダ間の混同防止(aws.Region≠gcp.Region)を一つの機構で両立する。「形は合っているが別物のIDを渡す」事故を型で止められる。#3218以降は方向付きのassignable_toと対称なsame_typeが分かれている。(公称軸ごとの幅部分型付けが再利用と混同防止を両立する)
4. 広い型で宣言して篩を消す抜け道を塞いでいる。モジュールの属性をStringと宣言しても、転送元の篩は証拠(evidence)として保持され、受け手では宣言と証拠の両方が通ることを要求する(carina#3798)。
5. Unknownの扱いが一貫して保守的。検査は素通し、等価性はSQLのNULLと同じく自分自身とも不成立で、「偽の型エラーは出さず、怪しい差分は出す」側に揃っている。(検査は素通し、等価性は不成立 — Unknownの一貫した保守性)
6. 差分が型主導。順序付き/なしのリスト、列挙の正規形、合併のメンバ比較が、すべて型に導かれる。(等価判定は正規形へ簡約してから型ごとに行う)
7. 実装層で壊れた状態を書けなくしている。Refを剥がしたShapeビュー、Concrete/Deferredの分離、正規化済みでないリソースを渡せないNormalizedResourceなど。compile_failのdoctestが27本あり、「コンパイルできてはいけないコード」を否定的な型付けの試験として固定している。WASM境界では網羅的な分解代入で、プロトコルに増えたフィールドを黙って捨てることをコンパイルエラーにしている。(typestateで壊れた状態を書けなくする / 循環スキーマは名前付きμ型で明示展開する)
8. 決定不能な問いを正直に扱っている。正規表現の包含は判定せず、パターンが違えば非互換とする。完全性を捨てて健全性を取る、と明示的に選んでいる。

弱み — 穴の場所ごとに

段階の継ぎ目: 漸進的型付けの動的な半分が無い

漸進的型付けは、型の分からない値が静的な型の世界に入る境界で実行時検査(キャスト)を挟み、違反したら出所を指して失敗させる(blame)ことで健全性を保つ。Carinaには静的な半分 — Rule 10で素のStringを受け入れて「値の検査に委ねる」、Deferredを素通しする — はあるが、委ねた先の検査が参照の解決後に走らない。

値の検証は参照を解決する前に1回だけ走る。上流stateの値はplan時に、リソースの出力はapply時に代入されるが、どちらの代入点にも検証経路が無い(carina#3448、open)。2026-09-29に、同じ根を持つcarina#3767がこの重複としてcloseされた。同じ根から別の症状も出ている。

• モジュール引数のvalidation { condition = ... }は展開時に評価されるので、参照を渡すとDeferredのまま評価されてエラーになる(carina#3805、open)
• 識別の無い篩に素のStringを渡すのはRule 10で静的に通し、値の検査に回す。その値が参照経由なら、値の検査も走らない。「委ねた」はずの検査がどこでも行われない
• 逆向きに、パース時の置換で参照がリテラルに化けると、宣言型の検査が飛ぶ(carina#3450、open)

→ 再配置後に検証がないのは型検査済みIRの不変条件の破壊である / 「全数検査」は検証ステップの時点で確定している値に限られる / 未知値の周りは無検査ではない

関係の継ぎ目: 代入可能性が一つの定義になっていない

• モジュール引数を転送するときだけ別の判定器type_expr_compatibleが使われる。これは文字列っぽい型をidentity無視で互いに通し、送り側の合併を「いずれかのメンバが合えば可」で通す(carina-core/src/module_resolver/typecheck.rs)。Union-Lは∀でなければならないので、これは不健全である(carina#3211、open)
• LSPは参照の検査を再実装しており、ネストした型違いを見逃す(carina#3043、open)
• 本体のis_assignable_toも、List/Map/Structは構成子で比べるようになったが、最後の腕はまだ表示名の文字列比較である(carina#3209、open)
• 性質試験は反射律と推移律まで。反対称律が無く、宇宙が手書きの有限リストに留まる(carina#3208、open)。変性も書かれていない(carina#3210、open)

→ 検査器が二系統あるのは設計負債である / 型名の文字列比較で代入可能性を決めるのは構造を捨てている / 部分型関係が公理化されていないと性質の破れを検出できない / 変性は書かれていないだけで、既に決まっている

検査器の中: 分からないと通す

• 注釈に対する値検査validate_type_expr_valueは、既知の組み合わせだけエラーを返し、最後の腕が_ => None(問題なし)である(carina-core/src/validation/mod.rs)。明示の腕が無い組み合わせは素通りする
• 篩のパターンは検査のたびにRegex::newし、コンパイルに失敗すると検査全体を飛ばす(if let Ok(re) = ...、carina-core/src/schema/mod.rs)。不正なパターンを持つ型は、どんな文字列も通す

型言語の継ぎ目: ユーザーが書ける型が貧しい

プロバイダのスキーマ型は篩・公称軸・合併・再帰を持つ。ユーザーが書く注釈の型はそれより狭く、しかも一部はスキーマ型へ写せない。写像lift_type_expr(carina-core/src/validation/mod.rs)はRef・StringLiteral・DottedUnresolved・Unknownに対してNoneを返し、Noneは「検査しない」として扱われる。

• リテラル型とその合併('dev' | 'prod')はどこへでも通る(carina#2648、open)
• リソース型の注釈(vpc: aws.ec2.Vpc)は未検査で、ハンドルとしての意味も定まっていない。リソースそのものをモジュール境界越しに渡すこともできない(carina#3803、open)
• letの注釈、型エイリアス、名前付きの構造体型(carina#2142)、ジェネリクス、関数型が無い。nullと??は言語にあるのに、null許容の型が無い
• ⊤と⊥が無く、「何でも受ける」は広い合併や識別なしのStringで代用している(carina#3220、open)
• 組み込み関数に型のシグネチャが無い。戻り値はString/Int/List/Map/Any/Secretの粗い6種類で、ListやMapは要素型を持たない。関数引数の中の参照は存在確認しかされないので、join(...)の結果をARN型の属性に入れてもvalidateは通る。関数呼び出しは型システムにとって事実上の?である
• ユーザ関数の引数・戻り値の検査は、リスト・マップ・構造体で浅く(carina#2810)、合併は文字列形のメンバしか扱えない(carina#2812)

プロバイダ作者はユーザーより強い型を書ける、という非対称になっている。モジュールを書く人は篩をスキーマ型で表せず、validationブロックという実行時述語に逃がすしかない — そしてそれが上の段階の穴に落ちる。→ 型注釈の言語とスキーマ型は別の言語である

境界の継ぎ目: WASMの向こうで型が薄くなる

スキーマはWITの型ではなくJSON文字列で渡され、検証関数は越えられないのでvalidate-custom-typeのコールバックに置き換わる。壊れたJSONをunwrap_or_default()で空にしてしまう箇所が残っている(carina#3811、open)。プロトコル側のスキーマはまだrequired: boolとread_only: boolの組で、不正な組み合わせを境界で弾いている。境界で解析して型に上げる正しい形ではあるが、ワイヤ形式でも3値にすれば境界のエラー経路自体が要らなくなる。→ プラグイン境界の型消去は事故クラスを予測する

表現の継ぎ目: 残っている理論的負債

• タグなし合併の判別はヒューリスティック。(タグなし合併の判別はヒューリスティックに頼るしかない)
• 属性の出所(ユーザー/プロバイダ/サーバ既定)が型に乗っていない。(属性の出所は型に昇格させるべきモダリティである)
• 「分からない」の語彙が層をまたいで複数ある — Value::Deferred/Unknown、参照型のRefType::Unchecked、lift_type_exprのNone、推論失敗のTypeExpr::Unknown。どこで静的な保証が切れているかを利用者に見せる手段が無い(carina#3212、open)。(「未確定」を表す表現が四つあるのは漸進的型付けの境界が引けていない徴候である)

改善すべき点 — 効く順に

1. 委ねた検査を解決後に必ず走らせる。漸進的型付けのキャスト挿入に当たる。Rule 10やUncheckedで静的検査を通った値に「後でこの型で検査する」義務を残し、参照が解決した時点で受け手の篩を検査して、失敗したら送り手の位置を指す。解決後の値をDeferredを含まない別の型(ResolvedValue)にし、そこへの変換関数だけが検査を行う形にすれば、呼び忘れが型で書けなくなる。#3448・#3805・#3767はこれで一箇所で閉じる。applyで動いているassert_fully_resolvedという実行時の表明も、この型に置き換えられる。(信頼境界を越えるデータは境界で再検証する)
2. 代入可能性を一つの関係にする。type_expr_compatibleを消して、展開前もlift_type_exprで持ち上げてからis_assignable_toで判定する。LSPも同じ入口を呼ぶ。最後の文字列比較の腕とvalidate_type_expr_valueの_ => Noneを網羅的な構成子の腕に置き換えれば、構成子を足したときにコンパイラが判断を迫る。
3. パターンを構築時にコンパイルするnewtypeにする。pattern: Option<String>をPattern型にし、不正なパターンはスキーマのデコード時に型付きのエラーにする。検査が黙って消える状態が書けなくなり、毎回の再コンパイルも消える。
4. lift_type_exprを全域にし、リソースハンドル型を足す。None=検査しない、をやめる。StringLiteralは1値の列挙として、Refは「そのリソースの属性を持つレコード」として居場所を作り、IDだけを渡すならaws.ec2.Vpc.Idで書く、と役割を分ける(#3803)。写せないものはエラーにする。carina#2360でOption<TypeExpr>を潰したのと同じ直しを、写像の側にも当てることになる。
5. 「未検査」を明示のDyn型に集め、書いた場所が分かる抜け道を用意する。⊤・⊥(#3220)と合わせて格子の端を定義で決め、LSPのホバーで?として見せる。正しいのに弾かれる偽陽性にはunchecked(x)のような明示のキャストを入れ(carina#3808)、1.の検査の対象にする。
6. 組み込み関数に型のシグネチャを与える。map・concat・lookup程度ならランク1の単純な型スキームで足り、Hindley-Milnerまでは要らない。関数引数にも受け手の型が届くようになる。
7. 性質試験を広げる。反対称律を足し、宇宙をproptestの生成型にする(#3208)。2.の後なら新しい構成子も自動で網羅される。
8. 出所をモダリティにする。差分の個別補正が型主導の規則になる。効果は大きいが、1〜4より後でよい。

他に気づいたこと

素のStringは二つ目の?になっている

Rule 10による非推移性はバグではなく、素のStringが漸進的型付けの?の役を兼ねていることの表れと読める。漸進的型付けで型の等しさの代わりに使う整合性(consistency)関係は、反射的・対称的だが推移的でない(Siek & Taha 2006)。ただ、それなら「Stringは?である」と明示したほうが意味論が読みやすい。Dynと明示のキャストがあれば、素のStringをただの基本型に戻せる。

same_typeも推移的でない

軸が空なら何とでも一致するので、Arnはaws.Arnともgcp.Arnとも「同じ」だが、後の二つは同じでない。関数名は同値関係を連想させるが、実態は整合性関係である。consistent_withのような名前にするだけでも誤用を防げる。→ 同値関係を方向付き判定に流用すると抽象から具体への代入が漏れる

「無い」が「許可」として読まれるパターンが繰り返されている

注釈のOption<TypeExpr>がNoneなら検査を飛ばす(#2360、直った)。identity: Noneが三つの意味を兼ねる。lift_type_exprのNoneは未検査。値検査の_ => Noneは問題なし。正規表現がコンパイルできなければ検査しない。プラグイン境界で検証関数が無いと何もしない検証器になる(#2354、直った)。壊れたJSONは既定値になる(#3811)。どれも「分からない」をNoneや既定値で表し、消費側が一番楽な既定 — 通す — を選んでいる。個別には直っていくが、不在が許可に化けない型の形(不在をResultのエラーにする、Uncheckedを明示の変種にして網羅マッチを強いる)を一般原則にしたほうがよい。→ 黙って捨てるのは、落とすことより悪い

ユーザ関数は型の上では関数ではない

パース時に展開され、注釈は呼び出しごとに実引数の値で確かめる契約として働く。関数型が無いのはそのためで、高階関数を入れるなら、まず関数型を型の言語に入れる必要がある。そこで初めて変性(引数位置の反変)と「関数値がgraph形状に届かない」制約の置き場所が問題になる。→ 高階関数の境界条件は「関数値がgraph形状決定位置に到達しない」ことである / 変性は選ぶものではなく、位置が決めるものである

deferred_populateは時刻の型の芽である

作成後に値が届く属性を、waitブロックが無ければ連鎖参照させないという検査は、型理論でいえば「後で」様相(▷)に近い。今は「そのバインディングに何らかのwaitがあればよい」という粗い判定で、どのwaitがどの属性を待つのかまで対応づければ、時刻についても型で保証できる。

Secretは型ではなく値の包みである

SecretはDeferredValueの一種で、注釈の無いexportではStringと推論される(carina-core/src/validation/inference.rs)。秘密であることが型に現れないので、境界を越えた先で秘密性を静的に追えない。情報フロー型の考え方でSecret<T>を型にすれば、漏洩経路を型検査で探せる。実害があるかは確かめていない。

型の実効的な強さはcodegenの注釈の細かさで決まる

vpc.vpc_idをSubnetIdの受け手に入れて弾けるかは、プロバイダのスキーマがその属性にaws.ec2.Vpc.Idという識別を付けているかだけで決まる。本体をいくら健全にしても、スキーマ側の注釈が粗ければ保証も粗い。識別が付いている属性の割合をプロバイダごとに測って回帰を監視すれば、型システムの強さを数字で追える。→ プロトコルで型が潰れるのは共通で、差はschemaの型語彙にある

Effectは型の上では追跡されていない

Effectは命令の平たい列で、依存は別のグラフが持つ。DSLの型はどのリソースがどの効果を起こすかを表さない。IaCとしてはこれで足りるが、型理論の文脈で「エフェクトシステム」と呼ぶと誤解を招く。→ 効果の具体化 — planは効果の自由モノイドである

未確定が型ではなく値の側にある

漸進的型付けの標準形は?という型を一つ置くが、Carinaの未確定はValue::Deferredである。IaCの未確定は段階を追って必ず消えるので、解決段階をtypestateにする設計(Raw→Inferred→ResolvedRefs→Applied)が書かれているが、コードにはまだ無い。改善点1のResolvedValueは、この計画のうち一番効く1段を先に切り出したものに当たる。

最近のissueの多くは規則の誤りではなく配線の欠落である

2026-09末に開いている型関連のissueは、「規則が間違っている」ものより「検査はあるが、その経路には呼ばれていない」もの(#3448、#3805、#3450、#3043、#3803)が多い。規則を正しく書くことより、すべての経路がその規則を通ることを型で強制することが今のボトルネックである。→ 型システムが難しいのは、健全性が「すべての経路で」を要求するからだ

#型システム #型理論 #carina