3.4.1. 배열🔗

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

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. 비어 있지 않은 리스트🔗

비어 있지 않은 리스트를 나타내는 데이터 타입은 리스트의 head를 위한 필드와, 비어 있을 수도 있는 일반적인 리스트인 tail을 위한 필드를 가진 구조체로 정의할 수 있습니다.

예를 들어, 비어 있지 않은 목록 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. 인덱싱 오버로딩🔗

컬렉션 타입에 대한 인덱싱(indexing) 표기법은 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은 점(point)의 필드 중 하나를 선택하는 데 사용될 수 있으며, false는 x에 대응하고 true는 y에 대응합니다:

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