Title
Effects, capabilities, and boxes: from scope-based reasoning to type-based reasoning and back
Abstract
AbstractReasoning about the use of external resources is an important aspect of many practical applications. Effect systems enable tracking such information in types, but at the cost of complicating signatures of common functions. Capabilities coupled with escape analysis offer safety and natural signatures, but are often overly coarse grained and restrictive. We present System C, which builds on and generalizes ideas from type-based escape analysis and demonstrates that capabilities and effects can be reconciled harmoniously. By assuming that all functions are second class, we can admit natural signatures for many common programs. By introducing a notion of boxed values, we can lift the restrictions of second-class values at the cost of needing to track degree-of-impurity information in types. The system we present is expressive enough to support effect handlers in full capacity. We practically evaluate System C in an implementation and prove its soundness.
Year
DOI
Venue
2022
10.1145/3527320
Proceedings of the ACM on Programming Languages
Keywords
DocType
Volume
effect systems, effect polymorphism, second-class values, capabilities
Journal
6
Issue
Citations 
PageRank 
OOPSLA1
0
0.34
References 
Authors
0
4