MRI: Modular reasoning about interference in incremental programming
Oliveira, Bruno C. D. S
Cook, William R
- Publisher: NEW YORK
modularity | Haskell | parametricity | monads
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 (OOP) inheritance, aspect-oriented programming
(AOP) advice and feature-oriented programming (FOP). 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 modular reasoning about interference 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.