# 付録 a1　特別な型カタログ
Source: https://rigor.typedduck.fail/ja/chibirigor/appendix/a1-special-types/

この付録は、本編のあちこちで初出した「特別な型」（`untyped`（`Dynamic[Top]`）、`void`、`never`（`Bot`）、格子の両端`Top`、`Bot`）を、巻をまたいで引けるよう1箇所に集めた**参照カタログ**です。前編Part 1（`untyped`の初出）、Part 4（Unionとボトム型）、Part 5（ナローイングで枝が空になる話）、Part 8（戻り型`void`）、Part 9（特別な型三つの総括box）から「詳しくは付録[a1](/ja/chibirigor/appendix/a1-special-types/)」のポインタで来た読者を想定しています。

必要な項だけ引いて、本編に戻ってください。各型の詳しい説明の所在は末尾の「さらに深く」で案内します。本筋は概念の整理に徹し、新しいコードは出しません（章末の発展ノートだけは、極小版の実演を1つ添えることがあります）。

---

## a1-1. `untyped`（`Dynamic[Top]`）（gradualの要）

`untyped`は「**知らない、確かめようがない、黙っておく**」を表す型です。chibirigor本体では`Dynamic`という型キャリアで表し、`to_s`は`untyped`と出ます。`type_of`が型を見失ったとき（知らない構文、知らないメソッド）に返すのがこれで、**`untyped`がどこに出るか＝Rigorが型を見失った場所**を指します。

### 2つの軸に分解する

`untyped`（やTypeScriptの`any`）でよく混同されるのは、本来別々の2つの軸が1つに見えてしまうからです。

- **軸A：部分型格子での位置**（型の格子のてっぺん（`Top`、⊤）か、底か）
- **軸B：チェックするか/しないか**（健全な静的型か、gradualの「黙る」型か）

この2軸で並べると、似た顔ぶれの違いがはっきりします。

- TypeScriptの`unknown`は**素直なトップ型**（軸Aだけ）
  - 何でも代入できるが、**絞り込むまで何にも使えない**
  - 「上には入れられるが下からは取り出せない」一方通行で、だから健全です
- TypeScriptの`any`は「何でも代入できる」だけでなく「何にでも代入できる」
  - 格子の**てっぺんと底に同時にいる**ようにふるまいます
  - 部分型関係としては矛盾なので、`any`は**健全性を捨ててチェックをオフにするスイッチ**（軸B）です
  - これがgradual typingの動的型`?`の正体です
- `Dynamic[Top]`は、この2つを**わざと分解して名前で見せた**表現です
  - `Top`が「何でもありうる」健全なトップ型の部分（値集合）で、`Dynamic`がその上に重ねた**gradualの`?`マーカー**（「型を見失った。黙る、脅かさない」の印）です
  - ふるまいは`any`に近いが、一語に潰れず「どこで黙ったか」が構造として残ります
  - 前編Part 9の`rigor check --explain`がfail-softした全箇所を地図にできるのは、この`Dynamic`マーカーが消えずに残るからです

> **Note**
>
> 本文の最小版`Dynamic`（`Dynamic.new`）と内部表記`Dynamic[Top]`は**同じもの**です。
> `[Top]`は「中身は何でもありうる」を明示した内部表記で、本文では添えていないだけです。
> 実Rigorのコードではトップ、ボトムは小文字`top`、`bot`ですが、本書では可読性のため大文字`Top`、`Bot`に統一しています。

ひとことでまとめると、**`unknown`は「分からないから絞れ」と迫り、`any`、`Dynamic[Top]`は「分からないから黙る」**という関係です。同じ「分からない」でも、健全性を取るか現場のコードを止めないことを取るかで、態度が真逆になります。

### 他言語、他ツールの対応表

`untyped`はRubyだけの概念ではなく、型チェッカーを持つ言語には必ず対応物があります。名前が違うだけで役割はどれも「知らない、確かめようがない、黙っておく」です。

| 言語 / ツール | 名前 | 一言 |
|---|---|---|
| TypeScript | `any` / `unknown` | `any`は全照合をオフ、`unknown`は絞り必須 |
| Python (mypy) | `Any` | 引数、戻りの両方向に流れる |
| Go | `interface{}` / `any` | インターフェースの空集合＝何でも入る |
| PHP (PHPStan) | `mixed` | 根型であり「不明」の印でもある |
| C# | `dynamic` | コンパイル時チェックをオフにする |
| Elixir (Dialyzer) | `dynamic()` | 集合論的型の「全集合」 |
| Rigor / RBS | `untyped`（内部: `Dynamic[Top]`） | `Top`（全型の上限）に`Dynamic`を重ねた表現 |

> **Note**
>
> `untyped`が三値受理判定で「両方向に通る」特別な関係（gradual consistency `~`、対称、非推移）になる話は、後編Part 2 §2-5で扱います。

---

## a1-2. `void`（⊤に準じる「値は返るが見るな」）

`void`はRBSの**戻り型**専用の型で、意味は「**値は返るが、その値を当てにするな（見るな）**」です。`Array#each`のように「副作用のために呼ぶ」メソッドに付けます。

### ⊤（トップ型）に準じるふるまい

RBSの型システム上、`void`の格子上のふるまいはトップ型（⊤）とほぼ同じです（top-like）。「どんな値でも受け付ける、その値からは何も引き出せない」からです。ただし`void`は**戻り位置限定のマーカー**で、値の位置に出たときは`top`に戻して扱われます（トップ型と完全な同一物ではありません）。違いは**ニュアンス（込めたメッセージ）**だけです。

- トップ型、`unknown`は「ここには意味のある値がある。使う前に絞れ」と言います
- `void`は「ここに値はあるが意味は無い。**そもそも使うな**」と言います

同じ格子の位置から、読み手に正反対の合図を送ります。型システムは同一でも意図が違う好例です。

### BC breakの契約

Rubyのメソッドは**最後に評価した式が暗黙の戻り値**になるので、`void`を付けたメソッドも実行時には何かを返し、実装を書き替えればその値は変わりえます。`void`はその現実を型として正直に認めた宣言で、「このメソッドは**どんな値を返す可能性もある**」と言っているに等しいです。だからこそ効くのが**契約**の面です。

- 戻り型`void`は呼び出し側に「戻り値に依存するな」と約束させます
  - その結果、**実装が後から戻り値を変えても破壊的変更（BC break）にならない**のです
- 逆に`-> nil`と宣言すると「nilを返す」を約束したことになり、後で別の値を返すよう変えると契約違反になります

ここに`void`を選ぶ実益があります。

### `void`が効くのは照合側`⇐`（後編Part 1への橋）

chibirigorは戻り型を**本体から合成する**側（注釈を検証するのではなく作る）なので、`void`は登場しません。常に「最後の式の型」という具体的な型を出します。つまり`void`は型を組み立てる**合成側`⇒`には出ず**、RBSで宣言された戻り型を本体に照合する**照合側`⇐`で効きます**。その`⇐`（subsumption、三値受理判定）の正体は後編Part 1で扱います。

> **Note**
>
> TypeScriptの`void`、CやJavaの`void`（こちらは「値が無い」寄り）も同じ位置の家族です。

---

## a1-3. `never`（`Bot`）（到達できない枝の型）

トップ型が「何でもありうる」格子のてっぺんなら、その**真逆**にあるのが**ボトム型**（`Bot`、⊥）です。「**値が一つも入らない一番小さい箱**」で、到達できない、起き得ないことを表す型です。

### どこに現れるか

- 戻ってこない式：`raise`だけして値を返さない経路、無限ループ
- 絞り尽くした枝：前編Part 5のdead branch
  - `x : Integer`に`if x.is_a?(String)`を当てたthen枝で`x`がもし型を持つなら「IntegerかつString」です
  - そんな値は**存在しない**ので、型は空集合、つまりボトムです
  - 「絞り込んで候補がゼロになった」状態の型とも言えます

### 双対の性質（`Bot <: T`）

性質もトップと**双対**です。

- トップ型の値は「何でもありうるので**絞るまで何もできない**」
- ボトム型の値は「**そもそも手に入らない**ので、手に入ったと仮定すれば**何にでも使える**」
  - これが**`Bot <: T`：どんな型の部分型でもある**という性質です
  - `never`を返す関数が「絶対に戻ってこない」関数である、というのはこの言い換えです

### 他言語、他ツールの対応表

| 言語 / ツール | 名前 | どこに現れるか |
|---|---|---|
| TypeScript | `never` | 網羅チェックの漏れ、`throw`や無限ループの戻り、絞り尽くした枝 |
| Rust | `!`（never type） | `panic!`、`return`、`loop {}`など「戻ってこない」式 |
| Scala / Kotlin | `Nothing` | 例外を投げるだけの式、空コレクションの要素型 |
| Haskell | `Void` | 値を持たない型（住人ゼロ） |
| Rigor / RBS | `bot`（内部: `Bot`） | 到達不能、`raise`で必ず止まる経路 |

> **Note**
>
> chibirigor本体ではボトム型を型としては作らず、「到達できない枝」を**診断**として扱うにとどめます（実Rigorのunreachable arm、ADR-47）。
> 「脅かさない」方針では、空集合を律儀に伝播させるより「ここは通らないよ」と一言伝える方が現場で役に立つからです。

### a1-3x. 発展：chibirigorにも到達不能アーム診断がある（opt-in）

上の方針どおり、chibirigorにも**到達不能の検出**を足しました。`Bot`という型キャリアは作らず、「その枝のsubjectが空集合（`Bot`）になる」ことを直接判定して`:info`診断を出します（`lib/chibirigor/narrowing.rb`の`unreachable_branch?`）。`check --unreachable`でopt-inします。

```console
$ printf 'x = 1\nif x.is_a?(String)\n  y = x + 1\nelse\n  z = x * 2\nend\n' > demo.rb
$ ruby exe/chibirigor check --unreachable demo.rb
demo.rb:3:3: info: this branch is unreachable (the condition is always false)
    y = x + 1
    ^^^^^^^^^
```

`x : Integer`に`if x.is_a?(String)`を当てたthen枝は「IntegerかつString」、つまり住人ゼロ、つまり`Bot`なので、到達しません。**既定（フラグ無し）では黙ります**。前編Part 4、5の「dead枝は絞らず触らない（誤検知ゼロ）」という約束を崩さないためです。「ここは通らない」と知らせるのは、読者が**明示的に頼んだとき**（`--unreachable`）だけにしてあります。

健全性のため、断言するのは**証明できるときだけ**です。

- subjectが**閉じた既知型**（`untyped`を一切含まない）のときに限ります
  - 少しでも`Dynamic`が混じれば黙ります（gradual）
- `is_a?`は**互いに素だと確実に言える具象クラス（葉）**同士でだけ「起き得ない」と断言します
  - `is_a?(Numeric)`や`is_a?(Object)`のような**祖先関係**は祖先表を持たないので断言しません
  - `x : Integer`でも`x.is_a?(Numeric)`は真になり得るからです（誤検知回避）

これが実RigorのADR-47（`flow.unreachable-clause`）の縮図です。実物はnarrowingがsubjectを`bot`に絞った節をdeadと判定し、ループ、ブロック、gradualを除外するFP envelope（誤検知を防ぐための除外条件の囲い）を持ちます。chibirigorは同じ着想を「葉クラスの互いに素」「閉じた型限定」「opt-in」の三点で最小化しています。

> **Note**
>
> **網羅性（missing arm）とは逆向き**である点に注意してください（付録[a5-5](/ja/chibirigor/appendix/a5-other-languages/)）。
> JavaやC# の網羅検査は「**足りない**枝」を咎めますが、unreachable armは「**余分な（決して通らない）**枝」を指します。前者は「書け」と迫り、後者は「消せる」と教えるだけで、動くコードは止めません。

---

## a1-4. `Top`、`Bot`（格子の両端）

部分型`<:`の格子には、両端があります。**`Bot <: T <: Top`**で、どんな型`T`も必ず`Bot`を下端、`Top`を上端とする間に収まります。

```text
                 Top（⊤）           ← どんな型もこれの部分型（一番大きい箱）
              ╱    │    ╲
     {name:}   Integer   String     ← 具体型
              ╲    │    ╱
                 Bot（⊥）           ← どんな型の部分型（不到達。一番小さい箱）
```

> **Note**
>
> 図の`{name:}`は同じ段の極大要素ではありません。
> 後編 §2-2のとおり構造型は**幅部分型で下に伸びる**（`{name:, age:} <: {name:}`）ので、ここでは「具体型の代表」として置いた略図です。

両端は**双対**です。

| | `Top`（⊤） | `Bot`（⊥） |
|---|---|---|
| 値集合 | 何でも入る（一番大きい箱） | 一つも入らない（一番小さい箱） |
| 部分型 | どんな型も`Top`の部分型（`T <: Top`） | どんな型の部分型（`Bot <: T`） |
| 値の使い方 | 絞るまで何もできない | そもそも手に入らない＝何にでも使える |
| 本編での顔 | `unknown`、`void`（前編Part 1、8） | `never`（前編Part 4、5） |

subsumptionが「上へ（`Top`方向に）緩める」操作なのに対し、`Bot`は格子の底から「どの型のふりでもできる」という向きになっています。双方が対称になっているのが格子の美点です。

> **Note**
>
> 注意：`untyped`（`any`、`Dynamic[Top]`）は**トップ型ではありません**。
> a1-1の軸A、軸Bのとおり、`Top`は健全なトップ型（軸A）で、`untyped`はそこに「チェックを切る」マーカー（軸B）を重ねたものです。別物です。

---

## a1-5. 三つの型まとめ比較（`untyped`、`void`、`never`）

初学者が混同しやすい三つを並べると、軸がはっきりします。

| 型 | 制御は戻る？ | 値は？ | 一言 | 初出 |
|---|---|---|---|---|
| `untyped`（`unknown`） | 戻る | あるが**型が不明** | 「中身が分からない」 | 前編Part 1 |
| `void` | **戻る** | あるが**見るな** | 「戻り値を当てにするな」 | 前編Part 8 |
| `never`（`Bot`） | **戻らない** | **無い**（住人ゼロ） | 「そもそも返ってこない」 | 前編Part 4 |

- `void`は「値の中身が分からない」（`untyped`）でも「返ってこない」（`never`）でもなく、**戻り位置に立てる「黙れ」の印**です
  - チェッカーに「ここの戻り値は照合しなくていい」と告げる点で`untyped`の親戚ですが、対象は値ではなく戻り値の使われ方です
- `untyped`と`void`はどちらも「黙れ」の家族ですが、`untyped`は格子に**トップとして自立しない**（`Top`にマーカーを重ねたgradual型）で、`void`は格子上は**トップに準じる**（ただし戻り位置限定のマーカー）という違いがあります
- `never`、`Bot`だけが格子の**底**で、他の二つ（てっぺん側）と方向が逆です

---

## a1-6. さらに深く（各詳しい説明の所在）

この付録は「引く」ための整理です。理屈の詳しい説明は次の場所にあります。

- **`never`、`Bot`、格子と双対の形式的扱い** → 後編Part 2「部分型と変性」（`Bot <: T <: Top`、S-Arrowと変性）
- **`void`、`Top`、戻り型の照合`⇐`** → 後編Part 1「双方向型付け」（合成`⇒`、照合`⇐`の地図）
- **`untyped`のgradual consistency `~`（対称、非推移）** → 後編Part 2 §2-5、および「わざとunsound」の総括は後編Part 7
- **refinement carrier（`non-empty-string`、`positive-int`等、述語で絞った型）** → 付録[a2](/ja/chibirigor/appendix/a2-narrowing-patterns/)「ナローイングのパターン集」、[用語集](/ja/chibirigor/glossary/)の「refinement carrier」「`Difference`型」の項
  - `Const`（ピンポイントの値）との違いもそこにあります
- **前編での総括** → 前編Part 9の「特別な型三つ」総括box