Part 9　gradual の哲学（最終章）

この章のゴールは、untypedの伝播を仕上げ、baselineを据え、「chibirigorがわざと見逃している所」を総括することです。そして、漸進的型付け（gradual typing）という大きな流れと、その先のRigorへ接続します。前編はここで閉じます。

---

9-1. untypedは伝染する

最後の小さなコード変更を一つ。untyped（Dynamic）がunionに混じったら、全体をuntypedにします。

module Type
  module_function

  def union(types)
    flat = types.flat_map { |t| t.is_a?(Union) ? t.members : [t] }.uniq
    return Dynamic.new if flat.empty?
    return Dynamic.new if flat.any?(Dynamic)   # ★ untyped が混じれば全体 untyped
    return flat.first if flat.size == 1
    Union[flat.freeze]
  end
end

c ? 1 : foo.bar  ->  untyped
c ? 1 : "a"      ->  1 | "a"

理屈は素直です。一部でも型を見失っているなら、そのユニオン型について断言はできません。1 | untypedと中途半端に持つより、untypedと正直に言う。これがgradualの考え方です。

---

9-2. chibirigorが「わざと見逃している」4箇所

chibirigorは健全（sound）ではありません。わざと見逃します。「動くコードを脅かさない」ためです。どこで見逃しているかを、最後にはっきりさせます。

1. untypedは何でも受理する（Part 7のacceptsが:maybe）。型を見失った境界の穴。
2. ハッシュの未知キーはnil（Part 6）。余剰キーも許す（open）。『しくみ』のように完全一致で弾けば、動くoptionsハッシュが真っ赤になる。
3. :maybeを罰しない（Part 7のdispatch）。疑わしきは黙る。
4. 絞り込みは保守的（Part 5）。読めない条件、disjoint、Dynamicは絞らない。

どれも「見逃し＝バグを見落とす危険」と引き換えに「誤検知＝動くコードを脅かす」を避けています。chibirigor（とRigor）は、後者のコストをずっと重く見ます。

ノート

いま標語として挙げたこの4つは、後編The Seasoned chibirigor Part 7で、健全性（progress＋preservation）をわざと破る穴として、形式の言葉で言い直します。「なぜunsoundでよいのか」に、理論からの答えが付きます。

この章の三つの視点（パースペクティブ）：

• ① 型理論：健全性（未定義動作の排除）か、誤検知の少なさか、というトレードオフ。
• ② Rubyだと：動的言語に後付けの型です。厳しすぎると現場のコードが回りません。
• ③ Rigorだと：「動くコードを脅かさない」を最上位の価値に置き、わざと見逃します。

---

9-3. baseline（既存を呑み、新規だけ見る）

それでも、初めて既存コードにかけると診断が大量に出ることはあります。そこでbaselineです。最初に出た診断を「呑んだもの」として記録し、以降は新規の診断だけを見せます。

def check(source, baseline = [])
  # …診断を集める…
  diagnostics.reject { |d| baseline.include?(d) }
end

base = check(source)              # 最初の診断を baseline として保存
check(edited_source, base)        # baseline に無い新規だけが出る

「既存の指摘は一旦そのまま、これから書くコードだけ綺麗に」。これも「脅かさない」の一形態です（Rigorの.rigor-baseline.ymlの縮図）。導入の最初の一回でいきなり全部を直させない、つまり既存コードを脅かさないためのもう一つの仕組みです。

何で照合するか（列は含めない）

baselineは「同じ診断かどうか」を判定して、既知のものを引きます。何をキーに照合するかが設計の勘どころです。chibirigorのbaselineは行とメッセージだけで照合し、列は含めません。

理由は単純で、同じ行を編集して桁がズレてもbaselineが外れないようにするためです。診断の表示（Part 1のキャレット^^^）には列と長さを持たせましたが、baselineの同一性判定には持ち込みません。表示の精度と照合の安定性は別の話、という切り分けです。

実Rigorのbaseline（ADR-22）は、これをさらに堅牢にしています。デフォルトで照合するのはルールID（どの規則に引っかかったか）で、行番号はキーに含めません。行が上下に動いてもbaselineが外れにくい、という設計です。列を含めないのはchibirigorとRigorのいずれも同じです。

まとめると、chibirigorは「行＋メッセージ」、Rigorは「ルールID（行は含めない）」で照合し、どちらも列は見ません。粗いキーほど、編集に強いbaselineになります。

ノート

実Rigorには、この「黙って見逃した（fail-softした）場所」を一覧にするrigor check --explainという調査コマンドがあります。「なぜ報告されないのか＝どこで型を見失ったか」の地図を出す道具で、chibirigorの「知らなければ黙る」が裏返すと「静かに見逃す」になる、その沈黙を可視化します。仕組みは付録a3-1へ。

---

9-4. 特別な型3種を総括する

前編を通して、ふつうの型（Integer、String、Const[1] …）とは毛色の違う「特別な型」が何度か顔を出しました。最後にここで束ねておきます。どれも「チェッカーにある態度を告げる印」であり、ふつうの型のように「値の形」を表しているのではありません。3種を一覧で見比べる表は付録a1-5にあります。

そしてこの3つの足元には、型を大小で並べた格子（lattice）の両端があります。一番大きい（何でも入る）Top（⊤）と、一番小さい（住人ゼロで到達しない）Bot（⊥）です。TopはJavaのObjectに近い「てっぺん」ですが、チェックでの効き方は別物です。ここでは記号と位置関係だけ掴めば十分で、格子そのものの本式は後編に送ります。untypedはTopに「黙れ」のマーカー（Dynamic）を重ねたもの、neverはBotそのもの、voidは格子上のふるまいとしてはTopの隣、という関係でした。

• untyped：型を見失ったときの逃げ場です。何でも受理し、何にでも渡せます（健全性を捨てた「黙る」型）。前編でいちばん働いた特別な型で、9-1の「伝染」もこれです。
• void：戻り型の位置に立てる「黙れ」です。「値は返るが当てにするな」という意味で、-> nilと違って実装が後で戻り値を変えても破壊的変更にならない、という契約上の実益があります。
• never／Bot：住人ゼロの型です。「この枝には到達しない」を表し、ナローイングのdead branch（Part 5）や、決して返らない式の型に使います。

ノート

3種のカタログ（軸A：部分型の位置、軸B：チェックの有無、any/unknown他言語対応表）は付録a1。never／Bot（底型と部分型格子）の本式は後編Part 2（部分型と変性）、void／Top（双方向の⇐側でどう効くか）は後編Part 1（双方向型付け）で扱います。前編では「3つの特別な型がある」と束ねるところまでです。

---

9-5. ここから先（gradual typingとRigorへ）

chibirigorは、最初から一貫してこの立場で作ってきました。

	静的、健全なチェッカー	chibirigor（漸進的）
判定	適合、不適合の二値	:yes/:no/:maybeの三値
未知の型	無い（注釈必須）	untyped（Dynamic）が主役
不適合のとき	例外で止まる	診断を貯めて続行、未知は黙る
価値観	健全性	誤検知を出さない（脅かさない）

「型を見失っても止まらない」「わからない所は黙る」「動くコードを脅かさない」。この漸進的型付けは、2000年代の型システム研究で定式化された設計思想です。chibirigorは、その入口を自分の手でなぞったものです。

ヒント

参考書メモ（任意）：『しくみ』や『TAPL』をお持ちなら。『しくみ』は静的で健全なチェッカーを作り、最後に「次のフロンティア」としてgradual typingを指さして終わります。chibirigorは、ちょうどその先から始めた、と読めます。併読すると「なぜ三値か」「なぜuntypedに逃がすか」が腑に落ちやすいでしょう。無くても本書だけで完結します。健全性の本式は『TAPL』8章 §8.3「安全性 = 進行 + 保存」、gradualはその先（『TAPL』後の研究）です。

chibirigorを作り終えたいま、本物のRigorを覗くと、ここで見た一つ一つ（Scope、accepts、ナローイング、RBS、sig推論）が、実用規模で作り込まれているのが分かります。chibirigorは、Rigorへの入口です。

---

9-6. ここまでのまとめ（前編 全9章）

Part	足したもの
1	Const/Dynamic/Nominal、type_of、check/annotate
2	Dispatch（メソッド表）、未知はdegrade、定数畳み込み（発展）
3	不変Scope、eval_statement（文を縫う）
4	Union、if/三項で枝の型を1本にまとめる
5	narrow、nil?/is_a?ナローイング、2つの掟、再代入リセット（dead branchは絞らない）
6	HashShape/Tuple、添字読み（未知キーはnil、open）
7	accepts（三値）、:noだけ報告
8	Rbs.load、defの戻り型合成、RBS風シグネチャ、untypedの可視化
9	untypedの伝播、baseline、わざと見逃す総括、特別な型3種

前編を読み終えたあなたができること

数百行のRubyだけで、ここまで来ました。

• Rubyのソースから型を推論し（リテラル、メソッド、変数、分岐、ハッシュ/配列）、
• 矛盾を診断として報告し（しかも止まらず、わからない所は黙る）、
• 推論した型とメソッドのシグネチャをannotateで見せ、
• 既存コードをbaselineで呑んで「これから書くコードだけ」を綺麗に保ち、
• 「動くコードを脅かさない」を、untyped、三値、open shape、保守的ナローイング、baselineという具体的な仕組みとして実装した。

これは本物のRigorの最小版です。後編では、この一つ一つに理論の裏打ちを与えます。

演習

1. c ? 1 : foo.barがuntypedになることを確かめ、unionのどの行が効いたか指せ。
2. checkにbaselineを渡し、既存の診断が消え、新規の診断だけが出ることを確かめよ。
3. baselineが「行＋メッセージ」で照合し列を含めないのはなぜか。同じ行の末尾に空白を足して桁をずらしたらbaselineはどうなるか、9-3の照合キーから説明せよ。
4. 「わざと見逃す4箇所」のうち1つ（例：未知キー→nil）を、あえて厳しく（エラーに）したら、どんな動くコードが脅かされるか、具体例を1つ挙げよ。

---

組み上がった推論器が動く様子をコマ送りで眺めたくなったら、付録a3のtraceを覗いてみてください。各Partで作った部品が、1つの式の上でどう連動するかを目で追えます。

続編「The Seasoned chibirigor」へ：双方向型付けの形式化、変性、再帰型、引数推論（型再構築）、完全なFactStore、健全性理論、erasure/sig-gen本体。『型システムのしくみ』の先と、Rigorの作り込みへ。前編で手を動かして作ったものに、後編で理屈の名前が付きます。

---

この章の実装（演習の答え合わせにも） → impls/dist/part9/lib