search

agda / agda-stdlib

The Agda standard library
https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary
Other
579 stars 237 forks source link

Add `Data.Matrix` #1526

Open MatthewDaggitt opened 3 years ago

MatthewDaggitt commented 3 years ago

It would be a great to have matrices in the standard library. In https://github.com/agda/agda-stdlib/pull/1525 I opened a small PR with a very simple implementation of Data.Matrix. Thanks to a valuable discussion with @jespercockx and @JacquesCarette I came to realise it was a far bigger project than I have time to tackle so the PR was abandoned.

Anyone else keen to add Data.Matrix should read the discussion first for some valuable tips!

Taneb commented 3 years ago

I was working on something similar a few months ago, my work in progress is at https://github.com/Taneb/matrices

Taneb commented 3 years ago

One approach might be to work with (semi)modules and (semi)module homomorphisms (which don't yet exist in stdlib, see #1297). And then, eventually, show an isomorphism with some concrete representation when the module we're working with has a finite basis.

mechvel commented 3 years ago

I do not think that Matrix is for standard library. Rather it needs to be for the application libraries. If matrices, then there will go module bases and homomorphisms by matrices, then this will lead to the linear algebra methods. If it has gcd for Integer, and Matrix is there, why has not it, for example, solving a linear system? Then we would say "polynomials are not any worse than matrices", finally we shall have a large computer algebra system in standard, somewhat 100.000 pages of source. And almost noone will use it, because each specialist will like to program these things in its own way.