Abstract:
Type-and-effect systems were originally used to reason about dynamic memory manipulation. However, effect systems have proven to be quite versatile, for example able to statically track exceptions and other control effects as well as locking and other concurrency effects. Language designers can't anticipate all the useful effect systems, and different applications will require different effect systems. Therefore I argue that we need a pluggable effect system.
Today each effect system is typically implemented in a monolithic manner, hard-coding a particular syntax of effects along with particular rules to track and control those effects. A pluggable effect system, on the other hand, must provide a generic scaffolding that allows a variety of disparate effect systems to be easily expressed, statically enforced, and proven sound. In this talk I will describe a formal type-and-effect system that is generic in the above sense, and as such represents a first step toward pluggable effects.
This is joint work with Dan Marino at UCLA.