Test.StrictCheck.Examples.Lists

This module defines a variety of specifications for functions on lists, demonstrating the specification interface of StrictCheck. See the documentation of Test.StrictCheck (specifically strictCheckSpecExact) for details on how to test these specifications.

This module's primary utility is to teach how specifications work. Because Haddock omits the definitions of values, you'll learn the most by viewing the source of this module.

Specifying some simple functions on lists

length_spec :: Spec '[[a]] Int

A correct specification for length

take_spec_too_easy :: Spec '[Int, [a]] [a]

A naive specification for take, which is wrong

take_spec :: Spec '[Int, [a]] [a]

A correct specification for take

take' :: Int -> [a] -> [a]

A functionally correct implementation of take which has subtly different strictness properties

This will fail when tested against take_spec.

append_spec :: Shaped a => Spec '[[a], [a]] [a]

A correct specification of '(++)'

reverse_spec :: Shaped a => Spec '[[a]] [a]

A correct specification of reverse

zip_spec :: (Shaped a, Shaped b) => Spec '[[a], [b]] [(a, b)]

A correct specification for zip

zip' :: [a] -> [b] -> [(a, b)]

A functionally correct implementation of zip which has subtly different strictness properties

This will fail when tested against zip_spec.

map_spec :: forall a b. (Shaped a, Shaped b) => Spec '[a -> b, [a]] [b]

A correct specification for map, demonstrating specifications for higher-order functions

Specifying the productive rotate function from Okasaki's purely functional

rotate :: [a] -> [a] -> [a] -> [a]

Given three lists xs, ys, and zs, compute xs ++ reverse ys ++ zs, but with more uniform strictness

Specifically, if ys is shorter than xs, the work necessary to reverse it will have already occurred by the time xs is traversed.

rot :: [a] -> [a] -> [a]

Specialization of rotate: rot xs ys = rotate xs ys []

rot' :: [a] -> [a] -> [a]

The naive version of rot: rot' xs ys = xs ++ reverse ys

This is functionally equivalent to rot but not equivalent in strictness behavior.

rot_spec :: Shaped a => Spec '[[a], [a]] [a]

A previous iteration of rot_spec', this one is also correct, but may be less readable.

rot_spec' :: Shaped a => Spec '[[a], [a]] [a]

A correct specification of rot, this is also the version we presented in the paper.

rot_simple_spec :: Shaped a => Spec '[[a], [a]] [a]

An incorrect specification for rot that miscalculates the number of cells forced.

test_rot :: [Int] -> [Int] -> [Int] -> IO ()

Utilities for working with demands over lists

replaceThunk :: Shaped a => [a] -> [a] -> [a]

If the tail of the second list is thunk, replace it with the first list

cap :: Shaped a => [a] -> [a]

If the tail of the list is thunk, replace it with []

This is a special case of replaceThunk.

(%$) :: (Shaped a, Shaped b) => (a -> b) -> Demand a -> Demand b

Lift an ordinary function to apply to explicit Demands

It is true that Demands are a functor, but they can't be a Haskell Functor because they're a type family

(%*) :: (Shaped a, Shaped b) => Demand (a -> b) -> Demand a -> Demand b

Apply a Demand on a function to a Demand on a value

It is true that Demands are an applicative functor, but they can't be a Haskell Functor because they're a type family

specify1 :: forall a b. (Shaped a, Shaped b) => (a -> b) -> b -> a -> a

Given a unary function, an implicit demand on its result, and its input, compute its actual demand on its input in that context

This demand is calculated using observe1, so it is guaranteed to be correct.

toContext :: Shaped b => b -> b -> ()

Given an implicit demand, convert it to an evaluation context

That is, toContext d a evaluates a to the degree that d is a defined value. This uses the function evaluateDemand; refer to its documentation for details about how demands are used to evaluate values.

expectTotal :: Shaped a => a -> a

Assert at runtime that a value is not a thunk, failing with an error if it is