Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

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

In Testing Monadic Code with QuickCheck (Claessen, Hughes 2002), assert has the type:

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

However, in Test.QuickCheck.Monadic, it has the type:

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

Why does assert have the latter type in the library?

like image 525
frasertweedale Avatar asked Jul 29 '15 13:07

frasertweedale


1 Answers

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.

like image 175
Helder Pereira Avatar answered Oct 21 '22 05:10

Helder Pereira