Levi Stephen schrieb:
On Fri, Jun 20, 2008 at 3:30 AM, Benedikt Huber <[EMAIL PROTECTED]> 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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
