Matrix math in Idris

root / README.md

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
# lazy_matrices

Functional, lazy matrix arithmetic.

## Installation

First install [permutations](https://github.com/vmchale/permutations). Then:

```bash
 $ 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.