Safe Array Indices
The GetElem
instance for Array
and Nat
requires a proof that the provided Nat
is smaller than the array.
In practice, these proofs often end up being passed to functions along with the indices.
Rather than passing an index and a proof separately, a type called Fin
can be used to bundle up the index and the proof into a single value.
This can make code easier to read.
Additionally, many of the built-in operations on arrays take their index arguments as Fin
rather than as Nat
, so using these built-in operations requires understanding how to use Fin
.
The type Fin n
represents numbers that are strictly less than n
.
In other words, Fin 3
describes 0
, 1
, and 2
, while Fin 0
has no values at all.
The definition of Fin
resembles Subtype
, as a Fin n
is a structure that contains a Nat
and a proof that it is less than n
:
structure Fin (n : Nat) where
val : Nat
isLt : LT.lt val n
Lean includes instances of ToString
and OfNat
that allow Fin
values to be conveniently used as numbers.
In other words, the output of #eval (5 : Fin 8)
is 5
, rather than something like {val := 5, isLt := _}
.
Instead of failing when the provided number is larger than the bound, the OfNat
instance for Fin
returns a value modulo the bound.
This means that #eval (45 : Fin 10)
results in 5
rather than a compile-time error.
In a return type, a Fin
returned as a found index makes its connection to the data structure in which it was found more clear.
The Array.find
in the previous section returns an index that the caller cannot immediately use to perform lookups into the array, because the information about its validity has been lost.
A more specific type results in a value that can be used without making the program significantly more complicated:
def findHelper (arr : Array α) (p : α → Bool) (i : Nat) : Option (Fin arr.size × α) :=
if h : i < arr.size then
let x := arr[i]
if p x then
some (⟨i, h⟩, x)
else findHelper arr p (i + 1)
else none
termination_by findHelper arr p i => arr.size - i
def Array.find (arr : Array α) (p : α → Bool) : Option (Fin arr.size × α) :=
findHelper arr p 0
Exercise
Write a function Fin.next? : Fin n → Option (Fin n)
that returns the next largest Fin
when it would be in bounds, or none
if not.
Check that
#eval (3 : Fin 8).next?
outputs
some 4
and that
#eval (7 : Fin 8).next?
outputs
none