Announcing SmallCheck 1.0

I am glad to announce a new major release of SmallCheck (hackage).

What is SmallCheck?

SmallCheck is a property-based testing library for Haskell.

If you are familiar with QuickCheck, you can think of SmallCheck as a better QuickCheck. The main way in which it is better is that it is non-random: whether your tests pass does not depend on the roll of the dice.

If you are not familiar with QuickCheck, the idea of SmallCheck is to check certain properties of your functions, as opposed to unit testing, where you just check the expected outcome of some particular tests.

For an introduction to property-based testing, check out Chapter 11 of Real World Haskell. It should be straightforward to translate all the examples there to SmallCheck.

What’s new in 1.0

Monadic properties

Properties are now parameterised on the monad they work in.

The two main ways a property can use the monad are:

1. generating test cases monadically
2. verifying the condition monadically

Monadic test cases generation can be used to read test cases from files. A well-known problem when testing compilers is that it is hard to enumerate or randomly generate valid programs. So here you go — just put some examples in the file system, and use them to verify some properties of your compiler.

An example of monadic verification is when you want to verify your code against an external (or otherwise impure) reference implementation.

Quantifiers

The semantics of quantifiers has changed. Previously, all variables were quantified universally by default, and a quantifier (like exists) changed the quantification of the next variable.

So, for example, exists $ \x y -> p x y was interpreted as \(\exists x: \forall y. p\ x\ y\), which is probably not what one would expect.

Now the quantification operators (forAll, exists and existsUnique) set the quantification context for all subsequent variables, so the above property means \(\exists x, y: p\ x\ y\).

Uniqueness quantification

There’s an interesting effect related to the uniqueness quantifier existsUnique (which was previously called exists1).

There are two ways to interpret existsUnique $ \x y -> p x y, “curried” and “uncurried”:

• \(\exists ! x: \exists ! y: p\ x\ y\)
• \(\exists ! (x,y): p\ x\ y\)

These two actually have different meaning. Suppose that \(p\ x\ y=(|x|=|y|)\), where \(|x|\) denotes the absolute value of an integer \(x\). Then the first property above is true, and the second is false (be sure to check this yourself).

When mathematicians write \(\exists ! x,y:p\ x\ y\), they really mean the second interpretation, so this is what SmallCheck implements (although the first interpretation would be much easier to implement).

Higher-order properties

Both SmallCheck and QuickCheck have a ==> operator, which tests an implication. The left argument of ==> has type Bool, and it’s usually a statement that the generated arguments satisfy some side condition (e.g. generated programs are valid).

In this new version of SmallCheck, the left argument of ==> can be an arbitrary property, with its own quantifiers etc. Here’s how we could test an isPrime function:

import Test.SmallCheck
import Test.SmallCheck.Series

isPrime :: Integer -> Bool
isPrime _ = True

main = 
  smallCheck 5 {- 5 is the testing depth -} $
    \(Positive n) ->
      (exists $ \(Positive d) -> d /= 1 && d /= n && n `mod` d == 0) ==> not (isPrime n)

Unsurprisingly, the result will be

Failed test no. 4.
there exists 4 such that
  condition is false

Ordered testing

SmallCheck has just got more efficient and less annoying!

Previously, if you wanted to get the minimal counterexample, you used the function smallCheck which tested the property first with depth 0, then with depth 1 and so on — up to the limit that you told it.

The reason was that the Serial instance of e.g. Integer generated the following integers for depth 3:

[-3,-2,-1,0,1,2,3]

They are tried in exactly this order, and, if all of them were counterexamples, the user would be presented with -3 as the first one.

Now the instances generate examples in the order of increasing depth, e.g.

[0,1,-1,2,-2,3,-3]

so there’s no need to try multiple depths.

Better reporting

The way SmallCheck reports its findings is now greatly improved, especially in some complex cases.

For example, consider the following property:

smallCheck 5 $ existsUnique $ \x -> (forAll $ \y -> x * y >= 0) ==> (forAll $ \y -> x * y == (0 :: Integer))

Here’s what SmallCheck 0.6.2 reports (or, to be precise, would report if it supported higher-order properties):

Depth 0:
  Completed 1 test(s) without failure.
Depth 1:
  Failed test no. 12. Test values follow.
  non-uniqueness
  -1
  0

And this is the output of SmallCheck 1.0:

Failed test no. 12.
there are at least two arguments satisfying the property:
  for 0
    condition is true
  for 1
    property is vacuously true because
      there exists -1 such that
        condition is false

Required type annotations

Because the Testable class is now multi-parameter (parameterised on the type and the monad), ambiguous types that involve this class do not get defaulted. To put it simply, most non-trivial properties now require some type annotations.

This turned out to be a very good thing for SmallCheck (which I couldn’t envision). Defaulting for properties often works in an unexpected way. For example, here’s what an older SmallCheck would tell you if you asked it whether all things are the equal:

> depthCheck 5 $ \x y -> x == y
Depth 5:
  Completed 1 test(s) without failure.

The result is unexpected, but at least we get some clue from the fact that there was just one test: the type of the variables got defaulted to ()!

Alas, QuickCheck doesn’t give us even this hint:

> quickCheck $ \x y -> x == y
+++ OK, passed 100 tests.

Luckily, with the new SmallCheck you actually get a type error:

<interactive>:10:26:
    No instance for (Eq a0) arising from a use of `=='
    The type variable `a0' is ambiguous
    Possible fix: add a type signature that fixes these type variable(s)

And indeed, the problem is easy to fix once you know it’s there:

> smallCheck 5 $ \x y -> x == (y :: Integer)
Failed test no. 2.
there exist 0 1 such that
  condition is false

Simpler interface

I took this chance to clean the API and make it more orthogonal.

Previously SmallCheck had functions like

forAllElem :: (Show a, Testable b) => [a] -> (a -> b) -> Property

which did three things at once:

• made the variable universally quantified
• converted the list to a depth-independent series
• quantified the variable over that series

No wonder the API suffered from the combinatorial explosion. Now these things are all done separately:

generate :: (Depth -> [a]) -> Series m a

can be used to turn a list into a series;

over :: (Monad m, Show a, Testable m b) => Series m a -> (a -> b) -> Property m

sets the domain of quantification; and

forAll :: Testable m a => a -> Property m

sets the quantification context.