Polymorphic Coverage Types
Zhe Zhou, Ashish Mishra, Benjamin Delaware, Suresh Jagannathan
TL;DR
The paper reframes test-input generator coverage as a type-theoretic underapproximation problem by introducing coverage types, a must-style refinement system that inverts traditional subtyping. It develops a core ML-like language with higher-order constructs, inductive datatypes, and a bidirectional typing algorithm that supports polymorphism and monadic generator combinators, enabling static verification of generator completeness. The authors implement an OCaml coverage-type checker, conduct extensive evaluations on hand-written and synthesized generators, and demonstrate practical utility across real-world PBT applications and monadic combinators. Overall, the approach provides a scalable, automated mechanism to certify that generators exhaustively cover the intended input space, with potential to guide repairs and improve documentation of generator behavior.
Abstract
Test input generators are an important part of property-based testing (PBT) frameworks, and a key expectation is that they be capable of producing all acceptable elements that satisfy both the function's input type and the generator-provided constraints. However, it is not readily apparent how to validate whether a particular generator's output satisfies this coverage requirement. In practice, developers typically rely on manual inspection and post-mortem analysis of test runs to determine whether a generator provides sufficient coverage; these approaches are error-prone and difficult to scale as generators grow more complex. To address this problem, we present a new refinement-type-based verification procedure for validating the coverage provided by input test generators, based on a novel interpretation of types that embeds "must-style" underapproximate reasoning principles as a fundamental part of the type system. In our formulation, the types associated with expressions capture the set of values guaranteed to be produced by the expression, rather than the usual interpretation in which types represent the set of values an expression may produce. We formalize the notion of coverage types in a rich core language supporting higher-order functions and inductive datatypes. To better support real-world test generators, we extend this type system with type and qualifier polymorphism, enabling static verification of coverage guarantees for test input generators constructed using the monadic combinators found in most PBT frameworks. Finally, we have implemented a coverage type checker for OCaml programs based on this core calculus and present a detailed evaluation of its utility using a corpus of benchmarks drawn from both the PBT literature and open-source projects.