1.5. 데이터 타입과 패턴
구조체를 사용하면 서로 독립적인 여러 데이터를 결합하여, 완전히 새로운 타입으로 표현되는 하나의 일관된 전체를 만들 수 있습니다. 구조체처럼 여러 값을 한데 묶는 타입을 곱 타입(product type)이라고 합니다. 그러나 도메인의 많은 개념은 구조체로 자연스럽게 표현할 수 없습니다. 예를 들어 애플리케이션에서 사용자 권한을 추적해야 할 수 있는데, 어떤 사용자는 문서 소유자이고, 어떤 사용자는 문서를 편집할 수 있으며, 나머지 사용자는 문서를 읽기만 할 수 있습니다. 계산기에는 덧셈, 뺄셈, 곱셈 같은 여러 이항 연산자가 있습니다. 구조체로는 여러 선택지를 쉽게 인코딩할 수 없습니다.
마찬가지로 구조체는 고정된 필드 집합을 관리하기에 훌륭한 방법이지만, 많은 애플리케이션에는 임의 개수의 원소를 담을 수 있는 데이터가 필요합니다. 트리나 리스트 같은 대부분의 고전적인 자료 구조는 재귀적인 구조를 가집니다. 리스트의 꼬리는 그 자체로 리스트이고, 이진 트리의 왼쪽 가지와 오른쪽 가지는 그 자체로 이진 트리입니다. 앞서 언급한 계산기에서는 표현식 자체의 구조가 재귀적입니다. 예를 들어, 덧셈 표현식의 피가수 자체가 곱셈 표현식일 수 있습니다.
선택지를 허용하는 데이터 타입을 합 타입이라 하고, 자기 자신의 인스턴스를 포함할 수 있는 데이터 타입을 재귀 데이터 타입이라 합니다. 재귀적인 합 타입은 귀납적 데이터 타입이라고 하는데, 이는 수학적 귀납법을 사용하여 이들에 관한 명제를 증명할 수 있기 때문입니다. 프로그래밍에서 귀납적 데이터 타입은 패턴 매칭과 재귀 함수를 통해 사용됩니다.
많은 내장 타입은 실제로는 표준 라이브러리에 정의된 귀납적 데이터 타입입니다. 예를 들어, Bool은 귀납적 데이터 타입입니다:
inductive Bool where
| false : Bool
| true : Bool
이 정의는 크게 두 부분으로 이루어져 있습니다. 첫 번째 줄은 새 타입의 이름(Bool)을 제공하고, 나머지 줄은 각각 생성자 하나를 기술합니다. 구조체의 생성자와 마찬가지로, 귀납적 데이터 타입의 생성자는 임의의 초기화 코드나 검증 코드를 넣는 곳이 아니라 다른 데이터를 받아 담아 두는 비활성 수신자이자 컨테이너일 뿐입니다. 구조체와 달리 귀납적 데이터 타입은 생성자를 여러 개 가질 수 있습니다. 여기에는 true와 false라는 두 생성자가 있으며, 둘 다 인자를 받지 않습니다. 구조체 선언이 자신의 이름들을 선언된 타입의 이름을 딴 네임스페이스에 두는 것처럼, 귀납적 데이터 타입도 생성자의 이름들을 네임스페이스에 둡니다. Lean 표준 라이브러리에서는 true와 false를 이 네임스페이스에서 다시 내보내므로, 각각 Bool.true와 Bool.false로 쓰지 않고 단독으로 쓸 수 있습니다.
데이터 모델링 관점에서 보면, 귀납적 데이터 타입은 다른 언어에서 봉인된(sealed) 추상 클래스를 사용할 만한 상황 대부분에서 사용됩니다. C#이나 Java 같은 언어에서는 Bool을 다음과 비슷하게 정의할 수 있습니다:
abstract class Bool {}
class True : Bool {}
class False : Bool {}
하지만 이러한 표현 방식의 세부 사항은 상당히 다릅니다. 특히 추상 클래스가 아닌 각 클래스는 새로운 타입과 데이터를 할당하는 새로운 방법을 함께 만들어 냅니다. 객체 지향 예제에서 True와 False는 모두 Bool보다 더 구체적인 타입인 반면, Lean 정의는 새로운 타입 Bool 하나만 도입합니다.
음이 아닌 정수의 타입인 Nat은 귀납적 데이터 타입입니다:
inductive Nat where
| zero : Nat
| succ (n : Nat) : Nat
여기서 zero는 0을 나타내고, succ는 다른 어떤 수의 후속자를 나타냅니다. succ의 선언에 등장하는 Nat은 지금 정의되고 있는 바로 그 타입 Nat입니다. 후속자는 “하나 더 큰 수”를 뜻하므로, 5의 후속자는 6이고 32,185의 후속자는 32,186입니다. 이 정의를 사용하면 4는 Nat.succ (Nat.succ (Nat.succ (Nat.succ Nat.zero)))로 표현됩니다. 이 정의는 이름이 조금 다를 뿐 Bool의 정의와 거의 같습니다. 실질적인 차이는 succ 뒤에 (n : Nat)이 붙는다는 점 하나뿐입니다. 이는 생성자 succ가 Nat 타입의 인자를 받으며, 그 인자의 이름이 마침 n이라는 것을 나타냅니다. zero와 succ라는 이름은 자신이 속한 타입의 이름을 딴 네임스페이스 안에 있으므로, 각각 Nat.zero와 Nat.succ로 참조해야 합니다.
n과 같은 인자 이름은 Lean의 오류 메시지나 수학적 증명을 작성할 때 제공되는 피드백에 나타날 수 있습니다. Lean에는 인자를 이름으로 전달할 수 있는 선택적 문법도 있습니다. 하지만 일반적으로 인자 이름은 구조체 필드 이름만큼 API에서 큰 비중을 차지하지 않으므로, 인자 이름을 정하는 일은 구조체 필드 이름을 정하는 일보다 덜 중요합니다.
C#이나 Java에서는 Nat를 다음과 같이 정의할 수 있습니다:
abstract class Nat {}
class Zero : Nat {}
class Succ : Nat {
public Nat n;
public Succ(Nat pred) {
n = pred;
}
}
위의 Bool 예시와 마찬가지로, 이 코드는 Lean의 대응 정의보다 더 많은 타입을 정의합니다. 또한 이 예시는 Lean의 데이터 타입 생성자가 C#이나 Java의 생성자보다는 추상 클래스의 서브클래스에 훨씬 더 가깝다는 점을 잘 보여 줍니다. 여기에 나온 생성자에는 실행될 초기화 코드가 들어 있기 때문입니다.
합 타입은 TypeScript에서 문자열 태그를 사용하여 판별 유니언(discriminated union)을 인코딩하는 방식과도 비슷합니다. TypeScript에서는 Nat을 다음과 같이 정의할 수 있습니다.
interface Zero {
tag: "zero";
}
interface Succ {
tag: "succ";
predecessor: Nat;
}
type Nat = Zero | Succ;
C#이나 Java와 마찬가지로, 이 인코딩에서는 Zero와 Succ가 각각 독립된 타입이기 때문에 결과적으로 Lean보다 더 많은 타입이 생깁니다. 또한 이 인코딩은 Lean의 생성자가 JavaScript나 TypeScript에서 내용을 식별하는 태그를 포함한 객체에 대응한다는 것을 보여 줍니다.
1.5.1. 패턴 매칭
많은 언어에서는 이러한 종류의 데이터를 사용할 때 먼저 instance-of 연산자로 어떤 서브클래스를 받았는지 확인한 다음, 해당 서브클래스에서 사용할 수 있는 필드의 값을 읽습니다. instance-of 검사는 어떤 코드를 실행할지 결정하여 그 코드에 필요한 데이터가 있음을 보장하고, 필드 자체는 그 데이터를 제공합니다. Lean에서는 패턴 매칭이 이 두 가지 목적을 동시에 수행합니다.
패턴 매칭을 사용하는 함수의 한 예로 isZero가 있습니다. 이 함수는 인자가 Nat.zero이면 true를 반환하고, 그렇지 않으면 false를 반환합니다.
def isZero (n : Nat) : Bool :=
match n with
| Nat.zero => true
| Nat.succ k => false
match 표현식에는 구조 분해할 대상으로 함수의 인자 n이 주어집니다. n이 Nat.zero로 생성되었다면 패턴 매칭의 첫 번째 분기가 선택되고, 결과는 true입니다. n이 Nat.succ로 생성되었다면 두 번째 분기가 선택되고, 결과는 false입니다.
isZero Nat.zero의 평가 과정을 단계별로 보면 다음과 같습니다.
isZero 5의 평가도 이와 비슷하게 진행됩니다:
isZero의 패턴 중 두 번째 분기에 있는 k는 장식용이 아닙니다. 이것은 Nat.succ의 인자인 Nat을 주어진 이름으로 사용할 수 있게 해 줍니다. 그런 다음 그 더 작은 수를 사용하여 표현식의 최종 결과를 계산할 수 있습니다.
어떤 수 n의 후속자가 n보다 1 큰 수(즉, n + 1)인 것처럼, 어떤 수의 선행자는 그 수보다 1 작은 수입니다. pred가 Nat의 이전 수를 구하는 함수라면, 다음 예제들은 예상한 결과를 내야 합니다:
#eval pred 5#eval pred 839
Nat은 음수를 표현할 수 없으므로, Nat.zero는 다소 골치 아픈 존재입니다. 보통 Nat을 다룰 때는, 일반적으로 음수를 만들어 낼 연산자들이 zero 자체를 만들도록 재정의됩니다:
#eval pred 0
Nat의 이전 수를 구하려면 먼저 그 값을 만드는 데 어떤 생성자가 사용되었는지 확인해야 합니다. Nat.zero였다면 결과는 Nat.zero입니다. Nat.succ였다면 그 안에 있는 Nat을 가리키는 데 k라는 이름을 사용합니다. 그리고 이 Nat이 바로 구하려는 이전 수이므로, Nat.succ 분기의 결과는 k입니다.
def pred (n : Nat) : Nat :=
match n with
| Nat.zero => Nat.zero
| Nat.succ k => k
이 함수를 5에 적용하면 다음과 같은 단계를 거칩니다:
1.5.2. 재귀 함수
정의하고 있는 이름 자체를 참조하는 정의를 재귀적 정의라고 합니다. 귀납적 데이터 타입은 재귀적일 수 있습니다. 실제로 Nat도 이러한 데이터 타입의 한 예입니다. succ에는 또 다른 Nat이 필요하기 때문입니다. 재귀적 데이터 타입은 얼마든지 큰 데이터를 표현할 수 있으며, 사용 가능한 메모리 같은 기술적 요인에 의해서만 제한됩니다. 데이터 타입 정의에 자연수마다 생성자를 하나씩 적는 것이 불가능하듯이, 가능한 모든 경우마다 패턴 매칭 케이스를 하나씩 적는 것도 불가능합니다.
재귀적 데이터 타입은 재귀 함수와 잘 어울립니다. Nat에 대한 간단한 재귀 함수로 인자가 짝수인지 확인할 수 있습니다. 이 경우 Nat.zero는 짝수입니다. 이처럼 재귀하지 않는 코드 분기를 기저 사례라고 합니다. 홀수의 후속자는 짝수이고, 짝수의 후속자는 홀수입니다. 즉, Nat.succ로 만든 수는 그 인자가 짝수가 아닐 때, 그리고 오직 그때에만 짝수입니다.
def even (n : Nat) : Bool :=
match n with
| Nat.zero => true
| Nat.succ k => not (even k)
이러한 사고 패턴은 Nat에 대한 재귀 함수를 작성할 때 전형적으로 나타납니다. 먼저 Nat.zero일 때 무엇을 해야 하는지 파악합니다. 그런 다음, 임의의 Nat에 대한 결과를 그 후속자에 대한 결과로 변환하는 방법을 정하고, 이 변환을 재귀 호출의 결과에 적용합니다. 이러한 패턴을 구조적 재귀라고 합니다.
다른 많은 언어와 달리, Lean은 기본적으로 모든 재귀 함수가 결국 기저 사례에 도달하도록 보장합니다. 프로그래밍 관점에서 보면, 이 덕분에 실수로 무한 루프를 만드는 일이 없습니다. 하지만 이 기능은 정리를 증명할 때 특히 중요합니다. 정리를 증명할 때는 무한 루프가 큰 문제를 일으키기 때문입니다. 그 결과, Lean은 원래의 수에 대해 자기 자신을 재귀적으로 호출하려는 버전의 even을 받아들이지 않습니다:
def evenLoops (n : Nat) : Bool :=
match n with
| Nat.zero => true
| Nat.succ k => not (evenLoops n)오류 메시지에서 중요한 부분은 Lean이 이 재귀 함수가 항상 기저 사례에 도달한다는 것을 확인할 수 없었다는 점입니다(실제로 도달하지 않기 때문입니다).
덧셈은 인자를 두 개 받지만, 그중 하나만 검사하면 됩니다. 수 n에 0을 더하려면 n을 그대로 반환하면 됩니다. k의 후속자를 n에 더하려면, k를 n에 더한 결과의 후속자를 취하면 됩니다.
def plus (n : Nat) (k : Nat) : Nat :=
match k with
| Nat.zero => n
| Nat.succ k' => Nat.succ (plus n k')
plus의 정의에서 k'라는 이름은 인자 k와 관련은 있지만 같지는 않다는 것을 나타내기 위해 선택되었습니다. 예를 들어, plus 3 2의 평가 과정을 따라가 보면 다음과 같은 단계를 거칩니다:
plus 3 2plus 3 (Nat.succ (Nat.succ Nat.zero))match Nat.succ (Nat.succ Nat.zero) with
| Nat.zero => 3
| Nat.succ k' => Nat.succ (plus 3 k')Nat.succ (plus 3 (Nat.succ Nat.zero))Nat.succ (match Nat.succ Nat.zero with
| Nat.zero => 3
| Nat.succ k' => Nat.succ (plus 3 k'))Nat.succ (Nat.succ (plus 3 Nat.zero))Nat.succ (Nat.succ (match Nat.zero with
| Nat.zero => 3
| Nat.succ k' => Nat.succ (plus 3 k')))Nat.succ (Nat.succ 3)5
덧셈을 이해하는 한 가지 방법은 n + k가 Nat.succ를 n에 k번 적용한다고 보는 것입니다. 마찬가지로, 곱셈 n × k는 n을 자기 자신에 k번 더하는 것이고, 뺄셈 n - k는 n의 이전 수를 k번 취하는 것입니다.
def times (n : Nat) (k : Nat) : Nat :=
match k with
| Nat.zero => Nat.zero
| Nat.succ k' => plus n (times n k')def minus (n : Nat) (k : Nat) : Nat :=
match k with
| Nat.zero => n
| Nat.succ k' => pred (minus n k')
모든 함수를 구조적 재귀로 쉽게 작성할 수 있는 것은 아닙니다. 덧셈을 Nat.succ의 반복으로, 곱셈을 덧셈의 반복으로, 뺄셈을 선행자(predecessor)의 반복으로 이해하면, 나눗셈은 뺄셈을 반복해서 구현할 수 있다는 것을 알 수 있습니다. 이 경우, 피제수가 제수보다 작으면 결과는 0입니다. 그렇지 않으면, 결과는 피제수에서 제수를 뺀 값을 제수로 나눈 결과의 후속자(successor)입니다.
def div (n : Nat) (k : Nat) : Nat :=
if n < k then
0
else Nat.succ (div (n - k) k)