Overview
A type system is a formal method for classifying program phrases according to the kinds of values they compute.
It acts as a static contract between programmer and compiler, ensuring that operations are applied only to compatible values.
Note
The type system doesn’t predict the result of computation, only that the computation will make sense.
Motivation
Types serve multiple overlapping goals:
- Safety: prevent runtime errors (e.g., adding numbers to strings).
- Abstraction: describe interfaces and modules.
- Documentation: types communicate program intent.
- Optimization: compilers use type information for efficient code generation.
- Proof connection: under Curry–Howard, types correspond to logical propositions.
Tip
“A type system is a lightweight proof system that every programmer uses.” (Benjamin Pierce)
Static vs Dynamic Typing
| Aspect | Static Typing | Dynamic Typing |
|---|---|---|
| Checking | Compile-time | Runtime |
| Error detection | Early (before execution) | Late (during execution) |
| Flexibility | Restrictive but safe | Flexible but risky |
| Examples | Haskell, Java, Rust | Python, JavaScript, Lisp |
Example
Static typing rejects this program before running:
3 + true (* type error: cannot add Bool to Int *)Dynamic typing detects it at runtime:
3 + True # raises TypeError
Type Judgments and Rules
Type systems are defined by typing judgments of the form:
Γ ⊢ e : T
Read as “under context Γ (a mapping of variables to types), expression e has type T.”
Each rule constrains how valid programs are built.
Example: Arithmetic
⊢ n : Int
⊢ m : Int
───────────────────────
⊢ n + m : Int
Example: Function Abstraction
Γ, x:T₁ ⊢ e : T₂
────────────────────────────
Γ ⊢ (λx:T₁. e) : T₁ → T₂
The combination of these rules defines what programs are well-typed in a language.
Type Soundness
The goal of any well-designed type system is soundness, that is:
A well-typed program will not “go wrong.”
Formally, type soundness is the combination of:
-
Progress: a well-typed expression is either a value or can take a step.
-
Preservation: evaluation preserves types across each step.
These correspond to safety and stability of execution.
| Theorem | Statement | Meaning |
|---|---|---|
| Progress | If ⊢ e : T, then e is a value or e → e'. | Never gets stuck. |
| Preservation | If ⊢ e : T and e → e', then ⊢ e' : T. | Type consistency holds. |
Note
Together, they imply that typed programs can only “go wrong” if the type checker is wrong.
Example: Preventing Stuck States
Consider this untyped fragment:
if 3 then true else falseEvaluation gets stuck: 3 isn’t a Boolean.
Adding typing prevents this:
⊢ if e1 then e2 else e3 : T
requires ⊢ e1 : Bool and ⊢ e2 : T, ⊢ e3 : T
Thus the ill-typed form never reaches execution.
Warning
A stuck term is syntactically valid but has no reduction rule, the classic indicator of a type error.
Nominal vs Structural Typing
| Model | Basis | Example |
|---|---|---|
| Nominal | Explicit declarations (by name) | Java, C#, Swift |
| Structural | Compatibility by shape (fields, members) | TypeScript, OCaml, Go |
Example (Structural)
type point = { x: int; y: int }
type pixel = { x: int; y: int; color: string }
(* point and pixel share structure, but differ by field sets *)Example (Nominal)
class Point { int x, y; }
class Pixel extends Point { String color; }Nominal typing enforces hierarchy; structural typing favors flexibility.
Weak vs Strong Typing
| Property | Weak Typing | Strong Typing |
|---|---|---|
| Conversions | Implicit and lenient | Explicit and enforced |
| Examples | C, JavaScript | Rust, ML, Haskell |
Example:
int x = 1;
float y = x + 0.5; // implicit conversion, weakly typedlet x: i32 = 1;
let y = x as f32 + 0.5; // explicit cast, strongly typedNote
“Strong” ≠ “Static.” A dynamically typed language can still be strong (e.g., Python disallows
3 + "a").
Types as Logical Propositions
Under the Curry–Howard correspondence:
| Programming | Logic |
|---|---|
Term e | Proof |
Type T | Proposition |
Γ ⊢ e : T | “e is a proof of T” |
Thus, type checking is proof verification, and type inference is proof search.
Tip
Every type rule corresponds to an inference rule in logic.
For example, function types mirror implication (→), and product types mirror conjunction (∧).
Extending Type Systems
Once the fundamentals (soundness, safety, progress) are established, languages add richer features:
-
Polymorphism: generalize over types (
∀α. α → α). -
Subtyping: allow safe substitution (
A <: B). -
Effects & Monads: track stateful or impure computations.
-
Dependent Types: allow types to depend on values.
-
Refinements: encode logical predicates within types.
Each extension must re-prove progress and preservation, maintaining the safety invariant.
Conceptual Summary
| Goal | Guarantee | Consequence |
|---|---|---|
| Type Checking | Detects errors statically | No runtime type mismatches |
| Progress | Well-typed programs reduce | No stuck states |
| Preservation | Reduction preserves types | Type safety |
| Soundness | Progress + Preservation | “Well-typed programs do not go wrong” |
Note
Type systems don’t guarantee correctness, only well-formedness.
A well-typed infinite loop is still infinite.
See also
Sources
-
“Type system,” Wikipedia. https://en.wikipedia.org/wiki/Type_system . Supports type systems as formal methods that classify program phrases by the kinds of values they compute, acting as a static contract for safety, abstraction, documentation, and optimization, and the static-vs-dynamic and nominal-vs-structural distinctions.
-
“Type safety,” Wikipedia. https://en.wikipedia.org/wiki/Type_safety . Supports soundness as the guarantee that a well-typed program will not go wrong, decomposed into progress and preservation.
-
“Curry–Howard correspondence,” Wikipedia. https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence . Supports the correspondence between types and propositions and between programs and proofs, including function types as implication and product types as conjunction.