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

Levi Stephen schrieb:

On Fri, Jun 20, 2008 at 3:30 AM, Benedikt Huber 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