Part 8 (finale) — Toward real Rigor

Tip

References (optional): Rigor’s ADRs and spec (no corresponding chapter in a type-theory textbook — this is the bridge from “learning minimal version” to “practical tool”). The chapter closing the Seasoned volume, and the whole tutorial.

So far, in the Little volume we built a working minimal version, and in the Seasoned volume recovered the theory behind it (bidirectional, subtyping and variance, generics, recursive types, inference, the FactStore, soundness). Finally, we build the bridge between chibirigor’s minimal version and real Rigor’s build-out. We close by surveying “from here on, what does a practical tool add.”

---

8-1. What we built / what we didn’t

chibirigor (the Little volume), with Prism + a few hundred lines, stacked up like this:

Component	Little volume’s minimal version	Rigor’s real thing
Typing an expression	type_of (synthesis ⇒)	ExpressionTyper (pure, non-destructive)
Acceptance check	accepts (three-valued)	accepts + AcceptsResult (three-valued + reason)
Type environment	Scope (Hash)	Scope + FactStore (six buckets, stability)
Method resolution	hand-written table → mini RBS	MethodDispatcher (multi-tier, RBS, inheritance)
Type carriers	7 kinds	many (Refined/Intersection/App/…)

The minimal version was “the skeleton faithfully, the flesh minimal.” The skeleton (bidirectional, gradual, flow, the RBS boundary) is the same as the real thing. What’s needed to become a practical tool from here?

---

8-2. What a practical tool adds

The layer of engineering, not theory. chibirigor deliberately cut it away. From here we show “if you read, from which ADR” as a concrete next step (ADR = Rigor’s design-decision records, in the repository’s docs/adr/):

What’s added	What engineering it solves	Doorway ADR
Plugin mechanism	type Rails/RSpec/dry-rb DSLs/macros/open classes from outside without polluting the core	ADR-2 (extension API) → ADR-37 (interface separation) → ADR-9 (inter-plugin coordination)
Macro/DSL expansion	type generated methods like attr_accessor and Data.define	ADR-16 (macro expansion) / ADR-48 (Data/Struct folding)
Cache/incremental	don’t fully re-analyze large code every time	ADR-6 (persistent cache) → ADR-45 (unchanged fast path) → ADR-46 (incremental analysis)
LSP (editor integration)	real-time type-error display, completion, hover	ADR-19 (bundled Language Server)
CI integration	output each CI can read: SARIF/GitHub/GitLab, etc.	ADR-51 (CI output formats) / ADR-27 (distribution)
baseline/onboarding	retrofit introduction to existing code (Little Part 9’s baseline in full)	ADR-22 (baseline + onboarding)
Performance	practical speed via reduced allocation, concurrent analysis	ADR-44 (allocation) / ADR-15 (Ractor/fork) / ADR-50 (performance gates)

These are not “the type system itself” but “features that apply the type system” (『しくみ』, too, at the start (the book’s background and purpose) cautions that editor support is not a property of the type system but an application). chibirigor making these out of scope was for keeping the minimal version’s gist. 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.”

---

8-2-a A note — a tiny plugin hook (Chibirigor.register_method)

Let’s give just the “plugin mechanism” of the table above a minimal implementation in chibirigor. The reason real Rigor’s ADR-2 made the design decision “separate the extension API from the core” should settle in.

What it does. Dispatch::METHODS is a read-only catalog generated by Rbs.load. Writing directly into it causes core-polluting problems — interference between tests, contamination by library-specific type info. Instead, prepare one registry composed from outside.

Chibirigor.register_method(
  :String, :shout,
  params:  [],
  returns: Chibirigor::Type::Nominal[:String]
)

Chibirigor.annotate('"hello".shout')
#=> the last expression's type is String (the registered return type is in effect)

How it works (excerpt from lib/chibirigor/plugin.rb)

module Plugin
  @registry = {}

  module_function

  def register_method(klass, name, params:, returns:)
    @registry[[klass, name]] = { params: Array(params), returns: returns }
  end

  def registry = @registry
  def reset! = @registry.clear
end

Dispatch#dispatch references in the order Plugin.registry[key] || METHODS[key]. Just that, and “plugins take priority, the core stays unchanged” holds.

Zero-FP guarantee. A method not in Plugin.registry is left to METHODS as before. If not in METHODS either, it falls back to Dynamic (untyped) — the Little volume’s promise “quietly untyped if you don’t know” is kept here too.

Contrast with real Rigor. chibirigor’s “single-point registry” corresponds to the skeleton of Rigor ADR-2’s extension API. The real thing adds DSLs, lifecycle, and inter-plugin coordination (ADR-9, 37), but the design axis “hold the core catalog and plugin-derived info separately” is the same.

---

8-3. Design decisions remain in the ADRs

A practical tool is the accumulation of countless design decisions. Rigor records them as ADRs (Architecture Decision Records) — “why allow open classes,” “why fork rather than Ractor,” “why design baseline this way.”

Now that you’ve finished building chibirigor, reading Rigor’s ADRs you see that many of them are concrete resolutions of the tensions met in the Little and Seasoned volumes:

• To grasp the big picture first: ADR-0 (the starting point of foundations and design principles) → ADR-4 (how the type inference engine works). These two are the map of all later ADRs.
• “How to avoid false positives” ← Little Part 4, 6, Seasoned Part 7 (unsound on purpose). To read: ADR-5 (the robustness principle) / ADR-22 (baseline).
• “How to stop recursion / inference” ← Seasoned Part 4 (fuel), Part 7 (budget). To read: ADR-20 (lightweight HKT) / ADR-41 (inference-budget design, unimplemented).
• “How to get along with RBS” ← Little Part 8, Seasoned Part 3 (erasure). To read: ADR-14 (sig-gen) / ADR-25, 32 (plugin RBS, inline RBS).
• “How to hold flow facts” ← Seasoned Part 6 (FactStore). To read: ADR-46 (incremental dependency graph) and the internal spec inference-engine.md.

Reading the implementation with the eye that’s settled, through theory, on “why it’s built that way,” each ADR reads as a narrative.

---

8-4. The whole picture so far

The tutorial’s two volumes on one sheet:

• The Little chibirigor — the working minimal version. With Prism + a few hundred lines, until check and annotate work. Feel gentleness, the complexity budget, and FP discipline in a minimal implementation.
• The Seasoned chibirigor — the theory behind it. Recover bidirectional, subtyping and variance, generics, recursive types, inference, the FactStore, soundness, in vocabulary and form.

And real Rigor is a practical-scale gradual type checker that layers onto this skeleton the build-out of plugins, cache, LSP, performance, and ADRs.

---

8-5. The close — three doorways

Finally, the map of this journey:

1. 『しくみ』/TAPL’s terminus is chibirigor’s starting point. Beyond a static, sound checker — from gradual typing, we began (not required, but reading them alongside reads continuously).
2. chibirigor’s starting point is the doorway to Rigor. Now that you’ve built the skeleton by hand in a minimal version, real Rigor’s implementation reads as “the same skeleton, scaled up.”
3. And Rigor’s doorway is the doorway to the still-continuing road of typing Ruby. Gradual typing is ongoing, in both research and implementation.

If you’ve built it all the way to here — now, open real Rigor’s code and read ExpressionTyper’s first case. The familiar shape of the type_of you wrote in the Little volume should be there.

---

8-6. Summary (the whole eight-chapter Seasoned volume)

Part	Theory recovered
1	Bidirectional typing (type_of = ⇒ / accepts = ⇐, diagnostics only at checking positions)
2	Subtyping and variance (width/depth, covariant returns / contravariant arguments, gradual consistency)
3	Generics and type substitution (α-equivalence, variable capture, fresh, erasure)
4	Recursive types (μ, coinduction ↔ HKT/fuel. HKT’s grounds are TAPL ch. 29)
5	Real type inference (capability/duck, constraint-based, only the obvious range)
6	The complete FactStore (six buckets, stability, closure capture, join)
7	Soundness, normalization, and “unsound on purpose” + the gradual guarantee
8	The bridge to a practical tool (plugins, cache, LSP, performance, ADRs)

Exercises

1. Pick one ADR to read next: from §8-2’s table, pick the one row that interests you most, open its doorway ADR, and write out one “which design decision corresponds to which chapter’s tension in the Seasoned volume.”
2. Map the skeleton: pick one pair from §8-1’s correspondence table (chibirigor ↔ Rigor), and state what part the code you wrote in the Little volume (e.g. accepts) has grown into in real Rigor.
3. Redraw the map: sum up what you learned across these two volumes in your own words, in three lines, in the three stages “① built in the Little volume ② read in the Seasoned volume ③ built out in Rigor.”

---

Run it in The Little chibirigor, let it settle in The Seasoned chibirigor, and on to Rigor. The map closes here.