부분구조 타입 이론과 소유권을 통해 프로그램의 안전성과 활성 보장을 어떻게 강화할 수 있는지 설명하고, Rust의 구현상의 한계와 개선 방향(선형 타입, memcpy와의 결합 해소, E0509 제거)을 논의합니다.
이 글은 부분구조 타입 이론(substructural type theory)이 프로그래밍 언어 설계에 어떻게 적용될 수 있는지 설명하기 위한 글이다. “부분구조 타입 이론” 같은 용어는 주말에 하스켈을 쓰지 않는 프로그래머들을 겁주고 혼란스럽게 만들곤 한다. 그래서 언어 설계자가 자신의 언어를 어떻게 소개할지 고민할 때, 약간은 부정확하더라도 은유를 만들어 더 일반적인 프로그래머가 언어의 작동 방식을 이해하도록 도울 필요가 있다. 그런 용어 중 하나가 “소유권(ownership)”이다.
프로그램의 객체는 적지 않게 자기 자신 바깥의 무언가를 대표하게 된다. 더 이상 “순수 데이터”가 아니라 정체성(identity)을 지닌 일종의 자원이다. 고전적인 예로는 어떤 자원에 대한 배타적 접근을 부여하는 핸들을 들 수 있다. 이것이 제대로 작동하려면, 그 객체를 얻으려면 특정 코드(“생성자”)를 실행해야 하고, 객체가 더 이상 사용되지 않으면 또 다른 코드(“소멸자”)가 실행된다는 점, 그리고 객체가 스코프에 있는 동안 동시 실행 중인 어떤 코드도 같은 배타적 자원을 나타내는 객체를 갖지 않는다는 점(즉, “별칭(aliasing)”되지 않는다는 점)을 보장하고 싶다. 적어도 Rust에서 제시되는 소유권은 바로 이것을 다룬다.
나는 소유권과 부분구조 타입을 탈신비화하고 싶다. 이 주제가 더 널리 알려지길 바라기 때문이다. 이 글에 진짜 획기적인 내용은 없다. 이미 “아는 사람”에게는 새로울 것이 없을 것이다. 다만 Rust 구현의 몇몇 측면에 대해 잘못되었다고 생각하는 부분(그중 하나는 바꾸기조차 쉽다)에 대한 메모가 포함되어 있다.
먼저 한 걸음 물러나 보다 근본적인 질문을 살펴보자. 타입 시스템은 무엇을 위한 것인가?
내가 매우 좋아하는 그레이든 호어(Graydon Hoare)의 말(아마도 다른 사람의 말을 인용한 것 같다)은, 타입 시스템은 우리가 쉽게 만들 수 있게 된 형식 기법(formal methods)의 일부라는 것이다. 즉, 타입 시스템은 프로그램의 동작 측면을 검증하기 위해 프로그램에 자동으로 적용되는 형식적(그리고 되도록 음이성(safe) 있는) 정적 분석 기법이다. 형식 분석에서는 프로그램이 가질 수 있는 두 종류의 속성 간에 가치 있는 구분이 있다.
우리는 보통 타입 시스템이 특정 안전성 속성을 지켜 준다고 생각한다. 예를 들어, fn(String) -> Integer라는 함수를 가지고 있다면, 타입 시스템은 프로그램이 이 함수를 String이 아닌 인자로(혹은 두 개, 제로나 등) 호출하지 않도록 보장한다. 하지만 타입 시스템은 몇몇 활성 속성도 지켜 준다. 예를 들어, 함수가 정수를 반환한다는 점을 보장한다.
그러나 우리가 사용하는 언어의 표현력이 매우 크기 때문에 활성 속성에는 대개 불행한 단서가 붙는다. 구체적으로, 거의 모든 널리 쓰이는 프로그래밍 언어는 튜링 완전하며, 그러므로 그 함수가 실제로 정수를 반환할 것이라고 보장할 수 없다. 대신 함수가 종료하지 않을 수도 있다. 그래서 활성 속성은 보통 프로그램이 언젠가는 그렇게 할 것이다라고 단서가 붙는데, 여기서 “언젠가”는 무한히 먼 미래일 수도 있다. 또한 대부분의 프로그래밍 언어는 프로그램을 중단(abort)하거나 타입이 없는 예외를 던질 수 있는데, 이것 역시 활성 속성에 관한 어떤 보장에도 또 다른 단서로 붙는다. 이상적이진 않지만, 현재 실무의 현실이 그렇다.
소유권은 언어의 타입 시스템을 확장하여, 특히 주어진 값이 “사용”되는 횟수와 관련해 프로그램의 안전성과 활성 속성에 대한 추가 보장을 확립할 수 있게 하는 방법이다.
수리논리에서 “구조 규칙(structural rules)”이라 불리는 보편 규칙들이 있다. 이는 논리의 구조의 일부다. 오늘 우리가 관심 있는 두 가지 규칙은 다음과 같다.
(이 글에서 처음 제시했던 축약(contraction)의 정의가 뒤집혀 있었다. 정정해 준 George Kulakowski에게 감사한다.)
A -> B), A와 다른 임의의 사실이 B를 함의한다는 것도 안다(예: A, C -> B). 즉, 규칙에서 불필요한 전제를 무시할 수 있다.A, A -> B), A 한 번만으로도 B를 함의한다는 것을 안다(예: A -> B). 즉, 동일한 전제를 여러 개 가질 필요가 없다.이러한 구조 규칙을 포함하지 않는 다른 종류의 논리를 구성할 수도 있다. 예를 들어, 선형 논리에서는 이 두 규칙이 모두 없다. 즉, A, A -> B를 안다고 해서 A, A, C -> B나 A -> B를 알 수 없다.
또 한동안 타입 이론과 수리논리가 강한 관계를 가진다는 점이 알려져 왔다. 주말에 하스켈을 쓰는 사람들은 이 얘기를 귀에 못이 박히도록 할 텐데, 이것이 바로 그들이 “커리-하워드 대응(Curry-Howard correspondence)”이라고 말할 때 의미하는 바다. 이 바탕 위에서, 이러한 구조 규칙이 없는 타입 시스템을 고안하려는 아이디어에 관심이 모였다. 아론 투론(Aaron Turon)이 내게 들려준 바(역사의 세부를 면밀히 조사하진 않았다)에 따르면, 처음에는 순전히 이론적인 시도였고 알려진 실용적 응용이 없었다. 그러나 앞서 설명한, 정체성의 의미 있는 개념을 가진 객체들을 표현하는 데 매우 유용하다는 사실이 드러났다.
“부분구조 타입”이란 하나 혹은 둘 모두의 구조 규칙을 제거한 타입을 말한다. 이를 이해하는 방법은 이렇다. 일반 타입의 값은 임의의 횟수만큼 사용할 수 있지만, 부분구조 타입의 값은 사용할 수 있는 횟수가 제한된다. 타입이 “약화”될 수 없으면, 스코프에서 벗어나기 전에 적어도 한 번은 사용되어야 한다. 타입이 “축약”될 수 없으면, 한 번을 초과하여 사용할 수 없다. 각 범주의 타입에는 이름이 있으며, 다음 표에 나타나 있다.
│ WEAKENING? │ CONTRACTION? │ USES
─────────────────┼────────────┼──────────────┼────────────────
│ │ │
Normal types │ YES │ YES │ Any number
│ │ │
Affine types │ YES │ │ At most once
│ │ │
Relevant types │ │ YES │ At least once
│ │ │
Linear types │ │ │ Exactly once
현재 Rust에서는 모든 타입이 약화 법칙을 가지지만, 기본적으로 타입은 축약 법칙을 가지지 않는다. 그래서 Rust의 대부분 타입은 이른바 아핀 타입(affine types)이며, 한 번 또는 0번만 사용할 수 있다. 사용하는 것은 “이동(move)”하는 것이고, 사용하지 않는 것은 “드롭(drop)”하는 것이다. 우리가 소유권이라고 부르는 것이 바로 이것이다.
Rust는 임의의 횟수로 사용할 수 있는 일반 타입도 지원하는데, 현재는 Copy를 구현하는 타입이 여기에 해당한다. 그 결과 Rust에서는 모든 일반 타입이 memcpy를 수행해 복사할 수 있어야 한다는 특이점이 있다. 다른 언어에서는 일반 타입일 법한 타입들은 Clone이라는 트레이트를 구현하여 일반 타입 의미론을 제공하지만, 한 번 이상 이동하고 싶을 때마다 clone 호출을 추가해야 한다. 이는 값비싼 연산(예: String을 복사하려면 임의 크기의 힙 할당을 새로 만들고 데이터를 복사해야 함)을 억제하려는 의도다. 하지만 어떤 memcpy는 비싸고(큰 복사) 어떤 비-memcpy 복사는 싸다(특히 Rc와 Arc). 최근 니코 마차키스(Niko Matsakis)가 글을 통해 일반 타입 의미론과 memcpy의 강한 결합을 끊자는 제안을 했는데, 나는 훌륭한 제안이라 생각하며 Rust가 이 부분에서 변하길 바란다.
안전성과 활성 속성 이야기로 돌아가서, 소유권이 실제로 우리에게 무엇을 제공하는지 짚어 보자. 첫째, 그 값이 프로그램의 다른 어디에서도 별칭되지 않았다는 보장을 얻었다. 이는 가변이고 별칭된 상태를 가지지 않는다는 안전성 속성을 유지하면서 그 값을 변경(mutating)할 수 있게 해 준다. 이는 Rust의 메모리 안전성과 데이터 경합 없는 동시성, 그리고 지역적 추론을 가능하게 하는 데 핵심적이다.
또한 값이 별칭되지 않았음이 알려져 있으므로, 스코프에서 벗어날 때 그 소멸자를 실행할 수 있음을 안다. 파일을 닫고, 뮤텍스를 잠금 해제하는 등의 작업이다. 소유권이 없는 언어는 이런 종류의 보장을 할 수 없다. 값이 다른 곳에서 별칭되어 있을 수 있기 때문이다. 일부 언어는 이 문제에 대해 불완전하고 나쁜 해결책(예: Python의 with)을 제공해 왔는데, 이는 프로그래머가 마주치는 오류의 수를 줄여 주긴 하지만 문제를 완전히 해결하지는 못한다. 예를 들어 Python에서는 with 블록으로 연 파일이 블록 밖으로 빠져나갈 수 있는데, 블록 밖 변수에 할당하는 것을 막는 것이 없기 때문이다.
Rust에는 아핀 타입이 있지만, 현재는 약화될 수 없는 타입, 즉 적어도 한 번은 사용되어야 하는 타입은 없다. 특히 정확히 한 번은 사용되어야 하는 _선형 타입(linear types)_에 대한 관심이 많다. 이 용어는 Rust 프로젝트의 일부 기여자들에 의해 누수(leak)에 관한 다른 아이디어를 가리키는 데 오용되기도 했지만(이 글의 뒷부분에서 공유 소유권을 다룰 때로 돌아오겠다), 올바른 의미로 언어에 제대로 된 선형 타입을 추가하는 것을 가리키는 데에도 사용된다. 이런 타입은 “반드시 이동해야 하는(must move)” 타입 혹은 “드롭 불가(undroppable)” 타입이라고도 불린다.
지금 Rust에 선형 타입을 추가하는 일은 결코 쉬운 일이 아닐 것이다. 하지만 어떤 언어에서든 그 가치가 무엇인지 설명하고 싶다. 그 유용성을 설명하는 가장 쉬운 방법은 세션 타입(session types)에 대해 이야기하는 것이다.
세션 타입의 아이디어는 동시에 실행 중인 어떤 프로세스의 프로토콜을 타입 시스템에 인코딩하여, 그 동시 프로세스가 놓인 상태에 따라 합법적인 연산만 수행할 수 있게 하는 것이다. 이는 기본적으로 상태 머신을 언어에 인코딩하는 것과 같으며, 각 상태는 그 자체의 타입으로 표현되고, 각 상태 전이는 다음 상태의 타입을 반환하는 메서드가 된다.
아주 간단한 예로, 커밋되거나 중단되어야 하는 트랜잭션을 보자.
impl Transaction {
pub fn commit(self) -> TransactionResult;
pub fn abort(self);
}
이런 세션 타입의 문제는 사용자가 트랜잭션을 그냥 드롭해 버릴 수 있다는 점이다. 이 경우 드롭 시에 트랜잭션을 중단(abort)하는 소멸자를 작성하겠다고 말할 수 있겠다(이 아이디어는 다음 절에서 다시 다룬다). 하지만 드롭 시 수행할 명백한 상태 전이가 없는 더 복잡한 예를 쉽게 상상할 수 있다.
선형 타입은 세션 타입을 드롭하는 문제를 막아 준다. 세션 타입을 반드시 사용해야 하기 때문이다. 사용자는 commit이나 abort를 호출함으로써 세션 타입을 사용할 수 있고, 아니면 그것을 새 함수로 이동시켜 사용할 수도 있다. 하지만 그 함수는 무엇을 할 수 있는가? 역시 다른 함수로 이동시키거나, commit이나 abort를 호출할 수 있다. 그 결과 우리는 (기억하자, “언젠가”는 무한히 먼 미래일 수도 있지만) 결국 프로그램이 이 트랜잭션에 대해 commit 또는 abort를 호출할 것이라는 활성 보장을 얻게 된다.
하지만 조금 더 깊이 들어가 보자. 그러면 다음 절에서 다룰 Rust의 아핀 타입 구현의 결함이 드러난다. commit과 abort의 구현을 생각해 보라. 이들은 Transaction이라는 선형 타입의 인자 self를 받는다. 이는 이 메서드들도 어떻게든 self 값을 사용해야 함을 뜻한다. 그런데 어떻게 동작하는가? 끝없이 거북이 위의 거북이일 수는 없지 않은가.
선형 세션 타입을 성립시키는 두 번째 요소는 구조 분해(destructuring)다. 트랜잭션 타입은 몇 개의 필드로 구성된 구조체이며, 그 필드들 자체는 일반 타입이거나 아핀 타입일 수 있다. 이들 메서드에서는 어느 시점에 트랜잭션 타입을 그 필드 타입들로 구조 분해한다. 이는 트랜잭션을 사용한 것이지만, 또 다른 트랜잭션 타입 값을 남기는 대신 자유롭게 드롭할 수 있는 타입들을 남긴다. 선형 타입을 성립시키는 유일한 방법은 이것뿐이다. 그렇지 않다면 여러분은 생성한 모든 선형 타입의 값을 저장하고 main에서 반환해야 할 것이다!
그러나 사용자가 트랜잭션 타입을 구조 분해할 수 있다면, 더 이상 commit이나 abort를 호출하리라는 활성 보장이 사라진다. 따라서 활성 보장을 가진 세션 타입을 성립시키는 세 번째이자 마지막 요소는, 어떤 코드가 세션 타입을 구조 분해할 수 있는지 제한하기 위해 가시성(privacy)을 사용해야 한다는 점이다. 트랜잭션의 필드가 비공개(private)라면, 해당 모듈의 메서드만 그것을 구조 분해할 수 있다. 이렇게 하면 트랜잭션 타입을 정의하는 라이브러리를 살펴봄으로써, commit과 abort에서만 구조 분해됨을 확인할 수 있고, 따라서 그 라이브러리를 사용하는 코드에서는 결국 프로그램이 모든 트랜잭션을 commit하거나 abort하리라는 활성 보장을 얻게 된다.
소유권을 가진 타입은 유효한 “기본 상태 전이(default state transition)”를 가진 세션 타입의 특별한 경우로 생각할 수 있다. 이 기본 상태 전이는 반드시 ()로 전이해야 하며(오류나 다른 의미 있는 값을 반환할 수 없다), 다른 전이 메서드(있다면)들을 호출하지 않고 값이 스코프에서 벗어날 때 호출된다. 우리는 이 기본 상태 전이를 _소멸자(destructor)_라고 부른다.
나는 소유권 타입을 이렇게 생각하는 것이 옳다고 본다. 기본 소멸자를 가진 세션 타입의 특수 사례일 뿐이다. 여기서 Rust 컴파일러가 허용하지 않는 프로그램 유형, 그리고 내가 Rust 컴파일러가 틀렸다고 생각하는 부분으로 이어진다. 바로 소멸자가 있는 타입을 구조 분해할 수 없다는 점이다. 이 오류의 코드가 E0509다.
세션 타입의 상태 전이가 세션 타입을 소비하고 그것을 구조 분해하는 메서드에 지나지 않으며, 소멸자가 그 어떤 다른 전이 메서드가 호출되지 않았을 때 자동으로 호출되는 상태 전이 메서드라면, 소멸자는 자동 구조 분해자이기도 하다. 이것이 내가 그 타입을 다른 방식으로 구조 분해하지 못할 이유가 되진 않는다. “이 타입은 구조 분해하거나, 소멸자를 실행해야 한다”라는 계약을 상정하는 것은 전적으로 가능하다. 하지만 오늘날 Rust에서는 이를 표현할 방법이 없다. 타입에 소멸자를 추가하면, 그 타입을 구조 분해할 수 없기 때문이다.
E0509는 Rust의 초창기에 추가되었고, 그 당시에는 이동 의미론과 소유권의 이론적 기반이 덜 잘 이해되었던 것 같다. 내가 보기엔 그 동기는 이렇다. 타입에 소멸자를 추가했다면 그 소멸자가 호출되길 원할 텐데, 그 타입을 구조 분해하면 소멸자가 호출되지 않는다는 것이다. 하지만 그 해결책은 선형 타입의 경우와 동일하다. 소멸자와 가시성을 결합해 구조 분해가 그 타입을 소비하는 옵션이 되지 않게 하면 된다.
이미 거의 모든 소멸자가 있는 타입이 이렇게 동작한다(모두 비공개 필드를 갖는다). 그래서 이슈가 드물게만 발생한다. 하지만 serde_json에서 데이비드 톨네이(David Tolnay)가 제공한 훌륭한 예가 있다. 라이브러리에 소멸자를 실행하거나 구조 분해로 소비되어야 하는 타입이 있는데, E0509가 정확히 이런 패턴을 막기 때문에 나쁜 우회책을 써야 했던 사례다.
그 타입은 Value 타입으로, 임의의 JSON 값을 나타낸다. 모든 종류의 JSON 값(숫자, 불리언, 배열 등)을 나열한 enum이다. 스키마를 예상하지 않는 JSON을 파싱해 match 등으로 순회할 수 있는 값으로 사용할 수 있다.
하지만 JSON은 종종 신뢰할 수 없는 입력에서 파싱되며, 일반 소멸자가 호출될 때 스택 오버플로를 일으킬 병적인 JSON을 정의하는 것이 충분히 그럴싸하다. 예를 들어 [[[]]]라는 JSON을 생각해 보자. 이를 Value로 파싱하면, 배열 안에 배열, 그 안에 빈 배열이 생긴다. 자동으로 생성되는 소멸자 코드는 각 배열 변형을 해제하기 위해 3단계로 중첩된 호출을 수행한다. 병적인 JSON 문자열은 그 깊이가 충분히 커서 값을 파괴(destroy)할 때 스택이 넘치게 만들 수 있다. 그래서 serde_json의 Value 타입에는 스택 사용량이 JSON의 깊이에 따라 증가하지 않도록 꼬리 호출 최적화 형태를 사용하는 사용자 정의 소멸자가 있어야 한다.
문제는 Value 타입에 이 소멸자를 구현하면 이제 구조 분해를 할 수 없게 된다는 점이다. 하지만 Value의 핵심 목적은 match로 구조 분해하는 것이다! 데이비드 톨네이는 Vec 대신 사용자 정의 Array 타입을 추가해 꼬리 호출 최적화 소멸자를 갖도록 우회했지만, 이는 좋은 이유 없이 API를 복잡하게 만든다. 대신 E0509를 제거해 사용자 정의 소멸자를 가진 Value 타입을 정의하되, 사용자가 그것을 구조 분해하는 것을 막지 않도록 해야 한다.
소유권은 훌륭하지만, 때로는 소유된 값을 별칭하도록 허용하고 싶을 때가 있다. 이를 구현하는 한 가지 방법은 아핀 타입을 받아 일반 타입을 생성하는(또는 현재 Rust의 경우 일반 타입 의미론을 흉내 내기 위한 Clone이 있는 아핀 타입을 생성하는) 일종의 생성자를 두는 것이다. 이를 “공유 소유권(shared ownership)”이라고 한다. 이러한 공유 소유권 구성은 그 값의 별칭 수를 추적하고, 마지막 값이 스코프에서 벗어날 때만 소멸자를 실행한다.
언어에 공유 소유권을 추가하려면 중요한 주의점이 있다.
첫째, 공유 소유권으로 공유되는 값을 동기화 없이 변경할 수 있도록 해서는 안 된다. 그렇게 하면 가변이고 별칭된 상태가 생긴다. 따라서 이 기능을 추가하려면 변경을 제어하는 이야기가 반드시 필요하다.
둘째, 공유 소유권의 구현이 어떤 종류의 순환 끊기(cycle breaking)를 수행하지 않는다면(참조 카운팅 포인터의 사용과 같이), 참조 순환이 존재하는 시나리오를 허용하게 되어 값이 누수되고 소멸자가 실행되지 않을 수 있다. 이는 소멸자 실행에 관한 모든 활성 보장(혹은 그 문제로 선형 세션 타입의 전이에 관한 보장)이 이제 값이 누수될 가능성이라는 단서와 함께 제시되어야 함을 의미한다. 그리고 솔루션이 순환을 끊긴 하지만 값이 언제 해제될지에 대한 적시성 보장을 제공하지 않는다면(추적 가비지 컬렉터처럼), 뮤텍스 락 가드와 같은 소멸자에는 성능 문제가 생길 가능성이 크다. 총체적으로 매우 험난한 기능이므로 추가에 신중해야 한다.
Rust는 순환을 끊지 않는 참조 카운팅 포인터를 허용하기로 했으므로, 소멸자에 기반한 모든 보장은 소멸자가 실행되지 않을 수도 있다는 단서를 달아야 한다. 이를 바꾸어 누수될 수 없는 타입(“unforgettable types”, 누수 불가 타입)을 정의하고, 그런 타입은 공유 소유권 구성에 안전하게 넣을 수 없도록 하자는 관심이 있었다. 선형 타입과 마찬가지로, 지금 언어에 이 구분을 추가하는 것은 매우 도전적이겠지만 매력적이다.
공유 소유권의 문제를 겪지 않고 값을 별칭할 수 있게 하는 한 가지 방법은 참조(references) 개념이다. 참조 연산자는 값을 가져오되 이동으로 간주하지 않으므로, 참조가 끝난 뒤에도 값이 남아 있다. 공유 참조는 일반 타입이 될 수 있으므로 별칭될 수 있다. 또한 _가변 참조(mutable references)_를 추가할 수 있는데, 이는 아핀 타입이며 별칭되지 않기 때문에 변경을 허용한다.
이 기능을 사용하려면 참조가 여전히 존재하는 동안 값이 다시 사용되지 않도록 보장해야 한다. 그렇지 않으면 그 참조가 무효화된다. Rust는 참조에 “수명(lifetime)”을 부여하고, 이 수명을 사용해 프로그램을 검증하는 “대여 검사기(borrow checker)”를 실행함으로써 이를 달성했다. 덧붙이자면, 이 솔루션은 수명의 작동 방식 때문에 순환 참조도 막아 준다. 이는 이 글의 범위를 약간 벗어나지만, 이 기능들은 흔히 공유된 용어 “소유권과 대여(ownership and borrowing)” 아래에서 함께 논의된다.
이런 종류의 글쓰기는 내게 새롭다. 내가 새롭다고 생각하는 아이디어를 전달하거나 탐색하려는 것이 아니라, 오래되었지만 널리 알려지지 않은 아이디어를 대중화하려는 시도이기 때문이다. 소유권과 부분구조 타입에 대한 보다 현실에 기반한 이해가 일부 독자에게는 계몽적이었기를 바란다.
나는 새로운 프로그래밍 언어를 설계하면서 어떤 형태로든 부분구조 타입을 빼놓지 않을 것이다. 별칭에 대한 안전 보장과 상태 전이에 대한 활성 보장의 가치 제안은 너무나 유용해 보인다. 앞으로 등장할 새로운 언어들에서 이러한 기능들이 제대로 구현되길 바란다.
마지막으로, Rust 프로젝트의 기여자들(특히 니코 마차키스)이 Rust의 소유권 규칙을 바꾸려는 데 관심이 있는 듯하다. 구현은 어렵겠지만 개선이라고 본다. Rust는 선형 타입을 갖게 되면 좋고, 일반 타입이 memcpy에 묶여 있지 않게 되는 것 또한 이롭다. 또한 훨씬 더 쉬운 변경으로, E0509를 제거해 소유된 타입을 구조 분해할 수 있게 하는 것도 고려해야 한다.