SmallerCheck – Example for ES talk

SmallerCheck.hs

import Control.Parallel.Strategies (using, parBuffer, rseq)
import Data.List (partition)

-- *** Example Haskell functions ***

-- Is a list of integers sorted?
isOrdered :: [Int] -> Bool
isOrdered (x:y:zs) = x <= y && isOrdered (y:zs)
isOrdered _        = True

-- Sort a list of any orderable type.
qsort :: Ord a => [a] -> [a]
qsort [] = []
qsort (x:xs) = qsort ls ++ [x] ++ qsort rs
  where (ls, rs) = partition (<= x) xs
        
-- *** Bounded exhaustive testing library ***
        
-- Step 1: Type specification
depthTest :: Seriesable a => Depth -> Property a -> Result a

-- Step 2: Elaborate on types
type Depth = Int

data Result a = Pass | Fail a deriving Show

type Property a = a -> Bool

class Seriesable a where
  series :: Series a
  
type Series a = Depth -> [a]

-- Step 3: Define function
depthTest d prop = reduce tests
  where tests = [ if prop x then Pass
                            else Fail x
                | x <- series d ]
                
reduce :: [Result a] -> Result a
reduce []          = Pass
reduce (Pass  :xs) = reduce xs
reduce (Fail x:xs) = Fail x

-- Step 6: Building the generators
instance Seriesable Bool where
  series = cons False \/ cons True
  
instance Seriesable a => Seriesable [a] where
  series = cons [] \/ cons (:) >< series >< series
  
instance (Seriesable a, Seriesable b) 
         => Seriesable (a, b) where
  series = cons (,) >< series >< series

instance (Seriesable a, Seriesable b, Seriesable c) 
         => Seriesable (a, b, c) where
  series = cons (,,) >< series >< series >< series
  
instance Seriesable Int where
  series d = [negate d + 1 .. (d - 1)]

-- Step 5: Abstraction!
cons :: a -> Series a
cons x = \_ -> [x]

infixr 1 \/
(\/) :: Series a -> Series a -> Series a
xs \/ ys = \d -> xs d ++ ys d

infixl 2 ><
(><) :: Series (a -> b) -> Series a -> Series b
fs >< xs = \d -> [ f x | d > 1, f <- fs d, x <- xs (d - 1) ]

-- Step 8: Make it faster
parDepthTest d prop = reduce tests
  where tests = [ if prop x then Pass
                            else Fail x
                | x <- series d ]
                `using` parBuffer 20 rseq
                
-- *** Example tests ***
prop_sorted xs = isOrdered (qsort xs)

prop_implAssoc (x, y, z) = ((x <= y) <= z) == (x <= (y <= z))

isPrefix = undefined

isPrefixCOMPL :: [Int] -> [Int] -> [Int] -> Property
isPrefixSOUND xs ys xs'
  = (xs ++ xs' == ys) ==>
    (isPrefix xs ys)

isPrefixSOUND :: [Int] -> [Int] -> Property
isPrefixSOUND xs ys
  = (isPrefix xs ys) ==>
    (exists $ \xs' -> xs ++ xs' == ys)