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) Thanks, Levi
Hi Levi,
so that I can muck around with a Vector type that includes its length encoded in its type.
I suppose you have some operations over these vectors, such as nil :: Vec Zero a (|>) :: a -> Vec n a -> Vec (Succ n) a If so, you could write a SmallCheck Series instance as follows. instance Serial (Vec Zero a) where series = cons0 nil instance (Serial a, Serial (Vec n a)) => Serial (Vec (Succ n) a) where series = cons2 (|>) Let's assume the earlier ops are defined as data Vec n a = V [a] nil :: Vec Zero a nil = V [] (|>) :: a -> Vec n a -> Vec (Succ n) a x |> V xs = V (x:xs) If we have the property prop_vector :: Vec (Succ (Succ Zero)) Bool -> Bool prop_vector (V xs) = xs == xs we can check it, and only 2 element vectors will be tested: *Main> smallCheck 4 prop_vector Depth 0: Completed 0 test(s) without failure. Depth 1: Completed 0 test(s) without failure. Depth 2: Completed 4 test(s) without failure. Depth 3: Completed 4 test(s) without failure. Depth 4: Completed 4 test(s) without failure. Now, it seems what you really want to do is define polymorphic properties like prop_poly :: Vec n Bool -> Vec n Bool -> Bool and have SmallCheck check all equal-sized vectors. If so, good question! :-) Anybody else? Matt.
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)
It is also possible to reify type-level numbers with more context; I managed to get as far as (iirc)
reifyPos :: Integer -> (forall n. (Pos n, Succ n n', DivMod10 n nd nm) => n -> r) -> r
This way you can test head, tail e.g., but I found it to be a lot of work to write additional reifications. I do not know if it is possible (I think it is not) to have a reification which allows you to use total type level functions such as Add, e.g.
tylvl = reifyIntegral? k $ \(n :: ty) -> toInt (m :: Add ty D9) -- (D9 is the type level number 9)
I'm really curious what exactly would make this possible. best regards, benedikt
participants (3)
-
Benedikt Huber -
Levi Stephen -
Matthew