--- title: Type Systems url: https://doc.liz6.com/en/compilers/03-semantic-analysis/02-type-systems locale: en area: compilers tags: - compilers - semantic-analysis date: 2026-06-30 modified: 2026-07-19 description: 'Type checking is the compiler’s static verification of a program—proving that no type errors will occur before runtime. From simple equality checks to Hindley-Milner inference, subtyping and variance, to the two paths of generics: monomorphization and type erasure.' --- # Type Systems > Type checking is the compiler’s static verification of a program—proving that no type errors will occur before runtime. From simple equality checks to Hindley-Milner inference, subtyping and variance, to the two paths of generics: monomorphization and type erasure. ## Overview [Symbol Tables and Scopes](/compilers/03-semantic-analysis/01-symbol-tables-and-scopes.md) solves "which definition does this name refer to?" The type system solves the next layer: **can the types of these names be legally combined**? Can `x` and `y` in `x + y` be added? Do the argument types in `f(a)` match? Type checking is the process of making judgments; type inference is the automatic completion of omitted type annotations. This article follows the difficulty gradient of "simple type checking → HM inference → subtyping → generics" to clearly explain the engineering implementation of types. ## Type Checking: Validating Every Subtree Type checking proceeds bottom-up on the AST: ``` typecheck(expr): match expr: Number(n) → Int Binary(op, left, right) → t_left = typecheck(left) t_right = typecheck(right) if op is '+' and t_left == Int and t_right == Int: return Int else: report_type_error("cannot add {t_left} and {t_right}") Variable(name) → lookup(name).type ← get type from symbol table Call(func, args) → t_func = typecheck(func) if t_func is not Function: error for (arg, param_type) in zip(args, t_func.params): t_arg = typecheck(arg) if t_arg != param_type: error return t_func.return_type ``` The skeleton is extremely simple: recursively traverse the AST, and for each node, verify that the types of its children match the node's type rules. The real complexity lies in **type representation** (how internal structures of types—functions, generics, algebraic types—are stored), **type equivalence** (what it means for two types to be "the same"—structural vs. nominal equivalence), and **generic instantiation** (behavior of `List` when `T=Int`). ### Type Representation The type system uses an AST-like data structure internally to represent types: ```rust enum Type { Int, Float, Bool, String, Function(Vec, Box), // params → return_type Struct(String, Vec<(String, Type)>), // name + fields Enum(String, Vec<(String, Vec)>), // name + variants TyVar(u32), // type variable, identified by a unique ID (O(1) comparison) Apply(Box, Vec), // generic instantiation: List } ``` It is recursively defined—`Function` parameters and return types are `Type`s, and `Apply(List, [Box])` can be nested (e.g., `Map>`). ### Type Equivalence: Structural vs. Nominal When are two types "the same"? - **Structural equivalence**: "Same shape means same type." `struct { x: Int, y: Float }` is the same type as `struct { x: Int, y: Float }`, even if they are defined in different modules. Go and TypeScript use this. The downside: two types that happen to be isomorphic but semantically completely different (e.g., `Point{x,y}` and `Vector{x,y}`) are treated as the same type. - **Nominal equivalence**: "Same name means same type." `Point{x:Int, y:Float}` and `Vector{x:Int, y:Float}` are different types. Rust, Java, and C++ use this. During type checking, the comparison is against a pair of types' "structured names" rather than field-by-field comparison. Nominal equivalence is safer (preventing semantic confusion) but requires additional mechanisms to express type constraints (such as Rust's trait bounds or Java's `extends`) to support generic inference. ## Hindley-Milner Type Inference: Checking Without Writing Types HM is the foundation of type inference for ML-family languages (OCaml, Haskell). Its core is **unification**: given two type expressions, determine if there exists a set of type variable substitutions that makes them equal. ``` Inference Process (Pseudocode): Generate a type variable for each node in the AST (e.g., t1, t2, ...) Apply type rules to nodes, generating constraints: Number(n) → t == Int x + y → t_x == Int, t_y == Int, t_result == Int if cond a b → t_cond == Bool, t_a == t_b, t_result == t_a Solve the constraint set — unification: For each equation t_i == t_j: If t_i is an unbound type variable, bind t_i → t_j If t_j is an unbound type variable, bind t_j → t_i If both sides are concrete types (e.g., Int and Float), check equality — if unequal, type error ``` Unification is deterministic—when an equation is encountered, it is replaced according to the rules, without needing backtracking or retries. HM Limitations: **Polymorphism is introduced only via `let`** (let-polymorphism—the `id` in `let id = fn x => x` is polymorphic, introducing generalization at the `let` binding; polymorphism of function arguments is determined automatically via type inference). This is due to HM's let-polymorphism rule: generalization occurs only at `let` bindings; lambda-bound variables are not generalized. This ensures **decidability** of inference—Hindley-Milner is guaranteed to derive the principal type for HM-valid programs within a finite number of steps, avoiding infinite loops. ## Subtyping: The Substitutability Principle When `Dog <: Animal` (Dog is a subtype of Animal), a position expecting an `Animal` can accept a `Dog`. Subtyping adds the concept that "type checking is not just a black-and-white comparison": - **Covariant**: `List <: List` if `Dog <: Animal`. This is safe only for **read-only** structures—e.g., Java's `List`. - **Contravariant**: `Fn(Animal) <: Fn(Dog)`. Function parameters are contravariant—a function that can consume an `Animal` can certainly consume a `Dog` (since `Dog <: Animal`, the set of Animals covers Dogs). Conversely, `Fn(Dog)` **cannot** substitute for `Fn(Animal)`—a function that can only consume Dogs cannot consume Cats, while a position expecting `Fn(Animal)` might pass a Cat. - **Invariant**: `Array` and `Array` are unrelated. For **read-write** structures (arrays are read-write), invariance is required—otherwise, if you put a `Cat` into `arr: Array`, an existing reference to `Array` would assume all elements are `Dogs`, breaking type safety. Rust is very restrained in its practical use of subtyping: **only lifetimes have a subtyping relationship** (`'static <: 'a`); all other types use nominal equivalence, with no structural subtyping. ## Generics: Different Implementations of Polymorphism How is code generated for generics (`List`) after compilation? ### Monomorphization Rust, C++, and Swift use this: generate a separate machine code instance for each actual type argument: ``` fn identity(x: T) → T // Generic definition (retained in IR) identity::(42) // Generate function body for identity_i32 identity::("hello") // Generate function body for identity_String ``` Advantages: Zero runtime overhead (direct calls, no indirection); independent optimization for each `T` (the compiler can inline or perform constant folding when it sees `T=i32`). Disadvantages: Code bloat—one instance per `T`. In practice, Rust places few restrictions on this due to effective deduplication (e.g., `Option` is generated only once). ### Type Erasure Java, Scala, and Kotlin use this: generics exist only at compile time—at runtime, all `List` become `List`: ``` List xs = ...; String s = xs.get(0); ← The compiler inserts an implicit cast: (String) xs.get(0) ``` Advantages: Only one copy of the code, no bloat. Disadvantages: Primitive types cannot be used directly as generics (`List` is illegal, must use boxed `List`); runtime overhead from casts and boxing. ## Traits/Typeclasses: Constrained Polymorphism Generic parameters need constraints: saying `T` must be "addable", "comparable", or "printable". Rust's traits and Haskell's typeclasses are expressions of such constraints. The compiler handles them as follows: - **Rust**: For `fn sum(xs: &[T]) → T`, during monomorphization, a separate `sum` is generated for each `T`. The call to `Add::add` in the parameters undergoes static dispatch—the specific implementation of `T::add` to jump to is determined at compile time. There is no vtable lookup. - However, when trait objects (`dyn Add`) appear, the compiler uses a vtable (virtual table)—a structure containing function pointers—for runtime lookup. The **Trait solver** is one of the most complex components in the Rust compiler. Its job: given `T: Add` and `Vec`, verify that all constraints are satisfiable—this is essentially a form of Prolog-style logic programming (the Chalk library translates Rust's trait rules into Prolog rules for solving). ## Trade-offs and Failure Modes - **Poor error messages when type inference fails**: When HM unification fails, it only knows "two types do not match," not "why"—producing "expected Foo, found Bar" without explaining "the function you called here expects Foo, and the x you passed is Bar because you assigned Bar to it three lines ago." → Modern compilers (like Rustc) record "constraint sources" during inference and backtrack along the constraint chain upon failure to generate diagnostic messages. - **Undecidable inference**: If features like GADTs, type families, or rank-N polymorphism are added outside of HM, type inference may become **undecidable**—the compiler might infer forever. → Add restrictions (Haskell requires type annotations for GADTs and type families; Rust restricts inference to function bodies, not across functions). - **Long compilation times due to monomorphization**: C++ templates and Rust generics can both cause compilation time explosions. → On-demand monomorphization (do not generate all theoretically possible instances), deduplication (generate only once for the same combination). ## References - **Pierce**: "Types and Programming Languages" (TAPL) — The standard textbook on type theory, covering simple types → subtyping → polymorphism → HM - **Dragon Book**: Chapter 6, Type Checking — Implementation of type checking in compilers - **Rust Chalk**: https://github.com/rust-lang/chalk — Logic programming implementation of the Rust trait solver *Keywords: type checking, type inference, Hindley-Milner, unification, type variable, principal type, subtyping, covariance, contravariance, invariance, monomorphization, type erasure, generic, trait, typeclass, vtable, static dispatch, dynamic dispatch, trait solver, nominal equivalence, structural equivalence, let-polymorphism*