QuickCheck 放弃研究递归数据结构（玫瑰树）。

Question

给定一棵任意树，我可以使用舒伯特编号在该树上构造子类型关系：

constructH :: Tree a -> Tree (Type a)

Type 嵌套了原始标签，另外还提供了执行子/父（或子类型）检查所需的数据。使用舒伯特编号，两个 Int 参数就足够了。

data Type a where !Int -> !Int -> a -> Type a

这导致二元谓词

subtypeOf :: Type a -> Type a -> Bool

我现在想用 QuickCheck 进行测试，这确实符合我的要求。但是，以下属性不起作用，因为 QuickCheck 只是放弃了：

subtypeSanity ∷ Tree (Type ()) → Gen Prop
subtypeSanity Node { rootLabel = t, subForest = f } =
  let subtypes = concatMap flatten f
  in (not $ null subtypes) ==> conjoin
     (forAll (elements subtypes) (\x → x `subtypeOf` t):(map subtypeSanity f))

如果我省略了对subtypeSanity 的递归调用，即我传递给conjoin 的列表的尾部，则该属性运行良好，但只测试树的根节点！如何在 QuickCheck 不放弃生成新测试用例的情况下递归地进入我的数据结构？

如果需要，我可以提供代码来构建舒伯特层次结构，以及 Tree (Type a) 的 Arbitrary 实例，以提供完整的可运行示例，但这将是相当多的代码。我确信我只是没有“获得” QuickCheck，并且在这里以错误的方式使用它。

编辑：不幸的是，sized 函数似乎并没有消除这里的问题。它最终得到相同的结果（请参阅对 J. Abrahamson 的回答的评论。）

编辑二：我最终通过避免递归步骤和避免conjoin来“解决”我的问题。我们只需列出树中所有节点的列表，然后在这些节点上测试单节点属性（从一开始就可以正常工作）。

allNodes ∷ Tree a → [Tree a]
allNodes n@(Node { subForest = f }) = n:(concatMap allNodes f)

subtypeSanity ∷ Tree (Type ()) → Gen Prop
subtypeSanity tree = forAll (elements $ allNodes tree)
  (\(Node { rootLabel = t, subForest = f }) →
    let subtypes = concatMap flatten f
    in (not $ null subtypes) ==> forAll (elements subtypes) (\x → x `subtypeOf` t))

调整树的 Arbitrary 实例不起作用。这是我仍在使用的任意实例：

instance (Arbitrary a, Eq a) ⇒ Arbitrary (Tree (Type a)) where
  arbitrary = liftM (constructH) $ sized arbTree

arbTree ∷ Arbitrary a ⇒ Int → Gen (Tree a)
arbTree n = do
  m ← choose (0,n)
  if m == 0
    then Node <$> arbitrary <*> (return [])
    else do part ← randomPartition n m
            Node <$> arbitrary <*> mapM arbTree part

-- this is a crude way to find a sufficiently random x1,..,xm,
-- such that x1 + .. + xm = n, for any n, m, with 0 < m.
randomPartition ∷ Int → Int → Gen [Int]
randomPartition n m' = do
  let m = m' - 1
  seed ← liftM ((++[n]) . sort) $ replicateM m (choose (0,n))
  return $ zipWith (-) seed (0:seed)

我认为这个问题“现在已经解决了”，但如果有人可以向我解释为什么递归步骤和/或 conjoin 让 QuickCheck 放弃（在通过“仅”0 次测试后），我将不胜感激.

Answer 1

在生成Arbitrary 递归结构时，QuickCheck 通常有点过于急切，会生成庞大的随机示例。这些是不可取的，因为它们通常不能更好地检查感兴趣的属性并且可能非常慢。两种解决方案是

1. 使用 size 参数（sized 函数）和 frequency 函数将生成器偏向小树。

2. 使用像smallcheck 中的小型面向生成器。这些尝试详尽地生成所有“小”示例，从而有助于减小树的大小。

为了阐明sized和frequency控制生成大小的方法，这里有一个例子RoseTree

data Rose a = It a | Rose [Rose a]

instance Arbitrary a => Arbitrary (Rose a) where
  arbitrary = frequency 
    [ (3, It <$> arbitrary)                   -- The 3-to-1 ratio is chosen, ah,
                                              -- arbitrarily...
                                              -- you'll want to tune it
    , (1, Rose <$> children)
    ]
    where children = sized $ \n -> vectorOf n arbitrary

通过非常小心地控制子列表的大小，可以更简单地使用不同的Rose 格式来完成

data Rose a = Rose a [Rose a]

instance Arbitrary a => Arbitrary (Rose a) where
  arbitrary = Rose <$> arbitrary <*> sized (\n -> vectorOf (tuneUp n) arbitrary)
    where tuneUp n = round $ fromIntegral n / 4.0

您可以在不引用 sized 的情况下执行此操作，但这会为您的 Arbitrary 实例的用户提供一个旋钮，以便在需要时请求更大的树。

Answer 2

如果它对遇到此问题的人有用：当 QuickCheck “放弃”时，这表明您的先决条件（使用 ==>）太难以满足。

QuickCheck 使用简单的拒绝抽样技术：前置条件对值的生成没有影响。 QuickCheck 会像正常一样生成一堆随机值。 这些生成后，通过前置条件发送：如果结果为True，则使用该值测试属性；如果是False，则丢弃该值。如果您的先决条件拒绝了 QuickCheck 生成的大部分值，那么 QuickCheck 将“放弃”（最好完全放弃，而不是提出统计上可疑的通过/失败声明）。

特别是，QuickCheck 将不会尝试生成满足给定前提条件的值。确保您使用的生成器（arbitrary 或其他方式）产生大量通过您的前提条件的值由您决定。

让我们看看这在您的示例中是如何体现的：

subtypeSanity :: Tree (Type ()) -> Gen Prop
subtypeSanity Node { rootLabel = t, subForest = f } =
  let subtypes = concatMap flatten f
  in (not $ null subtypes) ==> conjoin
     (forAll (elements subtypes) (`subtypeOf` t):(map subtypeSanity f))

==> 只出现一次，所以它的前提条件（not $ null subtypes）一定很难满足。这是由于递归调用map subtypeSanity f：您不仅拒绝任何Tree，其中subForest 为空，您也（由于递归）拒绝任何Tree其中subForest 包含Trees 和空subForests，和拒绝任何Tree 其中subForest 包含Trees 和subForests 包含Trees subForests 为空，以此类推。

根据您的 arbitrary 实例，Trees 仅嵌套到有限深度：最终我们将始终到达一个空的 subForest，因此您的递归前置条件将始终失败，并且 QuickCheck 将放弃。