[Haskell-cafe] Re: (Lazy) SmallCheck and peano numbers
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
[Haskell-cafe] Re: (Lazy) SmallCheck and peano numbers
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: (Lazy) SmallCheck and peano numbers
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 (|) 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 I have some code up now at http://hpaste.org/8420 It looks pretty much like what you've written above and is what I am doing for the moment, but for various size vectors from zero to four. 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! :-) Yep, this would be exactly what I'm after. Thanks for a better write up and background on what I'm after than I gave :) I'm thinking the property might be written as prop_poly:: size - Vec size Bool - Vec size Bool - Bool, so that the size is generated randomly and the types take care of ensuring the vectors generated are of the same size. Levi ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: (Lazy) SmallCheck and peano numbers
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
