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

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

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

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

規則そのものはおおむね正しい。穴は規則ではなく継ぎ目 — 段階の継ぎ目、二つの型言語の継ぎ目、プラグイン境界、同じ関係の複数の実装 — に集まっている。長く一番大きかった漸進的型付けの動的な半分(委ねた検査の行き先)は2026-10に入り(判定できない部分型は、拒否も受理もせず実行時の検査に回す(hybrid type checking))、同じ月に代入可能性の判定器の重複もほぼ一本化された。残る穴は、LSPの再実装、ユーザーが書ける型の狭さ、⊤・⊥の不在あたりに寄ってきている。

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

近い言語と並べると、検査の様式は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が500本を超えて(2026-11-07時点で519本)あり、「コンパイルできてはいけないコード」を否定的な型付けの試験として固定している。WASM境界では網羅的な分解代入で、プロトコルに増えたフィールドを黙って捨てることをコンパイルエラーにしている。(typestateで壊れた状態を書けなくする / 循環スキーマは名前付きμ型で明示展開する)
8. 決定不能な問いを正直に扱っている。正規表現の包含は判定せず、パターンが違えば非互換とする。完全性を捨てて健全性を取る、と明示的に選んでいる。

弱み — 穴の場所ごとに

段階の継ぎ目: 動的な半分は入り、逆向きの穴が残る

漸進的型付けは、型の分からない値が静的な型の世界に入る境界で実行時検査(キャスト)を挟み、違反したら出所を指して失敗させる(blame)ことで健全性を保つ。Carinaは静的な半分 — Rule 10で素のStringを受け入れて「値の検査に委ねる」、Deferredを素通しする — に加えて、委ねた先の検査も持つ。参照が解決した時点で受け手の篩を検査し、違反はどの参照から来た値かを示して報告する(判定できない部分型は、拒否も受理もせず実行時の検査に回す)。

値の検証は、参照を解決した後にも走る。planで分かった値はplanで、applyで初めて分かった値はプロバイダに送る直前に検査し、送信用の値は検査を通らないと作れない。モジュール引数のvalidationも、参照の値が分かるまで評価を待つ(carina#3825、carina#3846。これでcarina#3448・carina#3805・carina#3767がclose)。

残る穴は逆向きのものである。パース時の置換で参照がリテラルに化けると、宣言型の検査が飛ぶ(carina#3450、open)。

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

関係の継ぎ目: 代入可能性はほぼ一つの定義にまとまった

2026-10-15のcarina#3856で、モジュール引数・export・属性・ユーザ関数の型検査が、具体値の検査器check_type_expr_value一つと、参照の判定(BindingIndex + lift_type_expr + TypeInSchema)一つにまとまった。モジュール引数を転送するときだけ使われていた別の判定器type_expr_compatibleは、送り側の合併を「いずれかのメンバが合えば可」で通す不健全な規則ごと消えた。issueのcarina#3211はopenのまま残っている。

残っているのは次のとおり。

• LSPは属性の参照の型検査を自前で持っていて、属性の値が参照そのもののときに判定する(check_resource_ref_type_mismatch)。リストや構造体の中の参照で型違いを見逃すというcarina#3043はopenで、今回は再現を確かめていない
• is_assignable_toの分岐は網羅的になったが、構成子が違う組の判定にまだ表示名の文字列比較が残る(carina#3209、open)
• 性質試験は反射律と推移律まで。反対称律が無く、宇宙が手書きの有限リストに留まる(carina#3208、open)。変性も書かれていない(carina#3210、open)

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

検査器の中: 「分からないと通す」は塞がった

• 注釈に対する値検査はcheck_type_expr_valueに置き換わり、明示の腕に当たらない組み合わせは不一致を返す。以前のvalidate_type_expr_valueは最後の腕が_ => None(問題なし)で、明示の腕が無い組み合わせを素通りさせていた
• 篩のパターンは、スキーマを受け入れる時点でコンパイルするようになった(carina#4171、2026-11-01)。受け入れ前のDraftではパターンは文字列、受け入れ後のCompiledではCompiledPatternで、値の検査中にはコンパイルしない。以前は検査のたびにRegex::newし、失敗すると検査全体を飛ばしていた

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

プロバイダのスキーマ型は篩・公称軸・合併・再帰を持つ。ユーザーが書く注釈の型はそれより狭く、しかも一部はスキーマ型へ写せない。写像lift_type_expr(carina-core/src/validation/mod.rs)のNoneは「検査しない」として扱われるが、Noneを返すのは今はDottedUnresolved(スキーマでまだ解決していない点付きの名前)だけである。リテラル型は文字列リテラルの集合に、Refはリソースハンドルに写る。

• リテラル型とその合併('dev' | 'prod')は、文字列リテラルの集合として検査される(carina#2648、#3856でclose)
• リソース型の注釈(vpc: aws.ec2.Vpc)はハンドルだけを意味するようになり、モジュールの出力としてハンドルを渡せる。exportにリソース型は書けない(carina#3803、PR #4198で2026-11-01にclose)
• letの注釈、型エイリアス、名前付きの構造体型(carina#2142)、ジェネリクス、関数型が無い。nullと??は言語にあるのに、null許容の型が無い
• ⊤と⊥が無く、「何でも受ける」は広い合併や識別なしのStringで代用している(carina#3220、open)
• 組み込み関数に型のシグネチャは無い(signatureは説明用の文字列)。戻り値の分類(BuiltinResultTyping)は細かくなり、引数の型をそのまま返すArgument(i)、秘密の文字列、文字列の組み立て(ConstructedString)、要素が文字列だと分かるリストなどを区別する。join(...)のように文字列を組み立てる関数の結果は、補間と同じく、値が分かった時点で受け手の篩で検査される。要素型を持たないList/Mapと、引数次第のAny(lookup・map・min・max)はまだ粗く、そこでは関数呼び出しが事実上の?である
• ユーザ関数の引数・戻り値も同じ関係で検査されるようになり、リストの要素やInt | Stringのような混合の合併も検査される(carina#2810・carina#2812はopenのまま)

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

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

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

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

• タグなし合併の判別はヒューリスティック。タグなし合併の判別はヒューリスティックに頼るしかない
• 属性の出所(ユーザー/プロバイダ/サーバ既定)が型に乗っていない。属性の出所は型に昇格させるべきモダリティである
• 「分からない」の語彙が層をまたいで複数ある — Value::Deferred/Unknown、参照型のRefType::Unchecked、lift_type_exprのNone、静的な型が決まらないことを表すStaticType::Unchecked(以前のTypeExpr::Unknown)。今の形は文書化された(carina#3212、PR #4095でclose)が、どこで静的な保証が切れているかをエディタ上で見せる仕組みは確かめていない。「未確定」を表す表現が四つあるのは漸進的型付けの境界が引けていない徴候である

改善すべき点 — 効く順に

1. 委ねた検査を解決後に必ず走らせる。漸進的型付けのキャスト挿入に当たる。これは入った(carina#3825、carina#3846)。実装は、解決後の値を別の型にするのではなく、プロバイダに送る値をProviderReady<T>にし、それを作る関数だけが検査を行う形になった。呼び忘れが型で書けない点は同じである。(信頼境界を越えるデータは境界で再検証する)
2. 代入可能性を一つの関係にする。大部分は入った(#3856)。type_expr_compatibleは消え、値検査の_ => Noneも不一致に変わった。残りは、LSPの属性参照の検査を同じ入口に寄せること(#3043)と、構成子が違う組の表示名比較を構成子の腕に置き換えること(#3209)である。
3. パターンを構築時にコンパイルするnewtypeにする。これは入った(#4171)。パターンの表現をDraft/Compiledで分け、受け入れ後はCompiledPatternしか持てない。
4. lift_type_exprを全域にし、リソースハンドル型を足す。大部分は入った。StringLiteralは文字列リテラルの集合に、Refはリソースハンドルに写り(#3856、#4198)、Noneを返すのはDottedUnresolvedだけになった。残りは、これも写すかエラーにすることである。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は問題なし(#3856で直った)。正規表現がコンパイルできなければ検査しない(#4171で直った)。プラグイン境界で検証関数が無いと何もしない検証器になる(#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は、この計画のうち一番効く1段を、送信直前の型として先に入れたものに当たる。

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

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

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