We propose algebraic protocols that enable the definition of protocol templates and session types analogous to the definition of domain-specific types with algebraic datatypes. Parameterized algebraic protocols subsume all regular as well as most context-free and nested session types and, at the same time, replace the expensive superlinear algorithms for type checking by a nominal check that runs in linear time. Algebraic protocols in combination with polymorphism increase expressiveness and modularity by facilitating new ways of parameterizing and composing session types.
翻译:我们提出了代数协议,它们使得可以定义协议模板和会话类型,类似于使用代数数据类型定义特定领域类型。可参数化的代数协议包含了所有常规的、大多数上下文自由的和嵌套的会话类型,并且通过名义检查以线性时间运行,取代了昂贵的超线性类型检查算法。代数协议与多态相结合,通过便于新的会话类型参数化和组合的方式,提高了表达性和模块化。