Refinement and Dependent Types: Towards Types That Prove

Beyond classical typing, certain systems allow encoding finer properties. The compiler then becomes a proof assistant, enabling enforcement of even more precise business invariants.

Refinement Types

Refinement types constitute an extension of traditional type systems where we refine a base type with a logical predicate.

Rather than simply declaring that a variable is an integer, we can specify that it is, for example:

• A strictly positive integer
• An integer between 0 and 100
• An even integer

The classic notation borrows from set theory: $\{ x : \text{Int} \mid x > 0 \}$ denotes the type of integers satisfying the predicate $x > 0$.

The compiler or an external solver (often an SMT solver) then statically verifies that every value assigned to this type respects the constraint, transforming runtime errors into compilation errors.

Dependent Types

Dependent types go even further: they allow types to depend on values.

In a dependently typed system, we can express the type $\text{Vector}\langle n \rangle$ where $n$ is an integer value representing the vector’s length. The function:

$\text{concat} : \text{Vector}\langle n \rangle \to \text{Vector}\langle m \rangle \to \text{Vector}\langle n + m \rangle$

encodes in its signature that concatenation produces a vector whose length is the sum of the operands’ lengths.

The type $\text{head} : \text{Vector}\langle n + 1 \rangle \to A$ guarantees that this function can only be called on a non-empty vector: the error case disappears by construction.

Types become a formal specification language verified by the compiler.

Refinement vs Dependent: What’s the Difference?

The distinction between these two approaches is sometimes blurry, but can be summarized as follows:

• Refinement types enrich existing types with predicates verified separately, often by an automatic solver
• Dependent types integrate values directly into the type system itself, sometimes requiring explicit proofs

Liquid Haskell  illustrates the refinement approach: we annotate standard Haskell code and an SMT solver verifies the constraints. Idris , Agda , or Lean  embody the pure dependent approach: proofs are an integral part of the program and the developer must sometimes construct them manually.

Practical Applications

In practice, these systems allow encoding invariants impossible to express in languages like TypeScript or Java:

• Array access can be proven bounds-safe by the type itself
• A division function can require a denominator of type $\{ x : \text{Int} \mid x \neq 0 \}$, eliminating any possibility of division by zero
• A network protocol can be modeled as a state machine at the type level, making it impossible to send a message in the wrong order

We go beyond simple Make Illegal States Unrepresentable to reach “Make Illegal Operations Untypeable”: programs that compile are correct by construction, at least with respect to the encoded properties.

Limits and Trade-offs

However, this power has a cost:

• Type inference often becomes undecidable or requires heavy annotations
• Error messages can be cryptic, mixing formal logic and solver constraints
• The ecosystem is more restricted: fewer libraries, less tooling, steep learning curve
• Time spent convincing the compiler can exceed time spent writing the logic itself

These tools find their place in domains where correctness is critical (embedded systems, cryptography, consensus protocols, etc.) but remain marginal in common application development.

They nonetheless represent the horizon toward which type systems gradually progress, and fragments of their ideas slowly infuse into mainstream languages.