Skip to main content

Type System

A type system classifies values into types and enforces rules on their use, catching classes of errors and acting as machine-checked documentation.

A type system is the part of a programming language that classifies values into types — such as integer, string, boolean, or user-defined types — and defines which operations are valid on each. By enforcing these rules, a type system rejects programs that would combine values in nonsensical ways, like adding a number to a function.

How It Works

The type system checks that operations match the types of their operands. This checking can happen at compile time (static typing) or at run time (dynamic typing). Type systems vary in expressiveness: simple ones track primitive types, while advanced ones support generics, algebraic data types, union and intersection types, and even type inference that deduces types automatically so the programmer writes fewer annotations. Languages also differ in strength — how strictly they prevent implicit, error-prone conversions between types. A sound type system guarantees that well-typed programs cannot exhibit certain runtime errors.

Why It Matters

Type systems are a form of lightweight, always-on verification. They catch bugs such as passing the wrong argument or misspelling a field, often before the code ever runs. They serve as machine-checked documentation, power editor features like autocomplete and refactoring, and contribute to memory safety by preventing invalid operations. Richer type systems can encode invariants directly, making illegal states unrepresentable.

The trade-off is that stricter typing can require more upfront effort and can feel restrictive, which is part of why languages span a spectrum from dynamically to strongly statically typed.

Related Terms

Static typing and dynamic typing describe when type checks occur. A strong type system supports memory safety, and compilation is where static checks typically run.