A flow-insensitive, modular effect system for purity

Abstract

This article presents a modular, flow-insensitive type-and-effect system for purity with lightweight annotations. It does not enforce a global programming discipline and allows arbitrary effects to occur in impure parts of the program. The system is designed to support higher-order languages that mix functional and imperative code like Scala or C#. We show that it can express purity of non-local programming patterns which involve mutable state such as those used in the Scala collections library. We formalize the type system using a functional language with mutable records and define type and effect soundness.