CIS 5520

This problem is designed to give you practice with property-based testing and to give you experience with a cleverly designed purely functional data structure.

> module Queue where

You should use QuickCheck to test this module. If you want to use additional operations from the Haskell base libraries to complete this problem, you may import them here. You may also use any function from the Prelude without importing it.

> import Test.QuickCheck (Arbitrary(..), Property(..), (==>),quickCheckAll)
> import qualified Test.QuickCheck as QC
> import qualified Data.Foldable
> 
> import Data.List (uncons)

In this problem, you will implement a purely functional queue data structure. Queues store an unbounded sequence of elements and provide access to them in a first-in-first out (FIFO) order.

First, we specify this data structure using the following interface: a type, for queues, called Q a, that is parameterized by some type a, the type of elements stored in the queue.

      type Q a

And the following values and operations that the queue type should support:

empty    :: Q a                       -- a queue with no elements
lengthQ  :: Q a -> Int                -- return number of elements in the queue
enq      :: Q a -> a -> Q a           -- add element to back of the queue
peek     :: Q a -> Maybe a            -- look at the front of the queue
deq      :: Q a -> Maybe (a, Q a)     -- remove element from front of queue and return it
toList   :: Q a -> [a]                -- make a list from a queue
fromList :: [a] -> Q a                -- make a queue from a list

Note that these operations are pure functions, meaning that they do not have any side effects. In other words, functions such as enq and deq do not modify the queue passed in as input --- instead they return a new queue as output.

For example, suppose we have the following sequence of queue operations.

> -- sample queues
> q1, q2, q3, q4 :: Q Int
> q1 = enq empty 1
> q2 = enq q1 3
> q3 = enq q2 5
> Just (_, q4) = deq q3

We can look at the queue created at each step of the way: even though we construct q2 by adding the element 3 to the end of the q1, we always have access to the queue without this value. (These inline tests won't work until you finish the implementation of the data structure.)

> -- >>> toList q1
> -- [1]

> -- >>> toList q2
> -- [1,3]

> -- >>> toList q3
> -- [1,3,5]

> -- >>> toList q4
> -- [3,5]

> -- 1 - Queue Properties

Define at least five properties that your queue should satisfy, along with a descriptive comment that describes the property being tested. (You may want to define more than five to make sure that you are exhaustively testing your implementation below, but five is the miniumum number we are looking for.) Each operation above should be tested in at least one of your properties. Note: even though the queue is polymorphic, make sure that your properties are monomorphic. Also make sure that the name of each property that you define starts with the characters prop_. That way the call to quickCheckAll at the end of the file will automatically all of your properties on your implementation.

> -- 2 - Queue Representation and Validity

The properties that you defined in the previous problem should hold for any correct implementation of the queue interface.

Next, we will turn to a specific implementation of this interface and define the data structure that we will use to implement Queues.

The implementation that you will define is called a "Banker's Queue" and was created by Chris Okasaki.

The key feature of this implementation is that both the enq and deq operations can be performed in amortized constant time. This means that if you perform a sequence of n operations, the total time to perform all of those operations will be proportional to n.

To achieve this running time, the Banker's queue implementation uses two lists to implement the queue. Those lists represent the front and back parts of the queue. The back part of the queue is stored in reverse order, so that we can efficiently add elements to the back of the queue.

In addition to these two lists, the queue also keeps track of the number of elements in each list.

> data Q a  =  Q { nfront :: Int , front :: [a] , 
>                  nback  :: Int , back  :: [a] } deriving (Show)

At some time, the implementation must move elements from the back list to the front list, which takes time proportional to the number of elements that are moved. To make the amortized analysis work out, this data structure maintains the invariant that the length of the front list is always greater than or equal to the length of the back list. Each element is moves from the back list to the front list exactly once,

In other words, all valid queues satisfy the following property:

> -- | representation invariant for the Banker's queue
> prop_valid :: Q a -> Bool
> prop_valid q = 
>    nfront q == length (front q) 
>    && nback q == length (back q)
>    && nfront q >= nback q

This invariant means that if the front list is empty, then there are no elements in the queue.

For this part, define three distinct sample queues, each containing exactly the characters 'a', 'b', 'c', 'd' in order, that satisfy the invariant above. Then define three distinct queues, also containing exactly those characters in order, that do not satisfy the invariant.

> -- three good queues containing the sequence 'a', 'b', 'c' and 'd', in order
> good4 :: [ Q Char ]
> good4 = undefined

> -- >>> all prop_valid good4

> -- three bad queues containing the sequence 'a', 'b', 'c' and 'd', in order
> bad4 :: [ Q Char ]
> bad4 = undefined

> -- >>> not (any prop_valid bad4)

> -- 3 - Queue invariants

Your queue operations that produce new queues as output should also maintain the invariant above. Complete the last two properties that ensure that this is the case.

> -- | empty queue is valid
> prop_empty_valid :: Bool
> prop_empty_valid = prop_valid empty

> -- | enq produces a valid queue, when given a valid queue
> prop_enq_valid :: Int -> Q Int -> Property
> prop_enq_valid x q = prop_valid q ==> prop_valid (enq q x)

> -- | deq produces a valid queue, when given a valid queue
> prop_deq_valid :: Q Int -> Property
> prop_deq_valid = undefined

> -- | from list produces a valid queue
> prop_fromList_valid :: [Int] -> Bool
> prop_fromList_valid = undefined

> -- 4 - Arbitrary Instance

To be able to use QuickCheck to test your queue implementation below, you will need to first construct an instance of the Arbitrary type class to generate a random queue.

Make an Arbitrary instance for the Q type above, including definitions for both arbitrary and shrink. Your arbitrary definition should generate a queue that contains random data of random length. In your implementation, you should not use any of the queue operations (such as toList or enq). That way you will be able to test your generator before implementing these operations.

To make sure that your generator produces queues of different sizes, it should use the sized combinator from the QuickCheck library. (We have done this for you below.) And, to ensure that your generated queue sastisfies the invariant above, you should use the following operations from the QuickCheck library:

        chooseInt :: (Int, Int) -> Gen Int
        vectorOf :: Int -> Gen a -> Gen [a]

You can use simple tests to see what these operations do.

> -- >>> QC.sample' (QC.chooseInt (0, 23))

> -- >>> QC.sample' (QC.vectorOf 3 (arbitrary :: QC.Gen Int))

After you implement arbitrary, you can also use sample' to see what queues are generated.

> -- >>> take 3 <$> QC.sample' (arbitrary :: QC.Gen (Q Int))

You will also need to define a shrink operation. This operation should return valid queues that are "smaller" than the provided argument. A queue is "smaller" than the input if the front list is smaller, if the back list is smaller, and/or if the elements that it contains are smaller. Your implementation of shrink should return examples of all of these kinds of smaller queues, but does not need to return all smaller queues.

For example, shrinking this queue:

> -- >>> shrink  Q {nfront = 2, front = [0,2], nback = 1, back = [0]}

might produce these queues (among others)

 Q {nfront = 1, front = [2], nback = 1, back = [0]}   -- shrink front list
 Q {nfront = 1, front = [0], nback = 1, back = [0]}   -- shrink front list a different way
 Q {nfront = 2, front = [0,2], nback = 0, back = []}  -- shrink back list
 Q {nfront = 0, front = [], nback = 0, back = []}     -- shrink front & back list
 Q {nfront = 2, front = [0,1], nback = 1, back = [0]} -- shrink element in front list

Note that shrinking should not produce this queue because, even though it is smaller than the input, it violates the representation invariant.

 Q {nfront = 0, front = [], nback = 1, back = [0]}

> instance Arbitrary a => Arbitrary (Q a) where
>    arbitrary :: Arbitrary a => QC.Gen (Q a)
>    arbitrary = QC.sized gen where
>       gen :: Int -> QC.Gen (Q a)
>       gen = undefined
>    shrink :: Arbitrary a => Q a -> [Q a]
>    shrink = undefined

At this point make sure that you run QuickCheck on your definitions of arbitrary and shrink to make sure that you produce valid queues.

> -- | check that all generated queues are valid
> prop_arbitrary :: Q Int -> Bool
> prop_arbitrary = prop_valid

> -- | check that all shrunk queues are valid
> prop_shrink :: Q Int -> Bool
> prop_shrink q = all prop_valid (shrink q)

Recall that you can run QuickCheck in the terminal by first starting stack ghci src/Queue.hs:

    ghci> import qualified Test.QuickCheck as QC
    ghci> QC.quickCheck prop_arbitrary
    +++ OK, passed 100 tests.
    ghci> QC.quickCheck prop_shrink
    +++ OK, passed 100 tests.

> -- 5 - Implementation

Next, implement the queue operations, making sure that they satisfy all of the properties above. You can test individual properties in ghci in the terminal using the QC.quickCheck function. You can also call the main function in the terminal to run QuickCheck with all properties defined in this file. (See the end of the file for the definition of main.)

> -- | queue with no elements
> empty    :: Q a                       
> empty = undefined

> -- | number of elements in the queue
> lengthQ  :: Q a -> Int                
> lengthQ = undefined

> -- | access the first element in the queue (if there is one)
> peek     :: Q a -> Maybe a            
> peek = undefined

> -- | make a queue from a list
> fromList :: [a] -> Q a  
> fromList = undefined

> -- | access all of the elements in the queue
> toList   :: Q a -> [a]   
> toList = undefined

> -- | add element to back of the queue
> enq      :: Q a -> a -> Q a      
> enq = undefined

> -- | remove element from front of queue and return it along with shorter queue
> deq      :: Q a -> Maybe (a, Q a)
> deq = undefined

> -- Benchmarks: Try out Queue Performance

At this point, if your queue is correct you should be able to observe that it runs with the appropriate running time.

For example, constructing a queue using a sequence of enq operations should take time proportional to the number of enqs.

> bench1_Q :: Int -> Int
> bench1_Q m = last (toList q) where
>  q :: Q Int
>  q = foldl enq empty [0 .. m]

    ghci> bench1_Q 1000
    1000
    (0.01 secs, 1,548,232 bytes)
    ghci> bench1_Q 10000
    10000
    (0.03 secs, 12,591,176 bytes)
    ghci> bench1_Q 100000
    100000
    (0.18 secs, 122,987,056 bytes)

However, to use a list as a queue, we can deq efficiently, but we need to enq using (++).

> deqList :: [a] -> Maybe (a,[a])
> deqList (x:xs) = Just (x,xs)
> deqList [] = Nothing

> enqList :: [a] -> a -> [a]
> enqList x y = x ++ [y]

> bench1_list :: Int -> Int
> bench1_list m = last q where
>  q :: [ Int ]
>  q = foldl enqList [] [0 .. m]

With a list based queue, the same benchmark above is quadratic in the number of elements added to the queue.

    ghci> bench1_list 1000
    1000
    (0.01 secs, 28,548,608 bytes)
    ghci> bench1_list 10000
    10000
    (0.82 secs, 4,295,079,496 bytes)
    ghci> bench1_list 100000
    100000
    (129.76 secs, 444,480,765,552 bytes)

> -- Running QuickCheck

The hw03.cabal file enables the TemplateHaskell language extension. With this feature, the following code below defines an operation that will invoke QuickCheck with all definitions that start with prop_ above. This code must come after all of the definitions above (and runTests is not in scope before this point).

> return []
> runTests :: IO Bool
> runTests = $quickCheckAll

> main :: IO ()
> main = do
>   _ <- runTests
>   return ()

CIS 5520: Advanced Programming

Fall 2024