[Agda] Dimension-safe matrix operations?

[Peter Thiemann]

A good place to look is the Accelerate library for Haskell+GPU

https://hackage.haskell.org/package/accelerate

Several years back, I tried to make an Agda frontend for that library, 
but the Haskell implementation pushes the limit of what you can express 
in the types pretty far, so I didn't get much extra mileage from Agda.

There is also related work by Jeremy Gibbons; that paper should give you 
a start:

  * Jeremy Gibbons:
    APLicative Programming with Naperian Functors.ESOP2017
    <https://dblp.org/db/conf/esop/esop2017.html#Gibbons17>:556-583
  *


-Peter


On 09.06.21 09:44, Kenichi Asai 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.
>
> 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.
>