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

I think it was due to technical constraints, because currently to evaluate a Testable with the Test.QuickCheck library, you need to use one of the 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 which proves the property false. If such input is not found, the property is assumed to be true (although that is not necessarily the truth; there may be a counterexample that was not tested). And to be able to generate random inputs in Haskell, we are stuck to the IO monad.

Notice that even though assert was defined in such a generic way, it is used through all the paper only with Bool. So the library author (the same of the paper) preferred to sacrifice the generic Testable parameter for a simple Bool, to not force any monad at this point.

And we can see that they have even written the original signature as a comment in the source code:

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

Also note that despite the fact that stop function has a similar signature:

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

It is not the same as the assert function in the paper, as the former will stop the computation in both cases either the condition is True or False. On the other hand, assert will only stop the computation if the condition is False:

⟦ assert True ≫ p ⟧ = ⟦ p ⟧

⟦ assert False ≫ p ⟧ = { return False }

We can though easily write a IO version of the assert function from the paper:

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"

And now we can make a test to see the differences between assertIO and 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

The succeeded and failed could be replaced by True and False, respectively. It was just to show that now we are not limited to Bool, instead we can use any Testable.

And the output is:

prop_assert:
*** Failed! Assertion failed (after 1 test):
prop_stop:
+++ OK, passed 100 tests.

As we can see, despite the fact that the first assertIO succeeded, prop_assert failed due to the second assertIO. On the other hand, prop_stop passed the test, because the first stop succeeded and the computation has stopped at that point, not testing the second stop.

Recommended topics

Hot tags