You can do this with templates in C++ and generics in Rust I'm pretty sure. I think the Eigen C++ library supports this. (I have yet to do a linear algebra heavy Rust project, so I can't speak to the options that exist there.)
I'm talking about cases where the array size is not known at compile time. For example, say the user passes in a list of numbers as command line arguments. Then we have
argv: Vec<String, argc>
If I want to map these to ints, then I'd like a compile-time guarantee that the resulting array
nums: Vec<Int, argc>
is the same length as argv. Lean and Idris can do this, but AFAIK no commonly used languages can. But unlike general dependent types, these are not hard to wrap one's head around and would save a lot of frustration, in my experience.
I'm talking about cases where the array size is not known at compile time. For example, say the user passes in a list of numbers as command line arguments. Then we have
If I want to map these to ints, then I'd like a compile-time guarantee that the resulting array is the same length as argv. Lean and Idris can do this, but AFAIK no commonly used languages can. But unlike general dependent types, these are not hard to wrap one's head around and would save a lot of frustration, in my experience.