How do I get good (small) shrinks out of QuickCheck?

Question

I'm trying to run QuickCheck on some nested lists, something that looks like this:

type Constraint = Text
data Value = Value [Constraint]
data Literal = Literal Value [Value]
type Formula = [Literal]

So a formula is a list of literals, each of which contains a predicate and some arguments; predicate/arguments are values which are a disjunction of constraints in string form each. That gives us a list of lists of lists of lists, phew!

If one of my QuickCheck properties fails, I tend to get an incomprehensible pageful of output. Before experimenting with shrink, I used to get around this by having arbitrary instances that could only generate a small set of (small) values. Implementing the shrink function for each of my types seems to help a little, but not as much as I'd like. I still get a pageful of output.

I think what I want from shrink is a small list of literals, where each literal has a small list of values, which in turn has few constrains, each of which is as short as possible. But in my current efforts, at least of these lists gets big enough to make the output horrible. If I try to tune my shrink implementations, I also find that QC starts taking a very long time (searching for shrinks?), which kind of dampens my efforts to shrink effectively.

How do you improve your chances of understanding QuickCheck failures when you have nested data like this?

Colquitt

Some things I've tried: preferring shrinkList shrinkNothing to shrinkList shrink, and this alternative shrinkList which tries to favour removing more elements. I suspect I'm mucking around too much and should be doing something totally different, like changing my arbitrary implementations, or testing in a different way :-) – Colquitt

For now, I'm going the pre-shrunk route (take 5 <$> arbitrary), which I still seem to be finding bugs with – Colquitt

Not exactly an answer, but have you tried using SmallCheck or even LazySmallCheck instead of QuickCheck? – Starch

I was considering it. I was a bit scared off by having to write a bunch of new instances, but it shouldn't actually be that hard. I also wasn't sure if this sort of exhaustiveness is what I wanted in this list-of-list-of-list case. – Colquitt

Can you describe the properties that are failing in more detail? If the standard type-based shrinking isn't working, you probably need to write something more suited to your problem domain. – Christopher

Sure. So these are unification variables, eg ?X/cat|dog to mean label constrained to unify with only "cat" or "dog" (no label in my simplified code above). On top of this a function that does unification on formulas, and on top of that a function that expands another macro data structure (containing formulas). I wanted to check that the formulas in my expanded macros subsume the formulas in the original (ie. the template) – Colquitt

So the test input is just a single formula? – Christopher

Eh well! It's (A) formula which shares unification variables with a set of key-value pairs and (B) another set of key-value pairs. The idea is that (A) is a macro and (B) some instantiation, and you expand (A) by unifying B with the key-value pairs, percolating stuff into the formula via unification. – Colquitt

Meanwhile, I seem to be having a bit more luck with SmallCheck. Unfortunately, it seems to be telling me that my code is all wrong, which is good, but :-(! – Colquitt

Oh god, I'm an idiot. The test in question was failing because the property was incorrect. I just got subsumption backwards... again (it's more general subsumes more specific, so template subsumes expansion). Sigh. – Colquitt

I'm shocked that @ehird hasn't created an incredibly detailed and useful answer to this question yet, given his heavy activity on haskell-tag questions lately. :) – Turley

Answer 1

FWIW, have a look at https://github.com/leepike/SmartCheck, which claims to derive better shrinks than one can usually do manually.

Bcd

Answer 2

I had a similar problem, but I was using C and home made example generator :) I had slow and correct, and fast and incorrect implementation.

Using random examples, when you find incorrect example, I would suggest shrinking of example itself. (This, of course, could or should, be done by program, instead of by computer)

If you have predicate for this test, and you have example that does not work, try eliminating elements form lists, of all orders (this should be linear order of magnitude of callings) and for each try if it fails the test.

If it is still failing, there is no reason for keeping this in example.

If it starts passing, then this element should stay in reduced example.

(This is greedy and not optimal, but it does execute in poly, instead of exponential time, and it worked for me)

For more scientific look, I suggest chapter "Simplifying problems" from the book "WHY PROGRAMS FAIL: A Guide to Systematic Debugging" by A.Zeller.

Note: this is mostly what shrink does...

Upcast