Scoped Capabilities for Polymorphic Effects

TL;DR

This paper introduces CCsubBox, a calculus that tracks free variables in types to ensure safety in effectful programming, enabling effect polymorphism and practical capture checking.

Contribution

It presents a novel type system that captures free variables in values, facilitating safe effect implementation and effect polymorphism through scoped capabilities.

Findings

CCsubBox effectively models captured variables in types.

The calculus supports safe effect polymorphism.

Practical capture checking can be guided by the proposed type system.

Abstract

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.