3.4.1. Arrays🔗

예를 들어 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. Non-Empty Lists🔗

비어 있지 않은 리스트를 표현하는 데이터 타입은 리스트의 머리와 일반적인(비어 있을 수도 있는) 꼬리를 필드로 갖는 구조체로 정의할 수 있다.

예를 들어 미국 아이다호주에 서식하는 거미 종을 담은 비어 있지 않은 리스트 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. Overloading 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로 점의 필드 중 하나를 선택할 수 있다. false는 x, true는 y에 대응한다.

이 경우 두 불리언 모두 유효한 인덱스다. 가능한 모든 Bool이 범위 안이므로 증거는 참 명제 True일 뿐이다.