-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | Equational laws for free!
--
-- QuickSpec takes your Haskell code and, as if by magic, discovers laws
-- about it. You give QuickSpec a collection of Haskell functions;
-- QuickSpec tests your functions with QuickCheck and prints out laws
-- which seem to hold.
--
-- For example, give QuickSpec the functions reverse,
-- ++ and [], and it will find six laws:
--
--
-- reverse [] == []
-- xs ++ [] == xs
-- [] ++ xs == xs
-- reverse (reverse xs) == xs
-- (xs ++ ys) ++ zs == xs ++ (ys ++ zs)
-- reverse xs ++ reverse ys == reverse (ys ++ xs)
--
--
-- QuickSpec can find equational laws as well as conditional equations.
-- All you need to supply are the functions to test, as well as
-- Ord and Arbitrary instances for QuickSpec to use in
-- testing; the rest is automatic.
--
-- For information on how to use QuickSpec, see the documentation in the
-- main module, QuickSpec. You can also look in the
-- examples directory, for example at
-- Lists.hs, IntSet.hs, or
-- Parsing.hs. To read about how QuickSpec works, see our
-- paper, Quick specifications for the busy programmer.
@package quickspec
@version 2
-- | The main QuickSpec module. Everything you need to run QuickSpec lives
-- here.
--
-- To run QuickSpec, you need to tell it which functions to test. We call
-- the list of functions the signature. Here is an example
-- signature, which tells QuickSpec to test the ++,
-- reverse and [] functions:
--
--
-- sig = [
-- con "++" ((++) :: [A] -> [A] -> [A]),
-- con "reverse" (reverse :: [A] -> [A]),
-- con "[]" ([] :: [A]) ]
--
--
-- The con function, used above, adds a function to the signature,
-- given its name and its value. When declaring polymorphic functions in
-- the signature, we use the types A to E to represent type
-- variables. Having defined this signature, we can say
-- quickSpec sig to test it and see the discovered
-- equations.
--
-- If you want to test functions over your own datatypes, those types
-- need to implement Arbitrary and Ord (if the Ord
-- instance is a problem, see Observe). You must also declare
-- those instances to QuickSpec, by including them in the signature. For
-- monomorphic types you can do this using monoType:
--
--
-- data T = ...
-- main = quickSpec [
-- ...,
-- `monoType` (Proxy :: Proxy T)]
--
--
-- You can only declare monomorphic types with monoType. If you
-- want to test your own polymorphic types, you must explicitly declare
-- Arbitrary and Ord instances using the inst
-- function.
--
-- You can also use QuickSpec to find conditional equations. To do so,
-- you need to include some predicates in the signature. These are
-- functions returning Bool which can appear as conditions in
-- other equations. Declaring a predicate works just like declaring a
-- function, except that you declare it using predicate instead of
-- con.
--
-- You can also put certain options in the signature. The most useful is
-- withMaxTermSize, which you can use to tell QuickSpec to
-- generate larger equations.
--
-- The examples directory contains many examples. Here
-- are some interesting ones:
--
--
-- - Arith.hs: a simple arithmetic example.
-- Demonstrates basic use of QuickSpec.
-- - Lists.hs: list functions. Demonstrates testing
-- polymorphic functions.
-- - Sorted.hs: sorting. Demonstrates finding
-- conditional equations.
-- - IntSet.hs: a few functions from
-- Data.IntSet. Demonstrates testing user-defined datatypes and
-- finding conditional equations.
-- - PrettyPrinting.hs: pretty printing combinators.
-- Demonstrates testing user-defined datatypes and using observational
-- equality.
-- - Parsing.hs: parser combinators. Demonstrates
-- testing polymorphic datatypes and using observational equality.
--
--
-- You can also find some larger case studies in our paper,
-- <http://www.cse.chalmers.se/~nicsma/papers/quickspec2.pdf
-- Quick specifications for the busy programmer>.
module QuickSpec
-- | Run QuickSpec. See the documentation at the top of this file.
quickSpec :: Signature sig => sig -> IO ()
-- | A signature.
data Sig
-- | A class of things that can be used as a QuickSpec signature.
class Signature sig
-- | Convert the thing to a signature.
toSig :: Signature sig => sig -> Sig
-- | Declare a constant with a given name and value. If the constant you
-- want to use is polymorphic, you can use the types A, B,
-- C, D, E to monomorphise it, for example:
--
--
-- constant "reverse" (reverse :: [A] -> [A])
--
--
-- QuickSpec will then understand that the constant is really
-- polymorphic.
con :: Typeable a => String -> a -> Sig
-- | Declare a predicate with a given name and value. The predicate should
-- be a function which returns Bool. It will appear in equations
-- just like any other constant, but will also be allowed to appear as a
-- condition.
--
-- For example:
--
--
-- sig = [
-- con "delete" (delete :: Int -> [Int] -> [Int]),
-- con "insert" (insert :: Int -> [Int] -> [Int]),
-- predicate "member" (member :: Int -> [Int] -> Bool) ]
--
predicate :: (Predicateable a, Typeable a, Typeable (TestCase a)) => String -> a -> Sig
data A
data B
data C
data D
data E
-- | Declare a new monomorphic type. The type must implement Ord and
-- Arbitrary.
monoType :: forall proxy a. (Ord a, Arbitrary a, Typeable a) => proxy a -> Sig
-- | Customize how variables of a particular type are named.
vars :: forall proxy a. Typeable a => [String] -> proxy a -> Sig
-- | Declare a new monomorphic type, saying how you want variables of that
-- type to be named.
monoTypeWithVars :: forall proxy a. (Ord a, Arbitrary a, Typeable a) => [String] -> proxy a -> Sig
-- | Declare a typeclass instance. QuickSpec needs to have an Ord
-- and Arbitrary instance for each type you want it to test.
--
-- For example, if you are testing Map k v, you will need
-- to add the following two declarations to your signature:
--
--
-- inst (Sub Dict :: (Ord A, Ord B) :- Ord (Map A B))
-- inst (Sub Dict :: (Arbitrary A, Arbitrary B) :- Arbitrary (Map A B))
--
inst :: (Typeable c1, Typeable c2) => c1 :- c2 -> Sig
-- | A typeclass for types which support observational equality, typically
-- used for types that have no Ord instance.
--
-- An instance Observe test outcome a declares that values of
-- type a can be tested for equality by random testing.
-- You supply a function observe :: test -> outcome -> a.
-- Then, two values x and y are considered equal, if
-- for many random values of type test, observe test x ==
-- observe test y.
--
-- For an example of using observational equality, see
-- PrettyPrinting.hs.
--
-- You must use inst to add the Observe instance to your
-- signature. Note that monoType requires an Ord instance,
-- so this even applies for monomorphic types. Don't forget to add the
-- Arbitrary instance too in that case.
class (Arbitrary test, Ord outcome) => Observe test outcome a | a -> test outcome
-- | Make an observation on a value. Should satisfy the following law: if
-- x /= y, then there exists a value of test such that
-- observe test x /= observe test y.
observe :: Observe test outcome a => test -> a -> outcome
-- | Make an observation on a value. Should satisfy the following law: if
-- x /= y, then there exists a value of test such that
-- observe test x /= observe test y.
observe :: (Observe test outcome a, test ~ (), outcome ~ a) => test -> a -> outcome
-- | Declare some functions as being background functions. These are
-- functions which are not interesting on their own, but which may appear
-- in interesting laws with non-background functions. Declaring
-- background functions may improve the laws you get out.
--
-- Here is an example, which tests ++ and length,
-- giving 0 and + as background functions:
--
--
-- main = quickSpec [
-- con "++" ((++) :: [A] -> [A] -> [A]),
-- con "length" (length :: [A] -> Int),
--
-- background [
-- con "0" (0 :: Int),
-- con "+" ((+) :: Int -> Int -> Int) ] ]
--
background :: Signature sig => sig -> Sig
-- | Run QuickCheck on a series of signatures. Tests the functions in the
-- first signature, then adds the functions in the second signature, then
-- adds the functions in the third signature, and so on.
--
-- This can be useful when you have a core API you want to test first,
-- and a larger API you want to test later. The laws for the core API
-- will be printed separately from the laws for the larger API.
--
-- Here is an example which first tests 0 and + and
-- then adds ++ and length:
--
--
-- main = quickSpec [sig1, sig2]
-- where
-- sig1 = [
-- con "0" (0 :: Int),
-- con "+" ((+) :: Int -> Int -> Int) ]
-- sig2 = [
-- con "++" ((++) :: [A] -> [A] -> [A]),
-- con "length" (length :: [A] -> Int) ]
--
series :: Signature sig => [sig] -> Sig
-- | Set the maximum size of terms to explore (default: 7).
withMaxTermSize :: Int -> Sig
-- | Set how many times to test each discovered law (default: 1000).
withMaxTests :: Int -> Sig
-- | Set the maximum value for QuickCheck's size parameter when generating
-- test data (default: 20).
withMaxTestSize :: Int -> Sig
-- | Set which type polymorphic terms are tested at.
defaultTo :: Typeable a => proxy a -> Sig
-- | Set how hard QuickSpec tries to filter out redundant equations
-- (default: no limit).
--
-- If you experience long pauses when running QuickSpec, try setting this
-- number to 2 or 3.
withPruningDepth :: Int -> Sig
-- | Set the maximum term size QuickSpec will reason about when it filters
-- out redundant equations (default: same as maximum term size).
--
-- If you get laws you believe are redundant, try increasing this number
-- to 1 or 2 more than the maximum term size.
withPruningTermSize :: Int -> Sig
-- | Set the random number seed used for test case generation. Useful if
-- you want repeatable results.
withFixedSeed :: Int -> Sig
-- | The class Typeable allows a concrete representation of a type
-- to be calculated.
class Typeable k (a :: k)
-- | This is the type of entailment.
--
-- a :- b is read as a "entails" b.
--
-- With this we can actually build a category for Constraint
-- resolution.
--
-- e.g.
--
-- Because Eq a is a superclass of Ord a,
-- we can show that Ord a entails Eq a.
--
-- Because instance Ord a => Ord [a] exists, we
-- can show that Ord a entails Ord [a] as
-- well.
--
-- This relationship is captured in the :- entailment type here.
--
-- Since p :- p and entailment composes, :- forms
-- the arrows of a Category of constraints. However,
-- Category only became sufficiently general to support this
-- instance in GHC 7.8, so prior to 7.8 this instance is unavailable.
--
-- But due to the coherence of instance resolution in Haskell, this
-- Category has some very interesting properties. Notably, in the
-- absence of IncoherentInstances, this category is "thin",
-- which is to say that between any two objects (constraints) there is at
-- most one distinguishable arrow.
--
-- This means that for instance, even though there are two ways to derive
-- Ord a :- Eq [a], the answers from these
-- two paths _must_ by construction be equal. This is a property that
-- Haskell offers that is pretty much unique in the space of languages
-- with things they call "type classes".
--
-- What are the two ways?
--
-- Well, we can go from Ord a :- Eq a via
-- the superclass relationship, and then from Eq a :-
-- Eq [a] via the instance, or we can go from Ord
-- a :- Ord [a] via the instance then from
-- Ord [a] :- Eq [a] through the superclass
-- relationship and this diagram by definition must "commute".
--
-- Diagrammatically,
--
--
-- Ord a
-- ins / \ cls
-- v v
-- Ord [a] Eq a
-- cls \ / ins
-- v v
-- Eq [a]
--
--
-- This safety net ensures that pretty much anything you can write with
-- this library is sensible and can't break any assumptions on the behalf
-- of library authors.
newtype (:-) a b :: Constraint -> Constraint -> *
Sub :: (a -> Dict b) -> (:-) a b
-- | Values of type Dict p capture a dictionary for a
-- constraint of type p.
--
-- e.g.
--
--
-- Dict :: Dict (Eq Int)
--
--
-- captures a dictionary that proves we have an:
--
--
-- instance Eq 'Int
--
--
-- Pattern matching on the Dict constructor will bring this
-- instance into scope.
data Dict a :: Constraint -> *
[Dict] :: Dict a
-- | A concrete, poly-kinded proxy type
data Proxy k (t :: k) :: forall k. () => k -> *
Proxy :: Proxy k
-- | Random generation and shrinking of values.
--
-- QuickCheck provides Arbitrary instances for most types in
-- base, except those which incur extra dependencies. For a
-- wider range of Arbitrary instances see the
-- quickcheck-instances package.
class Arbitrary a
instance QuickSpec.Signature QuickSpec.Sig
instance QuickSpec.Signature sig => QuickSpec.Signature [sig]
instance GHC.Base.Monoid QuickSpec.Sig