Part 5　本物の型推論：引数を埋める

参考書（任意）：『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が何に応えられるか」が本質です。だから引数を、具体的な型ではなく能力（インターフェース）として推論します。

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

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の骨子です。

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

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です。型変数TVarと基底型TConだけの世界で、単一化はこれだけです：

# 代入 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になる、が緑になります：

PASS: id has no constraint (X stays generic)
PASS: inc resolves N to Integer from n + 1
PASS: conflicting constraints raise UnifyError

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

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

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

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

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）。

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

	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の判断）：

$ 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から引数推論）とは設計を分けた意図的な選択です
推論を足しても、診断は照合位置でしか出ません
- 脅かさない構造は不変です

演習

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

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

この章の設計スケッチ → examples/unification.rb（ruby unification.rbで自己チェック）

Part 5 本物の型推論：引数を埋める