一句话:将会话类型的线性约束放宽为仿射性,引入优雅错误处理并保持会话不会卡死的进展性。
会话类型通过线性来保证并发环境下通道严格按类型规定的顺序通信,避免干扰。本文把线性约束放宽为仿射性:通道至多执行类型规定的行为,而非必须完整执行。这个更宽松的设定使语言可以自然集成一种优雅的错误处理机制,相较已有基于异常的工作更简洁且有所改进。作者在保留会话类型核心保证的同时考察其与异常、错误终止的交互,并证明该处理不会损害语言的进展性质:会话不会卡死。
Session types describe the structure of communications implemented by channels. In particular, they prescribe the sequence of communications, whether they are input or output actions, and the type of value exchanged. Crucial to any language with session types is the notion of linearity, which is essential to ensure that channels exhibit the behaviour prescribed by their type without interference in the presence of concurrency. In this work we relax the condition of linearity to that of affinity, by which channels exhibit at most the behaviour prescribed by their types. This more liberal setting allows us to incorporate an elegant error handling mechanism which simplifies and improves related works on exceptions. Moreover, our treatment does not affect the progress properties of the language: sessions never get stuck.