付録 a4　参考書と ADR の対応早見表

ヒント

この付録は「任意の道しるべ」です。必読ではありません。 本書（前編、後編）は、参考書を1冊も開かなくても単独で完結します。ここは、各章の脇に散らばっていた「この話は『しくみ』の何章、『TAPL』の何章にあたるか」「本文のこの緊張はRigorのどのADRが解いているか」という対応情報を、一覧で引けるよう1つにまとめた参照表です。必要な所だけ拾ってください。

---

a4-1. 書誌

参考書（2冊）

• 『しくみ』：遠藤侑介『型システムのしくみ ― TypeScriptで実装しながら学ぶ型とプログラミング言語』（ラムダノート）
  • 『TAPL』のエッセンスをやさしく蒸留した入門書で、型注釈付きのミニ言語に対するチェッカーをTypeScriptで作る
  • 注釈を前提にする点で、推論を土台にするchibirigorとちょうど裏表の関係にある
  • 日本語のみ
• 『TAPL』：Benjamin C. Pierce『型システム入門 ― プログラミング言語と型の理論』（オーム社。原著Types and Programming Languages, MIT Press）
  • 本格的な教科書で、各話題に本式の証明がある
  • 英語で読むなら原著がそのまま参照先になる

道しるべの濃淡（前編と後編で違う）

• 前編The Little chibirigor：参考書は任意
  • 各章は参考書ゼロで完結する
  • 『しくみ』がやさしい裏面として最も近く、対応章を脇に添えてある
• 後編The Seasoned chibirigor：『TAPL』を一次の道しるべに据える（変性、再帰型、System F、健全性は『TAPL』の章立てに沿って進む）
  • 『しくみ』は要所で併走するが、後編が踏み込む領域（本物の型推論、FactStore）には対応章がない

RigorのADRとspec

• ADR（Architecture Decision Record）：Rigorの設計判断記録。リポジトリのdocs/adr/にある
  • 「なぜopen classを許すか」「なぜRactorでなくforkか」といった判断が物語として残る
• 内部仕様（spec）：inference-engine.md等。ADRが「なぜ」なら、specは「どう」を書く

ノート

型システムそのものの対応章は『しくみ』と『TAPL』に、Rigor固有の工学上の判断はADRにあります。後編Part 8が「最小版から実用ツールへ」の橋としてADRへの入口をまとめており、a4-4はその表を引いています。

---

a4-2. 前編　章 × 『しくみ』章 × 『TAPL』章

v1の新章立て（前編Part 0〜9）で並べます。参考書はどちらも任意で、一次の近さは『しくみ』側です。

v1章	テーマ	『しくみ』	『TAPL』	関係（一言）
0	はじめに（推論を土台にした型チェッカー）	1章	1章、8章 §8.3	対比（健全vs誤検知忌避）
1	リテラルと算術	2章	8章	ほぼ対応（精度はConstで上回る。type_of＝typecheck）
2	メソッド送信とディスパッチ	3章	9章	読み替え（関数 → メソッド、{params, retType}）
3	ローカル変数と不変Scope	3、4章	9、11章 §11.5	対応（tyEnv → 不変Scope、let束縛）
4	Union　型が一本に決まらない	（対応章なし）	11章 §11.10	独自地形（無タグのユニオン型。両書はタグ付きのみ）
5	ナローイング　場合分けで絞る	（対応章なし）	（対応章なし）	独自地形（gradual、フロー感応）
6	ハッシュと配列の型	5章	11章 §11.8、§11.7	対応（ただしopen vs完全一致で逆向き）
7	受理判定と三値	7章	15章	対応＋三値、consistency拡張
8	RBSと型シグネチャ	9章、9章演習、おわりに	23章、22章	部分対応（型代入の遠縁→戻り型合成。『しくみ』の空白を埋める）
9	gradualの哲学	おわりに	8章 §8.3の先	接続（健全性の本式、その先のgradual）

ノート

『しくみ』と『TAPL』がそのまま扱わなかった領域（無タグUnion、三値、gradual、フロー感応なナローイング）が、chibirigorが先に進めた部分です。前編Part 4、5に対応章がないのはそのためです。

---

a4-3. 後編　章 × 『しくみ』章 × 『TAPL』章

v1の新順序（後編Part 1〜8）で並べます。後編は『TAPL』を一次の道しるべに据えます。

v1章	テーマ	『TAPL』	『しくみ』	関係（一言）
1	双方向型付けの正体	9章	3章	土台（単純型付きラムダの型付け規則。⇒、⇐）
2	部分型と変性	15、16章	7章	対応（width/depth、変性、アルゴリズム的部分型付け）
3	ジェネリクスと型代入	23章、22章、26章、29章	9章	対応（System Fの型適用、α 変換、有界量化）
4	再帰型：μ と余帰納	20、21章（HKTは29章）	8章	対応（同値再帰、余帰納＝最大不動点。HKT別解は別根拠）
5	本物の型推論：引数を埋める	22章	9章演習、おわりに	前線（型再構築、制約、単一化。『しくみ』が解答を放棄した所）
6	完全なFactStore	（対応章なし）	（対応章なし）	独自地形（データフロー解析の一般論。型理論の教科書に章なし）
7	健全性と正規化、わざとunsound	8章 §8.3、12章	おわりに	中心定理（進行＋保存、正規化）を据え、なぜunsoundかを語る
8	本物のRigorへ	（対応章なし）	（対応章なし）	橋（学習用最小版 → 実用ツール。対応はADR群、spec）

ノート

後編Part 6（FactStore）とPart 8（Rigorへの橋）は、型理論の教科書に対応章がない独自地形です。後編が『TAPL』を超えて踏み込む工学の層がここに当たります。

---

a4-4. 本文が参照する主なADRの早見

後編Part 8がADRへの入口をまとめています。ここはその表を引いて一覧化したものです。番号と一言だけ添えます（詳しい文脈は後編Part 8 §8-2、§8-3を参照。本文の章番号はv1の新章立て）。

まず全体像をつかむ2本

ADR	一言
ADR-0	基盤と設計原則の出発点（あとの全ADRの地図）
ADR-4	型推論エンジンの仕組み

本文の緊張に対応するADR（後編Part 8 §8-3）

ADR	一言	本文での対応
ADR-5	ロバストネス原則（誤検知をどう避けるか）	前編Part 4、7、後編Part 7（わざとunsound）
ADR-22	baselineとオンボーディング	前編Part 9（baseline本体）
ADR-20	軽量HKT（還元fuelで再帰を止める。実装済み）	後編Part 4（fuel）、Part 7（予算）
ADR-41	推論予算の設計（Status: Proposed、未実装）	後編Part 7（予算）
ADR-14	sig-gen（シグネチャ生成）	前編Part 8、後編Part 3（erasure）
ADR-25	プラグインRBS	前編Part 8
ADR-32	inline RBS	前編Part 8
ADR-46	増分解析（ファイル横断の依存グラフ）	後編Part 8 §8-2（工学）

実用ツールが足す工学のADR

拡張API、インターフェース分離、マクロ展開、Data/Struct折りたたみ、永続キャッシュ、LSP同梱、CI出力形式、並行解析、性能ゲートといった工学寄りのADRは、後編Part 8 §8-2に一覧があります（前編の本文では名指ししません）。

ノート

読み進める順は、興味のある行のADRを1本開くのがいちばん早い方法です。どれも「なぜそう設計したか」が物語として書かれています。型推論エンジンの内部仕様はinference-engine.mdです。

---

a4-5. この付録の使い方

• 型理論をもう一段覗きたい → a4-2、a4-3で対応章を引き、手元の『しくみ』か『TAPL』を開く
  • どちらも持っていなくても本書は完結します。
• 本物のRigorを読みたい → a4-4から、いちばん気になる行のADRを1本開く
  • ADR-0からADR-4が全体の地図になります。
• 本文に戻る → 各章末の1行ポインタからここへ来た場合、表で位置を確かめたら章へ戻ってください
  • 早見表は道しるべであって、本筋ではありません。