Typing Linear Algebra: A Biproduct-oriented Approach

Interested in formalizing the generation of fast running code for linear algebra applica-tions, the authors show how an index-free, calculational approach to matrix algebra can be developed by regarding 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 biproduct equations makes it easy to calculate al-gorithms implementing matrix multiplication, the central operation of matrix algebra, ranging from its divide-and-conquer version to its vectorization implementation. From errant attempts to learn how particular products and coproducts emerge from biproducts, not only blocked matrix algebra is rediscovered but also a way of extend-ing other operations (e.g. Gaussian elimination) blockwise, in a calculational style, is found. The prospect of building biproduct-based type checkers for computer algebra sys-tems such as MATLAB ™ is also considered