A Study of Capability-Based Effect Systems

The problem of effect polymorphism is a major obstacle to wide adoption of effect systems in the programming community. The absence of effect systems reduces compiler optimization opportunities and disables effect constraints on APIs in parallel and distributed computations. This study shows that capability-based effect systems, equipped with stoic functions and free functions, can easily solve the problem of effect polymorphism without incurring notational burden on programmers. With this advantage, capability-based effect systems stand a better chance to be adopted by the programming community. The central idea of capability-based effect system is that a capability is required in order to produce side effects. If capabilities are passed as function parameters, by tracking capabilities in the type system we can track effects in the program. To ensure that capabilities are passed through function parameters, instead of being captured from the environment, we need to impose a variable-capturing discipline, stipulating that capa- bility variables cannot be captured. Functions observing the discipline are called stoic functions, while functions not observing the discipline are called free functions.