Comment by ethanlipson

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.:

  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>)

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.