A Flow-Insensitive, Modular Effect System for Purity
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 ar- bitrary effects to occur in impure parts of the program. The system is designed to support higher-order languages that mix functional and imperative code, such as 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 a dynamic semantics, a type safety and an effect soundness theorem.
Cite this item
Rytz, L., Amin, N., & Odersky, M. (2013). A Flow-Insensitive, Modular Effect System for Purity. FTfJP ’13: Proceedings of the 15th Workshop on Formal Techniques for Java-like Programs. Formal Techniques for Java-like Programs, Montpellier, France. https://doi.org/10.1145/2489804.2489808
Click Copy to copy the citation, or select the text manually.
purity-ftfjp13.pdf
openaccess
302.65 KB
Adobe PDF
0cc14f7012e16e127ad3456f69f09e5f