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 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<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>
}

It is recursively defined—Function parameters and return types are Types, 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 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<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 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<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 reference to Array<Dog> 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<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 function body for identity_i32
identity::<String>("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<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);     ← 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<int> is illegal, 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", or "printable". Rust's traits and Haskell's typeclasses are expressions of such constraints. The compiler handles them as follows:

• Rust: For fn sum<T: Add>(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<Output = T> and Vec<T>, 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