Why no Dependent Matrix Type?

help
1

Hello,

I don't really know how to really introduce this topic.
Background: I want to implement compile time safe matrix multiplication.
For that i want to have a struct with const generics for the number of columns and rows.
Then i want a function which takes two const generics and does the matrix multiplication.
The result would be a matrix with the different sizes.

So far so good i was able to implement this. One idea is sketched in this old post.

Now the caveat is that this works only at compile time and not at runtime.

1. Problem: currently for my thesis i am implementing a compiler and a library which transforms some DSL to a matrix. In my opinion it would be great if the library for matrixes has these const generics since this should remove many runtime dependencies. Are there any ideas on how to implement this?

2. Problem: I want to implement something like matrix concatenation. given two $n \times m$ and $n\times k$ matrix. the result of concatenation should be a $n \times m+k$ matrix. apparently this also does not work.

Any more inside into these dependent type problems in rust would be great.
I think from my point of view with safety in mind this should be inside the language.

2

If I'm understanding the situation properly (and I may not be), I think what you're looking for is the work being done on generic const args (GCA).

3

Because it’s a very difficult problem, even if we’re just talking about comparatively trivial stuff like Foo<N> * Foo<M> -> Foo<N + M>. An entire (runtime) dependent type system, the first in any non-research language? That’s just entirely beyond the horizon right now.

4

Thanks. I see the problems.

In my opinion this would be a great addition to the language but i see know it is quite difficult to implement currently.

However many research languages, like lean or rocq have not the wide spread adoption like rust has. Thus maybe in some future rust has a place there to bridge the gap.

5

A dependently typed system is interesting and has a lot of practically useful aspects, but I think it is less likely to happen. If you really want to express such a constraint which is applicable to scenarios involving runtime operations, I think you need to use some verification tools such as Verus and Creusot. These tools let you express far more complicated logical predicates that are verified statically. One caveat of this approach is that the downstream users also need to use these tools to verify their codes. Furthermore, it is worth noting that not all the langugage features are supported for verification, but I think more features will be adopted gradually.