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

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是一个简单的一元循环，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此处的符号。

树单子(monad)

Tree type in hedgehog由 Gen 内部使用看起来大致像这样(如果您正在查看刺猬中的链接实现，请设置 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 [] .

尝试循环

现在我们对树单子(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)

如上一节所示，一元绑定(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 通常相当于从头开始重新运行生成器。)