How to create quickcheck tests for dependently typed matrix addition without specifying each dimension statically?

Learn
3

I suggest to avoid “Some” wrappers and instead keep the size variables in scope.

test2 = generate $ do
  SomeNat @x _ <- arbitraryKnownNat
  SomeNat @y _ <- arbitraryKnownNat
  SomeNat @z _ <- arbitraryKnownNat
  m1 <- exampleThree @x @y @L2 @Diff
  m2 <- exampleThree @y @z @L2 @Diff
  pure $ (mult m1 m2) == (mult m1 m2)

Fulll code at: Generate matrices that can be added and multiplied · uvm-plaid/SensCheck@8312227 · GitHub

By the way, I appreciate you providing full source code. It made it much easier for me to know what to suggest. However, I couldn’t get the project to build with cabal because grenade’s dependencies on Hacakge are severely outdated. I’ve reported that at Adjust bounds by sorki · Pull Request #107 · HuwCampbell/grenade · GitHub

3 Likes