research

会话类型是有效的。大多数语言只是拒绝实现它们。

会话类型将通信协议编码到类型系统中，将运行时协议错误转化为编译时错误。以下是它们为何在论文中停留三十年才被生产代码采用的原因。

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