1.5. 데이터 타입과 패턴
구조체를 사용하면 서로 독립적인 여러 데이터 조각을 완전히 새로운 타입으로 표현되는 하나의 일관된 전체로 결합할 수 있습니다. 여러 값의 모음을 하나로 묶는 구조체와 같은 타입을 product type이라 부릅니다. 하지만 많은 도메인 개념은 구조체로 자연스럽게 표현할 수 없습니다. 예를 들어, 애플리케이션은 사용자 권한을 추적해야 할 수 있는데, 이때 일부 사용자는 문서 소유자이고, 일부는 문서를 편집할 수 있으며, 다른 일부는 읽기만 할 수 있습니다. 계산기에는 덧셈, 뺄셈, 곱셈과 같은 여러 가지 이항 연산자가 있습니다. 구조체는 여러 선택지를 인코딩하는 쉬운 방법을 제공하지 않습니다.
마찬가지로, 구조체는 고정된 필드 집합을 관리하는 데 훌륭한 방법이지만, 많은 애플리케이션은 임의 개수의 원소를 포함할 수 있는 데이터를 필요로 합니다. 트리와 리스트 같은 대부분의 고전적인 자료 구조는 재귀적인 구조를 가지고 있으며, 리스트의 꼬리는 그 자체로 리스트이고, 이진 트리의 왼쪽 및 오른쪽 가지는 그 자체로 이진 트리입니다. 앞서 언급한 계산기에서는 표현식 자체의 구조가 재귀적입니다. 예를 들어, 덧셈 표현식의 피가산수 자체가 곱셈 표현식일 수도 있습니다.
선택을 허용하는 데이터 타입을 합 타입(sum types)이라 부르며, 자기 자신의 인스턴스를 포함할 수 있는 데이터 타입을 재귀적 데이터 타입(recursive datatypes)이라 부릅니다. 재귀적 합 타입은 귀납적 데이터 타입이라고 불리는데, 이는 수학적 귀납법을 사용하여 이에 대한 명제를 증명할 수 있기 때문입니다. 프로그래밍할 때 귀납적 타입은 패턴 매칭과 재귀 함수를 통해 소비됩니다.
내장 타입 중 다수는 실제로 표준 라이브러리에 있는 귀납적 타입입니다. 예를 들어, Bool은 귀납적 데이터타입입니다:
inductive Bool where
| false : Bool
| true : Bool
이 정의는 두 개의 주요 부분으로 이루어져 있습니다. 첫 번째 줄은 새 타입(Bool)의 이름을 제공하며, 나머지 각 줄은 생성자를 설명합니다. 구조체의 생성자와 마찬가지로, 귀납적 데이터 타입의 생성자 또한 임의의 초기화 및 검증 코드를 삽입하는 자리가 아니라, 다른 데이터를 받아들이고 담아내는 단순한 비활성 수용체이자 컨테이너일 뿐입니다. 구조체와 달리, 귀납적 타입은 여러 개의 생성자를 가질 수 있습니다. 여기에는 true와 false라는 두 개의 생성자가 있으며, 둘 다 인자를 받지 않습니다. 구조체 선언이 자신의 이름들을 선언된 타입의 이름을 딴 네임스페이스에 배치하는 것과 마찬가지로, 귀납적 타입도 생성자의 이름들을 네임스페이스에 배치합니다. Lean 표준 라이브러리에서 true와 false는 각각 Bool.true와 Bool.false로 쓰는 대신 단독으로 쓸 수 있도록 이 네임스페이스에서 다시 내보내집니다.
데이터 모델링의 관점에서, 귀납적 데이터 타입은 다른 언어에서 봉인된 추상 클래스(sealed abstract class)가 사용될 법한 것과 동일한 많은 문맥에서 사용됩니다. 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는 다른 어떤 수의 successor를 나타냅니다. succ의 선언에 언급된 Nat은 현재 정의되고 있는 바로 그 Nat 타입입니다. successor는 “~보다 1 큰 수”를 의미하므로, 5의 successor는 6이고 32,185의 successor는 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 연산자를 사용해 어떤 서브클래스를 받았는지 확인한 다음, 해당 서브클래스에서 사용 가능한 필드의 값을 읽는 방식으로 사용됩니다. 인스턴스 여부 검사는 어떤 코드를 실행할지 결정하며, 이 코드에 필요한 데이터가 사용 가능한지 보장합니다. 한편 필드 자체는 해당 데이터를 제공합니다. 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의 successor(다음 수)가 n보다 1 큰 수(즉, n + 1)인 것과 마찬가지로, 어떤 수의 predecessor(이전 수)는 그 수보다 1 작은 수입니다. pred가 Nat의 선행자를 찾는 함수라면, 다음 예제들이 예상되는 결과를 찾아야 합니다:
#eval pred 5#eval pred 839
Nat은 음수를 표현할 수 없으므로, Nat.zero는 약간의 난제입니다. 일반적으로 Nat을 다룰 때는, 보통이라면 음수를 산출했을 연산자들이 zero 자신을 산출하도록 재정의됩니다:
#eval pred 0
Nat의 선행자를 찾으려면, 첫 번째 단계는 어떤 생성자가 이를 만드는 데 사용되었는지 확인하는 것입니다. 만약 Nat.zero였다면, 결과는 Nat.zero입니다. 만약 Nat.succ였다면, 이름 k는 그 아래에 있는 Nat을 가리키는 데 사용됩니다. 그리고 이 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는 짝수입니다. 이와 같이 재귀적이지 않은 코드 분기를 기저 사례(base case)라고 합니다. 홀수의 다음 수는 짝수이고, 짝수의 다음 수는 홀수입니다. 즉, Nat.succ로 만들어진 숫자는 그 인자가 짝수가 아닌 경우에만 짝수입니다.
def even (n : Nat) : Bool :=
match n with
| Nat.zero => true
| Nat.succ k => not (even k)
이러한 사고 패턴은 Nat에 대한 재귀 함수를 작성할 때 전형적으로 나타나는 것입니다. 먼저, Nat.zero에 대해 무엇을 해야 할지 파악합니다. 그런 다음, 임의의 Nat에 대한 결과를 그 후행자에 대한 결과로 변환하는 방법을 결정하고, 이 변환을 재귀 호출의 결과에 적용합니다. 이 패턴을 구조적 재귀라고 부릅니다.
많은 언어들과 달리, Lean은 기본적으로 모든 재귀 함수가 결국 기저 사례에 도달함을 보장합니다. 프로그래밍의 관점에서 볼 때, 이는 의도치 않은 무한 루프를 배제합니다. 하지만 이 기능은 정리를 증명할 때 특히 중요한데, 이때 무한 루프는 심각한 문제를 야기합니다. 이로 인한 결과로, 원래 숫자에 대해 재귀적으로 자기 자신을 호출하려 시도하는 버전의 even은 Lean이 받아들이지 않습니다:
def evenLoops (n : Nat) : Bool :=
match n with
| Nat.zero => true
| Nat.succ k => not (evenLoops n)이 오류 메시지에서 중요한 부분은 Lean이 이 재귀 함수가 항상 기저 사례에 도달한다는 것을 판단할 수 없었다는 점입니다(실제로 그렇지 않기 때문입니다).
더하기가 두 개의 인자를 받기는 하지만, 그중 하나만 검사하면 됩니다. 숫자 n에 0을 더하려면, 그냥 n을 반환합니다. n에 k의 후행자를 더하려면, n에 k를 더한 결과의 후행자를 취합니다.
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')