LiquidHaskell

Well then, time to let in the liquid one — as in Terminator 2, where a robot of liquid metal appears. The type $\mathtt{Int}$ guarantees the shape but says nothing about the content: that a number is non-zero, that a list is non-empty, that an index stays in bounds. LiquidHaskell hangs logical predicates onto ordinary Haskell types — refinement types — and checks them at compile time with an SMT solver (Z3). The “decorator” annotations live in special comments $\mathtt{\{\text{-}@\;\ldots\;@\text{-}\}}$, so the code remains plain Haskell and builds with plain GHC. The decorator syntax:

— “values of type $\tau$ for which the predicate $p$ holds”. The basic example is a division that cannot be called with zero:

{-@ type NonZero = {v:Int | v /= 0} @-}

{-@ safeDiv :: Int -> NonZero -> Int @-}
safeDiv :: Int -> Int -> Int
safeDiv x y = x `div` y

ok  = safeDiv 10 2    -- passes: the solver sees for itself that 2 /= 0
bad = safeDiv 10 0    -- compile error: 0 does not fit into NonZero

Under the hood this is subtyping — a comparison of two refined types, each with its own predicate: $p$ on the argument, $q$ on the parameter. The type $\{\, v:\tau \mid p \,\}$ is a subtype of $\{\, v:\tau \mid q \,\}$ when every value satisfying $p$ satisfies $q$ as well — and this implication is exactly what the SMT solver checks. For the call $\mathtt{safeDiv}\;10\;2$ the argument has $p$ $\equiv (v = 2)$ — the singleton type of the literal — the parameter $\mathtt{NonZero}$ has $q$ $\equiv (v \neq 0)$, and the implication $v$ $= 2$ $\Rightarrow v$ $\neq 0$ holds:

Predicates can use measures — simple functions over data that LiquidHaskell knows how to unfold in the logic. The classic is $\mathtt{head}$, which stops being partial:

{-@ measure len @-}
len :: [a] -> Int
len []     = 0
len (_:xs) = 1 + len xs

{-@ head' :: {v:[a] | len v > 0} -> a @-}
head' :: [a] -> a
head' (x:_) = x    -- no [] branch needed: the type rules it out

LiquidHaskell also checks recursion for termination — it looks for a decreasing metric (by default, the first numeric argument). The type $\mathtt{Nat}$ in the signature is LiquidHaskell’s built-in alias $\{\, v:\mathtt{Int} \mid v$ $\geq 0 \,\}$, declared just like our $\mathtt{NonZero}$. The factorial from the section on the Y combinator is total here:

{-@ fac :: Nat -> Nat @-}
fac :: Int -> Int
fac 0 = 1
fac n = n * fac (n - 1)   -- n decreases and never drops below zero — the solver is satisfied

In reflection mode, decorators prove genuine theorems: the property is written as a type, the proof as a program. This is the Curry–Howard correspondence:

{-@ LIQUID "--reflection" @-}
import Language.Haskell.Liquid.ProofCombinators

{-@ reflect double @-}
double :: Int -> Int
double x = x + x

{-@ doubleIsTwice :: x:Int -> { double x == 2 * x } @-}
doubleIsTwice :: Int -> Proof
doubleIsTwice x = double x === x + x === 2 * x *** QED

This is a step toward types that depend on terms, but not full dependent types as in Agda: the predicates are restricted to SMT-decidable theories (linear arithmetic, equality, sets) — in return, everything is checked automatically, with no manual proofs.