[Haskell-cafe] (Lazy) SmallCheck and peano numbers
Matthew
mfn-haskell-cafe at cs.york.ac.uk
Thu Jun 19 12:50:12 EDT 2008
Hi Levi,
> so that I can muck around with a Vector type that includes its length
> encoded in its type.
I suppose you have some operations over these vectors, such as
nil :: Vec Zero a
(|>) :: a -> Vec n a -> Vec (Succ n) a
If so, you could write a SmallCheck Series instance as follows.
instance Serial (Vec Zero a) where
series = cons0 nil
instance (Serial a, Serial (Vec n a)) => Serial (Vec (Succ n) a) where
series = cons2 (|>)
Let's assume the earlier ops are defined as
data Vec n a = V [a]
nil :: Vec Zero a
nil = V []
(|>) :: a -> Vec n a -> Vec (Succ n) a
x |> V xs = V (x:xs)
If we have the property
prop_vector :: Vec (Succ (Succ Zero)) Bool -> Bool
prop_vector (V xs) = xs == xs
we can check it, and only 2 element vectors will be tested:
*Main> smallCheck 4 prop_vector
Depth 0:
Completed 0 test(s) without failure.
Depth 1:
Completed 0 test(s) without failure.
Depth 2:
Completed 4 test(s) without failure.
Depth 3:
Completed 4 test(s) without failure.
Depth 4:
Completed 4 test(s) without failure.
Now, it seems what you really want to do is define polymorphic
properties like
prop_poly :: Vec n Bool -> Vec n Bool -> Bool
and have SmallCheck check all equal-sized vectors. If so, good
question! :-)
Anybody else?
Matt.
More information about the Haskell-Cafe
mailing list