Questions: Refinement Types

Question 1

How does the refinement type {v : Int | v > 0 && v < 100} differ from a runtime assertion assert(v > 0 && v < 100)?

• A. They check the same property but at different times: the refinement type checks statically at compile time, while the assertion checks at runtime. The refinement type guarantees the property holds on ALL executions, while the assertion only catches violations on executions that are actually run
• B. The refinement type is less precise than the assertion
• C. The assertion provides a formal proof while the refinement type does not
• D. There is no meaningful difference; they are equivalent

Answer: (A)

This is the fundamental value proposition of refinement types: they move runtime checks to compile time. If the program type-checks, the property is guaranteed to hold in all executions without any runtime cost. If the type checker cannot prove the property, it reports a type error before the program runs. Assertions catch bugs only in executions that are actually tested. Refinement types catch all possible violations statically.

Question 2

Liquid types achieve automatic type checking by restricting refinement predicates to decidable logics that SMT solvers can handle.

• T. True
• F. False

Answer: True

Full dependent types allow arbitrary computations in types, making type checking undecidable and requiring manual proof effort. Liquid types restrict refinements to quantifier-free formulas over SMT-decidable theories (linear arithmetic, arrays, uninterpreted functions). This restriction means subtype checking reduces to SMT validity queries, which Z3 or CVC5 can decide automatically. The user writes type annotations (or they are inferred); the tool generates SMT queries; no manual proofs are needed. This is the key tradeoff: less expressive than full dependent types, but fully automatic.

Question 3

Explain how refinement type checking reduces to SMT queries, using the example of checking that a function call div(x, y) is safe where div expects {v : Int | v != 0} as its second argument.

Model answer: At the call site div(x, y), the type checker must verify that y has type {v : Int | v != 0}. It collects the path conditions (e.g., from an enclosing 'if y != 0' branch) and the refinements of y's declared type, forming the context. It then asks the SMT solver: given the context, is y != 0 valid? If the solver says yes (valid), the call type-checks. If the solver says no (with a counterexample), the type checker reports an error showing a concrete scenario where y could be zero.

This reduction is what makes refinement types practical. Every subtyping check {v : T | P} <: {v : T | Q} reduces to the implication P => Q, which is an SMT query. Path-sensitivity comes from collecting predicates from conditional branches: inside 'if y != 0 then div(x, y)', the path condition y != 0 is added to the context, making the SMT query trivially valid. The programmer writes normal code with type annotations; the tool handles the rest.