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…
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?
Maybe Int
So your program splits into two branches:
1. Nothing branch: you failed to obtain an Int.
There is no integer to use as an index, so you can’t even attempt a safe lookup into something like Vect n a.
2. Just i branch: you do have an Int called i.
But an Int is not automatically a valid index for Vect n a, because vectors are indexed by Fin n (a proof carrying “bounded natural”).
So inside the Just i branch, you refine further:
3. Try to turn the runtime integer i into a value of type Fin n.
There are two typical shapes of this step:
* Checked conversion returning Maybe (Fin n)
If the integer is in range, you get Just (fin : Fin n). Otherwise Nothing.
Checked conversion returning evidence (proof) that it’s in range
For example: produce k : Nat plus a proof like k (But it’s the same basically, you end up with a “Maybe LTE…”
Now if you also have a vector: xs : Vect n a
… the n in Fin n and the n in Vect n a are the same n (that’s what “unifies” means here: the types line up), so you can do: index fin xs : a
And crucially:
there is no branch in which you can call index without having constructed the Fin n first, so out-of-bounds access is unrepresentable (it’s not “checked later”, it’s “cannot be expressed”).
And within _that_ branch of the program, you have a proof of Fin n.
Said differently: you don’t get “compile-time knowledge of i”; you get a compile-time guarantee that whatever value you ended up with satisfies a predicate.
Concretely: you run a runtime check i If it fails, you’re in a branch where you do not have Fin n.
If it succeeds, you construct fin : Fin n at runtime (it’s a value, you can’t get around that), but its type encodes the invariant “in bounds”/check was done somewhere in this branch.