QuickSpec: equational laws for free!

Ever get that nagging feeling that your code must satisfy some algebraic properties, but not sure what they are? Want to write some QuickCheck properties, but not sure where to start? QuickSpec might be for you! Give it your program — QuickSpec will find the laws it obeys.

QuickSpec takes any hodgepodge of functions, and tests those functions to work out the relationship between them. It then spits out what it discovered as a list of equations.

Give QuickSpec reverse, ++ and [], for example, and it will find six laws:

xs++[] == xs
[]++xs == xs
(xs++ys)++zs == xs++(ys++zs)
reverse [] == []
reverse (reverse xs) == xs
reverse xs++reverse ys == reverse (ys++xs)

All the laws you would expect to hold, and nothing more — and all discovered automatically! Brill!

Where’s the catch? While QuickSpec is pretty nifty, it isn’t magic, and has a number of limitations:

• QuickSpec can only discover equations, not other kinds of laws. Luckily, equations cover a lot of what you would normally want to say about Haskell programs. Often, even if a law you want isn’t equational, QuickSpec will discover equational special cases of that law which suggest the general case.

• You have to tell QuickSpec exactly which functions and constants it should consider when generating laws. In the example above, we gave reverse, ++ and [], and those are the only functions that appear in the six equations. For example, we don’t get the equation (x:xs)++ys == x:(xs++ys), because we didn’t include : in the functions we gave to QuickSpec. A large part of using QuickSpec effectively is choosing which functions to consider in laws.

• QuickSpec exhaustively enumerates terms, so it will only discover equations about small(ish) terms — in fact, terms up to a fixed depth. You can adjust the maximum depth but, as QuickSpec exhaustively enumerates terms, there is an exponential blowup as you increase the depth. Likewise, there is an exponential blowup as you give QuickSpec more functions to consider (though it doesn’t blow up as badly as you might think!)

• QuickSpec only tests the laws, it doesn’t try to prove them. So while the generated laws are very likely to be true, there is still a chance that they are false, especially if your test data generation is not up to scratch.

Despite these limitations, QuickSpec works well on many examples.

The rest of this README introduces QuickSpec through a couple of short examples. You can look at the bottom of this file for links to more examples, Haddock documentation and our paper about QuickSpec.

Installing

Install QuickSpec in the usual way — cabal install quickspec.

Booleans — the basics

Let’s start by testing some boolean operators.

To run QuickSpec, we must define a signature, which specifies which functions we want to test, together with the variables that can appear in the generated equations. Here is our signature:

bools = [
  ["x", "y", "z"] `vars` (undefined :: Bool),

  "||"    `fun2` (||),
  "&&"    `fun2` (&&),
  "not"   `fun1` not,
  "True"  `fun0` True,
  "False" `fun0` False]

In the signature, we define three variables (x, y and z) of type Bool, using the FUNvars[vars] combinator, which takes two parameters: a list of variable names, and the type we want those variables to have. We also give give QuickSpec the functions ||, &&, not, True and False, using the FUNfun0[fun0]/FUNfun1[fun1]/FUNfun2[fun2] combinators. These take two parameters: the name of the function, and the function itself. The integer, 0, 1 or 2 here, is the arity of the function.

Having written this signature, we can invoke QuickSpec just by calling the function FUNquickSpec[quickSpec]:

import Test.QuickSpec hiding (bools)
main = quickSpec bools

You can find this code in EXAMPLEBools.hs[examples/Bools.hs] in the QuickSpec distribution. Go on, run it! (Compile it or else it’ll go slow.) You will see that QuickSpec prints out:

1. The signature it’s testing, i.e. the types of all functions and variables. If something fishy is happening, check that the functions and types match up with what you expect! QuickSpec will also print a warning here if something seems fishy about the signature, e.g. if there are no variables of a certain type.

2. A summary of how much testing it did.

3. The equations it found — the exciting bit! The equations are grouped according to which function they talk about, with equations that relate several functions at the end.

Peering through what QuickSpec found, you should see the familiar laws of Boolean algebra. The only oddity is the equation x||(y||z) == y||(x||z). This is QuickSpec’s rather eccentric way of expressing that || is associative — in the presence of the law x||y == y||x, it’s equivalent to associativity, and QuickSpec happens to choose this formulation rather than the more traditional one. All the other laws are just as we would expect, though. Not bad for 5 minutes' work!

Lists — polymorphic functions and the prelude

Now let’s try testing some list functions — perhaps just reverse, ++ and []. We might start by writing a signature by analogy with the earlier booleans example:

lists = [
  ["xs", "ys", "zs"] `vars` (undefined :: [a]),

  "[]"      `fun0` [],
  "reverse" `fun1` reverse,
  "++"      `fun2` (++)]

Unfortunately, QuickSpec only supports monomorphic functions. The functions and variables in the lists signature are polymorphic, and GHC complains:

No instance for (Arbitrary a0) arising from a use of `vars'
The type variable `a0' is ambiguous

The solution is to monomorphise the signature ourselves. QuickSpec provides types called TYPEA[A], TYPEB[B] and TYPEC[C] for that purpose, so we simply specialise all type variables to TYPEA[A]:

lists = [
  ["xs", "ys", "zs"] `vars` (undefined :: [A]),

  "[]"      `fun0` ([] :: [A]),
  "reverse" `fun1` (reverse :: [A] -> [A]),
  "++"      `fun2` ((++) :: [A] -> [A] -> [A])]

Having done that, we get the six laws from the beginning of this file.

Perhaps we now decide we want laws about length too. We want to keep our existing list functions in the signature, so that we get laws relating them to length, but on the other hand we only want to see new laws, i.e. the ones that mention length. We can do this by marking the existing functions as background functions, and the resulting signature looks as follows:

lists = [
  ["xs", "ys", "zs"] `vars` (undefined :: [A]),

  background [
    "[]"      `fun0` ([] :: [A]),
    "reverse" `fun1` (reverse :: [A] -> [A]),
    "++"      `fun2` ((++) :: [A] -> [A] -> [A])],
  "length" `fun1` (length :: [A] -> Int)]

QuickSpec will only print an equation if it involves at least one non-background function, in this case length. Running QuickSpec again we get the following two laws:

length (reverse xs) == length xs
length (xs++ys) == length (ys++xs)

The first equation is all very well and good, but the second one is a bit unsatisfying. Wouldn’t we rather get length (xs++ys) = length xs + length ys? To get that equation, we need to add (+) :: Int -> Int -> Int to the signature. Adding it as a background function gives us the law we want.

You often need a wide variety of background functions to get good equations out of QuickSpec, and it gets a bit tedious declaring them all by hand. To help you with this QuickSpec provides a prelude, a predefined set of background functions which you can import into your own signature. The prelude is very minimal, but includes basic boolean, arithmetic and list functions. We can write our lists signature using the prelude as follows:

lists = [
  prelude (undefined :: A) `without` ["[]", ":"],

  background [
    "reverse" `fun1` (reverse :: [A] -> [A])],
  "length" `fun1` (length :: [A] -> Int)]

A call to FUNprelude[prelude] (undefined :: a) will declare the following background functions: * The boolean connectives ||, &&, not, True and False. * The arithmetic operations 0, 1, + and * over type Int. * The list operations [], :, ++, head and tail over type [a]. * Three variables each of type Bool, Int, a and [a].

In the example above we used the FUNwithout[without] combinator to leave out [] and : from the prelude, so as to get fewer laws. QuickSpec also provides the combinators FUNbools[bools], FUNarith[arith] and FUNlists[lists], which import only their respective part of the prelude, for when you want more control — see the DOCS[documentation] for more information.

In EXAMPLELists.hs[Lists.hs] you can find an extended version of the above example which also tests map.

Advanced: function composition — testing types with no Ord instance

Warning

this section isn’t finished.

Important

You can skip this section unless you need to test a type with no Ord instance.

Suppose we want to get QuickSpec to discover the laws of function composition — things like id . f == f.

If we just define a signature containing id and (.) (and suitable variables), the output is rather disappointing:

(f . g) x == f (g x)
id x == x

This is because QuickSpec is giving us laws about fully saturated applications of (.) and id, that is, (.) applied to three arguments and id applied to one argument. In the laws we are after, we only want to apply (.) to two arguments, and we don’t want to apply id to an argument at all. To fix this we can declare (.) to have arity 2 and id to have arity 1, so that QuickSpec won’t fully apply them:

composition = [
  vars ["f", "g", "h"] (undefined :: A -> A),
  fun2 "."   ((.) :: (A -> A) -> (A -> A) -> (A -> A)),
  fun0 "id"  (id  :: A -> A),
  ]

Unfortunately, we get the following error message:

Could not deduce (Ord (A -> A)) arising from a use of `fun2'

To test a law like id . f == f, QuickSpec generates a random value for f and then just evaluates the expression id . f == f to get either True or False.

The error message complains that we are trying to generate laws about terms of the type A -> A (i.e. functions), but as there is no Ord instance for functions QuickSpec has no way of testing the laws. QuickSpec tests a law like id . f == f by generating random values for f and seeing if the resulting left-hand side and right-hand side evaluate to the same value; it can only do this if it has an Ord instance for the values in question. As there is no way to tell if two functions are equal, it seems we are stuck!

Hang on, though. We can still test if two functions are equal: generate a random argument and apply the two functions to it, and see if they both give the same result. If they don’t, they’re certainly not equal. Repeat the process a few times, for several random arguments, and if both functions always seem to give the same result then they’re probably equal.

This is a common situation — we have a type, we cannot directly compare values of that type, but we can make random observations and compare those. For our example, observing a function consists of applying the function to a random argument. QuickSpec supports finding equations over types that you can observe. The observations must satisfy the following properties:

• The observation returns a value of a type that we can directly compare for equality.

• If two values are different, there is an observation that distinguishes them.

• If an observation distinguishes two values, they are not equal.

Common pitfalls

Warning

this section isn’t finished.

I get laws which seem to be false! If a law really is false, it means that QuickCheck didn’t discover the counterexample to it. Possible solutions include:

• Improve the test data generation. If you can’t change the Arbitrary` instance for your type, you can use the FUNgvars[gvars] combinator, which is like FUNvars[vars] but allows you to specify the generator.

• If you are testing a polymorphic function, try instantiating it with the QuickSpec type TYPETwo[Two] instead of TYPEA[A]. TYPETwo[Two] is a type that has only two elements, which may make it easier to hit counterexamples.

• Use the FUNwithTests[withTests] combinator to increase the number of tests.

QuickSpec runs for a very long time without terminating! QuickSpec works by enumerating all terms up to a certain depth, and therefore suffers from exponential blowup. Check the output where it reports how many terms it generated:

== Testing ==
Depth 1: 6 terms, 4 tests, 18 evaluations, 6 classes, 0 raw equations.
Depth 2: 61 terms, 500 tests, 28568 evaluations, 15 classes, 46 raw equations.
Depth 3: 412 terms, 500 tests, 205912 evaluations, 53 classes, 359 raw equations.

Here it’s generated 412 terms. If the number gets much above 100,000 then you will probably run into trouble. This can be caused by one of several things: * Too many functions in the signature.

I only get ground instances of the laws I want!

Perhaps you forgot to add

no variables

Law not found

Is it true? Is it provable? Are all necessary functions in the signature? Do the types match up so that the term is well-typed?

Get false laws

Tweak test data generators

Exponential blowup

I want to test a datatype with no Ord instance, such as functions

see function composition

A common mistake when using QuickSpec is to forget to define any variables of a certain type. In that case, you will typically get lots of special cases instead of the law you really want. For example,

True||True == True
True||False == True
False||True == True
False||False == False

Where to go from here?

Have a look at the examples that come with QuickSpec:

* link:examples/Bools.hs[Booleans]
* link:examples/Arith.hs[Arithmetic]
* link:examples/Lists.hs[List functions]
* link:examples/Heaps.hs[Binary heaps]
* link:examples/Composition.hs[Function composition]
* link:examples/Arrays.hs[Arrays]
* link:examples/TinyWM.hs[A tiny window manager]
* link:examples/PrettyPrinting.hs[Pretty-printing combinators]

Read our PAPER[paper].

Read the DOCS[Haddock documentation] for things to tweak.