Journal article
Designing with Static Capabilities and Effects: Use, Mention, and Invariants
Leibniz International Proceedings in Informatics, LIPIcs, v 166
22 May 2020
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.
Metrics
6 Record Views
11 citations in Scopus
Details
- Title
- Designing with Static Capabilities and Effects: Use, Mention, and Invariants
- Creators
- Colin S Gordon
- Publication Details
- Leibniz International Proceedings in Informatics, LIPIcs, v 166
- Resource Type
- Journal article
- Language
- English
- Academic Unit
- Computer Science
- Scopus ID
- 2-s2.0-85108910081
- Other Identifier
- 991019173783804721