Resumo: Motivated by the need to formalise generation of fast running
code for linear algebra applications, we show how an index-free,
calculational approach to matrix algebra can be developed by regarding
matrices as morphisms of a category with biproducts and its
self-adjoint functors. This shift, in the traditional view of matrices
as indexed structures to a type-level perspective analogous to that of
the pointfree algebra of programming, makes it easy to calculate
algorithms implementing matrix multiplication, the kernel operation of
matrix algebra, ranging from its divide-and-conquer version to the
conventional, iterative one and several vectorised variations. |