Matrices As Arrows! A Biproduct Approach to Typed Linear Algebra

Abstract. Motivated by the need to formalize generation of fast run-ning code for linear algebra applications, we show how an index-free, calculational approach to matrix algebra can be developed by regard-ing matrices as morphisms of a category with biproducts. This shifts the traditional view of matrices as indexed structures to a type-level perspective analogous to that of the pointfree algebra of programming. The derivation of fusion, cancellation and abide laws from the biprod-uct equations 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. From errant attempts to learn how particular products and coproducts emerge from biproducts, we not only rediscovered block-wise matrix com-binators but also found a way of addressing other operations calculation-ally such as e.g. Gaussian elimination. A strategy for addressing vector-ization along the same lines is also given.