# 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](https://github.com/mit-plv/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](https://ucsd-progsys.github.io/liquidhaskell/)** — refinement types
layered on GHC, SMT-discharged via [Z3](https://github.com/Z3Prover/z3) or
[CVC5](https://cvc5.github.io/); 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\*](https://www.fstar-lang.org/)** — dependent types + SMT;
[Project Everest](https://project-everest.github.io/)'s verified TLS.
- **[Dafny](https://dafny.org/)** — verification-oriented language; SMT under
the hood; used for AWS encryption SDK validation.
- **[Verus](https://github.com/verus-lang/verus)** — Rust-flavored verification language;
SMT-backed; proof-carrying Rust for systems code.
- **[Why3](https://www.why3.org/)** — multi-prover frontend; dispatches to Coq,
[Alt-Ergo](https://alt-ergo.ocamlpro.com/), Z3, CVC5.
### Full dependent types (proof assistants)
- **[Idris 2](https://www.idris-lang.org/)** — dependent types with linear
quantifiers.
- **[Agda](https://github.com/agda/agda)** — dependent types on a theory close to
Coq's; used for mathematics and programming-language research.
- **[Lean 4](https://lean-lang.org/)** — dependent types with strong automation
tactics (`omega`, `polyrith`, `decide`, `aesop`).
- **[Coq](https://rocq-prover.org/) / Rocq** — dependent types with tactic-based
interactive proof; [CompCert](https://compcert.org/) and Fiat-Crypto are
written in it.
### SMT solvers underneath
- **[Z3](https://github.com/Z3Prover/z3)**, **[CVC5](https://cvc5.github.io/)**, **[Yices2](https://yices.csl.sri.com/)**,
**[Alt-Ergo](https://alt-ergo.ocamlpro.com/)**. 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](https://sel4.systems/)),
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](https://quality.stereobooster.com/theorem-proving.md).
- 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](https://quality.stereobooster.com/contracts-and-runtime-assertions.md) or
[property-based testing](https://quality.stereobooster.com/property-based-testing.md).
- 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)[^vazou2014].
- **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)[^erbsen2019].
- **CompCert.** Verified compiler from Clight (a large C subset)
to PowerPC assembly, written in Coq (Leroy 2009)[^leroy2009].
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.
## Related
**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](https://quality.stereobooster.com/contracts-and-runtime-assertions.md) —
*check* P during execution, on the inputs you actually run, and crash if it's
violated.
- [Property-based testing](https://quality.stereobooster.com/property-based-testing.md) — *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](https://quality.stereobooster.com/theorem-proving.md) — *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
- [The axes](https://quality.stereobooster.com/axes.md) · The axes
- [Contracts and runtime assertions](https://quality.stereobooster.com/contracts-and-runtime-assertions.md) · Methods
- [Contracts as specifications](https://quality.stereobooster.com/contracts-as-specifications.md) · Methods
- [Effect systems](https://quality.stereobooster.com/effect-systems.md) · Methods
- [Exhaustive coverage (MC/DC, MCC)](https://quality.stereobooster.com/exhaustive-coverage.md) · Methods
- [Termination analysis](https://quality.stereobooster.com/termination-analysis.md) · Methods
- [Types and effects](https://quality.stereobooster.com/types.md) · Methods
- [Verifying memory safety](https://quality.stereobooster.com/memory.md) · Methods
- [How AI fits into software quality](https://quality.stereobooster.com/ai.md) · AI
## References
[^vazou2014]: Vazou, Niki, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon L. Peyton Jones. 2014. "[Refinement Types for Haskell](https://goto.ucsd.edu/~nvazou/refinement_types_for_haskell.pdf)." *Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming (ICFP '14)*, 269–82. .
[^erbsen2019]: Erbsen, Andres, Jade Philipoom, Jason Gross, Robert Sloan, and Adam Chlipala. 2019. "[Simple High-Level Code for Cryptographic Arithmetic: With Proofs, Without Compromises](https://dspace.mit.edu/bitstreams/77b6c2d1-49af-427f-a5a7-bf393f3bd5de/download)." *IEEE Symposium on Security and Privacy (s&p '19)*, 1202–19. .
[^leroy2009]: Leroy, Xavier. 2009. "[Formal Verification of a Realistic Compiler](https://xavierleroy.org/publi/compcert-CACM.pdf)." *Communications of the ACM* 52 (7): 107–15. .
## Acronyms
- MC/DC — modified condition/decision coverage
- MCC — multiple-condition coverage
- SMT — satisfiability modulo theories