8.5. Bounded Numbers🔗

Array와 Nat의 GetElem 인스턴스는 주어진 Nat이 배열보다 작다는 증명을 요구한다. 실제로 이 증명은 인덱스와 함께 함수에 전달되는 경우가 많다. 인덱스와 증명을 따로 전달하는 대신 Fin 타입으로 인덱스와 증명을 하나의 값으로 묶을 수 있다. 그러면 코드를 읽기 쉬워진다.

Fin n 타입은 n보다 엄격히 작은 수를 나타낸다. 즉 Fin 3은 0, 1, 2를 나타내고 Fin 0에는 값이 없다. Fin의 정의는 Subtype와 비슷하다. Fin n은 Nat과 그것이 n보다 작다는 증명을 포함하는 구조체다:

structure Fin (n : Nat) where
  val  : Nat
  isLt : LT.lt val n

Lean은 Fin 값을 수처럼 편리하게 사용하게 하는 ToString과 OfNat 인스턴스를 포함한다. 즉 #eval (5 : Fin 8)의 출력은 {val := 5, isLt := _} 같은 것이 아니라 5다.

주어진 수가 범위보다 클 때 실패하는 대신 Fin의 OfNat 인스턴스는 범위에 대한 나머지 값을 반환한다. 따라서 #eval (45 : Fin 10)은 컴파일 시점 오류 대신 5를 결과로 낸다.

찾은 인덱스를 반환 타입의 Fin으로 표현하면 해당 인덱스를 찾은 자료구조와의 연결이 더 분명해진다. 앞 절의 Array.find는 유효성 정보가 사라져 호출자가 배열 조회에 즉시 사용할 수 없는 인덱스를 반환한다. 더 구체적인 타입을 사용하면 프로그램을 크게 복잡하게 만들지 않고도 사용할 수 있는 값이 된다:

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

def Array.find (arr : Array α) (p : α → Bool) : Option (Fin arr.size × α) :=
  findHelper arr p 0

8.5.1. Exercise🔗

Fin.next? : Fin n → Option (Fin n) 함수를 작성하라. 범위 안에 다음으로 큰 Fin이 있으면 반환하고, 없으면 none을 반환하라. 다음이 맞는지 확인하라.

some 4#eval (3 : Fin 8).next?

출력:

some 4

그리고 다음도 확인하라:

none#eval (7 : Fin 8).next?

출력:

none