세션 타입은 작동한다. 대부분의 언어가 단지 구현을 거부했을 뿐이다.

세션 타입은 1993년에 발명되었다. 30년 후, 대부분의 네트워크 서비스는 여전히 프로토콜 상태를 수작업으로 작성한 런타임 검사로 검증하고 있다. 애초에 검증하는지조차 미지수다. 타입 시스템은 클라이언트가 HELLO 전에 PONG을 보냈는지, 또는 누군가 닫는 것을 잊어 연결이 누출되었는지에 대해 아무런 의견이 없다.

연구 커뮤니티는 수십 년 동안 이 문제에 대한 해결책을 가지고 있었다. 문제는 결코 이론적이지 않았다. 문제는 세션 타입이 대부분의 주류 언어가 30년 동안 거부해 온 기능을 필요로 했다는 것이었다: 선형 타입.

세션 타입은 컴파일러가 대신 확인해 주는 스테이트 머신이다

모든 네트워크 프로토콜은 state machine다. 간단한 요청-응답 프로토콜은 이렇게 보인다: 클라이언트가 i32를 보내고, 서버가 String으로 응답하고, 그런 다음 채널이 닫힌다. 클라이언트가 쓰기 전에 읽으려고 시도하거나, 한쪽이 연결을 닫는 것을 잊으면 프로토콜이 위반된다.

일반적인 코드베이스에서는 주석, 규칙, 그리고 아마도 런타임에 상태를 추적하는 수작업으로 작성한 Enum을 사용하여 이를 강제한다. 그 Enum은 작은 인터프리터다. 그것은 당신의 머릿속, 문서, 버그 추적기 안에 존재한다.

세션 타입은 그 스테이트 머신을 타입 시스템으로 옮긴다. 채널의 타입은 모든 연산 후에 변경된다. 정수를 보내면 채널의 타입은 “문자열 수신 대기 중”이 된다. 문자열을 수신하면 타입은 “닫아야 함”이 된다. 순서를 무시하고 채널을 사용하면 프로덕션의 프로토콜 위반이 아닌 컴파일 오류가 발생한다.

다음은 외부 의존성 없이 세션 타입을 인코딩하기 위해 타입 상태 패턴을 사용하는 Rust의 코드다:

use std::marker::PhantomData;

// Protocol states: Send<i32>, Recv<String>, Close
struct Start;
struct Sent;
struct Recvd;

struct Chan<S> {
    _state: PhantomData<S>,
}

impl Chan<Start> {
    fn connect() -> Self {
        Chan { _state: PhantomData }
    }

    fn send(self, _value: i32) -> Chan<Sent> {
        Chan { _state: PhantomData }
    }
}

impl Chan<Sent> {
    fn recv(self) -> (String, Chan<Recvd>) {
        (String::from("ok"), Chan { _state: PhantomData })
    }
}

impl Chan<Recvd> {
    fn close(self) {
        // Channel consumed and dropped.
    }
}

fn correct_client() {
    let c = Chan::<Start>::connect();
    let c = c.send(42);
    let (msg, c) = c.recv();
    println!("{}", msg);
    c.close();
}

시퀀스가 프로토콜과 정확히 일치하기 때문에 이것은 컴파일된다. Chan<Start>에서 recv를 호출하거나 send를 두 번 호출하려고 하면 컴파일러는 거부한다. state machine은 더 이상 런타임의 관심사가 아니다. 타입 오류다.

이것은 정말 강력한 아이디어다. 또한 이것은 최근까지 대부분의 언어가 표현할 수 없었던 아이디어이기도 하다.

선형 타입은 관문이며, 인체공학적으로는 가혹하다

위의 타입 시스템 트릭은 모든 메서드가 self를 소비하기 때문에만 작동한다. 채널을 이동한 후에는 사용할 수 없다. 이것이 선형성이다: 모든 값은 정확히 한 번 사용되어야 하며, 컴파일러가 이를 강제한다.

선형성은 틈새 취향이 아니다. 세션 타입을 위한 엄격한 요구사항이다. 채널을 복사해서 두 복사본으로 보낼 수 있다면, 프로토콜 상태는 분기할 것이다. 닫지 않고 채널을 드롭할 수 있다면, 다른 쪽은 영원히 멈출 것이다. 타입 시스템은 별칭 없이, 누출 없이, 채널의 전체 수명 주기를 추적해야 한다.

주류 언어는 수십 년 동안 별칭을 쉽게 만들고 메모리 관리를 암묵적으로 하는 타입 시스템을 구축하는 데 보냈다. C, C++, Java, Python, JavaScript, Go. 이들 중 어느 것도 선형 타입을 가지고 있지 않다. 이러한 언어에서 세션 타입의 구현은 실행 시간 검사에 의존해야 할 것이며, 그것은 본말이 전도된다.

OCaml과 Haskell은 강력한 타입 시스템을 가지고 있지만, 심지어 그들도 기본적으로 선형성을 강제하지 않는다. 채널을 변수에 바인딩하고 무시할 수 있다. 가비지 컬렉터는 언젠가 정리할 것이지만, “언젠가”는 명시적인 종료 메시지가 필요한 프로토콜에 대해서는 충분하지 않다.

Rust는 선형성에 근사하는 대여 검사기를 가진 첫 번째 주류 언어다. 이것은 우연이 아니다. Rust의 소유권 모델은 세션 타입이 연구 실험실을 떠나는 데 정확히 필요했던 것이다. crates.io의 session_types 크레이트는 Rust의 소유권 시스템 위에 완전한 이진 및 다자 세션 타입을 구현한다. 이것은 작동한다. 사용하는 것도 신경질적이며, 선형 추론은 원래 신경질적인 것이다.

세션 타입은 대부분의 개발자가 급하게 느끼지 않는 문제를 해결한다

여기 불편한 진실이 있다. 업계는 세션 타입 없이 분산 컴퓨팅의 전체 스택을 구축했으며, 대부분의 경우 작동했다. REST, HTTP를 통한 JSON, gRPC, GraphQL. 이들 모두는 프로토콜 수준에서 타입이 지정되지 않거나 약하게 타입이 지정된 프로토콜이다. gRPC 클라이언트는 순서를 무시하고 메서드를 호출하거나, 잘못된 페이로드를 전달하거나, 스트림을 중단시킬 수 있다. 오류는 일반적으로 400 Bad Request 또는 끊어진 연결로서 런타임에 나타난다.

이러한 런타임 오류는 성가시지만, 치명적인 경우는 드물다. HTTP는 무상태이므로 손상시킬 장기 채널이 없다. JSON 스키마는 메시지 경계에서 검증되며, 다단계 대화를 통해 검증되지 않는다. 웹의 전체 아키텍처는 세션 타입이 해결하는 정확한 문제를 피하기 위해 설계되었다. 왜냐하면 웹은 세션 타입을 표현할 수 없는 언어를 위해 설계되었기 때문이다.

세션 타입은 프로토콜 충실도가 매우 중요한 도메인에서 빛난다: 금융 거래 시스템, 하드웨어 제어 프로토콜, 안전에 필수적인 메시지 전달. 이러한 도메인은 존재하지만, 대부분의 개발자가 대부분의 시간을 보내는 곳은 아니다. 일반적인 웹 API의 경우, 각 엔드포인트 상호작용을 선형 타입 시스템에 인코딩하는 비용은 OpenAPI와 몇 가지 통합 테스트가 훨씬 더 적은 마찰로 동일한 버그를 잡을 때 정당화하기 어렵다.

분산 시스템은 프로토콜 순서보다 더 어려운 문제를 가지고 있다

프로토콜 충실도가 중요한 곳에서도 세션 타입은 오류의 한 클래스만 해결한다. 두 참가자가 연결된 상태로 선의를 유지하면 메시지가 올바른 순서로 도착함을 보장한다.

네트워크가 온라인 상태를 유지함을 보장하지는 않는다.

세션 타입은 리트라이, 타임아웃, 네트워크 분할, 충돌 복구에 대해 할 말이 없다. 선형 타입은 채널을 닫도록 강요할 수 있지만, 원격 호스트가 재부팅하기 전에 종료를 확인하도록 강요할 수는 없다. 분산 시스템의 어려운 문제는 해피 패스 순서가 아니라 장애 모드다. 세션 타입은 수학적 우아함으로 해피 패스를 다루기 때문에 연구에서 번성했다. 프로덕션 시스템은 장애 모드 속에서 살아가기 때문에 거기에 남아 있었다.

생태계는 마침내 변화하고 있지만, 느리게

Rust는 유일한 진보의 징후가 아니다. Pony나 실험적인 Austral과 같은 언어는 선형 타입이나 아핀 타입을 핵심 설계에 명시적으로 내장하고 있다. 아카데믹 컴파일러는 이제 세션 타입이 지정된 인터페이스를 가진 WebAssembly를 타겟팅하고 있다. IETF는 심지어 프로토콜 표준에 대한 세션 타입이 지정된 사양을 조사하기도 했다.

진정한 돌파구는 단일 언어 기능이 아니다. 컴파일 시간 안전을 학문적 사치가 아닌 생산성 도구로 여기는 문화적 변화의 느린 변모다. 메모리 안전이 C 프로그래머의 부담에서 Rust의 판매 포인트가 되었을 때, 그것은 선형 추론의 다른 응용에 대한 문을 열었다. 세션 타입은 그 물결을 타고 있지만, 여전히 해안 근처에 있다.

오늘 세션 타입을 시도해 보고 싶다면 Rust와 session_types 크레이트부터 시작하라. 이것은 컴파일 시간에 완전한 세션 타입 검사를 가진 채널 원시 요소를 제공한다. 다음은 해당 크레이트를 사용한 최소한의 서버-클라이언트 쌍이다:

use session_types::*;

// Client sends i32, receives String, ends.
type ClientProto = Send<i32, Recv<String, Eps>>;

// Server receives i32, sends String, ends.
type ServerProto = Recv<i32, Send<String, Eps>>;

fn client(c: Chan<(), ClientProto>) {
    let c = c.send(42);
    let (msg, c) = c.recv();
    println!("Got: {}", msg);
    c.close();
}

fn server(c: Chan<(), ServerProto>) {
    let (n, c) = c.recv();
    let c = c.send(format!("You sent {}", n));
    c.close();
}

이것은 session_types로 컴파일되고 프로토콜을 타입 수준에서 강제하는 실제 코드다. 한계는, 언제나처럼, 양쪽 모두 타입에 동의해야 한다는 것이다. 선형 프로토콜에 대한 점진적 도입은 없다. 마이크로서비스를 세션 타입으로 지정하고, 나머지 함대는 확인되지 않은 상태로 둘 수 있다.

Rust의 타입 상태 패턴부터 시작하라

연구용 크레이트를 도입하지 않아도 세션 타입에서 가치를 얻을 수 있다. 첫 번째 예제의 타입 상태 패턴은 실용적인 중간 단계다. 프로토콜을 일련의 타입으로 정의하고, 모든 전환에서 상태를 소비하고, 컴파일러가 스테이징에 도달하기 전에 시퀀스 오류를 잡도록 하라.

이것은 완전한 세션 타입 시스템이 아니다. 분기, 재귀, 다자 프로토콜을 처리하지 않는다. 그러나 외부 의존성 없이 오버헤드 제로로 런타임 프로토콜 버그의 전체 범주를 제거한다.

그것은 시작하기에 합리적인 곳이다. 나머지에 준비가 되었을 때, 연구 논문은 여전히 거기에 있을 것이다.