Saturday, May 11, 2013

HASKELL QUICKCHECK

HASKELL QUICKCHECK

REVISED: Wednesday, January 24, 2024




Haskell QuickCheck.

I. TESTING HASKELL

A. PROPERTIES

QuickCheck is a tool for testing Haskell programs automatically. The programmer provides a specification of the program, in the form of properties which functions should satisfy, and QuickCheck then tests that the properties hold in a large number of randomly generated cases.

Properties are expressed as Haskell function definitions, with names beginning with prop_ A QuickCheck property is a function whose output is a Boolean.

The syntax is quickCheck <property-name>.

For example:

Prelude>  import Test.QuickCheck
Prelude>

Prelude>  let prop_RevRev xs = reverse (reverse xs) == xs
  where types = xs::[Int]
prop_RevRev :: [Int] -> Bool
Prelude>

Prelude>  quickCheck prop_RevRev
Loading package array-0.5.0.0 ... linking ... done.
Loading package deepseq-1.3.0.2 ... linking ... done.
Loading package bytestring-0.10.4.0 ... linking ... done.
Loading package Win32-2.3.0.2 ... linking ... done.
Loading package old-locale-1.0.0.6 ... linking ... done.
Loading package time-1.4.2 ... linking ... done.
Loading package random-1.0.1.1 ... linking ... done.
Loading package containers-0.5.5.1 ... linking ... done.
Loading package pretty-1.1.1.1 ... linking ... done.
Loading package template-haskell ... linking ... done.
Loading package QuickCheck-2.6 ... linking ... done.
+++ OK, passed 100 tests.
it :: ()
Prelude>  

An example of quickCheck finding an error is as follows:

Prelude>  let prop_RevId xs = reverse xs == xs
  where types = xs::[Int]
prop_RevId :: [Int] -> Bool
Prelude>

Prelude>  quickCheck prop_RevId
*** Failed! Falsifiable (after 5 tests and 4 shrinks): 
[0,1]
it :: ()
Prelude>  

If you want to see which values QuickCheck tried, use verbose. To do so repeat the test using:

verboseCheck <property-name>

Verbose displays each test case before running the test; therefore, the last test case displayed is the one in which the loop or error arises.

Prelude>  verboseCheck prop_RevId
Passed:
[]
Passed:
[]
Passed:
[]
Failed:
[-2,1]
*** Failed! Passed:
[]
Passed:
[1]
Passed:
[-2]
Failed:
[2,1]
Passed:
[]
Passed:
[1]
Passed:
[2]
Failed:
[0,1]
Passed:
[]
Passed:
[1]
Passed:
[0]
Passed:
[0,0]
Falsifiable (after 4 tests and 2 shrinks): 
[0,1]
it :: ()
Prelude>  

Properties may take the form <condition> ==> <property>

For example:

Prelude>  let ordered xs = and (zipWith (<=) xs (drop 1 xs))
ordered :: Ord b => [b] -> Bool
Prelude>

Prelude>  let insert x xs = takeWhile (<x) xs++[x]++dropWhile (<x) xs
insert :: Ord a => a -> [a] -> [a]
Prelude>

Prelude>  let prop_Insert x xs = ordered xs ==> ordered (insert x xs)
  where types = x::Int
prop_Insert :: Int -> [Int] -> Property
Prelude>

Prelude>  quickCheck prop_Insert
*** Gave up! Passed only 71 tests.
it :: ()
Prelude>  

Such a property holds if the property after ==> holds whenever the condition does.

Testing discards test cases which do not satisfy the condition. Test case generation continues until 100 cases which do satisfy the condition have been found, or until an overall limit on the number of test cases is reached, to avoid looping if the condition never holds. 

B. LIST COMPREHENSION VERSUS LIST COMPREHENSION

Prelude>  import Test.QuickCheck
Prelude>

Prelude>  let squares xs = [ x*x | x <- xs ]
squares :: Num t => [t] -> [t]
Prelude>

Prelude>  let odds xs = [x | x <- xs, odd x]
odds :: Integral t => [t] -> [t]
Prelude>

Prelude>  let sumSqOdd xs = sum [ x*x | x <- xs, odd x ]
sumSqOdd :: Integral a => [a] -> a
Prelude>

Prelude>  let prop_sumSqOdd xs = sum (squares (odds xs)) == sumSqOdd xs
prop_sumSqOdd :: Integral a => [a] -> Bool
Prelude>

Prelude>  quickCheck prop_sumSqOdd
Loading package bytestring-0.9.2.1 ... linking ... done.
Loading package Win32-2.2.2.0 ... linking ... done.
Loading package array-0.4.0.0 ... linking ... done.
Loading package deepseq-1.3.0.0 ... linking ... done.
Loading package old-locale-1.0.0.4 ... linking ... done.
Loading package time-1.4 ... linking ... done.
Loading package random-1.0.1.1 ... linking ... done.
Loading package containers-0.4.2.1 ... linking ... done.
Loading package pretty-1.1.1.0 ... linking ... done.
Loading package template-haskell ... linking ... done.
Loading package QuickCheck-2.5.1.1 ... linking ... done.
+++ OK, passed 100 tests.
Prelude>  

C. LIST COMPREHENSION VERSUS RECURSION EXAMPLE 1

"Copy Paste" the following into your text editor and "File, Save As" squaresQuickCheck.hs to your working directory:

squares :: [Integer] -> [Integer]
squares xs = [ x*x | x <- xs ]                       -- List Comprehension

squaresRec :: [Integer] -> [Integer]
squaresRec []          = []                                     -- Recursion
squaresRec (x:xs) = x*x : squaresRec xs

prop_squares :: [Integer] -> Bool
prop_squares xs = squares xs == squaresRec xs

Then open GHCi; import Test.QuickCheck; :load squaresQuickCheck; and run quickCheck prop_squares as shown below:

GHCi, version 9.8.1: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Prelude>

Prelude>  import Test.QuickCheck
Prelude>

Prelude>  :load squaresQuickCheck
[1 of 1] Compiling Main             ( squaresQuickCheck.hs, interpreted )
Ok, modules loaded: Main.
Prelude>

Prelude>  quickCheck prop_squares
Loading package bytestring-0.9.2.1 ... linking ... done.
Loading package Win32-2.2.2.0 ... linking ... done.
Loading package array-0.4.0.0 ... linking ... done.
Loading package deepseq-1.3.0.0 ... linking ... done.
Loading package old-locale-1.0.0.4 ... linking ... done.
Loading package time-1.4 ... linking ... done.
Loading package random-1.0.1.1 ... linking ... done.
Loading package containers-0.4.2.1 ... linking ... done.
Loading package pretty-1.1.1.0 ... linking ... done.
Loading package template-haskell ... linking ... done.
Loading package QuickCheck-2.5.1.1 ... linking ... done.
+++ OK, passed 100 tests.
it :: ()
Prelude> 

The above is QuickCheck's proof that the list comprehension function's output is the same as the recursive function's output.

D. LIST COMPREHENSION VERSUS RECURSION EXAMPLE 2

"Copy Paste" the following example into your text editor and then "File, Save As" oddsQuickCheck.hs to your working directory:

oddsComp :: [Integer] -> [Integer]
oddsComp xs = [ x | x <- xs, odd x ]                        -- List Comprehension

oddsRec :: [Integer] -> [Integer]
oddsRec []                                  = []                                  -- Recursion
oddsRec (x:xs) | odd x        = x : oddsRec xs
                          | otherwise = oddsRec xs

prop_odds :: [Integer] -> Bool
prop_odds xs = oddsComp xs == oddsRec xs

Then open GHCi; import Test.QuickCheck:load oddsQuickCheck; and run quickCheck prop_odds as shown below:

Prelude>  import Test.QuickCheck
Prelude>

Prelude>  :load oddsQuickCheck
[1 of 1] Compiling Main             ( oddsQuickCheck.hs, interpreted )
Ok, modules loaded: Main.
Prelude>

Prelude>  quickCheck prop_odds
+++ OK, passed 100 tests.
it :: ()
Prelude>  

The above is QuickCheck's proof that the list comprehension function's output is the same as the recursive function's output.

E. LIST COMPREHENSION VERSUS RECURSION EXAMPLE 3

"Copy Paste" the following example into your text editor and then "File, Save As" sumSqOddQuickCheck.hs to your working directory:

-- Comprehension
sumSqOddComp :: [Integer] -> Integer
sumSqOddComp xs = sum [ x*x | x <- xs, odd x ]

-- Recursion
sumSqOddRec :: [Integer] -> Integer
sumSqOddRec []                            = 0
sumSqOddRec (x:xs) | odd x        = x*x + sumSqOddRec xs
                                    | otherwise = sumSqOddRec xs
                   
-- QuickCheck
prop_sumSqOdd :: [Integer] -> Bool
prop_sumSqOdd xs = sumSqOddComp xs == sumSqOddRec xs

Then open GHCi; import Test.QuickCheck:load sumSqOddQuickCheck; and run quickCheck prop_sumSqOdd as shown below:

GHCi, version 9.8.1: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Prelude>

Prelude>  import Test.QuickCheck
Prelude>

Prelude>  :load sumSqOddQuickCheck
[1 of 1] Compiling Main             ( sumSqOddQuickCheck.hs, interpreted )
Ok, modules loaded: Main.
Prelude>

Prelude>  quickCheck prop_sumSqOdd
Loading package bytestring-0.9.2.1 ... linking ... done.
Loading package Win32-2.2.2.0 ... linking ... done.
Loading package array-0.4.0.0 ... linking ... done.
Loading package deepseq-1.3.0.0 ... linking ... done.
Loading package old-locale-1.0.0.4 ... linking ... done.
Loading package time-1.4 ... linking ... done.
Loading package random-1.0.1.1 ... linking ... done.
Loading package containers-0.4.2.1 ... linking ... done.
Loading package pretty-1.1.1.0 ... linking ... done.
Loading package template-haskell ... linking ... done.
Loading package QuickCheck-2.5.1.1 ... linking ... done.
+++ OK, passed 100 tests.
it :: ()
Prelude>  

The above is QuickCheck's proof that the comprehension function's output is the same as the recursive function's output.

F. RECURSION VERSUS CONDITIONAL

"Copy Paste" the following example into your text editor and "File, Save As" oddsCondQuickCheck.hs to your working directory:

oddsRec :: [Integer] -> [Integer]
oddsRec []                                  = []                                    -- Recursion
oddsRec (x:xs) | odd x          = x : oddsRec xs
                                | otherwise = oddsRec xs

oddsCond :: [Integer] -> [Integer]
oddsCond ws =                                                                    -- Conditional
    if null ws then
        []
    else
        let
            x = head ws
            xs = tail ws
        in
            if odd x then
                x : oddsCond xs
            else
                oddsCond xs

prop_oddsCond :: [Integer] -> Bool
prop_oddsCond xs = oddsRec xs == oddsCond xs


Then open GHCi; import Test.QuickCheck:load oddsCondQuickCheck; and run quickCheck prop_oddsCond as shown below:

GHCi, version 9.8.1: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Prelude>

Prelude>   import Test.QuickCheck
Prelude>

Prelude>  :load oddsCondQuickCheck
[1 of 1] Compiling Main             ( oddsCondQuickCheck.hs, interpreted )
Ok, modules loaded: Main.
Prelude>

Prelude>  quickCheck prop_oddsCond
Loading package bytestring-0.9.2.1 ... linking ... done.
Loading package Win32-2.2.2.0 ... linking ... done.
Loading package array-0.4.0.0 ... linking ... done.
Loading package deepseq-1.3.0.0 ... linking ... done.
Loading package old-locale-1.0.0.4 ... linking ... done.
Loading package time-1.4 ... linking ... done.
Loading package random-1.0.1.1 ... linking ... done.
Loading package containers-0.4.2.1 ... linking ... done.
Loading package pretty-1.1.1.0 ... linking ... done.
Loading package template-haskell ... linking ... done.
Loading package QuickCheck-2.5.1.1 ... linking ... done.
+++ OK, passed 100 tests.
it :: ()
Prelude> 

The above is QuickCheck's proof that the recursive function's output is the same as the conditional function's output.

G. TESTING A NUMBER THEORY PROPERTY

Consider a very simple property from number theory:

“For each integer n, if n is even, then n+1 is odd.”

We can validate this property using QuickCheck by asking it to generate random integers and test the property.

Prelude>  import Test.QuickCheck
Prelude>

Prelude>  quickCheck(\n -> even(n) ==> odd(n+1))
Loading package array-0.5.0.0 ... linking ... done.
Loading package deepseq-1.3.0.2 ... linking ... done.
Loading package bytestring-0.10.4.0 ... linking ... done.
Loading package Win32-2.3.0.2 ... linking ... done.
Loading package old-locale-1.0.0.6 ... linking ... done.
Loading package time-1.4.2 ... linking ... done.
Loading package random-1.0.1.1 ... linking ... done.
Loading package containers-0.5.5.1 ... linking ... done.
Loading package pretty-1.1.1.1 ... linking ... done.
Loading package template-haskell ... linking ... done.
Loading package QuickCheck-2.6 ... linking ... done.
+++ OK, passed 100 tests.
Prelude>

Haskell inferred that the type of n is Int.

It then invoked the function on 100 random integers, ensuring that each invocation satisfied the test.

II. REFERENCES

Bird, R. (2015). Thinking Functionally with Haskell. Cambridge, England: Cambridge University Press.

Davie, A. (1992). Introduction to Functional Programming Systems Using Haskell. Cambridge, England: Cambridge University Press.

Goerzen, J. & O'Sullivan, B. &  Stewart, D. (2008). Real World Haskell. Sebastopol, CA: O'Reilly Media, Inc.

Hutton, G. (2007). Programming in Haskell. New York: Cambridge University Press.

Lipovača, M. (2011). Learn You a Haskell for Great Good!: A Beginner's Guide. San Francisco, CA: No Starch Press, Inc.

Thompson, S. (2011). The Craft of Functional Programming. Edinburgh Gate, Harlow, England: Pearson Education Limited.

In this tutorial, you have received an introduction to Haskell QuickCheck.