trjhtr

I'm reading The Haskell Road to Logic, Math and Programming and for each exercise solution I write some properties to learn QuickCheck. One of the exercises is to write a function that sorts a list of strings (srtStr). I wonder if my properties are right. Also, is there something missing?

propIdempotent ∷ [String] → Bool
propIdempotent xs = srtStr xs == srtStr (srtStr xs)

propLength ∷ [String] → Bool
propLength str = length str == length (srtStr str)

propOrder ∷ [String] → Bool
propOrder xs = process (srtStr xs) True where
 process ∷ [String] → Bool → Bool
 process (x : y : xs) state = process xs (if state then x <= y else False)
 process _ state = state

check ∷ IO ()
check = do
 quickCheck propIdempotent
 quickCheck propLength
 quickCheck propOrder

Correctness of a sorting algorithm consists of showing that the resulting list is in order which your propOrder takes care of and that the resulting list is a permutation of the other list. Your propLength does the latter partially. It prevents you from adding or removing an element out of thin air but doesn't prevent you to replace one with another.

You can write a permutation checker as follows:

First define a subbag relation that is every element of the first list appears in the second.

isSubBag :: Eq a => [ a ] -> [ a ] -> Bool
isSubBag ys = True
isSubBag (x:xs) ys = x `elem` ys && isSubBag xs (delete x ys)

Then you can write a permutation checker by applying it both ways.

isPerm :: Eq a => [ a ] -> [ a ] -> Bool
isPerm xs ys = isSubBag xs ys && isSubBag ys xs

Your property comes out as:

propPerm :: [ String ] -> Bool
propPerm xs = isPerm xs (srtStr xs)

Overall, you can improve your process function by eliminating accumulator and using the built-in conjunction. Also a better name for it would be isInOrder

process :: [String] -> Bool
process (x : y : xs) = x <= y && process (y : xs)
process _ = True

One property that comes to mind is that applying any permutation before srtStr does not change the result. But what is a permutation? I'd say it's a function that doesn't exploit properties of the element type, has a left inverse and preserves the length. (The first ensures that only input elements are used. The second ensures that no elements can be dropped. The third ensures that there is no space for duplicated elements.)

propPermutationInvariant
 :: (forall a. [a] -> [a]) -> (forall a. [a] -> [a]) -> [String] -> Bool
propPermutationInvariant permutation inverse xs
 = length (permutation xs) /= length xs
 || inverse (permutation xs) /= xs
 || srtStr xs == srtStr (permutation xs)

For example, this implies srtStr xs == strStr (reverse xs), via propPermutationInvariant reverse reverse xs.

In addition to the other great answers, I'd like to point out a few details.

First, in your process function you skip too far, you need to go through elements one by one. Your code applied to [4, 5, 2, 3, 0, 1] passes. Rather you need to pattern match like this:

... process (x : xs@(y : _)) state = process xs (if state then x <= y else False)

Next, as pointed out in the comment, it's better to short-circuit if the property fails. It's more efficient and also more idiomatic in Haskell. Use an accumulator only if you need it. Something like this:

prop_order :: [String] -> Bool
prop_order (x : xs@(y : _)) = (x <= y) && prop_order xs
prop_order _ = property ()

Also note that (if state then x <= y else False) can be simplified to state && (x <= y).

Finally, I'd suggest you to express your property in such a way that you get more detailed information about what's wrong in a failing test. This can be accomplished using Property instead of Bool as the result type and using combinators in Test.QuickCheck.Property:

import Test.QuickCheck
import Test.QuickCheck.Property

-- | Tests if left is less or equal than right.
(<?=) :: (Ord a, Show a) => a -> a -> Property
x <?= y = counterexample (show x ++ " must be less than " ++ show y) (x <= y)

prop_order :: [String] -> Property
prop_order (x : xs@(y : _)) = (x <?= y) .&&. prop_order xs
prop_order _ = property ()

Note that operators (.&.) and (.&&.) are very different!

I'd probably prefer yet another variant using conjoin, which spares you of the explicit recursion. By zipping a list with its tail we get all consecutive pairs, and then we just express that each of such pairs must satisfy <?=.

prop_order2 :: [String] -> Property
prop_order2 xs = conjoin $ zipWith (<?=) xs (tail xs)