QuickCheck tests for dependent types

Question

I am writing Vector and Matrix data types that are dependently typed.

data Vector n e where
  EmptyVector :: Vector Zero e
  (:>)        :: e -> Vector n e -> Vector (Succ n) e

deriving instance Eq e => Eq (Vector n e)

infixr :>

data Matrix r c e where
  EmptyMatrix :: Matrix Zero c e
  (:/)        :: Vector c e -> Matrix r c e -> Matrix (Succ r) c e

deriving instance Eq e => Eq (Matrix r c e)

infixr :/

They depend on the natural numbers, also a type.

data Natural where
    Zero :: Natural
    Succ :: Natural -> Natural

I have written a function to calculate the number of columns in a matrix.

columns :: Matrix r c e -> Int
columns m = Fold.foldr (\_ n -> 1 + n) 0 $ getRow 0 m

getRow :: Int -> Matrix r c e -> Vector c e
getRow 0 (v :/ _)    = v
getRow i (_ :/ m)    = getRow (i - 1) m
getRow _ EmptyMatrix = error "Cannot getRow from EmptyMatrix."

I would now like to test the columns function using QuickCheck.

To do this, I have to declare Matrix and Vector as instances of the Arbitrary type class provided by QuickCheck.

However, I'm at a loss as to how to do this.

• Does the fact that my data is dependently typed affect how I write these instances?

• How do I generate matrices of arbitrary length, ensuring that they match their definitions (eg. (Succ (Succ r)) will have two rows)?

Isherwood

Answer 1

You can write an instances for a certain length known at compile-time:

instance Arbitrary (Vector Zero e) where
    arbitrary = return EmptyVector

instance (Arbitrary e, Arbitrary (Vector n e))
    => Arbitrary (Vector (Succ n) e) where
    arbitrary = do
      e <- arbitrary
      es <- arbitrary
      return (e :> es)

By themselves, the above instances aren't very useful unless you want to write one expression for each length you want to try (or get template-haskell to generate those expressions). One way to get an Int to decide what the type n should be is to hide the n in an existential:

data BoxM e where
    BoxM :: Arbitrary (Vector c e) => Matrix r c e -> BoxM e

data Box e where Box :: Arbitrary (Vector c e) => Vector c e -> Box e

addRow :: Gen e -> BoxM e -> Gen (BoxM e)
addRow mkE (BoxM es) = do
    e <- mkE
    return $ BoxM (e :/ es)

firstRow :: Arbitrary a => [a] -> BoxM a
firstRow es = case foldr (\e (Box es) -> Box (e :> es)) (Box EmptyVector) es of
    Box v -> BoxM (v :/ EmptyMatrix)

With addRow and firstRow, it should be pretty straightforward to write a mkBoxM :: Int -> Int -> Gen (BoxM Int), and then use it like:

forAll (choose (0,3)) $ \n -> forAll (choose (0,3)) $ \m -> do
      BoxM matrix <- mkBoxM n m
      return $ columns matrix == m -- or whatever actually makes sense

Manned