# The Seasoned chibirigor (後編)
Source: https://rigor.typedduck.fail/ja/chibirigor/seasoned/

前編[The Little chibirigor](/ja/chibirigor/little/)で動く最小版（`check`＋`annotate`）を作り切ったあと、その裏側を形式の言葉で読み解く巻です。前編でわざと避けたもの（双方向型付けの形式化、変性、ジェネリクス、再帰型、本物の型推論、FactStore、健全性）を、ここで回収します。

コードより概念が主役で、各章は前編の実装を起点にした解説と設計スケッチの集まりです（動くスケッチは[`examples/`](https://github.com/rigortype/chibirigor/blob/master/book/v2/ja/seasoned/examples/README.md)にあり、`ruby <file>`で自己チェックが緑になります）。

> **重要**
>
> **後編は「作る」より「読み解く」巻です**。前編は「とても易しく、専門用語は後出し」でしたが、後編は用語と形式を扱います。
>
> 参考書（『しくみ』/『TAPL』）の対応は[付録a4](/ja/chibirigor/appendix/a4-bibliography/)に一元化しています（どちらも必読ではありません）。

## 章立て（構造から推論、フローを経て理論の頂点へ、そして橋へと続く一本の坂）

| Part | テーマ | 起点（前編） |
|---|---|---|
| [1](/ja/chibirigor/seasoned/part1-bidirectional-typing/) | 双方向型付けの正体（`type_of`＝合成`⇒`／`accepts`＝照合`⇐`） | 前編P7、P9 |
| [2](/ja/chibirigor/seasoned/part2-subtyping-and-variance/) | 部分型と変性（width/depth、戻り共変、引数反変） | 前編P6、P7 |
| [3](/ja/chibirigor/seasoned/part3-generics-and-substitution/) | ジェネリクスと型代入（`subst`、α 同値、変数捕獲、erasure） | 前編P8 |
| [4](/ja/chibirigor/seasoned/part4-recursive-types/) | μ と余帰納でみる再帰型（発展：HKT/`App`+fuel） | 前編P6 |
| [5](/ja/chibirigor/seasoned/part5-real-inference/) | 引数を埋める本物の型推論（能力収集、制約、単一化） | 前編P8 |
| [6](/ja/chibirigor/seasoned/part6-fact-store/) | 完全なFactStore（6バケツ、stability、クロージャ捕獲、join） | 前編P3、P5 |
| [7](/ja/chibirigor/seasoned/part7-soundness/) | 健全性と正規化、そして「わざとunsound」（gradualの2規律） | 前編P9 |
| [8](/ja/chibirigor/seasoned/part8-toward-rigor/) | 本物のRigorへ（プラグイン、キャッシュ、LSP、ADR、性能） | 前編全体 |

## 動く設計スケッチ

中核アルゴリズムは単体で走る最小のRubyとして[`examples/`](https://github.com/rigortype/chibirigor/blob/master/book/v2/ja/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）の5本です。本文とコードのドリフトは`check_docs.rb`が検出します。

## 読む順番

前編（The Little chibirigor）を読み終えてから来てください。後編の各章は「前編のあの実装は、実は◯◯という理論だった」「前編が避けた◯◯を、ここで読み解く」という形で進みます。