This isn't really a fundamental disagreement. If we think of array functions as functions `Array<Index1, Element1> → Array<Index2, Element2>`, then essentially

This isn't really a fundamental disagreement. If we think of array functions as functions `Array<Index1, Element1> → Array<Index2, Element2>`, then essentially all you need to be able to say is that a function is generic over `Index1` and calculates some output index type `Index2` as a function of `Index1`. This is perfectly possible to do with Rust traits or Haskell type classes (although not all that ergonomic).