[BlackFly]

Arrays are syntactic sugar over something that resembles a function, sure.

Real signature of an array implementation would be something like V: [0, N] -> T, but that implies you need to statically prove that each index i for V[i] is less than N. So your code would be littered with such guards for dynamic indexing. Also, N itself will be dynamic, so you need some (at least limited) dependent typing on top of this.

So you don't want these things in your language so you just accept the domain as some integer type, so now you don't really have V: ℕ -> T, since for i > N there is no value. You could choose V: ℕ -> Maybe<T> and have even cases where i is provably less than N to be littered with guards, so this cure is worse than the disease. Same if you choose V: ℕ -> Result<T, IndexOutOfBounds>. So instead you panic or throw, now you have an effect which isn't really modeled well as a function (until we start calling the code after it a continuation and modify the signature, and...).

So it looks like a function if you squint or are overly formal with guards or effects, but the arrays of most languages aren't that.

> for one of the best ways to improve a language is to make it smaller.

I think this isn't one of those cases.

[zozbot234]

> but that implies you need to statically prove that each index i for V[i] is less than N. So your code would be littered with such guards for dynamic indexing.

You just need a subrange type for i. Even PASCAL had those. And if you have full dependent types you can statically prove that your array accesses are sound without required bounds checking. (You can of course use optional bounds checking as one of many methods of proof.)

[BlackFly]

Yes, as I said, you must use bounds checking or dependent types or effects or monad returns.

Arrays are the effect choice in most languages. The signature as a function becomes a gnarly continuation passing if you insist on the equivalence and so most people just tend to think of it imperatively.

[fanf2]

Functions are partial in most programming languages, so the fact that arrays are best modelled as partial functions (rather than total functions) isn’t a huge obstacle.

[BlackFly]

Yeah, in languages with effects (exceptions/panics). That is a bit more than a partial function though.