Part 3 · 1 chapters · ~8 min

Type Checking

Symbol tables and scopes, synthesising types bottom-up, checking against expected types, function signatures and calls, return-path checking, good error messages, type inference (unification and Hindley-Milner in outline), bidirectional checking as in TypeScript and Rust, and soundness.

Types computed bottom-up

code

// from src/checker.ts (abridged): the type of an expression, or an error with a position
function typeOf(e: Expr, scope: Scope): Type {
  switch (e.k) {
    case 'num': return 'int';
    case 'bool': return 'bool';
    case 'var': { const t = scope.lookup(e.name); if (!t) throw new CompileError(`unknown variable '${e.name}'`, e.line, e.col); return t; }
    case 'binary': {
      const l = typeOf(e.l, scope), r = typeOf(e.r, scope);
      if (['+', '-', '*', '/', '%'].includes(e.op)) {
        if (l !== 'int' || r !== 'int') throw new CompileError(`'${e.op}' needs two ints, got ${l} and ${r}`, e.line, e.col);
        return 'int';
      } …
    }
  }
}
// let x: int = 1 + true;   →   CompileError "1:16: '+' needs two ints, got int and bool"

Inference: this checker needs annotations on lets and functions. Hindley-Milner inference (ML, Haskell) assigns type variables and solves equations between them (unification), so no annotations are needed. TypeScript and Rust use bidirectional checking: infer where easy, require annotations at function boundaries.

WHAT THE CHECKER CHECKS

errors found before a single instruction runs

swipe the figure sideways, or tap expand for full screen

1/4

scopes

The checker keeps a stack of scopes (maps from names to types), pushed on blocks and functions, so shadowing and undeclared names are caught.

a stack of mapsundeclared names caught