Chapter 6 · Type Systems & Type Checking¶

Part 1 · Front End · about 3 weeks · Previous: Ch 5 · Next: Ch 7

The problem¶

After name resolution (Chapter 5) every identifier knows its declaration, but nothing yet says what a program computes with: whether w * h multiplies two numbers of the same kind, whether a call passes what the function expects, whether &mut xs[i] names storage the callee may write. A type system answers these questions with rules, and a type checker applies them to every expression, reporting each mistake once, where it happened, with the annotation that explains why. This chapter builds the theory that says what the rules guarantee (judgments, derivations, progress and preservation), the ways real languages differ (static or dynamic, strong or weak, sound or not, nominal or structural), and the checking algorithms production compilers run — syntax-directed and bidirectional checking, subtyping, flow-sensitive narrowing, gradual typing, places and borrow checking — and ends with how generics become machine code. The input is a resolved AST; the output is the same AST with a type on every declaration and expression and a category (value, place, mutable place) on every expression. In pebblec this is typeCheck (pebble/include/pebble/Sema/Sema.h), which lowering (Ch 11) and every later chapter rely on.

What you will be able to do¶

Read and write typing rules, build and check derivation trees, and prove progress and preservation for a small language — and predict which of the two a modified rule set loses.
Place any language on the static/dynamic, strong/weak and sound/unsound axes, with a program that demonstrates each classification.
Implement syntax-directed checking with an error type that prevents cascades; trace C's usual arithmetic conversions and C++/Java overload resolution.
Implement a bidirectional checker, explain which annotations it needs and why, and trace local type-argument inference.
Decide structural subtyping algorithmically with records, functions, top and bottom; compute variance; explain nominal vs structural subtyping.
Compute flow-sensitive narrowing and occurrence-typing propositions; explain Kotlin's stability rule.
Insert casts for a gradually typed program, predict blame, and state the gradual guarantee.
Classify places, check reference arguments and exclusivity, and trace NLL regions and loans in scope.
Explain monomorphization, erasure and dictionary passing from compiler output (symbols, javap, GHC Core).
Implement pebblec's type checker (typeCheck) and pass ./course test 6.
Find each technique in Clang (SemaExpr.cpp, SemaOverload.cpp), rustc (rustc_hir_typeck, rustc_borrowck, rustc_monomorphize), javac, tsc, mypy, Kotlin and GHC.

Prerequisites: Ch 5 (names bound, the Pebble AST, dataflow on the AST in Lesson 5.7). Proofs are by induction on derivations; Lesson 6.1 introduces the technique.

Notation¶

Shared notation follows the house notation (§1 sets and functions, §3 graphs, §7 dataflow, §8 complexity). In this chapter:

Symbol	Meaning
\(\Gamma\), \(\Gamma, x{:}\tau\), \(\Gamma(x)\)	a typing context, its extension, lookup (Definition 6.1.2)
\(\Gamma \vdash e : \tau\)	the typing judgment: \(e\) has type \(\tau\) under \(\Gamma\) (Definition 6.1.2)
\(\dfrac{J_1 \ \cdots\ J_k}{J}\ (\textsf{Name})\)	an inference rule with premises \(J_i\) and conclusion \(J\) (Definition 6.1.3)
\(e \longrightarrow e'\), \(\longrightarrow^{*}\), \([x \mapsto v]e\)	one evaluation step, its reflexive-transitive closure, substitution (Definition 6.1.7)
\(\langle \mathit{tag}, v \rangle\), \(\mathsf{dyn}\)	a tagged run-time value; the single static type of a dynamically typed language (Definition 6.2.3)
\(\mathsf{err}\) / `<error>`, \(\approx\)	the error type; compatibility, which accepts it everywhere (Definition 6.3.2)
\(\Gamma \vdash e \Rightarrow \tau\), \(\Gamma \vdash e \Leftarrow \tau\)	synthesis and checking judgments of bidirectional typing (Definition 6.4.1)
\(\theta = [\alpha \mapsto \tau]\)	a substitution of type variables (Definition 6.4.5)
\(S <: T\), \(\top\), \(\bot\)	subtyping; the top and bottom types (Definitions 6.5.1–6.5.3)
\(+\), \(-\)	the polarity of a position in a type (Definition 6.5.5)
\(U{\downarrow}g\), \(U \setminus g\), \(\Gamma \vdash e : \tau \mathrel{;} \psi_{+} \mid \psi_{-}\)	restriction and removal of a union by a test; typing with then/else propositions (Definitions 6.6.1–6.6.2)
\(?\), \(\tau \sim \sigma\), \(\tau \sqsubseteq \tau'\), \(\tau \sqcap \sigma\)	the dynamic type; consistency; precision (\(\tau'\) less precise); the meet (Definitions 6.7.1–6.7.2)
\(\langle \sigma \Rightarrow \tau \rangle^{\ell}\, e\)	a cast with blame label \(\ell\) (Algorithm 6.7.4, Definition 6.7.5)
\(\Gamma \vdash e : \tau \mathrel{@} \kappa\)	the category \(\kappa \in \{\mathsf{value}, \mathsf{place}, \mathsf{mutplace}\}\) of an expression (Definition 6.8.1)
\(({'a} : {'b}) \mathrel{@} P\)	lifetime `'a` outlives `'b` from point \(P\) (Definition 6.8.5)
\(\lvert \tau \rvert\), \(D_C\,\alpha\)	the erasure of a type; the dictionary type of class \(C\) (Definitions 6.9.3, 6.9.5)

Technique map¶

Family	Techniques (origin)	Lesson
Foundations	typing judgments, inference rules and derivations (Church 1940; Martin-Löf; Cardelli 1996); type safety by progress and preservation (Wright & Felleisen 1994), after Milner 1978	6.1
Classification	static vs dynamic checking and the undecidability that makes static checking conservative (Rice 1953); strong vs weak typing as trapped vs untrapped errors (Cardelli 1996); sound vs intentionally unsound systems (TypeScript; Java's covariant arrays)	6.2
Syntax-directed checking	bottom-up checking with an error type (Algol 68, Pascal, C); implicit conversions and promotion (C11 §6.3.1.8, JLS ch. 5; coercions, Reynolds 1980, Breazu-Tannen et al. 1991); overload resolution by conversion ranking (C++, Java's three phases, Swift)	6.3
Bidirectional typing	synthesis and checking modes (Pierce & Turner 2000; Dunfield & Krishnaswami 2013, 2021); local type inference and target typing (Pierce & Turner 2000; Java, C#, Scala, TypeScript)	6.4
Subtyping	structural and algorithmic subtyping with records, functions, top and bottom (Cardelli 1984/1988); variance, declaration-site vs use-site (Scala, Kotlin, C#; Java wildcards, Igarashi & Viroli 2002, Torgersen et al. 2004); nominal vs structural (Java, Featherweight Java 2001; TypeScript, Go)	6.5
Flow-sensitive typing	occurrence typing (Tobin-Hochstadt & Felleisen 2008, 2010; mypy, Pyright); control-flow narrowing (TypeScript) and smart casts with stability (Kotlin)	6.6
Gradual typing	consistency and cast insertion (Siek & Taha 2006); the gradual guarantee (Siek et al. 2015); blame (Wadler & Findler 2009) and the cost of sound boundaries (Takikawa et al. 2016)	6.7
Places and references	l-values, places and categories (C, C++ value categories, Rust); exclusivity (Swift SE-0176, Pebble E0414); borrow checking with non-lexical lifetimes (Rust RFC 2094) and Polonius	6.8
Implementing generics	monomorphization (C++ templates, Rust); erasure and uniform representation (GJ, Bracha et al. 1998; ML); dictionary passing and witness tables (Wadler & Blott 1989; Swift)	6.9

flowchart LR
  subgraph FOUND[Foundations]
    J[Judgments and derivations] --> PP[Progress + preservation<br/>Wright-Felleisen 1994]
  end
  subgraph CLASS[Classification]
    SD[Static vs dynamic] --- SW[Strong vs weak] --- SU[Sound vs unsound]
  end
  subgraph ALG[Checking algorithms]
    SYN[Syntax-directed<br/>+ error type] -->|add modes| BID[Bidirectional<br/>Pierce-Turner 2000]
    BID -->|omitted type args| LTI[Local inference]
    SYN --- CONV[Conversions, overloading]
  end
  subgraph SUB[Subtyping]
    DEC[Declarative + S-Trans] -->|eliminate transitivity| ASUB[Algorithmic<br/>Cardelli 1988]
    ASUB --> VAR[Variance]
    NOM[Nominal] --- STR[Structural]
  end
  subgraph FLOW[Flow-sensitive]
    OCC[Occurrence typing<br/>2008, 2010] --- NAR[Narrowing, smart casts]
  end
  subgraph GRAD[Gradual]
    CONS[Consistency, casts<br/>Siek-Taha 2006] --> BL[Blame<br/>Wadler-Findler 2009]
  end
  subgraph REFS[Places]
    PL[Places] --> EX[Exclusivity<br/>SE-0176] --> BC[NLL borrow check<br/>RFC 2094, Polonius]
  end
  subgraph GEN[Generics]
    MONO[Monomorphization] --- ERA[Erasure] --- DICT[Dictionaries]
  end
  J --> SYN
  PP -. what soundness means .-> SU
  BID -->|mode switch becomes subsumption| ASUB
  ASUB -->|unions| NAR
  SU -. an unsound escape hatch, checked .-> CONS
  BID --> PL
  NAR -. dataflow, Ch 14 .-> BC
  VAR --> ERA
  LTI -. Ch 7: full inference .-> DICT

Who uses what¶

System	Technique	Notes
Clang/LLVM 23	syntax-directed checking with `RecoveryExpr`; usual arithmetic conversions and implicit-cast nodes (`SemaExpr.cpp`); overload ranking (`SemaOverload.cpp`); value categories (`ExprClassification.cpp`); template instantiation (monomorphization)	Lessons 6.3, 6.8, 6.9
rustc 1.94	bidirectional checking with `Expectation` (`rustc_hir_typeck`); coercions at expected types; NLL borrow checking on MIR (`rustc_borrowck`); monomorphization collector	Lessons 6.4, 6.8, 6.9
javac 21	bottom-up attribution with poly expressions and target typing (`Attr.java`); three overload phases; nominal subtyping with use-site variance (`Types.java`); erasure and casts (`TransTypes.java`)	Lessons 6.3–6.5, 6.9
HotSpot JVM	covariant-array store checks; display-based subtype checks	Lessons 6.2, 6.5
tsc 5.9	structural subtyping, bivariant methods, covariant arrays (intentionally unsound); control-flow narrowing (`getFlowTypeOfReference`); `any` without casts	Lessons 6.2, 6.5–6.7
mypy 1.19 / Pyright 1.1	occurrence typing for `isinstance`/`is None`; `Any` consistent with every type, erased at run time	Lessons 6.6, 6.7
Kotlin 2.2	smart casts for stable variables; declaration-site variance (`in`/`out`)	Lessons 6.5, 6.6
Swift 6	bidirectional constraint solving; exclusivity enforcement (static + dynamic); witness tables and specialization	Lessons 6.4, 6.8, 6.9
GHC 9.4	dictionary passing in Core; specialisation; `unsafeCoerce` as the documented hole	Lessons 6.1, 6.9
Typed Racket, beartype	occurrence typing; sound boundaries with blame / first-order boundary checks	Lessons 6.6, 6.7
`pebblec`	bidirectional checking with the literal rule, `let` inference, the error type, places, reference arguments and the exclusivity rule E0414	Exercises

Comparison¶

Every row is the corresponding lesson's §8 row.

Technique	Power / precision	Speed (asymptotic · practical)	Output / error quality	Implementation effort	Typical use
Typing judgments and derivations	Defines exactly the well-typed programs; syntax-directed rules give unique types (Theorem 6.1.10) and a checking algorithm for free (Theorem 6.1.11)	\(\Theta(n)\) with interned types · negligible in compilers	A failed premise names the rule and the subterm: the natural error location	Low for syntax-directed rules; a separate algorithm for declarative ones	Every language specification and type-system paper; the structure of every checker
Syntactic type safety (progress + preservation)	Guarantees no stuck states for all well-typed programs (Corollary 6.1.17); scales to state and exceptions [WF94]	A proof, not an algorithm; bounded enumeration finds counterexamples in 0.1 s (drill)	Pinpoints the lemma a bad rule breaks	High by hand for real languages (hundreds of cases); routine in proof assistants	Language design (Wasm, Java/FJ, ML), validating rule changes
Static checking	Rejects every program that could go wrong, and some that could not (Theorem 6.2.2)	\(O(n)\) at compile time · no run-time cost	Errors before running, at the offending subterm, on every path	Rules + checker (Lessons 6.3–6.4)	C, Java, Rust, Swift, Haskell, Pebble
Dynamic checking	Exact: only executed errors are reported (Proposition 6.2.9)	\(\Theta(k)\) tag checks at run time · JITs remove most	Errors only on executed paths, at the failing operation (often far from the mistake)	Tags on values, checks in every primitive	Python, JavaScript, Lisp, Ruby
Strong typing	No untrapped errors and no silent cross-type conversions	Checks at run time or compile time as above	Mix-ups become errors	Low once conversions are explicit	Python, Rust, Pebble
Weak typing	Untrapped errors or implicit conversions accepted (Proposition 6.2.10)	Conversions cost per operation; UB costs nothing until it bites	Mix-ups produce wrong values silently	Lowest for the language implementer	C (untrapped), JavaScript (conversions)
Sound type systems	The promise holds for all well-typed programs (Definition 6.2.7)	Sometimes needs run-time checks (Algorithm 6.2.8)	No surprises at run time for the excluded errors	Higher: every convenient rule must be justified	Java (modulo casts/arrays checks), Rust safe code, Haskell, Pebble
Intentionally unsound systems	Accepts documented programs that fail (TS arrays, method bivariance)	No checks needed	Occasional run-time type errors despite a clean compile	Lower; more JavaScript idioms type-check	TypeScript, Dart 1, Eiffel (catcalls)
Syntax-directed checking	Types flow only upward: unannotated λs, `[]`, overloaded literals need help from above	\(\Theta(n)\) · negligible	Local errors at the failing premise; one per root cause with the error type (Proposition 6.3.9)	Lowest: one post-order walk	C, Pascal, Go, Java (most forms), the Dragon book's checker
Implicit conversions and promotion	Mixed arithmetic "just works"; not coherent in C (Proposition 6.3.12), not value-preserving (Proposition 6.3.11)	\(O(1)\) per operator at compile time; conversions cost instructions at run time	Silent value changes; warnings are heuristic	Low for C's table; high to keep coherent	C, C++, Java, JavaScript; not Rust, Swift, Go, Pebble
Overload resolution by ranking	One name for many types; ambiguity is an error (Theorem 6.3.13)	\(\Theta(c \cdot k)\) per call; templates make it costly	Ambiguity/no-viable errors list candidates; hard to read with many overloads	High (ranking rules, ADL, templates)	C++, Java (phases), C#, Swift (joint solving)
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
Structural subtyping (algorithmic)	Width, depth, permutation, contravariant parameters, top and bottom; equals the declarative rules (Theorem 6.5.13)	\(O(\lvert S \rvert + \lvert T \rvert)\) with hashed labels · cached per type pair in practice	Explains the failing path ("types of parameters … are incompatible")	Low for the algorithm; joins/meets and recursion add effort	TypeScript, OCaml objects, Go interfaces, Scala structural types, the lab's L4
Variance of generics	Covariance for producers, contravariance for consumers, invariance for mutable containers (Theorem 6.5.15)	Linear declaration check; wildcard subtyping undecidable in general [Gri17]	Declaration-site: errors at the declaration; use-site: at each use, with capture variables	Medium (declaration-site), high (use-site with capture)	Scala, Kotlin, C# (declaration-site); Java (use-site); Rust (inferred)
Nominal subtyping	Only declared relations; abstraction boundaries enforced (Proposition 6.5.16)	\(O(h)\), \(O(1)\) with displays at run time	"X cannot be converted to Y" names both types	Low	Java, C#, Swift, C++, Kotlin, Rust traits (nominal impls)
Structural typing (whole types)	Any matching shape is accepted; unrelated code interoperates	As algorithmic subtyping	Accepts accidental matches (meters for seconds)	Low; branding for nominal needs	TypeScript, Go interfaces, OCaml, Elm records
Occurrence typing	Refines variables (and paths into data) by arbitrary boolean combinations of predicates; sound (Theorem 6.6.6)	Linear with normalized propositions; DNF blow-up in the worst case	Types at each occurrence are explainable by the guarding tests	Medium: propositions in every typing judgment	Typed Racket, mypy/Pyright (`isinstance`, `is None`)
Control-flow narrowing and smart casts	Exact for single-variable tests on loop-free code (Theorem 6.6.7); follows statements (early returns, assignments); Kotlin adds stability for soundness (Theorem 6.6.8)	\(O(n \cdot \lvert \mathcal{P} \rvert)\); per-reference on demand in TypeScript	Errors show the narrowed union; Kotlin names why a cast is impossible	Medium–high: a flow graph and caching	TypeScript, Kotlin, Swift (`if let`), C# nullable references, Flow
Gradual typing	Accepts every fully static and every fully dynamic program; static programs are typed exactly as before (Theorem 6.7.8); removing annotations never breaks a program (Theorem 6.7.7)	Checking linear; the run-time cost depends on whether casts are inserted	Static errors only where types are known to clash; the rest deferred to run time	Low for the checker (consistency for equality), high for sound run-time casts	TypeScript, mypy/Pyright, Typed Racket, C# `dynamic`, Dart before 2.0
Blame and the cost of soundness	Sound: typed code never sees an ill-typed value, and failures name the boundary (Theorem 6.7.8, [WF09])	\(O(1)\) first-order checks, wrappers for functions; whole-program slowdowns up to orders of magnitude [TFGNVF16]	Blame names the boundary and, with polarity, which side broke it	High: wrappers, representation of injected values, space-efficient casts	Typed Racket (contracts), beartype-style boundary checks; erased in TypeScript and mypy
L-values and places	Decides where storage is needed and whether it may be modified; sound for `&mut` arguments (Theorem 6.8.9)	\(O(n)\) with the type checker	Separates "not a place" from "not mutable", with a note at the declaration	Low: one more attribute per expression	Every compiler: C/C++ value categories, Rust places, Pebble §9.1
Exclusivity	Conservative per-call rule on roots; no aliasing between a `&mut` parameter and others (Theorem 6.8.10); rejects disjoint elements	\(O(k \cdot s)\) per call	Points at the conflicting occurrence and the `&mut` it conflicts with	Low for calls on roots; medium for field-sensitive or dynamic enforcement	Swift (static + dynamic), Pebble E0414, Rust's `&mut`
Borrow checking with non-lexical lifetimes	References may be stored, returned and copied; accepts until the last use (Theorem 6.8.11); Polonius accepts more	Fixed point over regions + bit-vector dataflow; linear-ish in practice	Borrow, conflicting access and later use, each labelled	High: MIR, liveness, region inference, two-phase borrows	Rust (NLL since 2018, Polonius in development)
Monomorphization	Generic code as fast as specialized code; needs a finite instance set (Theorem 6.9.7): no polymorphic recursion, no run-time instantiation	Best run time; code size and compile time grow with instances (exponential worst case)	C++ templates report errors per instance (deep instantiation backtraces); Rust checks the generic body once, before instantiation	Medium: substitution + collector; the optimizer does the rest	C++, Rust, Swift/GHC specialization, Go (partly, by GC shape)
Erasure and uniform representation	One copy; old and new code interoperate; no primitive type arguments and no run-time type arguments	Casts and boxing at run time; the JIT removes many	Errors at the generic definition; heap pollution warnings for unchecked code	Low in the compiler (Algorithm 6.9.4), no VM changes	Java, Kotlin/JVM, Scala, OCaml, Haskell values
Dictionary passing and witness tables	One copy; polymorphic recursion, separate compilation and run-time instantiation all work	An indirect call per method; specialization recovers speed where applied	Errors at the definition, in terms of constraints	Medium: dictionaries, coherence, metadata for unboxed values (Swift)	Haskell, Swift, Rust `dyn Trait`, Go interfaces

Comparison-lab results (reproduce with build/<preset>/bin/ch06-bidir-measure labs/ch06-bidir/corpus; reference solutions): of the 32 annotations written in the 12 well-typed corpus programs, the syntax-directed checker needs 24 and the bidirectional one 9; on the 10 ill-typed programs, the bidirectional checker reports the error at the position of the actual mistake in all 10 cases, the syntax-directed one in 5. ★ L4: the algorithmic subtype check agrees with the brute-force declarative closure on all 180 625 pairs of types of up to 4 nodes (10 061 subtypes). ★ L5: every well-typed corpus program and 200 random programs keep their value when all their annotations are replaced by ?. On a generated 132 002-line Pebble program, pebblec --emit=typed-ast (resolution, type checking and flow checks) takes 0.56–0.61 s against 0.42–0.44 s for parsing alone (Lesson 6.1 §5).

Route through this chapter¶

Step	What	Techniques	How it is exercised
1	Lesson 6.1	judgments, derivations, progress and preservation	drills `typing-derivation`, `progress-preservation`; quiz
2	Lesson 6.2	static/dynamic, strong/weak, sound/unsound	quiz; flashcards
3	Lesson 6.3 and Exercises E1, E2, E6	syntax-directed checking, conversions, overloading	`ch06.Types.E1_`, `E2_`, `E6_*`; lab L1
4	Lesson 6.4 and Exercise E3	bidirectional checking, local inference	drill `bidir-modes`; `ch06.Types.E3_*`; lab L2–L3
5	Lesson 6.8 (places and exclusivity) and Exercises E4, E5	places, reference arguments, exclusivity	`ch06.Types.E4_`, `E5_`, lit goldens
6	Comparison lab `labs/ch06-bidir/` L1–L3	syntax-directed vs bidirectional	lab tests + `ch06-bidir-measure`
7	Lesson 6.5	subtyping, variance, nominal vs structural	drill `subtype-query`; lab L4 ★
8	Lesson 6.6	occurrence typing, narrowing, smart casts	drill `narrowing`; quiz
9	Lesson 6.7	gradual typing, blame	lab L5 ★; quiz
10	Lesson 6.8 (borrow checking)	NLL, loans in scope, Polonius	quiz
11	Lesson 6.9	monomorphization, erasure, dictionaries	quiz; flashcards
12	Theory test	all	`./course quiz 6` (≥ 80 % to finish)

Practice and check¶

./course drill typing-derivation --difficulty easy     # warm up; --solution shows every step
./course drill progress-preservation
./course drill bidir-modes
./course drill subtype-query
./course drill narrowing
./course flash 6                                       # daily, a few minutes
./course quiz 6                                        # after the lessons
./course test 6                                        # after the exercises and the lab
./course status                                        # done = quiz ≥ 80 % and tests pass

References¶

The chapter's annotated bibliography — papers, textbook sections, pinned source files, docs — is in references.md. Start with: [TAPL] (Ch. 8–9 and 15–16: safety and subtyping), [WF94] (progress and preservation), [PT00] and [DK21] (bidirectional typing), [ST06] and [SVCB15] (gradual typing), [RFC2094] (non-lexical lifetimes) and [WB89] (type classes as dictionaries).