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

[Levi Stephen]

On Fri, Jun 20, 2008 at 3:30 AM, Benedikt Huber <benjovi at gmx.net> 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