[Haskell-cafe] Re: (Lazy) SmallCheck and peano numbers
Benedikt Huber
benjovi at gmx.net
Thu Jun 19 14:00:50 EDT 2008
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
More information about the Haskell-Cafe
mailing list