Type Systems

Add a number to a number and you get a number. Add a number to a function, or call a string as if it were a procedure, and you have written something meaningless — an operation that has no sensible answer. A type system is the set of rules a language uses to spot such nonsense and rule it out before it can run.

The core idea is small and powerful: every phrase of a program — a literal, a variable, an expression, a function — is assigned a type, a label describing what kind of value it stands for (\text{number}, \text{string}, \text{list of booleans}, \text{number} \to \text{number}). The rules then say which combinations are allowed. If the pieces don't fit — you tried to feed a string where a number was demanded — the checker refuses the program. That refusal is a type error, and catching it is a gift: a bug found while you are still typing, not one that pages you at 3 a.m.

This page builds on the data types a language offers; here we ask the deeper question — what are the rules that decide which operations on those types are legal, and when are they checked?

A crash you can prevent

JavaScript is famously permissive. The expression "1" + 1 does not raise an error — it silently decides the + means "join text" and hands you the string "11". Later arithmetic then produces garbage, and nothing ever complained. A stricter type system would have stopped you at the +. Run this, then read what happened:

// JavaScript-style coercion: + is overloaded, so it guesses. const a = "5" + 1; // string "5" wins → text concatenation const b = Number("5") + 1; // convert first, THEN add → real arithmetic console.log("'5' + 1 =", a, "(a " + typeof a + ")"); console.log("Number('5') + 1 =", b, "(a " + typeof b + ")"); // A typed function states its intent. TypeScript checks callers at COMPILE time. function doubleIt(n: number): number { return n * 2; } console.log("doubleIt(21) =", doubleIt(21)); // doubleIt("21") would be a COMPILE error: the string never reaches runtime. console.log("doubleIt(Number('21')) =", doubleIt(Number("21")));

The surprise is line one: "5" + 1 is "51", not 6. The type annotation n: number on doubleIt is the fix — TypeScript reads it and rejects doubleIt("21") before the program ever runs, forcing you to convert with Number(...) and make your intent explicit. The type is a promise the checker enforces.

Axis one: static vs dynamic — when is the check?

The first great division is about timing.

Static typing checks types at compile time, before the program runs, using only the source text. A type error is a build failure — the bad program is never produced. TypeScript, Haskell, Java, Rust, C and C++ are static. The payoff: whole classes of bugs are impossible to ship, and editors can autocomplete because they know every type.
Dynamic typing checks types at run time, as each operation happens, by tagging every value with its type. A type error is a runtime exception — TypeError: 'int' object is not callable. Python, Ruby, JavaScript and Lisp are dynamic. The payoff: flexibility and terse code; the cost: the error surfaces only when execution actually reaches that line.

A slogan: a static type checker asks "could this ever go wrong?" and a dynamic one asks "did this just go wrong?". Static typing trades a little up-front ceremony for guarantees that hold across every possible run.

Axis two: strong vs weak — does it bend the rules?

The second division is a different question — not when types are checked, but how firmly the rules are enforced once you hit a mismatch.

Strong typing refuses to silently reinterpret a value as the wrong type. If you mix a string and a number, you get an error or must convert explicitly. Python is strongly typed: "1" + 1 raises TypeError — it will not guess.
Weak typing will quietly coerce or reinterpret the bits to make an operation "work". JavaScript's "1" + 1 === "11" is a weak, implicit coercion. C is weaker still: a cast or a union lets you read the very same bytes as an int one moment and a float the next — no conversion, just a reinterpretation the compiler permits.

"Strong" and "weak" are really a spectrum, not a switch — languages sit at points along it — but the essential test is: when the types don't match, does the language stop you, or does it shrug and reinterpret?

The single most common confusion in this whole topic: strong/weak is NOT the same axis as static/dynamic. They are two independent dials, giving a 2×2 grid — and every box is occupied by a real, famous language:

Static & strong — Haskell, Rust. Checked before running, and no sneaky coercions.
Static & weak(ish) — C. Checked at compile time, yet casts and unions let you reinterpret bits freely.
Dynamic & strong — Python. Checked at run time, but "1" + 1 is refused, not coerced.
Dynamic & weak — JavaScript, PHP. Checked at run time and happy to coerce "5" + 1 into "51".

So "Python is dynamic" tells you nothing about whether it coerces — and in fact it is fairly strong. Keep the two questions separate: when is it checked (static/dynamic) vs how strictly (strong/weak).

Types form a lattice

The types a language knows about aren't a flat list — they are ordered by a subtype relation. If every value of type S can safely be used wherever a T is expected, then S is a subtype of T. Many languages cap this ordering with a top type (unknown / Object / any) that every type is a subtype of, and a bottom type (never) that is a subtype of everything — the type of an expression that never produces a value at all. Together this forms a lattice, drawn below.

Reading it top-down: unknown sits above the concrete types number, string and boolean; each of those sits above never at the base. Widening (moving up the lattice, e.g. treating a number as unknown) is always safe. Narrowing (moving down) is where checks are needed — and where an unsound system can let a lie slip through.

Soundness: "well-typed programs don't go wrong"

Why trust a type checker at all? Because of a property called soundness. A type system is sound if it never lies: whenever it says a program is well-typed, that program really will not commit a type error at run time. Robin Milner captured it in 1978 in one of computer science's most quoted lines:

Well-typed programs cannot "go wrong."
If the checker accepts a program, no execution of it will apply an operation to a value of the wrong type.
The proof has two halves — progress (a well-typed program is never stuck) and preservation (each step keeps it well-typed).

Soundness is what turns a type annotation from a comment into a guarantee. In a sound, statically-typed language an entire family of crashes — "undefined is not a function", "null pointer", "added a string to a list" — simply cannot occur in accepted code. That is the safety you are buying.

Because most languages are deliberately unsound in places, trading a guarantee for power or convenience. C's casts and pointer arithmetic are escape hatches the compiler cannot check — so C is type-checked but not type-safe. TypeScript's any and its type assertions (x as Foo) punch sound holes on purpose, to model messy real-world JavaScript. Even Java's array covariance is a known unsoundness patched by a runtime check. A perfectly sound system also rejects some programs that would actually have been fine — no checker can be both perfectly sound and perfectly permissive, so language designers pick where to sit.

Classifying real languages

Put the two axes together and every language lands somewhere. A rough field guide:

Haskell — static, strong, sound. Types inferred, coercions basically forbidden; the compiler is a co-author.
Rust — static, strong. Adds ownership types to rule out data races too.
TypeScript — static, strong in intent but with deliberate soundness holes (any, assertions) for JS compatibility.
Java / C# — static, mostly strong, with a runtime safety net.
Python / Ruby — dynamic, but fairly strong — it refuses "1" + 1 rather than coercing.
JavaScript / PHP — dynamic and weak: implicit coercion everywhere.
C / C++ — static, yet relatively weak and unsound: casts and unions reinterpret bits, and there is no runtime type tag to save you.