2

当我们使用 QuickCheck 检查我们的程序时，我们需要为我们的数据定义生成器，有一些通用的方式来定义它们，但是当我们需要生成的数据满足某些约束才能工作时，通用的方式通常变得无用。

例如

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

现在我需要定义 Expr 的生成器（即Gen Expr或instance Arbitrary Expr），但也希望它生成正确的类型（即isJust (typeInfer generatedExpr)）

一种天真的方法是使用suchThat过滤掉无效的方法，但这显然是低效的，Expr并且TyRep在更多情况下变得复杂。

另一个类似的情况是关于参考完整性，例如

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

在这种情况下，我们希望生成的所有引用名称Expr都包含在某些特定的名称中Context，现在我必须Expr为特定的名称生成Context：

arbExpr :: Context -> Gen Expr

但是现在shrink会成为一个问题，而要解决这个问题，我必须定义一个特定版本的shrink，并且forAllShrink每次使用时都要使用arbExpr，这意味着很多工作。

所以我想知道，有没有做这些事情的最佳实践？

4

1 回答 1

2

对于类型良好的术语，在许多情况下，一种简单的方法是为每种类型使用一个生成器，或者等效地，使用一个函数TyRep -> Gen Expr。在此之上添加变量，这通常会变成一个函数Context -> TyRep -> Gen Expr。

在使用变量（并且没有或非常简单的类型）生成术语的情况下，通过上下文索引术语的类型（例如，就像您使用bound库所做的那样）应该可以很容易地生成通用的生成器。

对于收缩，hedgehog的方法可以很好地工作，它Gen与收缩版本一起生成一个值，使您无需定义单独的收缩函数。

请注意，随着格式正确/键入关系变得更加复杂，您开始碰到理论墙，生成术语至少与任意证明搜索一样难。

对于更先进的技术/相关文献，我自己对可能在 Haskell 中使用它的评论：

  • 生成具有均匀分布的约束数据，Claessen 等人，FLOPS'14 ( PDF )。我相信 Haskell 包惰性搜索具有论文中描述的大部分机制，但它似乎旨在枚举而不是随机生成。

  • 做出随机判断：从类型系统的定义中自动生成类型良好的术语，作者 Fetscher 等人，ESOP'15 ( PDF )，标题说明了一切。不过，我不知道 Haskell 的实现；你可能想问作者。

  • Beginner's Luck: A Language for Property-Based Generators，Lampropoulos 等人，POPL'17 ( PDF )（免责声明：我是合著者）。T -> Bool一种可以解释为随机生成器 ( )的属性语言（更具体地说，是函数，例如类型检查器Gen T）。该语言的语法受到 Haskell 的强烈启发，但仍有一些差异。该实现有一个接口来提取 Haskell ( github repo ) 中生成的值。

  • 为归纳关系生成良好的生成器，Lampropoulos 等人。POPL'18（PDF）。它在 Coq QuickChick 中，但通过提取将其绑定到 Haskell QuickCheck 似乎相当可行。

于 2019-01-10T07:31:46.883 回答