论文标题
多态代数效应的签名限制
Signature Restriction for Polymorphic Algebraic Effects
论文作者
论文摘要
众所周知，多态效应和多态性分配的幼稚组合因打破类型的安全性而众所周知。现有的该问题方法分为两组：一个用于限制触发效果的方式，另一种用于限制其实施方式。这项工作探讨了一种新方法，以确保多态性分配中多态性效应的安全性。我们工作的新颖性在于找到对影响界面的限制。为了使我们的想法形式化，我们采用代数效应和处理程序，其中一组操作与类型签名一起给出了效果接口。我们提出了签名限制，这是一种限制操作类型签名的新概念，并表明签名限制足以确保配备有不受限制的多态性分配的有效语言的类型安全性。我们还开发了一个类型和效应系统，以实现两个操作，这些操作满足并且不满足单个程序中的签名限制。
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.
