Refinement Types

Core Idea

Refinement types augment base types with logical predicates that constrain the set of values. Instead of just Int, you write {v : Int | v > 0} — the type of positive integers. A function div : Int -> {v : Int | v != 0} -> Int statically guarantees the divisor is nonzero. Unlike full dependent types, refinement predicates are restricted to decidable logics (typically quantifier-free theories handled by SMT solvers), enabling fully automatic type checking without manual proofs. Liquid types, the most successful refinement type system, infer refinement predicates automatically using abstract interpretation over types, combining the expressiveness of dependent-types-lite with the automation of type inference.

Explainer

Full dependent types (as in Coq or Agda) let types express arbitrarily precise specifications, but at a cost: type checking is undecidable and requires the programmer to construct proofs manually. At the other extreme, simple type systems (as in Java or Python) are fully automatic but cannot express properties like "this integer is positive" or "this list is sorted." Refinement types occupy a sweet spot: they extend base types with logical predicates, gaining significant expressive power while retaining automatic type checking.

A refinement type has the form {v : T | P(v)}, where T is a base type and P is a logical predicate. The type {v : Int | v > 0} contains exactly the positive integers. A function can declare `div : (x : Int) -> (y : {v : Int | v != 0}) -> Int`, making division by zero a static type error. Array access can use `get : (a : Array T) -> (i : {v : Int | 0 <= v && v < len(a)}) -> T`, making out-of-bounds access a type error. These specifications live in the type system, are checked at compile time, and carry zero runtime cost.

The key to automation is restricting predicates to decidable theories that SMT solvers can handle. Liquid types, developed by Rondon, Kawaguchi, and Jhala, restrict refinements to conjunctions of qualifiers — simple predicates from a fixed set — and use abstract interpretation to infer which qualifiers apply at each program point. Subtype checking reduces to SMT validity: {v : T | P} is a subtype of {v : T | Q} if and only if P implies Q, which the solver decides automatically. LiquidHaskell applies this to Haskell, enabling programmers to verify memory safety, termination, functional correctness, and information flow properties with minimal annotation burden. The tool infers most refinements automatically; the programmer adds annotations only where inference needs guidance.

Path sensitivity is crucial for practical refinement typing. Inside `if x > 0 then f(x) else g(x)`, the type of x in the then-branch is refined to {v : Int | v > 0} by the branch condition. The type checker tracks these path conditions and includes them in SMT queries. This means that idiomatic null checks, bounds checks, and error handling are automatically recognized by the type system. The programmer does not need to add explicit annotations for code that already checks its preconditions — the type system extracts the information from the control flow.

Refinement types are less expressive than full dependent types — they cannot express properties requiring quantifiers (like "for all elements in this list, P holds") without extensions. But for a large class of safety and correctness properties — array bounds, division by zero, resource protocol compliance, numeric invariants — they provide strong static guarantees with an experience closer to ordinary type checking than to theorem proving. Tools like LiquidHaskell, Flux (for Rust), and F* (which combines refinement and dependent types) demonstrate that refinement types can scale to substantial codebases while catching real bugs that conventional type systems miss.