Skip to content

Software Quality

Refinement and dependent types

Refinement and dependent type systems push the boundary of what a type system can express past shape and into predicates over values. Refinement types attach SMT-discharged predicates to ordinary types — {x : Int | x > 0} is the type of integers the compiler has proved positive. Dependent types let types depend on values — Vector n A is a vector of exactly n elements of type A, with n a runtime value lifted into the type.

What it catches

  • Array out-of-bounds. Vector n A plus a bounded index Fin n makes lookup : Vector n A -> Fin n -> A total — the compiler proves the index is in range.
  • Division by zero. A NonZero : Int -> Prop refinement on the divisor makes division total at the type level. Liquid Haskell, F*, and Dafny all reject x / 0 at compile time when the divisor's type is unrefined.
  • Numerical preconditions. sqrt : {x : Real | x >= 0} -> Real forces the caller to prove non-negativity before the call.
  • State invariants encoded in types. A BalancedTree type whose definition includes the balance invariant; a SortedList n indexed by length and order.
  • Protocol state in types. A session type carries the current step of a protocol; the type system rejects out-of-order operations. Common pattern in F* and Idris.
  • Cryptographic constants and field arithmetic. Fiat-Crypto verifies elliptic-curve arithmetic in Coq.

What refinement and dependent types do not catch: bugs whose predicate is too hard to discharge (undecidable for the SMT solver, or too tedious to prove interactively), bugs outside the typed region (FFI calls, unsafe), and bugs in the predicate itself.

Refinement vs dependent — the practical distinction

Refinement and dependent types sub-split by how much dependence they allow and how the proof obligation is discharged, from SMT-checked predicates to full interactive proof.

Sub-tier How it works Discharge Tools
Refinement types a predicate carves a subset of a base type ({x : Int | x > 0}); types and values stay separate SMT, automatic Liquid Haskell, LiquidJava
SMT-assisted hybrid dependent types, SMT for the easy obligations and interactive proof for the rest SMT + interactive proof F*, Dafny, Verus, Why3
Full dependent types types indexed by values directly (Vector n A), and types are first-class interactive proof Idris 2, Agda, Lean 4, Coq

F* spans the whole spectrum — automatic SMT refinements and full interactive dependent proofs — though its home is the hybrid tier.

Tools

Refinement types

  • Liquid Haskell — refinement types layered on GHC, SMT-discharged via Z3 or CVC5; rejects head [] at compile time, proves bounded indexing, encodes data-structure invariants.
  • LiquidJava — refinement types for Java; research-grade.
  • Stainless — Scala with verification; refinement-typed contracts.

SMT-assisted dependent

  • F* — dependent types + SMT; Project Everest's verified TLS.
  • Dafny — verification-oriented language; SMT under the hood; used for AWS encryption SDK validation.
  • Verus — Rust-flavored verification language; SMT-backed; proof-carrying Rust for systems code.
  • Why3 — multi-prover frontend; dispatches to Coq, Alt-Ergo, Z3, CVC5.

Full dependent types (proof assistants)

  • Idris 2 — dependent types with linear quantifiers.
  • Agda — dependent types on a theory close to Coq's; used for mathematics and programming-language research.
  • Lean 4 — dependent types with strong automation tactics (omega, polyrith, decide, aesop).
  • Coq / Rocq — dependent types with tactic-based interactive proof; CompCert and Fiat-Crypto are written in it.

SMT solvers underneath

  • Z3, CVC5, Yices2, Alt-Ergo. Refinement-typed languages dispatch to one of these, and the solver supplies the oracle. They take its verdict on trust, which puts the solver in the trusted computing base; a proof assistant instead re-checks a proof term against its own kernel.

When to use, when not

Use:

  • For libraries with strong invariants — collections, parsers, numerical code, crypto primitives. The invariant is captured in the type and survives every change.
  • At the boundary between trusted and untrusted code. Refinement types are a compact way to demand proof from the caller.
  • For verified systems work — kernels (seL4), compilers (CompCert), TLS (Project Everest), crypto (Fiat-Crypto). The cost is justified by the blast radius, and the proof effort it takes is measured in theorem proving.
  • As an escape hatch from heavy ceremony: refinement types in Liquid Haskell can be added incrementally to a mainstream Haskell codebase.

Don't:

  • For business logic where the predicates are vague. "This is a reasonable email address" is not a refinement; reach for contracts or property-based testing.
  • For one-off scripts. The cost is wrong for the value.
  • Past the SMT solver's reach without dropping to interactive proof. A predicate the solver cannot discharge fails the build whether or not the code is correct, and the failure does not distinguish the two.

Evidence

  • The foundational Liquid Haskell paper introduces refinement types for GHC Haskell, with the proof obligations discharged by an SMT solver (Vazou et al. 2014)1.
  • Fiat-Crypto. Elliptic-curve field arithmetic proved correct in Coq, with the straight-line implementation generated from a high-level functional one by partial evaluation (Erbsen et al. 2019)2.
  • CompCert. Verified compiler from Clight (a large C subset) to PowerPC assembly, written in Coq (Leroy 2009)3.

The empirical record concentrates at the heavyweight end where the proven invariants are the point. For refinement types specifically, the literature is thinner; the Liquid Haskell documentation has worked examples but controlled comparisons are rare.

Oracle: predicate

All four answer the same question — does property P hold? — and differ only in how that answer is obtained, from cheapest-and-weakest to strongest:

  • Runtime contracts — check P during execution, on the inputs you actually run, and crash if it's violated.
  • Property-based testing — check P on many generated inputs; empirical, with no guarantee past what was sampled.
  • Refinement & dependent types — encode P in the type, so the compiler rejects any program that could violate it (sound within what the type can express).
  • Theorem proving — prove P holds for all inputs, ahead of time.

Classification

  • Quality dimensions: Functionality, Maintainability (an invariant captured in the type survives every change (refactor-safety), partly offset by the added proof-obligation burden).
  • Area: Array indexing, numerical preconditions, value-range constraints, verified algorithms, crypto and TLS verification, formalized mathematics, verified compilers.
  • Guarantee: Mathematical with proof-assistant discharge (dependent types); Exhaustive within the SMT solver's reach (refinement types).

Referenced by

References

  1. Vazou, Niki, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon L. Peyton Jones. 2014. "Refinement Types for Haskell." Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming (ICFP '14), 269–82. https://doi.org/10.1145/2628136.2628161. ↩

  2. Erbsen, Andres, Jade Philipoom, Jason Gross, Robert Sloan, and Adam Chlipala. 2019. "Simple High-Level Code for Cryptographic Arithmetic: With Proofs, Without Compromises." IEEE Symposium on Security and Privacy (s&p '19), 1202–19. https://doi.org/10.1109/SP.2019.00005. ↩

  3. Leroy, Xavier. 2009. "Formal Verification of a Realistic Compiler." Communications of the ACM 52 (7): 107–15. https://doi.org/10.1145/1538788.1538814. ↩