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

[Benedikt Huber]

Levi Stephen schrieb:
> On Fri, Jun 20, 2008 at 3:30 AM, Benedikt Huber <benjovi at gmx.net> wrote:
>> Levi Stephen schrieb:
>>> Hi,
>>>
>>> I have the following definitions
>>>
>>> type Zero
>>> type Succ a
>>>
>>> so that I can muck around with a Vector type that includes its length
>>> encoded in its type.
>>>
>>> I was wondering whether it was possible to use SmallCheck (or
>>> QuickCheck) to generate random Peano numbers? Is there an issue here
>>> in that what I actually want to generate is a type rather than a
>>> value?
>>>
>>> I do have
>>>
>>> reifyInt :: Int -> (forall a. ReflectNum a => a -> b) -> b
>>>
>>> but, I'm not sure if this can help me when I need to generate other
>>> values based upon that type (e.g., two vectors with the same size
>>> type)
>> Hi Levi,
>>
>> For QuickCheck, I know it is possible as long as you do not need to use type
>> level functions in your tests. For example, using Alfonso's type-level and
>> parametrized-data packages, one can write:
>>
>>> instance (Nat n, Arbitrary a) => Arbitrary (FSVec n a) where
>>>    arbitrary =
>>>      liftM (unsafeVector (undefined :: n)) $
>>>        mapM (const arbitrary) [1..toInt (undefined :: n)]
>>> propLength :: forall n a. (Nat n) => FSVec n Integer -> Bool
>>> propLength (FSVec xs) = P.length xs == toInt (undefined :: n)
>>> propLengthEqual :: forall n a. (Nat n) =>
>>>                    FSVec n Integer -> FSVec n Integer -> Bool
>>> propLengthEqual v1 v2 = length v1 == length v2
>>> tests1 = forM_ [0..100] $ \n -> reifyIntegral n $ \(t :: ty) ->
>>>    quickCheck (propLength :: FSVec ty Integer -> Bool)
>>> tests2 = forM_ [0..100] $ \n -> reifyIntegral n $ \(t :: ty) ->
>>>    quickCheck (uncurry propLengthEqual ::
>>>                     (FSVec ty Integer,FSVec ty Integer) -> Bool)
> 
> Thanks for the example code. Ideally it would be great to have n generated also.

Generating n isn't hard, in IO above you could just use Random.
But I assume you want to use QuickCheck, so see below.

> Any thoughts on whether something like
> 
> propLengthEqual :: forall n a. (Nat n) => n -> FSVec n Integer ->
> FSVec n Integer -> Bool
> propLengthEqual _ v1 v 2 = length v1 == length v2
> 
> with an arbitrary instance for generate all Nat n's is possible?

propLengthEqual is exactly the same as propLength, I just left out the 
first argument (it is redundant).

You cannot use an `Arbitrary' instance to generate some type level 
number, at least not in the same way as for ordinary numbers.

What you can do is introduce an existential type

 > data SomeNat = forall n. (Nat n) => SomeNat Int n
 > instance Show SomeNat where show (SomeNat value typ) = show value

 > instance Arbitrary SomeNat where
 >    arbitrary = sized $ \n -> reifyIntegral n (return . SomeNat n)


If you look into the QuickCheck source, you'll find that a property
is a result generator: newtype Property = Prop (Gen Result)

So a property can be written as a result generator:

 > propLength' :: SomeNat -> Gen Result
 > propLength' (SomeNat vn (n :: t)) = do
 >    (vector :: FSVec t Integer) <- arbitrary
 >    buildResult [show vn , show vec] $ propLength vector

--
What follows next is the neccessary boilerplate to have a working example
----
 > buildResult :: [String] -> Bool -> Gen Result
 > buildResult args b = evaluate b >>= \r ->
 >    return $ r { arguments = show args : arguments r}
 > natProp :: (SomeNat -> Gen Result) -> Property
 > natProp f = flip forAll id $ do
 >    (k::Int) <- choose (0,10)
 >    n <- resize k arbitrary
 >    f n
 > deriving instance Show Result
----

Finally, run the tests

 > tests = verboseCheck (natProp propLength')

Hope that helps.


best regards, benedikt