Appendix a4 — Reference & ADR correspondence table

Tip

This appendix is an “optional signpost.” It is not required reading. This book (both volumes) stands on its own without opening a single reference book. This is a reference table that gathers, into one place, the correspondence information scattered beside each chapter — “this topic corresponds to which chapter of『しくみ』 / TAPL,” “which ADR of Rigor resolves this tension in the text” — so you can look it up at a glance. Pick up only the parts you need.

---

a4-1. Bibliography

Reference books (two)

• TAPL — Benjamin C. Pierce, Types and Programming Languages (MIT Press). The full textbook, with proper proofs for each topic. For English readers, the original is the reference.
• 『しくみ』 (The Mechanics of Type Systems) — Yusuke Endoh, Learning Types and Programming Languages by Building Them in TypeScript (Lambda Note). A gentle distillation of TAPL’s essence that builds a checker for an annotated mini-language in TypeScript. In presupposing annotations, it is exactly the mirror image of chibirigor, which builds on inference. Published in Japanese only — where it is the sole correspondence and no English equivalent exists, the text says so plainly.

Different weight of signposts (the two volumes differ)

• The Little chibirigor — references are optional. Each chapter is complete with zero references. 『しくみ』is the closest, as a gentle mirror image, with corresponding chapters noted in the margin (Japanese readers only).
• The Seasoned chibirigor — sets TAPL as the primary signpost (variance, recursive types, System F, soundness proceed along TAPL’s chapter structure). 『しくみ』runs alongside at key points, but the areas the Seasoned volume steps into (real type inference, the FactStore) have no corresponding chapter in it.

Rigor’s ADRs / spec

• ADR (Architecture Decision Record) — Rigor’s design-decision records, in the repository’s docs/adr/. Judgments like “why allow open classes,” “why fork rather than Ractor” remain as a narrative.
• Internal spec — inference-engine.md and others. If an ADR is the “why,” the spec writes the “how.”

Note

Correspondence chapters for the type system itself are in『しくみ』 / TAPL; judgments of Rigor’s own engineering are in the ADRs. Seasoned Part 8 gathers a doorway to the ADRs as the bridge from “minimal version → practical tool,” and a4-4 draws on that table.

---

a4-2. The Little volume — chapter × 『しくみ』ch. × TAPL ch.

Laid out by the v1 chapter structure (Little Part 0–9). Both references are optional. The closer primary is the『しくみ』side.

v1 ch.	Theme	『しくみ』	TAPL	Relation (in a phrase)
0	Introduction (an inference-driven type checker)	ch. 1	ch. 1, ch. 8 §8.3	contrast (sound vs. false-positive-averse)
1	Literals and arithmetic	ch. 2	ch. 8	near match (precision exceeds via Const / type_of = typecheck)
2	Method sends and dispatch	ch. 3	ch. 9	reread (function → method, {params, retType})
3	Local variables and an immutable Scope	ch. 3, 4	ch. 9, 11 §11.5	match (tyEnv → immutable Scope, let-bindings)
4	Union — a type doesn’t settle on one	(no corresponding ch.)	ch. 11 §11.10	own terrain (untagged union; both books have only tagged)
5	Narrowing — splitting by case	(no corresponding ch.)	(no corresponding ch.)	own terrain (gradual / flow-sensitive)
6	Hash and array types	ch. 5	ch. 11 §11.8, §11.7	match (but reversed for open vs. exact match)
7	Acceptance checks and three-valued logic	ch. 7	ch. 15	match + three-valued / consistency extension
8	RBS and type signatures	ch. 9, ch. 9 exercises, afterword	ch. 23, 22	partial match（distant relative of type substitution → return-type synthesis; fills『しくみ』‘s gap）
9	The philosophy of gradual typing	afterword	beyond ch. 8 §8.3	connection (soundness in full → gradual beyond it)

Note

The areas『しくみ』 / TAPL didn’t treat directly (untagged Union, three-valued logic, gradual, flow-sensitive narrowing) are precisely where chibirigor “pushed past.” That’s why Little Part 4 and 5 have no corresponding chapter.

---

a4-3. The Seasoned volume — chapter × 『しくみ』ch. × TAPL ch.

Laid out by the v1 new order (Seasoned Part 1–8). The Seasoned volume sets TAPL as the primary signpost.

v1 ch.	Theme	TAPL	『しくみ』	Relation (in a phrase)
1	What bidirectional typing really is	ch. 9	ch. 3	foundation (typing rules of simply-typed lambda; ⇒/⇐)
2	Subtyping and variance	ch. 15, 16	ch. 7	match (width/depth, variance, algorithmic subtyping)
3	Generics and type substitution	ch. 23, 22, 26, 29	ch. 9	match (System F type application, α-conversion, bounded quantification)
4	Recursive types: μ and coinduction	ch. 20, 21 (HKT in ch. 29)	ch. 8	match (equi-recursive, coinduction = greatest fixed point; the HKT aside has separate grounds)
5	Real type inference: filling in arguments	ch. 22	ch. 9 exercises, afterword	frontier（type reconstruction, constraints, unification; where『しくみ』gave up the answer）
6	The complete FactStore	(no corresponding ch.)	(no corresponding ch.)	own terrain (general dataflow analysis; no chapter in a type-theory textbook)
7	Soundness, normalization, unsound on purpose	ch. 8 §8.3, ch. 12	afterword	sets the central theorem (progress + preservation / normalization), tells why unsound
8	Toward real Rigor	(no corresponding ch.)	(no corresponding ch.)	bridge (learning minimal version → practical tool; the correspondence is the ADRs and spec)

Note

Seasoned Part 6 (FactStore) and Part 8 (the bridge to Rigor) are terrain of their own with no corresponding chapter in a type-theory textbook. This is the engineering layer where the Seasoned volume steps beyond TAPL.

---

a4-4. Quick reference to the main ADRs the text cites

Seasoned Part 8 gathers a doorway to the ADRs. This is a list drawn from that table. Just a number and a phrase (for detailed context see Seasoned Part 8 §8-2 / §8-3; the chapter numbers in the text use the v1 structure).

Two to grasp the big picture first

ADR	In a phrase
ADR-0	The starting point of the foundations and design principles (a map for all later ADRs)
ADR-4	How the type inference engine works

ADRs that correspond to the text’s tensions (Seasoned Part 8 §8-3)

ADR	In a phrase	Where in the text
ADR-5	The robustness principle (how to avoid false positives)	Little Part 4, 7; Seasoned Part 7 (unsound on purpose)
ADR-22	baseline + onboarding	Little Part 9 (baseline proper)
ADR-20	Lightweight HKT (stop recursion with reduction fuel; implemented)	Seasoned Part 4 (fuel), Part 7 (budget)
ADR-41	Design of an inference budget (Status: Proposed, not implemented)	Seasoned Part 7 (budget)
ADR-14	sig-gen (signature generation)	Little Part 8, Seasoned Part 3 (erasure)
ADR-25	plugin RBS	Little Part 8
ADR-32	inline RBS	Little Part 8
ADR-46	incremental analysis (a cross-file dependency graph)	Seasoned Part 8 §8-2 (engineering)

Engineering ADRs the practical tool adds

The more engineering-leaning ADRs — extension API, interface separation, macro expansion, Data/Struct folding, persistent cache, bundled LSP, CI output formats, concurrent analysis, performance gates, and so on — are listed in Seasoned Part 8 §8-2 (the Little volume’s text doesn’t name them).

Note

The fastest reading order is to open one ADR for a row that interests you — each is written as a narrative of “why it was designed this way.” The type inference engine’s internal spec is inference-engine.md.

---

a4-5. How to use this appendix

• Want to peek one level deeper into type theory → look up the corresponding chapter in a4-2 / a4-3 and open your copy of『しくみ』 / TAPL. The book is complete even if you have neither.
• Want to read real Rigor → from a4-4, open one ADR for the row that interests you most. ADR-0 → ADR-4 is the map of the whole.
• Back to the text → if you came here from a one-line pointer at the end of a chapter, check your position in the table and return to the chapter. The quick-reference table is a signpost, not the main line.