Part 1　双方向型付けの正体

後編の最初の章です。後編は「作る」より「読み解く」巻で、前編で無意識に作っていた仕組みに正式な名前を与え、その裏側を形式の言葉で読み解きます。この章はほとんど新しいコードを書きません。既に書いたものが、実は何だったのかを明かす総論（地図）です。ただし終わりに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本の矢印です：

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

図1-1　合成⇒と照合⇐

▼ 図1-1　合成⇒（下から上へ型を作る）と照合⇐（上の期待型に突き合わせる）

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. なぜ診断は照合（`⇐`）でしか出ないのか

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

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

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

合成⇒がわざと失敗しない（chibirigor固有）。双方向型付けの一般的な定義では、未束縛変数や合成不能な構文で合成は失敗し得ます。chibirigorは意図的に、未知をすべてuntypedに合成して全域化しています。だから「型を見失った式」が⇐位置に来ても、合成結果はuntypedです。
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は、この三者の最小版でした。後編は、この骨格に肉を付けていきます。

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つだけです。照合⇐がどこに診断の口を開けるかを見るための小窓です。

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抜粋）

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

# ⇐ 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（推論が型を見失ったとき）でも照合しない。これで「動くコードを脅かさない」は戻り型チェックでも守られます。

param:ディレクティブが担う2つの仕事

Rigorには、RBSの拡張アノテーション%a{rigor:v1:param: name is String}で書くparam:ディレクティブがあります（.rb本体にはインラインで書けず、RBS側に置きます）。これは同時に2つの効果をもたらします：

本体ナローイング（⇒側に型の出発点を与える）：本体内でnameの型が宣言されたStringから始まる。is_a?を書かなくても最初から宣言型で推論が進む。
呼び出し地点の⇐照合：greet(42)のような呼び出しで、引数型が宣言と合うかacceptsで照合し、:noなら診断を追加する。

つまりparam:は「書いた人への約束（本体は型に沿う）」と「呼ぶ人への約束（引数を守れ）」を同時に担う。どちらも⇐（照合）として統一されているのが双方向型付けのきれいな点です。

演習

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

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