Refinement and Dependent Types

A type such as integer, string, or List<Item> says what kind of value a program manipulates. It does not necessarily say that an integer is positive, a string is normalized, or two lists have equal length. Those facts often live in comments and tests even when every operation depends on them.

Refinement types and dependent types move such facts into the language of types. A refinement restricts a base type with a predicate. A dependent type allows a type expression to mention a value, so an input can determine the type of an output or two values can carry a statically checked relationship. Both approaches can turn validation results into reusable evidence rather than transient control flow.

Their power has a cost. Richer propositions demand a checking strategy, and arbitrary program properties are not automatically decidable. External bytes still require runtime validation. Proofs can improve an API or bury it under obligations that exceed the risk. The useful goal is therefore not to encode every true statement. It is to choose invariants whose evidence meaningfully changes what later code is allowed to do.

Refine a Base Type with a Predicate #

A refinement type is commonly written as

meaning values x of base type T for which predicate P(x) holds. Examples include non-negative integers, non-empty strings, sorted lists, and indexes smaller than a particular length:

The base representation need not change. What changes is the proposition available to the checker. A function accepting Port may omit a range check only if callers cannot construct that value without supplying evidence. A function returning Index(n) promises not merely an integer, but one related to the particular bound n.

Refinement subtyping follows logical implication. If every value satisfying 1 <= p <= 65535 also satisfies p >= 0, then Port can be used where a non-negative integer is required. The checker establishes this by proving an implication from known predicates, not by comparing field names.

Flow-sensitive narrowing is a modest form of refinement. After if (count > 0), the true branch knows more about count than its declared type alone states. A refinement system makes that knowledge explicit and can preserve it across function boundaries. Instead of repeatedly checking count > 0, code passes a value whose type records the fact.

The predicate must match the claimed invariant precisely. A string that is merely non-empty is not necessarily a valid hostname. A list whose adjacent elements were compared with one ordering is not proven sorted under another. More expressive notation cannot rescue a vague proposition.

Turn Checks into Proof-Carrying Values #

A boolean validator answers a momentary question. Proof-carrying validation returns the value together with evidence of the proposition that downstream code needs. In mathematical notation, a successful result can contain a pair

where the type of the second component depends on the first. If no proof can be constructed, the validator returns an error instead.

There are several ways to obtain that evidence:

• A compiler can derive it statically from path conditions and arithmetic constraints.
• A runtime decision procedure can check a predicate and return either evidence or a counterexample.
• A trusted constructor can establish an invariant while building a data structure.
• A programmer can write a proof whose cases the type checker verifies.

The evidence may have no runtime representation after compilation. Erasure is safe when execution never inspects the proof and the compiler has already checked its construction. Other systems retain a compact witness, certificate, or validation result because another process must inspect it. “Proof-carrying” describes the logical relationship, not a requirement that theorem objects consume production memory.

Evidence has provenance. If code creates a proof through an unchecked cast, assumes an axiom inconsistent with the runtime, or trusts an inaccurate foreign interface, every conclusion derived from it is suspect. The trusted core should therefore be small: primitive decision procedures, total constructors, and reviewed foreign boundaries.

This model changes API design. Parsing is no longer string -> Config; it is string -> Either ParseError ValidConfig. Index selection is not integer -> element; it requires evidence that the integer lies within the collection’s bound. The extra result handling occurs where uncertainty enters, while the interior receives stronger inputs and removes repeated defensive branches.

Keep Automated Checking Decidable #

For unrestricted predicates, automatic checking cannot always terminate or find a proof. A predicate may invoke arbitrary user code, quantify over an infinite domain, or encode whether another program halts. Program equivalence and many useful semantic properties are undecidable in general.

Practical refinement systems choose a tractable logical fragment. Quantifier-free linear arithmetic over integers, equalities over uninterpreted functions, and finite algebraic cases are common examples. The compiler generates verification conditions from the program and asks a decision procedure, often an SMT solver, whether the conditions follow from known facts.

For example, if a function requires {x : Int | x > 10} and a branch knows x >= 20, the obligation is a small arithmetic implication. A loop that increments i while accessing an array may require an explicit invariant such as 0 <= i <= length. The checker cannot infer every useful invariant; annotations connect local steps into an inductive proof.

Restricting the logic is a feature. It gives predictable termination and a clear boundary for automation. When the solver cannot prove a true statement, the system should report an obligation, not silently accept it. The programmer can strengthen an invariant, split a function, provide a lemma, or fall back to a checked runtime predicate.

Runtime validation is more permissive about the predicate because it can execute ordinary code on one concrete input. That does not make the general proposition decidable. A regex can decide whether this string matches; it does not prove a theorem about every future string. A runtime checker also needs termination and resource limits, especially when inputs can trigger expensive search.

Proof assistants take another route: programmers construct proofs interactively, while a small kernel verifies each term. They can express much richer mathematics, but automation and ergonomics differ from lightweight refinements. The right question is not which system is most powerful. It is which obligations need automation, explicit proof, or runtime rejection.

Let Types Depend on Values #

Dependent types generalize the relationship between values and types. A classic example is a vector Vec(A, n): a sequence of elements of type A whose length is the value n. The length is part of the type, so a function can express relationships that an ordinary list signature omits.

Two constructions appear repeatedly. A dependent function type, often written with $\Pi$, lets the result type depend on the argument:

Such a function accepts a natural number n and returns exactly n elements. A dependent pair type, written with $\Sigma$, packages a value with a component whose type depends on it:

This pair is useful when the length is discovered at runtime. The caller does not know which n it received, but it knows that the packaged vector has that same length.

Other examples include matrices indexed by row and column counts, protocol states indexed by legal transitions, syntax trees indexed by the type of expression they represent, and permission values indexed by the resource they authorize. The index need not exist at runtime after checking, although it often corresponds to ordinary data already present.

A refinement can be viewed as selecting values of one base type that satisfy a proposition. Full dependency can describe relationships among several values and produce different type structures for different indexes. The boundary is not always sharp in language implementations, but the design distinction is useful: refinements constrain membership, while dependent signatures make value relationships shape composition.

Dependency does not imply that every value should appear in a type. Highly dynamic business policy, user-authored expressions, and facts that change independently of a value’s lifetime may be clearer as runtime data. Index stable structural relationships whose violation would make an operation nonsensical.

Work Through Dimension-Safe Matrices #

Matrix multiplication illustrates a relationship that ordinary element types miss. A matrix with dimensions $m \times n$ can multiply a matrix with dimensions $n \times p$, producing an $m \times p$ matrix. The inner dimensions must match:

In dependent pseudocode, vectors enforce both row width and row count:

Matrix : Nat -> Nat -> Type -> Type
Matrix rows cols element = Vec (Vec element cols) rows

multiply : Matrix m n Number
        -> Matrix n p Number
        -> Matrix m p Number

The implementation cannot be called with a 3 x 4 matrix and a 5 x 2 matrix because no substitution makes the shared index n both 4 and 5. The output dimensions follow from the inputs without a comment or caller-selected annotation.

Real matrices often arrive from a file or network, so their dimensions are not known at compile time. A parser can validate that every row has equal length and package the discovered dimensions with the matrix:

record SomeMatrix element where
  rows   : Nat
  cols   : Nat
  value  : Matrix rows cols element

parseMatrix : Bytes -> Either MatrixError (SomeMatrix Number)

Now consider multiplying two parsed values. Their inner dimensions are initially unrelated. The program runs a decidable equality check:

multiplySome : SomeMatrix Number
            -> SomeMatrix Number
            -> Either DimensionError (SomeMatrix Number)

multiplySome left right =
  case decideEqual left.cols right.rows of
    Yes Refl => Right (Pack left.rows right.cols
                             (multiply left.value right.value))
    No proofOfDifference => Left (Mismatch left.cols right.rows)

Refl is evidence that the compared dimensions are equal. In the successful branch, the checker rewrites right.rows as left.cols, making the static multiply signature applicable. In the failure branch, the returned error contains the concrete mismatch. One runtime comparison creates evidence that safely governs the rest of the operation.

The parser carries important proof obligations. It must reject ragged rows, numeric decoding failures, and dimensions too large for resource policy. The type prevents dimension mismatch after construction; it does not prevent memory exhaustion or floating-point error. The worked example shows both the strength and limit of the guarantee.

Budget for Proof and API Ergonomics #

Stronger types move effort. They remove invalid call paths but add indexes, equality transport, lemmas, totality requirements, and more precise error handling. A proof can break after an implementation refactor even when runtime behavior remains acceptable, because the checker needs a new route from assumptions to conclusion.

The cost is worthwhile when an invariant is stable, compositional, and expensive to violate. Matrix dimensions, bounded indexes, parser well-formedness, and protocol sequencing often qualify. A frequently changing pricing policy may be easier to validate as data with decision-table tests. Encoding it as a theorem can couple releases to proof maintenance without eliminating the need to test the policy source.

Hide proof machinery behind small constructors and combinators. A caller should usually request multiplySome rather than manually transport equality evidence. Error messages should report domain values such as expected and actual dimensions, not expose internal unification terms. Inferred indexes reduce annotation noise, but important relationships should remain visible in public signatures.

Beware of proof theater. An opaque “trusted” conversion that can manufacture any proposition makes the surrounding precision misleading. So does a postcondition that restates a weak implementation fact instead of the business invariant. Review propositions with the same care as executable requirements: ask what they exclude, what assumptions they use, and whether those assumptions survive mutation and concurrency.

Immutability or controlled ownership often supports the proof. Evidence that a list is sorted becomes stale if another alias can reorder it. A bound proven against one array length is unsafe if the array can shrink independently. The type and memory model must agree about which values remain stable.

Validate Dynamic Boundaries and Preserve Evidence #

Static types do not inspect JSON, database rows, command-line arguments, or corrupted files. The boundary should decode syntax, validate semantic predicates, and return a proof-carrying value or a structured error. After that transition, internal code can rely on the established invariant without repeating checks.

Serialization usually erases evidence. A Vec(A, n) written as a JSON array does not force another process to agree on n; the receiver must count and reconstruct the package. If a protocol transmits both a claimed count and elements, validation must prove they agree rather than trusting the redundant field.

Versioning matters because predicates evolve. Tightening a refinement from non-empty names to normalized names changes which stored values are valid. Plan migration or support versioned validators instead of asserting that old data satisfies the new proposition. Report validation failures by schema and reason so operators can distinguish malformed input, obsolete data, and a buggy producer.

Security boundaries deserve independent limits. A proof that dimensions match says nothing about whether dimensions are acceptable. Check maximum rows, columns, nesting depth, integer overflow, and evaluation cost before allocating. Logical validity is one layer of input safety, not the complete policy.

When evidence crosses a trust boundary in certificate form, verify the certificate with a small checker and bind it to the exact payload, version, and algorithm. A valid proof about one digest must not be reusable for different bytes. This is the operational form of the same principle: evidence is meaningful only in the context named by its proposition.

Verify the Verifier and Choose Proportionately #

Compile-time proofs and runtime tests cover different risks. The type checker verifies every well-typed construction under its trusted rules. Tests exercise parsers, foreign interfaces, resource behavior, and the assumptions imported into those rules. A proof can establish that matrix dimensions compose; tests still need to cover numeric results and parsing errors.

For the matrix example, verification should include:

• Compile-time examples showing incompatible static dimensions are rejected.
• Unit tests for empty, rectangular, ragged, malformed, and oversized input.
• Property tests comparing valid multiplication with a simple reference implementation.
• Round-trip tests that serialize, parse, and recover the same dimensions and elements.
• Mutation or ownership tests ensuring a validated structure cannot become ragged through an alias.
• Tests that every failed dynamic equality produces the expected structured mismatch.

Decision procedures need testing too. Keep their trusted implementation small, compare them with known positive and negative cases, and fuzz parsers for proof or certificate formats. For solver-backed systems, pin tool versions where reproducibility matters and retain enough diagnostics to inspect an unproved obligation. A timeout should mean “not proved,” never “assume true.”

Choose the lightest mechanism that preserves the important relationship. Ordinary algebraic types handle finite alternatives well. Runtime schemas handle dynamic object shapes. Refinements add predicates and automated obligations. Dependent types express exact relationships among values and outputs. Explicit proofs cover properties beyond automation. These mechanisms can coexist across one system.

Refinement and dependent types are most valuable when they make evidence reusable. Validate uncertainty once, carry the result in a type, and let later composition preserve the proposition. Keep the logic decidable where automation is expected, expose dynamic failures honestly, and test every boundary the proof system must trust. The result is not a program with no runtime errors; it is a program whose strongest invariants have named evidence and far fewer places where that evidence can be lost.