What is the best practice to generate data which satisfy specific property in QuickCheck?

user_1608276 0
Viewed 165

When we are using QuickCheck to check our programs, we need to define generators for our data, there is some generic way to define them, but the generic way usually become useless when we need the generated data to satisfy some constraints to work.

e.g.

data Expr
    = LitI Int
    | LitB Bool
    | Add Expr Expr
    | And Expr Expr

data TyRep = Number | Boolean

typeInfer :: Expr -> Maybe TyRep
typeInfer e = case e of
    LitI _ -> Number
    LitB _ -> Boolean
    Add e1 e2 -> case (typeInfer e1, typeInfer e2) of
        (Just Number, Just Number) -> Just Number
        _ -> Nothing
    And e1 e2 -> case (typeInfer e1, typeInfer e2) of
        (Just Boolean, Just Boolean) -> Just Boolean
        _ -> Nothing

now I need to define generator of Expr (i.e. Gen Expr or instance Arbitrary Expr), but also want it generates the type correct ones (i.e. isJust (typeInfer generatedExpr))

a naive way to do that is use suchThat to filter out the invalid ones, but that is obviously inefficient when Expr and TyRep becomes complicated with more cases.

Another similar situation is about reference integrity, e.g.

data Expr
    = LitI Int
    | LitB Bool
    | Add Expr Expr
    | And Expr Expr
    | Ref String -- ^ reference another Expr via it's name

type Context = Map String Expr

In this case, we want all the referenced names in the generated Expr are contained in some specific Context, now I have to generate Expr for specific Context:

arbExpr :: Context -> Gen Expr

but now shrink will be a problem, and to solve this problem, I have to define a specific version of shrink, and use forAllShrink everytime I use arbExpr, that means a lot of work.

So I want to know, is there a best practice to do such things?

property-based-testing quickcheck haskell
1 Answers

For well-typed terms, a simple approach in many cases is to have one generator for each type, or, equivalently, a function TyRep -> Gen Expr. Adding variables on top of that, this usually turns into a function Context -> TyRep -> Gen Expr.

In the case of generating terms with variables (and with no or very simple types), indexing the type of terms by the context (e.g., like you would do using the bound library) should make it quite easy to derive a generator generically.

For shrinking, hedgehog's approach can work quite well, where Gen generates a value together with shrunk versions, sparing you from defining a separate shrinking function.

Note that as the well-formedness/typing relation becomes more complex, you start hitting the theoretical wall where generating terms is at least as hard as arbitrary proof search.

For more advanced techniques/related literature, with my own comments about possibly using it in Haskell:

  • Generating Constrained Data with Uniform Distribution, by Claessen et al., FLOPS'14 (PDF). I believe the Haskell package lazy-search has most of the machinery described by the paper, but it seems aimed at enumeration rather than random generation.

  • Making Random Judgments: Automatically Generating Well-Typed Terms from the Definition of a Type-System, by Fetscher et al., ESOP'15 (PDF), the title says it all. I don't know about a Haskell implementation though; you might want to ask the authors.

  • Beginner's Luck: A Language for Property-Based Generators, by Lampropoulos et al., POPL'17 (PDF) (disclaimer: I'm a coauthor). A language of properties (more concretely, functions T -> Bool, e.g., a typechecker) that can be interpreted as random generators (Gen T). The language's syntax is strongly inspired by Haskell, but there are still a few differences. The implementation has an interface to extract the generated values in Haskell (github repo).

  • Generating Good Generators for Inductive Relations, by Lampropoulos et al. POPL'18 (PDF). It's in Coq QuickChick, but tying it to Haskell QuickCheck by extraction seems reasonably feasible.

user_68637490
Related