What Is a Type System?

A type is a name for a set of values together with the operations that are valid on them. The type `Int` names the set of integers and licenses operations like addition and comparison; the type `String → Int` names functions that consume a string and produce an integer, such as a "length" function. Crucially, a type is a static, compile-time description — a prediction about what a piece of code will produce or accept — as opposed to the actual, concrete value that exists only once the program runs. A type system is the formal apparatus that assigns types to the pieces of a program (expressions, variables, functions) and checks that these assignments are mutually consistent. Formally, a type system is usually presented as a set of typing rules that define a relation ``` Γ ⊢ e : T ``` read "under context `Γ` (a mapping from variable names to their types), expression `e` has type `T`." The rules are inductive: the type of a compound expression like `e1 + e2` is derived from the types of its parts, `e1` and `e2`, plus a rule saying that `+` requires both operands to be numeric and yields a numeric result. If no rule applies — for example, if `e1` is a function and `+` has no rule for functions — the expression is ill-typed and the type system rejects the program. The core distinction that motivates all of this is between a type error and a runtime crash for other reasons (out of memory, disk failure) or a logic error (the program runs fine but computes the wrong business answer). A type system targets exactly the first category: it tries to guarantee that if a program passes its checks, it will never attempt an operation on a value of the wrong shape — never call a non-function, never access a field that doesn't exist, never treat a string as a number. This guarantee, when it can be proven, is called type soundness, popularly summarized as "well-typed programs don't go wrong."

Conceptually, a type system operates as an inference and checking procedure that walks the abstract syntax tree (AST) of a program — the same tree a compiler's parser produces — and computes or checks a type for every node, bottom-up. Two closely related jobs are usually distinguished:

• Type checking: given an expression and a claimed type, verify the claim is consistent with the typing rules.
• Type inference: given an expression with no annotations, work out its type (or report that none exists).

Both rely on the same typing rules; inference simply runs them "backwards," inventing placeholders for unknown types and solving constraints between them. The mechanics below sketch the checking direction, which is the conceptual core.

Step 1 — Build the context. Start with a typing context `Γ`, a table mapping already-known names (function parameters, previously declared variables) to their types.

Step 2 — Recurse over the syntax tree. For each subexpression, look up the relevant typing rule based on its syntactic shape (literal, variable reference, function application, arithmetic operation, conditional, etc.) and recursively determine the types of its subparts.

Step 3 — Apply the rule and check consistency. Each rule states required types for the subparts and computes the resulting type. If the required types don't match what was found, reject the program with a type error, pinpointing the offending subexpression.

Step 4 — Extend the context where necessary. Constructs that introduce new bindings (function definitions, `let` expressions) extend `Γ` for the scope in which the new name is visible.

Step 5 — Report success or failure. If every node receives a type with no rule violations, the whole program is well-typed and assigned the type of its outermost expression. Otherwise, the compiler reports the specific ill-typed location. ``` function typeOf(expr, context): match expr: case IntLiteral(n): return Int case BoolLiteral(b): return Bool case Variable(name): if name not in context: error("undefined variable: " + name) return context[name] case BinaryOp(op, left, right): tLeft = typeOf(left, context) tRight = typeOf(right, context) if op in {"+", "-", "*"}: require(tLeft == Int and tRight == Int, "arithmetic requires two Ints") return Int if op in {"==", "<", ">"}: require(tLeft == tRight, "comparison requires matching types") return Bool error("unknown operator: " + op) case If(cond, thenBranch, elseBranch): tCond = typeOf(cond, context) require(tCond == Bool, "condition must be Bool") tThen = typeOf(thenBranch, context) tElse = typeOf(elseBranch, context) require(tThen == tElse, "branches must have the same type") return tThen case FunctionDef(paramName, paramType, body): innerContext = context.extend(paramName, paramType) tBody = typeOf(body, innerContext) return Function(paramType, tBody) case Apply(func, arg): tFunc = typeOf(func, context) tArg = typeOf(arg, context) match tFunc: case Function(paramType, returnType): require(tArg == paramType, "argument type mismatch") return returnType case _: error("attempted to call a non-function") function require(condition, message): if not condition: error(message) ``` This tiny checker already demonstrates the essential machinery: types propagate upward from literals and variables, get combined by rules attached to each syntactic construct, and any mismatch is caught structurally — without ever running the program. Real type systems add generics, subtyping, inference of unannotated code, and much richer rules, but the recursive "walk the tree, check the rules, propagate the type" skeleton stays the same.

Time complexity. For the syntax-directed checker sketched above, each node in the AST is visited a constant number of times (once per rule application, occasionally consulting the context via a hash-map lookup), so checking runs in O(n) time for a program of `n` AST nodes, assuming type equality itself is O(1) (true for simple base types). Type systems with structural equality on large record or variant types can make equality checks O(size of type), and systems with full type inference (like Hindley–Milner, used in ML and Haskell) solve unification constraints; naive unification is close to linear in practice but has a theoretical worst case of exponential time in pathological cases due to the size of types after substitution, though this is essentially never observed on real programs. Systems with subtyping or generics can add polynomial overhead per comparison but remain, in practice, near-linear.

Space complexity. The typing context grows with the number of nested bindings in scope at once — O(depth of nesting) auxiliary space beyond the AST itself, plus O(n) to store inferred/checked types alongside each node if desired.

Correctness — what "sound" actually means. The central theorem type systems aim for is type soundness, traditionally split into two lemmas following the syntactic approach popularized in operational semantics:

• Progress: a well-typed expression that is not already a final value can always take an evaluation step — it never gets "stuck" (e.g., it never reaches a state like "try to call the number `5` as if it were a function," which has no defined next step).
• Preservation (a.k.a. subject reduction): if a well-typed expression takes an evaluation step, the result is still well-typed, with the same type.

Together, by induction on the number of evaluation steps: starting from any well-typed program, every step preserves well-typedness (Preservation), and every well-typed, non-final expression can always step (Progress) — so the program can never reach a stuck state. This is the formal content behind the slogan "well-typed programs don't go wrong": it is not a vague guarantee but an inductive proof obligation the language designer discharges once, for the whole language, covering infinitely many programs.

Honesty about tradeoffs. Soundness is a guarantee about a category of error, not about all errors. A sound type system will happily typecheck a program that divides by zero, loops forever, or computes the wrong tax rate — those aren't type errors. Also, every practical, decidable type system is incomplete in a precise sense: there exist programs that behave correctly at runtime but that the type system rejects anyway, because proving "this is always safe" in general is undecidable (a consequence of Rice's theorem). Type systems are therefore engineering compromises: they reject some good programs to guarantee they never accept a bad one, and different systems draw this line differently — which is precisely the design space explored by richer type systems (subtyping, generics, dependent types).

Consider a tiny function in a made-up language, checked against the rules above: ``` function average(x: Int, y: Int) -> Int: (x + y) / 2 ``` Suppose it is called as `average(4, "oops")`. Trace the type checker:

The checker never executes `(x + y) / 2` — it never divides anything. It only reasons about the shapes of the values that would flow through the program if it ran, using the typing rules as a substitute for actual execution. This is exactly why it is so cheap: instead of testing `average` on every possible pair of inputs (infinitely many), the type system proves a single fact — "for all `Int, Int` pairs, this function returns an `Int`, and misuse is impossible" — in one linear pass over the code. Now contrast with a well-typed call, `average(4, 8)`:

Nothing here executes the addition or division; it only checks that `+` and `/` are being fed `Int` operands per their rules, and that the body's computed type matches the promised return type — catching, for instance, a bug where someone declares `-> Int` but the last line accidentally returns a `Bool`.

Type systems are not an academic curiosity; they are load-bearing infrastructure in nearly every major software system in production. Compilers for languages like C, Java, C#, Rust, Haskell, and OCaml perform static type checking before generating machine code, catching mismatches at build time rather than in a customer's data center. Interpreted languages like Python, Ruby, and JavaScript still have types — every value carries one — but check them at runtime instead, a distinction developed fully under Static Typing versus Dynamic Typing. Modern large codebases increasingly add optional static typing atop dynamic languages (TypeScript over JavaScript, mypy over Python), specifically because catching mismatches at scale, before deployment, is worth the upfront annotation cost. Database systems enforce column types (`INTEGER`, `VARCHAR`) as a lightweight external type system over stored data. Network protocols and serialization formats (Protocol Buffers, Thrift) use type schemas so that two independently-compiled programs agree on data shape across a network boundary. Even security-critical systems — smart contracts, cryptographic libraries, aerospace software — lean on strong, sometimes highly expressive type systems (dependent types, refinement types) specifically because the cost of a type error in production is measured in millions of dollars or worse. The mechanics of exactly how a compiler performs this checking are the subject of Type Checking.

Ask the tutor: How does a type system's checking strategy change once we move from static to dynamic typing?