付録 a3 道具（実 Rigor の CLI と dispatch カスケード）
これは参照付録です。本書（chibirigor）は「動く最小版」を手で作るのが主目的なので、本編の各所では実物のRigorのツール挙動を1行ポインタで送りました。その送り先がここです。chibirigorの最小版と実Rigorの差を「本書では素朴／実物はこう」という橋渡しで並べます。
ここに書くRigorの事実記述は本編の原稿と一致させています（5段の順序、名称は原稿どおりです）。本書のコード挙動を変える記述ではありません。
a3-1. rigor check --explain（fail-softの地図を出す）
Section titled “a3-1. rigor check --explain（fail-softの地図を出す）”通常のrigor checkは、証明できた問題だけを診断として報告し、Dynamic[Top]（本文の最小版Dynamicの内部表記＝untyped。付録a1-1参照）にfail-softした箇所については黙っています（前編Part 2「知らなければ黙る」、Part 9「わざと見逃す」の実物です）。これは誤検知を出さないための態度ですが、裏を返せば「静かに見逃している」でもあります。
--explainを付けると、そのfail-softした全箇所が:info診断として現れます。「ここで型を見失いました」という地図が出力されます。
$ rigor check --explain app/models/user.rbapp/models/user.rb:42:7: info: fell soft to Dynamic[Top] here (RBS not found for `external_call`)app/models/user.rb:51:3: info: fell soft to Dynamic[Top] here (param `opts` is untyped)使い道はこうです：
- 「このバグを見落としているのでは？」という疑問が出たとき、
--explainの出力で「どこで型が消えたか」を遡る。 - たどり着いたfail-soft地点から、RBSの不足、プラグイン未設定、型注釈の抜け漏れを発見できる。
なぜ「地図」が描けるのか（Dynamic[Top]マーカーの回収）
Section titled “なぜ「地図」が描けるのか（Dynamic[Top]マーカーの回収）”この一覧が成り立つのは、前編Part 1で触れたDynamic[Top]のDynamicマーカーが、fail-softした箇所に消えずに残っているからです。untypedを「ただの穴」ではなく「Dynamicという印の付いたTop」として持つことで、「どこで黙ったか」が構造として残ります。だからこそ、後から--explainで一覧に起こせます。
| 本書（chibirigor） | 実物（Rigor） | |
|---|---|---|
untypedの正体 | Type::Dynamic（印だけ） | Dynamic[Top]（TopにDynamicマーカー） |
| fail-soft地点 | 黙ってDynamicを返すだけ | 地点を構造に保持し、--explainで一覧化 |
| 沈黙の可視化 | 仕組みなし（最小版の対象外） | check --explainが:info診断で地図を出す |
chibirigorの「知らなければ黙る」は誤検知を防ぎますが、--explainはその沈黙そのものを可視化する道具です。
a3-1x. 発展：chibirigorにも極小--explainがある
Section titled “a3-1x. 発展：chibirigorにも極小--explainがある”上の表は本書を「沈黙の可視化＝仕組みなし」としていますが、ここにも極小版を足しました。check --explainを付けると、推論がuntypedに倒した地点（未知メソッドのディスパッチ）を:info診断として併せて出します：
$ printf 'x = mystery_call\ny = x + 2\n' > demo.rb$ ruby exe/chibirigor check --explain demo.rbdemo.rb:1:5: info: fell to untyped here (can't look up the type of `mystery_call`) x = mystery_call ^^^^^^^^^^^^demo.rb:2:5: info: fell to untyped here (can't look up the type of `+`) y = x + 2 ^^^^^注目したいのは2行目です。mystery_callの型がわからずxがuntypedになり、そのxに対する+も型を引けずにuntypedへ倒れています。沈黙が伝播していく様子が地図に出ます。--explain無しなら（誤検知を出さないので）No type errorsと黙るだけです。:infoは終了コードを汚さない（exit 0）ので、CIを止めずに「どこで型が消えたか」だけ覗けます。
実物との差は、実RigorがDynamic[Top]のDynamicマーカーを構造に保持してあらゆるfail-soft（RBS不足、未注釈引数、プラグイン未設定など）を一覧化するのに対し、chibirigorが拾うのは未知ディスパッチ1種だけ、という点です（実装はlib/chibirigor/dispatch.rbのsignatureがnilの枝でprovenanceを1行積むだけです）。沈黙を地図にするという発想は同じです。
a3-2. Rigorの型表示（内部の精密型とRBS境界の保守型）
Section titled “a3-2. Rigorの型表示（内部の精密型とRBS境界の保守型）”本書のannotateは、推論した型を1つそのまま見せます。実Rigorもannotate（本書と同じ名前の道具です）やエディタのhoverで型を見せますが、実物には本書に無い二段構えがあります：
- Rigor内部での精密な型（例：
Constant<"FOO">）。 - RBSの境界で粗い型に落とした後の保守的な型（例：
String）。
chibirigorのannotateは内部型だけを見せます。実物は「内部では精密に知っているが、境界では捨てる」という二重構造を持つので、「推論はもっと知っていそうなのに、シグネチャ（RBS）はなぜこんなに粗いのか」という状況が起こります。その答えが、この二段構えです。
| 本書（chibirigor） | 実物（Rigor） | |
|---|---|---|
| 型の見せ方 | annotateが行単位で内部型を並べる | annotate／hoverで見せ、境界ではerasureで丸める |
| 見せる型 | 内部型1つ | 内部の精密な型、境界で丸めた保守的な型の二段 |
| ズレの正体 | （境界が無いので起きない） | 内部精密型とRBS境界型の食い違い（erasure） |
そしてchibirigorもdump_typeを基本機能として持っています。道具はcheckとannotateの2つに絞ったままです。これはコマンドではなく、checkが認識する式です。includeも要らず、dump_type（式）と書いてcheckするだけです：
$ printf 'x = c ? 1 : "a"\ndump_type(x)\n' > demo.rb$ ruby exe/chibirigor check demo.rbdemo.rb:2:1: info: dump_type: 1 | "a" dump_type(x) ^^^^^^^^^^^^:infoなので診断は赤くならず（終了コードは0）、本物の型エラーと一緒に出しても邪魔をしません。仕組みは前編Part 9で作った:info診断そのままです。type_ofがdump_type（式）を見つけたら、引数の推論型を:info診断に記録し（checkがそれを表に出します）、値はそのまま返します（だからdump_type(x)の型はxの型のままです）。実装はlib/chibirigor/type_of.rb、挙動の網羅はtest/test_dump_type.rbです。
a3-3. dispatch 5段カスケード（表引きの実物）
Section titled “a3-3. dispatch 5段カスケード（表引きの実物）”前編Part 2は、メソッド送信の型付けを素朴な表引き一段に留めました（（クラス,メソッド）でMETHODS表を引き、見つかれば戻り型、見つからなければuntyped）。実物のRigorは、この「表引き」を5段のカスケードにしています。上の段から順に当て、その段が当てられなければ次の段へ落ちます（fall through）。各段が何を解決し、外れたら何に渡すかを示します：
| 段 | 名前 | 何を当てるか | 外れたら |
|---|---|---|---|
| ① | 定数畳み込み | 1 + 2のように両辺が既知の定数なら、その場で実際に計算して結果の型（3）を出す | ② へ |
| ② | shape dispatch | HashShapeのキー読み出しなど、型の構造に直接触れる操作を構造から直接解く | ③ へ |
| ③ | RBS | コア、stdlib、プラグインが提供するRBSの型で引く（本書の手書きMETHODS表の実物） | ④ へ |
| ④ | in-source（本体推論） | RBSに無いメソッドは、本体を推論して戻り型を合成する（前編Part 8の戻り型合成の実物） | ⑤ へ |
| ⑤ | fallback | どの段でも当たらなければDynamic[Top]にdegrade（脅かさない） | （ここで止まる） |
流れの読み方
Section titled “流れの読み方”ひとつの呼び出しは、上から順に「この段で解けるか？」を問われ、解けた段で打ち止めになります。解けない段は黙って次に渡すだけです。誤検知を出さず、最後は必ずDynamic[Top]で受けるので、未知の呼び出しでも止まりません（前編Part 2「知らないメソッドは脅かさない」の実物です）。
receiver.method(args) │ ▼ ① 定数畳み込み ── 当たる ─→ 結果の型（例: 3） │ 外れ ▼ ② shape dispatch ─ 当たる ─→ 構造から直接解いた型 │ 外れ ▼ ③ RBS ────────── 当たる ─→ RBS 由来の戻り型 │ 外れ ▼ ④ in-source ──── 当たる ─→ 本体推論で合成した戻り型 │ 外れ ▼ ⑤ fallback ───────────────→ Dynamic[Top]（untyped）優先順位が効く例（なぜ ③ が ④ に勝つか）
Section titled “優先順位が効く例（なぜ ③ が ④ に勝つか）”カスケードは順序そのものが意味を持ちます。たとえばRBS::Extendedディレクティブで宣言した型が、メソッド本体の推論に勝つのは、③ RBSが ④ in-sourceより先に当たるからです。「宣言を本体に優先する」という設計判断が、段の並び順として表れています。
| 本書（chibirigor） | 実物（Rigor） | |
|---|---|---|
| dispatchの段数 | 1段（METHODS表を引くだけ） | 5段（① 定数畳み込み、② shape、③ RBS、④ in-source、⑤ fallback） |
| 表の中身 | 手書きのMETHODS Hash | ③ がRBS（コア、stdlib、プラグイン由来） |
| 本体推論 | annotateで別途（前編Part 8） | ④ in-sourceとしてdispatchに組み込み |
| 未知の扱い | Dynamicを返す | ⑤ fallbackでDynamic[Top] |
| 宣言vs推論の優先 | （区別なし） | 段の順序（③ が ④ より先）で表現 |
a3-3b. rigor trace（推論の手順をコマ送りで見る）
Section titled “a3-3b. rigor trace（推論の手順をコマ送りで見る）”ここまでの道具（--explain、型表示の二段構え、カスケード）は、推論の答えや地図を見せるものでした。実Rigorにはもう一つ、推論の手順そのものを見せる道具があります。rigor traceです。checkが走らせるのと同じ推論をファイルに対して再走させ、記録した推論イベントを端末のコマ送りアニメーションとして再生します。1コマ＝推論の1場面で、ローカルがscopeに入る瞬間（bind）、分岐の型が1つのunionに溶ける瞬間（union）、メソッド送信が解決する（またはDynamic[top]にfail-softする）瞬間（dispatch）を、評価される範囲をハイライトしながら見せます。
rigor trace lib/example.rb # キー押しでコマ送りrigor trace --delay=0.5 lib/example.rb # 自動再生rigor trace --format=json lib/example.rb # 生のイベント列--verboseは式ごとのenter/resultまで全部出し、既定では上の3種の「教えどころ」だけに絞ります。JSONのイベント列は安定しているので、教材の図や講義資料の素材にできます。
a3-3bx. 発展：chibirigorにも極小traceがある
Section titled “a3-3bx. 発展：chibirigorにも極小traceがある”これは付録の中でも珍しく、本書側にも実物とほぼ同じ道具がある節です（実装はlib/chibirigor/tracer.rb）。本書で各Partを写経して作った部品（scopeへの束縛、Type.unionの畳み込み、dispatchの表引き）が、動く順番で目の前を流れていきます。読者が「評価順はこうだろう」「ここでunionになるはず」と頭の中で組み立てた推論を、目で確かめるための学習用の道具です。
3行の例で動かしてみます。代入、三項演算子、メソッド呼び出しを1つずつ含みます：
$ printf 'x = 5\ny = x > 0 ? 1 : -1\nz = y + 2\n' > demo.rb$ ruby exe/chibirigor trace demo.rb端末では1コマずつEnterで送ります（qで終了）。全17コマのうち、要点のコマだけ抜き出すと：
chibirigor trace ─ step 2/17──────────────────────────────────────────────────────────────── 1 x = 5 2 y = x > 0 ? 1 : -1 3 z = y + 2────────────────────────────────────────────────────────────────type env : x: 5evaluating : (top level)► bind: x ← 5 (added to type env)…chibirigor trace ─ step 5/17…type env : x: 5evaluating : if (incl. ternary) › call to >► dispatch: 5.>(0) → untyped (not in table → fail-soft to untyped)…chibirigor trace ─ step 7/17…evaluating : if (incl. ternary)► union: 1 , -1 → 1 | -1…chibirigor trace ─ step 9/17…type env : x: 5 y: 1 | -1evaluating : (top level)► bind: y ← 1 | -1 (added to type env)…chibirigor trace ─ step 12/17…evaluating : call to +► dispatch: 1.+(2) → 3 (constant folding)chibirigor trace ─ step 13/17…► dispatch: -1.+(2) → 1 (constant folding)chibirigor trace ─ step 14/17…► union: 3 , 1 → 3 | 1chibirigor trace ─ step 15/17…► dispatch: 1 | -1.+(2) → 3 | 1 (distribute Union to members)…chibirigor trace ─ step 17/17…type env : x: 5 y: 1 | -1 z: 3 | 1evaluating : (top level)► bind: z ← 3 | 1 (added to type env)
── playback done (17 steps total) ──この17コマで、本編の部品が動く順に並びます。xの束縛（step 2）から、三項の条件x > 0が表に無い>なのでfail-softでuntypedに倒れ（step 5）、2本のアーム1と-1がunionに溶けてyに束縛され（step 7、9）、y + 2はyが1 | -1なのでメンバへ分配して各メンバを定数畳み込みし（step 12、13）、結果をまたunionでまとめて（step 14、15）zを3 | 1に束縛する（step 17）という流れです。各Partで別々に作った仕組みが、1つの式でどう連動するかが一望できます。--verboseを付ければ、間引いた式ごとのenter/resultも全部出ます。JSONで出したいときは--json、自動再生は--delay 0.5です。
仕組みは実物と同じ発想で、コアには一切手を入れていません。type_of、eval_statement、Type.union、Dispatch.dispatchにModule#prependでフックを差し込むだけで、レコーダがnil（トレース中でない）ときフックは即superします。だからcheckやannotateの挙動は変わらず、本編で写経したコードを1行も汚しません（tracer.rb冒頭コメント参照）。
| 本書（chibirigor） | 実物（Rigor） | |
|---|---|---|
| 見せるもの | 推論イベントのコマ送り（bind、union、dispatch） | 同じ（推論のderivationを再生） |
| コアへの干渉 | Module#prependのフック、レコーダnilなら即super | checkと同じ推論に乗る記録から再生する探針 |
| 出力形式 | 端末アニメーション、--json、--verbose、--delay | 端末アニメーション、--format=json、--verbose、--delay、--line |
実物が--line=Nで1行だけに絞れるのに対し、chibirigorは行フィルタを持たない、といった枝葉の差はありますが、推論の手順を再生して見せるという発想と3種のイベントは同じです。本書の他の道具が「Rigorの実物から極小版」だったのに対し、traceは珍しく本書側がほぼ実物と同型で並びます。
a3-4. まとめ（「素朴／実物」対応の早見）
Section titled “a3-4. まとめ（「素朴／実物」対応の早見）”本付録で橋渡しした4つを一枚に：
| 仕組み | 本書での扱い | 実物の挙動 | 戻りポインタ |
|---|---|---|---|
rigor check --explain | 極小版あり（未知ディスパッチを:info地図化、§a3-1x） | Dynamic[Top]マーカーを手がかりにfail-soft地点を:infoで地図化 | 前編Part 9 |
| 型表示の二段構え（erasure） | annotateは内部型1つ（境界が無いのでズレない、§a3-2） | annotate／hoverの裏で内部精密型とRBS境界型をerasureで丸める | 前編Part 1 |
rigor trace file | ほぼ実物と同型の極小版あり（bind、union、dispatchをコマ送り、§a3-3bx） | 推論の手順を端末アニメーションで再生（--verbose、--line、--format=json） | （なし） |
| dispatch 5段カスケード | 1段の表引き（METHODS、極小版は設けず） | ① 定数畳み込み、② shape、③ RBS、④ in-source、⑤ fallback | 前編Part 2 |
いずれも、本書で手作りした骨格（Dynamicマーカー、annotate、METHODS表）が、実Rigorでは同じ骨格を拡大した形で動いている、という対応で読めます。
© 2026 TypedDuck. Licensed under CC BY-SA 4.0.