Skip to content

Software Quality

Types and effects

Catching whole classes of error before the program runs.

A type system classifies every expression in a program and rejects any use the classification does not fit (before the program runs). Types-and-effects is the family that varies what the classification can express, from everyday static checking through verified algorithms.

The kinds at a glance

What each kind constrains:

  • Static types: shape. "This is an Int, this is a User."
  • Linear types: usage. How many times, and in what order, a value may be used. A file handle opened and closed exactly once.
  • Refinement and dependent types: value-dependence. A checkable predicate on a value, or a type that depends on a value. {x : Int | x > 0}, Vector n A.
  • Effect systems: effect. What a computation does, not just what it returns. Int / {IO, Exn}.

Static is the common base; a language adds any combination of the others. Rust adds linearity; F* adds dependence and effects; Idris 2 adds dependence and linearity.

What the family catches

  • Representational and shape bugs. Field renames, type confusion, missing branches.
  • Memory and concurrency bugs. Rust's defining case; use-after-free, data races, iterator invalidation gone by construction in the safe subset.
  • Effect leaks and unhandled exceptions. Effect systems prevent pure code from accidentally performing I/O and force every exception to have a handler.
  • Value-range and indexing bugs. Refinement types reject x / 0 and out-of-bounds indexing at compile time.
  • Spec-level invariants. Dependent types lift arbitrary predicates into the type system; the proof of correctness lives alongside the code.

What the family does not catch: logic bugs that respect the declared types.

When to use, when not

Use:

  • Always for mainstream typing. The marginal cost of turning on strict mode in a typed language is near-zero.
  • Specialized kinds when the problem matches. Linear types for systems code; effect systems for concurrency or pure-core maintenance; refinement / dependent types for invariant-rich algorithms.

Don't:

  • Treat types as a substitute for tests. A type system proves the absence of what it can express; behavior outside that reach needs a test.
  • Reach for dependent types in mainstream production code without a clear cost case. The pragmatic SMT-assisted tier (F*, Dafny, Verus) is usually a better starting point.
  • Forget the boundary. Static types vanish at deserialization, so every network or storage boundary needs its own schema check.

Evidence

Gradual typing has the family's most direct empirical record: it catches a specific, measurable bug class, without a demonstrable reduction in overall bug rate.

The other kinds — sound mainstream types, linear types, effect systems, refinement types — have few controlled comparisons, and the case for them rests on the definitional point that a passing check eliminates the bug class it names.

Soundness — the central property

A type system is sound if a passing type check guarantees the absence of the type errors the system claims to forbid at runtime. Type systems fall on a spectrum:

Soundness tier Languages What a passing check means
Sound by design Haskell, OCaml, F#, Standard ML Within the language's expressive reach, a proof with no escape hatch. The cost is a smaller expressive surface (no bottom values from null in idiomatic code; effects pushed through the types).
Sound at the core, unsound at named boundaries Kotlin (Java platform types), Swift (Objective-C bridges), Rust (unsafe) A proof except at specific escape hatches; the unsoundness is named and scoped.
Unsound by design (gradual) TypeScript, Python + mypy / pyright any and unchecked imports let the type system lie to stay compatible with dynamic code.
Unsound in practice Java (covariant arrays, flagged by the JLS), Scala (legacy null), C++ (pointer aliasing, signed overflow, lifetime bugs) The compiler accepts programs that exhibit the very errors the type system claims to forbid.

A passing check in an unsound system is evidence, not proof.

Strict modes narrow the gap between what a system claims to forbid and what it enforces at runtime — TypeScript's strict: true, noUncheckedIndexedAccess, and exactOptionalPropertyTypes; mypy's --strict; Kotlin's -Xexplicit-api=strict.

Referenced by