# Part 8 (finale) — Toward real Rigor
Source: https://rigor.typedduck.fail/chibirigor/seasoned/part8-toward-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.**

```ruby
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`)

```ruby
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.