[Agda] Dimension-safe matrix operations?

[Manuel Bärenz]

> If I want to use dimension-safe matrix operations (on a type of
> matrices parameterized by numbers of rows and columns, similar to
> Vec), what is the good way?  Are there comprehensive libraries for
> them already, probably?  I appreciate any information.
You might want to look into
https://github.com/ryanorendorff/functional-linear-algebra/ which is
well-maintained and does your job, I believe.
> Also, is the same (or similar) thing possible in Haskell (or even
> OCaml)?  If so, information on Haskell (or OCaml) libraries is also
> welcome.  Thank you in advance.
You can do this (inefficiently) in Haskell using GADTs (and datakinds),
since type-level natural numbers and fixed-length vectors can be
implemented. Or you can do it efficiently but somewhat unsafely by
encapsulating the types of your favourite linear algebra package in a
newtype annotated with the assumed dimensions.