Session types 發明於 1993 年。三十年後,大多數網路服務仍然用手寫的執行期檢查來驗證protocol狀態,如果它們會驗證的話。你的型別系統對於用戶端是否在 HELLO 之前就傳送 PONG,或者是否因為有人忘了關閉連線而導致連線洩漏,完全無從置喙。

研究社群數十年前就有了對策。這從來不是理論問題。問題在於 session types 需要一項多數主流語言花了三十年拒絕實作的功能:linear types。

Session type 就是一台由編譯器幫你檢查的 state machine

每個網路protocol都是一台state machine。一個簡單的請求-回應protocol看起來像這樣:用戶端傳送一個 i32,伺服器回傳一個 String,然後通道關閉。如果用戶端在寫入之前就嘗試讀取,或者任一方忘了關閉連線,protocol就被違反了。

在一般的程式碼庫中,你用註解、慣例、也許還有一個手寫的列舉來在執行期追蹤狀態。那個列舉是一台小小的直譯器。它活在你的腦袋裡、文件裡、以及缺陷追蹤系統裡。

Session types 把這台state machine搬進型別系統。通道的型別在每次操作後都會改變。傳送一個整數,通道的型別就變成「等待接收字串」。接收字串後,型別變成「必須關閉」。順序錯誤地使用通道,你會得到編譯錯誤,而不是正式環境中的protocol違規。

以下是用 Rust 的 type-state pattern 來編碼 session type 的樣子,無需任何外部依賴:

use std::marker::PhantomData;

// protocol狀態: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) {
        // 通道被消耗並釋放。
    }
}

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

這段程式碼能編譯,因為順序完全符合protocol。嘗試在 Chan<Start> 上呼叫 recv,或者呼叫兩次 send,編譯器就會拒絕。state machine不再是執行期的問題。它是一個型別錯誤。

這確實是個強大的概念。但同時也是一個直到最近大多數語言都無法表達的概念。

Linear types 是守門人,而且它們對開發者極不友善

上面的型別系統技巧之所以可行,是因為每個方法都消耗了 self。你不能在移動了一個值之後繼續使用它。這就是 linearity:每個值必須恰好使用一次,由編譯器強制執行。

Linearity 不是小眾偏好。它是 session types 的硬性要求。如果你能複製一個通道並在兩份複本上傳送,protocol狀態就會分歧。如果你能在不關閉的情況下丟棄一個通道,另一端就會永遠懸置。型別系統必須在整個生命週期中追蹤通道,不允許別名,也不允許洩漏。

主流語言花了數十年建立讓別名變得容易、讓記憶體管理隱式的型別系統。C、C++、Java、Python、JavaScript、Go。它們全都沒有 linear types。在這些語言中,session type 的實作必須退回到執行期檢查,而這就違背了初衷。

OCaml 和 Haskell 擁有強大的型別系統,但即使它們預設也不強制執行 linearity。你可以把通道綁定到一個變數然後忽略它。垃圾回收器最終會清理它,但「最終」對於一個需要明確關閉訊息的protocol來說是不夠的。

Rust 是第一個擁有近似 linearity 的 borrow checker 的主流語言。這絕非巧合。Rust 的 ownership model 正是 session types 逃出研究實驗室所需要的。crates.io 上的 session_types crate 在 Rust 的 ownership system 之上實作了完整的雙方與多方 session types。它運作正常。但用起來也很挑剔,因為 linear reasoning 本來就很挑剔。

Session types 解決了一個多數開發者並未強烈感受到的問題

以下是令人不安的真相。產業在沒有 session types 的情況下建構了整套分散式運算堆疊,而且大致上運作正常。REST、JSON over HTTP、gRPC、GraphQL。這些在protocol層級全都是無型別或鬆散型別的。gRPC 用戶端可以亂序呼叫方法、傳送格式錯誤的酬載、或讓串流懸置。錯誤在執行期浮現,通常表現為 400 Bad Request 或連線中斷。

那些執行期錯誤很惱人,但很少是致命的。HTTP 是無狀態的,因此沒有長期存在的通道會被汙染。JSON schema 在訊息邊界處驗證,而非跨越多步驟的對話。整個網頁架構的設計就是為了迴避 session types 所解決的問題,因為網頁是為無法表達 session types 的語言設計的。

Session types 在protocol正確性至關重要的領域發光發熱:金融交易系統、硬體控制protocol、安全關鍵的訊息傳遞。這些領域存在,但它們不是多數開發者花費大部分時間的地方。對於典型的網頁 API,當 OpenAPI 加上幾個整合測試就能用遠低摩擦的方式抓到同樣的錯誤時,要把每個端點互動都編碼進 linear type system 的額外負擔很難說得過去。

分散式系統有比protocol順序更棘手的問題

即使在意protocol正確性的地方,session types 也只解決了一類錯誤。它們保證的是:如果雙方都保持連線且行為正確,訊息就會以正確的順序送達。

它們不保證網路不會斷線。

Session type 對於重試、逾時、網路分區或崩潰復原都無從置喙。Linear type 可以強迫你關閉一個通道,但它無法強迫遠端主機在重開機前確認關閉。分散式系統中的難題是失敗模式,而非正常路徑的順序。Session types 以數學優雅處理了正常路徑,這就是為何它們在研究領域蓬勃發展。產品系統活在失敗模式之中,這就是為何它們始終留在那裡。

生態系終於在轉變,但速度緩慢

Rust 不是唯一的進展指標。Pony 這類語言,以及實驗性的 Austral,都明確將 linear 或 affine types 納入核心設計。學術編譯器現在開始針對具備 session-typed 介面的 WebAssembly 產出程式碼。IETF 甚至探索過以 session-typed 規格來制定protocol標準。

真正的突破不是任何單一語言功能。而是編譯期安全性從學術奢侈品轉變為生產力工具的緩慢文化轉向。當記憶體安全性從 C 程式設計師的負擔變成 Rust 的賣點時,它為其他 linear reasoning 的應用開啟了大門。Session types 正乘著這股浪潮,但它們仍靠近岸邊。

如果你想在今天嘗試 session types,從 Rust 和 session_types crate 開始。它在編譯期提供具備完整 session type 檢查的通道原語。以下是用這個 crate 寫成的最小伺服器-用戶端配對:

use session_types::*;

// 用戶端傳送 i32,接收 String,結束。
type ClientProto = Send<i32, Recv<String, Eps>>;

// 伺服器接收 i32,傳送 String,結束。
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 編譯的實際程式碼,並在型別層級強制執行protocol。限制一如既往:雙方必須在型別上達成共識。Linear protocol 沒有漸進採納這回事。你不能只給一個微服務加上 session type,而讓艦隊的其餘部分不受檢查。

從 Rust 的 type-state pattern 開始

你不需要採用研究等級的 crate 就能從 session types 獲得價值。第一個範例所示的 type-state pattern 是個實用的過渡步驟。把你的protocol定義成一系列型別,在每次轉換時消耗狀態,讓編譯器在錯誤到達 staging 環境之前就抓到順序錯誤。

這不是完整的 session type 系統。它不處理分支、遞迴或多方protocol。然而,它能以零額外負擔、無外部依賴的方式消滅一整類執行期protocol錯誤。

這是個合理的起點。研究論文會在你準備好繼續深入時仍然等在那裡。