//:replacements.DOCS: http://hackage.haskell.org/package/quickspec-0.9.5/docs/Test-QuickSpec.html
//:replacements.PAPER: http://www.cse.chalmers.se/~nicsma/papers/quickspec.pdf
//:replacements.FUN: http://hackage.haskell.org/package/quickspec-0.9.5/docs/Test-QuickSpec.html#v:
//:replacements.TYPE: http://hackage.haskell.org/package/quickspec-0.9.5/docs/Test-QuickSpec.html#t:
//:replacements.EXAMPLE: link:examples/

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. You can adjust the maximum terms
  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.

This directory contains a new version of QuickSpec which is currently
in flux - it works well, but has little documentation and the user
interface is likely to change. If you look in the `examples`
directory, you will find many examples which should help you on your
way. Alternatively, if you check out the `v1` branch of this
repository, you will find an older version of QuickSpec, which is
better-documented and slightly more polished, but worse at finding
equations.

//
//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:
//
//[source,haskell]
//------------------------------------------------
//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`]:
//
//[source,haskell]
//------------------------------------------------
//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:
//
//[source,haskell]
//----
//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`]:
//
//[source,haskell]
//----
//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:
//
//[source,haskell]
//----
//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:
//
//[source,haskell]
//----
//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.