lazy_matrices

Functional, lazy matrix arithmetic.

Installation

First install permutations. Then:

 $ idris --install lazy_matrices.ipkg

Use

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.