3.4.1. 배열🔗

예를 들어, Lean의 배열은 대부분의 용도에서 연결 리스트보다 훨씬 더 효율적입니다. Lean에서 Array α 타입은 α 타입의 값을 담는 동적 크기 배열로, Java의 ArrayList, C++의 std::vector, Rust의 Vec와 매우 비슷합니다. cons 생성자를 사용할 때마다 포인터 간접 참조가 발생하는 List와 달리, 배열은 메모리의 연속된 영역을 차지하므로 프로세서 캐시에 훨씬 유리합니다. 또한 배열에서 값을 조회하는 데에는 상수 시간이 걸리는 반면, 연결 리스트에서의 조회는 접근하는 인덱스에 비례하는 시간이 걸립니다.

Lean과 같은 순수 함수형 언어에서는 자료 구조의 특정 위치를 변경하는 것이 불가능합니다. 대신 원하는 수정 사항이 반영된 복사본을 만듭니다. 하지만 복사가 항상 필요한 것은 아닙니다. Lean 컴파일러와 런타임에는 배열에 대한 참조가 단 하나뿐일 때 수정이 내부적으로 변경으로 구현될 수 있도록 하는 최적화가 들어 있습니다.

배열은 리스트와 비슷하게 작성하지만, 앞에 # 기호가 붙습니다:

배열에 들어 있는 값의 개수는 Array.size로 구할 수 있습니다. 예를 들어, northernTrees.size는 4로 평가됩니다. 배열 크기보다 작은 인덱스에 대해서는 리스트와 마찬가지로 인덱싱 표기법을 사용하여 해당 값을 찾을 수 있습니다. 즉, northernTrees[2]는 "elm"으로 평가됩니다. 또한 리스트와 마찬가지로 컴파일러는 인덱스가 범위 안에 있다는 증명을 요구하며, 배열의 범위를 벗어난 값을 조회하려고 하면 컴파일 타임 오류가 발생합니다. 예를 들어, northernTrees[8]은 다음과 같은 결과를 냅니다:

failed to prove index is valid, possible solutions:
  - Use `have`-expressions to prove the index is valid
  - Use `a[i]!` notation instead, runtime check is performed, and 'Panic' error message is produced if index is not valid
  - Use `a[i]?` notation instead, result is an `Option` type
  - Use `a[i]'h` notation instead, where `h` is a proof that index is valid
⊢ 8 < northernTrees.size

3.4.2. 비어 있지 않은 리스트🔗

비어 있지 않은 리스트를 나타내는 데이터 타입은 리스트의 머리를 위한 필드와 꼬리를 위한 필드를 가진 구조체로 정의할 수 있으며, 이때 꼬리는 빈 리스트일 수도 있는 평범한 리스트입니다:

예를 들어, 비어 있지 않은 리스트 idahoSpiders(미국 아이다호주에 서식하는 거미 종 몇 가지가 들어 있습니다)는 "Banded Garden Spider"와 그 뒤에 이어지는 다른 거미 네 종으로, 모두 다섯 종의 거미로 이루어져 있습니다:

이 리스트에서 특정 인덱스의 값을 재귀 함수로 찾으려면 다음 세 가지 경우를 고려해야 합니다.

1. 인덱스가 0인 경우로, 이때는 리스트의 헤드를 반환해야 합니다.

2. 인덱스가 n + 1이고 꼬리가 비어 있는 경우로, 이때 인덱스는 범위를 벗어납니다.

3. 인덱스가 n + 1이고 꼬리가 비어 있지 않은 경우입니다. 이 경우에는 꼬리와 n에 대해 함수를 재귀적으로 호출할 수 있습니다.

예를 들어, Option을 반환하는 조회 함수는 다음과 같이 작성할 수 있습니다:

패턴 매칭의 각 경우는 위에서 설명한 가능성 중 하나에 대응합니다. 정의의 본문은 암묵적으로 그 정의의 네임스페이스 안에 있으므로, get?를 재귀 호출할 때 NonEmptyList 네임스페이스 한정자를 붙일 필요가 없습니다. 이 함수는 인덱스가 0보다 클 때 리스트 조회 xs.tail[n]?를 사용하는 방식으로도 작성할 수 있습니다:

리스트에 항목이 하나만 있다면 0만 유효한 인덱스입니다. 항목이 두 개 있다면 0과 1 모두 유효한 인덱스입니다. 항목이 세 개 있다면 0, 1, 2가 유효한 인덱스입니다. 다시 말해, 비어 있지 않은 리스트의 유효한 인덱스는 리스트의 길이보다 엄격히 작은 자연수이며, 이는 곧 꼬리의 길이보다 작거나 같은 자연수입니다.

인덱스가 범위 안에 있다는 것의 의미에 대한 정의는 abbrev로 작성해야 합니다. 인덱스가 허용 가능하다는 증거를 찾는 데 사용되는 택틱은 수의 부등식을 풀 수는 있지만, NonEmptyList.inBounds라는 이름에 대해서는 아무것도 알지 못하기 때문입니다:

이 함수는 참일 수도 있고 거짓일 수도 있는 명제를 반환합니다. 예를 들어, 2는 idahoSpiders의 범위 안에 있지만, 5는 그렇지 않습니다:

논리 부정 연산자는 우선순위가 매우 낮으므로 ¬idahoSpiders.inBounds 5는 ¬(idahoSpiders.inBounds 5)와 동등합니다.

이 사실을 이용하면 컴파일 시점에 증거를 검사하는 리스트용 버전에 처리를 위임하여, 인덱스가 유효하다는 증거를 요구하므로 Option을 반환할 필요가 없는 조회 함수를 작성할 수 있습니다:

물론 같은 근거를 마침 사용할 수 있는 표준 라이브러리 함수에 위임하지 않고, 이 함수가 근거를 직접 사용하도록 작성할 수도 있습니다. 이렇게 하려면 증명과 명제를 다루는 기법이 필요하며, 이 기법은 이 책의 뒷부분에서 설명합니다.

3.4.3. 인덱싱 오버로딩🔗

컬렉션 타입의 인덱싱 표기법은 GetElem 타입 클래스의 인스턴스를 정의하여 오버로드할 수 있습니다. 유연성을 위해 GetElem에는 다음 네 개의 매개변수가 있습니다:

• 컬렉션의 타입

• 인덱스의 타입

• 컬렉션에서 추출되는 원소의 타입

• 인덱스가 범위 안에 있다는 증거로 무엇을 인정할지 결정하는 함수

원소 타입과 증거 함수는 둘 다 출력 매개변수입니다. GetElem에는 getElem이라는 메서드 하나만 있습니다. 이 메서드는 컬렉션 값, 인덱스 값, 그리고 인덱스가 범위 안에 있다는 증거를 인자로 받아 원소를 반환합니다:

NonEmptyList α의 경우, 이 매개변수들은 다음과 같습니다.

• 컬렉션은 NonEmptyList α입니다

• 인덱스의 타입은 Nat입니다

• 요소의 타입은 α입니다

• 인덱스가 꼬리의 길이보다 작거나 같으면 범위 안에 있습니다

사실 GetElem 인스턴스는 NonEmptyList.get에 바로 위임할 수 있습니다:

이 인스턴스를 사용하면 NonEmptyList도 List만큼 편리하게 사용할 수 있습니다. idahoSpiders.head를 평가하면 "Banded Garden Spider"가 나오지만, idahoSpiders[9]를 평가하면 다음과 같은 컴파일 타임 오류가 발생합니다:

failed to prove index is valid, possible solutions:
  - Use `have`-expressions to prove the index is valid
  - Use `a[i]!` notation instead, runtime check is performed, and 'Panic' error message is produced if index is not valid
  - Use `a[i]?` notation instead, result is an `Option` type
  - Use `a[i]'h` notation instead, where `h` is a proof that index is valid
⊢ idahoSpiders.inBounds 9

컬렉션 타입과 인덱스 타입이 모두 GetElem 타입 클래스의 입력 매개변수이므로, 새로운 타입으로 기존 컬렉션을 인덱싱할 수 있습니다. 양수 타입 Pos는 첫 번째 항목을 가리킬 수 없다는 단서가 붙기는 하지만, List의 인덱스로 사용하기에 전혀 무리가 없습니다. 다음 GetElem 인스턴스를 사용하면 리스트 항목을 찾을 때 Pos를 Nat만큼이나 편리하게 사용할 수 있습니다:

인덱싱은 숫자가 아닌 인덱스에도 의미가 있을 수 있습니다. 예를 들어 Bool을 사용하여 점의 필드 중 하나를 선택할 수 있습니다. 이때 false는 x에, true는 y에 대응합니다:

이 경우에는 두 불리언 값 모두 유효한 인덱스입니다. 가능한 모든 Bool 값이 범위 안에 있으므로, 증거는 단순히 참인 명제 True입니다.