Part 1 — What bidirectional typing really is

The first chapter of the Seasoned volume. The Seasoned volume is the “read it” volume, not the “build it” one — we give proper names to the mechanism we built unconsciously in the Little volume, and read the back of it in formal language. This chapter writes almost no new code. It’s an overview (a map) revealing what the things we already wrote actually were — though at the end we peek, in just one place, at the point where checking ⇐ emits a diagnostic.

In the Little volume (The Little chibirigor), we built two functions as the heart of the inferencer:

• type_of(node, scope, diag) — find a type from an expression.
• accepts(expected, actual) — check whether a type fits an expectation.

These two have proper names in the world of type theory. That’s bidirectional typing. The Seasoned volume starts here.

---

1-1. Two directions — synthesis and checking

Typing has two modes of opposite direction.

• Synthesis (⇒): look at an expression and build a type from the bottom up. The Little volume’s type_of is this. See 1, it’s Integer; see a + b, it’s (from both their types) Integer. Input is just the expression, output is the type.
• Checking (⇐): against an already-expected type, check from the top down whether the expression fits. The Little volume’s accepts (and the dispatch that calls it) is this. “An Integer is wanted here. Does this expression fit?” Input is the expression and the expected type, output is a verdict (three-valued in chibirigor).

The Little volume’s type_of was through-and-through ⇒, and only where dispatch looks at arguments was it ⇐. That is, chibirigor was bidirectional from the start. As a figure, it’s two arrows of opposite direction:

   expected type T (RBS signature · annotation · declared return type)
            │
            │  ⇐  check        : S <: T ?  ── mismatch → diagnostic
            ▼
   expr e  ──⇒──▶  type S
        synthesize: build a type from the expression (chibirigor never fails; unknown → untyped)

▼ Figure 1-1 — synthesize ⇒ (build a type from the bottom up) and check ⇐ (match against the expected type above)

Tip

Reference note (optional). The form of bidirectional typing rests on the typing rules of TAPL ch. 9 (the simply-typed lambda calculus). 『しくみ』ch. 3 (function types)‘s typecheck is made of pure ⇒ (synthesis) alone — that book’s mini-language always has type annotations on parameters, so it didn’t need to be aware of ⇐ (checking) independently.

chibirigor, dealing with annotation-free Ruby, had to clearly separate ⇒ and ⇐ — that’s bidirectional typing.

---

1-2. Writing the rules formally

In the Seasoned volume we don’t fear notation. A typing rule writes the “premises” above a horizontal line and the “conclusion” below. There are two judgments:

• Synthesis: Γ ⊢ e ⇒ T (under environment Γ, synthesizing the type of expression e gives T)
• Checking: Γ ⊢ e ⇐ T (under environment Γ, expression e checks against expected type T)

(⊢ is a type-theory symbol read “turnstile,” meaning under the premises on the left, the right is derivable. ⇒/⇐ were the synthesis/checking directions.)

Γ (gamma) is the Little volume’s Scope (variable name → type). For example, the synthesis rule for a variable reference:

  x : T ∈ Γ
  ───────────  (Var-Synth)
  Γ ⊢ x ⇒ T

“If x : T is in Γ, then x’s type is synthesized as T.” The Little volume’s scope.local(node.name) || Dynamic is exactly this rule (with a chibirigor-style footnote: if it isn’t there, fall back to untyped).

And the most important rule, tying the two directions together — subsumption:

  Γ ⊢ e ⇒ S    S <: T
  ─────────────────────  (Sub)
  Γ ⊢ e ⇐ T

“Synthesizing expression e gave S. If S is a subtype of T, then e checks against T.” Checking is ‘synthesize, then match by subtyping’ — this is the true form of the Little volume’s “type_of an argument, then accepts.” The relation between <: (subtyping) and chibirigor’s three-valued accepts is pinned down in Part 2.

---

1-3. Why a diagnostic only comes out in checking (⇐)

In the Little volume we wrote the most important sentence thus: “a diagnostic only appears where the expected type is fixed.” In bidirectional words:

Important

A diagnostic is born only when S <: T breaks in the subsumption of checking ⇐. A ⇐ position = where the expected type T is declared/known: an explicit annotation, a declared return type, and also the argument position of a method call listed in RBS (or the Little volume’s hand-written table).

Let’s be precise here. It is not that “annotation-free code has no ⇐ position” — a core-type method call (the + in 1 + x, etc.) is a ⇐ position even with zero annotations, because RBS gives the argument’s expected type. So why does working code still go unflagged? There are two reasons, both corresponding to the Little volume’s Part 9 “deliberately miss”:

1. Synthesis ⇒ deliberately doesn’t fail (chibirigor-specific). In bidirectional typing in general, synthesis can fail on an unbound variable or a form with no synthesis rule. chibirigor intentionally synthesizes every unknown into untyped, totalizing it. So even when “an expression that lost its type” comes to a ⇐ position, the synthesis result is untyped.
2. untyped passes straight through checking. accepts is unconditionally :maybe (not punished) if either side is Dynamic. So even when untyped comes to a ⇐ position, it’s not a diagnostic.

To sum up — working code goes unflagged not because “there’s no ⇐ position” but because “synthesis collapses the unknown to untyped, and checking doesn’t punish untyped.” You can state this property only by laying chibirigor’s two gradual design judgments — ① totalizing synthesis, ② lenient checking — onto the bidirectional framework. Seasoned Part 7’s “deliberately let go of soundness” catches these same two points in the language of progress/preservation — we recover, late in the volume, the foreshadowing dropped at the entrance.

---

1-4. The robustness principle is the direction itself

In Little Part 7 we saw the asymmetry “strict on returns, lenient on arguments.” Seen bidirectionally, this is the direction itself:

• The return value is synthesis ⇒: build the narrowest type from the body (strict = high precision).
• An argument is checking ⇐: receive leniently against the expected type (let :maybe through too).

The robustness principle Rigor upholds (Postel’s law: “strict in what you return, liberal in what you accept”) overlaps the two directions of bidirectional typing exactly, on one sheet. In the Little volume it appeared as a practice; in the Seasoned volume, as theory.

---

1-5. How it works inside Rigor

Real Rigor’s architecture has these two directions as parts directly:

• ExpressionTyper (typing an expression) = synthesis ⇒. Pure, non-destructive, builds a type from an expression.
• accepts at a call site (the acceptance check, three-valued + reason) = checking ⇐. Works only where an RBS declaration gives the expected type T.
• Scope / FactStore = the environment Γ (far richer than the Little volume’s; treated in Part 6).

chibirigor’s type_of / accepts / Scope were the minimal version of these three. The Seasoned volume adds flesh to this skeleton.

Note

Where the notation comes from. Bidirectional typing is a framework popularized by Pierce & Turner, “Local Type Inference” (2000), with Dunfield & Krishnaswami’s survey “Bidirectional Typing” (2021) as the modern overview. It’s the apparatus for organizing where to place annotations so type inference runs deterministically.

---

1-6. What the Seasoned volume stacks on this — the volume’s map

With the map of bidirectionality in hand, the rest of the Seasoned chapters are surveyable by “which part of the map they fill in.” The whole is one long climb: “① bidirectional (the map) → ② the structure of types → ③ inference and flow → ④ the peak of theory → ⑤ the bridge”:

• Part 2 Subtyping and variance: refine subsumption’s <:. In particular, the story where a function’s argument is contravariant — the direction twists one more turn (the climax of 『しくみ』ch. 7).
• Part 3 Generics and type substitution: type variables (X) -> X and type substitution (System F). Part 5’s inference references this backward.
• Part 4 Recursive types: μ and coinduction: how ⇒/⇐ handle a type that references itself (μ-types / coinduction ↔ Rigor’s HKT). Adjacent to Part 3, tying up the mutual reference of α-equivalence.
• Part 5 Real type inference: fill in what the Little volume fell back to untyped with ⇒ — arguments in particular — from how they’re used in the body. Widening ⇒’s coverage (the frontier of『しくみ』ch. 9’s exercises). The TypeProf comparison is consolidated here too.
• Part 6 The complete FactStore: extend the environment Γ into a flow-sensitive set of facts.
• Part 7 Soundness and normalization: the peak that pairs with this chapter’s bidirectional map. Read the design that “deliberately lets go” of soundness in the language of progress/preservation. We recover §1-3’s foreshadowing here.
• Part 8 Toward real Rigor: the bridge handing off from the minimal version to real Rigor.

---

1-7. This chapter’s summary

We wrote almost no new code. Instead we gave names to what we built in the Little volume:

What we wrote in the Little volume	What it really is
type_of (find a type)	synthesis ⇒ (synthesize)
the argument check of accepts / dispatch	checking ⇐ (check) = synthesize, then <:
Scope	the type environment Γ
”diagnostics only where there’s an expectation”	a diagnostic is born only at a ⇐ position (follows from the structure)
“strict on returns, lenient on arguments”	synthesis ⇒ strict / checking ⇐ lenient (the robustness principle)

---

1-7-a A note — the first point where ⇐ emits a diagnostic (check(rbs:) mode)

In §1-3 we said “a diagnostic only appears in checking (⇐).” The check up to the Little volume used checking only in “dispatch’s argument check.” Add to it a check(source, rbs:) mode that checks the body against a declared return type, and a scene arises where ⇐ works outside the “caller side” too. The only code we peek at this chapter is this one — a small window for seeing where checking ⇐ first raises a diagnostic.

rbs = <<~RBS
  class Greeter
    def greet: () -> Integer
  end
RBS

Chibirigor.check('def greet; "hi"; end', rbs: rbs)
# => [{line: 1, message: "return type Integer is declared but \"hi\" is returned"}]

Chibirigor.check('def greet; 1; end', rbs: rbs)   # => [] (matches)
Chibirigor.check('def greet; "hi"; end')           # => [] (no declaration = no check)

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

1. Collect body errors in the usual eval_statement loop (as before).
2. If rbs: is present, load the user declarations with Rbs.load(rbs), and for each DefNode call check_against(node, declared_return, body_type, diagnostics).
3. check_against adds a diagnostic only when Accepts.call(expected, actual) == :no. If untyped is involved, it stays quiet (gradual’s promise).

# ⇐ subsumption: check actual against expected. diagnose only :no.
def check_against(node, expected, actual, diagnostics)
  return if expected.is_a?(Type::Dynamic) || actual.is_a?(Type::Dynamic)
  return unless Accepts.call(expected, actual) == :no

  diagnostics << diagnostic(node, "return type #{expected} is declared but #{actual} is returned")
end

This is the minimal point at which ⇐ does work outside “arguments.” Recall §1-4’s robustness principle — “the return type strictly (checked with ⇐)” appears in the implementation for the first time here. It pairs with the Little volume’s dispatch “checking arguments with ⇐.”

Zero-FP guarantee. Pass no rbs: and it checks nothing (opt-in). If the declaration is untyped, no check. Even if the body is untyped (when inference lost the type), no check. With this, “never frighten working code” is kept in return-type checking too.

Note

The param: directive does two jobs

Rigor has a param: directive written with the RBS extension annotation %a{rigor:v1:param: name is String} (it can’t be written inline in the .rb body; it’s placed on the RBS side). It brings two effects at once:

1. Body narrowing (gives the ⇒ side a starting point for the type): inside the body, name’s type starts from the declared String. Inference proceeds from the declared type from the start, without writing is_a?.
2. ⇐ checking at the call site: for a call like greet(42), the argument type is checked against the declaration with accepts, and :no adds a diagnostic.

That is, param: carries both “a promise to the writer (the body follows the type)” and “a promise to the caller (keep to the argument)” at once. That both are unified as ⇐ (checking) is the clean point of bidirectional typing.

---

Exercises

1. Using only the subsumption (Sub) rule, explain in two lines that “no diagnostic is born on the synthesis ⇒ side” (hint: where in Sub’s premise does the failure of S <: T occur).
2. Consider annotation-free Ruby 1 + x (x unbound). (a) What is x’s synthesis result? (b) Is +’s argument position a ⇐ position? (c) Why is there still no diagnostic — which of §1-3’s two reasons works?
3. Restate the robustness principle “strict on returns, lenient on arguments” using only the words ⇒/⇐ (with a phrase for why each direction is strict/lenient).

---

Next chapter (Part 2): we build subsumption’s <: head-on. The width/depth subtyping of objects, and contravariance — where the argument direction alone reverses when you pass a function — that climax『しくみ』ch. 7 called “variance changing direction in the implementation.”