Is there a "there exists" quantifier in QuickCheck?

Question

There is the forAll quantifier that returns a property which checks if all test cases pass. Is there a way to define a "there exists" quantifier that returns a property which checks it at least one test case passes?

Interdenominational

Problem is that the library usually generates random values. So it is possible it will take ages before you find a value that satisfies the condition. Furthermore if the test itself is not true. It will never end generating values. – Noaccount

Yes, but it can still be useful if you're confident that there are many test cases that satisfy the condition. I'm looking for a property that will stop generating values as soon as the condition is satisfied once. – Emmerie

That would allow us to write, for example, propositions like "There exists an n such that the property is true for all m > n". – Emmerie

But say you have a property: length a < 0. So the length should be less than 0. It is clear it will never be satisfied. So the tests will get stuck into an infinite loop where they will keep generating lists in the hope one of them will have a lenght less than 0. Now you cannot make a distinction between: "not satisfied because the condition is rare", or "unsatisifiable". – Noaccount

Why not stop generating cases after 100 tries like with forAll? The same argument could be used against forAll anyway: you cannot make a distinction between "satisfied because the counter example is rare" and "true". – Emmerie

yeah but the outcome is different: if a counterexample is rare: the program will report "satisfied", whereas if an example in an exists is rare, it will report "false". QuickCheck is optimistic: there is no guarantee - as with all unit tests - that a program is correct if the tests are satisifed. It however makes you more certain. – Noaccount

I don't get it. I need a "there exists" quantifier that generates tests until one passes and reports "satisfied" or "false/not satisfied" if a max number of tests are reached. I know that quickCheck can't work well with rare examples or counter examples, but it's useful anyway. I don't really understand if you're telling me "it's impossible with quickCheck as it is". Is this so? Or are you arguing about whether it's a good thing to do? – Emmerie

Answer 1

Testing existence by enumeration would be more reliable: SmallCheck, LeanCheck, FEAT.

If you must use random generation there are some indirect ways in QuickCheck.

---

expectFailure seems like a good candidate for negation. However it isn't quite it, as it isn't involutive so you must negate the property in other ways, like not, if your property is in fact boolean.

exists :: Gen a -> (a -> Bool) -> Property
exists gen prop = once $ expectFailure (forAll gen (not . prop))

This counts crashing as a failure though, which thus makes the test pass even though you might not expect it.

---

Existential quantification is kind of a disjunction, and QuickCheck has disjoin. Just make a huge enough disjunction.

exists :: Gen a -> (a -> Property) -> Property
exists gen prop = once $ disjoin $ replicate 10000 $ forAll gen prop

But you get spammed with counterexamples when no good example is found. Maybe it is better to rewrite the logic of forAll yourself to avoid the call to counterexample.

---

More simply you can always write your own property as a generator to get the proper quantification.

exists :: Gen a -> (a -> Bool) -> Property
exists gen prop = property (exists' 1000 gen prop)

exists' :: Int -> Gen a -> (a -> Bool) -> Gen Bool
exists' 0 _ _ = return False
exists' n gen prop = do
  a <- gen
  if prop a
    then return True
    else exists' (n - 1) gen prop

Doing this manually also has the property that if prop unexpectedly crashes, it is immediately reported as a failure, as opposed to the previous methods.

---

EDIT

So if you only have a (a -> Property) instead of (a -> Bool) it seems much trickier to achieve a good result, because it's non-trivial to check whether a property succeeded. A proper way would be to mess with the internals of QuickCheck, probably something similar to disjoin. Here is a quick hack

• Use mapResult to silence the output of disjoin when no (counter)example was found.

• Override the size parameter because if your witnesses are non-trivial, they will not be found if the size is too small or too large.

import Test.QuickCheck
import Test.QuickCheck.Property as P

-- Retry n times.
exists :: Testable prop => Int -> Gen a -> (a -> prop) -> Property
exists n gen prop =
  mapResult (\r -> r {P.reason = "No witness found.", P.callbacks = []}) $
  once $
  disjoin $
  replicate n $ do
    a <- gen
    return (prop a)

main = quickCheck $ exists 100
  (resize 5 arbitrary)
  (\x -> (x :: Integer) == 2)

Metacenter

Your third suggestion is close to what I'm looking for. But in order to combine it with forAll, for example to write exists gen1 $ \a -> forAll gen2 ..., exists would have to have signature (Testable prop) => Gen a -> (a -> prop) -> Property. I've trouble finding out how to do this reading QuickCheck's source code. Would you know how to do it? – Emmerie

I guess my example relies a lot on the property being simply boolean. If you have an abstract prop you can use .||. or disjoin, which ends up resembling what I suggested in the second example about not calling counterexample. – Metacenter

once $ disjoin $ replicate 10000 $ do { a <- gen ; return (prop a) }But as I said, it silences exceptions. It turns out you can use mapResult as suggested by Alexey Romanov to check for exceptions raised at the end of disjoin. – Metacenter

Your last suggestion seems to work but takes a long time and fills the console with empty lines. I've spent days on it but I still can't figure out how to do this properly. Could you rewrite your 3rd suggestion in your post so that it works with a Testable prop instead of a Bool? The whole problem I can't solve is how to check if prop a is a success of a failure. – Emmerie

I appended something that seems to work, still with disjoin. Unfortunately I couldn't figure out a good way based on a pure generator (mainly because I'm not familiar enough with the internals of Property). Somehow once doesn't have the effect I expected. Sorry if that answer is still unsatisfactory. – Metacenter

Answer 2

I don't know if something like this exist in QuickCheck. Also not convinced it would be helpful, but that's another matter. Since we have:

∃ x . P x <=> ¬ ¬ ∃ x . P x <=> ¬ ∀ x . ¬ P x

I suppose you could set it up so your test-case tests the negation and if it fails it means you have your existential. HTH.

Microgamete

I've thought about that, but how do you take the negation of forAll ... in quickCheck? I've already tried not (forAll gen prop) but forAll returns a Property ant not expects a Bool. – Emmerie

@GuillaumeChérel You should be able to implement it using mapResult: hackage.haskell.org/package/QuickCheck-2.9.2/docs/src/…. – Duenna