Computer Science Department
School of Computer Science, Carnegie Mellon University
A Modal Calculus for Effect Handling
In this paper we adopt a different approach, founded on the observation of Pfenning and Davies that an abstract monad can be decomposed in terms of modal operators for possibility &lang〉 and necessity Box. Our idea is to use the Box modality (which is a comonad) for hygienic propagation of effects, and leave the globalization of effects scope to &lang〉.
Then the effects which admit a natural notion of handling can be encoded using &Box; since they are not global, there is no need to push them under &lang〉.
Based on this idea, we develop a general framework for effect handling systems, and obtain novel calculi for exceptions, catch-and-throw and composable continuations as specific instantiations.