> we put dimensions of data types on the type level to avoid a large set of errors that might arise at the runtime stage. During the compile stage, one may check some properties of matrix dimensions expressed via type-level natural numbers and find out the reason of that error as a type error.
> In this part, we describe our approach to the matrix data type that is parameterised via its numbers of columns and rows
> In this approach, matrix dimensions are lifted to the type level with the use of the Singletons library. At first glance, our solution looks a bit sophisticated. Why? There remains a question about the way to make it less devious and more idiomatic. In other words, we have to recognise the restrictions of Haskell expressive opportunities. What about performance? Also, our approach helps to remove only errors that affect the dimensions of arrays. Can we track other array parameters to reduce a set of possible runtime errors even more?
... not the horrible "singleton" design pattern https://en.wikipedia.org/wiki/Singleton_pattern
Prior art for identifying errors due to mismatched array dimensions include:
* (Eigen, C++) support for compile-time static assertions in some situations: https://eigen.tuxfamily.org/dox/TopicAssertions.html
* (numpy, python) raising ValueErrors at runtime about shape misalignment