Published on February 19, 2013; tags: Haskell

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

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.

Properties are now parameterised on the monad they work in.

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

- generating test cases monadically
- 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.

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\).

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).

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
```

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.

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
```

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
```

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.