A type system is a formal set of rules in a programming language that assigns a type to every expression and enforces constraints on how values of different types may be combined, with the purpose of preventing type errors — operations applied to values of incompatible types — either at compile time (static typing) or at runtime (dynamic typing).
A type system is the language's set of rules about what kinds of values can be combined with what operations — and whether those rules are checked before the program runs, or only when the program actually tries to do something illegal.
Why types exist
Every value in a program is stored as bits. The number 65 and the letter 'A' are stored as the same bits (01000001). Without types, a program might try to multiply the letter 'A' by 2 — which is a meaningless operation. Types tell the computer what kind of thing each value is, so it knows what operations make sense.
Types also represent a contract. If a function says it accepts an integer, you know you can pass 5 to it. If it said it accepts anything, you'd have no idea what the function expects, and you'd have to read its source code to be safe.
Static typing: checking before the program runs
In a statically typed language, every variable and expression has a type known at compile time. The compiler checks that all operations are valid before producing an executable. If you try to add a number to a string, the compiler refuses — the program never runs at all.
int x = 5;
String name = "Alice";
int result = x + name; // COMPILE ERROR: cannot add int and String
// The program never runs — caught before executionC, C++, Java, Go, Rust, Swift, Kotlin, and TypeScript are statically typed. The type checker is part of the compiler. Errors appear as you write code or at build time — not when a user runs your program months later.
Dynamic typing: checking while the program runs
In a dynamically typed language, types are attached to values at runtime, not to variables at compile time. A variable can hold an integer, then later hold a string. The interpreter checks types when each operation is actually performed.
x = 5
x = "Alice" # Fine — x now holds a string
result = x + 10 # TypeError at RUNTIME: can't add str and int
# Only discovered when this line actually executesPython, Ruby, JavaScript, PHP, and Lua are dynamically typed. The flexibility lets you write code faster and more expressively. The risk is that type errors are discovered at runtime — potentially by a user in production rather than by you during development.
Strong and weak typing
These terms describe how willing a language is to automatically convert values between types. A strongly typed language refuses implicit conversions that don't make sense. A weakly typed language will convert values automatically in ways that can produce surprising results.
console.log("5" + 3); // "53" — string + number = string (concatenation)
console.log("5" - 3); // 2 — string - number = number (subtraction)
console.log([] + []); // "" — array + array = empty string
console.log([] + {}); // "[object Object]"print("5" + 3) # TypeError: can only concatenate str (not "int") to str
# Python refuses — no implicit conversionPython is dynamically typed but strongly typed. JavaScript is dynamically typed and weakly typed. Java is statically typed and strongly typed. These are two independent dimensions.
Type inference: the best of both worlds
Writing types on every variable is tedious. Many modern statically typed languages use type inference — the compiler figures out the type from context, so you don't have to write it.
// Rust — compiler infers type from the value
let x = 42; // compiler infers: i32
let name = "Alice"; // compiler infers: &str
let nums = vec![1, 2, 3]; // compiler infers: Vec<i32>
// Still statically typed — types are checked at compile time
// You just don't have to write them everywhereRust, Go, Swift, Kotlin, and modern C++ all use type inference extensively. You get static typing's safety with dynamic typing's conciseness.
Static vs. dynamic: where type information lives
In a statically typed language, types are attached to variables and expressions in the source code. The type checker walks the AST and verifies that every operation is applied to compatible types. At runtime, type tags may be stripped — a compiled C program's integers have no type metadata at runtime; the type information was used and discarded during compilation.
In a dynamically typed language, types are attached to values at runtime. Every Python object carries a type tag: type(42) is int, type("hello") is str. When an operation is performed, the interpreter checks the type tags of the operands. This runtime overhead is one reason dynamically typed languages are typically slower than statically typed ones for raw computation.
Strong vs. weak: implicit coercion rules
"Strong" and "weak" typing are informal terms with no universally agreed definition. The most useful way to understand them is through a language's implicit coercion rules:
| Language | Static/Dynamic | Strong/Weak | Notes |
|---|---|---|---|
| C | Static | Weak | Implicit int↔pointer coercions; undefined behaviour from type punning |
| Java | Static | Strong | Explicit casts required for narrowing conversions |
| Rust | Static | Strong | No implicit numeric conversions; all casts explicit with as |
| Python | Dynamic | Strong | No implicit conversions; "5" + 3 is a TypeError |
| JavaScript | Dynamic | Weak | Extensive implicit coercion; == applies type coercion |
| PHP | Dynamic | Weak | Extensive string-to-number coercions; historically source of security bugs |
| Go | Static | Strong | Even int and int32 require explicit conversion |
| TypeScript | Static (optional) | Strong | Structural typing; any type opt-out |
Structural vs. nominal typing
This distinction determines how the type checker decides whether two types are compatible.
Nominal typing: two types are compatible only if they have the same name or one explicitly declares that it is a subtype of the other. Java, C#, Kotlin, and Swift use nominal typing. A class Cat is only compatible with Animal if Cat extends Animal is declared — even if Cat has all the same methods.
Structural typing: two types are compatible if they have the same structure (the same fields or methods), regardless of their names. TypeScript, Go (interfaces), and Haskell use structural typing. If a type has the methods the interface requires, it satisfies the interface — no explicit declaration needed.
interface Printable {
print(): void;
}
class Document {
print() { console.log("Printing document"); }
// Document never declares "implements Printable"
}
function printIt(p: Printable) { p.print(); }
printIt(new Document()); // VALID — Document has a print() method
// TypeScript accepts this structurallyGradual typing
Gradual typing allows a mix of typed and untyped code in the same program. It was formalised by Jeremy Siek and Walid Taha (2006). The key mechanism is a dynamic type (any in TypeScript, dynamic in Dart) that is compatible with any other type — essentially opting out of the type checker for specific values.
TypeScript is the most widely used gradual type system in production: a JavaScript codebase can be migrated incrementally by adding type annotations file by file. Python's type hint system (introduced in PEP 484 and the typing module) is also gradual — annotations are optional and not enforced by the runtime, but tools like mypy and pyright check them statically when present.
Type theory: the formal foundation
Type theory is a branch of mathematical logic. The foundation relevant to programming languages is Alonzo Church's simply typed lambda calculus (Church, 1940) — an extension of the lambda calculus with a type system that assigns a base type to every term and prevents applying a function to an argument of incompatible type. Church's type theory establishes that well-typed programs cannot get "stuck" — cannot reach an undefined state — a property called type safety.
The Curry-Howard correspondence (Curry, 1934; Howard, 1969) establishes a deep isomorphism between type systems and logical proof systems: types correspond to propositions, programs correspond to proofs, and type checking corresponds to proof verification. A type-safe program is a proof that a certain proposition (specified by the types) holds. This correspondence underlies dependently typed languages like Coq, Agda, and Idris.
Type safety theorems
A type system is sound if a program that passes type checking cannot produce a type error at runtime. Soundness is expressed formally as two properties:
- Progress: a well-typed program is either a value (done) or can take a step (is not stuck)
- Preservation (subject reduction): if a well-typed program takes a step, the result is also well-typed
Java's type system is unsound in practice because of raw types, unchecked casts, and covariant arrays — a well-typed Java program can throw a ClassCastException at runtime. TypeScript's type system is intentionally unsound: any, type assertions, and structural subtyping with covariant fields all introduce unsoundness. Rust's type system (excluding unsafe blocks) is sound — the borrow checker and ownership rules ensure that well-typed Rust programs are free from data races, dangling pointers, and use-after-free errors.
Hindley-Milner type inference
The Hindley-Milner type system (Roger Hindley, 1969; Robin Milner, 1978) provides a complete type inference algorithm: given an untyped program, HM infers the most general (principal) type of every expression without any type annotations. The algorithm (Algorithm W) runs in nearly linear time in practice. HM is the basis of type inference in Haskell, ML, OCaml, F#, and Rust (with extensions for ownership types).
The authoritative text on programming language type theory: Pierce, B. C. (2002). Types and Programming Languages. MIT Press. — Covers simply typed lambda calculus, System F, subtyping, recursive types, and more. The formal definitions of type safety (progress and preservation) are in Part II. Available in full text at the author's site.
Gradual typing: formal specification
Siek, J. G. & Taha, W. (2006). "Gradual Typing for Functional Languages." Scheme and Functional Programming Workshop. Formalises the dynamic type ? (written any in TypeScript) and the consistency relation — a relaxed compatibility check that allows ? to match any type. Casts between static and dynamic code are inserted automatically by the type checker, making type errors from untyped code detectable at the boundary.