Formal Foundations of Capture Tracking

Type systems are a device for verifying properties of programs without running them. Many programming languages used in the industry have always had a type system, while others were initially created without a type system and later adopted one, when the advantages of doing so became apparent. Most such type systems stop at verifying that operations are invoked on appropriate operands, e.g., that we do not add characters and do not ask for the length of an integer. Still, verifying many desirable properties requires a type system that can describe what sort of operations a program might invoke. For instance, if a certain part of the program is interpreted during compilation, we would prefer this part to refrain from accessing operations whose result is non-deterministic, such as querying a database.

Naturally, various type systems which can verify such properties were proposed, with key areas including effect systems, resource ownership systems and object capabilities. The outward differences of these systems result in each of them being typically studied in the context of different categories of properties. Of course, ideally we would want to verify as many properties as possible, yet naively integrating different approaches in a single system does not provide good results in practice. Moreover, the industry has so far been slow to adopt the aforementioned systems, arguably because they are not yet sufficiently ergonomic and the costs of applying them outweigh their numerous advantages.

I describe Capture Tracking, an approach which views both effects and resources through the lens of capabilities tracked in types. The capability angle solves usability problems associated with effect and resource ownership systems and provides a uniform framework for verifying a wide range of properties. I present the key principles of Capture Tracking with the SCC system and discuss how to extend it with type polymorphism based on two other systems, CF