Type Systems

A type system is a lightweight proof system running on a decidability budget. What it proves is a theorem you can state; what it declines to prove is a design decision, not an oversight.

Not “safe versus unsafe”. Two placements of the same check, differing on seven axes that each cut both ways — and orthogonal to the strong/weak axis that gets confused with it constantly.

One expression — `1 + "hello"` — asked of eight languages, with eight answers and four of them from statically checked languages that disagree with each other. The answer is a design decision, not a fact about types.

Premises above the line, conclusion below, and a name in brackets. Once you can read one aloud you can read a language specification, and the shape of the rule set tells you what the checker’s algorithm has to be.

Γ = { x: int, name: string }, and `Γ ⊢ x + 1 : int` says “under those assumptions, this holds”. In a real compiler Γ is not a new structure — it is the symbol table, read by the type checker instead of by the resolver.

`let x = 42` gives `x : int` in every language that has inference at all. The differences start at the second line, and the reason most mainstream languages infer locally rather than globally is error messages, not difficulty.

Fresh type variables, constraints, unification, and one clever step — generalization at `let` — buy whole-module inference with a principal type. Then subtyping, overloading and mutable references each break it in a different way.

Three rules solve every type equation: decompose matching constructors, bind a variable, or fail. The fourth thing the algorithm must do is refuse to bind a variable to a term containing itself — skip that and the type is infinite and the compiler does not terminate.

A genuinely parametric `identity<T>(x: T): T` can only return its argument. That is not a convention or a code review rule — it is a theorem about the type, provable because the function is forbidden from knowing anything about T.

Overloading, operator overloading, type classes, traits, concepts and protocols are one idea: different code per type behind one name. The interesting question is not the syntax but what each does to compilation — resolution, monomorphization or a dictionary.

One rule — if `S <: T` then an `S` may appear wherever a `T` was demanded — and it applies to every expression, which is why adding it to a checker is a redesign rather than an addition. The compiler checks the signature; Liskov’s behavioural obligations are checked by nobody.

A function is contravariant in its argument and covariant in its result; a mutable container must be invariant in its element. Java made arrays covariant anyway, and pays for it with a runtime check on every array store — `ArrayStoreException` is that decision, visible.