Type system
The rules a language uses to classify values and to decide, before or during a run, which operations on them are legal. Every language in this corpus has one. What differs is when it is checked, how much it is asked to prove, and whether it survives compilation.
typescript is the source that forced this page: it is a language whose only contribution is a type system. It has no memory model and no concurrency model of its own, so the four axes on programming-language have nothing to say about it.
When the check happens
c, go, rust, kotlin and dart check at compile time. clojure is dynamic by
design and php and JavaScript-on-nodejs check as they run. typescript adds a third
position — gradual: checking is opt-in per file (// @ts-check, JSDoc annotations) over a
codebase that stays runnable the whole time. The pitch is explicitly about migration cost, not about
correctness, which is a different argument from the one static languages make.
What the types are asked to do
The corpus spreads across a wide range of ambition:
| Language | The type system’s job |
|---|---|
| c | classify storage; it does not stop you |
| go | keep the compiler fast and the code obvious |
| typescript | describe existing JavaScript well enough for an editor |
| kotlin | rule out one specific bug class — null dereference |
| rust | encode ownership and lifetime, so memory and data-race errors are type errors |
| spark | carry contracts, and prove absence of runtime errors outright |
| haskell | make effects visible, so purity is checkable |
Read down the column and the type system stops being bookkeeping and becomes the safety mechanism. rust is the pivot: its memory model is its type system, which is why it needs neither a collector nor a runtime (memory-management-model).
Erasure: does the type survive?
typescript‘s types are deleted before the program runs — the compiled output is the same JavaScript, and nothing checks the types again at the boundary where data actually arrives. The guarantee therefore covers the code you compiled and stops at its edges. rust‘s ownership checks are also compile-time-only, but they are erased into something the machine still honours: a memory layout with no collector behind it. Same timing, opposite consequence — one erases into nothing, the other erases into the runtime’s absence.
Types that carry semantics (added 2026-08-06, same day)
haskell extends the table’s bottom row. Purity means an effect has to appear in a type instead of happening anywhere, so the checker enforces what a program is allowed to mean, not only what it may touch. Set against typescript, the day’s other type-first language, the two point opposite ways: TypeScript infers types over code that already exists and then deletes them; Haskell’s types decide what code is admissible. Describe versus constrain.
Haskell also closes half the gap below — it names its inference as bidirectional unification, the first algorithm any source here has given.
What a type system declines to abstract over (added 2026-08-12)
A dimension the table above misses: not how much the types prove, but what can be a variable. In
haskell a type variable may range over a type constructor, which is why Monad m is expressible
at all. In ocaml and typescript every type variable has kind *, so Option as such cannot
be abstracted — only Option<number>.
lightweight-hkt (Yallop & White, FLOPS 2014) shows the standard workaround, and fp-ts runs it
in TypeScript: encode type application as an ordinary type and give each constructor an uninhabited
brand. It buys the expressiveness and gives up kind checking — the paper says so directly. Two
unrelated languages needing the same trick is decent evidence that this is a property of *-only
type systems rather than a quirk of either. See functional-programming for what it costs a
paradigm.
Open
No source measures what inference costs (compile time, error-message quality), and no third-party source measures whether gradual typing catches the defects it advertises. typescript‘s own evidence is a 2020 survey.
Related
programming-language · typescript · rust · kotlin · spark · hosted-language · memory-management-model · functional-programming · lightweight-hkt · fp-ts · synthesis