Reimagining matrices
to make strange things settled, so much as
to make settled things strange.
- G.K. Chesterton
Why is matrix multiplication defined so very differently from matrix addition? If we didn’t know these procedures, could we derive them from first principles? What might those principles be?
This post gives a simple semantic model for matrices and then uses it to systematically derive the implementations that we call matrix addition and multiplication. The development illustrates what I call “denotational design”, particularly with type class morphisms. On the way, I give a somewhat unusual formulation of matrices and accompanying definition of matrix “multiplication”.
For more details, see the linear-map-gadt source code.
Edits:
- 2012–12–17: Replaced lost entries in description of matrix addition. Thanks to Travis Cardwell.
- 2012–12018: Added note about math/browser compatibility.
Note: I’m using MathML for the math below, which appears to work well on Firefox but on neither Safari nor Chrome. I use Pandoc to generate the HTML+MathML from markdown+lhs+LaTeX. There’s probably a workaround using different Pandoc settings and requiring some tweaks to my WordPress installation. If anyone knows how (especially the WordPress end), I’d appreciate some pointers.