<div dir="ltr">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 <a href="http://RoutingLib.Data.Matrix">RoutingLib.Data.Matrix</a>.<div><br></div><div>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!</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Jun 9, 2021 at 3:50 PM Manuel Bärenz <<a href="mailto:manuel@enigmage.de">manuel@enigmage.de</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><br>
> If I want to use dimension-safe matrix operations (on a type of<br>
> matrices parameterized by numbers of rows and columns, similar to<br>
> Vec), what is the good way?  Are there comprehensive libraries for<br>
> them already, probably?  I appreciate any information.<br>
You might want to look into<br>
<a href="https://github.com/ryanorendorff/functional-linear-algebra/" rel="noreferrer" target="_blank">https://github.com/ryanorendorff/functional-linear-algebra/</a> which is<br>
well-maintained and does your job, I believe.<br>
> Also, is the same (or similar) thing possible in Haskell (or even<br>
> OCaml)?  If so, information on Haskell (or OCaml) libraries is also<br>
> welcome.  Thank you in advance.<br>
You can do this (inefficiently) in Haskell using GADTs (and datakinds),<br>
since type-level natural numbers and fixed-length vectors can be<br>
implemented. Or you can do it efficiently but somewhat unsafely by<br>
encapsulating the types of your favourite linear algebra package in a<br>
newtype annotated with the assumed dimensions.<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>