Futhark is really such a great idea. I'm not convinced that dependent types are worth the cognitive overhead in general, but it's definitely worth it to include the length as part of the type information for dynamic arrays, e.g.:<p><pre><code> concat(Vec<T, n>, Vec<T, m>) -> Vec<T, n+m>
matmul(Mat<T, n, m>, Mat<T, m, l>) -> Mat<T, n, l>
head(Vec<T, n+1>) -> (T, Vec<T, n>)
</code></pre>
This would have saved me so much headache debugging CUDA kernels and numpy!! I wish it were a first-class feature in those frameworks, and even general-purpose languages, but alas.
Here they are in Futhark:<p><pre><code> val concat [n] [m] 't : (xs: [n]t) -> (ys: [m]t) -> *[n + m]t
val matmul [n] [m] [l] 't : (xs: [n][m]t) -> (ys: [m][l]t) -> *[n][l]t
val head [n] 't : (x: [n]t) -> t
</code></pre>
And here's the pathological case (length cannot be determined at compile time):<p><pre><code> val filter [n] 'a : (p: a -> bool) -> (as: [n]a) -> *[]a
</code></pre>
Other pathological cases include conditionals and loops.
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<p><pre><code> argv: Vec<String, argc>
</code></pre>
If I want to map these to ints, then I'd like a compile-time guarantee that the resulting array<p><pre><code> nums: Vec<Int, argc>
</code></pre>
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.
Yeah, C++ arrays are literally that.
Arrays are not dynamically sized though (handling runtime sizes) and don’t have efficient append/concat. The point of the dependent types is that you can have the type system track that concat creates an M+N length vector, sort preserves length (and adds a sorted guarantee that slice preserves), etc.
Sure you can do a lot with templates, but that’s advanced templates not just “C++ arrays” in a throwaway “literally that” way.