논리로 로워링하기

여기서 핵심적인 관찰은 Rust 트레이트 시스템이 기본적으로 일종의 논리이며, 표준 논리 추론 규칙으로 대응시킬 수 있다는 점입니다. 그러면 예를 들어 Prolog 솔버가 동작하는 방식과 매우 유사한 방식으로 그 추론 규칙들의 해를 찾을 수 있습니다. 알고 보면 Prolog 규칙(혼 절(Horn clause)이라고도 합니다)을 그대로 사용할 수는 없고, 그보다 표현력이 다소 더 높은 변형이 필요합니다.

Rust 트레이트와 논리

가장 먼저 짚어 볼 점 중 하나는 Rust 트레이트 시스템이 기본적으로 일종의 논리라는 것입니다. 따라서 구조체, 트레이트, impl 선언을 논리 추론 규칙으로 대응시킬 수 있습니다. 대부분의 경우 이것들은 기본적으로 혼 절이지만, Rust의 풍부한 표현력을 온전히 담아내려면(특히 제네릭 프로그래밍을 지원하려면) 표준 혼 절보다 조금 더 나아가야 한다는 것을 보게 될 것입니다.

이 대응이 어떻게 동작하는지 알아보기 위해 예제부터 시작합시다. 다음과 같이 트레이트 하나와 impl 몇 개를 선언한다고 가정해 보십시오.

#![allow(unused)]
fn main() {
trait Clone { }
impl Clone for usize { }
impl<T> Clone for Vec<T> where T: Clone { }
}

이 선언들을 Prolog와 비슷한 표기법으로 작성한 몇 개의 혼 절로 다음과 같이 대응시킬 수 있습니다.

Clone(usize).
Clone(Vec<?T>) :- Clone(?T).

// The notation `A :- B` means "A is true if B is true".
// Or, put another way, B implies A.

Prolog 용어로 말하자면, Clone(Foo)(여기서 Foo는 어떤 Rust 타입입니다)는 타입 Foo가 Clone을 구현한다는 개념을 나타내는 술어라고 할 수 있습니다. 이 규칙들은 프로그램 절이며, 해당 술어가 증명될 수 있는(즉, 참으로 간주되는) 조건을 기술합니다. 따라서 첫 번째 규칙은 단순히 “usize에 대해 Clone이 구현되어 있다“라고 말합니다. 다음 규칙은 “임의의 타입 ?T에 대해, ?T에 clone이 구현되어 있으면 Vec<?T>에 Clone이 구현되어 있다“라고 말합니다. 따라서 예를 들어 Clone(Vec<Vec<usize>>)를 증명하고 싶다면, 다음과 같이 규칙을 재귀적으로 적용하여 증명합니다.

• Clone(Vec<Vec<usize>>)는 다음 조건에서 증명 가능합니다.
  • Clone(Vec<usize>)는 다음 조건에서 증명 가능합니다.
    • Clone(usize)가 증명 가능합니다. (실제로 증명 가능하므로 아무 문제가 없습니다.)

그런데 이번에는 Clone(Vec<Bar>)를 증명하려 한다고 가정해 봅시다. 이는 실패합니다(애초에 Bar에 대한 Clone의 impl을 제공하지 않았기 때문입니다).

• Clone(Vec<Bar>)는 다음 조건에서 증명 가능합니다.
  • Clone(Bar)가 증명 가능합니다. (하지만 적용 가능한 규칙이 없으므로 증명 가능하지 않습니다.)

위의 예제를 입력 타입이 둘 이상인 제네릭 트레이트까지 다루도록 쉽게 확장할 수 있습니다. 그러면 Self가 타입 T의 값과 동등 비교가 가능함을 선언하는 Eq<T> 트레이트를 생각해 보십시오.

trait Eq<T> { ... }
impl Eq<usize> for usize { }
impl<T: Eq<U>> Eq<Vec<U>> for Vec<T> { }

이는 다음과 같이 대응시킬 수 있습니다.

Eq(usize, usize).
Eq(Vec<?T>, Vec<?U>) :- Eq(?T, ?U).

여기까지는 순조롭습니다.

일반 함수의 타입 검사

자, 이제 트레이트가 언제 구현되는지 표현하고 연관 타입을 처리할 수 있는 논리 규칙들을 정의했으니, 타입 검사로 관심을 조금 돌려 봅시다. 타입 검사가 흥미로운 이유는 바로 타입 검사가 우리가 증명해야 할 목표를 제공하기 때문입니다. 즉, 지금까지 살펴본 모든 내용은 프로그램의 트레이트와 impl로부터 목표를 증명하는 데 쓰이는 규칙을 어떻게 도출하는지에 관한 것이었습니다. 하지만 우리는 증명해야 할 목표를 어떻게 도출하는지에도 관심이 있으며, 그 목표는 타입 검사에서 나옵니다.

여기 있는 함수 foo()의 타입 검사를 생각해 보십시오.

fn foo() { bar::<usize>() }
fn bar<U: Eq<U>>() { }

물론 이 함수는 매우 단순합니다. 하는 일이라고는 bar::<usize>()를 호출하는 것뿐입니다. 이제 bar()의 정의를 보면, where 절 U: Eq<U> 하나가 있음을 알 수 있습니다. 따라서 foo()는 usize를 타입 인자로 하여 bar()를 호출할 수 있음을 보이려면 usize: Eq<usize>임을 증명해야 합니다.

원한다면 bar()를 호출할 수 있는 조건을 정의하는 Prolog 술어를 작성할 수도 있습니다. 이러한 조건을 만족하는 것을 “적격(well-formed)“이라고 부르겠습니다.

barWellFormed(?U) :- Eq(?U, ?U).

그러면 bar::<usize>에 대한 참조(즉, usize 타입에 적용된 bar())가 적격이라면 foo()가 타입 검사를 통과한다고 말할 수 있습니다.

fooTypeChecks :- barWellFormed(usize).

목표 fooTypeChecks를 증명하려고 하면 성공합니다.

• fooTypeChecks는 다음 조건이 성립하면 증명 가능합니다.
  • barWellFormed(usize), 이는 다음 조건이 성립하면 증명 가능합니다.
    • Eq(usize, usize), 이는 impl이 있으므로 증명 가능합니다.

좋습니다. 여기까지는 순조롭습니다. 이제 더 복잡한 함수의 타입 검사로 넘어갑시다.

제네릭 함수의 타입 검사: 혼 절을 넘어서

앞 절에서는 (Rust의 타입 동등성 개념으로 보강한) 표준 Prolog 혼 절을 사용하여 몇 가지 간단한 Rust 함수를 타입 검사했습니다. 하지만 이 방법은 제네릭이 아닌 함수, 즉 제네릭 함수가 아닌 함수를 타입 검사할 때만 통합니다. 제네릭 함수를 타입 검사하려면 Prolog가 제공하는 것보다 더 강력한 목표 개념이 필요하다는 것이 드러납니다. 무슨 말인지 알아보기 위해, 앞의 예제를 고쳐 foo를 제네릭으로 만들어 봅시다.

fn foo<T: Eq<T>>() { bar::<T>() }
fn bar<U: Eq<U>>() { }

foo의 본문을 타입 검사하려면 타입 T를 “추상적“으로 유지할 수 있어야 합니다. 즉, foo의 본문이 어떤 특정 타입에 대해서만이 아니라 모든 타입 T에 대해 타입 안전한지 확인해야 합니다. 이를 다음과 같이 표현할 수 있습니다.

fooTypeChecks :-
  // for all types T...
  forall<T> {
    // ...if we assume that Eq(T, T) is provable...
    if (Eq(T, T)) {
      // ...then we can prove that `barWellFormed(T)` holds.
      barWellFormed(T)
    }
  }.

여기서 사용하는 표기법은 제가 프로토타입 구현에서 사용해 온 표기법으로, 표준 수학 표기법과 비슷하지만 약간 Rust식으로 바꾼 것입니다. 어쨌든 문제는 표준 혼 절이 목표 안에 전칭 양화(forall)나 함의(if)를 허용하지 않는다는 것입니다(많은 Prolog 엔진이 확장 기능으로 이를 지원하기는 합니다). 이러한 이유로 “1차 유전 해롭(first-order hereditary harrop)”(FOHH) 절이라는 것을 받아들여야 합니다. 이 긴 이름은 기본적으로 “본문에 forall과 if가 있는 표준 혼 절“을 의미합니다. 하지만 정식 이름을 알아 두면 좋습니다. FOHH 절을 효율적으로 처리하는 방법을 다룬 연구가 많기 때문입니다. 예를 들어 Chalk Book의 참고 문헌에 있는 Gopalan Nadathur의 훌륭한 논문 “A Proof Procedure for the Logic of Hereditary Harrop Formulas”를 참고하십시오.

FOHH를 지원하는 것은 사실 그리 어렵지 않습니다. 그리고 일단 이를 지원할 수 있게 되면, foo와 같은 제네릭 함수의 타입 검사 규칙을 우리 논리로 쉽게 기술할 수 있습니다.

출처

이 페이지는 Nicholas Matsakis의 블로그 글을 약간 수정한 것입니다.