a1 School of Computing, National University of Singapore, Singapore (e-mail: [email protected])
a2 Department of Applied Mathematics and Computer Science Ghent University, Ghent, Belgium (e-mail: [email protected])
a3 Department of Computer Science, University of Texas at Austin, University Station, Austin, TX, USA (e-mail: [email protected])
Incremental Programming (IP) is a programming style in which new program components are defined as increments of other components. Examples of IP mechanisms include Object-oriented programming inheritance, aspect-oriented programming advice, and feature-oriented programming. A characteristic of IP mechanisms is that, while individual components can be independently defined, the composition of components makes those components become tightly coupled, sharing both control and data flows. This makes reasoning about IP mechanisms a notoriously hard problem: modular reasoning about a component becomes very difficult; and it is very hard to tell if two tightly coupled components interfere with each other's control and data flows. This paper presents modular reasoning about interference (MRI), a purely functional model of IP embedded in Haskell. MRI models inheritance with mixins and side effects with monads. It comes with a range of powerful reasoning techniques: equational reasoning, parametricity, and reasoning with algebraic laws about effectful operations. These techniques enable MRI in the presence of side effects. MRI formally captures harmlessness, a hard-to-formalize notion in the interference literature, in two theorems. We prove these theorems with a non-trivial combination of all three reasoning techniques.