代码之家 › 专栏 › 技术社区 › Damian Nadales

为什么此收缩树的外观与使用过滤器时的外观相同

haskell-hedgehog property-based-testing quickcheck haskell

1

Damian Nadales · 技术社区 · 6 年前

我试图了解过滤器在使用时对生成器的收缩树有什么影响 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

1 回复 | 直到 6 年前

1

2

Li-yao Xia 6 年前

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 type in hedgehog 由内部使用的 消息 大致如下所示(如果您正在查看hedgehog中的链接实现,请设置 m ~ Maybe ):

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

还有很多其他的 树 -像是单子的类型,和单子绑定 (>>=) 通常采用树替换的形式。

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

然后 参加 步骤展平嵌套树结构,将标签内部的子项与外部的子项连接起来:

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

Monad 例如,请注意,我们有 pure x = Node x [] .

现在我们对树单子有了一些直觉,我们可以转向您的特定生成器。我们要评估 try k 上面,哪里 p = (== 'x') 和 g = elements "yx" g 对树中的任意一个进行随机计算 Node 'y' [] 'y' 没有收缩),又名。 pure 'y' 或 Node 'x' [Node 'y' []] (产生 'x' 退缩到 ; 的确,” 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 纯“y” 最终简化为递归项 try (k + 1) 节点“x”[节点“y”[] :

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

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)]

总之,从 尝试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 ,因为这显示了 发电机过滤器 通常相当于从头开始重新运行生成器。)

2

1

edsko 6 年前

虽然 Li-yao Xia 的详细回答正确地描述了如果发生这种情况,它不会解决问题 为什么? ; 为什么? 每次收缩后是否重新运行发电机?答案是不应该;这是一个错误。请参阅错误报告 Improve Filter 在GitHub上。