protocols

会话类型如何将死锁转化为编译器错误

会话类型将通信协议编码到你的类型系统中，在代码运行之前将消息传递不匹配转化为编译器错误。

死锁本应该是运行时问题。这就是它们如此烦人的原因。你的代码编译干净，测试通过，然后它在生产环境中卡住，因为进程A在等待进程B，而进程B在等待进程A。 会话类型扭转了这一点。它们将进程之间的通信协议编码到类型系统本身中。某些类别的死锁不再是运行时的意外，而开始成为编译器错误。你字面意义上无法编写会导致死锁的代码。…