# The Seasoned chibirigor
Source: https://rigor.typedduck.fail/chibirigor/seasoned/

Once the [Little chibirigor](/chibirigor/little/) has built a *working* minimal checker
(`check` + `annotate`), this volume **reads the machinery behind it in the language of formal
theory**. Everything the Little volume **deliberately avoided** — the formalization of
bidirectional typing, variance, generics, recursive types, real type inference, the FactStore,
soundness — is collected here.

Concepts lead, not code: each chapter is a *commentary plus design sketches* anchored to the
Little volume's implementation (the runnable sketches live in [`examples/`](https://github.com/rigortype/chibirigor/blob/master/book/v2/en/seasoned/examples/README.md),
where `ruby <file>` turns its own self-check green).

> **Important**
>
> **The Seasoned volume is the "read it" volume, not the "build it" one.** The Little volume
> was "very gentle, jargon deferred"; the Seasoned volume takes *vocabulary and formality*
> head-on.
>
> The reference correspondence（『しくみ』 / TAPL）is consolidated in
> [appendix a4](/chibirigor/appendix/a4-bibliography/) (**neither is required reading**).

## Chapters (one long climb: structure → inference & flow → the peak of theory → the bridge)

| Part | Theme | Starting point (Little) |
|---|---|---|
| [1](/chibirigor/seasoned/part1-bidirectional-typing/) | What bidirectional typing really is (`type_of` = synthesis `⇒` / `accepts` = checking `⇐`) | Little P7 · P9 |
| [2](/chibirigor/seasoned/part2-subtyping-and-variance/) | Subtyping and variance (width/depth · covariant returns · contravariant parameters) | Little P6 · P7 |
| [3](/chibirigor/seasoned/part3-generics-and-substitution/) | Generics and type substitution (`subst` · α-equivalence · variable capture · erasure) | Little P8 |
| [4](/chibirigor/seasoned/part4-recursive-types/) | Recursive types — μ and coinduction (+ a note: HKT / `App` + fuel) | Little P6 |
| [5](/chibirigor/seasoned/part5-real-inference/) | Real type inference — filling in arguments (capability gathering / constraints + unification) | Little P8 |
| [6](/chibirigor/seasoned/part6-fact-store/) | The complete FactStore (six buckets · stability · closure capture · join) | Little P3 · P5 |
| [7](/chibirigor/seasoned/part7-soundness/) | Soundness, normalization, and "unsound on purpose" (+ the two disciplines of gradual typing) | Little P9 |
| [8](/chibirigor/seasoned/part8-toward-rigor/) | Toward real Rigor (plugins · cache · LSP · ADRs · performance) | the whole Little volume |

## Runnable design sketches

The core algorithms run on their own as minimal Ruby under [`examples/`](https://github.com/rigortype/chibirigor/blob/master/book/v2/en/seasoned/examples/README.md):
`subtype.rb` (Part 2) / `subst.rb` (Part 3) / `mu_typeeq.rb` (Part 4) / `unification.rb`
(Part 5) / `fact_invalidation.rb` (Part 6). `check_docs.rb` detects drift between the prose
and the code.

## Reading order

Come here after finishing the Little chibirigor. Each Seasoned chapter proceeds as "that
implementation back in the Little volume was really the theory of ◯◯" and "the ◯◯ the Little
volume avoided, read here."