# Part 9　gradual の哲学（最終章）
Source: https://rigor.typedduck.fail/ja/chibirigor/little/part9-gradual-philosophy/

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

---

## 9-1. `untyped`は伝染する

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

```ruby
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
```

<!-- run: examples/part9.rb -->
```text
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）は、後者のコストをずっと重く見ます。

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

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

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

---

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

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

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

```ruby
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になります。

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

---

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

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

そしてこの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）や、決して返らない式の型に使います。

> **Note**
>
> 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は、その入口を自分の手でなぞったものです。

> **Tip**
>
> **参考書メモ（任意）**：『しくみ』や『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](/ja/chibirigor/appendix/a3-tooling/)の`trace`を覗いてみてください。各Partで作った部品が、1つの式の上でどう連動するかを目で追えます。

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

---

> **この章の実装（演習の答え合わせにも）** → [`impls/dist/part9/lib`](https://github.com/rigortype/chibirigor/tree/master/impls/dist/part9/lib)