Static types

A type is a promise about what a value can do: this is a number, this is a list of them, this is a record with a name and a tonnage. Stating the promise lets a compiler refuse programs that break it, and lets it help where the promise holds — no conversion, no surprise, no “undefined behaviour” at three in the morning.

The arguments are old. FORTRAN needed types to compile floating-point arithmetic at all; ALGOL 60 needed them to scope names; every language since has picked a side in the same fight — nominal systems name their types like Java and C++, structural systems compare shapes like Haskell and TypeScript. And every language since has found a third door: gradual typing, where JavaScript gets annotations it can remove and C# gets nullability it can enforce.

The trade-off

• Types buy guarantees and cost expressiveness — every type system is a list of programs it refuses to compile.
• Gradual typing moves the cost to the boundary: checks where you asked for them, trust where you did not.

Where it came from

FORTRAN, 1957 — typed variables so that the compiler could do the arithmetic for you. Ada, 1983, took it further and made the type system a safety argument for avionics.