Type Systems & Type Checking

A type system is a lightweight formal method: a set of rules that prove, before the program runs, that certain kinds of errors cannot occur. That framing is more useful than "types catch bugs," because it makes the tradeoff explicit. Every type system rejects some programs that would have worked — the guarantee is bought by ruling out a class of behavior, and the design question is always which class, and at what cost in expressiveness.

For a compiler implementer, type checking is a pass over the AST that computes a type for every expression and reports where the rules are violated. For a simple language this is a recursive walk. For anything with inference, it becomes a constraint-solving problem — generate constraints from the tree, solve them by unification, and report a failure when no solution exists.

The part that determines whether people enjoy using your language is the last one: error messages. A type checker that reports "cannot unify t42 with t17" is technically correct and functionally useless, and getting this right is more engineering than theory.

TL;DR

Quick Example

A type checker with Hindley-Milner inference, in about 120 lines:

Everything interesting is in unify. Inference generates equations between types; unification solves them; a contradiction is a type error. The occurs_in check is what stops \x -> x(x) from producing an infinite type.

Core Concepts

The axes

The strong/weak distinction is informal and often used sloppily; the useful question is "what implicit conversions does this language perform, and are they surprising?"

Inference

Hindley-Milner (as in ML, Haskell, and OCaml) infers principal types for a whole program with no annotations. Most mainstream languages use local inference instead — infer within a function body, require annotations on signatures. That's a deliberate tradeoff: full inference produces worse error messages (a mistake in one place surfaces as a failure somewhere unrelated) and interacts badly with subtyping and overloading.

Requiring signature annotations also serves documentation and gives the checker anchor points to localize errors against, which is why even Haskell programmers usually write them.

Variance

The question is: given Cat <: Animal, when is F<Cat> <: F<Animal>?

Java's arrays are covariant and therefore unsound — the check is deferred to runtime, which is why ArrayStoreException exists. Generics were made invariant precisely to avoid repeating the mistake, with ? extends and ? super (use-site variance) as the escape valves.

Function types are the case people find counterintuitive: contravariant in parameters, covariant in return type.

Nominal vs. structural

Structural typing is flexible and composes well with duck-typed idioms; nominal typing prevents accidental compatibility between things that happen to look alike. TypeScript users simulate nominal typing with branded types exactly because the flexibility is sometimes wrong:

Soundness

Most practical languages also deliberately sacrifice soundness in specific places, and knowing where matters:

TypeScript is worth calling out: it's explicitly and by design not sound, because its goal is to describe existing JavaScript rather than to prove properties. That's a defensible product decision and it means a TypeScript type is a strong hint, not a guarantee.

Gradual typing

Adding optional static types to a dynamic language — TypeScript over JavaScript, Python type hints, Sorbet over Ruby, PHP's declarations.

The erasure point catches people out constantly: a Python function annotated def f(x: int) will happily receive a string at runtime, and a TypeScript API response typed as User is an assertion about data you haven't validated. This is what runtime validators like Zod and Pydantic exist to close.

Error Messages

The single largest determinant of whether people enjoy a statically typed language, and the part most often treated as an afterthought.

What makes the third one work: the actual and expected types named plainly, both source locations shown (where the expectation came from and where it was violated), and a concrete suggestion. Rust and Elm invested heavily here and it's widely cited as a major reason people adopt them.

The engineering behind good errors: track why the checker expected a type (an expectation stack, not just a constraint), keep spans on everything, and prefer reporting at the point of the annotation the user wrote rather than at a synthesized internal node.

Best Practices

Report the expectation's origin, not just the mismatch

"Expected Int" is much more useful with "because the function's return type is declared here." Threading an expectation reason through the checker is real work and it's the difference between a usable and a frustrating language.

Recover and keep checking

After a type error, substitute an error type that unifies with anything and continue. Reporting fifteen genuine errors in one run beats reporting one — and it stops a single mistake from cascading into fifty spurious ones.

Localize with annotations

Require or strongly encourage signatures on top-level functions. They anchor inference, so an error is reported inside the function that's wrong rather than at some distant call site. This is why even full-inference languages recommend writing them.

Be careful adding subtyping to inference

Hindley-Milner and subtyping interact badly — principal types stop existing, and inference becomes much harder. Most languages that want both use local inference plus bidirectional type checking rather than global inference.

Make unsoundness explicit and searchable

If your system has escape hatches, name them (unsafe, any, as) so they're greppable and lintable. An unsoundness that looks like ordinary code is one nobody can audit.

Validate at the boundary

Static types describe your code, not the data arriving from a network, a file, or a database. Parse and validate at the edge with a runtime schema, then let the type system carry the guarantee inward. See Zod.

Test the error messages

Golden-file tests asserting on diagnostic output. Errors are a user-facing surface that silently degrades as the checker changes, and nobody notices until a user complains.

Don't over-engineer the type system

Dependent types, higher-kinded types, and effect systems each buy real guarantees and each raise the cost of using the language. Most languages benefit more from excellent inference and excellent errors on a modest system than from an expressive system nobody can debug.

Common Mistakes

Type variable names in user-facing errors

Stopping at the first error

Covariant mutable containers

Trusting types at a system boundary

Omitting the occurs check

Inference so aggressive that errors are unlocatable

FAQ

Are static types worth it?

The empirical evidence is more equivocal than either camp claims, and the practical consensus has shifted strongly toward yes for anything long-lived or multi-person. The benefits that hold up best aren't bug-catching in isolation — they're tooling (autocomplete, go-to-definition, safe rename), refactoring confidence at scale, and documentation that can't go stale. For a script you'll run once, the overhead isn't worth it.

What's the difference between type checking and type inference?

Checking verifies that a program with annotations satisfies the rules. Inference derives the annotations. Most real systems do both — bidirectional type checking alternates between checking an expression against an expected type and inferring a type from an expression, which handles constructs that pure inference struggles with.

Why is TypeScript unsound?

Deliberately, and for a good reason: it was designed to type existing JavaScript, which does things a sound system would have to reject. any, type assertions, bivariant method parameters, and the absence of runtime checks are all explicit tradeoffs favoring adoption over guarantees. The practical implication is that TypeScript types are excellent tooling and documentation, and are not proofs — validate external data at runtime. See TypeScript.

What are dependent types?

Types that depend on values — Vector<n> where n is a runtime length, letting the type system prove an index is in bounds. Idris, Agda, Lean, and (in restricted form) Rust's const generics and F*'s refinements offer versions of this. They're extremely powerful and raise the cost of writing and debugging code substantially, which is why they remain mostly in research and verification contexts.

How do I add types to an existing dynamic codebase?

Incrementally, from the boundaries inward. Start with the most-used modules and the public interfaces, allow any/Any liberally at first, enable strictness flags one at a time, and add runtime validation at I/O boundaries. Trying to reach full strictness in one pass on a large codebase reliably stalls. TypeScript's allowJs and Python's per-module mypy configuration exist for exactly this migration.

Should my language have subtyping?

It complicates inference significantly and is hard to remove later. Languages built around parametric polymorphism without subtyping (ML, Haskell, and to a large extent Rust) get simpler, more predictable inference. Languages with class hierarchies need it. If you're designing something new, be clear about which model you're in before adding features from the other.

Related Topics

References