为什么这个收缩树看起来像使用过滤器时的样子

Question

我试图了解过滤器在使用hedgehog时对生成器的收缩树有什么影响集成收缩。

考虑以下函数：

{-# LANGUAGE OverloadedStrings #-}

import Hedgehog
import qualified Hedgehog.Gen as Gen

aFilteredchar:: Gen Char
aFilteredchar =
  Gen.filter (`elem` ("x" :: String)) (Gen.element "yx")

当打印收缩树时：

>>>  Gen.printTree aFilteredchar

我会得到如下所示的收缩树：

'x'
 └╼'x'
    └╼'x'
       └╼'x'
               ...

                   └╼<discard>

这是一个非常深的树，只包含x，最后是discard。

为什么收缩函数不断返回x，而不是一个空列表，这表明不可能进一步收缩？

Answer 1

Gen本质上是一个概率monad和一个tree monad的组合，你观察到的行为大多来自于tree monad和Gen.filter的定义。

基本上，Gen.filter p g 是一个简单的一元循环，try 0 其中：

-- simplified body of filter
try k =
  if k > 100 then
    discard  -- empty tree
  else do
    x <- g
    if p x then
      pure x  -- singleton tree
    else
      try (k + 1)  -- keep looping

所以要理解你得到的树，你必须在这里理解 do 符号下的 tree monad。

树单子

Gen 内部使用的Tree type in hedgehog 大致是这样的（如果您正在查看hedgehog 中的链接实现，请设置m ~ Maybe）：

data Tree a = Empty | Node a [Tree a]  -- node label and children

还有许多其他类似Tree 的类型是单子，单子绑定(>>=) 通常采用树替换的形式。

假设你有一棵树t = Node x [t1, t2, ...] :: Tree a，还有一个延续/替换k :: a -> Tree b，它将每个节点/变量x :: a替换为树k x :: Tree b。我们可以分两步描述t >>= k，fmap 然后join，如下所示。首先fmap 在每个节点标签上应用替换。所以我们得到一棵树，其中每个节点都被另一棵树标记。具体来说，说k x = Node y [u1, u2, ...]：

fmap k t
=
Node
  (k x)                        -- node label
  [fmap k t1, fmap k t2, ...]  -- node children
=
Node
  (Node y [u1, u2, ...])       -- node label
  [fmap k t1, fmap k t2, ...]  -- node children

然后join 步骤将嵌套树结构展平，将标签内部的子级与外部的子级连接起来：

t >>= k
=
join (fmap k t)
=
Node
  y
  ([join (fmap k t1), join (fmap k t2), ...] ++ [u1, u2, ...])

要完成Monad 实例，请注意我们有pure x = Node x []。

try 循环

现在我们对 tree monad 有了一些直觉，我们可以求助于您的特定生成器。我们要评估上面的try k，其中p = (== 'x') 和g = elements "yx"。我在这里挥手致意，但您应该想象g 随机评估为树Node 'y' []（生成'y'，没有收缩），又名。 pure 'y'，或Node 'x' [Node 'y' []]（生成'x'并缩小为'y'；实际上，“elements向左缩小”），并且g的每一次出现都是独立于其他的，所以我们得到一个重试时结果不同。

让我们分别检查每个案例。如果g = pure 'y' 会发生什么？假设k <= 100，所以我们在顶级if 的else 分支中，下面已经简化了：

-- simplified body of filter
try k = do
    c <- pure 'y'     -- g = pure 'y'
    if c == 'x' then  -- p c = (c == 'x')
      pure c
    else
      try (k + 1)

-- since   (do c <- pure 'y' ; s c) = s 'y'  (monad law)   and   ('y' == 'x') = False

try k = try (k + 1)

因此，g 评估为 pure 'y' 的所有时间最终都被简化为递归项 try (k + 1)，而我们只剩下 g 评估为另一棵树 Node 'x' [Node 'y' []] 的情况：

try k = do
  c <- Node 'x' [Node 'y' []]  -- g
  if c == 'x' then
    pure c
  else
    try (k + 1)

如上一节所述，monadic bind 等价于以下内容，我们以一些等式推理结束。

try k = join (Node (s 'x') [Node (s 'y') []])
  where
    s c = if c == 'x' then pure c else try (k + 1)

try k = join (Node (pure 'x') [Node (try (k + 1)) []])
try k = join (Node (pure 'x') [pure (try (k + 1))]  -- simplifying join
try k = Node 'x' [join (pure (try (k + 1)))]        -- join . pure = id
try k = Node 'x' [try (k + 1)]

综上所述，从try 0开始，有一半概率try k = try (k + 1)，另一半概率try k = Node 'x' [try (k + 1)]，最后我们停在try 100。这解释了您观察到的树。

try 0 = Node 'x' [Node 'x' [ ... ]]  -- about 50 nodes

---

（我相信这至少也为your other question 提供了部分答案，因为这表明缩小Gen.filter 通常相当于从头开始重新运行生成器。）

Answer 2

虽然Li-yao Xia 的详细回答正确地描述了如何发生这种情况，但它没有解决为什么； 为什么每次收缩后它都会重新运行生成器？答案是不应该；这是一个错误。请参阅 GitHub 上的错误报告 Improve Filter。