7.5. 의존 타입 프로그래밍의 함정
의존 타입의 유연성 덕분에 타입 검사기는 더 많은 유용한 프로그램을 받아들일 수 있습니다. 타입의 언어가 충분히 표현력이 풍부하여, 표현력이 약한 타입 시스템으로는 기술할 수 없는 변형까지 기술할 수 있기 때문입니다. 동시에, 의존 타입은 매우 세밀한 명세를 표현할 수 있으므로 타입 검사기는 버그가 있는 프로그램을 더 많이 거부할 수 있습니다. 이러한 강력함에는 대가가 따릅니다.
Row처럼 타입을 반환하는 함수의 내부 구현과 그 함수가 만들어 내는 타입이 긴밀하게 결합되어 있다는 점은 더 큰 어려움의 한 사례입니다. 함수가 타입 안에서 사용되면 함수의 인터페이스와 구현 사이의 구분이 무너지기 시작합니다. 일반적으로 함수의 타입 시그니처나 입출력 동작을 바꾸지 않는 한 모든 리팩터링은 유효합니다. 클라이언트 코드를 망가뜨리지 않고도 함수를 더 효율적인 알고리즘과 자료 구조를 사용하도록 다시 작성할 수 있고, 버그를 고칠 수 있으며, 코드의 명확성을 높일 수 있습니다. 그러나 함수가 타입 안에서 사용되면 함수 구현의 내부가 타입의 일부가 되고, 따라서 다른 프로그램에 대한 인터페이스의 일부가 됩니다.
예를 들어, 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를 펼치기만 하는 것이 아니라는 점입니다. Lean은 두 타입이 서로 동등한지, 즉 한 타입의 어떤 표현식이든 다른 타입을 기대하는 문맥에서 사용할 수 있는지 검사하는 동안 계산을 수행할 수도 있습니다. 이 성질을 정의상 동등성이라고 하며, 이는 미묘한 개념입니다.
물론 똑같이 작성된 두 타입은 정의상 같은 것으로 간주됩니다. 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]과 같습니다.
하지만 타입에는 함수 화살표, 데이터 타입, 생성자만 있는 것이 아닙니다. 타입에는 변수와 함수도 들어 있습니다. 변수의 정의상 동등성은 비교적 간단합니다. 각 변수는 오직 자기 자신과만 같으므로, (n k : Nat) → Vect Int n은 (n k : Nat) → Vect Int k와 정의상 같지 않습니다. 반면 함수는 더 복잡합니다. 수학에서는 입력과 출력의 동작이 똑같은 두 함수를 같다고 봅니다. 하지만 이를 확인하는 효율적인 알고리즘은 없습니다. 게다가 정의상 동등성은 애초에 Lean이 두 타입을 서로 바꿔 쓸 수 있는지 확인하려고 존재합니다. 대신 Lean은 두 함수가 모두 정의상 같은 본문을 가진 fun 표현식일 때 정의상 같다고 간주합니다. 다시 말해, 두 함수가 정의상 같다고 간주되려면 같은 보조 함수를 호출하는 같은 알고리즘을 사용해야 합니다. 이런 동등성은 대개 그다지 쓸모가 없으므로, 함수의 정의상 동등성은 주로 정의된 함수 하나가 두 타입에 똑같이 나타날 때 쓰입니다.
타입 안에서 함수가 호출되면, 정의상 동등성을 확인할 때 그 함수 호출을 축약해야 할 수도 있습니다. 1 + 4와 3 + 2가 정의상 같으므로 타입 Vect String (1 + 4)는 타입 Vect String (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의 패턴 매칭이 첫 번째 인자를 검사하기 때문입니다. 이것은 문제가 됩니다. 0은 덧셈의 왼쪽 항등원이자 오른쪽 항등원이어야 하는데도 (n : Nat) → Vect String n은 (n : Nat) → Vect String (Nat.plusL n 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)
정의상 동등성을 사용하여 타입을 비교한다는 것은 함수 정의의 내부를 포함하여 정의상 동등성에 관여하는 모든 것이 의존 타입과 인덱스 족을 사용하는 프로그램의 인터페이스의 일부가 된다는 것을 의미합니다. 함수의 내부를 타입에 노출한다는 것은, 노출된 프로그램을 리팩터링하면 그 프로그램을 사용하는 다른 프로그램이 더 이상 타입 검사를 통과하지 못하게 될 수 있다는 뜻입니다. 특히 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. 명제적 동등성
명제적 동등성은 두 표현식이 같다는 수학적 명제입니다. 정의상 동등성은 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을 쓰면 정의에 증명을 사용해야 합니다.