为什么这个缩小树看起来就像使用过滤器时那样

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和树monad的组合，你观察到的行为主要来自树monad和Gen.filter的定义。

基本上，Gen.filter p g是一个简单的monadic循环，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表示法理解树monad。

The tree monad

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

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

还有许多其他类似Tree的类型是monad，而monadic bind (>>=)通常采用树替换的形式。

假设你有一棵树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 []。

The try loop

现在我们对树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所以我们在顶部else的if分支，已经简化了下面：

-- 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绑定等同于以下内容，我们以一些等式推理完成。

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。