You can go even further with this in other languages, with things like dependent typing - which can assert (among other interesting properties) that, for example, something like

    get_elem_at_index(array, index)

cannot ever have index outside the bounds of the array, but checked statically at compilation time - and this is the key, without knowing a priori what the length of array is.

"In Idris, a length-indexed vector is Vect n a (length n is in the type), and a valid index into length n is Fin n ('a natural number strictly less than n')."

Similar tricks work with division that might result in inf/-inf, to prevent them from typechecking, and more subtle implications in e.g. higher order types and functions

▲ satvikpendem an hour ago | parent | next [-]

Rust has some libraries that can do dependent typing too, based on macros. For example: https://youtube.com/watch?v=JtYyhXs4t6w

Which refers to https://docs.rs/anodized/latest/anodized/

▲ VorpalWay 3 hours ago | parent | prev | next [-]

How does that work? If the length of the array is read from stdin for example, it would be impossible to know it at compile time. Presumably this is limited somehow?

	▲	marcosdumay 2 hours ago \| parent \| next [-]
		If you check that the value is inside the range, and execute some different code if it's not, then congratulations, you now know at compile time that the number you will read from stdin is in the right range.
	▲	mdm12 2 hours ago \| parent \| prev \| next [-]
		One option is dependent pairs, where one value of the pair (in this example) would be the length of the array and the other value is a type which depends on that same value (such as Vector n T instead of List T). Type-Driven Development with Idris[1] is a great introduction for dependently typed languages and covers methods such as these if you're interested (and Edwin Brady is a great teacher). [1] https://www.manning.com/books/type-driven-development-with-i...
	▲	dernett 2 hours ago \| parent \| prev \| next [-]
		Not sure about Idris, but in Lean `Fin n` is a struct that contains a value `i` and a proof that `i < n`. You can read in the value `n` from stdin and then you can do `if h : i < n` to have a compile-time proof `h` that you can use to construct a `Fin n` instance.
	▲	ratorx 2 hours ago \| parent \| prev \| next [-]
		It doesn’t have to be a compile time constant. An alternative is to prove that when you are calling the function the index is always less than the size of the vector (a dynamic constraint). You may be able to assert this by having a separate function on the vector that returns a constrained value (eg. n < v.len()).
	▲	jaggederest 3 hours ago \| parent \| prev [-]
		If the length is read from outside the program it's an IO operation, not a static variable, but there are generally runtime checks in addition to the type system. Usually you solve this as in the article, with a constructor that checks it - so you'd have something like "Invalid option: length = 5 must be within 0-4" when you tried to create the Fin n from the passed in value

▲ esafak 2 hours ago | parent | prev [-]

I wish dependent types were more common :(