Semantic Analysis
& Type Systems

The parser handed us a tree that is syntactically legal. This deck makes it meaningful: every identifier bound, every operation type-checked, every static rule the grammar couldn't express now enforced.

Parsing answers “is this a sentence of the grammar?” Semantic analysis answers “does this sentence mean anything sensible?” It is the last phase of the front end — its output is an annotated, type-checked AST plus a populated symbol table.

Once this phase signs off, the rest of the compiler may assume the program is meaningful — IR generation never re-checks a type.

A language's semantics — what programs mean — splits into what can be decided before the program runs and what only emerges as it runs.

Every snippet below is a perfectly valid parse tree — grammatically flawless. Each is rejected only by semantic analysis, because the offending property is context-sensitive.

int main(void) {
    y = 3;            // undeclared 'y'
    int x = "hello";  // type error: char* → int
    int x = 7;        // redeclaration of 'x'
    foo(1, 2);        // arity: foo takes 1 arg
    return;           // missing return value
}

The symbol table maps names to everything the compiler knows about them. Lookups must be fast and frequent, so it is usually a hash table — or a stack of them, one per scope.

struct Symbol {
  std::string  name;
  Kind         kind;   // Var, Func, Type, ...
  Type*        type;
  int          scopeLevel;
  Location     loc;    // offset / reg / addr
  Attrs        attrs;  // const, mut, visibility
};

// A scope is one hash table; scopes nest.
struct Scope {
  std::unordered_map<std::string, Symbol> table;
  Scope* parent;   // enclosing scope (or null)
};

Symbol* lookup(Scope* s, const std::string& n) {
  for (; s; s = s->parent)
    if (auto it = s->table.find(n); it != s->table.end())
      return &it->second;   // first hit wins → shadowing
  return nullptr;            // undeclared
}

Nested blocks form a tree of scopes. At any point the live scopes are a stack, root at the bottom. lookup walks the stack outward; the innermost binding wins — that is shadowing.

The two x bindings coexist; the reference resolves to whichever scope is nearer on the stack.

Binding connects each use of a name to the declaration it refers to. Resolution is the algorithm that finds that declaration — and the rules for it are surprisingly subtle.

Knuth (1968) gave a formal way to attach meaning to a grammar: decorate each production with attributes and semantic rules that compute them. This is the theory behind syntax-directed translation.

In practice few compilers run a full attribute-grammar engine; they hand-write tree walks. But the vocabulary — what flows up, what flows down, and the legal dependency order — is exactly how we reason about an AST traversal.

Attaching a synthesized .type attribute to an expression grammar gives a one-pass bottom-up type-checker. Each rule combines its children's types into its own.

E → E1 + E2   { E.type =
                  unify(E1.type, E2.type) }
E → E1 * E2   { E.type =
                  numeric(E1.type, E2.type) }
E → ( E1 )    { E.type = E1.type }
E → num       { E.type = int }
E → real      { E.type = float }
E → id        { E.type =
                  lookup(id.name).type }

The product of type checking is a typed AST: every expression node carries a resolved type, every identifier a pointer into the symbol table, and implicit conversions are made explicit as Coerce nodes.

A type system is a tractable, syntactic method for proving the absence of certain bad behaviours by classifying values. Languages sit at different points on several independent axes.

Milner's 1978 slogan is the promise a type system makes: if the checker accepts a program, certain run-time errors cannot happen. Soundness is proved as two lemmas.

Type rules are written as inference rules: premises above the line, conclusion below. The judgement Γ ⊢ e : τ reads “in context Γ, expression e has type τ”. Γ is the typing environment — the symbol table, formally.

Type if b then x else 0 in context Γ = { b : bool, x : int }. We compose the rules into a derivation tree — leaves are axioms, the root is the goal.

The rules above need types written down. Hindley–Milner (HM) reconstructs them: with no annotations it finds the most general type, if one exists. Discovered independently by Hindley (1969) and Milner (1978); Milner's Algorithm W is the implementation.

-- No annotations anywhere...
compose f g x = f (g x)
-- W infers the principal type:
-- compose :: (b -> c) -> (a -> b) -> a -> c

twice f x = f (f x)
-- twice :: (a -> a) -> a -> a

id x = x
-- id :: a -> a   (a is a fresh type variable)

Unification (Robinson, 1965) is HM's engine: given two type terms, find the most general substitution making them equal — or fail. It solves the equality constraints W generates.

unify(t1, t2):
  t1, t2 = resolve(t1), resolve(t2)   # follow bound vars
  if t1 == t2:                  return            # done
  if t1 is a var α:    occurs_check(α, t2)
                       bind α := t2;  return
  if t2 is a var β:    occurs_check(β, t1)
                       bind β := t1;  return
  if t1 = C(a1..an) and t2 = C(b1..bn):  # same constructor
       for i: unify(ai, bi)              # arity must match
       return
  fail("cannot unify " + t1 + " with " + t2)

Infer the type of apply f x = f x. Give fresh variables, generate the one constraint f imposes, and unify.

f : α          x : β        (fresh)
apply : α → β → γ           (γ fresh, result)

the call  f x  demands:
   α  =  β → γ        ← f used as a function

unify(α, β → γ):
   α is a var, occurs-check(α, β→γ) ✓ (α ∉ β→γ)
   bind  α := β → γ

substitute back:
   apply : (β → γ) → β → γ
generalise free vars β, γ →  ∀β γ. ...

   apply :: (b -> c) -> b -> c     ✓ principal

HM's polymorphism lives at let. When a binding is generalised, its free type variables are closed over into a type scheme ∀α. τ — each use then gets fresh copies (instantiation).

let id = \x -> x in
  (id 3, id True)
-- id generalised to  ∀a. a -> a
-- use 1: instantiate a := Int   → id 3
-- use 2: instantiate a := Bool  → id True
-- BOTH type-check ✓

-- λ-bound params are NOT generalised:
\id -> (id 3, id True)   -- TYPE ERROR
-- one monomorphic α can't be both Int and Bool

Subtyping S <: T means an S may stand in wherever a T is expected (Liskov substitution). The hard question: how does subtyping lift through type constructors?

“Polymorphism” — one name, many behaviours — comes in distinct flavours (Strachey, Cardelli–Wegner). Each is resolved differently by the checker.

Beyond accepting or rejecting, the checker sometimes inserts work: implicit conversions that bridge nearly-compatible types — the source of much convenience and many bugs.

Type checking is the headline, but the same phase runs a battery of other flow-sensitive analyses — many are small dataflow problems over the AST/CFG.

These reuse the symbol table and run as AST/CFG traversals — the attribute-grammar machinery from earlier, applied to control flow rather than types.

The richest semantic checks push the type system to encode memory safety, resource ownership and even logical specifications.

A type system is only as good as its error messages. The cruel irony: the more inference a system does, the harder good diagnostics become — the error surfaces far from its cause.

// Elm / Rust set the bar: span-precise, fix-it
error[E0308]: mismatched types
  --> src/main.rs:3:18
   |
 3 |     let x: i32 = "hello";
   |            ---   ^^^^^^^ expected `i32`,
   |            |             found `&str`
   |            expected due to this
   = help: try parsing with `.parse()`