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, to subtyping and variance, and finally to the two paths for generics: monomorphization and type erasure.

Overview

Symbol Tables and Scopes 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, while 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                 ← fetch 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 to store internal structures of types—functions, generics, algebraic types), type equivalence (what it means for two types to be "the same"—structural vs. nominal equivalence), and generic instantiation (behavior of List<T> when T=Int).

Type Representation

The type system uses an AST-like data structure internally to represent types:

enum Type {
    Int,
    Float,
    Bool,
    String,
    Function(Vec<Type>, Box<Type>),    // params → return_type
    Struct(String, Vec<(String, Type)>),  // name + fields
    Enum(String, Vec<(String, Vec<Type>)>),  // name + variants
    TyVar(u32),                        // Type variable, identified by a unique ID (O(1) comparison)
    Apply(Box<Type>, Vec<Type>),       // Generic instantiation: List<Int>
}

Recursive representation—Function parameters and return types are both Type, and Apply(List, [Box<Type>]) can be nested (e.g., Map<String, List<Int>>).

Type Equivalence: Structural vs. Nominal

When are two types "the same"?

• Structural equivalence: "Same structure 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, a pair of types' "structured names" are compared 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 the need for backtracking or retrying.

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 rules: generalization occurs only at let bindings; lambda-bound variables are not generalized. This ensures decidability of inference—Hindley-Milner is guaranteed to derive a 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 requiring Animal can accept Dog. Subtyping adds the concept that "type checking is not just a black-and-white comparison":

• Covariant: List<Dog> <: List<Animal> if Dog <: Animal. This is safe only for read-only structures—e.g., Java's List<? extends Animal>.
• Contravariant: Fn(Animal) <: Fn(Dog). Function arguments are contravariant—a function that can consume Animal can certainly consume 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<Dog> and Array<Animal> are unrelated. For read-write structures (arrays are read-write), invariance is required—otherwise, if you put a Cat into arr: Array<Animal>, an existing Array<Dog> reference would assume all elements are Dog, breaking type safety.

Rust is very conservative 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<T>) after compilation?

Monomorphization

Rust, C++, and Swift use this: generate a separate machine code instance for each actual type argument:

fn identity<T>(x: T) → T           // Generic definition (retained in IR)
identity::<i32>(42)                 // Generate the function body for identity_i32
identity::<String>("hello")         // Generate the function body for identity_String

Advantages: Zero runtime overhead (direct calls, no indirection); independent optimization for each T (the compiler can inline and perform constant folding when it sees T=i32). Disadvantages: Code bloat—one instance per T. In practice, Rust mitigates this with extensive deduplication (e.g., Option<i32> is generated only once).

Type Erasure

Java, Scala, and Kotlin use this: generics exist only at compile time—at runtime, all List<T> become List<Object>:

List<String> xs = ...;
String s = xs.get(0);     ← Compiler inserts an implicit cast: (String) xs.get(0)

Advantages: Only one copy of the code, no bloat. Disadvantages: Primitive types cannot be used as generics (List<int> is invalid, must use boxed List<Integer>); runtime overhead from casts and boxing.

Traits/Typeclasses: Constrained Polymorphism

Generic parameters need constraints: saying T must be "addable", "comparable", "printable", etc. Rust's traits and Haskell's typeclasses are expressions of such constraints. How the compiler handles them:

• Rust: For fn sum<T: Add>(xs: &[T]) → T, monomorphization generates a separate sum for each T. The Add::add call in the parameters is statically dispatched—the jump target to the specific implementation of T::add is determined at compile time. No virtual table lookup.
• However, when trait objects dyn Add appear, the compiler uses a vtable (virtual table)—a structure containing function pointers, looked up at runtime.

The Trait solver is one of the most complex components in the Rust compiler. Its job: given T: Add<Output = T> and Vec<T>, verify that all constraints are satisfiable—this is essentially a Prolog-style logic programming problem (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 don't 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 are added outside of HM (such as GADTs, type families, or rank-N polymorphism), 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 within 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 (not generating all theoretically possible instances), deduplication (generating the same combination only once).

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