Rust의 타입 시스템을 라이프타임 대신 장소 기반의 오리진(대여들의 집합)으로 표현하는 대안을 소개한다. 라이브니스(생존성) 정보를 타이핑 판단식에 통합해 대여 검사를 수행하고, 예제 프로그램과 함께 오리진, 대여, 장소, permits 판단 및 호환성 규칙의 핵심 아이디어를 간략히 설명한다.
이 글은 Rust의 타입 시스템을 라이프타임을 버리고 대신 플레이스(places)에 기반해 재구성하는 대안을 탐구한다. TL;DR은 다음과 같다. 코드에서 'a가 _라이프타임_을 나타내는 대신, shared(a.b.c)나 mut(x) 같은 _대여(loan)의 집합_을 나타낼 수 있다는 것이다. 익숙하게 들린다면 맞다. 이는 polonius의 기초이지만, 정적 분석이 아닌 타입 시스템으로 재정식화한 버전이다. 이 글은 높은 수준의 아이디어만을 다룬다. 후속 글에서는 내부 참조 등 더 진보된 대여 패턴을 어떻게 지원할 수 있는지 파고들 예정이다. 구현 측면에서 약간의 모형을 만들어봤고, a-mir-formality를 확장하여 이 분석을 포함시키기 시작할 생각이다.
라이프타임은 Rust의 최고이자 최악의 부분이다. 최고인 이유는 자료구조 중간 어딘가에 있는 데이터에 대한 포인터를 반환하는 등 아주 멋진 패턴을 표현할 수 있게 해주기 때문이다. 하지만 상당한 문제가 있다. 우선 라이프타임이라는 개념 자체가 꽤 추상적이어서 사람들이 이해하기 어렵다(“'a는 실제로 무엇을 나타내는가?”). 또한 Rust는 일부 중요한 패턴, 특히 구조체의 한 필드가 다른 필드가 소유한 데이터를 참조하는 내부 참조(interior references)를 제대로 표현하지 못한다.
다음은 비-렉시컬 라이프타임(NLL) RFC에 나오는 라이프타임의 정의다:
차용을 만들 때마다, 컴파일러는 그 결과 레퍼런스에 라이프타임을 부여한다. 이 라이프타임은 그 레퍼런스를 사용할 수 있는 코드 구간(span)에 대응한다. 컴파일러는 레퍼런스의 모든 사용을 포괄하면서도 가능한 한 가장 작은 라이프타임으로 이를 유추한다.
이 재정식화에서 'a는 더 이상 _라이프타임_이 아니라 오리진(origin), 즉 그 레퍼런스가 어디에서 왔는지를 설명하는 값이 된다. 오리진은 대여(loan)의 집합으로 정의한다. 각 대여는 어떤 장소 표현(place expression)(예: a나 a.b.c)이 어떤 모드(shared 또는 mut)로 차용되었는지를 담는다.
Origin = { Loan }
Loan = shared(Place)
| mut(Place)
Place = variable(.field)* // 예: a.b.c
오리진을 이용해 Rust 타입을 대략 다음과 같이 정의할 수 있다(물론 여기서는 많은 복잡성을 생략한다…):
Type = TypeName < Generic* >
| & Origin Type
| & Origin mut Type
TypeName = u32 (당분간 다른 스칼라는 무시)
| () (단위 타입, 튜플은 일단 신경 쓰지 말자)
| StructName
| EnumName
| UnionName
Generic = Type | Origin
여기서 주목할 첫 번째 흥미로운 점은, 'a 표기가 없다는 것이다! 아직 제네릭을 도입하지 않았기 때문이다. 실제 Rust와 달리, 이 타입 시스템에서는 'a가 의미하는 바를 구체적으로 표현하는 문법(Origin)이 존재한다.
완전히 명시적인 타입 시스템이 있으면 모든 타입이 완전히 지정된 예제 프로그램을 쉽게 작성할 수 있다. 예전에는 라이프타임을 표기할 방법이 없어 꽤 어려웠다. 오류가 나야 마땅한 간단한 예제를 보자:
let mut counter: u32 = 22_u32;
let p: & /*{shared(counter)}*/ u32 = &counter;
// ---------------------
// 현재는 이를 표현하는 문법이 없음!
counter += 1; // 오류: `p`가 살아 있는 동안 `counter`는 변경할 수 없음
println!("{p}");
p의 타입을 제외하면, 이는 유효한 Rust 코드다. 물론 컴파일은 되지 않는다. 라이브한(shared) 참조 p가 있는 동안 counter를 수정할 수 없기 때문이다(playground). 계속해서, 새로운 타입 시스템 정식화가 어떻게 동일한 결론에 도달하는지 보게 될 것이다.
타이핑 판단식(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
차용 검사를 도입하려면 라이브니스(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 ...
차용 검사 오류를 감지하려면, 라이브니스를 판단식에 통합해야 한다. 결과는 다음과 같다:
(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 집합이 라이브함
이제 라이브니스 정보를 알게 되었으니, 이를 사용해 차용 검사를 수행할 수 있다. “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) – 두 대여가 양립 가능한지 정의한다. 두 공유 대여는 항상 양립 가능하다. 가변 대여는 플레이스가 서로 분리되어 있을 때에만 다른 대여와 양립 가능하다.이 글의 목표는 높은 수준의 직관을 전달하는 것이었다. 기억을 더듬어 쓴 터라 한두 가지를 간과했을지도 모른다. 하지만 후속 글에서는 내가 실험 중인 시스템이 어떻게 동작하는지, 그리고 무엇을 새로 지원할 수 있는지 더 깊이 있게 다룰 생각이다. 몇 가지 고수준 예시는 다음과 같다: