# Part 1　双方向型付けの正体
Source: https://rigor.typedduck.fail/ja/chibirigor/seasoned/part1-bidirectional-typing/

> 後編の最初の章です。後編は「作る」より「読み解く」巻で、前編で*無意識に*作っていた仕組みに正式な名前を与え、その裏側を形式の言葉で読み解きます。この章はほとんど新しいコードを書きません。既に書いたものが、実は何だったのかを明かす総論（地図）です。ただし終わりに1箇所だけ、照合`⇐`が診断を出す口を覗きます。

前編（The Little chibirigor）で、私たちは推論器の心臓として2つの関数を作りました：

- `type_of(node, scope, diag)`：式から型を求める
- `accepts(expected, actual)`：型が期待に合うか確かめる

この2つには、型理論の世界でちゃんとした名前があります。それが**双方向型付け（bidirectional typing）**です。後編は、まずここから始めます。

---

## 1-1. 合成と照合という2つの方向

型付けには、向きの違う2つのモードがあります。

- **合成（synthesize, `⇒`）**：式を見て、型を*下から上へ組み立てる*モード
  - 前編の`type_of`がこれにあたります。`1`を見れば`Integer`、`a + b`を見れば（両者の型から）`Integer`です。入力は式だけ、出力が型になります。
- **照合（check, `⇐`）**：*あらかじめ期待された型*に対して、式が合うかを*上から下へ照合する*モード
  - 前編の`accepts`（を呼ぶディスパッチ）がこれにあたります。「ここは`Integer`が欲しい。この式は合うか？」と問います。入力は式と期待型、出力は合否（chibirigorでは三値）です。

前編の`type_of`は徹頭徹尾`⇒`、`dispatch`が引数を見るところだけが`⇐`でした。つまりchibirigorは、最初から双方向だったのです。図にすると、向きが違う2本の矢印です：

```text
   期待型 T（RBS シグネチャ・注釈・宣言された戻り型）
            │
            │  ⇐  照合（check）   ：S <: T か？（Sが狭い、Tが広い）  ── 合わなければ診断
            ▼
   式 e  ──⇒──▶  型 S
        合成（synthesize）：式から型を組み立てる（chibirigor は失敗せず、未知なら untyped）
```

![図1-1　合成⇒と照合⇐](/ja/chibirigor/figures/svg/seasoned-1-1.svg)
> ▼ 図1-1　合成`⇒`（下から上へ型を作る）と照合`⇐`（上の期待型に突き合わせる）

> **Tip**
>
> **参考書メモ（任意）**：双方向型付けの形式は『TAPL』9章（単純型付きラムダ計算）の型付け規則が土台です。『しくみ』3章（関数型）の`typecheck`は純粋な`⇒`（合成）だけでできています。同書のミニ言語は仮引数に必ず型注釈があるので、`⇐`（照合）を独立に意識する必要がなかったのです。
>
> chibirigorは注釈の無いRubyを相手にするぶん、`⇒`と`⇐`をはっきり分ける必要がありました。それが双方向型付けです。

---

## 1-2. 規則を形式で書く

後編では記法を恐れません。型付け規則は、横線の上に「前提」、下に「結論」を書きます。判断（judgement）は2種類：

- 合成：`Γ ⊢ e ⇒ T`（環境 Γ のもとで、式eの型を合成するとT）
- 照合：`Γ ⊢ e ⇐ T`（環境 Γ のもとで、式eは期待型Tに照合できる）

`⊢`は「ターンスタイル」と読む型理論の記号で、*左の前提のもとで右が導ける*、を表します。`⇒`/`⇐`が合成／照合の向きでした。

`Γ`（ガンマ）は前編の`Scope`（変数名→型）です。たとえば変数参照の合成規則：

```
  x : T ∈ Γ
  ───────────  (Var-Synth)
  Γ ⊢ x ⇒ T
```

「Γ に`x : T`があれば、`x`の型は合成で`T`になる」。前編の`scope.local(node.name)`がこの規則にあたります。`|| Dynamic`の分岐（`x ∉ Γ`）はここではカバーされない別規則で、chibirigorは`x ∉ Γ ⟹ Γ ⊢ x ⇒ untyped`を追加して全域化しています（§1-3①の先取り）。

そして2つの方向をつなぐ、最重要の規則が**subsumption（包摂）**です：

```
  Γ ⊢ e ⇒ S    S <: T
  ─────────────────────  (Sub)
  Γ ⊢ e ⇐ T
```

「式eを合成したらSになった。SがTの部分型なら、eはTに照合できる」。照合とは、『合成してから部分型で突き合わせる』ことです。これが前編の「引数を`type_of`してから`accepts`する」の正体です。`<:`（部分型）と、chibirigorの三値`accepts`の関係はPart 2で詰めます。

---

## 1-3. なぜ診断は照合（`⇐`）でしか出ないのか

前編で、いちばん大事な一行をこう書きました。「診断は『期待される型が決まっている所』でしか出ない」。これを双方向の言葉に直すと、こうなります：

> **重要**
>
> 診断が生まれるのは、照合`⇐`のsubsumptionで`S <: T`が崩れたときだけだ。`⇐`位置とは、期待型Tが宣言または既知の所である。明示注釈や宣言された戻り型に加え、RBS（や前編の手書き表）に載っているメソッド呼び出しの引数位置も含む。

ここは正確に言います。「注釈の無いコードには`⇐`位置が無い」**のではありません**。コア型のメソッド呼び出し（`1 + x`の`+`など）は、RBSが引数の期待型を与えるので、注釈ゼロでも`⇐`位置です。

では*なぜ*それでも動くコードが脅かされないのか。理由は2つあり、どちらも前編Part 9の「わざと見逃す」に対応します：

1. **合成`⇒`がわざと失敗しない（chibirigor固有）**。双方向型付けの**一般的な**定義では、未束縛変数や合成不能な構文で合成は失敗し得ます。chibirigorは*意図的に*、未知をすべて`untyped`に合成して全域化しています。だから「型を見失った式」が`⇐`位置に来ても、合成結果は`untyped`です。
2. **`untyped`は照合を素通りする**。 `accepts`は片方でも`Dynamic`なら無条件で`:maybe`（罰しない）。だから`untyped`が`⇐`位置に来ても診断にならない。

つまり、動くコードが脅かされないのは「`⇐`位置が無いから」ではなく、「合成が未知を`untyped`に倒し、照合が`untyped`を罰しないから」です。双方向の枠組みに、chibirigorのgradualな2つの設計判断（①全域化する合成、②寛容な照合）を重ねて初めて言える性質です。

後編Part 7の「健全性をわざと手放す」で、この同じ2点をprogress／preservationの言葉で受けます。入口で振った伏線を、巻の終盤で回収します。

---

## 1-4. robustness principleと2つの方向

前編Part 7で「返りは厳しめ、引数は緩め」という非対称を見ました。双方向で見ると、これは*方向そのもの*です：

- **戻り値は合成`⇒`**：本体から*いちばん狭い型*を組み立てる（厳しい＝精度が高い）。ただし戻り型の宣言があれば、その宣言に対して本体を`⇐`で照合する（§1-7-aで実装）。
- **引数は照合`⇐`**：期待型に対して*寛容に*受ける（`:maybe`も通す）

Rigorが掲げるrobustness principle（Postelの法則：「返すものは厳密に、受け取るものは寛容に」）は、双方向型付けの2方向に、ぴったり重なります。前編では作法として、後編では理論として現れます。

---

## 1-5. Rigorの中ではどうなっているか

本物のRigorのアーキテクチャは、この2方向がそのまま部品になっています：

- **`ExpressionTyper`**（式の型付け）＝ 合成`⇒`
  - 純粋かつ非破壊で、式から型を組み立てる
- **呼び出し地点での`accepts`**（受理判定、三値 ＋ 理由）＝ 照合`⇐`
  - RBSの宣言が期待型Tを与える所でだけ働く
- **`Scope` / `FactStore`**＝ 環境 Γ（前編より遥かにリッチ。Part 6で扱う）

chibirigorの`type_of`/`accepts`/`Scope`は、この三者の最小版でした。後編は、この骨格に肉を付けていきます。

> **Note**
>
> **記法の出どころ**：双方向型付けはPierce & Turner "Local Type Inference"（2000）が広めた枠組みで、Dunfield & Krishnaswamiのサーベイ "Bidirectional Typing"（2021）が現代的な総説です。注釈をどこに置けば型推論が決定的に回るか、を整理する道具立てです。

---

## 1-6. 後編の地図

双方向という地図を手にすると、後編の残りの章が「地図のどこを埋める作業か」で見渡せます。全体は「① 双方向（地図）→ ② 型の構造 → ③ 推論とフロー → ④ 理論の頂点 → ⑤ 橋」の一本の坂です：

- **Part 2部分型と変性**：subsumptionの`<:`を精密化する
  - とくに*関数の引数は反変*という、方向がもう一段ねじれる話です（『しくみ』7章の本丸）。
- **Part 3ジェネリクスと型代入**：型変数`(X) -> X`と型代入（System F）
  - Part 5の推論がこれを*後方*参照します。
- **Part 4再帰型：μ と余帰納**：`⇒`/`⇐`が自分自身を参照する型をどう扱うか（μ型と余帰納 ↔ RigorのHKT）
  - Part 3と隣接し、α 同値の相互参照が締まります。
- **Part 5本物の型推論**：前編が`⇒`で`untyped`に倒していた所（とくに*引数*）を、本体での使われ方から埋める
  - `⇒`の守備範囲を広げる作業です（『しくみ』9章演習の前線）。TypeProf対比もここに一本化します。
- **Part 6完全なFactStore**：環境 Γ を、フロー感応な事実の集合へ拡張する
- **Part 7健全性と正規化**：双方向の地図（この章）と対をなす頂点
  - 健全性を「わざと手放す」設計をprogress／preservationの言葉で読み解きます。§1-3の伏線をここで回収します。
- **Part 8本物のRigorへ**：最小版から本物のRigorへ渡す橋

---

## 1-7. この章のまとめ

新しいコードはほとんど書きませんでした。代わりに、前編で作ったものに名前を与えました：

| 前編で書いたもの | その正体 |
|---|---|
| `type_of`（型を求める） | 合成`⇒`（synthesize） |
| `accepts`／`dispatch`の引数チェック | 照合`⇐`（check）＝ 合成してから`<:` |
| `Scope` | 型環境 Γ |
| 「診断は期待のある所だけ」 | 診断は必ず`⇐`（subsumption）の中から来る（合成判断それ自体は診断を出さない） |
| 「返り厳しめ、引数緩め」 | 合成`⇒`厳密／照合`⇐`寛容（robustness principle） |

---

### 1-7-a発展ノート：`⇐`が診断を出す最初の口（`check(rbs:)`モード）

§1-3で「診断は`⇐`（照合）でしか出ない」と述べました。前編までの`check`が照合を使うのは「`dispatch`の引数チェック」だけでした。ここに、宣言された戻り型に本体を照合する`check(source, rbs:)`モードを加えると、`⇐`が「呼び出し側」以外でも仕事をする場面が生まれます。

この章で覗くコードはこの1つだけです。照合`⇐`がどこに診断の口を開けるかを見るための小窓です。

```ruby
rbs = <<~RBS
  class Greeter
    def greet: () -> Integer
  end
RBS

Chibirigor.check('def greet; "hi"; end', rbs: rbs)
# => [{line: 1, message: "return type Integer is declared but \"hi\" is returned"}]

Chibirigor.check('def greet; 1; end', rbs: rbs)   # => []（一致）
Chibirigor.check('def greet; "hi"; end')           # => []（宣言なし＝照合なし）
```

**仕組み**（`lib/chibirigor/checker.rb`抜粋）

1. 通常の`eval_statement`ループで本体エラーを収集する（今まで通り）。
2. `rbs:`があれば`Rbs.load(rbs)`でユーザ宣言を読み込み、`DefNode`ごとに`check_against(node, declared_return, body_type, diagnostics)`を呼ぶ。
3. `check_against`は`Accepts.call(expected, actual) == :no`のときだけ診断を追加。`untyped`が絡んだら黙る（gradualの約束）。

```ruby
# ⇐ subsumption: expected に actual を照合。:no だけ診断。
def check_against(node, expected, actual, diagnostics)
  return if expected.is_a?(Type::Dynamic) || actual.is_a?(Type::Dynamic)
  return unless Accepts.call(expected, actual) == :no

  diagnostics << diagnostic(node, "return type #{expected} is declared but #{actual} is returned")
end
```

これが`⇐`を「引数」以外で仕事させる最小の口です。§1-4のrobustness principleを思い出してください。「戻り型は厳密に（`⇐`でチェック）」がここで初めて実装に現れます。前編の`dispatch`が「引数を`⇐`で照合」していたのと対をなしています。

**FPゼロの保証**　`rbs:`を渡さなければ何も照合しない（opt-in）。宣言が`untyped`なら照合しない。本体が`untyped`（推論が型を見失ったとき）でも照合しない。これで「動くコードを脅かさない」は戻り型チェックでも守られます。

> **Note**
>
> **`param:`ディレクティブが担う2つの仕事**
>
> Rigorには、RBSの拡張アノテーション`%a{rigor:v1:param: name is String}`で書く**`param:`ディレクティブ**があります（`.rb`本体にはインラインで書けず、RBS側に置きます）。これは同時に2つの効果をもたらします：
>
> 1. **本体ナローイング**（`⇒`側に型の出発点を与える）：本体内で`name`の型が宣言された`String`から始まる。`is_a?`を書かなくても最初から宣言型で推論が進む。
> 2. **呼び出し地点の`⇐`照合**：`greet(42)`のような呼び出しで、引数型が宣言と合うか`accepts`で照合し、`:no`なら診断を追加する。
>
> つまり`param:`は「書いた人への約束（本体は型に沿う）」と「呼ぶ人への約束（引数を守れ）」を同時に担う。どちらも`⇐`（照合）として統一されているのが双方向型付けのきれいな点です。

---

## 演習

1. `subsumption`（Sub）規則だけを使って、「合成判断`⇒`それ自体は診断を出さない。診断は必ず内側の`⇐`（subsumption）から来る」ことを2行で説明せよ（ヒント：規則Subの前提に`S <: T`の失敗がどこで起きるか）。
2. 注釈ゼロのRuby `1 + x`（`x`は未束縛）を考える。（a）`x`の合成結果は何か。（b）`+`の引数位置は`⇐`位置か。（c）それでも診断が出ないのはなぜか（§1-3の2つの理由のどちらが効くか）。
3. robustness principle「返りは厳密、引数は寛容」を、`⇒`/`⇐`の語だけで言い換えよ（各方向がなぜ厳密／寛容なのかも一言で）。

---

**次章（Part 2）**：subsumptionの`<:`を作り込みます。オブジェクトのwidth/depth部分型、そして関数を渡すときに引数の向きだけ逆になる**反変**です。『しくみ』7章が「実装で変性が向きを変える」と呼んだ、あの山場へ進みます。