notes mizzy.org

「未確定」を表す表現が四つあるのは漸進的型付けの境界が引けていない徴候である

確認済み 出典: audits/2026-05-23-type-system-evaluation.md §3.2 (h), §6 / specs/2026-05-23-gradual-typing-design.md / carina#3212 作成/ 更新

Carinaの型システムには「まだ確定していない」を表す表現が四つ独立に存在する

四つはそれぞれ違う種類の未確定を表しており、どれも必要な区別ではある。しかし四つあること自体が、この型システムの漸進性(gradual typing)の境界がどこにあるかを見えにくくしている

Carinaの現状 — 四つが層をまたいで散らばる 値の側 deferredな値 Unknown値 型の側 識別なしのカスタム型 注釈側の未知型 解消の時点も担い手もそれぞれ違う。 「今どういう意味で未確定か」は四つを特定しないと答えられない。 標準的な漸進的型付け Dynamic (?) 未確定は一つの型に集約され、 既知型との関係は整合性という 単一の関係で与えられる。
散らばりそのものが問題なのではなく、散らばったまま四つの意味論が並べて書かれていないことが、境界を読めなくしている。

一本化した体系との差

漸進的型付けの標準的な構成では、未確定はDynamic型(?)という一つの型に集約され、既知型との関係は整合性(consistency)という単一の関係で与えられる。どこが動的でどこが静的かが型の上で一目で読める。

Carinaはそうなっていない。四つの表現は層も違う — 値の側にあるもの(deferred、Unknown)と型の側にあるもの(識別なしのカスタム型、注釈の未知型)が混在し、静的段階のどの時点で解消されるかもそれぞれ違う。結果として「この値は今どういう意味で未確定なのか」を答えるには、四つのうちどれかを特定する必要がある。

本当の軸は「層」ではなく「解決時期」である

四つを「値の側/型の側」で割るのは、実は粗い。設計文書がコードと突き合わせて精密化した分類を見ると、同じDeferredValue::Unknownに同居しているものどうしでも解決経路が違う

いつ解決するか
DeferredValue::ResourceRef / BindingRef / Interpolation / FunctionCall値(式)参照解決時
DeferredValue::Unknown(UpstreamRef / UpstreamBareRef)値(apply待ち)上流apply時
DeferredValue::Unknown(ForKey / ForIndex / ForValue / ForValuePath)値(式)iterable解決時
DeferredValue::Unknown(EmptyInterpolation)値(パースエラー)解決しない(診断のみ)
DeferredValue::Secret値(直交)中身に依存
Custom { identity: None }型(静的)解決しない(不変)
TypeExpr::Unknown型(推論エラー復旧)解決しない(エラー復旧)

つまり「未確定」という一語が、正常な未確定・エラー復旧の番人・直交する属性という三つの違う役割を兼ねているEmptyInterpolationTypeExpr::Unknownはどちらも「誰も埋めない」が、前者は編集途中の値、後者は推論失敗の印で、正常系に残るかどうかが違う。Unknownの理由は診断文言ではなく「誰がいつ埋めるか」の分類であるUnknownReasonの10変種を解決経路で割ったのと同じ線が、四つの表現をまたいでも引ける。

型安全性は層ごとに評価が割れる

同じ設計文書が、階層ごとの型安全性をA〜Dで採点している。

Value の Concrete/Deferred 軸 A DeferredValue の変種別 B+ UnknownReason の変種別 B TypeExpr::Unknown の伝播 C Custom { identity: None } の意味 C 階層間の関係性 D 個々の層は型で守られている。守られていないのは、層をまたぐ整合性だけである。
「境界が見えにくい」は主観的な読みにくさではなく、この最下位の一行に対応している。

Custom { identity: None }Noneに混ざっている三つとは、codegenが生成した匿名の篩型・パーサが生成した解決中のもの・provider軸を持たない組み込み型(Ipv4Cidr等)である。同じNoneが「識別を持たせる意義がない」「まだ解決していない」「その軸で区別しない」を兼ねている。

整理が先、統合は後

解の方向は二段階になる。まず四つの意味論を一枚にまとめる — それぞれが何を表し、いつ・誰によって解消され、検査と等価性でどう扱われるかを並べて書く。この整理だけでも、どの二つが実は同じものかが見える。その上で、統合できる組があれば一本化する。

整理が先に来るのは、四つのうちどれが本質的な区別でどれが実装の都合かが、現状では書き出されていないからである。Unknownが理由を持ち運ぶ設計であることや、識別なしのカスタム型が明示キャストなしでは識別付きの受け側に流せないことは、いずれも意図された意味論である。一方でdeferredと注釈側の未知型の関係は説明されていない。区別が意図的なのか偶然なのかを分けることが、統合の可否を決める

目指す形は決まっているが、着手されていない

上の「整理が先」に対する答えは、実は同じ日のうちに設計文書として書かれている。四つの不変条件と四段階のロードマップが引かれ、それぞれ目指すコードの形まで提示されている。

  1. 解決時期を型で区別するValueConcrete / Reference / ApplyTime / Secretに割り直し、参照解決で消えるものとapplyまで残るものを別の型にする
  2. 型レベルの不在と値レベルの不在を統一するTypeExpr::Unknownを廃し、推論失敗はResultで表す(異常系を正常系の語彙で表さない)
  3. identity: Noneの三つの意味を分けるCustomTypeOriginというAnonymous / Builtin / Providerの三値に置き換える
  4. 解決段階を型相(typestate)に持ち上げるStagedValue<Raw / Inferred / ResolvedRefs / Applied>で、関数シグネチャが段階を要求できるようにする。typestateで壊れた状態を書けなくするが挙げる手口を、未確定という軸にも当てるということである

方向としては、この4つ目がノートの言う「境界を引く」ことそのものである。Dynamic型1本への集約ではなく、未確定を消す順序の側を型にするという別の解き方になっている。IaCの未確定は?のように「いつまでも動的」ではなく、段階を追って必ず消えるものだからで、IaC言語は二段階の言語であるの構造に素直に対応している。

2026-08-16 時点の実装状況 不変条件1 — Value を Reference / ApplyTime に割る 未着手 不変条件2 — TypeExpr::Unknown を廃す 未着手 不変条件3 — CustomTypeOrigin を導入 未着手 コードを変えない Phase 1(文書整理)すら完了していない — carina#3212 は今も open
設計は3か月弱前に決まっている。動いていないのは実装の側である。

ただし2026-08-16時点で、コードは1つも動いていない。

コードを変えないPhase 1(用語と文書整理)すら完了していない。完了基準に挙げられたcarina-core/docs/gradual-typing.mdは存在せず、module docからのリンクも無い。対応するissue carina#3212「Document the four forms of 'unknown' in carina's gradual type system」は2026-05-23に立って今もopenである。

動いたのは隣接する二つだけ

この期間に完了したのは、四つの統合ではなく周辺の個別修正である。

注意すべきは#3218の直し方で、identity: Noneの三つの意味を分けないまま判定側だけを直している。設計文書は「#3218の修正をこの新しい型(CustomTypeOrigin)に乗せて実装する」と書いていたが、実際には表現を変えずに閉じられた。症状は消えたが、typestateで壊れた状態を書けなくするの意味での壊れた状態は依然として書けるまま残っている。

結果として、四つという数は3か月弱を経ても四つのままである。

根拠の確度

四つの表現が現在も並存すること、TypeExpr::Unknownidentity: Option<TypeIdentity>が健在でCustomTypeOriginが存在しないこと、ValueConcrete / Deferredの2軸であることは、2026-08-16時点のソースで確認済み(carina-core/src/parser/ast.rscarina-core/src/schema/mod.rscarina-core/src/resource/mod.rs)。

解決時期の表と型安全性のA〜D採点はnotes/specs/2026-05-23-gradual-typing-design.md §1.1 / §1.2 の引き写しで、四つの不変条件とロードマップも同文書 §3 / §4 による。issue #3212 / #2972 / #3218 の状態はGitHub APIで確認済み。

carina-core/docs/gradual-typing.mdが無いことは確認したが、Phase 1の実質的な内容が別の場所で果たされている可能性は追っていない(設計文書そのものが§1.1の表を持っているので、形式的な完了基準を満たしていないだけ、という読み方もできる)。

「動いたのは隣接する二つだけ」は、この四つに直接関わるものに限った話。型システム全般では他にも変更が入っている。

#3218を表現を変えずに閉じたことへの評価は解釈である。判定側だけの修正で健全性が回復しているなら、それで足りるという立場もありうる。

#型システム #漸進的型付け #設計負債