Effectful Software Contracts

Software contracts empower programmers to describe functional properties of components. When it comes to constraining effects, though, the literature offers only one-off solutions for various effects. It lacks a universal principle. This paper presents the design of an effectful contract system in the context of effect handlers. A key metatheorem shows that contracts cannot unduly interfere with a program’s execution. An implementation of this design, along with an evaluation of its generality, demonstrates that the theory can guide practice.