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.
翻译:我们提出代数协议,使得能够以类似于代数数据类型定义领域特定类型的方式,定义协议模板与会话类型。参数化代数协议涵盖了所有正则型以及大多数上下文无关和嵌套会话类型,同时将类型检查中代价高昂的超线性算法替换为线性时间内运行的名称检查。代数协议与多态性相结合,通过促进会话类型参数化与组合的新方式,提升了表达能力和模块化程度。