7.5. 의존 타입으로 프로그래밍할 때의 함정
의존 타입의 유연성 덕분에 타입 검사기는 더 유용한 프로그램들을 받아들일 수 있는데, 이는 타입의 언어가 표현력이 낮은 타입 시스템으로는 기술할 수 없는 변형들을 기술할 만큼 충분히 표현력이 풍부하기 때문입니다. 동시에, 의존 타입이 매우 세밀한 명세를 표현할 수 있는 능력 덕분에 타입 검사기가 더 많은 버그가 있는 프로그램을 거부할 수 있습니다. 이러한 강력함에는 대가가 따릅니다.
Row와 같은 타입을 반환하는 함수의 내부와 그것이 생성하는 타입 사이의 긴밀한 결합은 더 큰 어려움의 한 사례입니다: 함수가 타입에서 사용될 때 함수의 인터페이스와 구현 사이의 구분이 무너지기 시작합니다. 일반적으로 모든 리팩터링은 함수의 타입 시그니처나 입출력 동작을 변경하지 않는 한 유효합니다. 함수는 클라이언트 코드를 손상시키지 않고도 더 효율적인 알고리즘과 자료 구조를 사용하도록 다시 작성할 수 있고, 버그를 수정할 수 있으며, 코드의 명료성을 개선할 수 있습니다. 하지만 함수가 타입에 사용될 경우, 함수 구현의 내부 사항이 타입의 일부가 되며, 따라서 다른 프로그램에 대한 interface의 일부가 됩니다.
예를 들어, Nat에 대한 덧셈의 다음 두 구현을 살펴보겠습니다. Nat.plusL은 첫 번째 인자에 대해 재귀적입니다:
def Nat.plusL : Nat → Nat → Nat
| 0, k => k
| n + 1, k => plusL n k + 1
반면 Nat.plusR는 두 번째 인자에 대해 재귀적입니다:
def Nat.plusR : Nat → Nat → Nat
| n, 0 => n
| n, k + 1 => plusR n k + 1덧셈의 두 구현은 모두 기저의 수학적 개념에 충실하며, 따라서 동일한 인자가 주어졌을 때 동일한 결과를 반환합니다.
하지만 이 두 구현은 타입에 사용될 때 상당히 다른 인터페이스를 제시합니다. 예를 들어, 두 Vect를 이어붙이는 함수를 살펴보겠습니다. 이 함수는 인자들의 길이의 합을 길이로 갖는 Vect를 반환해야 합니다. Vect는 본질적으로 더 많은 정보를 담은 타입을 가진 List이기 때문에, List.append를 작성할 때와 마찬가지로 첫 번째 인자에 대한 패턴 매칭과 재귀를 사용하여 함수를 작성하는 것이 합당합니다. 타입 시그니처와, 자리표시자를 가리키는 초기 패턴 매칭에서 시작하면 다음과 같은 두 개의 메시지가 나타납니다:
def appendL : Vect α n → Vect α k → Vect α (n.plusL k)
| .nil, ys => _
| .cons x xs, ys => _
nil 경우의 첫 번째 메시지는 자리표시자가 길이가 plusL 0 k인 Vect로 대체되어야 함을 나타냅니다:
cons 경우의 두 번째 메시지는 자리 표시자가 길이 plusL (n✝ + 1) k인 Vect로 대체되어야 함을 나타냅니다:
n 뒤에 붙은 dagger라고 불리는 기호는 Lean이 내부적으로 만들어낸 이름을 나타내는 데 사용됩니다. 내부적으로, 첫 번째 Vect에 대한 패턴 매칭은 첫 번째 Nat의 값도 암묵적으로 정제되게 만들었는데, 이는 생성자 cons의 인덱스가 n + 1이고 Vect의 꼬리 부분은 길이가 n이기 때문입니다. 여기서 n✝은 인자 n보다 1 작은 Nat을 나타냅니다.
7.5.1. 정의적 동치
plusL의 정의에는 0, k => k라는 패턴 케이스가 있습니다. 이는 첫 번째 자리표시자에 쓰인 길이에도 적용되므로, 밑줄의 타입 Vect α (Nat.plusL 0 k)를 다시 쓰는 또 다른 방법은 Vect α k입니다. 마찬가지로, plusL은 n + 1, k => plusL n k + 1이라는 패턴 케이스를 포함합니다. 이는 두 번째 밑줄의 타입을 Vect α (plusL n✝ k + 1)로 동등하게 쓸 수 있음을 의미합니다.
배후에서 벌어지는 일을 드러내기 위한 첫 단계는 Nat 인자를 명시적으로 작성하는 것이며, 이는 프로그램에 이름이 명시적으로 작성되었기 때문에 단검 기호가 없는 오류 메시지를 초래하기도 합니다:
def appendL : (n k : Nat) → Vect α n → Vect α k → Vect α (n.plusL k)
| 0, k, .nil, ys => _
| n + 1, k, .cons x xs, ys => _밑줄에 단순화된 버전의 타입을 주석으로 달아도 타입 오류가 발생하지 않으며, 이는 프로그램에 작성된 타입이 Lean이 스스로 찾아낸 타입과 동등하다는 것을 의미합니다:
def appendL : (n k : Nat) → Vect α n → Vect α k → Vect α (n.plusL k)
| 0, k, .nil, ys => (_ : Vect α k)
| n + 1, k, .cons x xs, ys => (_ : Vect α (n.plusL k + 1))
첫 번째 경우는 Vect α k를 요구하는데, ys가 바로 그 타입을 가지고 있습니다. 이는 빈 리스트를 다른 어떤 리스트에 이어붙이더라도 그 다른 리스트가 그대로 반환되는 방식과 유사합니다. 첫 번째 밑줄 대신 ys를 사용하여 정의를 다듬으면 채워야 할 밑줄이 하나만 남은 프로그램이 만들어집니다:
def appendL : (n k : Nat) → Vect α n → Vect α k → Vect α (n.plusL k)
| 0, k, .nil, ys => ys
| n + 1, k, .cons x xs, ys => (_ : Vect α (n.plusL k + 1))
여기서 매우 중요한 일이 일어났습니다. Lean이 Vect α (Nat.plusL 0 k)를 기대한 문맥에서, Vect α k를 받았습니다. 하지만 Nat.plusL는 abbrev가 아니므로, 타입 검사 중에 실행되지 않아야 할 것처럼 보일 수 있습니다. 무언가 다른 일이 일어나고 있습니다.
이 상황을 이해하는 핵심은, Lean이 타입 검사 중에 abbrev를 단순히 펼치기만 하는 것이 아니라는 점입니다. 또한 두 타입이 서로 동등한지 확인하는 과정에서 계산을 수행할 수 있으며, 이를 통해 한 타입의 표현식이 다른 타입을 요구하는 문맥에서도 사용될 수 있도록 합니다. 이 속성은 definitional equality(정의적 동치)라고 불리며, 미묘한 성질을 지니고 있습니다.
물론, 동일하게 작성된 두 타입은 정의상 동등한 것으로 간주됩니다—Nat와 Nat, 또는 List String과 List String은 동등한 것으로 간주되어야 합니다. 서로 다른 데이터 타입으로 만들어진 두 구체 타입은 결코 같지 않으므로, List Nat은 Int와 같지 않습니다. 또한 내부 이름을 바꾸기만 한 타입들은 서로 같으므로, (n : Nat) → Vect String n은 (k : Nat) → Vect String k와 같습니다. 타입에는 일반적인 데이터가 포함될 수 있으므로, 정의적 동등성은 데이터가 언제 동등한지도 기술해야 합니다. 동일한 생성자를 사용한 경우는 서로 같으므로, 0은 0과 같고 [5, 3, 1]은 [5, 3, 1]과 같습니다.
그러나 타입에는 함수 화살표, 데이터 타입, 생성자만 있는 것이 아닙니다. 또한 variables와 functions도 포함합니다. 변수의 정의적 동등성은 비교적 단순합니다: 각 변수는 오직 자기 자신과만 같으므로, (n k : Nat) → Vect Int n은 (n k : Nat) → Vect Int k와 정의적으로 동등하지 않습니다. 반면, 함수는 더 복잡합니다. 수학에서는 입력-출력 동작이 동일하면 두 함수를 같다고 간주하지만, 이를 확인하는 효율적인 알고리즘은 존재하지 않으며, 정의적 동등성의 핵심 목적은 Lean이 두 타입을 서로 바꾸어 사용할 수 있는지 확인하는 데 있습니다. 대신, Lean은 두 함수가 모두 정의상 동등한 본문을 가진 fun-표현식일 때 이들을 정의상 동등한 것으로 간주합니다. 다시 말해, 두 함수가 정의상 동등하다고 간주되려면 동일한 헬퍼를 호출하는 동일한 알고리즘을 사용해야 합니다. 이는 보통 그다지 유용하지 않으므로, 함수의 정의적 동등성은 대체로 정확히 동일한 정의된 함수가 두 타입에 등장하는 경우에 사용됩니다.
타입에서 함수가 호출될 때, 정의적 동치성을 검사하려면 함수 호출을 축약해야 할 수 있습니다. Vect String (1 + 4) 타입은 Vect String (3 + 2) 타입과 정의상 동일한데, 이는 1 + 4가 3 + 2와 정의상 동일하기 때문입니다. 이 둘의 상등을 확인하려면 둘 다 5로 축약되며, 그런 다음 생성자 규칙을 다섯 번 사용할 수 있습니다. 데이터에 적용된 함수의 정의적 동치는 먼저 두 항이 이미 같은지 확인함으로써 검사할 수 있습니다—어쨌든 ["a", "b"] ++ ["c"]가 ["a", "b"] ++ ["c"]와 같은지 확인하기 위해 이를 축약할 필요는 없습니다. 그렇지 않다면 함수가 호출되어 그 값으로 대체되며, 이후 이 값을 검사할 수 있습니다.
모든 함수 인자가 구체적인 데이터인 것은 아닙니다. 예를 들어, 타입에는 zero와 succ 생성자로부터 만들어지지 않은 Nat이 포함될 수 있습니다. (n : Nat) → Vect String n 타입에서 변수 n은 Nat이지만, 함수가 호출되기 전에는 그것이 어느 Nat인지 알 수 없습니다. 실제로 이 함수는 처음에 0으로 호출되었다가, 나중에 17로, 그리고 다시 33으로 호출될 수 있습니다. appendL의 정의에서 볼 수 있듯이, Nat 타입을 가진 변수는 plusL와 같은 함수에도 전달될 수 있습니다. 실제로, 타입 (n : Nat) → Vect String n은 타입 (n : Nat) → Vect String (Nat.plusL 0 n)과 정의상 동일합니다.
n과 Nat.plusL 0 n이 정의적으로 동일한 이유는 plusL의 패턴 매칭이 첫 번째 인자를 검사하기 때문입니다. 이는 문제가 됩니다: (n : Nat) → Vect String n는 (n : Nat) → Vect String (Nat.plusL n 0)와 정의상 동일하지 않습니다. 0은 덧셈의 좌항등원이자 우항등원이어야 하는데도 그렇습니다. 이는 패턴 매칭이 변수를 만나면 진행이 멈추기 때문에 발생합니다. n의 실제 값을 알기 전까지는 Nat.plusL n 0의 어떤 경우를 선택해야 하는지 알 방법이 없습니다.
쿼리 예제에 있는 Row 함수에서도 동일한 문제가 나타납니다. Row의 정의가 원소가 하나뿐인 리스트와 원소가 둘 이상인 리스트에 대해 별도의 경우를 가지고 있기 때문에, Row (c :: cs) 타입은 어떤 데이터 타입으로도 축약되지 않습니다. 다시 말해, 변수 cs를 구체적인 List 생성자와 매칭하려 할 때 막혀버립니다. 이것이 Row를 분해하거나 구성하는 거의 모든 함수가 Row 자체와 동일한 세 가지 경우를 매칭해야 하는 이유입니다: 막힌 상태를 해소하면 패턴 매칭이나 생성자 어느 쪽에든 사용할 수 있는 구체적인 타입이 드러납니다.
appendL의 누락된 경우는 Vect α (Nat.plusL n k + 1)을 요구합니다. 인덱스에 있는 + 1은 다음 단계로 Vect.cons를 사용해야 함을 시사합니다:
def appendL : (n k : Nat) → Vect α n → Vect α k → Vect α (n.plusL k)
| 0, k, .nil, ys => ys
| n + 1, k, .cons x xs, ys => .cons x (_ : Vect α (n.plusL k))
appendL을 재귀 호출하면 원하는 길이의 Vect를 구성할 수 있습니다:
def appendL : (n k : Nat) → Vect α n → Vect α k → Vect α (n.plusL k)
| 0, k, .nil, ys => ys
| n + 1, k, .cons x xs, ys => .cons x (appendL n k xs ys)
프로그램이 완성되었으므로, n과 k에 대한 명시적 매칭을 제거하면 읽기도 쉬워지고 함수를 호출하기도 더 쉬워집니다:
def appendL : Vect α n → Vect α k → Vect α (n.plusL k)
| .nil, ys => ys
| .cons x xs, ys => .cons x (appendL xs ys)
정의적 동등성을 사용하여 타입을 비교한다는 것은, 함수 정의의 내부 구현을 포함하여 정의적 동등성에 관여하는 모든 것이 의존 타입과 인덱싱된 패밀리를 사용하는 프로그램의 interface의 일부가 됨을 의미합니다. 함수의 내부 구현을 타입에 노출한다는 것은, 노출된 프로그램을 리팩터링할 경우 이를 사용하는 프로그램이 더 이상 타입 검사를 통과하지 못하게 될 수 있음을 의미합니다. 특히, plusL이 appendL의 타입에서 사용된다는 사실은 plusL의 정의가 그 외의 경우에는 동등한 plusR로 대체될 수 없음을 의미합니다.
7.5.2. 덧셈에서 막히기
append를 대신 plusR로 정의하면 어떻게 됩니까? 각 경우에 대해 명시적인 길이와 자리 표시자로 밑줄을 사용하여 동일한 방식으로 시작하면 다음과 같은 유용한 오류 메시지가 나타납니다:
def appendR : (n k : Nat) → Vect α n → Vect α k → Vect α (n.plusR k)
| 0, k, .nil, ys => _
| n + 1, k, .cons x xs, ys => _
하지만 첫 번째 자리 표시자에 Vect α k 타입 주석을 붙이려고 하면 타입 불일치 오류가 발생합니다.
def appendR : (n k : Nat) → Vect α n → Vect α k → Vect α (n.plusR k)
| 0, k, .nil, ys => (_ : Vect α k)
| n + 1, k, .cons x xs, ys => _
이 오류는 Nat.plusR 0 k와 k가 정의상 동등하지 않다는 것을 지적하고 있습니다.
이는 plusR가 다음과 같이 정의되어 있기 때문입니다:
def Nat.plusR : Nat → Nat → Nat
| n, 0 => n
| n, k + 1 => plusR n k + 1
이 함수의 패턴 매칭은 첫 번째 인자가 아니라 두 번째 인자에서 일어나므로, 그 위치에 변수 k가 있다는 것은 이 함수가 축약되는 것을 막습니다. Lean 표준 라이브러리의 Nat.add는 plusL이 아니라 plusR과 동치이므로, 이 정의에서 그것을 사용하려고 하면 정확히 같은 어려움이 발생합니다:
def appendR : (n k : Nat) → Vect α n → Vect α k → Vect α (n + k)
| 0, k, .nil, ys => (_ : Vect α k)
| n + 1, k, .cons x xs, ys => _덧셈은 변수에서 막혀 있습니다. 이를 해결하려면 명제적 동등성이 필요합니다.
7.5.3. 명제적 동등성
명제적 동등성(propositional equality)은 두 표현식이 같다는 수학적 명제입니다. 정의적 동치가 필요할 때 Lean이 자동으로 확인하는 일종의 배경 사실인 반면, 명제적 동치의 진술은 명시적인 증명을 필요로 합니다. 동등성 명제가 증명되고 나면, 이를 프로그램에서 사용하여 타입을 수정할 수 있는데, 이때 동등성의 한쪽을 다른 쪽으로 치환함으로써 타입 검사기가 막힌 상태를 풀 수 있습니다.
정의적 동등성이 이렇게 제한적인 이유는 알고리즘으로 검사할 수 있도록 하기 위해서입니다. 명제적 동등성은 훨씬 더 풍부하지만, 컴퓨터는 일반적으로 두 표현식이 명제적으로 동등한지 검사할 수 없습니다. 다만 제시된 증명이 실제로 증명인지는 검증할 수 있습니다. 정의적 동등성과 명제적 동등성의 구분은 인간과 기계 사이의 역할 분담을 나타냅니다. 가장 지루한 동등성들은 정의적 동등성의 일부로서 자동으로 검사되며, 이로써 인간의 정신은 명제적 동등성에서 다룰 수 있는 흥미로운 문제들에 집중할 수 있게 됩니다. 마찬가지로, 정의적 동등성은 타입 검사기에 의해 자동으로 호출되는 반면, 명제적 동등성은 특별히 호출해야 합니다.
명제, 증명, 인덱싱에서는 일부 동등성 명제가 decide 택틱을 사용하여 증명됩니다. 이러한 동등성 명제들은 모두 명제적 동등성이 사실 이미 정의적 동등성이기도 한 경우들입니다. 일반적으로 명제적 동등성에 대한 진술은 먼저 정의적으로 성립하거나 이미 증명된 동등성에 충분히 가까운 형태로 만든 다음, decide나 simp와 같은 택틱 도구를 사용하여 단순화된 경우를 처리함으로써 증명됩니다. simp 택틱은 상당히 강력합니다. 내부적으로는 여러 빠른 자동화 도구를 사용하여 증명을 구성합니다. rfl이라는 더 단순한 택틱은 정의적 동등성을 사용하여 명제적 동등성을 증명합니다. rfl이라는 이름은 reflexivity(반사성)의 줄임말로, 모든 것이 자기 자신과 같다는 동치성의 속성을 나타냅니다.
appendR의 막힌 상태를 풀려면 k = Nat.plusR 0 k라는 증명이 필요한데, 이는 plusR가 두 번째 인자의 변수에서 막혀 있기 때문에 정의상 동일성이 아닙니다. 이를 계산하게 하려면, k가 구체적인 생성자가 되어야 합니다. 이것은 패턴 매칭이 필요한 작업입니다.
특히 k는 어떤 Nat이든 될 수 있으므로, 이 작업에는 어떤 k에 대해서든 k = Nat.plusR 0 k라는 증거를 반환할 수 있는 함수가 필요합니다. 이는 (k : Nat) → k = Nat.plusR 0 k 타입을 가지는, 동등성의 증명을 반환하는 함수여야 합니다. 초기 패턴과 플레이스홀더로 시작하면 다음과 같은 메시지가 나타납니다:
def plusR_zero_left : (k : Nat) → k = Nat.plusR 0 k
| 0 => _
| k + 1 => _
패턴 매칭을 통해 k를 0으로 정제한 뒤, 첫 번째 플레이스홀더는 정의상 성립하는 명제에 대한 증거를 나타냅니다. rfl 택틱이 이를 처리하여, 두 번째 자리표시자만 남습니다:
def plusR_zero_left : (k : Nat) → k = Nat.plusR 0 k
⊢ 0 = Nat.plusR 0 0 ⊢ 0 = Nat.plusR 0 0 All goals completed! 🐙
| k + 1 => _
두 번째 자리 표시자는 조금 더 까다롭습니다. 표현식 Nat.plusR 0 k + 1은 Nat.plusR 0 (k + 1)과 정의상 동일합니다. 이는 목표를 k + 1 = Nat.plusR 0 k + 1로도 쓸 수 있음을 의미합니다:
def plusR_zero_left : (k : Nat) → k = Nat.plusR 0 k
⊢ 0 = Nat.plusR 0 0 ⊢ 0 = Nat.plusR 0 0 All goals completed! 🐙
| k + 1 => (_ : k + 1 = Nat.plusR 0 k + 1)
등식의 양변에 있는 + 1 아래에는 함수 자체가 반환하는 것의 또 다른 인스턴스가 있습니다. 다시 말해, k에 대한 재귀 호출은 k = Nat.plusR 0 k라는 증거를 반환할 것입니다. 함수 인자에 적용되지 않는다면 동등성은 동등성이 아닐 것입니다. 다시 말해, x = y이면, f x = f y입니다. 표준 라이브러리에는 함수와 동등성 증명을 받아, 그 함수를 동등성의 양변에 적용한 새로운 증명을 반환하는 congrArg 함수가 포함되어 있습니다. 이 경우, 함수는 (· + 1)입니다:
def plusR_zero_left : (k : Nat) → k = Nat.plusR 0 k
⊢ 0 = Nat.plusR 0 0 ⊢ 0 = Nat.plusR 0 0 All goals completed! 🐙
| k + 1 =>
congrArg (· + 1) (plusR_zero_left k)
이는 실제로는 명제의 증명이므로, theorem으로 선언해야 합니다:
theorem plusR_zero_left : (k : Nat) → k = Nat.plusR 0 k
⊢ 0 = Nat.plusR 0 0 ⊢ 0 = Nat.plusR 0 0 All goals completed! 🐙
| k + 1 =>
congrArg (· + 1) (plusR_zero_left k)
명제 등식은 오른쪽 삼각형 연산자 ▸를 사용하여 프로그램에 적용할 수 있습니다. 첫 번째 인자로 동등성 증명을 받고 두 번째 인자로 다른 표현식을 받으면, 이 연산자는 두 번째 인자의 타입에서 동등성의 한쪽을 나타내는 항들을 동등성의 다른 쪽으로 치환합니다. 다시 말해, 다음 정의는 타입 오류를 포함하지 않습니다:
def appendR : (n k : Nat) → Vect α n → Vect α k → Vect α (n.plusR k)
| 0, k, .nil, ys => plusR_zero_left k ▸ (_ : Vect α k)
| n + 1, k, .cons x xs, ys => _첫 번째 자리표시자는 예상 타입을 가지고 있습니다:
이제 ys로 채울 수 있습니다:
def appendR : (n k : Nat) → Vect α n → Vect α k → Vect α (n.plusR k)
| 0, k, .nil, ys => plusR_zero_left k ▸ ys
| n + 1, k, .cons x xs, ys => _남은 자리표시자를 채우려면 또 다른 덧셈 인스턴스를 풀어야 합니다:
여기서 증명해야 할 명제는 Nat.plusR (n + 1) k = Nat.plusR n k + 1이며, 이는 ▸와 함께 사용하여 + 1을 표현식의 맨 위로 끌어내어 cons의 인덱스와 일치하도록 만들 수 있습니다.
이 증명은 plusR의 두 번째 인자, 즉 k에 대해 패턴 매칭을 수행하는 재귀 함수입니다. 이는 plusR 자체가 두 번째 인자에 대해 패턴 매칭을 수행하기 때문이며, 따라서 증명이 패턴 매칭을 통해 이를 “풀어내어” 계산적 동작을 드러낼 수 있습니다. 증명의 골격은 plusR_zero_left의 것과 매우 유사합니다:
theorem plusR_succ_left (n : Nat) :
(k : Nat) → Nat.plusR (n + 1) k = Nat.plusR n k + 1
n:Nat⊢ (n + 1).plusR 0 = n.plusR 0 + 1 n:Nat⊢ (n + 1).plusR 0 = n.plusR 0 + 1 All goals completed! 🐙
| k + 1 => _
남은 경우의 타입은 정의상 Nat.plusR (n + 1) k + 1 = Nat.plusR n (k + 1) + 1와 같으므로, plusR_zero_left에서와 마찬가지로 congrArg로 해결할 수 있습니다:
그 결과 완성된 증명은 다음과 같습니다:
theorem plusR_succ_left (n : Nat) :
(k : Nat) → Nat.plusR (n + 1) k = Nat.plusR n k + 1
n:Nat⊢ (n + 1).plusR 0 = n.plusR 0 + 1 n:Nat⊢ (n + 1).plusR 0 = n.plusR 0 + 1 All goals completed! 🐙
| k + 1 => congrArg (· + 1) (plusR_succ_left n k)
완성된 증명을 사용하여 appendR의 두 번째 경우를 해결할 수 있습니다:
def appendR : (n k : Nat) → Vect α n → Vect α k → Vect α (n.plusR k)
| 0, k, .nil, ys =>
plusR_zero_left k ▸ ys
| n + 1, k, .cons x xs, ys =>
plusR_succ_left n k ▸ .cons x (appendR n k xs ys)
appendR에 대한 길이 인자를 다시 암시적으로 만들면, 이 인자들은 증명에서 참조하기 위해 명시적으로 이름 붙여지지 않습니다. 그러나 Lean의 타입 검사기는 다른 값으로는 타입이 일치할 수 없기 때문에, 이를 배후에서 자동으로 채워 넣을 수 있는 충분한 정보를 가지고 있습니다:
def appendR : Vect α n → Vect α k → Vect α (n.plusR k)
| .nil, ys => plusR_zero_left _ ▸ ys
| .cons x xs, ys => plusR_succ_left _ _ ▸ .cons x (appendR xs ys)7.5.4. 장단점
인덱스 패밀리는 중요한 속성을 가지고 있습니다: 이에 대한 패턴 매칭은 정의적 동등성에 영향을 미칩니다. 예를 들어, Vect에 대한 match 식에서 nil 경우에는 길이가 단순히 0이 됩니다. 정의적 동등성은 항상 활성화되어 있고 명시적으로 호출할 필요가 없기 때문에 매우 편리할 수 있습니다.
하지만 의존 타입 및 패턴 매칭과 함께 정의적 동등성을 사용하는 것에는 심각한 소프트웨어 공학적 단점이 있습니다. 우선, 함수는 타입에 사용되도록 특별히 작성되어야 하며, 타입에 사용하기 편리한 함수가 가장 효율적인 알고리즘을 사용하지 않을 수도 있습니다. 함수가 타입에서 사용됨으로써 노출되고 나면, 그 구현이 인터페이스의 일부가 되어 향후 리팩터링에 어려움을 초래하게 됩니다. 둘째, 정의적 동치는 느릴 수 있습니다. 두 표현식이 정의상 동일한지 확인하라는 요청을 받으면, 문제가 되는 함수들이 복잡하고 여러 층의 추상화를 가지고 있을 경우 Lean은 많은 양의 코드를 실행해야 할 수도 있습니다. 셋째, 정의적 동등성의 실패로 인해 발생하는 오류 메시지는 함수의 내부 구현을 기준으로 표현되는 경우가 있어, 항상 이해하기 쉬운 것은 아닙니다. 오류 메시지에 나타나는 표현식의 출처를 이해하는 것이 항상 쉬운 것은 아닙니다. 마지막으로, 색인화된 패밀리와 의존 타입 함수의 모음에 사소하지 않은 불변량을 인코딩하는 것은 종종 취약할 수 있습니다. 시스템에서 함수의 노출된 축약 동작이 편리한 정의적 동등성을 제공하지 못하는 것으로 판명되면, 초기 정의를 변경해야 하는 경우가 종종 있습니다. 이에 대한 대안은 프로그램 곳곳에 동등성 증명 호출을 흩뿌려 넣는 것이지만, 이는 상당히 다루기 번거로워질 수 있습니다.
관용적인 Lean 코드에서는 인덱싱된 데이터 타입이 자주 사용되지 않습니다. 대신, 서브타입과 명시적 명제를 사용하여 중요한 불변식을 강제하는 것이 일반적입니다. 이 접근 방식은 많은 명시적인 증명을 수반하며, 정의적 동등성에 의존하는 경우는 매우 적습니다. 대화형 정리 증명기에 걸맞게, Lean은 명시적 증명을 편리하게 작성할 수 있도록 설계되었습니다. 일반적으로 말해서, 대부분의 경우 이 접근 방식을 선호해야 합니다.
하지만 인덱싱된 데이터타입 패밀리를 이해하는 것은 중요합니다. plusR_zero_left와(과) plusR_succ_left와(과) 같은 재귀 함수는 사실 수학적 귀납법에 의한 증명입니다. 재귀의 기저 사례는 귀납법의 기저 사례에 대응하며, 재귀 호출은 귀납 가설에 대한 호소를 나타냅니다. 더 일반적으로, Lean에서 새로운 명제는 흔히 증거의 귀납적 타입으로 정의되며, 이러한 귀납적 타입은 대개 인덱스를 가집니다. 정리를 증명하는 과정은 사실 뒤에서 이러한 타입을 가지는 표현식을 구성하는 과정이며, 이는 이 절의 증명들과 다르지 않습니다. 또한, 색인화된 데이터 타입이 때로는 정확히 그 작업에 알맞은 도구인 경우도 있습니다. 이를 능숙하게 사용하는 것은 언제 사용해야 하는지 아는 것의 중요한 부분입니다.
7.5.5. 연습문제
-
plusR_succ_left스타일의 재귀 함수를 사용하여, 모든Nat인n과k에 대해n.plusR k = n + k임을 증명하십시오. -
plusR이plusL보다 더 자연스러운Vect함수를 작성하십시오. 여기서plusL은 정의에 증명을 사용해야 합니다.