# Part 5　本物の型推論：引数を埋める
Source: https://rigor.typedduck.fail/ja/chibirigor/seasoned/part5-real-inference/

> 参考書（任意）：『TAPL』22章「型再構築」、『しくみ』9章演習、おわりに。
> 前編が`untyped`に倒していた*引数*の型を、本体での使われ方から導出する章です。
> 『しくみ』が「正解を知らない」と解答を放棄した、推論の前線です。

Part 4では型が*自分自身*を参照する再帰型を扱いました。ここからは向きを変え、前編で*untypedに倒していた*引数を埋めにいきます。

前編Part 8で、メソッドの**戻り型**は本体から合成できました（`def shout; "hi".upcase; end` → `() -> String`）。しかし**引数**は`untyped`に倒したままでした。`def double(n); n * 2; end`は`(untyped) -> untyped`でした。

この章は、その`untyped`を埋めにいきます。これは前編で*意図的に避けた*最大の山であり、本物の型推論の入口です。

---

## 5-1. なぜ引数は難しいのか

戻り型は「本体を合成（`⇒`）すれば出てくる」という、下から上への一方向でした。引数は逆です。`n`の型は、`n`が本体で**どう使われたか**を集めて、初めて分かります。`n * 2`を見て「`n`は`*`に整数を渡せる何か」と*逆算*する必要があります。これは合成`⇒`の素直な流れに逆らうので、別の道具が要ります。

道は大きく2つあります。**（A）使われ方から能力を集める**（capability/duck推論）と、**（B）型変数を置いて制約を解く**（制約ベース、『TAPL』22章の型再構築）です。後編は（A）を主に、（B）を初歩だけ扱います。

---

## 5-2. 道A　使われ方から「能力」を集める

Rubyはダックタイピングの言語です。「`n`が何のクラスか」より「`n`が何に**応えられるか**」が本質です。だから引数を、具体的な型ではなく**能力（インターフェース）**として推論します。

本体を一度なめて、その引数に送られたメッセージを集めます：

```ruby
def greet(user)
  "Hello, " + user.name        # user に .name（→ String を返す何か）
end
# 集めた能力: { name: () -> String }
# 推論: user : { name: () -> String } を満たす何か（構造的インターフェース）
```

これは前編Part 6の`HashShape`と地続きの**構造的な型**で、Rigorでは**capability role**（`_ToS`、`_Each[T]`などの能力ロール）に対応します。「`String`か」ではなく「`name`に応えるか」で受けるので、ダックタイピングを*壊さずに*型を付けられます。

**FP安全の要**：集めるのは「確実に送られたメッセージ」だけです。条件分岐の奥や`respond_to?`ガードの内側など、**送られるか怪しい**メッセージは能力に*加えません*（疑わしきは要求しない）。要求を増やしすぎると、動く呼び出しを弾く誤検知になります。

---

## 5-3. 道B　型変数と制約（型再構築の初歩）

もう一段進めると、**型変数**を置いて**制約**を集め、まとめて解きます。これが『TAPL』22章の**型再構築（type reconstruction）**、いわゆるHindley–Milnerの骨子です。

```ruby
def id(x)
  x            # x の型を未知の型変数 X とする
end
# 制約: （本体は x をそのまま返すだけ）→ 制約なし
# 解: id : (X) -> X   （= ジェネリック！ Part 3 で作った型変数の正道）
```

```ruby
def inc(n)
  n + 1        # n は Integer#+ に渡せる → 制約 X <: (Integer#+ の引数を受ける)
end
# 解: n は Integer 寄りに絞られる
```

手順は3段あります。**（1）各未知に型変数を割り当て**、**（2）本体を歩いて制約（等式、部分型）を集め**、**（3）単一化（unification）で解く**（集めた等式を見て、2つの型を「同じ」とおける型変数の割り当てを求める操作）です。`id`のように制約が残らなければ、その型変数は*そのままジェネリック*になります（`(X) -> X`）。ここで使う型変数、型代入は、Part 3で作ったものです。

この「制約を集めて単一化で解く」核を、動く最小スケッチにしたのが[`examples/unification.rb`](https://github.com/rigortype/chibirigor/blob/master/book/v2/ja/seasoned/examples/unification.rb)です。型変数`TVar`と基底型`TCon`だけの世界で、単一化はこれだけです：

<!-- include: unification.rb#unify -->
```ruby
# 代入 subst で type をたどり、これ以上たどれない形まで解決する
def resolve(type, subst)
  type.is_a?(TVar) && subst.key?(type.name) ? resolve(subst[type.name], subst) : type
end

class UnifyError < StandardError; end

# a と b を等しくする代入を返す（できなければ UnifyError）
# 注：本スケッチは occurs-check を省略している（`unify(X, X->X)` のような自己参照が通ってしまう）。
# TVar/TCon のみの世界では関数型を作らないため自己チェックは緑のまま動くが、
# 本物の HM では occurs-check が停止性・健全性に必須。
def unify(a, b, subst)
  a = resolve(a, subst)
  b = resolve(b, subst)
  return subst if a == b
  return subst.merge(a.name => b) if a.is_a?(TVar) # 変数 a を b に束縛
  return subst.merge(b.name => a) if b.is_a?(TVar) # 変数 b を a に束縛

  raise UnifyError, "#{a.name} and #{b.name} don't match"
end

# 制約（= 等しくしたい型のペア）を順に単一化していく
def solve(constraints)
  constraints.reduce({}) { |subst, (a, b)| unify(a, b, subst) }
end
```

`ruby unification.rb`で、`id`は制約ゼロで`X`が自由（ジェネリック）になり、`inc`は`N = Integer`に解け、矛盾する制約は`UnifyError`になる、が**緑**になります：

<!-- run: unification.rb -->
```text
PASS: id has no constraint (X stays generic)
PASS: inc resolves N to Integer from n + 1
PASS: conflicting constraints raise UnifyError
```

> **Tip**
>
> **参考書メモ**：『TAPL』22章が制約生成と単一化を丁寧に展開します。ここで作るのは「単一化と制約」までで、**MLの`let`多相**（束縛ごとに型を一般化するHM固有の仕組み）には踏み込みません。全称型（∀）の一般化が絡む話で、本書ではPart 3で扱いました。
>
> 『しくみ』もこの推論には踏み込まず、9章では演習の課題として読者に残しています。後編がここを埋めます。

---

## 5-4. なぜ「全部」はやらないのか

完全なHM推論は、MLのように*注釈ゼロ*で大域的に型を解きます。なぜchibirigor（とRigor）はそこまで行かないのか。理由は3つあります：

1. **決定性と速度**：大域単一化は、メソッドをまたぐと制約が爆発しやすく、実コードの規模ではコストが高くつきます。
2. **誤検知**：強く推論するほど「動くが型が付かない」コードに当たり、`:no`を出してしまいます。Rigorの最上位価値（脅かさない）に反します。
3. **境界の存在**：RubyにはRBSという*宣言の境界*があります。推論で全部埋めるより、「型のある所（RBS）は引く、無い所は控えめに推論し、最後は`untyped`に逃がす」方が、現実に合います。

だから方針は**「自明な範囲だけ推論する」**です。`id`のような恒等は`(X) -> X`、`n + 1`のような明らかな使われ方は能力で絞る。でも怪しければ`untyped`のままです。これは『しくみ』9章演習の助言（「自明なケースに限定して推論するとよい」）と同じ立場です。

> **Note**
>
> **HMが使えない理由は1つではない**
>
> 「なぜ完全なHMを使わないのか」に対して「遅いから」「誤検知が増えるから」と答えることもできますが、型理論の言葉では3種類の**別々の問題**がそれぞれ別の対処を必要としています。
>
> **① 決定不能性（decidability problem）**
> ここで「ランク」とは、関数の*引数側*に多相`∀`がどれだけ深く入れ子になるかの段数です（ランク1＝`∀`は先頭にだけ、というHMの世界。引数の引数の…と`∀`が潜るほど上がります）。HM本体（ランク1）の推論は決定可能、ランク2までも決定可能で、**ランク3以上の多相型推論は決定不能**です（Kfoury–Wells 1994）。なおWells 1994/1999は、ランクを問わない*無制限* System Fの型付け可能性そのものが決定不能であることを示しました。HMを超えて高階の多相へ踏み込もうとすると、「この推論は原理的に終わらない」領域に入ります。対処：型変数の使用に制限を設ける（ランク1に留める、局所に絞る）か、`untyped`でそもそも問わない、です。
>
> **② 到達不能性（reachability problem）**
> `define_method`や`method_missing`、マクロ展開など、ASTだけでは「何が定義されるか」を読めない構造がRubyには多くあります。いくら制約を集めても、存在を知らないメソッドの型は求められません。対処：プラグイン（ADR-2、16）が「ASTの外の知識」を補います。
>
> **③ 精度問題（precision problem）**
> 朴訥なjoin（型の合流）は広い型を生みます。`foo(1)`と`foo("a")`を両方見た後、引数を`Integer | String`に合流させても、実際には「どちらかだけ渡す呼び出し元は別々」なので無用に広くなります。対処：meet/joinを最小限に抑え、残りは`untyped`にdegradeします。
>
> chibirigorの「引数は`untyped`」という判断は、この3つをまとめて回避する最も保守的な答えです。Rigorの推論を「局所とカタログ」に絞るのも、同じ3問題への同じ答えです。

---

## 5-4a. TypeProfとの対比　whole-program vs local+catalog

「なぜ全部やらないか」の答えを鮮明にするために、Rubyの公式型推論ツールである**TypeProf**と比べます。TypeProfは*mametter（TypeProf作者）*が設計した、Rubyコアに同梱された型レベル抽象インタプリタです（詳細：Rigorハンドブックappendix-typeprof）。

> **Note**
>
> **TypeProfのやり方　whole-program抽象解釈**
>
> TypeProfはプログラムを入口から「型レベルで実行」します。メソッド呼び出しを見つけると、*呼び出し元*から引数の抽象型を追いかけて呼び先の本体を解釈し、戻り型を逆算します。これを繰り返すことで、注釈ゼロのコードから`def foo: (Integer) -> String`のようなRBSを生成できます。呼び出し元を見るので**引数型をcall siteから推論できる**のが最大の強みです。

やっていること（呼び出し元から引数型を起こす）の*方向*は前節の「道B」と同じですが、TypeProfの*やり方*は型変数と制約の単一化ではなく、**プログラムを型レベルで抽象実行すること**です（HMの単一化とは別系統）。全プログラムを同時に解釈するので、規模が大きくなると組合わせ爆発が起きやすく、TypeProf自身が「小規模ファイル、プロトタイプ用途向け」と位置付けています。

> **Note**
>
> **Rigorのやり方　local+catalog**
>
> Rigorは**1メソッドずつ**推論します。別メソッドを呼び出す箇所では、本体を再解釈するのではなく、事前に用意した**カタログ**（コア、stdlib、gemのRBS、プラグイン貢献）から戻り型を引きます。解けない引数は`Dynamic[Top]`（= `untyped`）に落として打ち切り、**推論予算**でコスト上限を確保します（Part 6のキャッシュも効く）。全コードベースを毎pushで走らせることが目標なので、スケールを最優先にしています。

| | TypeProf | Rigor |
|---|---|---|
| 解析の単位 | プログラム全体（入口から） | 1メソッドずつ |
| 他メソッドの戻り型 | 本体を再解釈 | カタログを参照 |
| 引数型をcall siteから推論？ | **できる**（最大の強み） | しない（`untyped`がデフォルト） |
| スケール目標 | 小ファイル、プロトタイプ用 | 全コードベース、CI常時実行 |
| 主な出力 | RBSシグネチャ（エラーは副産物） | 診断（確実なバグのみ、FPゼロ主義） |

前節で「引数推論を自明な範囲だけに抑える」と言ったのは、この対比が理由です。TypeProfのwhole-program方式は精度は高いが規模に弱く、Rigorは局所とカタログで規模を優先し、解けない所は素直に`untyped`にします。**同じ「引数を推論する」課題を、スケールとFPゼロという別の価値観で解いた2つの答え**です。

なお`rigor sig-gen`（Chapter 11）はTypeProfと同じ仕事（注釈ゼロからRBSを生成する）をこなしますが、引数型の扱いは「観測されたcall siteをデフォルトにしない」方針（ADR-5）が異なります。TypeProfが見た型をそのまま出すのに対して、Rigorは「この引数がそれしか受けない」を固めてしまわず、`untyped`のまま人間に委ねます。

---

## 5-5. 双方向で見ると

Part 1の地図で言えば、引数推論は**合成`⇒`の守備範囲を広げる**作業です。前編は引数で`⇒`を諦めて`untyped`を返していました。後編は、本体の使われ方（道A）や制約（道B）を使って、その`⇒`を*できる範囲で*埋めます。埋まらない所は素直に`untyped`です。双方向の枠組みはそのままで、`⇒`の精度だけが上がります。

精度が上がっても診断は増えない点も変わりません。引数の型が`untyped`から`{name: () -> String}`に絞れても、それは*合成側*の話です。診断は依然として照合`⇐`の位置（RBSの宣言がある所）でしか出ない。Part 1で見た「脅かさない」の構造は、推論を足しても壊れません。

---

## 5-6. Rigorの中では

- **capability role**：`_ToS`、`_Each[T]`、`_Reader`などの能力ロールが、道Aの「集めた能力」の実体です
  - 構造的インターフェースとして受理判定に使われます
- **ジェネリクス具体化**：呼び出し地点で型変数を実引数から束縛します（道Bの単一化の限定版）
  - ブロックの戻り型から型変数を解くなど
- **fail-soft**：解けない型変数は`Dynamic[Top]`（＝`untyped`）にdegradeします
  - 前編の「埋まらねばuntyped」と同じです

---

## 5-6x. 発展：ブロック仮引数への押し下げはlibに入った（generics 5b、5c）

道Bの核（要素型`Elem`をブロック仮引数へ流し込む）は、chibirigor本体に昇格しました（`lib/chibirigor/type_of.rb`の`type_of_block`）。後編Part 3「3-6x」の**読み（5a）**に続く**押し下げ（5b）**で、genericsの読みと押し下げがlibでひとつながりになります。要素が*未知の型変数*の一般ケースを解く本格的な単一化（§5-3）は、なお設計スケッチのままです（道A、Bの「全部はやらない」§5-4の判断）：

```console
$ printf '[1, 2].map { |x| x + 1 }\n[1, 2].map { |x| x.to_s }\n[1, 2].select { |x| x }\n' | ruby exe/chibirigor annotate /dev/stdin
1: Array[Integer]
2: Array[String]
3: Array[Integer]
```

`map`のブロック仮引数`x`が**要素型`Integer`**に束縛され、本体`x.to_s`が`String`だから`map`の戻りは`Array[String]`です（戻り値も要素型つきの配列になる、つまり**戻り多相**です。これが5c）。ブロック本体は`x : Elem`のもとで**型チェックされます**。だから`[1,2].map { |x| x + true }`は「can't add true to an Integer」を1件出します（押し下げが効いている証拠）。`each`はレシーバ（self）を返し、`select`、`reject`は要素型を保ちます。

ここで使ったのは**単一化ではなく直接代入**です。chibirigorの配列は要素型が*具体*（`Tuple`か`Array[Elem]`）なので、`x := Elem`はまさに §5-3の単一化の**自明な特例**です。制約が`[[X, Integer]]` 1本だけ（右辺`Elem`がground＝自由変数を含まないので、単一化が**代入に退化**する）という場合に相当します。`solve`を呼ぶまでもなく束縛が決まるので、配管を増やさず直接代入で済ませました（最小、予算優先）。`examples/unification.rb`の**本格的な制約解き**が要るのは、要素型が*未知の型変数*で、ブロックの使われ方からそれを*逆算*する一般の場合です。そこは設計スケッチのままにしてあります（道A、Bの「全部はやらない」§5-4の判断）。

誤検知ゼロも不変です。空配列`[].map { ... }`は要素が`untyped`なので本体も`untyped`になり、未知レシーバ`foo.map { ... }`は「配列と決めつけない」ので本体を検査せず`untyped`に倒します。

## 5-7. まとめ

- 戻り型は合成で出ますが、引数は「使われ方の逆算」が要ります
  - 推論の難所です
- 道A：能力（capability/duck）を集めて構造的インターフェースにします
  - 確実なメッセージだけを対象にします
- 道B：型変数、制約、単一化（型再構築、HMの骨子）を使います
  - 残った変数はジェネリックになります
- **全部はやらない**：自明な範囲だけです
  - 怪しければ`untyped`のまま（決定性、誤検知、RBS境界のため）
  - TypeProf（whole-program抽象解釈、call siteから引数推論）とは設計を分けた意図的な選択です
- 推論を足しても、診断は照合位置でしか出ません
  - 脅かさない構造は不変です

## 演習

1. **単一化をトレース**：`examples/unification.rb`で`solve([[X, Integer], [Y, X]])`を手でたどり、最終的な`subst`を書け（`X`と`Y`がそれぞれ何に解けるか）。
2. **道Aで能力を集める**：`def f(x); x.name + "!"; end`から、`x`に要求される能力（構造的インターフェース）を書き出せ。`x.name`の戻りに付く制約も一言で。
3. **なぜ全部やらないか**：`def g(x); x; end`を「大域HMで型を解く」のと「引数＝`untyped`に倒す」のとで、`g(foo.bar)`の呼び出しに対する診断の出方がどう変わるかを述べよ（誤検知の観点で）。

**次章（Part 6）**：ナローイングで積んだ事実を貯め、再代入や副作用で*無効化*しながら持ち回る完全な**FactStore**へ拡張する。6バケツ、stability、joinで、フロー感応な絞り込みを実装する。

---

> **この章の設計スケッチ** → [`examples/unification.rb`](https://github.com/rigortype/chibirigor/blob/master/book/v2/ja/seasoned/examples/unification.rb)（`ruby unification.rb`で自己チェック）