speculate
discovery of properties about Haskell functions
https://github.com/rudymatela/speculate#readme
LTS Haskell 22.33: | 0.4.20 |
Stackage Nightly 2024-09-07: | 0.4.20 |
Latest on Hackage: | 0.4.20 |
speculate-0.4.20@sha256:c7b4d1d3022ad4e90d2793222259bf91f52d47aa52be9c9da58f9b714658e623,5812
Module documentation for 0.4.20
Speculate
Speculate automatically discovers laws about Haskell functions. Give Speculate a bunch of Haskell functions and it will discover laws like:
- equations, such as
id x == x
; - relations of order, such as
0 <= x * x
; - conditional equations, such as
x <= 0 ==> x + abs x == 0
.
Speculate is similar to, and inspired by, QuickSpec.
Installing Speculate
To install the latest Speculate version from Hackage, just:
$ cabal update
$ cabal install speculate
Pre-requisites are cmdargs, express and leancheck. They should be automatically resolved and installed by Cabal.
Using Speculate
Speculate is used as a library: import it, then call the function speculate
with relevant arguments. The following program Speculates about the
functions (+)
and abs
:
import Test.Speculate
main :: IO ()
main = speculate args
{ constants =
[ showConstant (0::Int)
, showConstant (1::Int)
, constant "+" ((+) :: Int -> Int -> Int)
, constant "abs" (abs :: Int -> Int)
]
}
when run, it prints the following:
_ :: Int (holes: Int)
0 :: Int
1 :: Int
(+) :: Int -> Int -> Int
abs :: Int -> Int
abs (abs x) == abs x
x + 0 == x
x + y == y + x
(x + y) + z == x + (y + z)
abs (x + abs x) == x + abs x
abs x + abs x == abs (x + x)
abs (1 + abs x) == 1 + abs x
x <= abs x
0 <= abs x
x <= x + 1
Now, if we add <=
and <
as background constants on args
, constants =
[ showConstant (0::Int)
, showConstant (1::Int)
, constant "+" ((+) :: Int -> Int -> Int)
, constant "abs" (abs :: Int -> Int)
, background
, constant "<=" ((<=) :: Int -> Int -> Bool)
, constant "<" ((<) :: Int -> Int -> Bool)
]
then run again, we get the following as well:
y <= x ==> abs (x + abs y) == x + abs y
x <= 0 ==> x + abs x == 0
abs x <= y ==> abs (x + y) == x + y
abs y <= x ==> abs (x + y) == x + y
For more examples, see the eg folder.
(One can use the TypeApplications to simplify the above examples:
((+) @ Int)
instead of ((+) :: Int -> Int -> Int))
.
I have chosen to keep the example Haskell 98 compliant.)
Supported types
Speculate works for virtually any type.
However,
if you would like to produce equations,
comparisons and variables of any given type
this type must be respectively
an instance of the Eq
, Ord
, Listable
and Name
typeclasses.
By default,
Speculate will produce equations, comparison and variables
to a few types
in the Haskell 2010 Language Report.
If you would like expand that to more types,
you need to pass reified instances to Speculate explicitly by
using reifyInstances
on instances =
of speculate
’s args
like so:
main = speculate args
{ instances = [ reifyInstances (undefined :: <Type1>)
, reifyInstances (undefined :: <Type2>)
, reifyInstances (undefined :: <Type3>)
, ...
]
, constants = ...
, ...
}
To use reifyInstances
,
your type must be an instance of
Eq
, Ord
, Listable
and Name
.
-
Eq
is needed for equations between values of the type; -
Ord
is needed for comparisons between values of the type; -
Listable
is needed for involving variables of the type. This is needed in order for Speculate to be able to generate values of your type to replace any variables. LeanCheck comes withListable
instances for virtually all types in the Haskell 2010 Language Report. -
Name
is needed for cosmetic puposes: if there are any variables of your type,Name
allows you to tell Speculate how to call your variables. For example, if you have anUser
type, you can define your name instance as:instance Name (User) where name u = "usr"
This way, variables of your
User
type will be called:usr
,usr1
,usr2
,usr3
, etc.
It is also fine to have only one, two or three of the above instances.
In that case, instead of reifyInstances
you can use reifyEq
, reifyOrd
, reifyListable
and reifyName
accordingly.
If you do not provide a Name
implementation,
your variables will default to being x
, y
and z
.
This may cause confusion as you involve more and more types,
compare the following two identical equations:
[x,y] `areOwnedBy` z == z `owns` x && z `owns` y
[tckt,tckt1] `areOwnedBy` user == usr `owns` tckt && user `owns tckt1`
The second is clearer.
So, I recomment you add a Name
instance.
It is simple enough.
You also have to do this for any user defined types you are using or even for newtypes.
Speculate comes with a few examples illustrating the use of reifyInstances
:
on the eg folder:
eg/algebraic-graphs.hs,
eg/binarytree0.hs,
eg/binarytree.hs,
eg/colour.hs,
eg/digraphs.hs,
eg/fun.hs,
eg/monad.hs,
eg/pretty-compact.hs,
eg/pretty.hs,
eg/regexes.hs,
eg/sets.hs,
eg/speculate-reason.hs,
eg/string.hs,
eg/tauts.hs,
eg/tuples.hs,
eg/zip.hs.
Not having the reified instances for a given type will cause the following warnings to be printed:
Warning: no Listable instance for <YourTypeHere>, variables of this type will not be considered
Warning: no Listable instance for <YourTypeHere>, variables of this type will not be considered
Warning: no Eq instance for <YourTypeHere>, equations of this type will not be considered
Warning: no Eq instance for <YourTypeHere>, equations of this type will not be considered
Warning: no Ord instance for <YourTypeHere>, inequations of this type will not be considered
Warning: no Ord instance for <YourTypeHere>, inequations of this type will not be considered
You can silence the above warnings by following the instructions above. However, it may be the case that you don’t want variables, equations or comparisons for a given type. If that is so, you can ignore these warnings.
Similarities and Differences to QuickSpec
Speculate is inspired by QuickSpec. Like QuickSpec, Speculate uses testing to speculate equational laws about given Haskell functions. There are some differences:
- Speculate tests enumeratively using LeanCheck, QuickSpec tests randomly using QuickCheck;
- Speculate is able to report comparisons directly;
- QuickSpec allows polymorphism, Speculate does not;
- For most examples, Speculate runs slower than QuickSpec 2 but faster than QuickSpec 1.
More documentation
For more examples, see the eg and bench folders.
Speculate has been subject to a paper, see the Speculate Paper on Haskell Symposium 2017. Speculate is also subject to a chapter in a PhD Thesis (2017).
Changes
Changelog for Speculate
v0.4.20 (February 2024)
- minor changes only
- improve
consider
by favouring the normalization only if it reduces the number of variables - revert back (v0.4.16) to using vanilla syntactic unification instead of syntactic unification modulo commutativity
- some internal refactoring
v0.4.18 (February 2024)
Test.Speculate.Expr.Ground
: addconstify
andconstifications
Reason
: fixgroundJoinable
with the last criteriumReason
: useunificationsC
to unify- minor improvements in the code
- rework test scripts and
Makefile
- remove stale tests
v0.4.16 (February 2024)
- no changes in API
- fix compatibility with express >= v1.0.16
- bump LeanCheck requirement to >= 1.0.0
- improve tests of Speculate itself
- add release dates on this changelog
v0.4.14 (September 2021)
Test.Speculate.Reason
: adddoubleCheck
;- add
lowtests
benchmark; - bump express requirement to v1.0.0;
- fix parallel compilation when using the Makefile.
v0.4.12 (July 2021)
- bump express requirement to v0.2.0
- add this changelog
v0.4.10 (June 2021)
- no changes in the actual Speculate library
- cleanup build files
- remove uneeded typeable derivations on examples and tests
v0.4.8 (June 2021)
- no changes in the actual Speculate library
- refactor build scripts
- use GitHub Workflows as the CI
- fix compilation of some examples under the new LeanCheck
v0.4.6 (April 2021)
Test.Speculate
: exportreifyName
;- “internal” modules:
Test.Speculate.Args
: removecompareExpr
;Test.Speculate.Engine
: add three new wrappers for “theory and representatives”;Test.Speculate.Expr.Core
: rename functions tocompareLexicographicallyBy
andcompareComplexityThenIndex
;Test.Speculate.Function
: addFunction.A10
andA100
andA1000
;Test.Speculate.Reason
: exportisRootNormal
andisRootNormalE
;
- add trilean benchmark;
- improve order tests.
Earlier versions
Please refer to the git commit history.