Test.QuickCheck.Monadic:为什么断言应用于Bool,而不是Testable a => a

Question

在使用QuickCheck测试Monadic代码时(Claessen,Hughes 2002),assert有类型:

assert :: (Monad m, Testable a) => a -> PropertyM m ()

但是,在Test.QuickCheck.Monadic,它有类型:

assert :: (Monad m) => Bool -> PropertyM m ()

为什么assert在库中有后一种类型？

Answer 1

我认为这是由于技术限制，因为目前要评估Testable库Test.QuickCheck，您需要使用其中一个quickCheck*功能，这些功能非常以 为IO中心。发生这种情况是因为 QuickCheckTestable通过随机生成可能的输入（默认为 100）来测试属性，试图找到证明属性错误的反例。如果找不到这样的输入，则假定该属性为真（尽管这不一定是真的；可能存在未经测试的反例）。为了能够在 Haskell 中生成随机输入，我们必须使用 monad IO。

\n\n

请注意，即使是以assert这种通用方式定义的，它在整篇论文中仅与 一起使用Bool。因此，库作者（与论文相同）更愿意牺牲通用Testable参数来获得简单的Bool，此时不强制任何 monad 。

\n\n

我们可以看到他们甚至在源代码中将原始签名写为注释：

\n\n

-- assert :: Testable prop => prop -> PropertyM m ()\n

\n\n

另请注意，尽管该stop函数具有相似的签名：

\n\n

stop :: (Testable prop, Monad m) => prop -> PropertyM m a\n

\n\n

它与论文中的函数不同，因为前者在条件为或 的两种情况下都会停止计算。另一方面，只有在满足以下条件时才会停止计算：assertTrueFalseassertFalse

\n\n

\n

\xe2\x9f\xa6 断言 True \xe2\x89\xab p \xe2\x9f\xa7 = \xe2\x9f\xa6 p \xe2\x9f\xa7

\n\n

\xe2\x9f\xa6 断言 False \xe2\x89\xab p \xe2\x9f\xa7 = { 返回 False }

\n

\n\n

我们可以轻松地从论文中编写IO该函数的一个版本：assert

\n\n

import Control.Monad\nimport Control.Monad.Trans\nimport Test.QuickCheck\nimport Test.QuickCheck.Monadic\nimport Test.QuickCheck.Property\nimport Test.QuickCheck.Test\n\nassertIO :: Testable prop => prop -> PropertyM IO ()\nassertIO p = do r <- liftIO $ quickCheckWithResult stdArgs{chatty = False} p\n                unless (isSuccess r) $ fail "Assertion failed"\n

\n\n

现在我们可以做一个测试来看看assertIO和之间的差异stop：

\n\n

prop_assert :: Property\nprop_assert = monadicIO $ do assertIO succeeded\n                             assertIO failed\n\nprop_stop :: Property\nprop_stop = monadicIO $ do stop succeeded\n                           stop failed\n\nmain :: IO ()\nmain = do putStrLn "prop_assert:"\n          quickCheck prop_assert\n          putStrLn "prop_stop:"\n          quickCheck prop_stop\n

\n\n

和可以分别替换为succeeded和。这只是为了表明现在我们不限于，而是我们可以使用任何。failedTrueFalseBoolTestable

\n\n

输出是：

\n\n

\n

prop_assert:
\n *** 失败！断言失败（1 次测试后）：
\n prop_stop：
\n +++ 好的，通过了 100 次测试。

\n

\n\n

正如我们所看到的，尽管第一个assertIO成功了，但prop_assert由于第二个而失败了assertIO。另一方面，prop_stop通过了测试，因为第一个stop成功并且计算已在此时停止，而不是测试第二个stop。

\n