一句话：提出签名限制，通过约束代数效应操作的类型签名，在多态类型赋值下保障多态效应的类型安全。
多态效应与多态类型赋值的朴素结合会破坏类型安全。已有方案要么限制效应如何触发，要么限制效应如何实现。本文提出第三种思路：限制效应接口。作者以代数效应与 handler 为形式化框架，其中效应接口由一组带类型签名的操作给出；提出“签名限制”（signature restriction）这一新概念，限制操作的类型签名，并证明满足该限制时，带无限制多态类型赋值的效应语言仍可保证类型安全。为提升实用性，文章还设计了一个类型与效应系统，允许同一程序中同时使用满足和不满足签名限制的操作。
The naive combination of polymorphic effects and polymorphic type assignment has been well known to break type safety. Existing approaches to this problem are classified into two groups: one for restricting how effects are triggered and the other for restricting how they are implemented. This work explores a new approach to ensuring the safety of polymorphic effects in polymorphic type assignment. A novelty of our work lies in finding a restriction on effect interfaces. To formalize our idea, we employ algebraic effects and handlers, where an effect interface is given by a set of operations coupled with type signatures. We propose signature restriction, a new notion to restrict the type signatures of operations, and show that signature restriction is sufficient to ensure type safety of an effectful language equipped with unrestricted polymorphic type assignment. We also develop a type-and-effect system to enable the use of both operations that satisfy and do not satisfy the signature restriction in a single program.
@article{paperbot920,
title = {Signature restriction for polymorphic algebraic effects},
author = {Taro Sekiyama and Takeshi Tsukada and Atsushi Igarashi},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {ICFP},
year = {2020},
doi = {10.1145/3408999}
}