Refinement type

A refinement type is a base type carved down by a logical predicate: not Int but the integers satisfying $\{v:\mathtt{Int}\mid v>0\}$^[1][6]. A function type can refine its arguments, stating preconditions, and its result, stating a postcondition that may mention the arguments. Checking reduces to subtyping between refinements, which reduces to the validity of implications in the refinement logic; those verification conditions are discharged by an SMT solver at compile time, and the programmer writes no proof terms. The approach grew from Freeman and Pfenning's refinements of ML datatypes in 1991^[1] and Xi and Pfenning's Dependent ML^[4], and was made largely automatic by Liquid Types in 2008^[3], which infer refinements from a set of candidate predicates. LiquidHaskell brought it to Haskell^[2], and F* combines refinements with full dependent types^[5].

{-@ type Pos = {v:Int | v > 0} @-}
 
{-@ safeDiv :: Int -> Pos -> Int @-}
safeDiv :: Int -> Int -> Int
safeDiv x y = x `div` y
 
{-@ average :: {v:[Int] | len v > 0} -> Int @-}
average :: [Int] -> Int
average xs = safeDiv (sum xs) (length xs)   -- len xs > 0 discharges Pos

The annotations are comments that ordinary GHC ignores. LiquidHaskell checks that every call to safeDiv passes a positive divisor: in average it knows length xs = len xs and len xs > 0, and the solver proves length xs > 0. A call average [] elsewhere would be rejected^[2].

A refinement type $\{v:B\mid p\}$ is a subtype of $\{v:B\mid q\}$ when every value satisfying $p$ satisfies $q$, given what is known in the current environment $\Gamma$^[3][6]:

Here $[[\Gamma ]]$ is the conjunction of the refinements of the variables in scope, together with the branch conditions on the current path. Function types are contravariant in their arguments, as usual. Every place where a value flows into a position with a declared refinement, such as a function argument or a function's result, generates one such implication, a verification condition.

The implication $H\Rightarrow g$ is valid exactly when $H\wedge \neg g$ is unsatisfiable, which is the question an SMT solver answers. For the checker to be complete and terminating, predicates must come from a decidable logic. The usual choice is quantifier-free linear integer arithmetic with uninterpreted functions and equality; functions of data structures, such as the length of a list, enter as uninterpreted functions called measures^[2].

The core of a refinement type checker fits in a page. The one below handles integer functions whose refinements are conjunctions of linear comparisons. It checks if expressions by adding the condition, or its negation, to the hypotheses of each branch; it checks calls by proving each argument's refinement and assuming the callee's result refinement; and it uses a function's declared type for its recursive calls. Verification conditions are decided by Fourier–Motzkin elimination over the rationals^[9], which is sound for the integers when used to prove unsatisfiability, after strict inequalities are tightened to $t+1\le 0$.

(* hyps |= goal, over the integers (soundly, via the rationals) *)
let valid (hyps : atom list) (goal : atom) =
  let h = List.concat_map to_le hyps in
  let r = List.for_all (fun alt -> not (sat (h @ List.concat_map to_le alt))) (negate goal) in
  (match !trace with Some l -> l := (hyps, goal, r) :: !l | None -> ());
  r
 
let subst_atom x by ((a, c, b) : atom) = (subst x by a, c, subst x by b)
 
let fresh = let n = ref 0 in fun base -> incr n; Printf.sprintf "%s%d" base !n
 
exception Unproved of string

open Refine
open Show

abs(x : int) : {v | v >= 0 && v >= x}
  = if x >= 0 then x else 0 - x
  checks
max(x : int, y : int) : {v | v >= x && v >= y}
  = if x >= y then x else y
  checks
bad_abs(x : int) : {v | v >= 0}
  = if x >= 0 then x else x
  REJECTED: cannot prove the result in the else branch
clamp(lo : int, hi : {v | v >= lo}, x : int) : {v | v >= lo && v <= hi}
  = if x < lo then lo else if x > hi then hi else x
  checks

open Refine
open Show

abs:
  x >= 0       |- x >= 0   valid
  x < 0        |- -x >= 0  valid
bad_abs:
  x >= 0       |- x >= 0   valid
  x < 0        |- x >= 0   NOT VALID

The failed condition, $x<0⊢x\ge 0$, has a counterexample, any negative $x$, which an SMT solver would return as a model.

Preconditions

Refinements on arguments are preconditions that every caller must establish. Division by zero and out-of-bounds indexing become type errors.

open Refine
open Show

div(x : int, y : {v | v > 0}) : int
  (assumed)
get(len : {v | v >= 0}, i : {v | v >= 0 && v < len}) : int
  (assumed)
ratio(a : int, b : int) : int
  = if b > 0 then div(a, b) else 0
  checks
unsafe_ratio(a : int, b : int) : int
  = div(a, b)
  REJECTED: cannot prove the argument y of div
last(len : {v | v >= 1}) : int
  = get(len, len - 1)
  checks
off_by_one(len : {v | v >= 1}) : int
  = get(len, len)
  REJECTED: cannot prove the argument i of get
sum_to(k : {v | v >= 0}) : {v | v >= k}
  = if k <= 0 then 0 else k + sum_to(k - 1)
  checks

In ratio the branch condition b > 0 is a hypothesis in the then branch, which is exactly what the precondition of div needs. The recursive sum_to is checked using its own signature for the recursive call: in the else branch k ≥ 1, so the argument k - 1 is non-negative, and the result $k+r$ with $r\ge k-1$ is at least $k$.

Checking requires a refinement on every function, and on intermediate values such as loop variables and the elements of data structures. Liquid Types infer these^[3]. The programmer supplies, or the tool guesses, a finite set of qualifiers, predicate templates such as $v\ge 0$, $v<\star$ or $v=\mathrm{len}\star$. The unknown refinements are conjunctions of instances of the qualifiers, and the verification conditions become a system of Horn clauses over these unknowns; a fixpoint computation, predicate abstraction, finds the strongest conjunction that satisfies them. Because the space of candidates is finite, inference terminates.

The boundary with dependent types is about who does the work. A dependent type can express anything and asks the programmer to prove it; a refinement type is limited to what the solver decides, and in exchange the proof is found rather than written. Everything outside that fragment, typically nonlinear arithmetic, quantifiers and properties of recursive functions, is where the approach stops or needs help. Refinement reflection in LiquidHaskell lets function definitions be unfolded into the logic, so that programs can state and prove properties of recursive functions with proof terms written as ordinary Haskell, recovering some of the expressiveness of dependent types^[8]. F* goes further, combining refinements discharged by an SMT solver with full dependent types and effects^[5].

A refinement type is a subset of an ordinary type, so refinements can be erased, leaving a well-typed program in the underlying language. This makes refinements easy to add to an existing language: LiquidHaskell checks ordinary Haskell programs^[2], and F7 checked annotated F# code for security properties of cryptographic protocols^[7].

Freeman and Pfenning introduced refinement types in 1991 as refinements of ML datatypes, such as the non-empty lists, with inference by abstract interpretation over a finite lattice^[1]. Xi and Pfenning's Dependent ML of 1998–1999 indexed types by integer expressions and checked constraints with a decision procedure for linear arithmetic^[4]. Liquid Types, by Rondon, Kawaguchi and Jhala in 2008, used SMT solvers and predicate abstraction to infer refinements automatically^[3], and LiquidHaskell brought the approach to Haskell in 2014^[2]. Bengtson and colleagues used refinement types to verify cryptographic protocol implementations in F7^[7], which led to F*^[5]. Refinement reflection extended LiquidHaskell to proofs about recursive functions in 2018^[8].

• SMTSatisfiability modulo theories (SMT) is the problem of deciding whether a first-order formula is satisfiable when some of its symbols are interpreted by background theories, such as integer or real arithmetic, bit-vectors, arrays and uninterpreted functions. SMT solvers such as Z3 and cvc5 combine a SAT solver, which handles the Boolean structure, with specialized decision procedures for the theories, usually in the DPLL(T) architecture. They read the standard SMT-LIB language and are the reasoning engines of program verifiers, symbolic execution tools, test generators and many other analysis tools.
• Dependent typeA dependent type is a type that may mention values, so that a vector's length can appear in its type and a function's result type can be computed from its arguments. Function types generalize to dependent products Π(x : A). B(x), and pairs to dependent sums Σ(x : A). B(x). Because types can express propositions and programs can be proofs, languages with dependent types, such as Agda, Coq (Rocq), Lean and Idris, double as proof assistants. The price is that type checking involves evaluating programs, so these languages require functions to terminate, and type equality is decided up to computation.
• Phantom typeA phantom type is a type parameter that appears in a type's declaration but in none of its fields, used to keep otherwise identical representations apart: lengths in metres and in feet, validated and unvalidated strings, read-only and writable handles, SQL expressions of different result types. It carries no data and costs nothing at run time. Combined with an abstract type whose constructors are hidden, it lets a library enforce invariants through the type checker. Unlike a GADT index it tells a pattern match nothing; it constrains what callers may do, not what the compiler can learn.
• GADTA generalized algebraic data type (GADT) is an algebraic data type whose constructors may each give a more specific result type than the declared one, instead of all sharing one polymorphic return type. Matching on a constructor then tells the type checker what the type parameter was, so a single well-typed eval can return an int for an Add node and a bool for an Eq node, checked at compile time rather than by a run-time tag test. GADTs express typed syntax trees, type representations and equality proofs, typed format strings and length-indexed data. The price is that type inference needs annotations.
• Theory solverIn an SMT solver, a theory solver decides whether a conjunction of literals of one theory, such as linear arithmetic or equality with uninterpreted functions, is consistent. The SAT search asserts literals to it incrementally and asks it to check them; on inconsistency it returns an explanation, a small subset of the asserted literals that is already inconsistent, which the SAT search learns as a clause. A theory solver must also undo assertions when the search backtracks, and it may propagate literals that the asserted ones imply. The quality of explanations and propagation largely determines the solver's performance.
• Fourier–Motzkin eliminationFourier–Motzkin elimination removes a variable from a system of linear inequalities by combining every inequality that bounds the variable from below with every inequality that bounds it from above. The result has a solution exactly when the original system does, over the real or rational numbers, and describes the projection of the solution set. Eliminating all variables decides satisfiability, and back-substitution recovers a solution, but the number of inequalities can grow doubly exponentially.

1. [1]T. Freeman, F. Pfenning, “Refinement types for ML”, PLDI (1991).
2. [2]N. Vazou, E. L. Seidel, R. Jhala, D. Vytiniotis, S. Peyton Jones, “Refinement types for Haskell”, ICFP (2014).
3. [3]P. M. Rondon, M. Kawaguchi, R. Jhala, “Liquid types”, PLDI (2008).
4. [4]H. Xi, F. Pfenning, “Dependent types in practical programming”, POPL (1999).
5. [5]N. Swamy et al., “Dependent types and multi-monadic effects in F*”, POPL (2016).
6. [6]R. Jhala, N. Vazou, “Refinement types: a tutorial”, Foundations and Trends in Programming Languages 6 (2021).
7. [7]J. Bengtson, K. Bhargavan, C. Fournet, A. D. Gordon, S. Maffeis, “Refinement types for secure implementations”, ACM Transactions on Programming Languages and Systems 33 (2011).
8. [8]N. Vazou, A. Tondwalkar, V. Choudhury, R. G. Scott, R. R. Newton, P. Wadler, R. Jhala, “Refinement reflection: complete verification with SMT”, POPL (2018).
9. [9]G. B. Dantzig, B. C. Eaves, “Fourier–Motzkin elimination and its dual”, Journal of Combinatorial Theory, Series A 14 (1973).

last updated 29 September 2026