# Types and effects

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](https://quality.stereobooster.com/static-types.md)**: shape. "This is an `Int`, this is a `User`."
- **[Linear types](https://quality.stereobooster.com/linear-types.md)**: 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](https://quality.stereobooster.com/refinement-and-dependent-types.md)**: 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](https://quality.stereobooster.com/effect-systems.md)**: 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](https://dafny.org/), [Verus](https://github.com/verus-lang/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](https://quality.stereobooster.com/schema-and-boundary-validation.md).

## Evidence

[Gradual typing](https://quality.stereobooster.com/static-types.md) 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

- [Maintainability](https://quality.stereobooster.com/maintainability.md) · Quality dimensions
- [Quality dimensions](https://quality.stereobooster.com/quality-dimensions.md) · Quality dimensions
- [Guarantee](https://quality.stereobooster.com/guarantee.md) · The axes
- [Effect systems](https://quality.stereobooster.com/effect-systems.md) · Methods
- [Linear types](https://quality.stereobooster.com/linear-types.md) · Methods
- [Schema and boundary validation](https://quality.stereobooster.com/schema-and-boundary-validation.md) · Methods
- [Static types](https://quality.stereobooster.com/static-types.md) · Methods
- [Conventional terminology](https://quality.stereobooster.com/terminology.md) · Conventional
- [Choosing methods](https://quality.stereobooster.com/choosing.md) · Overview

## Acronyms

- JLS — Java Language Specification
- SMT — satisfiability modulo theories