플레이스홀더와 유니버스

때로는 구체적으로 알 수 없는 영역에 대해 추론해야 합니다. 예를 들어, 다음 프로그램을 살펴보십시오.

// A function that needs a static reference
fn foo(x: &'static u32) { }

fn bar(f: for<'a> fn(&'a u32)) {
       // ^^^^^^^^^^^^^^^^^^^ a function that can accept **any** reference
    let x = 22;
    f(&x);
}

fn main() {
    bar(foo);
}

이 프로그램은 타입 검사를 통과해서는 안 됩니다. foo는 인자로 정적 참조를 요구하고, bar는 어떤 참조든 받아들이는 함수를 전달받기를 원하기 때문입니다(예를 들어, 자신의 스택에 있는 값으로 그 함수를 호출할 수 있도록 하기 위해서입니다). 그렇다면 이 프로그램을 어떻게 거부하며, 왜 거부합니까?

서브타이핑과 플레이스홀더

main을 타입 검사할 때, 특히 bar(foo) 호출을 검사할 때, 결국 다음과 같은 서브타이핑 관계를 얻게 됩니다.

fn(&'static u32) <: for<'a> fn(&'a u32)
----------------    -------------------
the type of `foo`   the type `bar` expects

이러한 종류의 서브타이핑은 상위 타입에서 바인딩된 변수들을 가져와 전칭 양화된 대표자로 치환하는 방식으로 처리하며, 여기서는 이를 !1처럼 표기합니다. 이러한 영역을 “플레이스홀더 영역“이라고 부르며, 이는 기본적으로 “알 수 없는 어떤 영역“을 나타냅니다.

이 치환을 마치면 다음과 같은 관계를 얻습니다.

fn(&'static u32) <: fn(&'!1 u32)

여기서 핵심 아이디어는 이 알 수 없는 영역 '!1이 다른 어떤 영역과도 관련이 없다는 것입니다. 따라서 '!1에 대해 서브타이핑 관계가 참임을 증명할 수 있다면, 그 관계는 어떤 영역에 대해서도 참이어야 하며, 이것이 바로 우리가 원하던 바입니다.

그러면 다음에 어떤 일이 일어나는지 차례대로 살펴봅시다. 두 함수가 서브타입 관계인지 확인하기 위해, 두 함수의 인자가 원하는 관계를 가지는지 확인합니다(fn 인자는 반공변이므로 여기서는 왼쪽과 오른쪽을 바꿉니다).

&'!1 u32 <: &'static u32

참조에 대한 기본 서브타이핑 규칙에 따르면, 이는 '!1: 'static인 경우에 참이 됩니다. 즉, “알 수 없는 어떤 영역 !1“이 'static보다 오래 살아남는 경우입니다. 이는 참일 수도 있습니다. 결국 '!1이 'static일 수도 있기 때문입니다. 하지만 그것이 참이라는 것을 알지는 못합니다. 따라서 이는 (결국) 오류를 발생시켜야 합니다.

유니버스란 무엇입니까?

앞 절에서 플레이스홀더 영역이라는 개념을 소개하고, 이를 !1로 표기했습니다. 이 숫자 1을 유니버스 인덱스라고 부릅니다. “유니버스“라는 개념은 어떤 타입 안에서 또는 어떤 시점에 스코프 안에 있는 이름들의 집합을 뜻합니다. 유니버스는 트리 형태로 구성되며, 각 자식은 부모에 새로운 이름 몇 개를 추가하여 확장합니다. 따라서 루트 유니버스는 개념적으로 라이프타임 'static이나 타입 i32와 같은 전역 이름들을 포함합니다. 컴파일러에서는 제네릭 타입 매개변수도 이 루트 유니버스에 넣습니다(이런 의미에서 루트 유니버스는 하나만 있는 것이 아니라 아이템마다 하나씩 있습니다). 그러면 다음 함수 bar를 살펴보십시오.

struct Foo { }

fn bar<'a, T>(t: &'a T) {
    ...
}

여기서 루트 유니버스는 라이프타임 'static과 'a로 구성됩니다. 사실 여기서는 라이프타임에 초점을 맞추고 있지만, 같은 개념을 타입에도 적용할 수 있으며, 그 경우 타입 Foo와 T가 (i32 같은 다른 전역 타입과 함께) 루트 유니버스에 속하게 됩니다. 기본적으로 루트 유니버스는 bar의 본문에 자유롭게 나타나는 모든 이름을 포함합니다.

이제 변수 x를 추가하여 bar를 조금 확장해 봅시다.

fn bar<'a, T>(t: &'a T) {
    let x: for<'b> fn(&'b u32) = ...;
}

여기서 이름 'b는 루트 유니버스에 속하지 않습니다. 대신 이 for<'b>에 “진입“할 때(예를 들어, 이를 플레이스홀더로 치환할 때) 루트의 자식 유니버스를 생성하게 되며, 이를 U1이라고 부르겠습니다.

U0 (root universe)
│
└─ U1 (child universe)

이 자식 유니버스 U1은 루트 유니버스 U0에 새 이름 하나를 더해 확장한 것이며, 이 이름은 유니버스 번호를 사용해 !1로 식별합니다.

이제 변수 y를 하나 더 추가하여 bar를 조금 확장해 봅시다:

fn bar<'a, T>(t: &'a T) {
    let x: for<'b> fn(&'b u32) = ...;
    let y: for<'c> fn(&'c u32) = ...;
}

이 타입에 진입하면 다시 새 유니버스를 생성하며, 이를 U2라고 부르겠습니다. 이 유니버스의 부모는 루트 유니버스이고, U1은 이 유니버스의 형제가 됩니다:

U0 (root universe)
│
├─ U1 (child universe)
│
└─ U2 (child universe)

이는 U2 안에 있는 동안 U0나 U2에 속한 것은 이름으로 지칭할 수 있지만 U1에 속한 것은 지칭할 수 없다는 뜻입니다.

존재 변수에 유니버스 부여하기. 이제 유니버스라는 개념이 생겼으므로, 이를 사용해 타입 검사기 등을 확장하여 허용되지 않은 이름이 밖으로 새어 나가지 않도록 막을 수 있습니다. 핵심은 타입이든 라이프타임이든 각 추론(존재) 변수에 유니버스를 하나씩 부여한다는 것입니다. 그러면 그 변수의 값은 해당 유니버스에서 보이는 이름만 참조할 수 있습니다. 예를 들어 라이프타임 변수가 U0에서 생성되었다면, 그 변수에는 !1이나 !2 값을 할당할 수 없습니다. 이 이름들은 유니버스 U0에서 보이지 않기 때문입니다.

카운터 하나만으로 유니버스 표현하기. 컴파일러가 유니버스의 전체 트리를 추적하지 않는다는 사실에 놀라실 수도 있습니다. 대신 컴파일러는 카운터 하나만 유지하며, 한 유니버스가 다른 유니버스를 볼 수 있는지 판단할 때는 인덱스가 더 큰지만 확인합니다. 예를 들어 2 >= 0이므로 U2는 U0를 볼 수 있습니다. 하지만 0 >= 2는 거짓이므로 U0는 U2를 볼 수 없습니다.

어떻게 이렇게 해도 문제가 없는 것입니까? 이렇게 하면 U2가 U1도 볼 수 있게 허용하는 것이 아닙니까? 답은, 그렇습니다. 그런 질문이 실제로 제기된다면 허용하게 됩니다. 하지만 타입 검사기 등의 구조상 그런 일이 일어날 방법이 없습니다. 유니버스 U1에서 일어나는 무언가가 U2에서 일어나는 무언가와 “소통“하려면, 둘이 공통으로 공유하는 추론 변수 X가 있어야 합니다. 그리고 U1의 모든 것은 U1과 그 자식으로만 범위가 한정되므로, 그 추론 변수 X는 U0에 있어야 합니다. 그리고 X가 U0에 있으므로, X는 U1(또는 U2)의 어떤 것도 이름으로 지칭할 수 없습니다. 이는 일종의 제네릭한 “논리” 예제를 사용하면 가장 쉽게 이해할 수 있을 것입니다.

exists<X> {
   forall<Y> { ... /* Y is in U1 ... */ }
   forall<Z> { ... /* Z is in U2 ... */ }
}

여기서 두 forall이 상호 작용할 수 있는 유일한 방법은 X를 통하는 것이지만, X가 선언될 때 Y와 Z는 모두 스코프 안에 있지 않으므로 X의 값은 둘 중 어느 것도 참조할 수 없습니다.

유니버스와 플레이스홀더 영역 요소

그렇다면 그 오류는 어디에서 비롯됩니까? 그 과정은 다음과 같습니다. 영역 추론 컨텍스트를 구성할 때, 타입 추론 컨텍스트로부터 플레이스홀더 변수가 몇 개 존재하는지 알 수 있습니다(InferCtxt에는 내부 카운터가 있습니다). 각 플레이스홀더 변수에 대해 대응하는 보편 영역 변수 !n과 “영역 요소” placeholder(n)을 생성합니다. 이는 “알 수 없는 다른 요소들의 어떤 집합“에 해당합니다. !n의 값은 {placeholder(n)}입니다.

동시에 각 존재 변수에도 유니버스를 부여합니다(이 역시 InferCtxt에서 가져옵니다). 이 유니버스는 변수의 값에 어떤 플레이스홀더 요소가 나타날 수 있는지를 결정합니다. 예를 들어 유니버스 U3에 있는 변수는 placeholder(1), placeholder(2), placeholder(3)은 지칭할 수 있지만 placeholder(4)는 지칭할 수 없습니다. 추론 변수의 유니버스는 그 값에 어떤 리전 요소가 나타날 수 있는지를 제어할 뿐이며, 리전 요소가 반드시 나타난다는 뜻은 아니라는 점에 유의하십시오.

플레이스홀더와 outlives 제약 조건

영역 추론 엔진에서 outlives 제약 조건은 다음과 같은 형태를 가집니다:

V1: V2 @ P

여기서 V1과 V2는 영역 인덱스이므로 어떤 영역 변수(전칭 양화 또는 존재 양화될 수 있음)에 대응됩니다. 여기서 P는 제어 흐름 그래프의 “지점“이며, 이 절에서는 중요하지 않습니다. 이 변수는 유니버스를 가지므로, 그 유니버스들을 각각 U(V1)과 U(V2)라고 부릅시다. (사실 우리가 신경 쓸 것은 U(V1)뿐입니다.)

이 제약 조건을 만나면, 일반적인 절차는 P에서 DFS를 시작하는 것입니다. 순회 중인 노드가 value(V2)에 존재하는 한 계속 순회하며, 그 노드들을 value(V1)에 추가합니다. 반환 지점에 도달하면 모든 end(X) 요소를 추가합니다. 이 부분은 변경되지 않습니다.

하지만 그 다음에는 V2에 있는 플레이스홀더 placeholder(x) 요소들을 순회하려고 합니다(각 요소는 U(V2)에서 보여야 하지만, 이는 확인할 필요 없이 참이라고 그냥 가정할 수 있어야 합니다). value(V1)이 각 플레이스홀더 요소보다 오래 살아남도록 보장해야 합니다.

이제 이것이 일어날 수 있는 방법은 두 가지입니다. 첫째, U(V1)이 유니버스 x를 볼 수 있다면(즉, x <= U(V1)이라면), placeholder(x)를 value(V1)에 추가하기만 하면 됩니다. 그렇지 않다면 근사해야 합니다. placeholder(x)가 어떤 요소 집합을 나타내는지 모를 수도 있지만, 그에 대한 일종의 상한 B, 즉 placeholder(x)보다 오래 살아남는 어떤 영역 B는 계산할 수 있어야 합니다. 지금은 이를 위해 그냥 'static을 사용합니다(모든 것보다 오래 살아남기 때문입니다). 앞으로는 여기서 때때로 더 똑똑하게 처리할 수 있을 것입니다(실제로 다른 맥락에서는 이미 이를 수행하는 코드가 있습니다). 또한 'static은 루트 유니버스 U0에 있으므로 모든 변수가 이를 볼 수 있음을 압니다. 따라서 기본적으로 V1이 볼 수 없는 어떤 유니버스 x에 대해 value(V2)가 placeholder(x)를 포함한다는 것을 발견하면, V1을 'static으로 강제합니다.

“보편 영역” 검사 확장하기

모든 제약이 전파된 후, NLL 영역 추론은 마지막 검사를 하나 수행합니다. 이 검사에서는 각 보편 영역에 대해 최종적으로 계산된 값들을 살펴보고, 그 값들이 ‘너무 커지지’ 않았는지 확인합니다. 우리의 경우에는 각 플레이스홀더 영역을 살펴보면서, 해당 영역이 outlive한다고 알려진 placeholder(u) 요소만 포함하는지 확인합니다. (나중에는 두 플레이스홀더 영역 사이에 관계가 있음을 알아내어 이를 고려할 수 있게 될지도 모릅니다. fn 시그니처에서 오는 보편 영역에 대해 그렇게 하는 것처럼 말입니다.)

다르게 말하면, “보편 영역” 검사는 다음과 같은 제약을 검사하는 것으로 볼 수 있습니다.

{placeholder(1)}: V1

여기서 {placeholder(1)}은 상수 집합과 같고, V1은 !1 영역을 나타내기 위해 만든 변수입니다.

예제로 돌아가기

좋습니다, 지금까지는 순조롭습니다. 이제 첫 번째 예제에서 어떤 일이 일어나는지 살펴봅시다:

fn(&'static u32) <: fn(&'!1 u32) @ P  // this point P is not imp't here

영역 추론 엔진은 다음과 같은 영역 요소 도메인을 생성합니다:

{ CFG; end('static); placeholder(1) }
  ---  ------------  ------- from the universe `!1`
  |    'static is always in scope
  all points in the CFG; not especially relevant here

이 엔진은 항상 두 개의 전칭 변수를 생성하는데, 하나는 'static을 나타내고 다른 하나는 '!1을 나타냅니다. 이들을 Vs와 V1이라고 부릅시다. 이들은 다음과 같은 초기값을 가집니다:

Vs = { CFG; end('static) } // it is in U0, so can't name anything else
V1 = { placeholder(1) }

위의 서브타이핑 제약 조건으로부터 다음과 같은 outlives 제약 조건을 얻게 됩니다

'!1: 'static @ P

이를 처리하기 위해 V1의 값을 Vs 전체를 포함하도록 키웁니다:

Vs = { CFG; end('static) }
V1 = { CFG; end('static), placeholder(1) }

이 시점에서 모든 outlives 관계가 충족되므로 제약 전파가 완료됩니다. 그런 다음 코드의 “보편 영역 검사” 부분으로 넘어가며, 이 부분에서는 어떤 보편 영역도 너무 커지지 않았는지 테스트합니다.

이 경우 V1은 실제로 너무 커졌습니다. V1은 end('static)보다 오래 산다고 알려져 있지 않고 CFG의 어느 부분보다도 오래 산다고 알려져 있지 않으므로 오류를 보고하게 됩니다.

또 다른 예입니다.

다음 서브타이핑 관계는 어떻습니까?

for<'a> fn(&'a u32, &'a u32)
    <:
for<'b, 'c> fn(&'b u32, &'c u32)

여기서는 이전과 마찬가지로 상위 타입의 바운드 영역을 플레이스홀더로 대체하며, 그 결과는 다음과 같습니다:

for<'a> fn(&'a u32, &'a u32)
    <:
fn(&'!1 u32, &'!2 u32)

그런 다음 좌변의 변수를 유니버스 U2의 존재 변수로 인스턴스화하며, 그 결과는 다음과 같습니다(?n은 존재 변수를 나타내는 표기입니다):

fn(&'?3 u32, &'?3 u32)
    <:
fn(&'!1 u32, &'!2 u32)

그런 다음 이것을 더 분해합니다:

&'!1 u32 <: &'?3 u32
&'!2 u32 <: &'?3 u32

그리고 더 분해하여 영역 제약 조건을 도출합니다:

'!1: '?3
'!2: '?3

이 경우 '!1과 '!2는 모두 변수 '?3보다 오래 살아야 하지만, 변수 '?3은 다른 어떤 것보다도 오래 살도록 강제되지 않는다는 점에 유의하십시오. 따라서 이 변수는 단순히 빈 원소 집합으로 시작하고 끝나며, 그러므로 여기서는 타입 검사가 성공합니다.

(이 결과는 조금 놀라울 것입니다. 저도 이 사실을 처음 깨달았을 때 놀랐습니다. 즉, 우리가 두 인자가 모두 같은 영역을 가져야 하는 fn이라면, 서로 다른 두 영역을 가진 인자로 호출되는 것을 받아들일 수 있다는 뜻입니다. 이는 직관적으로 건전하지 않아 보입니다. 하지만 실제로는 문제가 없으며, 이는 제가 오래전에 Rust 이슈 트래커의 이 이슈에서 설명하려 했던 바와 같습니다. 그 이유는 서로 다른 두 라이프타임의 인자로 호출되더라도 두 라이프타임에는 어떤 교집합(호출 자체)이 존재하며, 그 교집합을 인자들의 공통 라이프타임으로 사용하는 'a의 값으로 삼을 수 있기 때문입니다. -nmatsakis)

마지막 예제

마지막 예제를 하나 살펴봅시다. 이전 예제에 반환 타입을 추가하여 확장하겠습니다:

for<'a> fn(&'a u32, &'a u32) -> &'a u32
    <:
for<'b, 'c> fn(&'b u32, &'c u32) -> &'b u32

이전 예제와 매우 비슷해 보이지만, 이 경우에는 오류가 발생합니다. 이는 바람직한 결과입니다. 문제는 두 인자 중 하나를 반환하겠다고 약속하는 fn에서 첫 번째 인자를 반환하겠다고 약속하는 fn으로 바뀌었다는 점입니다. 이는 건전하지 않습니다. 이것이 어떻게 진행되는지 살펴봅시다.

먼저 상위 타입의 바운드 영역을 플레이스홀더로 대체합니다:

for<'a> fn(&'a u32, &'a u32) -> &'a u32
    <:
fn(&'!1 u32, &'!2 u32) -> &'!1 u32

그런 다음 서브타입을 (U2 안의) 존재 변수로 인스턴스화합니다.

fn(&'?3 u32, &'?3 u32) -> &'?3 u32
    <:
fn(&'!1 u32, &'!2 u32) -> &'!1 u32

이제 서브타이핑 관계를 생성합니다:

&'!1 u32 <: &'?3 u32 // arg 1
&'!2 u32 <: &'?3 u32 // arg 2
&'?3 u32 <: &'!1 u32 // return type

마지막으로 outlives 관계입니다. 여기서 V1, V2, V3를 각각 !1, !2, ?3에 할당하는 변수라고 합시다:

V1: V3
V2: V3
V3: V1

이 변수들은 다음과 같은 초깃값을 갖습니다:

V1 in U1 = {placeholder(1)}
V2 in U2 = {placeholder(2)}
V3 in U2 = {}

이제 V3: V1 제약 조건 때문에 placeholder(1)을 V3에 추가해야 하며(실제로 이는 V3에서 보입니다), 그 결과는 다음과 같습니다:

V3 in U2 = {placeholder(1)}

그런 다음 V2: V3 제약 조건이 있으므로, 결국 V2를 확장하여 placeholder(1)을 포함하도록 해야 합니다(V2에서도 이것이 보입니다):

V2 in U2 = {placeholder(1), placeholder(2)}

이제 제약 전파는 완료되었지만, outlives 관계를 검사할 때 V2에 새로운 요소 placeholder(1)이 포함되어 있음을 발견하므로 오류를 보고합니다.