Matrix math in Idris
Functional, lazy matrix arithmetic.
First install permutations. Then:
$ idris --install lazy_matrices.ipkg
Matrices are functions from natural numbers (i.e. indices) to some field. This library provides the usual facilities for manipulating them (inverses, adjoints, etc.), with the added benefit that multiplication is now type-safe.
This makes fusion trivial; for example, transposing a matrix twice will not allocate an intermediate matrix but rather compose functions.