Refinement type

also: liquid type

A base type paired with a logical predicate that its values must satisfy, such as the integers greater than zero. Checking is discharged by an SMT solver at compile time, so the guarantees are stronger than a plain type without requiring dependent-type-style proof terms from the programmer.

A refinement type is a base type carved down by a logical predicate: not Int but the integers satisfying ${v : Int ∣ v > 0}$ . The predicates are drawn from a decidable logic, so an SMT solver discharges the obligations at compile time and the programmer writes no proof terms.

LiquidHaskell. The refinement on `div` is a precondition; the one on `average` is what makes the call site check.

{-@ 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 boundary with dependent types is about who does the work. A dependent type can express anything and asks you 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 and quantifier alternation, is where the approach stops.