chibirigor — learn type checking by building a tiny Ruby type checker

An online tutorial where you learn by building the smallest Ruby type checker, chibirigor, with your own hands. Just as chibivue teaches Vue by rebuilding it in miniature, we learn the real Rigor — a gradual type checker for Ruby — by rebuilding it small.

Note

This directory is the English edition (v2), transcreated from the Japanese original under ../ja/. Contributor notes on how it is written live in STYLE.md.

What you get from this book

By writing a few dozen to a few hundred lines of Ruby, you’ll be able to answer these questions with your own hands:

• How does a type checker infer types straight from source code?
• Why does Rigor refuse to reject untyped code, and still report only genuine contradictions?
• What does “never frighten working code” actually mean as a design stance?

When you’re done, you’ll have a small, working type checker with two commands — check (type diagnostics) and annotate (show the inferred types) — and a head start on reading real Rigor’s source.

Who this is for, and what’s assumed

• Intermediate Rubyists — comfortable reading and writing classes, modules, case/when, and blocks.
• No type-system theory required (the Little volume). Every concept the Little volume leans on is introduced gently, right where it’s needed.
• The only prerequisite is Ruby. There is no math or proof in the Little volume — the Seasoned volume takes those on.

Two volumes

Following Scheme’s classics (The Little Schemer / The Seasoned Schemer), the book is split in two.

• The Little chibirigor (little/) — the gentle introduction. Build a minimal implementation where check and annotate work, across Part 0 through Part 9. The code runs to completion within the Little volume; the formal theory is handed to the Seasoned volume.
• The Seasoned chibirigor (seasoned/) — the advanced volume. Here we read the machinery behind what the Little volume built, in the language of formal theory (bidirectional typing, subtyping and variance, generics, recursive types, real inference, the FactStore, soundness). It takes the notation and vocabulary head-on.

Note

The Little volume is the “build it” volume; the Seasoned volume is the “read it” volume. In the Seasoned volume, concepts — not code — take the lead.

Either order works, but if this is your first time, read Little → Seasoned.

The three perspectives in every chapter

Each chapter is written from a small set of three perspectives — “① type theory ↔ ② Ruby/RBS ↔ ③ Rigor’s implementation,” laid over one another (Part 0 explains it in full).

Every chapter ends with exercises you run by hand. At the back of the book you’ll find a glossary (glossary.md) and a set of cross-volume appendices (appendix/).

Further reading (optional)

For readers who want to look one level deeper into type theory, each chapter carries a short reference note in the margin. Neither book below is required — chibirigor stands on its own; reach for them only where you want more.

• TAPL — Benjamin C. Pierce, Types and Programming Languages (MIT Press). The full textbook, with real proofs for each topic. This is the shared reference for English readers.
• 『しくみ』 (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 a typed mini-language — almost exactly chibirigor’s mirror image. It is published in Japanese only; where it is the sole correspondence and no English equivalent exists, the text says so plainly.

A correspondence table lives in appendix appendix/a4-bibliography.md.

Setup

Anything with Ruby 3.4+ (which bundles the Prism parser) will run it. No test framework needed.

$ git clone <this repository>
$ cd chibirigor
$ ruby exe/chibirigor check    path/to/file.rb   # type diagnostics
$ ruby exe/chibirigor annotate path/to/file.rb   # show inferred types

If you want to follow along by typing the code out, a lib/ directory in your own working folder, grown file by file per chapter, is all you need. Every chapter’s code has been checked to run on real Prism/Ruby.

Table of contents

The Little chibirigor (build it)

Part	Theme
0	Introduction — an inference-driven type checker
1	Literals and arithmetic
2	Method sends and dispatch
3	Local variables and an immutable Scope
4	Union — when a type doesn’t settle on one
5	Narrowing — splitting by case
6	Hash and array types
7	Acceptance checks and three-valued logic
8	RBS and type signatures
9	The philosophy of gradual typing (finale)

The Seasoned chibirigor (read it)

Part	Theme
1	What bidirectional typing really is
2	Subtyping and variance
3	Generics and type substitution
4	Recursive types — μ and coinduction
5	Real type inference — filling in arguments
6	The complete FactStore
7	Soundness, normalization, and “unsound on purpose”
8	Toward real Rigor (finale)

Appendices

• a1 — Catalog of special types — untyped / void / never / Top / Bot
• a2 — Narrowing patterns (a warm-up for Seasoned Part 6; skippable if you’re reading only the Little volume)
• a3 — Tooling — --explain / the two-layer type display / trace / the dispatch cascade
• a4 — Reference & ADR correspondence table
• a5 — Bridges from other languages — null safety / nominal vs. structural subtyping / the HashShape lineage / untagged unions

Now let’s begin with Part 0.