haskell - Test.QuickCheck.Monadic : why is assert applied to Bool, 不可测试 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

我认为这是由于技术限制，因为目前要评估 Testable与 Test.QuickCheck库，您需要使用 quickCheck* 之一函数，非常IO -中心。这是因为 QuickCheck 测试了 Testable属性通过随机生成可能的输入(默认为 100)，试图找到 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 .