Test.QuickCheck.Monadic: 为什么assert应用于Bool, not 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* functions, which are very IO-centric. That happens because QuickCheck tests Testable properties by randomly generating possible inputs (by default 100), trying to find a 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:

时停止计算

⟦ assert True ≫ p ⟧ = ⟦ p ⟧

⟦ assert False ≫ p ⟧ = { return 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:
*** Failed! Assertion failed (after 1 test):
prop_stop:
+++ OK, passed 100 tests.

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

Test.QuickCheck.Monadic: 为什么assert应用于Bool, not Testable a => a

Test.QuickCheck.Monadic: why is assert applied to Bool, not Testable a => a

haskell

quickcheck