[Haskell-cafe] Re: (Lazy) SmallCheck and peano numbers

[Levi Stephen]

> 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 (|>)

> 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

I have some code up now at http://hpaste.org/8420

It looks pretty much like what you've written above and is what I am
doing for the moment, but for various size vectors from zero to four.


> 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! :-)

Yep, this would be exactly what I'm after. Thanks for a better write
up and background on what I'm after than I gave :)

I'm thinking the property might be written as

prop_poly:: size -> Vec size Bool -> Vec size Bool -> Bool,

so that the size is generated randomly and the types take care of
ensuring the vectors generated are of the same size.

Levi