[Haskell-cafe] Re: (Lazy) SmallCheck and peano numbers

[Benedikt Huber]

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