[Haskell-cafe] Re: (Lazy) SmallCheck and peano numbers
Benedikt Huber
benjovi at gmx.net
Fri Jun 20 03:37:41 EDT 2008
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
More information about the Haskell-Cafe
mailing list