SHF:Small:Making Effect Systems Practical with Polymorphism, Inference, and Prototyping Support

Drexel University, Philadelphia PA

Investigators

Abstract

Effect systems are extensions to the type system in a programming language that aid in checking aspects of how a program behaves, for example whether it uses concurrency constructs safely, or respects certain kinds of security policies. The most popular example is the notion of checked exceptions built into the Java programming language. Yet despite many years of research experience with effect systems, they are not widely used outside Java. This project pursues work to make effect systems easier to design, easier to implement, and easier for regular developers to apply to programs to prevent bugs. The project investigates both the theory of effect systems, such as how to extend them to non-trivial programming constructs like exceptions and generators, and their application. The project implements and applies a variety of effect systems to substantial real-world programs written in Java, using experience with that empirical evaluation to guide improvements to the theory of effect systems, focusing in particular on lightweight ways to accommodate code reuse and effect polymorphism without requiring excessive guidance from developers. The project constructs an open-source implementation framework for effect systems, which will make it easier to implement new effect systems. The project validates the framework by building open-source implementations of previously proposed and new effect systems for Java, providing tools directly useful to practicing developers. Furthermore, the project develops generic inference techniques to automatically deduce effects for many effect systems, further reducing the effort required to design, implement, and use them. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.