Designing with Static Capabilities and Effects: Use, Mention, and Invariants

TL;DR

This paper compares static capabilities and effect systems, analyzing their trade-offs and interactions in restricting and reasoning about effects in programming, with insights from prior systems and subtle type system aspects.

Contribution

It provides a systematic discussion of the trade-offs between static capabilities and effect systems, highlighting subtle type system factors affecting their effectiveness.

Findings

Trade-offs between static capabilities and effect systems are context-dependent.

Minor type system aspects significantly influence system efficacy.

Historical analysis of prior systems illustrates these trade-offs.

Abstract

Capabilities (whether object or reference capabilities) are fundamentally tools to restrict effects. Thus static capabilities (object or reference) and effect systems take different technical machinery to the same core problem of statically restricting or reasoning about effects in programs. Any time two approaches can in principle address the same sets of problems, it becomes important to understand the trade-offs between the approaches, how these trade-offs might interact with the problem at hand. Experts who have worked in these areas tend to find the trade-offs somewhat obvious, having considered them in context before. However, this kind of design discussion is often written down only implicitly as comparison between two approaches for a specific program reasoning problem, rather than as a discussion of general trade-offs between general classes of techniques. As a result, it is not uncommon to set out to solve a problem with one technique, only to find the other better-suited. We discuss the trade-offs between static capabilities (specifically reference capabilities) and effect systems, articulating the challenges each approach tends to have in isolation, and how these are sometimes mitigated. We also put our discussion in context, by appealing to examples of how these trade-offs were considered in the course of developing prior systems in the area. Along the way, we highlight how seemingly-minor aspects of type systems -- weakening/framing and the mere existence of type contexts -- play a subtle role in the efficacy of these systems.