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
