会话类型发明于1993年。三十年后,大多数网络服务仍然通过手写运行时检查来验证协议状态,如果它们验证的话。类型系统对于客户端是否在HELLO之前发送了PONG,或者连接是否因为某人忘记关闭而泄漏,完全没有任何意见。

研究界几十年来一直拥有这个问题的解决方案。问题从来不是理论性的。问题是会话类型需要一种大多数主流语言三十年间都拒绝实现的功能:线性类型。

会话类型是编译器替你检查的状态机

每个网络协议都是状态机。一个简单的请求-响应协议看起来是这样的:客户端发送一个i32,服务器用String响应,然后通道关闭。如果客户端尝试在写入之前读取,或者某一方忘记关闭连接,协议就被违反了。

在典型的代码库中,你通过注释、约定,以及可能的手写Enum来强制执行这一点,这个Enum在运行时跟踪状态。这个Enum是一个微小的解释器。它存在于你的脑海中、文档中、缺陷跟踪器中。

会话类型将这个状态机移入类型系统。通道的类型在每次操作后都会改变。你发送一个整数,通道类型变为”等待接收字符串”。你接收字符串,类型变为”必须关闭”。你乱序使用通道,你会得到编译错误,而不是生产环境中的协议违反。

以下是使用Rust中的type-state模式编码会话类型,无需外部依赖:

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,编译器会拒绝。状态机不再是运行时的关注点。它是类型错误。

这是一个非常强大的想法。同时这也是一个大多数语言直到最近才能表达的想法。

线性类型是看门人,而且人机工程学上很严苛

上述类型系统的技巧之所以有效,仅仅是因为每个方法都消耗了self。移动通道后你就不能再使用它了。这就是线性:每个值必须恰好使用一次,编译器强制执行这一点。

线性不是小众偏好。它是会话类型的硬性要求。如果你能复制通道并在两个副本上发送,协议状态就会分歧。如果你能丢弃通道而不关闭它,另一方就会永远挂起。类型系统必须在通道的整个生命周期中跟踪它,不能有别名,也不能有泄漏。

主流语言花了数十年时间构建让别名变得容易、内存管理变得隐式的类型系统。C、C++、Java、Python、JavaScript、Go。它们都没有线性类型。在这些语言中,会话类型的实现必须依赖运行时检查,这就失去了意义。

OCaml和Haskell拥有强大的类型系统,但即使它们也不默认强制线性。你可以将通道绑定到一个变量然后忽略它。垃圾回收器会在某个时候清理它,但”某个时候”对于一个需要显式关闭消息的协议来说是不够好的。

Rust是第一个拥有能够近似线性的借用检查器的主流语言。这不是巧合。Rust的所有权模型正是会话类型离开研究实验室所需要的东西。crates.io上的session_types crate在Rust所有权系统之上实现了完整的二元和多方会话类型。它有效。但用起来也让人紧张,因为线性推理本身就是紧张的。

会话类型解决了一个大多数开发者并不急迫感受到的问题

这里有个令人不安的真相。业界在没有会话类型的情况下构建了一整套分布式计算栈,而且大多数时候都能工作。REST、基于HTTP的JSON、gRPC、GraphQL。这些都是在协议层面无类型或弱类型的协议。gRPC客户端可以乱序调用方法、传递格式错误的负载、或让流挂起。错误在运行时出现,通常表现为400 Bad Request或连接断开。

这些运行时错误很烦人,但很少是致命的。HTTP是无状态的,所以没有长期运行的通道可以被破坏。JSON模式在消息边界处验证,而不是通过多步对话。整个Web架构的设计就是为了避免会话类型所解决的精确问题,因为Web是为无法表达会话类型的语言设计的。

会话类型在协议保真度极其重要的领域闪耀:金融交易系统、硬件控制协议、安全关键的消息传递。这些领域存在,但不是大多数开发者花费大部分时间的地方。对于一个典型的Web API,将每个端点交互编码到线性类型系统中的成本,在OpenAPI和一些集成测试就能用更少的摩擦捕获相同缺陷的情况下,是很难证明其合理性的。

分布式系统有比协议顺序更难的问题

即使在协议保真度很重要的地方,会话类型也只解决了一类错误。它们保证如果双方保持连接且善意运行,消息会按正确顺序到达。

它们不保证网络保持在线。

会话类型对重试、超时、网络分区或崩溃恢复没有任何发言权。线性类型可以强迫你关闭通道,但无法强迫远程主机在重启前确认关闭。分布式系统中的难题是故障模式,而不是快乐路径的顺序。会话类型以数学上的优雅解决了快乐路径,这就是它们在研究中蓬勃发展原因。生产系统生活在故障模式中,所以它们留在了那里。

生态系统终于开始转变,但很慢

Rust不是唯一的进步信号。像Pony和实验性的Austral这样的语言正在将线性或仿射类型显式构建到其核心设计中。学术编译器现在以带会话类型接口的WebAssembly为目标。IETF甚至探索了会话类型规范用于协议标准。

真正的突破不是单一语言特性。它是向编译时安全作为生产力工具而非学术奢侈的缓慢文化转变。当内存安全从C程序员的负担变成Rust的卖点时,它为线性推理的其他应用打开了大门。会话类型正乘着这波浪潮,但仍然靠近岸边。

如果你想今天尝试会话类型,从Rust和session_types crate开始。它提供具有完整编译时会话类型检查的通道原语。以下是使用该crate的最小服务器-客户端对:

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的type-state模式开始

你不需要采用研究用的crate就能从会话类型中获得价值。第一个例子中的type-state模式是一个实用的中间步骤。将你的协议定义为一系列类型,在每次转换时消耗状态,让编译器在序列错误到达预发布环境之前捕获它们。

它不是一个完整的会话类型系统。它不处理分支、递归或多方协议。然而,它以零开销且无需外部依赖的方式消除了整个类别的运行时协议缺陷。

那是一个合理的起点。当你准备好迎接其余部分时,研究论文仍然会在那里。