1.5. Datatypes and Patterns
구조체를 사용하면 서로 독립적인 여러 데이터를 일관된 전체로 묶어 완전히 새로운 타입으로 표현할 수 있다. 값의 모음을 묶는 구조체와 같은 타입을 곱 타입이라고 한다. 하지만 많은 영역 개념은 구조체로 자연스럽게 표현할 수 없다. 예를 들어 애플리케이션은 사용자 권한을 추적해야 할 수 있는데, 어떤 사용자는 문서 소유자이고 어떤 사용자는 문서를 편집할 수 있으며 다른 사용자는 읽기만 할 수 있다. 계산기에는 덧셈, 뺄셈, 곱셈과 같은 여러 이항 연산자가 있다. 구조체는 여러 선택지를 쉽게 인코딩하는 방법을 제공하지 않는다.
마찬가지로 구조체는 고정된 필드 집합을 추적하기에는 훌륭하지만, 많은 애플리케이션에는 임의 개수의 원소를 포함할 수 있는 데이터가 필요하다. 트리와 목록 같은 고전적인 자료 구조 대부분은 재귀 구조를 가진다. 목록의 꼬리 자체가 목록이거나 이진 트리의 왼쪽·오른쪽 가지 자체가 이진 트리인 식이다. 앞서 말한 계산기에서는 표현식 자체의 구조가 재귀적이다. 예를 들어 덧셈 표현식의 피연산자가 곱셈 표현식일 수 있다.
선택을 허용하는 데이터 타입을 합 타입이라고 하고 자기 자신의 인스턴스를 포함할 수 있는 데이터 타입을 재귀 데이터 타입이라고 한다. 재귀 합 타입은 그에 대한 명제를 수학적 귀납법으로 증명할 수 있으므로 귀납적 데이터 타입이라고 한다. 프로그램에서는 패턴 매칭과 재귀 함수를 통해 귀납적 데이터 타입을 소비한다.
내장 타입 중 상당수는 실제로 표준 라이브러리의 귀납적 데이터 타입이다.
예를 들어 Bool은 귀납적 데이터 타입이다:
inductive Bool where
| false : Bool
| true : Bool
이 정의는 크게 두 부분으로 이루어진다.
첫 번째 줄은 새 타입의 이름(Bool)을 제공하고 나머지 줄은 각각 생성자를 설명한다.
구조체의 생성자와 마찬가지로 귀납적 데이터 타입의 생성자는 임의의 초기화·검증 코드를 넣는 곳이 아니라 다른 데이터를 받거나 담아 두는 수동적인 그릇이다.
구조체와 달리 귀납적 데이터 타입에는 생성자가 여러 개일 수 있다.
여기에는 true와 false라는 두 생성자가 있으며 어느 것도 인수를 받지 않는다.
구조체 선언이 선언된 타입의 이름을 딴 네임스페이스에 이름을 넣듯이, 귀납적 데이터 타입은 생성자의 이름을 네임스페이스에 넣는다.
Lean 표준 라이브러리에서는 이 네임스페이스의 true와 false를 다시 내보내므로 각각 Bool.true, Bool.false라고 쓰지 않고 이름만 쓸 수 있다.
데이터 모델링 관점에서 귀납적 데이터 타입은 다른 언어에서 봉인된 추상 클래스를 사용하는 많은 상황에 사용된다.
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 타입이다.
후속 수는 “1만큼 큰 수”를 뜻하므로 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에서 문자열 태그를 사용해 구별된 유니언을 인코딩하는 것과도 비슷하다.
TypeScript에서는 Nat을 다음과 같이 정의할 수 있다:
interface Zero {
tag: "zero";
}
interface Succ {
tag: "succ";
predecessor: Nat;
}
type Nat = Zero | Succ;
이 인코딩도 C#이나 Java와 마찬가지로 Lean보다 많은 타입을 만들게 된다. Zero와 Succ가 각각 독립적인 타입이기 때문이다.
또한 Lean의 생성자가 JavaScript나 TypeScript에서 내용을 식별하는 태그를 포함한 객체에 대응한다는 점도 보여 준다.
1.5.1. Pattern Matching
많은 언어에서는 먼저 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)인 것처럼, 수의 직전 수(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로 만들어졌다면 그 아래의 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. Recursive Functions
정의 중인 이름을 참조하는 정의를 재귀 정의라고 한다.
귀납적 데이터 타입은 재귀적이어도 된다. 실제로 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은 기본적으로 모든 재귀 함수가 결국 기저 사례에 도달하도록 보장한다.
프로그래밍 관점에서는 우발적인 무한 루프를 배제한다.
무한 루프가 큰 어려움을 일으키는 정리 증명에서는 특히 중요한 기능이다.
따라서 원래 수에 대해 재귀적으로 자기 자신을 호출하려는 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가 n에 Nat.succ를 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')