Copyright | (c) 2016-2017 Rudy Matela |
---|---|
License | 3-Clause BSD (see the file LICENSE) |
Maintainer | Rudy Matela <rudy@matela.com.br> |
Safe Haskell | None |
Language | Haskell2010 |
Speculate: discovery of properties by reasoning from test results
Speculate automatically discovers laws about Haskell functions. Those laws involve:
- equations, such as
id x == x
; - inequalities, such as
0 <= x * x
; - conditional equations, such as
x <= 0 ==> x + abs x == 0
.
_Example:_ the following program prints laws about 0
, 1
, +
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) , background , constant "<=" ((<=) :: Int -> Int -> Bool) ] }
Synopsis
- speculate :: Args -> IO ()
- data Args = Args {
- maxSize :: Int
- maxTests :: Int
- constants :: [Expr]
- instances :: [Instances]
- maxSemiSize :: Int
- maxCondSize :: Int
- maxVars :: Int
- showConstants :: Bool
- showEquations :: Bool
- showSemiequations :: Bool
- showConditions :: Bool
- showConstantLaws :: Bool
- autoConstants :: Bool
- minTests :: Int -> Int
- maxConstants :: Maybe Int
- maxDepth :: Maybe Int
- showCounts :: Bool
- showTheory :: Bool
- showArgs :: Bool
- showHelp :: Bool
- evalTimeout :: Maybe Double
- force :: Bool
- extra :: [String]
- exclude :: [String]
- onlyTypes :: [String]
- showClassesFor :: [Int]
- showDot :: Bool
- quietDot :: Bool
- args :: Args
- data Expr
- constant :: Typeable a => String -> a -> Expr
- showConstant :: (Typeable a, Show a) => a -> Expr
- hole :: (Listable a, Typeable a) => a -> Expr
- foreground :: Expr
- background :: Expr
- type Instances = [Instance]
- ins :: (Typeable a, Listable a, Show a, Eq a, Ord a) => String -> a -> Instances
- eq :: (Typeable a, Eq a) => a -> Instances
- ord :: (Typeable a, Ord a) => a -> Instances
- eqWith :: (Typeable a, Eq a) => (a -> a -> Bool) -> Instances
- ordWith :: (Typeable a, Ord a) => (a -> a -> Bool) -> Instances
- names :: Instances -> TypeRep -> [String]
- report :: Args -> IO ()
- getArgs :: Args -> IO Args
- module Test.LeanCheck
- uint4 :: UInt4
- uint3 :: UInt3
- uint2 :: UInt2
- uint1 :: UInt1
- word4 :: Word4
- word3 :: Word3
- word2 :: Word2
- word1 :: Word1
- int4 :: Int4
- int3 :: Int3
- int2 :: Int2
- int1 :: Int1
- nat :: Nat
- natural :: Natural
- eith :: a -> b -> Either a b
- mayb :: a -> Maybe a
- ordering :: Ordering
- string :: String
- char :: Char
- bool :: Bool
- rational :: Rational
- double :: Double
- float :: Float
- integer :: Integer
- int :: Int
- und :: a
- (>-) :: a -> b -> a -> b
- (->>>>>>>>>>>>:) :: (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m) -> m -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m
- (->>>>>>>>>>>:>) :: (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m) -> m -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m
- (->>>>>>>>>>>:) :: (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l) -> l -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l
- (->>>>>>>>>>:>) :: (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l) -> k -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l
- (->>>>>>>>>>:) :: (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k) -> k -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k
- (->>>>>>>>>:>) :: (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k) -> j -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k
- (->>>>>>>>>:) :: (a -> b -> c -> d -> e -> f -> g -> h -> i -> j) -> j -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j
- (->>>>>>>>:>) :: (a -> b -> c -> d -> e -> f -> g -> h -> i -> j) -> i -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j
- (->>>>>>>>:) :: (a -> b -> c -> d -> e -> f -> g -> h -> i) -> i -> a -> b -> c -> d -> e -> f -> g -> h -> i
- (->>>>>>>:>) :: (a -> b -> c -> d -> e -> f -> g -> h -> i) -> h -> a -> b -> c -> d -> e -> f -> g -> h -> i
- (->>>>>>>:) :: (a -> b -> c -> d -> e -> f -> g -> h) -> h -> a -> b -> c -> d -> e -> f -> g -> h
- (->>>>>>:>) :: (a -> b -> c -> d -> e -> f -> g -> h) -> g -> a -> b -> c -> d -> e -> f -> g -> h
- (->>>>>>:) :: (a -> b -> c -> d -> e -> f -> g) -> g -> a -> b -> c -> d -> e -> f -> g
- (->>>>>:>) :: (a -> b -> c -> d -> e -> f -> g) -> f -> a -> b -> c -> d -> e -> f -> g
- (->>>>>:) :: (a -> b -> c -> d -> e -> f) -> f -> a -> b -> c -> d -> e -> f
- (->>>>:>) :: (a -> b -> c -> d -> e -> f) -> e -> a -> b -> c -> d -> e -> f
- (->>>>:) :: (a -> b -> c -> d -> e) -> e -> a -> b -> c -> d -> e
- (->>>:>) :: (a -> b -> c -> d -> e) -> d -> a -> b -> c -> d -> e
- (->>>:) :: (a -> b -> c -> d) -> d -> a -> b -> c -> d
- (->>:>) :: (a -> b -> c -> d) -> c -> a -> b -> c -> d
- (->>:) :: (a -> b -> c) -> c -> a -> b -> c
- (->:>) :: (a -> b -> c) -> b -> a -> b -> c
- (->:) :: (a -> b) -> b -> a -> b
- (-:>) :: (a -> b) -> a -> a -> b
- (-:) :: a -> a -> a
- newtype Int1 = Int1 {}
- newtype Int2 = Int2 {}
- newtype Int3 = Int3 {}
- newtype Int4 = Int4 {}
- newtype Word1 = Word1 {}
- newtype Word2 = Word2 {}
- newtype Word3 = Word3 {}
- newtype Word4 = Word4 {}
- newtype Natural = Natural {}
- newtype Nat = Nat {}
- newtype Nat1 = Nat1 {}
- newtype Nat2 = Nat2 {}
- newtype Nat3 = Nat3 {}
- newtype Nat4 = Nat4 {}
- newtype Nat5 = Nat5 {}
- newtype Nat6 = Nat6 {}
- newtype Nat7 = Nat7 {}
- type UInt1 = Word1
- type UInt2 = Word2
- type UInt3 = Word3
- type UInt4 = Word4
- newtype NoDup a = NoDup [a]
- newtype Bag a = Bag [a]
- newtype Set a = Set [a]
- newtype Map a b = Map [(a, b)]
- newtype X a = X {
- unX :: a
- newtype Xs a = Xs [a]
- (|=) :: (a -> Bool) -> a -> Bool
- (=|) :: Eq a => [a] -> Int -> [a] -> Bool
- ($=) :: (a -> Bool) -> a -> Bool
- (=$) :: Eq b => a -> (a -> b) -> a -> Bool
- okNum :: (Eq a, Num a) => a -> a -> a -> Bool
- okEqOrd :: (Eq a, Ord a) => a -> a -> a -> Bool
- okOrd :: Ord a => a -> a -> a -> Bool
- okEq :: Eq a => a -> a -> a -> Bool
- neverIdentity :: Eq a => (a -> a) -> a -> Bool
- identity :: Eq a => (a -> a) -> a -> Bool
- idempotent :: Eq a => (a -> a) -> a -> Bool
- strictTotalOrder :: Eq a => (a -> a -> Bool) -> a -> a -> a -> Bool
- totalOrder :: Eq a => (a -> a -> Bool) -> a -> a -> a -> Bool
- strictPartialOrder :: (a -> a -> Bool) -> a -> a -> a -> Bool
- partialOrder :: Eq a => (a -> a -> Bool) -> a -> a -> a -> Bool
- equivalence :: (a -> a -> Bool) -> a -> a -> a -> Bool
- asymmetric :: (a -> a -> Bool) -> a -> a -> Bool
- antisymmetric :: Eq a => (a -> a -> Bool) -> a -> a -> Bool
- symmetric :: (a -> a -> Bool) -> a -> a -> Bool
- irreflexive :: (a -> a -> Bool) -> a -> Bool
- reflexive :: (a -> a -> Bool) -> a -> Bool
- transitive :: (a -> a -> Bool) -> a -> a -> a -> Bool
- symmetric2 :: Eq b => (a -> a -> b) -> (a -> a -> b) -> a -> a -> Bool
- distributive :: Eq a => (a -> a -> a) -> (a -> a -> a) -> a -> a -> a -> Bool
- associative :: Eq a => (a -> a -> a) -> a -> a -> a -> Bool
- commutative :: Eq b => (a -> a -> b) -> a -> a -> Bool
- (||||) :: (a -> b -> Bool) -> (a -> b -> Bool) -> a -> b -> Bool
- (|||) :: (a -> Bool) -> (a -> Bool) -> a -> Bool
- (&&&&) :: (a -> b -> Bool) -> (a -> b -> Bool) -> a -> b -> Bool
- (&&&) :: (a -> Bool) -> (a -> Bool) -> a -> Bool
- (====) :: Eq c => (a -> b -> c) -> (a -> b -> c) -> a -> b -> Bool
- (===) :: Eq b => (a -> b) -> (a -> b) -> a -> Bool
- countsOn :: Eq b => (a -> b) -> [a] -> [(b, Int)]
- countsBy :: (a -> a -> Bool) -> [a] -> [(a, Int)]
- counts :: Eq a => [a] -> [(a, Int)]
- classifyOn :: Eq b => (a -> b) -> [a] -> [[a]]
- classifyBy :: (a -> a -> Bool) -> [a] -> [[a]]
- classify :: Eq a => [a] -> [[a]]
- conditionStatsT :: Listable a => Int -> [(String, a -> Bool)] -> IO ()
- conditionStats :: Listable a => Int -> [(String, a -> Bool)] -> IO ()
- classStatsT :: (Listable a, Show b) => Int -> (a -> b) -> IO ()
- classStats :: (Listable a, Show b) => Int -> (a -> b) -> IO ()
- module Data.Typeable
Documentation
speculate :: Args -> IO () Source #
Calls Speculate. See the example above (at the top of the file).
Its only argument is an Args
structure.
Arguments to Speculate
Args | |
|
The constants list
An encoded Haskell functional-application expression for use by Speculate.
constant :: Typeable a => String -> a -> Expr Source #
Encode a constant Haskell expression for use by Speculate.
It takes a string representation of a value and a value, returning an
Expr
. Examples:
constant "0" 0 constant "'a'" 'a' constant "True" True constant "id" (id :: Int -> Int) constant "(+)" ((+) :: Int -> Int -> Int) constant "sort" (sort :: [Bool] -> [Bool])
hole :: (Listable a, Typeable a) => a -> Expr Source #
(intended for advanced users)
hole (undefined :: Ty)
returns a hole of type Ty
By convention, a Hole is a variable named with the empty string.
foreground :: Expr Source #
A special Expr
value.
When provided on the constants
list,
makes all the following constants foreground
constants.
background :: Expr Source #
A special Expr
value.
When provided on the constants
list,
makes all the following constants background
constants.
Background constants can appear in laws about other constants, but not by
themselves.
The instances list
Misc.
module Test.LeanCheck
eith :: a -> b -> Either a b #
Undefined Either
value. Uses the types of the given values as the
argument types. For use with type binding operators.
Undefined Integer
value for use with type binding operators.
check $ (\x y -> x + y == y + x) ->:> integer
Undefined Int
value for use with type binding operators.
check $ (\x y -> x + y == y + x) ->:> int
(>-) :: a -> b -> a -> b infixr 9 #
Returns an undefined functional value that takes an argument of the type of its first argument and return a value of the type of its second argument.
ty >- ty = (undefined :: Ty -> Ty)
Examples:
'a' >- 'b' = char >- char = (undefined :: Char -> Char) int >- bool >- int = undefined :: Int -> Bool -> Int
(->>>>>>>>>>>>:) :: (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m) -> m -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m infixl 1 #
Forces the result type of a 12-argument function.
(->>>>>>>>>>>:>) :: (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m) -> m -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m infixl 1 #
Forces the type of the 12th argument.
(->>>>>>>>>>>:) :: (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l) -> l -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l infixl 1 #
Forces the result type of a 11-argument function.
(->>>>>>>>>>:>) :: (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l) -> k -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l infixl 1 #
Forces the type of the 11th argument.
(->>>>>>>>>>:) :: (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k) -> k -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k infixl 1 #
Forces the result type of a 10-argument function.
(->>>>>>>>>:>) :: (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k) -> j -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k infixl 1 #
Forces the type of the 10th argument.
(->>>>>>>>>:) :: (a -> b -> c -> d -> e -> f -> g -> h -> i -> j) -> j -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j infixl 1 #
Forces the result type of a 9-argument function.
(->>>>>>>>:>) :: (a -> b -> c -> d -> e -> f -> g -> h -> i -> j) -> i -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j infixl 1 #
Forces the 9th argument type.
(->>>>>>>>:) :: (a -> b -> c -> d -> e -> f -> g -> h -> i) -> i -> a -> b -> c -> d -> e -> f -> g -> h -> i infixl 1 #
Forces the result type of a 8-argument function.
(->>>>>>>:>) :: (a -> b -> c -> d -> e -> f -> g -> h -> i) -> h -> a -> b -> c -> d -> e -> f -> g -> h -> i infixl 1 #
Forces the 8th argument type.
(->>>>>>>:) :: (a -> b -> c -> d -> e -> f -> g -> h) -> h -> a -> b -> c -> d -> e -> f -> g -> h infixl 1 #
Forces the result type of a 7-argument function.
(->>>>>>:>) :: (a -> b -> c -> d -> e -> f -> g -> h) -> g -> a -> b -> c -> d -> e -> f -> g -> h infixl 1 #
Forces the 7th argument type.
(->>>>>>:) :: (a -> b -> c -> d -> e -> f -> g) -> g -> a -> b -> c -> d -> e -> f -> g infixl 1 #
Forces the result type of a 6-argument function.
(->>>>>:>) :: (a -> b -> c -> d -> e -> f -> g) -> f -> a -> b -> c -> d -> e -> f -> g infixl 1 #
Forces the 6th argument type.
(->>>>>:) :: (a -> b -> c -> d -> e -> f) -> f -> a -> b -> c -> d -> e -> f infixl 1 #
Forces the result type of a 5-argument function.
(->>>>:>) :: (a -> b -> c -> d -> e -> f) -> e -> a -> b -> c -> d -> e -> f infixl 1 #
Forces the 5th argument type.
(->>>>:) :: (a -> b -> c -> d -> e) -> e -> a -> b -> c -> d -> e infixl 1 #
Forces the result type of a 4-argument function.
(->>>:>) :: (a -> b -> c -> d -> e) -> d -> a -> b -> c -> d -> e infixl 1 #
Forces the 4th argument type.
(->>>:) :: (a -> b -> c -> d) -> d -> a -> b -> c -> d infixl 1 #
Type restricted version of const that forces the result of the result of the result of its first argument to have the same type as the second.
(->>:>) :: (a -> b -> c -> d) -> c -> a -> b -> c -> d infixl 1 #
Type restricted version of const that forces the third argument of its first argument to have the same type as the second.
(->>:) :: (a -> b -> c) -> c -> a -> b -> c infixl 1 #
Type restricted version of const that forces the result of the result of its first argument to have the same type as the second.
f ->>: ty = f -: und -> und -> ty = f :: a -> b -> Ty
(->:>) :: (a -> b -> c) -> b -> a -> b -> c infixl 1 #
Type restricted version of const that forces the second argument of its first argument to have the same type as the second.
f ->:> ty = f -: und -> ty -> und = f :: a -> Ty -> b
(->:) :: (a -> b) -> b -> a -> b infixl 1 #
Type restricted version of const that forces the result of its first argument to have the same type as the second.
f ->: ty = f -: und >- ty = f :: a -> Ty
(-:>) :: (a -> b) -> a -> a -> b infixl 1 #
Type restricted version of const that forces the argument of its first argument to have the same type as the second:
f -:> ty = f -: ty >- und = f :: Ty -> a
Example:
abs -:> int = abs -: int >- und = abs :: Int -> Int
(-:) :: a -> a -> a infixl 1 #
Type restricted version of const
that forces its first argument
to have the same type as the second.
A symnonym to asTypeOf
:
value -: ty = value :: Ty
Examples:
10 -: int = 10 :: Int undefined -: 'a' >- 'b' = undefined :: Char -> Char
Single-bit signed integers: -1, 0
Two-bit signed integers: -2, -1, 0, 1
Three-bit signed integers: -4, -3, -2, -1, 0, 1, 2, 3
Four-bit signed integers: -8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7
Single-bit unsigned integer: 0, 1
Two-bit unsigned integers: 0, 1, 2, 3
Three-bit unsigned integers: 0, 1, 2, 3, 4, 5, 6, 7
Four-bit unsigned integers: 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15
Natural numbers (including 0): 0, 1, 2, 3, 4, 5, 6, 7, ...
Internally, this type is represented as an Integer
allowing for an infinity of possible values.
Its Enum
and Listable
instances only produce non-negative values.
Negatives can still be generated by negate
or subtraction.
Instances
Enum Natural | |
Eq Natural | |
Integral Natural | |
Defined in Test.LeanCheck.Utils.Types | |
Num Natural | |
Ord Natural | |
Read Natural | |
Real Natural | |
Defined in Test.LeanCheck.Utils.Types toRational :: Natural -> Rational # | |
Show Natural | |
Listable Natural | |
Natural numbers (including 0): 0, 1, 2, 3, 4, 5, 6, 7, ...
Internally, this type is represented as an Int
.
So, it is limited by the maxBound
of Int
.
Natural numbers modulo 1: 0
Natural numbers modulo 2: 0, 1
Natural numbers modulo 3: 0, 1, 2
Natural numbers modulo 4: 0, 1, 2, 3
Natural numbers modulo 5: 0, 1, 2, 3, 4
Natural numbers modulo 6: 0, 1, 2, 3, 4, 5
Natural numbers modulo 7: 0, 1, 2, 3, 4, 5, 6
Lists without repeated elements.
> take 6 $ list :: [NoDup Nat] [NoDup [],NoDup [0],NoDup [1],NoDup [0,1],NoDup [1,0],NoDup [2]]
Example, checking the property that nub
is an identity:
import Data.List (nub) > check $ \xs -> nub xs == (xs :: [Int]) *** Failed! Falsifiable (after 3 tests): [0,0] > check $ \(NoDup xs) -> nub xs == (xs :: [Int]) +++ OK, passed 200 tests.
NoDup [a] |
Lists representing bags (multisets).
The Listable
tiers
enumeration will not have repeated bags.
> take 6 (list :: [Bag Nat]) [Bag [],Bag [0],Bag [0,0],Bag [1],Bag [0,0,0],Bag [0,1]]
See also: bagsOf
and bagCons
.
Bag [a] |
Lists representing sets.
The Listable
tiers
enumeration will not have repeated sets.
> take 6 (list :: [Set Nat]) [Set [],Set [0],Set [1],Set [0,1],Set [2],Set [0,2]]
Set [a] |
Lists of pairs representing maps.
The Listable
tiers
enumeration will not have repeated maps.
> take 6 (list :: [Map Nat Nat]) [Map [],Map [(0,0)],Map [(0,1)],Map [(1,0)],Map [(0,2)],Map [(1,1)]]
Map [(a, b)] |
X
type to be wrapped around integer types for an e-X
-treme integer
enumeration. See the Listable
instance for X
. Use X
when
testing properties about overflows and the like:
> check $ \x -> x + 1 > (x :: Int) +++ OK, passed 200 tests.
> check $ \(X x) -> x + 1 > (x :: Int) +++ Failed! Falsifiable (after 4 tests): 9223372036854775807
Wrap around lists of integers for an enumeration containing e-X
-treme
integer values.
> check $ \xs -> all (>=0) xs ==> sum (take 1 xs :: [Int]) <= sum xs +++ OK, passed 200 tests.
> check $ \(Xs xs) -> all (>=0) xs ==> sum (take 1 xs :: [Int]) <= sum xs *** Failed! Falsifiable (after 56 tests): [1,9223372036854775807]
Xs [a] |
(=|) :: Eq a => [a] -> Int -> [a] -> Bool infixl 4 #
Check if two lists are equal for n
values.
This operator has the same fixity of ==
.
xs =| n |= ys = take n xs == take n ys
[1,2,3,4,5] =| 2 |= [1,2,4,8,16] -- > True [1,2,3,4,5] =| 3 |= [1,2,4,8,16] -- > False
(=$) :: Eq b => a -> (a -> b) -> a -> Bool infixl 4 #
Equal under, a ternary operator with the same fixity as ==
.
x =$ f $= y = f x = f y
[1,2,3,4,5] =$ take 2 $= [1,2,4,8,16] -- > True [1,2,3,4,5] =$ take 3 $= [1,2,4,8,16] -- > False [1,2,3] =$ sort $= [3,2,1] -- > True 42 =$ (`mod` 10) $= 16842 -- > True 42 =$ (`mod` 9) $= 16842 -- > False 'a' =$ isLetter $= 'b' -- > True 'a' =$ isLetter $= '1' -- > False
neverIdentity :: Eq a => (a -> a) -> a -> Bool #
Is the given function never an identity? f x /= x
holds n $ neverIdentity not
fails n $ neverIdentity negate -- yes, fails: negate 0 == 0, hah!
Note: this is not the same as not being an identity.
identity :: Eq a => (a -> a) -> a -> Bool #
Is the given function an identity? f x == x
holds n $ identity (+0) holds n $ identity (sort :: [()]) holds n $ identity (not . not)
idempotent :: Eq a => (a -> a) -> a -> Bool #
Is the given function idempotent? f (f x) == x
holds n $ idempotent abs holds n $ idempotent sort
fails n $ idempotent negate
strictTotalOrder :: Eq a => (a -> a -> Bool) -> a -> a -> a -> Bool #
Is the given binary relation a strict total order?
totalOrder :: Eq a => (a -> a -> Bool) -> a -> a -> a -> Bool #
Is the given binary relation a total order?
strictPartialOrder :: (a -> a -> Bool) -> a -> a -> a -> Bool #
Is the given binary relation a strict partial order? Is the given relation irreflexive, asymmetric and transitive?
partialOrder :: Eq a => (a -> a -> Bool) -> a -> a -> a -> Bool #
Is the given binary relation a partial order? Is the given relation reflexive, antisymmetric and transitive?
equivalence :: (a -> a -> Bool) -> a -> a -> a -> Bool #
Is the given binary relation an equivalence? Is the given relation reflexive, symmetric and transitive?
> check (equivalence (==) :: Int -> Int -> Int -> Bool) +++ OK, passed 200 tests. > check (equivalence (<=) :: Int -> Int -> Int -> Bool) *** Failed! Falsifiable (after 3 tests): 0 1 0
Or, using Test.LeanCheck.Utils.TypeBinding:
> check $ equivalence (<=) -:> int *** Failed! Falsifiable (after 3 tests): 0 1 0
asymmetric :: (a -> a -> Bool) -> a -> a -> Bool #
Is a given relation asymmetric? Not to be confused with "not symmetric" and "antissymetric".
antisymmetric :: Eq a => (a -> a -> Bool) -> a -> a -> Bool #
Is a given relation antisymmetric? Not to be confused with "not symmetric" and "assymetric".
symmetric :: (a -> a -> Bool) -> a -> a -> Bool #
Is a given relation symmetric?
This is a type-restricted version of commutative
.
irreflexive :: (a -> a -> Bool) -> a -> Bool #
An element is never related to itself.
transitive :: (a -> a -> Bool) -> a -> a -> a -> Bool #
Is a given relation transitive?
symmetric2 :: Eq b => (a -> a -> b) -> (a -> a -> b) -> a -> a -> Bool #
Are two operators flipped versions of each other?
holds n $ (<) `symmetric2` (>) -:> int holds n $ (<=) `symmetric2` (>=) -:> int
fails n $ (<) `symmetric2` (>=) -:> int fails n $ (<=) `symmetric2` (>) -:> int
distributive :: Eq a => (a -> a -> a) -> (a -> a -> a) -> a -> a -> a -> Bool #
Does the first operator, distributes over the second?
associative :: Eq a => (a -> a -> a) -> a -> a -> a -> Bool #
Is a given operator associative? x + (y + z) = (x + y) + z
commutative :: Eq b => (a -> a -> b) -> a -> a -> Bool #
Is a given operator commutative? x + y = y + x
holds n $ commutative (+)
fails n $ commutative union -- union [] [0,0] = [0]
classifyOn :: Eq b => (a -> b) -> [a] -> [[a]] #
classifyBy :: (a -> a -> Bool) -> [a] -> [[a]] #
module Data.Typeable