Effects as Implicit Capabilities

We propose to investigate a new approach to effect checking that has an elegant solution to the effect polymorphism problem. The central idea is that instead of talking about effects we talk about capabilities. For instance, instead of saying a function “throws an IOException” we say that the function “needs the capability to throw an IOException”. Capabilities are modeled as values of some capability type. For instance, the aforementioned capability could be modeled as a value of type CanThrow[IOException]. A function that might throw an IOException needs to have access to an instance of this type. Typically it takes an argu- ment of the type as a parameter. It turns out that that the treatment of effects as capabilities gives a simple and natural solution to the problem of effect polymorphism.