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. 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? Is something like instance (forall n. Nat n) => Arbitrary n possible/legal haskell? and would it for the above test? > > best regards, > > benedikt > Thanks, Levi _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
