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

Question

在Testing Monadic Code with QuickCheck (Claessen, Hughes 2002) 中，assert 的类型为：

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

但是，在Test.QuickCheck.Monadic 中，它的类型为：

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

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

Answer 1

我认为这是由于技术限制，因为目前要使用Test.QuickCheck 库评估Testable，您需要使用quickCheck* 函数之一，它非常以IO 为中心。发生这种情况是因为 QuickCheck 通过随机生成可能的输入（默认为 100）来测试 Testable 属性，试图找到证明属性为假的 counterexample。如果未找到此类输入，则假定该属性为真（尽管这不一定是事实；可能存在未测试的反例）。为了能够在 Haskell 中生成随机输入，我们坚持使用 IO monad。

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

而且我们可以看到他们甚至在source code中写了原始签名作为评论：

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

还要注意，尽管stop 函数具有相似的签名：

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

它不与本文中的assert 函数相同，因为前者将在两种情况下停止计算，条件是True 或False。另一方面，assert 只会在条件为False 时停止计算：

⟦ 断言 True ≫ p ⟧ = ⟦ p ⟧

⟦ 断言 False ≫ p ⟧ = { 返回 False }

我们可以很容易地从论文中编写IO 版本的assert 函数：

import Control.Monad
import Control.Monad.Trans
import Test.QuickCheck
import Test.QuickCheck.Monadic
import Test.QuickCheck.Property
import Test.QuickCheck.Test

assertIO :: Testable prop => prop -> PropertyM IO ()
assertIO p = do r <- liftIO $ quickCheckWithResult stdArgs{chatty = False} p
                unless (isSuccess r) $ fail "Assertion failed"

现在我们可以做一个测试，看看assertIO和stop之间的区别：

prop_assert :: Property
prop_assert = monadicIO $ do assertIO succeeded
                             assertIO failed

prop_stop :: Property
prop_stop = monadicIO $ do stop succeeded
                           stop failed

main :: IO ()
main = do putStrLn "prop_assert:"
          quickCheck prop_assert
          putStrLn "prop_stop:"
          quickCheck prop_stop

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

输出是：

prop_assert:
*** 失败的！断言失败（经过 1 次测试）：
道具停止：
+++ 好的，通过了 100 次测试。

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