Test.LeanCheck.Utils.TypeBinding

This module is part of LeanCheck, a simple enumerative property-based testing library.

Infix operators for type binding using dummy first-class values.

Those are useful when property based testing to avoid repetition. Suppose:

prop_sortAppend :: Ord a => [a] -> Bool
prop_sortAppend xs =  sort (xs++ys) == sort (ys++xs)

Then this:

testResults n =
  [ holds n (prop_sortAppend :: [Int] -> [Int] -> Bool)
  , holds n (prop_sortAppend :: [UInt2] -> [UInt2] -> Bool)
  , holds n (prop_sortAppend :: [Bool] -> [Bool] -> Bool)
  , holds n (prop_sortAppend :: [Char] -> [Char] -> Bool)
  , holds n (prop_sortAppend :: [String] -> [String] -> Bool)
  , holds n (prop_sortAppend :: [()] -> [()] -> Bool)
  ]

Becomes this:

testResults n =
  [ holds n $ prop_sortAppend -:> [int]
  , holds n $ prop_sortAppend -:> [uint2]
  , holds n $ prop_sortAppend -:> [bool]
  , holds n $ prop_sortAppend -:> [char]
  , holds n $ prop_sortAppend -:> [string]
  , holds n $ prop_sortAppend -:> [()]
  ]

Or even:

testResults n  =  concat
  [ for int, for uint2, for bool, for (), for char, for string ]
  where  for a  =  [ holds n $ prop_sortAppend -:> a ]

This last form is useful when testing multiple properties for multiple types.

Type binding operators

Summary:

• as type of: -:
• argument as type of: -:>
• result as type of: ->:
• second argument as type of: ->:>
• second result as type of: ->>:
• third argument as type of: ->>:>
• third result as type of: ->>>:

(-:) :: 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

(-:>) :: (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 -> 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 -> 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 -> 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 -> 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 -> 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 -> e) -> d -> a -> b -> c -> d -> e infixl 1

Forces the 4th 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 -> f) -> e -> a -> b -> c -> d -> e -> f infixl 1

Forces the 5th 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 -> g) -> f -> a -> b -> c -> d -> e -> f -> g infixl 1

Forces the 6th 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 -> h) -> g -> a -> b -> c -> d -> e -> f -> g -> h infixl 1

Forces the 7th 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 -> 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 -> 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 -> 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 -> 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 -> 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 -> 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 -> 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 -> 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 -> 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 -> 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.

Dummy (undefined) values

Standard Haskell types

und :: a

Shorthand for undefined

(>-) :: 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

bool :: Bool

Undefined Bool value.

int :: Int

Undefined Int value for use with type binding operators.

check $ (\x y -> x + y == y + x) ->:> int

integer :: Integer

Undefined Integer value for use with type binding operators.

check $ (\x y -> x + y == y + x) ->:> integer

float :: Float

Undefined Float value for use with type binding operators.

double :: Double

Undefined Double value for use with type binding operators.

rational :: Rational

Undefined Rational value for use with type binding operators.

char :: Char

Undefined Char value.

string :: String

Undefined String value.

ordering :: Ordering

Undefined Ordering value.

mayb :: a -> Maybe a

Undefined Maybe value. Uses the type of the given value as the argument type. For use with type binding operators.

To check a property with the first argument bound to Maybe Int, do:

check $ prop -:> mayb int

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.

Testing types

natural :: Natural

Undefined Natural value.

nat :: Nat

Undefined Nat value.

int1 :: Int1

Undefined Int1 value.

int2 :: Int2

Undefined Int2 value.

int3 :: Int3

Undefined Int3 value.

int4 :: Int4

Undefined Int4 value.

word1 :: Word1

Undefined Word1 value.

word2 :: Word2

Undefined Word2 value.

word3 :: Word3

Undefined Word3 value.

word4 :: Word4

Undefined Word4 value.

Deprecated testing types

uint1 :: UInt1

Deprecated. Use word1.

uint2 :: UInt2

Deprecated. Use word2.

uint3 :: UInt3

Deprecated. Use word3.

uint4 :: UInt4

Deprecated. Use word4.