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

[Matthew]

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.