[Agda] Dimension-safe matrix operations?

[Matthew Daggitt]

I'm not aware of any large scale matrix libraries in Agda. I have a very
small one in my own library for routing protocols which lies in the
directories underneath RoutingLib.Data.Matrix.

I've always been hesitant to add it to the standard library as I kind of
believe we should be leapfrogging it directly for `Tensor` but maybe I'm
sacrificing good on the altar of perfection!

On Wed, Jun 9, 2021 at 3:50 PM Manuel Bärenz <manuel at enigmage.de> wrote:

>
> > 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.
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210609/7ad6be23/attachment.html>