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.

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

int :: Int

integer :: Integer

float :: Float

double :: Double

char :: Char

string :: String

mayb :: a -> Maybe a

It might be better to just use Just

eith :: a -> b -> Either a b

Testing types

nat :: Nat

int1 :: Int1

uint1 :: UInt1

int2 :: Int2

uint2 :: UInt2

int3 :: Int3

uint3 :: UInt3

int4 :: Int4

uint4 :: UInt4