2

我试图了解 filter 在使用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's，discard最后是 a。

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

4

2 回答 2

2

Gen本质上是概率单子和树单子的组合，您观察到的行为主要来自于树单子和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类型Gen大致如下所示（如果您正在查看刺猬中的链接实现，请设置m ~ Maybe）：

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

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

假设您有一个 treet = Node x [t1, t2, ...] :: Tree a和一个 continuation/substitution k :: a -> Tree b，它将每个节点/变量x :: a替换为 tree k x :: Tree b。那么，我们可以t >>= k分两步来描述，如下。首先，在每个节点标签上应用替换。所以我们得到一棵树，其中每个节点都被另一棵树标记。具体来说，说：fmapjoinfmapk 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 [].

尝试循环

现在我们对 tree monad 有了一些直觉，我们可以转向您的特定生成器。我们要评估try k上面的 wherep = (== 'x')和g = elements "yx"。我在这里挥手致意，但你应该想象这会g随机评估任何一棵树Node 'y' []（生成'y'时没有收缩），也就是。pure 'y', or Node 'x' [Node 'y' []](generate 'x'and shrink to 'y'; 实际上, "elements向左收缩"), 并且每次出现g都是独立于其他的，所以当我们重试时会得到不同的结果。

让我们分别检查每个案例。如果 会发生什么g = pure 'y'？假设k <= 100我们在elsetoplevel 的分支中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 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

（我相信这也至少为您的其他问题提供了部分答案，因为这表明缩小 aGen.filter通常等于从头开始重新运行生成器。）

于 2019-01-29T03:06:57.067 回答
1

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

于 2019-04-29T06:32:18.673 回答