  Interested in formalizing the generation of fast running code for linear
algebra applications, 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 algorithms
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 extending other operations (e.g. Gaussian
elimination) blockwise, in a calculational style, is found. The prospect of
building biproduct-based type checkers for computer algebra systems such as
MatlabTM is also considered.
