Part 7　健全性と正規化、そして「わざと unsound」

ヒント

参考書（任意）：『TAPL』8章「型付き算術式」§8.3（安全性＝進行＋保存）、12章「正規化」、『しくみ』おわりに。 型理論の中心定理を据え、なぜchibirigorはわざと健全でないのかを形式の言葉で言い切る章です。

この章のゴール：「型システムとは何か」「健全とは何か」を定義し、chibirigor（とRigor）が意図的にその健全性を手放していることの意味を言葉にする。

Part 6では、フローを支える本物のFactStore（6種の事実、無効化、クロージャ捕獲）まで道具を作り切りました。最後に一段引いて、ここまで作ってきたものが「型システム」として何を保証し、何をわざと保証しないのかを、理論の言葉で言い切ります。

---

7-1. 「型システム」の狭義と広義

『しくみ』おわりにの整理を借ります：

• 狭義：型システム＝型付け規則の集まり（どの式にどう型を付けるか）
• 広義：それに加えて、規則について証明できる定理、とくに型安全性（健全性）と正規化可能性

型チェッカーは、「入力プログラムが型付け規則で説明できるか」を機械的に判定するプログラムです。前編で作ったものは、まさにこの「規則を機械的に決定可能にしたプログラム」でした。『TAPL』9章Figure 9-1の変数規則T-Varを、前編のtype_ofのLocalVariableRead節と並べると、規則とコードが一対一に対応しているのが見えます。

---

7-2. 健全性（進行と保存）

型安全性（type safety / soundness）の標準的な定式化は、2つの定理の組です（『TAPL』8.3）：

• 進行（progress）：型の付いた項は、値であるか、次の評価ステップが必ず存在する（＝行き詰まらない＝未定義動作に陥らない）
• 保存（preservation / subject reduction）：型の付いた項を1ステップ評価しても、型は保たれる

二つ合わせると：「型の付いたプログラムは、評価のどの時点でも行き詰まらない」。これが「型が付けば未定義動作に陥らない」という保証の中身です。「Well-typed programs cannot go wrong」（Milner）。

---

7-3. 正規化（型が付けば止まる）

もう一つの定理が正規化可能性（normalization）（『TAPL』12章）です。単純型付きラムダ計算では、型の付いたすべての項は、必ず停止する。(λx. x x)(λx. x x)（発散項 Ω）のようなものは、型が付きません。

鍵は自己適用x xです。xを「xを受け取る関数」と「その引数」の両方に使うには、x : A -> Bかつx : A、つまりA = A -> Bという再帰的な型が要ります。単純型にはそれが無いので、Ω は型付け不能です。だから「型が付けば止まる」が破れません（再帰型を足すと話が変わる、後編Part 4）。

正規化（型が付けば必ず止まる）は単純型付きの中核の性質で、『TAPL』12章の主題です。再帰型（『しくみ』8章）や一般再帰を足すと一般には成り立ちません。そしてchibirigorは、この性質を持ちません。相手は停止しない実Rubyだからです。

---

7-4. なぜchibirigorはわざとunsoundなのか

ここが、後編で最も大事な一節です。前編で作ったものは健全ではありません。わざとです。

健全なチェッカーは「型が付く ⇒ 絶対に安全」を保証する代わりに、安全だが証明できないプログラムを弾きます（保守側の誤検知）。動的言語の現実のコードは、その「安全だが証明しにくい」塊です。ここで健全性を貫くと、動くコードが真っ赤になる。だからchibirigor（とRigor）は、健全性を意図的に手放します。

前編Part 9 §9-2で標語として挙げた「わざと見逃す4箇所」を、ここで §7-2の言葉（進行と保存）で言い直します。

健全な型システムは「型が付く ⇒ 実行が行き詰まらない（progress）」を保証します。chibirigorの4つの穴は、いずれもこのprogress保証をわざと手放す箇所です。つまり「型が付いても、NoMethodError等で行き詰まり得る」を許します。各穴が許してしまう「行き詰まり（stuck state）」はこうです：

前編 §9-2の標語	progress、preservationの言葉	許す「行き詰まり」
① untypedは何でも受理	progressを放棄（untypedをどの期待型にも受理＝subsumptionを素通し）	untyped値が応えないメソッドを呼ぶ → NoMethodError
② openなhash、未知キー→nil	progressを放棄（幅部分型を引数で緩める）	実は無いキーがnil → nilへの呼び出しで停止
③ :maybeを罰しない	progressを放棄（証明不能を:noに昇格させない）	:maybeが実は不一致 → 実行時の型エラー
④ 保守的ナローイング	progressの検出を放棄（disjoint、Dynamicを絞らない）	絞れず見逃した枝の実エラーを報告しない

preservation（評価で型が保たれる）の側は、chibirigorはそもそも強く主張しません。怪しくなればuntypedにwidenするので、preservationはconsistency（~）の意味で自明に保たれます（型が合わなくなったらuntypedに倒すだけ）。手放しているのは主にprogress、というのがこの4箇所の正体です。

形式的に言えば：chibirigorは健全性（soundness）、とくにprogressを、誤検知の少なさ（“never frighten working code”）と引き換えに、限定的に放棄している。これは欠陥ではなく設計の選択です。健全性は「バグを1つも見逃さない」を意味しますが、その代償（動くコードを脅かす）の方が、実用チェッカーでは高くつくと判断しているのです。

重要

巻のブックエンド：前編 §1-3で「動くコードを脅かさない／わからない所はそっと通す」と前振りした約束を、後編はここでprogress、preservationの言葉で回収しました。 双方向の地図を広げた後編Part 1（入口）と、健全性を「わざと手放す」設計を言い切るこの章とが、呼応します。

---

7-5. gradualの2つの規律（consistencyとguarantee）

「では完全に何でもありか」というと、そうではありません。健全性は手放しても、gradual typingには別の規律があります。chibirigorが守っているのは、次の2つです。

規律その1（gradual consistency ~、型の側の規律）

untyped（Dynamic）が絡むと、部分型<:は両方向に通る特別な関係になります。これをgradual consistency（漸進的整合性） ~と呼びます（後編Part 2 §2-5から送られてくる論点）：

• untyped ~ TもT ~ untypedも成り立つ（対称）
• でも~は推移的でない：Integer ~ untypedかつuntyped ~ StringでもInteger ~ Stringではない
  • だからuntypedを「何にでも化ける抜け穴」にしつつ、IntegerとStringの取り違えは依然:noにできる

ノート

~はgradual typingの学術慣例（Siek）の記号です。 実Rigorはドキュメントで記号衝突を避け、この関係をconsistent(A, B)と綴ります（~Tは否定、補型に予約）。 意味（対称、非推移）は同じです。

前編の三値acceptsは、まさにこの<:（証明できる、できない）と~（untypedが絡む）を一つの判定に畳むためのものでした：

状況	結果
S <: Tが証明できる	:yes
untypedが絡む（~だが<:は不明）	:maybe
SとTが確実に互いに無関係	:no

~が非推移だからこそ、untypedは無制限の抜け穴になりきらない。ここが「無秩序ではない」の一つ目の意味です。

規律その2（gradual guarantee、注釈量の側の規律）

もう一つがgradual guarantee（Siekら）です。型の側ではなく、注釈の量と挙動の関係に対する規律です：

ノート

注釈を増やしても減らしても、プログラムの意味（通る、通らない、動作）は連続的に変わる。 型注釈を減らせばチェックは緩くなるだけで、急に壊れたりはしない。

chibirigorの「untypedに倒す」「注釈の無い所は照合位置を作らない」という設計は、このgradual guaranteeの素朴な現れです。注釈を1つ足したからといって、無関係な箇所が突然真っ赤になったりしない。健全性は手放したが、無秩序ではないの二つ目の意味です。

~（型の整合）とguarantee（注釈量への連続性）。この2つの規律が、「わざとunsound」を無秩序から区別しています。

ヒント

参考書メモ：静的な<:までが『TAPL』15、16章の世界です。 untypedを足した~は『TAPL』の先、gradual typing（Siek & Taha 2006）の領域で、前編Part 9、この章で扱う「わざとunsound」の核です。

ノート

assert:ディレクティブで「確かめた上で約束する」

Rigorがunsoundであっても、特定の箇所だけ健全性を取り戻す抜け道がassertディレクティブ（RBSの拡張アノテーション）です。 検査、正規化を行うメソッドに付けます：

# RBS側に書く（`.rb`本体にはインラインで書けない）
# %a{rigor:v1:assert x is non-empty-string}
def ensure_present!(x) = (raise if x.nil? || x.empty?)

意味は「このメソッドが返った後、呼び出し元のxはnon-empty-stringだ」。 本体内ではなく呼ぶ側のスコープに事実を足すゲートです。 推論が型を追えない動的ディスパッチやevalの後でも、ガードメソッドを一度通せば「ここから先は私が保証する」と宣言できます。 嘘を書けばその先の診断が嘘になります（acceptsが:yesに化ける）。

機構	型の根拠
is_a?(String)	Rigorが推論した事実
%a{rigor:v1:param: x is String}	宣言 → 呼び出し地点の照合＋本体での束縛
%a{rigor:v1:assert x is String}	ガード通過後、呼び出し元のxを強制

TypeScriptのユーザー定義型ガード（x is Tを返す述語関数）に近い役割です。 Rigorでは「unsoundな型キャスト」ではなく「確かめた上で事実を足す操作」として扱います。

---

7-6. 停止性をどう工学で守るか（余帰納、fuel、予算）

正規化（型が付けば止まる）もchibirigorは持てません。理論が「型が付けば止まる」を証明で保証するのに対し、実用チェッカーは「解析そのものが止まる」を工学で守ります。この章まで出てきた停止性の道具は、同じ対比の相似形が三段の大きさで並んでいます。

余帰納（後編Part 4）

同値再帰の型等価判定は、放っておくと止まりません（μX.{foo:X}を展開し続ける）。後編Part 4は余帰納（coinduction）＝仮定集合seenでこれを断ちました。「いま比較中のペアを再び問われたら、等しいと仮定して打ち切る」。これは正しく止める解です（最大不動点としての部分型、『TAPL』21章）。

HKT還元fuel（後編Part 4、ADR-20）

Rigorは再帰型を μ＋余帰納で直接は実装せず、軽量HKT（Type::App）＋fuel（燃料）予算で別解にしています（後編Part 4 §4-5から送られてくる論点）。高階型を展開するたびにカウンタを消費し、上限（既定64ステップ）で打ち切ります。これは危なくなったら止める解です。fuelが尽きれば結果を:maybeに倒し、untypedに逃がして安全側に着地します。

止め方	性格	どこで
余帰納（seen）	正しく止める（最大不動点）	教える等価判定（後編Part 4）
HKT還元fuel（ADR-20）	危なくなったら止める	Rigor実装済み
推論予算（ADR-41）	危なくなったら止める（広義）	設計済み、未実装

推論予算（inference budget、ADR-41）

fuelがHKT還元という局所の停止を守るのに対し、より広義の推論予算（inference budget、ADR-41）も設計されています。解析全体を予算で打ち切る、fuelの大きな相似形です。ただしこちらは現時点では未実装（ADR-41はStatus: Proposed）です。

「型システムが正規化を保証する」という理論の美しさが、実用チェッカーでは「解析を予算で打ち切る」という工学に置き換わる。余帰納（正しく止める）、fuel、予算（危なくなったら止める）は、同じ「展開をどう止めるか」という問いに対する、規模を変えた同じ答えです。実用チェッカーが「危なくなったら止める」を選べるのは、「分からなくなったらuntypedに倒す」というgradualの割り切りがあるからでした。

---

7-7. まとめ

• 型システム＝狭義（型付け規則）＋広義（健全性、正規化の定理）
  • チェッカー＝規則の決定手続き
• 健全性（進行と保存）：型の付いたプログラムは評価のどの時点でも行き詰まらない（『TAPL』8.3）
• 正規化：型が付けば停止（『TAPL』12）
  • 再帰型や一般再帰を入れると一般には成り立たない
• chibirigorはわざとunsound：健全性（とくにprogress）を「誤検知の少なさ」と引き換えに限定放棄
  • 前編 §9-2の「見逃す4箇所」がその穴の正体
  • §1-3の前振りをここで回収する
• ただし無秩序ではない。gradualの2つの規律：consistency ~（対称、非推移）とgradual guarantee（注釈量に対して挙動が連続）を守る
• 正規化の代わりに、停止性を工学で守る
  • 余帰納（正しく止める）、HKT fuel（ADR-20、実装済み）、推論予算（ADR-41、設計済み、未実装）の、規模を変えた相似形

演習

1. 穴をprogressで言い直す：§7-4の表の4つから1つ選び、その穴が許す具体的な動くRubyと、それが行き詰まる入力を1組作れ（例：untyped受理 → x.fooがNoMethodError）。
2. 進行と保存：「型が付いてもNoMethodErrorになり得る」は進行と保存のどちらの放棄か。 chibirigorが保存はほぼ保てる理由（untypedへのwiden）と併せて述べよ。
3. Ω が型付け不能：(λx. x x)に単純型を付けようとして詰まる所（A = A -> Bが要る）を示し、再帰型（後編Part 4）を足すと何が変わるかを一言で。
4. 2つの規律：gradual consistency ~が非推移であることと、gradual guaranteeが注釈量に効くことを、それぞれ「もしこの規律が無かったら何が壊れるか」で1文ずつ説明せよ。
5. 止め方を並べる：余帰納（seen）、HKT fuel、推論予算の3つを「正しく止める、危なくなったら止める」で分類し、Rigorが後者を選べる理由（gradualの割り切り）を一言で述べよ。

次章（Part 8、最終章）：chibirigorの最小版から、本物のRigorの作り込み（プラグイン、キャッシュ、LSP、性能、baseline）へ橋を架けて、後編を締めます。