论文标题
多态效应的范围功能
Scoped Capabilities for Polymorphic Effects
论文作者
论文摘要
类型系统通常表征值的形状，而不是其自由变量。但是，如果一个人知道值捕获的自由变量，则可以保证许多理想的安全属性。我们描述了CCSUBBOX，这是一种微积分，其中这种捕获的变量在类型中简洁地表示，并证明它可用于通过范围的功能安全地实现效果和效应多态性。我们讨论了跟踪捕获变量的决定如何指导微积分的关键方面，并表明CCSUBBOX允许对常见数据结构及其典型用法模式的简单和直观类型。我们演示了如何使用这些想法来指导用实用的编程语言实施捕获检查的实施。
Type systems usually characterize the shape of values but not their free variables. However, many desirable safety properties could be guaranteed if one knew the free variables captured by values. We describe CCsubBox, a calculus where such captured variables are succinctly represented in types, and show it can be used to safely implement effects and effect polymorphism via scoped capabilities. We discuss how the decision to track captured variables guides key aspects of the calculus, and show that CCsubBox admits simple and intuitive types for common data structures and their typical usage patterns. We demonstrate how these ideas can be used to guide the implementation of capture checking in a practical programming language.
