라이프타임 없이 하는 대여 검사 · baby steps

이 글은 Rust의 타입 시스템을 라이프타임을 버리고 대신 플레이스(places)에 기반해 재구성하는 대안을 탐구한다. TL;DR은 다음과 같다. 코드에서 'a가 _라이프타임_을 나타내는 대신, shared(a.b.c)나 mut(x) 같은 _대여(loan)의 집합_을 나타낼 수 있다는 것이다. 익숙하게 들린다면 맞다. 이는 polonius의 기초이지만, 정적 분석이 아닌 타입 시스템으로 재정식화한 버전이다. 이 글은 높은 수준의 아이디어만을 다룬다. 후속 글에서는 내부 참조 등 더 진보된 대여 패턴을 어떻게 지원할 수 있는지 파고들 예정이다. 구현 측면에서 약간의 모형을 만들어봤고, a-mir-formality를 확장하여 이 분석을 포함시키기 시작할 생각이다.

Why would you want to replace lifetimes?

라이프타임은 Rust의 최고이자 최악의 부분이다. 최고인 이유는 자료구조 중간 어딘가에 있는 데이터에 대한 포인터를 반환하는 등 아주 멋진 패턴을 표현할 수 있게 해주기 때문이다. 하지만 상당한 문제가 있다. 우선 라이프타임이라는 개념 자체가 꽤 추상적이어서 사람들이 이해하기 어렵다(“'a는 실제로 무엇을 나타내는가?”). 또한 Rust는 일부 중요한 패턴, 특히 구조체의 한 필드가 다른 필드가 소유한 데이터를 참조하는 내부 참조(interior references)를 제대로 표현하지 못한다.

So what is a lifetime exactly?

다음은 비-렉시컬 라이프타임(NLL) RFC에 나오는 라이프타임의 정의다:

차용을 만들 때마다, 컴파일러는 그 결과 레퍼런스에 라이프타임을 부여한다. 이 라이프타임은 그 레퍼런스를 사용할 수 있는 코드 구간(span)에 대응한다. 컴파일러는 레퍼런스의 모든 사용을 포괄하면서도 가능한 한 가장 작은 라이프타임으로 이를 유추한다.

자세한 내용은 RFC를 참고하라.

Replacing a lifetime with an origin

이 재정식화에서 'a는 더 이상 _라이프타임_이 아니라 오리진(origin), 즉 그 레퍼런스가 어디에서 왔는지를 설명하는 값이 된다. 오리진은 대여(loan)의 집합으로 정의한다. 각 대여는 어떤 장소 표현(place expression)(예: a나 a.b.c)이 어떤 모드(shared 또는 mut)로 차용되었는지를 담는다.

Origin = { Loan }

Loan = shared(Place)
     | mut(Place)

Place = variable(.field)*  // 예: a.b.c

Defining types

오리진을 이용해 Rust 타입을 대략 다음과 같이 정의할 수 있다(물론 여기서는 많은 복잡성을 생략한다…):

Type = TypeName < Generic* >
     | & Origin Type
     | & Origin mut Type
     
TypeName = u32 (당분간 다른 스칼라는 무시)
         | ()  (단위 타입, 튜플은 일단 신경 쓰지 말자)
         | StructName
         | EnumName
         | UnionName

Generic = Type | Origin

여기서 주목할 첫 번째 흥미로운 점은, 'a 표기가 없다는 것이다! 아직 제네릭을 도입하지 않았기 때문이다. 실제 Rust와 달리, 이 타입 시스템에서는 'a가 의미하는 바를 구체적으로 표현하는 문법(Origin)이 존재한다.

Explicit types for a simple program

완전히 명시적인 타입 시스템이 있으면 모든 타입이 완전히 지정된 예제 프로그램을 쉽게 작성할 수 있다. 예전에는 라이프타임을 표기할 방법이 없어 꽤 어려웠다. 오류가 나야 마땅한 간단한 예제를 보자:

let mut counter: u32 = 22_u32;
let p: & /*{shared(counter)}*/ u32 = &counter;
//       ---------------------
//       현재는 이를 표현하는 문법이 없음!
counter += 1; // 오류: `p`가 살아 있는 동안 `counter`는 변경할 수 없음
println!("{p}");

p의 타입을 제외하면, 이는 유효한 Rust 코드다. 물론 컴파일은 되지 않는다. 라이브한(shared) 참조 p가 있는 동안 counter를 수정할 수 없기 때문이다(playground). 계속해서, 새로운 타입 시스템 정식화가 어떻게 동일한 결론에 도달하는지 보게 될 것이다.

Basic typing judgments

타이핑 판단식(typing judgment)은 타입 시스템을 설명하는 표준 방식이다. 여기서는 우리의 시스템을 위한 판단식을 점진적으로 도입한다. 먼저 차용 검사를 포함하지 않는, 단순하고 꽤 표준적인 정식화에서 시작하여, 이후 차용 검사를 어떻게 도입하는지 보일 것이다. 첫 번째 버전에서 정의하는 판단식의 형태는 다음과 같다.

Env |- Expr : Type

이는 “환경 Env에서, 표현식 Expr는 합법이며 타입 Type을 가진다”는 뜻이다. 여기서 환경 Env는 스코프 내의 지역 변수를 정의한다. 샘플 프로그램에서 살펴볼 Rust 표현식은 꽤 단순하다:

Expr = 정수 리터럴 (예: 22_u32)
     | & Place
     | Expr + Expr
     | Place (플레이스의 값을 읽음)
     | Place = Expr (플레이스의 값을 덮어씀)
     | ...

스칼라 타입으로 u32만 지원하므로, Expr + Expr에 대한 판단식은 다음처럼 단순하다:

Env |- Expr1 : u32
Env |- Expr2 : u32
----------------------------------------- addition
Env |- Expr1 + Expr2 : u32

Place = Expr 대입 규칙은 서브타이핑에 기반한다:

Env |- Expr : Type1
Env |- Place : Type2
Env |- Type1 <: Type2
----------------------------------------- assignment
Env |- Place = Expr : ()

&Place에 대한 규칙은 좀 더 흥미롭다:

Env |- Place : Type
----------------------------------------- shared references
Env |- & Place : & {shared(Place)} Type

이 규칙은 차용되는 플레이스 Place의 타입을 구한 다음(여기서는 플레이스가 counter이고, 타입은 u32가 될 것이다) 그 타입에 대한 레퍼런스를 얻는다고 말한다. 레퍼런스의 오리진은 {shared(Place)}가 되며, 이는 그 레퍼런스가 Place에서 비롯되었음을 나타낸다:

&{shared(Place)} Type

Computing liveness

차용 검사를 도입하려면 라이브니스(liveness), 곧 생존성 개념을 단계적으로 도입해야 한다.1 익숙하지 않다면, NLL RFC의 좋은 소개를 참고하라:

“라이브니스”라는 용어는 컴파일러 분석에서 비롯되었지만 꽤 직관적이다. 어떤 변수가 보유한 현재 값이 이후에 사용될 수 있다면, 그 변수를 라이브하다고 말한다.

NLL에서는 라이브 변수만 계산했지만, 여기서는 라이브 플레이스를 계산할 것이다:

LivePlaces = { Place }

라이브 플레이스 집합을 계산하기 위해 보조 함수 LiveBefore(Env, LivePlaces, Expr): LivePlaces를 도입한다. LiveBefore()는 환경 Env와 표현식 이후에 라이브한 플레이스 집합이 주어졌을 때, Expr가 평가되기 _이전_에 라이브한 플레이스 집합을 반환한다. 이 함수를 자세히 정의하지는 않겠지만, 대략 다음과 같다:

// `&Place`는 `Place`를 읽으므로, 이를 `LivePlaces`에 추가한다
LiveBefore(Env, LivePlaces, &Place) =
    LivePlaces ∪ {Place}

// `Place = Expr`는 `Place`를 덮어쓰므로, 이를 `LivePlaces`에서 제거한다
LiveBefore(Env, LivePlaces, Place = Expr) =
    LiveBefore(Env, (LivePlaces - {Place}), Expr)

// `Expr1`이 먼저 평가되고, 그 다음 `Expr2`가 평가된다. 따라서
// expr1 이후에 라이브한 플레이스 집합은 expr2 이전에 라이브한 플레이스 집합이다
LiveBefore(Env, LivePlaces, Expr1 + Expr2) =
    LiveBefore(Env, LiveBefore(Env, LivePlaces, Expr2), Expr1)
    
... etc ...

Integrating liveness into our typing judgments

차용 검사 오류를 감지하려면, 라이브니스를 판단식에 통합해야 한다. 결과는 다음과 같다:

(Env, LivePlaces) |- Expr : Type

이 판단식은 “환경 Env에서, 그리고 함수가 미래에 LivePlaces를 접근할 것이라는 전제하에, Expr는 유효하며 타입 Type을 가진다”는 뜻이다. 이처럼 라이브니스를 통합하면 미래에 어떤 접근이 일어날지에 대한 정보를 일부 얻을 수 있다.

Expr1 + Expr2 같은 합성 표현식의 경우, 제어 흐름을 반영하도록 라이브 플레이스 집합을 조정해야 한다:

LiveAfter1 = LiveBefore(Env, LiveAfter2, Expr2)
(Env, LiveAfter1) |- Expr1 : u32
(Env, LiveAfter2) |- Expr2 : u32
----------------------------------------- addition
(Env, LiveAfter2) |- Expr1 + Expr2 : u32

우리는 전체 표현식 이후에 라이브한 플레이스인 LiveAfter2로부터 시작한다. 이 집합은 표현식 2가 평가된 후에도 동일하다. 이 표현식 자체는 어떤 플레이스도 참조하거나 덮어쓰지 않기 때문이다. 그런 다음 LiveAfter1, 즉 Expr1이 평가된 이후에 라이브한 플레이스 집합을 계산하는데, 이는 Expr2를 평가하기 _이전_에 라이브한 플레이스(= Expr2의 LiveBefore)를 살펴봄으로써 얻는다. 이는 약간 정신을 꼬이게 만들 수 있고, 나도 이해하는 데 시간이 좀 걸렸다. 까다로운 부분은 라이브니스가 _역방향_으로 계산되는 반면, 대부분의 타이핑 규칙(그리고 우리의 직관)은 _정방향_으로 흐른다는 점이다. 도움이 된다면, +의 “완전히 디슈거된” 버전을 떠올려 보라:

let tmp0 = <Expr1>
    // <-- 여기에서 LiveAfter1 집합이 라이브함 (tmp0, tmp1은 무시)
let tmp1 = <Expr2>
    // <-- 여기에서 LiveAfter2 집합이 라이브함 (tmp0, tmp1은 무시)
tmp0 + tmp1
    // <-- 여기에서 LiveAfter2 집합이 라이브함

Borrow checking with liveness

이제 라이브니스 정보를 알게 되었으니, 이를 사용해 차용 검사를 수행할 수 있다. “permits” 판단을 도입하자:

(Env, LiveAfter) permits Loan

이는 “환경과 라이브 플레이스를 고려했을 때 Loan 대여를 취하는 것이 허용된다”는 뜻이다. 다음은 대입 규칙을 라이브니스와 새 “permits” 판단을 포함하도록 수정한 것이다:

(Env, LiveAfter - {Place}) |- Expr : Type1
(Env, LiveAfter) |- Place : Type2
(Env, LiveAfter) |- Type1 <: Type2
(Env, LiveAfter) permits mut(Place)
----------------------------------------- assignment
(Env, LiveAfter) |- Place = Expr : ()

“permits”를 어떻게 정의하는지로 들어가기 전에, 예제로 돌아가 직관을 살펴보자. 우리는 다음 대입에서 오류를 보고하고 싶다:

let mut counter: u32 = 22_u32;
let p: &{shared(counter)} u32 = &counter;
counter += 1; // <-- 오류
println!("{p}"); // <-- p는 라이브함

바로 다음 줄의 println! 때문에, p는 우리의 LiveAfter 집합에 포함될 것이다. p의 타입을 보면 shared(counter) 대여를 포함하고 있음을 알 수 있다. 아이디어는 다음과 같다. shared(counter)라는 라이브 대여가 존재하므로, 이는 counter가 불변이어야 함을 의미하고, 따라서 counter를 변경하는 것은 불법이다.

그 직관을 다시 말하면:

라이브 플레이스 집합 Live는, Live에 있는 모든 라이브 플레이스 Place에 대해, Place의 타입에 들어 있는 대여들이 Loan1과 양립 가능하다면, 대여 Loan1을 허용(permit) 한다.

좀 더 형식적으로 쓰면:

∀ Place ∈ Live {
    (Env, Live) |- Place : Type
    ∀ Loan2 ∈ Loans(Type) { Compatible(Loan1, Loan2) }
}
-----------------------------------------
(Env, Live) permits Loan1

이 정의는 두 가지 보조 함수를 사용한다:

• Loans(Type) – 타입에 등장하는 대여들의 집합
• Compatible(Loan1, Loan2) – 두 대여가 양립 가능한지 정의한다. 두 공유 대여는 항상 양립 가능하다. 가변 대여는 플레이스가 서로 분리되어 있을 때에만 다른 대여와 양립 가능하다.

Conclusion

이 글의 목표는 높은 수준의 직관을 전달하는 것이었다. 기억을 더듬어 쓴 터라 한두 가지를 간과했을지도 모른다. 하지만 후속 글에서는 내가 실험 중인 시스템이 어떻게 동작하는지, 그리고 무엇을 새로 지원할 수 있는지 더 깊이 있게 다룰 생각이다. 몇 가지 고수준 예시는 다음과 같다:

• 서브타이핑을 어떻게 정의하는지, 특히 서브타이핑에서 라이브니스가 어떤 역할을 하는지
• 오늘날 우리가 사용하는 중요한 차용 패턴들이 새 시스템에서 어떻게 동작하는지
• 다른 구조체 필드가 소유한 데이터를 가리키는 내부 참조를 어떻게 지원할 수 있는지

---

1. 이것이 자명하지 않다면 걱정하지 마라. 나에게도 자명하지 않았다. 규칙에 라이브니스를 사용하는 것이 그것들을 단순하게 만드는 핵심이라는 사실이 드러났다. 대안으로 탐구했던 방법들과 왜 잘 작동하지 않았는지에 대해서는 나중에 후속 글로 다뤄보겠다.↩︎