Lesson 6.4 — Bidirectional type checking and local type inference¶
Techniques: bidirectional type checking — synthesis ⇒ and checking ⇐ modes, the mode switch (subsumption), annotation rules and mode-correctness (Pierce & Turner 2000 [PT00]; Pfenning's recipe as surveyed by Dunfield & Krishnaswami [DK21]; higher-rank extension [DK13]); local type inference — synthesizing omitted type arguments of polymorphic calls from the arguments and the expected type, and target-typing lambdas ([PT00, §4]; Java's inference [JLS21-5]; C#, Scala, TypeScript contextual typing) · Pebble implements: bidirectional checking with the literal rule and
letinference (E1–E6; pebble-spec §8.1); the comparison lab measures both disciplines on one calculus · Drills:bidir-modes· Prerequisites: Lessons 6.1 and 6.3 · Time: 5 hours
Lesson 6.3's checker lets information flow only upward. That is why C needs a cast to make 1 a double, why a lambda passed to map must repeat the parameter type that map's signature already implies, and why a mismatch deep inside an argument is reported at the whole argument. Bidirectional checking adds a second judgment in which the type flows down: "check this expression against this expected type". The two modes, and the rules that say when to switch between them, give a checker that stays linear and syntax-directed, needs far fewer annotations, and reports errors closer to the mistake. Pebble's checker is bidirectional; so, in varying degrees, are the checkers of Rust, Swift, Scala, Java, C# and TypeScript. The second half of the lesson adds local type inference: filling in omitted type arguments of generic calls from nearby information only.
1. Problem and motivation¶
Bidirectional type checking¶
The problem. In Lesson 6.1's system every λ carries its parameter type, because the only way to type \(\lambda x.\,e\) bottom-up is to know \(x\)'s type beforehand. Full inference (Chapter 7) removes all annotations but is expensive to extend (subtyping, overloading, higher-rank types make it undecidable or exponential) and gives non-local errors. Pierce and Turner [PT00] observed that most annotations are redundant: in apply(fn x => x + 1) the parameter type of apply already says what x is. Their "local type propagation" and, independently, work on dependent and refinement types (Coquand; Pfenning's refinement types) crystallized into bidirectional typing: two judgments, \(\Gamma \vdash e \Rightarrow \tau\) (\(e\) synthesizes \(\tau\)) and \(\Gamma \vdash e \Leftarrow \tau\) (\(e\) checks against \(\tau\)), with each rule declaring which of its premises synthesize and which check [DK21, §2–4]. Pebble uses it to make integer literals floats where a float is expected (pebble-spec §5) and to point E0401 at the precise subexpression, with a note at the annotation that set the expectation.
Local type inference¶
The problem. A polymorphic function map : ∀α β. [α] → (α → β) → [β] used as map(xs, fn x => x + 1) has two type arguments that the programmer did not write. Hindley–Milner inference (Chapter 7) would solve them globally by unification. Local type inference [PT00, §4] solves them using only the call's own arguments and its expected type: a small constraint problem per call, no inference variables escaping the call, and errors that mention the call. It is what Java's generic-method inference and lambda target typing, C#'s method type inference, Scala 2 and TypeScript's generic calls do. Pebble has no generic functions, so local inference is theory plus drills here; Chapter 7 compares it with global inference.
2. Definitions and algorithms¶
Bidirectional type checking¶
The running language is Lesson 6.1's, with λ-annotations optional and one new form, the ascription \((e : \tau)\).
Definition 6.4.1 (Bidirectional judgments and modes)
A synthesis judgment \(\Gamma \vdash e \Rightarrow \tau\) has inputs \(\Gamma, e\) and output \(\tau\); a checking judgment \(\Gamma \vdash e \Leftarrow \tau\) has inputs \(\Gamma, e, \tau\) and no output. A rule is mode-correct if (1) every input of each premise is an input of the conclusion or an output of an earlier premise (left to right), and (2) the output of a synthesizing conclusion is determined by its inputs and its premises' outputs. A mode-correct rule system can be read as a pair of mutually recursive functions without search [DK21, §3].
Definition 6.4.2 (Bidirectional rules; Figure 6.4.2)
Lt is Add with conclusion type \(\mathsf{bool}\); an annotated λ may also be checked (\({\to}\textsf{I}{\Leftarrow}\) with the side condition that its annotation equals \(\tau_1\)); in Let, \(\Updownarrow\) is the same mode (\(\Rightarrow\) or \(\Leftarrow\)) in premise and conclusion. With subtyping (Lesson 6.5), \(\sigma = \tau\) in Sub⇐ becomes \(\sigma <: \tau\): this is the only place subsumption is needed.
The Pfenning recipe [DK21, §4] explains the modes: introduction forms (λ, and in Pebble array and struct literals) check — their type is what the context expects; elimination forms (application, projection, indexing) synthesize — the type comes from the eliminated expression's synthesized type; the eliminated expression (the principal judgment) is synthesized; ascriptions switch from checking to synthesis, and Sub⇐ switches back.
Definition 6.4.3 (Erasure and annotation)
The erasure \(\lvert e \rvert\) removes every ascription and every λ-annotation. A term \(e'\) is an annotation of \(e\) if \(\lvert e' \rvert = \lvert e \rvert\) (it may have more or fewer annotations). The declarative (Curry-style) system is Figure 6.1.1 with unannotated λs typed by \(\dfrac{\Gamma, x{:}\tau_1 \vdash e : \tau_2}{\Gamma \vdash \lambda x.\, e : \tau_1 \to \tau_2}\) (any \(\tau_1\)) and ascriptions typed by \(\dfrac{\Gamma \vdash e : \tau}{\Gamma \vdash (e : \tau) : \tau}\).
Algorithm 6.4.4 (Bidirectional checker: Synth and Check)
- Input: a context \(\Gamma\) and a term \(e\); for
Check, also an expected type \(\tau\). - Output:
Synthreturns \(\tau\) with \(\Gamma \vdash e \Rightarrow \tau\) or fails;Checksucceeds iff \(\Gamma \vdash e \Leftarrow \tau\). - Precondition: Figure 6.4.2 (mode-correct: Theorem 6.4.8).
- Postcondition: results agree with the rules (Theorem 6.4.8); every call is on an immediate subterm.
- Invariant:
Checkuses a checking rule for the forms that have one (λ,if,let) and the mode switch for every other form;Synthfails exactly on the forms without a synthesis rule (an unannotated λ).
function Synth(Γ, e):
case e of
x: return Γ(x) # fail if unbound
n / b: return int / bool
(e1 : τ): Check(Γ, e1, τ); return τ
λx:τ1. e1: return τ1 → Synth(Γ[x ↦ τ1], e1)
λx. e1: fail "cannot synthesize a type for an unannotated λ"
e1 e2: τf ← Synth(Γ, e1)
if τf is not τ1 → τ2: fail "applying a non-function" (at e1)
Check(Γ, e2, τ1); return τ2
e1 + e2, e1 < e2: Check(Γ, e1, int); Check(Γ, e2, int); return int / bool
if c then a else b: Check(Γ, c, bool); τ ← Synth(Γ, a); Check(Γ, b, τ); return τ
let x = e1 in e2: return Synth(Γ[x ↦ Synth(Γ, e1)], e2)
function Check(Γ, e, τ):
case e of
λx[:τ1]. e1: if τ is not τa → τr: fail "a function where τ is expected" (at e)
if τ1 given and τ1 ≠ τa: fail (at e)
Check(Γ[x ↦ τa], e1, τr)
if c then a else b: Check(Γ, c, bool); Check(Γ, a, τ); Check(Γ, b, τ)
let x = e1 in e2: Check(Γ[x ↦ Synth(Γ, e1)], e2, τ)
otherwise: σ ← Synth(Γ, e) # Sub⇐, the mode switch
if σ ≠ τ: fail "expected τ, found σ" (at e)
Pebble's checker (solutions/pebble/lib/Sema/Types/src/Expressions.cpp) has the same shape, with Pebble's checking rules: an integer literal checked against float becomes a float; parentheses, unary - and + - * / % pass a numeric expected type to their operands; array literals and repeats pass the element type (pebble-spec §8.1). Its Origin argument remembers which annotation produced \(\tau\), so the failure message of the mode switch can say "expected 'T' because of this".
Local type inference¶
Definition 6.4.5 (Polymorphic application with omitted type arguments)
Extend types with type variables \(\alpha\) and let some functions have polymorphic types \(f : \forall \alpha_1 \dots \alpha_k.\ \sigma_1 \to \cdots \to \sigma_m \to \sigma\). A call \(f(e_1, \dots, e_m)\) written without type arguments requires a substitution \(\theta = [\alpha_i \mapsto \tau_i]\) with \(\Gamma \vdash e_j \Leftarrow \theta\sigma_j\) for every \(j\), and (in checking mode against \(\tau\)) \(\theta\sigma = \tau\). Local inference finds \(\theta\) from this call's arguments and expected type only; if some \(\alpha_i\) is constrained by nothing, it reports "cannot infer" (or picks a default).
Algorithm 6.4.6 (Local type-argument synthesis by matching, with deferred lambdas)
- Input: \(f : \forall \vec{\alpha}.\ \sigma_1 \to \cdots \to \sigma_m \to \sigma\), arguments \(e_1, \dots, e_m\), optionally an expected type \(\tau\).
- Output: \(\theta\) and the call's type \(\theta\sigma\), or an error at a specific argument.
- Precondition: without subtyping (constraints are equations); [PT00, §4] generalizes to subtype constraints with minimal solutions.
- Postcondition: every argument checks against \(\theta\sigma_j\); \(\theta\) is the unique solution determined by the synthesized argument types and \(\tau\) (Theorem 6.4.10).
- Invariant: \(\theta\) only grows; an argument is checked only when \(\theta\sigma_j\) has no unsolved variable in the positions that argument needs (a λ's parameter types).
function InferCall(Γ, f, args, τexp):
θ ← {}
if τexp given: Match(σ, τexp, θ) # expected type first (target typing)
pending ← []
for j in 1..m:
if args[j] is an unannotated λ: pending.append(j); continue
Match(σj, Synth(Γ, args[j]), θ) # constraints from the argument
repeat until pending is empty:
j ← some pending λ whose parameter types θσj are fully solved
if none: fail "cannot infer the parameter types of args[j]"
(τp → τr) ← θσj with unsolved result variables left as they are
body ← Synth(Γ[x ↦ τp], args[j].body); Match(σj's result, body, θ)
remove j from pending
if some αi ∉ dom(θ): fail "cannot infer αi"
return θσ
function Match(pattern, τ, θ): # one-sided: τ has no variables
case pattern of
α: if α ∈ dom(θ) and θ(α) ≠ τ: fail "conflicting types for α"
θ(α) ← τ
C(p1…pn): if τ = C(t1…tn): Match(pi, ti, θ) for each i else fail
3. Worked examples¶
Bidirectional type checking¶
The drill's format on the term \(\mathsf{if}\ (\lambda x{:}\mathsf{bool}.\,\mathsf{false})\ \mathsf{true}\ \mathsf{then}\ \lambda y.\,y\ \mathsf{else}\ \lambda z.\,4\) checked against \(\mathsf{int} \to \mathsf{int}\) (./course drill bidir-modes --seed 2 --difficulty hard). One row per premise, in the order Algorithm 6.4.4 visits them:
| node | subterm | how | type |
|---|---|---|---|
| s1 | if (λx:bool. false) true then λy. y else λz. 4 |
check (If⇐) | int -> int |
| s2 | (λx:bool. false) true |
switch (condition checked against bool) | bool |
| s3 | λx:bool. false |
synth (→I⇒, function of an application) | bool -> bool |
| s4 | false |
synth (body of a synthesizing λ) | bool |
| s5 | true |
switch (argument checked against the domain) | bool |
| s6 | λy. y |
check (→I⇐) | int -> int |
| s7 | y |
switch (body checked against the codomain) | int |
| s8 | λz. 4 |
check (→I⇐) | int -> int |
| s9 | 4 |
switch | int |
- s6 and s8 need no annotation: the expected type \(\mathsf{int} \to \mathsf{int}\) flows into both branches (If⇐), then into each λ (→I⇐), which binds \(y\) and \(z\) to \(\mathsf{int}\). A syntax-directed checker would reject both.
- s3 must be annotated: it is the function of an application, a synthesizing position; erasing its annotation makes Synth fail.
- Every
switchrow synthesizes and compares: s2 synthesizesboolby →E (rows s3–s5 are its premises), equal to the expectedbool.
In Pebble. let v: [float; 2] = [1, -(2 + 3)]; is checked by the reference checker as:
| call | expression | mode, expected | rule | type recorded |
|---|---|---|---|---|
| 1 | [1, -(2 + 3)] |
check [float; 2] |
array literal passes the element type | [float; 2] |
| 2 | 1 |
check float |
literal checked against float (§5) | float |
| 3 | -(2 + 3) |
check float |
unary - passes a numeric type |
float |
| 4 | (2 + 3) |
check float |
parentheses pass it | float |
| 5 | 2 + 3 |
check float |
+ passes it to both operands |
float |
| 6, 7 | 2, 3 |
check float |
literal rule | float |
With let n = 2; let v: [float; 2] = [1, -(n + 3)]; call 5 reaches n, which has no checking rule: the mode switch synthesizes int and reports E0401 at n, "expected 'float', found 'int'", with the note "expected '[float; 2]' because of this" at the annotation.
Try it
./course drill bidir-modes --seed 5 --difficulty medium --solution traces a term with ascriptions and unannotated λs; the comparison lab's ch06-bidir-measure runs both disciplines on a corpus (§8).
Local type inference¶
Algorithm 6.4.6 on map(xs, fn x => x + 1) with \(\mathit{map} : \forall \alpha \beta.\ [\alpha] \to (\alpha \to \beta) \to [\beta]\) and \(xs : [\mathsf{int}]\), in synthesis mode:
| step | action | θ after the step | pending |
|---|---|---|---|
| 1 | no expected type | {} | [] |
| 2 | arg 1: Synth(xs) = [int]; Match([α], [int]) |
{α ↦ int} | [] |
| 3 | arg 2 is an unannotated λ: defer | {α ↦ int} | [2] |
| 4 | pending 2: parameter type θα = int is solved; Synth(x + 1) with x : int = int; Match(β, int) |
{α ↦ int, β ↦ int} | [] |
| 5 | all variables solved; result θ[β] |
— | — |
Result: [int]. With let ys: [float] = map(xs, fn x => x + 1) in checking mode, step 1 matches [β] against [float] first (β ↦ float); step 4 then synthesizes int for the body and Match fails: "conflicting types for β" at the λ — the error mentions the call, not a distant use of ys.
4. Invariants and correctness¶
Bidirectional type checking¶
Theorem 6.4.7 (Soundness of bidirectional typing)
If \(\Gamma \vdash e \Rightarrow \tau\) or \(\Gamma \vdash e \Leftarrow \tau\) (Figure 6.4.2), then \(\Gamma \vdash \lvert e \rvert : \tau\) in the declarative system of Definition 6.4.3.
Proof
By mutual induction on the two derivations, one case per rule. Var⇒, Int⇒, Bool⇒: the declarative axioms. Anno: the premise gives \(\Gamma \vdash \lvert e \rvert : \tau\) by hypothesis, and \(\lvert (e : \tau) \rvert = \lvert e \rvert\). →I⇐: the hypothesis gives \(\Gamma, x{:}\tau_1 \vdash \lvert e \rvert : \tau_2\); the declarative λ rule (any \(\tau_1\)) gives \(\lambda x.\,\lvert e \rvert : \tau_1 \to \tau_2\). →I⇒: the same with the annotation's \(\tau_1\). →E: the hypotheses type \(\lvert e_1 \rvert : \tau_1 \to \tau_2\) and \(\lvert e_2 \rvert : \tau_1\); T-App. Add, Lt, If⇐, If⇒, Let: each premise yields the corresponding declarative premise; the declarative rule concludes. Sub⇐: the hypothesis gives \(\Gamma \vdash \lvert e \rvert : \sigma\) and \(\sigma = \tau\).
Theorem 6.4.8 (Mode-correctness and decidability)
Every rule of Figure 6.4.2 is mode-correct, and Algorithm 6.4.4 terminates on every input and returns exactly the judgments derivable by the rules.
Proof
Mode-correctness, rule by rule: in →E, \(e_1\)'s premise has inputs \(\Gamma, e_1\) (from the conclusion), and its output \(\tau_1 \to \tau_2\) supplies the input \(\tau_1\) of \(e_2\)'s checking premise and the conclusion's output \(\tau_2\); in If⇒, \(e_2\)'s output \(\tau\) is the input of \(e_3\)'s premise and the output; in Anno, \(\tau\) is part of the term; in Sub⇐, \(\sigma\) is an output compared with the input \(\tau\); the checking rules take \(\tau\) from the conclusion. Algorithm: for each mode and term form the algorithm applies the unique rule whose conclusion matches — in checking mode the λ/if/let rules for those forms and Sub⇐ otherwise, in synthesis mode the rule for the form — and evaluates its premises in the left-to-right order that mode-correctness makes possible. Each call is on an immediate subterm, so it terminates in one call per subterm (and per mode switch, which re-enters Synth on the same term once). Soundness and completeness with respect to the rules follow by induction on \(e\) as in Theorem 6.1.11, because the choice of rule is forced. (The only non-forced choices in the rules are checking an if, a let or an annotated λ by Sub⇐ instead of its own ⇐ rule; in each case a Sub⇐ derivation can be rebuilt with the ⇐ rule, applying Sub⇐ to the branches or the body instead, so the algorithm's preference loses nothing.)
Theorem 6.4.9 (Completeness: annotatability)
If \(\Gamma \vdash e : \tau\) in the declarative system, then there are annotations \(e_{\Leftarrow}\) and \(e_{\Rightarrow}\) of \(e\) (Definition 6.4.3) with \(\Gamma \vdash e_{\Leftarrow} \Leftarrow \tau\) and \(\Gamma \vdash e_{\Rightarrow} \Rightarrow \tau\). Moreover, if \(e\) is fully annotated (every λ carries its parameter type, as in Figure 6.1.1), then \(\Gamma \vdash e \Rightarrow \tau\) with no extra annotation.
Proof
By induction on the declarative derivation. It suffices to build \(e_{\Leftarrow}\), because \(e_{\Rightarrow} = (e_{\Leftarrow} : \tau)\) synthesizes \(\tau\) by Anno. Variables and constants: they synthesize their type, hence check by Sub⇐. λ: the hypothesis gives \(e_0{}_{\Leftarrow}\) for the body in \(\Gamma, x{:}\tau_1\); \(\lambda x.\, e_0{}_{\Leftarrow} \Leftarrow \tau_1 \to \tau_2\) by →I⇐. Application: take \(e_1{}_{\Rightarrow}\) (synthesizing \(\tau_1 \to \tau_2\)) and \(e_2{}_{\Leftarrow}\) (checking \(\tau_1\)); →E synthesizes \(\tau_2\), and Sub⇐ checks it. Add, Lt: the operands' \(e_i{}_{\Leftarrow}\) against \(\mathsf{int}\); the rule synthesizes, Sub⇐ checks. If: If⇐ with \(c_{\Leftarrow}\) against \(\mathsf{bool}\) and both branches' checking annotations. Let: \(e_1{}_{\Rightarrow}\) and the body's checking annotation, Let in checking mode. Ascription: the declarative rule's premise gives \(e_{\Leftarrow}\) for the inner term; \((e_{\Leftarrow} : \tau) \Rightarrow \tau\) and Sub⇐. For a fully annotated term, the same induction shows every form already synthesizes: an annotated λ synthesizes by →I⇒, an if by If⇒ (its else branch synthesizes the same type, by Theorem 6.1.11, and therefore checks by Sub⇐), and so on — no ascription needed. The lab's test L3_BothAcceptFullyAnnotatedProgramsWithTheSameType checks this second statement on 300 random programs.
Theorem 6.4.9 says the bidirectional system rejects nothing that a type-annotated program could not express, and the second statement says it accepts every program a syntax-directed checker accepts: annotations can only be removed by switching disciplines, never needed.
Local type inference¶
Theorem 6.4.10 (Matching computes the unique local solution)
Let the argument types \(A_j\) (synthesized) and the expected type \(\tau\) (if any) contain no type variables. If InferCall returns \(\theta\), then \(\theta\sigma_j = A_j\) for every synthesized argument, \(\theta\sigma = \tau\) in checking mode, and every deferred λ checks against \(\theta\sigma_j\); and any substitution with these properties agrees with \(\theta\) on \(\vec{\alpha}\). If InferCall fails with "conflicting types", no such substitution exists.
Proof
Match is correct: by induction on the pattern: a variable is bound to the matched type or compared with its existing binding; a constructor pattern matches componentwise. Because \(\tau\) has no variables, the result is a function of the pattern's variables to types with \(\theta p = t\) exactly when Match succeeds, and every binding is forced by a subterm of \(t\) — so any solution agrees with \(\theta\) on the variables Match bound (uniqueness). InferCall: each Match adds forced bindings or detects a conflict (in which case two forced values differ and no solution exists). A deferred λ is checked only when its parameter types are solved; its body's synthesized type is then forced (Theorem 6.1.11), so matching the result pattern again adds only forced bindings. At the end every variable is bound, so \(\theta\) is the unique solution. (Failure because no pending λ has solved parameters means the local information is insufficient, not that no solution exists — the incompleteness that global inference, Chapter 7, removes.)
5. Complexity¶
| Technique | Time (worst) | Time (typical) | Space | Variables |
|---|---|---|---|---|
| Bidirectional checking (Algorithm 6.4.4) | \(\Theta(n)\) calls, each \(O(1)\) with interned types | linear | \(O(d)\) stack | \(n\) subterms, \(d\) nesting depth |
| Local type-argument synthesis (Algorithm 6.4.6) | \(O(m \cdot s + \ell)\) per call, \(\ell\) passes over pending λs \(\le\) their number | constant for small signatures | \(O(k)\) | \(m\) arguments, \(s\) signature size, \(k\) type variables |
Justification. Algorithm 6.4.4 makes one Synth or Check call per subterm, plus one extra Synth per mode switch on the same node; each does \(O(1)\) work apart from type comparisons, which are \(O(1)\) with interned types (Lesson 6.1 §5). Algorithm 6.4.6 matches each argument type against its parameter pattern in \(O(s)\), and each deferred λ is checked once; the "repeat" loop picks at least one pending λ per iteration or fails.
Pathological family. Bidirectional checking itself has none beyond Lesson 6.1's: its cost is linear. Local inference becomes expensive only when it is extended past this lesson's algorithm: Java's inference with wildcards and bounded variables is so expressive that subtyping queries encode arbitrary Turing machines — the Java type checker can be driven into non-termination by a program with generic types [Gri17]. A cheaper pathological family for Algorithm 6.4.6 is a chain of \(\ell\) deferred λs in which each λ's parameter type is solved only by the previous λ's result: the loop needs \(\ell\) passes, and a naive implementation that re-scans the pending list each time costs \(\Theta(\ell^2)\).
Scale. The lab measures what bidirectionality buys, not what it costs: on the 12 well-typed programs of labs/ch06-bidir/corpus, the syntax-directed checker needs 24 of the 32 written annotations and the bidirectional checker 9 (§8), at the same linear cost.
6. Variants and refinements¶
Bidirectional type checking¶
- Checking-mode-first vs synthesis-first [DK21, §4.3]: some systems let every form synthesize if it can and check only when it must (Pebble, Rust), others push checking as far as possible (Agda). The former give more synthesized types for error messages; the latter need fewer annotations.
- Subsumption with subtyping (Lesson 6.5): Sub⇐ with \(\sigma <: \tau\); the declarative subsumption rule is no longer needed anywhere else, which is what makes subtyping algorithmic in a bidirectional system.
- Spine form and higher-rank polymorphism [DK13]: check applications by walking the whole argument spine against a polymorphic type, instantiating quantifiers with existential variables in an ordered context; complete and decidable for predicative higher-rank types.
- Mode-annotated elaboration (Pebble's literal rule, Swift's literal protocols, Go's untyped constants): the checking mode not only verifies but decides the meaning of a term (a literal becomes
float).
Local type inference¶
- Subtype constraints and minimal solutions [PT00, §4]: arguments give lower bounds, the expected type an upper bound; choose the minimal (or maximal) solution depending on the variable's variance in the result type.
- Java's inference (JLS 18): bounds with wildcards, capture, and lambda "pertinent to applicability" rules, solved by incorporation and resolution. More powerful, far more complex, undecidable in the presence of certain wildcard patterns [Gri17].
- Colored local type inference (Odersky, Zenger and Zenger 2001) and Scala's implementation: propagate partial type information (some components known) into arguments.
- TypeScript's contextual typing: an expected (contextual) type types unannotated callback parameters; generic type arguments are inferred from arguments in several passes, deferring context-sensitive arguments (lambdas) as in Algorithm 6.4.6.
7. In real compilers¶
Bidirectional type checking¶
rustc's type checker is bidirectional: check_expr_with_expectation takes an Expectation [RUSTC-Typeck] — ExpectHasType(ty) is ⇐ and NoExpectation is ⇒ — and closures take their parameter types from the expected signature (deduce_closure_signature [RUSTC-Closure]). javac threads the expected type as ResultInfo.pt through attribution [JAVAC-Attr]. Pebble's reference checker has synth and check methods (Algorithm 6.4.4 with Pebble's rules). The comparison lab implements both disciplines side by side.
Expected types in rustc 1.94: closures, notes and the missing annotation
Reproduce (rustc 1.94.1):
mkdir -p rs && cat > rs/bidir.rs <<'EOF'
fn apply(f: impl Fn(i32) -> i32) -> i32 { f(1) }
fn main() {
let a = apply(|x| x + 1); // x : i32, pushed in from apply's parameter
let g: fn(u8) -> u8 = |x| x * 2; // checked against the annotation
let h = |x| x; // nothing to check against
println!("{} {}", a, g(3));
}
EOF
rustc --edition 2021 rs/bidir.rs -o rs/bidir
cat > rs/bidir2.rs <<'EOF'
fn main() {
let a = 2;
let g: fn(u8) -> u8 = |x| x * 2;
let s: bool = a > 1 && g(3);
println!("{}", s);
}
EOF
rustc --edition 2021 rs/bidir2.rs -o rs/bidir2
Output (complete):
error[E0282]: type annotations needed
--> rs/bidir.rs:6:14
|
6 | let h = |x| x; // nothing to check against
| ^
|
help: consider giving this closure parameter an explicit type
|
6 | let h = |x: /* Type */| x; // nothing to check against
| ++++++++++++
error: aborting due to 1 previous error
For more information about this error, try `rustc --explain E0282`.
error[E0308]: mismatched types
--> rs/bidir2.rs:4:28
|
4 | let s: bool = a > 1 && g(3);
| ----- ^^^^ expected `bool`, found `u8`
| |
| expected because this is `bool`
error: aborting due to 1 previous error
For more information about this error, try `rustc --explain E0308`.
What to notice: lines 4 and 5 of bidir.rs are accepted without annotating x: the parameter type flows in from apply's signature and from the fn(u8) -> u8 annotation (→I⇐). Line 6 has nothing to check against, and a closure in synthesis position cannot be typed (the unannotated-λ case of Synth). In bidir2.rs, && checks its right operand against bool and the mode switch finds u8; the error points at g(3) and explains where the expectation came from — Pebble's "expected 'T' because of this" note, and the conv.rs box of Lesson 6.3 ("expected due to this") at an annotation.
Local type inference¶
javac infers generic method type arguments and target-types lambdas (Attr.visitLambda, Infer [JAVAC-Attr]); TypeScript's getContextualType [TSC-Checker] supplies the expected type for callback parameters.
Local inference in javac 21 and tsc 5.9: from arguments, from the target, or not at all
Reproduce (javac 21.0.10, tsc 5.9.3 via npx):
mkdir -p java ts && cat > java/Local.java <<'EOF'
import java.util.List;
import java.util.function.Function;
class Local {
static <T, R> R apply(Function<T, R> f, T x) { return f.apply(x); }
static void run() {
List<String> names = List.of("a", "bb"); // T := String, from the arguments
Function<Integer, Integer> inc = x -> x + 1; // x : Integer, from the target type
int n = apply(s -> s.length(), "abc"); // T := String from "abc", then R := Integer
var twice = x -> x * 2; // no target type for the lambda
List<Integer> empty = List.of(); // T := Integer, from the target type
}
}
EOF
javac -d java java/Local.java
cat > ts/contextual.ts <<'EOF'
const nums = [1, 2, 3];
const lens = ["a", "bb"].map(s => s.length); // s: string from map's parameter type
const handler: (e: { key: string }) => void = e => console.log(e.key.toUpperCase());
const bad = (x) => x * 2; // no contextual type for x
nums.forEach(n => n.toFixed(1));
EOF
npx -y -p typescript@5.9 tsc --strict --noEmit ts/contextual.ts
Output (complete; the container's Picked up JAVA_TOOL_OPTIONS banner removed):
java/Local.java:10: error: cannot infer type for local variable twice
var twice = x -> x * 2; // no target type for the lambda
^
(lambda expression needs an explicit target-type)
1 error
ts/contextual.ts(4,14): error TS7006: Parameter 'x' implicitly has an 'any' type.
What to notice: every line but one of each file is accepted. apply(s -> s.length(), "abc") is Algorithm 6.4.6's §3 trace: T comes from the non-lambda argument, then the deferred lambda is checked with s : String and its body gives R. List.of() gets T := Integer from the target type alone (matching the expected type first). The lambdas with no target type — var twice = … in Java, (x) => x * 2 in TypeScript — are the unannotated λ in synthesis position: Java rejects it; TypeScript under --strict reports that x would silently become any.
8. Comparison¶
| Technique | Power / precision | Speed (asymptotic · practical) | Output / error quality | Implementation effort | Typical use |
|---|---|---|---|---|---|
| Bidirectional checking | Accepts every fully annotated program a syntax-directed checker does (Theorem 6.4.9), plus unannotated λs, literals and aggregates in checking positions | \(\Theta(n)\) · as fast as syntax-directed | Errors at the smallest mistyped subterm, with the origin of the expectation; lab: 10 of 10 errors at the blamed position vs 5 of 10 | Low: two mutually recursive functions | Pebble, Rust, Swift (parts), Scala, Agda, Idris, TypeScript contextual typing |
| Local type inference | Omitted type arguments solved from one call's arguments and expected type (Theorem 6.4.10); fails when information is not local | \(O(m \cdot s)\) per call · negligible except in Java's full inference (undecidable with wildcards [Gri17]) | "cannot infer T" at the call; no action at a distance | Medium (matching, deferred lambdas); high for Java-scale bounds | Java, C#, Scala 2, TypeScript, Kotlin |
Comparison-lab results (reproduce with build/<preset>/bin/ch06-bidir-measure labs/ch06-bidir/corpus, reference solutions): on the 12 well-typed programs, 32 annotations written, 24 needed by the syntax-directed checker and 9 by the bidirectional one (the smallest subset each accepts, found exhaustively); on the 10 ill-typed programs, the error is at the blamed position (the real mistake, marked in each file) in 5 cases for the syntax-directed checker and 10 for the bidirectional one. Of the five misses, four report an unannotated λ — twice the mistake is in that λ's body, once in another field of the same record literal, once in the other branch of the same if — and one reports the whole argument λ where the mistake is in its body.
Choose bidirectional checking for any statically typed language with first-class functions, literals that can have several types, or subtyping: it costs one extra function and gives better errors. Choose local type inference for generic calls when you want predictable, local errors and can accept writing an annotation when information is not available at the call; choose global inference (Chapter 7) when you want no annotations at all.
9. Assessment¶
| Technique | Quiz ids | Drill | Flashcard tag | Exercises |
|---|---|---|---|---|
| Bidirectional checking | bidir-mode-of-premise, pebble-literal-propagation, find-rustc-expectation |
bidir-modes |
bidirectional |
E3 (checking mode, literal rule, notes), E5 (arguments checked against parameters) |
| Local type inference | local-inference-trace, local-inference-limits |
— (Algorithm 6.4.6 on a generic call is traced in the quiz; Chapter 7's drills cover unification) | local-inference |
— |
References¶
See the chapter references.