Skip to content

Software Quality

Refinement and dependent types

Refinement and dependent types are type systems whose types state predicates over values, not only the shape of the data. 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 a division whose divisor is not proved non-zero before the program runs.
  • 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 cannot hold an unbalanced tree; a SortedList n is indexed by its length and cannot hold its elements out of 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 SMT discharges the easy obligations and hand-written lemmas the rest; of these tools only F* has full dependent types SMT + hand-written lemmas 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 hybrid

  • 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.
  • For an existing Haskell codebase. Liquid Haskell refinement types can be added to it incrementally.

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. Its elliptic-curve field arithmetic is proved correct in Coq, and the straight-line implementation is generated from a high-level functional one by partial evaluation (Erbsen et al. 2019)2.
  • CompCert. The compiler from Clight (a large C subset) to PowerPC assembly is written and proved correct in Coq (Leroy 2009)3.

The support is definitional, not statistical: these results demonstrate verified artifacts rather than measure defect rates against unverified code.

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. ↩