Type Checking

Definition. Type checking is the semantic-analysis pass that verifies every operation in a program receives operands whose types are permitted by the language. It runs after parsing, on the AST.

After parsing, the program is structurally correct but may still be meaning-wrong. Adding two integers is fine; multiplying a pointer by a string is not. The type checker enforces those rules.

It takes the AST plus the symbol table (the compiler's dictionary of declared names and their types) and produces an annotated AST where every node carries a verified type.

Two more definitions

Type system — a set of rules that assigns a type expression (e.g. int, float, int → int, int[10]) to every construct in a program. A type checker implements a type system.

Type error — applying an operation to operands whose types the type system does not permit.

Type checking is syntax-directed. The checker attaches one synthesized attribute, type, to every AST node and computes it bottom-up: type the children first, then derive the parent.

The rule used above: if both children are int and the operator is +, the result is int.

Leaves that are identifiers have no children, so their type is looked up in the symbol table instead of synthesized.

This is exactly a post-order, S-attributed SDD walk of the AST.

Languages differ in when they check types.

Static type checking — types are checked at compile time, before the program runs. (C, Java, Go, Rust, TypeScript.)

Dynamic type checking — types are checked at run time, as each operation executes; values carry a type tag. (Python, JavaScript, Ruby, Lisp.)

Example — same bug, different time:

Three properties describe how strict a type system is. They are independent of static vs. dynamic.

Strongly typed — the language never silently reinterprets a value's bits as another type.

Weakly typed — implicit reinterpretations are allowed.

Strength is independent of timing: Python is strongly but dynamically typed.

Sound — a type system is sound if well-typed programs cannot go wrong: if a program passes the static checks, no type error can happen at runtime.

Why soundness matters: a sound, static system needs no runtime type checks for the properties it guarantees, so it can emit faster code.

A type system is specified as type rules, each written like a logical inference rule.

Read it as "if all premises hold, the conclusion holds." The form ⊢ e : T means "expression e has type T."

Example 1 — integer addition:

To check a + 2 where a : int: left is int (premise 1), right is int (premise 2), so a + 2 : int.

Example 2 — if-else:

The condition must be boolean — not merely "truthy".

Example 3 — assignment:

The RHS type must equal x's declared type.

Each rule maps directly to one case in the recursive checkType function — that is why the notation is useful.

Type synthesis — compute a node's type bottom-up from its sub-expression types, using the type rules. Requires that variables are declared (it looks them up). This is what C and Java do.

Type inference — the programmer writes no annotations; the compiler deduces types from usage. (ML, Haskell, parts of Rust/TypeScript, via the Hindley-Milner algorithm.)

This course focuses on synthesis; full inference is an advanced topic.

Error handling: the type_error type

When a rule fails, the checker must not crash. It assigns the special type type_error to the bad node and keeps going (so it can report many errors in one pass).

Key rule. If any operand has type type_error, the result is also type_error — and no new error is reported.

This stops one real error from cascading into spurious follow-on errors.

Next topic: Type Checking — Expressions, Statements, and Functions works through the concrete rules, coercions (int → float), and annotated-AST examples for each construct.

• Type checking (semantic analysis) verifies every operation gets operands of permitted types. A type system is the rule set; a type checker implements it.

• It is syntax-directed: a type synthesized attribute computed bottom-up, with the symbol table supplying identifier types — an S-attributed SDD.

• Static = checked at compile time (C, Java, Rust); dynamic = checked at run time (Python, JavaScript).

• Strong = no silent reinterpretation; weak = implicit casts allowed; sound = well-typed programs cannot go wrong (so no runtime checks needed). Strength is independent of timing — Python is strong but dynamic.

• Type rules are inference rules (premises over a line, conclusion below); each maps to one case in checkType.

• Synthesis computes types bottom-up from declarations (C, Java); inference deduces them from usage (Hindley-Milner: ML, Haskell).

• On a failed rule, assign type_error and propagate it silently upward to avoid a cascade of spurious messages.