| Imagine you read a value from stdin and parse it as: 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 < n (or LTE (S k) n), and then you can construct Fin n from that evidence. (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 < n. _ONCE_ 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. |