Static vs Dynamic Typing

A type system, as established previously, assigns types to program expressions and restricts which operations are legal on which types. The question this article addresses is when the system enforces those restrictions. In static typing, a compiler (or a separate static type-checking pass) analyzes the program's source text and rejects programs containing type errors before any execution begins. The type of every variable and expression is, in principle, determined without running the program — this is why static typing is sometimes described as reasoning about the program's shape rather than its behavior. In dynamic typing, the language runtime attaches type information to values (not variables or expressions), and checks are performed at the moment an operation is about to execute, e.g., "is this value actually a number before I add it?" This distinction is orthogonal to another important axis: type safety. A language is type-safe if it never permits an operation on a value of the wrong type to silently produce a meaningless or undefined result — instead it must raise a well-defined error or reject the program outright. Static typing does not automatically imply safety (C's `union` types and pointer casts allow a statically typed but unsafe escape), and dynamic typing does not imply unsafety (Python raises a clean `TypeError` rather than corrupting memory). The safety axis is explored fully under Type Safety and Soundness; here we hold it fixed and focus purely on timing. A second precise distinction worth naming: static type systems are typically conservative. Because they must decide, without running the program, whether every possible execution path is well-typed, they necessarily reject some programs that would actually run correctly (the type checker cannot see everything a dynamic run would reveal). This conservatism is not a design flaw — it is a mathematical necessity, a direct consequence of the undecidability of runtime behavior in general (an instance of Rice's theorem: any nontrivial semantic property of programs is undecidable in general). Static type checkers approximate program behavior soundly but incompletely; dynamic type checking, by contrast, is exact for the single execution path actually taken, but offers zero guarantee about paths not yet exercised.

Static type checking operates as a compiler phase, positioned after parsing and typically producing or consuming an abstract syntax tree (AST). It assigns a type to every subexpression using a set of typing rules and a symbol table (environment) mapping variables to declared or inferred types, then verifies that every operation's operand types match what the operation requires. ``` function TYPECHECK(expr, env): match expr: case Literal(v): return typeof(v) // base case: int, bool, string, ... case Var(name): if name not in env: error "undefined variable " + name return env[name] // base case: lookup case BinOp(op, left, right): tL = TYPECHECK(left, env) tR = TYPECHECK(right, env) if not COMPATIBLE(op, tL, tR): error "type mismatch: " + op + " on " + tL + ", " + tR return RESULTTYPE(op, tL, tR) case If(cond, thenBranch, elseBranch): tC = TYPECHECK(cond, env) if tC != Bool: error "condition must be Bool, got " + tC tT = TYPECHECK(thenBranch, env) tE = TYPECHECK(elseBranch, env) if tT != tE: error "branches disagree: " + tT + " vs " + tE return tT case Func(param, paramType, body): env' = env EXTENDED WITH param : paramType tBody = TYPECHECK(body, env') return Arrow(paramType, tBody) case App(f, arg): tF = TYPECHECK(f, env) tArg = TYPECHECK(arg, env) if tF is not Arrow(tArg, _): error "cannot apply " + tF + " to " + tArg return tF.returnType case Let(name, valueExpr, body): tVal = TYPECHECK(valueExpr, env) env' = env EXTENDED WITH name : tVal return TYPECHECK(body, env') ``` This recursion terminates because it strictly decreases the size of the AST at every recursive call — the base cases (`Literal`, `Var`) have no subexpressions left to check. The algorithm runs once, entirely before execution; if it reports no errors, the program is accepted and compiled/executed, otherwise it is rejected outright and never runs at all.

Dynamic type checking instead defers this exact same question — "are these operand types compatible?" — to run time, and it checks values rather than static expressions: ``` function EVAL(expr, runtimeEnv): match expr: case Literal(v): return TaggedValue(v, typeof(v)) case Var(name): return runtimeEnv[name] // no static lookup — literally run case BinOp(op, left, right): vL = EVAL(left, runtimeEnv) vR = EVAL(right, runtimeEnv) if not COMPATIBLE(op, vL.tag, vR.tag): raise TypeError at RUNTIME // caught only if this line executes return APPLY(op, vL, vR) case If(cond, thenBranch, elseBranch): vC = EVAL(cond, runtimeEnv) if vC.tag != Bool: raise TypeError at RUNTIME if vC.value: return EVAL(thenBranch, runtimeEnv) else: return EVAL(elseBranch, runtimeEnv) case App(f, arg): vF = EVAL(f, runtimeEnv) vArg = EVAL(arg, runtimeEnv) if vF.tag != Closure: raise TypeError at RUNTIME return APPLYCLOSURE(vF, vArg) ``` The crucial structural difference: `TYPECHECK` walks the entire static structure of the program exactly once, including branches never taken at runtime — the `else` branch is checked even if the program only ever executes `then`. `EVAL` walks only the single dynamic execution path actually taken, and re-derives and re-checks type compatibility at every single operation, every time it executes — even inside a loop executed a million times.

Time complexity of static checking. For a syntax-directed type checker like the pseudocode above (no unification, all annotations explicit), each AST node is visited a constant number of times and does O(1) work (a table lookup and a comparison), so the total cost is O(n) in the size of the AST, `n`. If the language requires type inference (Hindley–Milner style, as in ML or Haskell), the checker must additionally solve a system of unification constraints; the classical algorithm is O(n · α(n)) with a union-find implementation in practice, though the worst-case complexity of full Hindley–Milner inference with let-polymorphism is known to be exponential (and even DEXPTIME-complete) in adversarially constructed programs due to nested generalization — a subtlety that matters for compiler engineers but is rarely observed in ordinary code. This static cost is paid once, at compile time, and is completely amortized away by the time the program executes even once.

Time complexity of dynamic checking. Each individual runtime type check (comparing a tag) is O(1), but the checks recur on every single execution of every operation, including inside loops and recursive calls. A dynamically typed loop executing an addition `n` times performs `n` runtime type checks, each with real cost: dereferencing a tagged value, branching on its tag, and dispatching to the correct implementation. This is why dynamically typed language implementations (CPython, MRI Ruby) are typically several times slower per operation than statically typed compiled code — the check that a static compiler pays for once is paid, at minimum, once per dynamic occurrence, and JIT compilers (V8, PyPy) exist substantially to try to recover this cost through runtime type specialization.

Space complexity. Static typing requires storing a symbol table during compilation — O(n) transient space, discarded after compilation, and it can erase type tags entirely from runtime representations (type erasure), yielding smaller and more cache-friendly runtime objects. Dynamic typing must keep a type tag attached to every value at runtime, permanently, adding a constant per-value overhead (commonly a machine word) that persists for the entire program's execution.

Correctness argument — what each discipline actually guarantees. The precise claim of a sound static type system is: if a program type-checks, then it will not encounter a type error at runtime — informally captured by the slogan "well-typed programs don't go wrong" (Robin Milner). This is proven, not merely observed, via two lemmas about the operational semantics of the language: 1. Progress — a well-typed expression is either a value or can take an execution step (it never "gets stuck"). 2. Preservation — if a well-typed expression takes a step, the result is still well-typed at the same type. By induction on the length of an execution, Progress + Preservation together imply that a well-typed program either runs forever, terminates with a value, or terminates cleanly — never with a stuck, type-confused operation. (This is exactly the machinery developed under Type Safety and Soundness.) Crucially, this guarantee covers every possible execution path, including ones a test suite never exercises. Dynamic typing offers a strictly weaker, path-local guarantee: if this particular execution reaches this particular operation, its runtime tags will be checked before the operation proceeds. Untaken branches receive no guarantee whatsoever until (if ever) they execute. The soundness of a dynamically checked language is therefore a statement about the runtime's per-operation checks being exhaustive and non-bypassable, not a statement about the whole program in advance.

Honest trade-off summary. Static typing buys a whole-program guarantee at the cost of conservatism (some correct programs are rejected) and annotation burden; dynamic typing buys unconditional flexibility (any value can flow anywhere) at the cost of deferring — sometimes indefinitely — the discovery of type errors, and at the cost of repeated runtime check overhead.

Consider a function intended to double a numeric value, implemented in a hypothetical language once statically and once dynamically, then traced against three calls. ``` // Static version (explicit types) function double(x: Int) -> Int { return x + x; } // Dynamic version (no annotations) function double(x) { return x + x; } ```

Two details matter here and are frequently missed. First, in the static language, `double(3.5)` is rejected even if that call site is inside a branch that never executes at runtime — for instance, `if (false) { double(3.5); }` — because static checking inspects the AST, not the trace. Second, in the dynamic language, `double("cat")` might not even be an error: many dynamically typed languages (Python, JavaScript) define `+` on strings as concatenation, so the "same" source code silently does something entirely different depending on the runtime tag of the argument — a flexibility that is a feature when intentional (generic, duck-typed code) and a bug when accidental (a typo passes a string where a number was meant). A second illustrative case: type-driven dispatch inside a loop, showing the repeated-cost argument concretely. ``` total = 0 for item in data: // data: mixture of Int and Float, 10^6 items total = total + item ``` In a statically typed language with a homogeneous array type `Array`, the compiler proves once, at compile time, that every `item` is `Int`, and the generated machine code for `total + item` is a single unchecked integer-add instruction, executed `10^6` times at native speed. In a dynamically typed language, `data` may hold a mixture of ints and floats; the runtime must inspect the tag of `item` on every one of the 10^6 iterations, branch to integer-add or float-add accordingly, and possibly re-box the result — the same asymptotic O(n) work, but with a materially larger constant factor per iteration, which is precisely why numerically intensive dynamic code is often rewritten in, or delegated to, statically typed/compiled libraries (NumPy's C core beneath Python is the canonical example).

Static typing underlies systems where correctness before deployment is paramount: aviation and automotive software (often written in statically typed, sometimes formally verified subsets of C or Ada), operating system kernels (C, increasingly Rust for its stronger static guarantees), and large-scale distributed systems at companies like Google and Meta, where Java, Go, and increasingly typed Python variants replace dynamic scripts as codebases and teams grow — the whole-program guarantee scales better across thousands of engineers who cannot mentally track every runtime path. Compilers for statically typed languages also enable aggressive optimizations (register allocation, inlining, dead-code elimination) that rely on knowing types in advance, which is one reason C, Rust, and Java-with-JIT achieve high throughput. Dynamic typing dominates rapid iteration contexts: data science and machine learning prototyping (Python, R), web scripting (JavaScript, PHP), and domains where the shape of data is only known at runtime, such as parsing arbitrary JSON or building flexible plugin architectures. The rise of gradual typing — TypeScript layered over JavaScript, Python's `typing` module and tools like `mypy`, Racket's Typed Racket — reflects industry's practical answer to this whole trade-off: let engineers add static guarantees incrementally to the parts of a codebase that need them (public APIs, critical business logic) while retaining dynamic flexibility elsewhere (glue code, experimental scripts), rather than forcing an all-or-nothing choice for an entire project.

Ask the tutor: How does gradual typing insert runtime checks at the boundary between statically and dynamically typed code to keep the whole system sound?