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)?
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
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With