多态代数效应的签名限制
Signature Restriction for Polymorphic Algebraic Effects
AI总结：
本研究提出签名限制新概念，通过限制效应接口中操作的类型签名，确保多态效应在多态类型赋值下的类型安全性，并开发类型与效应系统以兼容两类操作。
摘要：
众所周知，多态效应与多态类型赋值的朴素组合会破坏类型安全性。解决该问题的现有方法分为两类：一类限制效应的触发方式，另一类限制效应的实现方式。本研究探索了一种在多态类型赋值中确保多态效应安全性的新方法。我们工作的新颖之处在于发现了对效应接口的限制。为形式化我们的想法，我们采用代数效应与处理器，其中效应接口由一组操作及其类型签名组成。我们提出了签名限制这一新概念，用于限制操作的类型签名，并证明签名限制足以确保配备了无限制多态类型赋值的效应语言的安全性。我们还开发了一个类型与效应系统，使得在同一程序中既能使用满足签名限制的操作，也能使用不满足签名限制的操作。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
