we might get a counter-example such as this:

failed after 9 shrinks
(xs !! 0) /= (xs !! 1)
xs     : [0,1]
xs !! 0: 0
xs !! 1: 1

More interesting than the counter-example itself is how falsify arrived at that counter-example; if we look at the shrink history (--falsify-verbose), we see that the list shrunk as follows:

   [1,1,0,1,0,1]
~> [1,1,0]       -- shrink the list length
~> [0,1,0]       -- shrink an element of the list
~> [0,1]         -- shrink the list length again

That is, we apply f to specific input, and then verify that we get an expected result. By contrast, in property based testing, we do not specify a specific input, but instead generate a random input using some generator genInput, and then verify that the input and the output are related by some property prop:

Since the property is false, we will get a counter-example. Without shrinking, one such a counter-example might be

x = 38
y = 23

Given such an interface, we might define the type of generators as

Then we can shift our perspective: rather than thinking of generating random values from a PRNG we instead parse this stream of random samples:

Instead of having a separate shrinking function, we now simply shrink the list of samples, and then re-run the parser. This is the Hypothesis approach in a nutshell; parsers of course need to ensure that the produced value shrinks as the samples are shrunk. For example, here is a very simple (proof of concept) generator for Bool:

Assuming that the sample is chosen uniformly in the full Word range, this parser will choose uniformly between True and False; and as the sample is shrunk towards zero, the boolean will shrink towards False.

Streams versus trees

Like our definition above, this generator takes a PRNG as input, but it does not return an updated PRNG. This might seem confusing: suppose we are generating two numbers, as in our example above; how do we ensure those two numbers are generated from different PRNGs?

To solve this problem, we will need a PRNG that in addition to next, also provides a way to split the PRNG into two new PRNGs:

Then to run two generators, we first split the PRNG:

A generator is then a function that takes a part of a sample tree, parses it, and produces a value and an updated sample tree:

This does not reintroduce dependencies between generators: each generator will be run against a different subtree, and update only that subtree. For example, here is how we might run two generators:

Sample 1 in tree1 is less than the corresponding sample 2 in tree2, but sample 4 in tree1 is greater than the corresponding sample 3 in tree2. Hence, we have neither tree1 < tree2 nor tree2 < tree1: these two trees are incomparable. Instead, falsify works with a partial ordering; instead of the multitude of shrinking passes of Hypothesis, falsify has precisely one pass: shrink an individual sample in the tree.

Distributing samples to parsers

When we have a stream of values that we need to use for multiple parsers, we need to decide which samples go to which parser. In Hypothesis, this essentially happens on a first-come-first-served basis: any samples left unused by the first parser will be used by the next. As discussed, falsify parsers do not return “samples left unused”. Instead, the sample tree is split each time we compose parsers, like we did in both, shown above. In practice, this happens primarily when using applicative <*> or monadic >>=.

Predictability

These two differences are rather technical in nature; how do they affect users? Suppose we have a generator that produces a list and then a number:

If we are using a stream of samples, Hypothesis style, and then drop a random sample from that stream, the generator for int might suddenly be run against an entirely different sample; it might increase in value! Similarly, if we run that int generator against the first sample left over by the list generator, and if that list generator uses fewer samples as it shrinks, we might also run int against an unrelated sample, and its value might again increase.

This is not necessarily a problem; after all, we can then start to decrease that new int value again. However, that is only possible if the generated value with the larger int is still a counter-example to whatever property is being tested. If that is not the case, then we might not be able to shrink the list, and we might end up with a non-minimal counter-example. That can make debugging more difficult (we haven’t gotten rid of all the “junk”), and it can be difficult for users to understand why this might not shrink any further; even if the library offers facilities for showing why shrinking stopped (for example, showing which shrunk examples were rejected; verbose mode in falsify), it can still be quite puzzling why the library is trying to increase a value during shrinking.

Neither of these problems can arise in falsify: it never drops samples at all (instead, only shrinking individual samples), and since monadic bind splits the sample tree, we are guaranteed that the behaviour of int is entirely unaffected by the behaviour of list. This makes the shrinking behaviour in falsify more predictable and easier to understand.

Monadic bind

We cannot shrink the right hand side of (>>=) independent from the left hand side, because the right hand side is not a generator. We only have a generator once we apply the supplied function to the result of the first generator. This means that we cannot shrink these two generators independently: if, after shrinking the right hand side, we go back and then shrink the left hand side, we get an entirely different generator, and the shrinking we did previously is just wasted.

In practice what this means is that once we start shrinking the right hand side, we will never go back anymore and shrink the left hand side. In the example from the introduction we first generated a list length, and then the elements of the list:

With integrated shrinking, once we start shrinking elements from the list, we will never go back anymore and shrink the list length. With internal shrinking, however, we can go back and forth across monadic bind. This is the raison d’être of internal shrinking: it doesn’t matter that we cannot shrink the two generators independently, because we are not shrinking generators! Instead, we just shrink the samples that feed into those generators.

Selective functors

It is important to understand the limitations of internal shrinking: it is certaintly not a silver bullet. For example, consider this combinator that takes two generators, flips a coin (generates a boolean, shrinking towards True), and then executes one of the two generators:

While is is true that generation using this definition of choose will work just fine (and laziness ensures that we will in fact only run whatever generator is used), this combinator shrinks very poorly. The problem is that if we generate a value but they don’t use it, the (part of) the sample tree that we used to produce that value is irrelevant, and so by definition we can always replace it by the sample tree that is zero everywhere. This means that if we later want to switch to that generator, we will only be able to do so if the absolute minimum value that the generator can produce happens to work for whatever property we’re testing. This is an important lesson to remember:

Do not generate values and then discard them: such values will always shrink to their minimum. (Instead, don’t generate the value at all.)

The intuition is that we run the first generator; if that produces Left a, we run the second generator to get a b; if the first generator produces Right b, we skip the second generator completely. Like for applicative <*> and monadic (>>=), the two generators are run against different subtrees of the sample tree, but the critical difference is that we will not try to shrink the right subtree for the second generator unless that generator is used.

If that all sounds a bit abstract, perhaps suffices to say that any selective functor supports

which we can use to implement choose in a way that avoids reusing the sample tree of the first generator for the second:

Some observations:

If we run this test, we will get a counter-example:

multiply3_even: FAIL
  failed after 14 shrinks
  not even
  Logs for failed test run:
  generated 1 at CallStack (from HasCallStack):
    gen, called at demo/Demo/Blogpost.hs:217:10 in main:Demo.Blogpost

but in such a way that it can produce a meaningful message if the predicate is not satisfied. Here’s how we might use it for our example:

Some comments:

will produce a value between 10 and 100 (inclusive), shrinking towards 10; it is also possibly to flip the two bounds to shrink towards 100 instead.

will produce values between (0, 100), like between does, but skewed towards zero; a negative skew value will instead skew towards 100 (but still shrink towards zero). As an example use case, suppose that for a certain property we need a list of Int and an Int, and sometimes that separate Int should be a member of the list, sometimes not:

This property says that for any function f :: [Int] -> Bool, if we apply that function to the list [1, 2, 3] we must get the same result as when we apply it to the list [4, 5, 6]. Of course, that is not true, and when we run this test, falsify will give us a counter-example:

failed after 53 shrinks
(f x) /= (f y)
x  : [1,2,3]
y  : [4,5,6]
f x: True
f y: False

Logs for failed test run:
generated {[1,2,3]->True, _->False} at CallStack (from HasCallStack):
  gen, called at demo/Demo/Blogpost.hs:244:32 in main:Demo.Blogpost

Notice the counter-example we get: a function that returns True for the list [1, 2, 3], and False everywhere else. It truly is quite astonishing that this works: we can see that the list [1, 2, 3] is special by inspecting the source code, but of course falsify (or indeed, QuickCheck; this is not unique to falsify) cannot! Instead, falsify will generate a random infinitely large description of functions from [Int] -> Bool, that covers all possible input lists, and then start shrinking this description, throwing away values for inputs it doesn’t need, until a minimal test case remains. Truly a testament to the power of laziness in Haskell.

For a more realistic example, let’s port an example from Koen Claessen’s presentation to falsify. This example is testing the (wrong) property that for all functions f and predicates p,

map f . filter p == filter p . map f

In falsify, we might express this as:

We generate a random function f, a random predicate p, a random list xs, and then assert the property; and of course, falsify will happily give us a counter-example:

failed after 25 shrinks
(map f (filter p xs)) /= (filter p (map f xs))
xs                 : [96]
xs                 : [96]
filter p xs        : [96]
map f xs           : [0]
map f (filter p xs): [0]
filter p (map f xs): []

Logs for failed test run:
generated {_->0} at CallStack (from HasCallStack):
  gen, called at demo/Demo/Blogpost.hs:254:30 in main:Demo.Blogpost
generated {96->True, _->False} at CallStack (from HasCallStack):
  gen, called at demo/Demo/Blogpost.hs:255:30 in main:Demo.Blogpost
generated [96] at CallStack (from HasCallStack):
  gen, called at demo/Demo/Blogpost.hs:256:20 in main:Demo.Blogpost

It generated a function that maps anything to 0, a predicate that is True for 96 and False for everything else, and a list containing only the value 96; this is indeed a nice counter-example, as the output from the assert explains.

This property will fail:

failed after 4 successful tests and 14 shrinks
original < shrunk
original: 0
shrunk  : 1

Logs for failed test run:
generated 2 at CallStack (from HasCallStack):
  gen, called at demo/Demo/Blogpost.hs:281:10 in main:Demo.Blogpost

Suppose we want to verify that if we use this generator to test the (false) property that “all elements of all lists are always equal” we should always get either [0, 1] or [1, 0] as a counter-example; after all, those are the two minimal counter-examples. We could test this as follows:

The counter-example reported by falsify is (somewhat shortened):

naiveList_minimum: FAIL
  failed after 0 shrinks
  minimum `notElem` expected
  minimum : [0,0,1]
  expected: [[0,1],[1,0]]

Logs for failed test run:
generated [0,0,1] at CallStack (from HasCallStack):
  gen, called at demo/Demo/Blogpost.hs:294:13 in main:Demo.Blogpost

Logs for rejected potential next shrinks:

** Rejected run 0
generated [] at CallStack (from HasCallStack):

** Rejected run 3
generated [0] at CallStack (from HasCallStack):

** Rejected run 4
generated [0,0] at CallStack (from HasCallStack):

** Rejected run 8
generated [0,0,0] at CallStack (from HasCallStack):

This is telling us that the minimum value it produced was [0, 0, 1], instead of one of the two lists that we expected. It also tells us what shrink steps were rejected (because they weren’t counter-examples). This is informative, because _none of those shrink steps is [0, 1]: the naive list generator, unlike the real one (which does pass this property) cannot drop elements from the start of the list.

and hedgehog style shrinking

respectively. The implementation of these combinators depends on a minor generalization of the sample tree representation; the details are discussed in the paper.

Conclusions

Shrinking is an essential component of any approach to property based testing. In the Haskell world, two libraries offered two competing approaches to shrinking: manual shrinking offered by QuickCheck, where users are entirely responsible for writing shrinkers for their generators, and integrated shrinking, offered by hedgehog. Integrated shrinking is nice, but does not work well with monadic bind. The Python Hypothesis library taught us how we can have “internal” shrinking: like in integrated shrinking, we do not write a separate generator and shrinker, but unlike in integrated shrinking, this approach does work across monadic bind.

The Haskell falsify library takes the core ideas of Hypothesis and applies them in the context of Haskell. As we have seen, however, the actual details of how these two libraries work differ quite significantly. The falsify approach is more suitable to Haskell where we might deal with infinite data structures, provides the user with more predictable shrinking, and provides the user with tools for controlling generator independence (through the use of selective functors).