ZU064-05-FPR

paper

22 August 2012

14:18

Under consideration for publication in J. Functional Programming

1

MRI: Modular Reasoning about Interference inIncremental Programming
BRUNO C. D. S. OLIVEIRANational University of Singapore
TOM SCHRIJVERS
Dept. of Applied Mathematics and Computer Science
Ghent University, Belgium
WILLIAM R. COOK
University of Texas at Austin, USA

Abstract
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 totell 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 comeswith 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.

1 Introduction
Cook and Palsberg (1989) define Incremental Programming (IP) as a programming stylein which new program components are defined as increments of existing ones. Objectoriented programming (OOP) inheritance (Dahl & Nygaard, 1966) is probably the mostwidely used mechanism for IP; other specialized forms of IP include variants of inheritancesuch as mixins (Bracha & Cook, 1990; Flatt et al., 1998); aspect-oriented programming(AOP) (Kiczales et al., 1997) and feature-oriented programming (FOP) (Prehofer, 1997).
A characteristic of IP systems is that the control and data flows between the derived andthe original components are quite complex, since control flows back and forth between
components in a composition. In other words, despite being textually separated, IP components are semantically coupled. This makes reasoning a significant challenge: it is hard toZU064-05-FPR

paper

2

22 August 2012

14:18

B. Oliveira, T. Schrijvers and W. Cook

understand a component in isolation, and it is hard to understand the interaction between
components. The former problem is known as modular reasoning and has been intensely
studied in the OOP and AOP literature (Stata & Guttag, 1995; Kiczales & Mezini, 2005;
Aldrich, 2005). The latter problem, usually referred to as interference, has also received
much attention in the AOP literature (Rinard et al., 2004; Douence et al., 2004; Dantas& Walker, 2006; Clifton et al., 2007; Bagherzadeh et al., 2011); and the OOP literatureaddresses symptoms of interference (Clifton et al., 2007), but is perhaps less aware of thegeneral notion.
The essence of both problems lies in the hidden control and data flows required by thetight coupling of components but not visible from the interfaces of these same components.
Because IP systems share similar characteristics and problems, it is reasonable to expectthat there is a general framework which can describe those systems. The benefits of suchgeneral framework is that once it is shown that a certain property holds in the generalframework, the fact that that property holds for particular instances comes for free.
One such framework is the denotational model of inheritance proposed by Cook (1989),
which serves as the starting point for this article. This model uses traditional techniques of
fixed-point theory, allowing inheritance to be understood compositionally. One advantage
is that modular reasoning is to an extent possible since no effects are considered. In otherwords, the setting is a variation of a pure lambda calculus in which equational reasoning ispossible. The benefits of purely functional settings for modular reasoning about forms of
IP have been explored in more detail by other authors. Most prominently, Open Modules(Aldrich, 2005) support reasoning about tightly coupled components. In Open Modules,
effects are not considered and modular reasoning about components is possible throughlogical relations, which play a similar role to equational reasoning in more conventional
purely functional languages. By not allowing any effects, the biggest obstacle to reasoning
is removed. Unfortunately, this solution is not effective in practice, as almost all practicaluses of IP involve effects.
The latter observation leads us to the principal goal of this article, which concerns
answering the question of whether it is possible to have a model of IP with effects, while
supporting both modular reasoning and reasoning about non-interference of effects. To
our knowledge there is no IP approach capable of handling both reasoning concerns at
the same time. This is understandable because the introduction of implicit effects is wellknown to destroy the nice reasoning properties of pure languages. It thus seems that wehave a dilemma: on the one hand it is possible to have a pure language with modular
reasoning properties, but in which most interesting uses of IP are not possible; and on theother hand it is possible to have an impure language in which interesting uses of IP are
possible, but modular reasoning is significantly undermined. Indeed this has lead someauthors, including Kiczales and Mezini (2005), to argue that modular reasoning aboutmechanisms that capture crosscutting concerns (a particular yet significant case of IP) issimply not possible, and that a degree of global analysis is always needed.
Inspired by research on handling effects in purely functional languages, we propose
modular reasoning about interference (MRI) in incremental programming as an extensionof Cook’s semantic model of inheritance with explicit effects through the use of monads (Wadler, 1992a). This enables uses of IP involving effects without losing the purity andthe reasoning properties of the model. We do not devise a novel core language, but reuse

ZU064-05-FPR

paper

22 August 2012

14:18

MRI: Modular Reasoning about Interference in Incremental Programming3

the well-studied polymorphic λ -calculus, System Fω (Reynolds, 1974), extended with recursion and benefit from the many established technical results. Like other authors (Wadler,
1989; Voigtländer, 2009), we use Haskell as a convenient source language for System Fω
and elaborate the model as a Haskell library1 .
Our model is well-suited to make formal statements about non-interference. Inspired by
Dantas and Walker’s (2006) notion of harmless advice, we express two non-trivial theorems about harmless mixin inheritance. This is possible because of the purely functional
nature of our setting, which provides us with a range of powerful techniques to reason aboutsuch formal statements: equational reasoning, parametricity and reasoning with algebraiclaws about (monadic) effectful operations.
MRI is a compelling application of the latter two techniques, which are particularly
relevant for reasoning about effectful programs, but have been relatively unexplored sofar. Most importantly, these techniques allow powerful forms of modular reasoning: parametricity enables reasoning based on types only and not the implementation of components, while algebraic laws support reasoning independent of the implementation details
of effects (monads). With respect to parametricity our work builds on foundational work by
Voigtländer (2009) and shows how parametric properties about effectful programs are important to state basic non-interference properties. With respect to algebraic laws our proof
for the harmless observation mixin theorem (Oliveira et al., 2010) (see also Section 5.2)
provides an application of algebraic laws for stateful monadic effects. Interestingly, while
work on reasoning about pure functional programs abounds, there is far less work on
reasoning about effectful monadic programs using algebraic laws. One notable exception
is the work by Liang and Hudak (1996), where they have shown how to reason aboutmonadic programs with laws for the reader monad. With respect to other types of effects,
and as far as we can tell, the laws about stateful monadic effects presented in Oliveira et al.
(2010) have not appeared before in the literature. More recently Gibbons and Hinze (2011)
picked up on this topic and have explored algebraic properties for various types of monadic
effects.
In summary, the contributions of this paper are:
• MRI: a purely functional model for incremental programming with effects (see Section 2). Monads make effects an integral part of each component’s interface. Thus,
MRI allows interesting, effectful, programs to be expressed, while still supporting
all the benefits of purely functional programming. We illustrate our model on aninterpreter, modularizing orthogonal aspects of computation such as logging andtracing through mixin inheritance.
• A non-trivial application of various functional programming reasoning techniques tothe notoriously hard problem of modular reasoning about inheritance in the presenceof effects. Our approach combines familiar reasoning techniques such as equational
reasoning and parametricity (see Sections 3 and 4) with some relatively unexploredtechniques to reason about effectful code. These techniques are used to prove twoharmless mixin theorems (see Section 5).

1

http://users.ugent.be/~tschrijv/MRI/ZU064-05-FPR

paper

4

22 August 2012

14:18

B. Oliveira, T. Schrijvers and W. Cook
• Two different techniques to reason about non-interference of mixin components. We
first present a simple, but non-modular approach in Section 3. This technique allows
us to reason about any non-interference of two individual components and proofs canbe easily mechanized in theorem provers like Coq. We then present a modular andmore generic approach in Section 5. This approach allows general non-interference
statements, for any given mixin and base programs, provided that they conform to asuitable type scheme and are composed with an appropriate mixin combinator.
• A classification system for mixin interference inspired by Rinard et al.’s (2004)
similar classification for AOP advice (see Section 4). We adapt Rinard et al.’s control
and data flow classification for advice to mixins and we provide a fine-grainedclassification for stateful effects.
• An implementation of the MRI model as a Haskell library using open recursion tomodel mixin inheritance and monads to model effects. The model is statically typed
and purely functional.

We believe that these results are relevant to the common problems of all IP approaches
and provide strong incentives for OOP and other IP instances based on inheritance toconsider similar solutions.
This paper is an extended version of a paper published at AOSD (Oliveira et al., 2010).
With respect to that paper we generalize the scope of our work from AOP-style advice toinheritance, elaborate on the proof techniques used and include the proofs of our theorems.
Furthermore the technique to reason about non-interference presented in Section 3 is new.
While this approach is non-modular, it has the advantage that it can be used to prove someharmlessness results that are not possible to prove with the modular technique presented in
Section 5. For example, the proof that memoization does not interfere with the Fibonacci
function (see Section 3) does not follow from the harmless mixin theorems, but can beproved directly with our new technique.

2 MRIThis section introduces the Haskell implementation of MRI using open recursion andmonads. Monads and monad transformers are introduced briefly in Section 2.2, but morethorough introductions can be found in the literature (Wadler, 1992a; Liang et al., 1995).
2.1 Open Recursion
The standard mechanism for extending a component’s behavior is through composition
or decoration. However, this only affects the external clients of the extended component,
and not the internal recursive uses. Open recursion is a way of structuring a component
that leaves recursive references open, so that the recursive behavior can be extended too.
This is the basis for modeling inheritance and mixin composition in object-oriented languages (Cook, 1989), and it also provides a simple model for some types of aspects (LopezHerrejon et al., 2006; Oliveira et al., 2010).
We now present the open recursive model of inheritance, formulated in Haskell, that isused throughout this article.

ZU064-05-FPR

paper

22 August 2012

14:18

MRI: Modular Reasoning about Interference in Incremental Programming

5

type Open s = s → s
new :: Open s → s
new a = let this = a this in thiszero :: Open s
zero = id(⊕) :: Open s → Open s → Open s
a1 ⊕ a2 = λ super → a1 (a2 super) superFig. 1. Basic inheritance model.

Inheritance Model Schematically, our denotational model of inheritance represents thecomposition of components with open recursion as follows:
thisw
p = new (a1 ⊕ ? a2 ⊕ ...
C ⊕ @ an ⊕ base)
;
super

super

super

super

The open base component provides base behavior similar to a base class, and the othermixin components a1 ,. . . ,an provide behavior extensions, similar to AOP advice or Scala’s
mixins. The inheritance operator ⊕ extends one component with another; extensions areapplied from right to left. Finally, the new operator closes an open component; using OOP
terminology, this operator instantiates an object p of the class a1 ⊕ a2 ⊕ ... ⊕ an ⊕ base.
The arrows in the diagram show what happens to the references during composition. The⊕ operator instantiates the super reference of the extending component with the extended
component. In contrast, the new operator instantiates the self-reference (this) of the basecomponent to the entire composition.
The basis of the implementation is shown in Figure 1. The type Open s is a synonym
for a function of type s → s representing an open component of type s. The parameter s ofthis function is the self-reference and the return value is the resulting closed module. The
inheritance operator ⊕ defines component composition. Composition is associative, and it
has the zero component as left and right unit, forming a monoid.2
f ⊕ zero ≡ f ≡ zero ⊕ f(f ⊕ g) ⊕ h ≡ f ⊕ (g ⊕ h)
The function new is a fixpoint combinator used for closing, or instantiating, an open andpotentially extended component.
There are several other models of inheritance. Cook (1989) explores many other variants.
We believe that similar results to those in this paper can be obtained for these other models.
We adopt the model of inheritance in Figure 1 because it is simple yet expressive enoughto tackle the reasoning issues at the heart of this paper. In this model, which is polymorphic
2

Open s is the monoid of endofunctions with identity and function composition; ≡ means
denotational equivalence throughout the article.

ZU064-05-FPR

paper

6

22 August 2012

14:18

B. Oliveira, T. Schrijvers and W. Cookin the type s of open modules, we can capture the simplest form of open modules that isstill interesting: single-argument functions.
Example The open (single-argument) function fib1 defines the standard Fibonacci function, except that recursive calls are replaced by this.
fib1 :: Open (Int → Int)
fib1 this n = case n of 0 → 0
1→1→ this (n − 1) + this (n − 2)
The open function optfib optimizes two calls of the Fibonacci function by returning theappropriate values immediately. Note that optfib is not meant to be used standalone. It
assumes that it is used in combination with an open function like fib1 that takes care of theuncovered cases.
optfib :: Open (Int → Int)
optfib super n = case n of 10 → 55
30 → 832040→ super n
Different combinations of open functions are closed with new:slowfib1 , fastfib1 :: Int → Int
slowfib1 = new fib1
fastfib1 = new (optfib ⊕ fib1 )The functions slowfib1 and fastfib1 illustrate that MRI unifies the concept of extensions andbase programs under a single type. There is still a conceptual difference between them,because in a base program this is understood as a recursive call, while in the mixin superrefers to the original computation that is extended by that mixin. Instantiating extensions
alone will typically result in a useless program, as it has no base case.
In the Haskell approach presented in this section, the super argument for extensions or
this for base programs is always explicitly passed. However, it is possible to make them
implicit using implicit parameters (Lewis et al., 2000).

2.2 Monads and Monad Transformers
Monads are a standard technique for encapsulating computational effects in pure functional
languages (Wadler, 1992a). Examples of computational effects include mutable state, error
handling, and non-determinism. Monads allow explicit representation of computations,which produce values of a given type and may perform side effects. Computations arecomposed by a bind operator that hides the details of the computation effect (passing
explicit state, handling errors, etc.). In Haskell, monads are described by a type class:class Monad m wherereturn :: a → m a(>>=) :: m a → (a → m b) → m b

ZU064-05-FPR

paper

22 August 2012

14:18

MRI: Modular Reasoning about Interference in Incremental Programming-- Identity
runI :: I arunIT :: IT m a

7

→a
→a

-- State
runS :: S s a→ s → (a, s)evalS :: S s a→s→arunST :: ST s m a → s → m (a, s)class Monad m ⇒ SM s m | m → s where
get :: m s
put :: s → m ()-- Writer
runW :: W w a→ (a, w)
evalW :: W w a→aexecW :: W w a→w
runWT :: WT w m a → m (a, w)
evalWT :: WT w a → a
execWT :: WT w a → w
class (Monoid w, Monad m) ⇒ WM w m | m → w wheretell :: w → m ()-- Reader
runR :: R e a→e→arunRT :: RT e m a → e → m aclass Monad m ⇒ RM e m | m → e where
ask :: m e-- Error
runE :: Error e a → Either e a
runET :: ET e m a → m (Either e a)class Monad m ⇒ EM e m | m → e where
throwError :: e → m acatchError :: m a → (e → m a) → m a
Fig. 2. Monads and monad transformer types.

The type m a describes computations of type m which produce values of type a when
executed. The function return lifts a value of type a into a (pure) computation that simply
produces the value. The bind function >>= composes a computation m a, which produces
values of type a, with a function that accepts a value of type a and returns a computationof type b. The convenient funtion >> defines a special case of bind where the intermediate
value is not used:(>>) :: Monad m ⇒ m a → m b → m b
ma >> mb = ma >>= \ → mb
All instances of Monad must satisfy the following laws:

ZU064-05-FPR

paper

8

22 August 2012

14:18

B. Oliveira, T. Schrijvers and W. Cook
Definition 1 (M ONAD L AWS)
return x >>= f ≡ f x(R ETURN -B IND )p >>= return ≡ p(B IND -R ETURN )(p >>= f ) >>= g ≡ p >>= λ x → (f x >>= g)(B IND -B IND )The Haskell do notation is syntactic sugar for the bind operator: do {x ← f ; g} meansf >>= λ x → g.
A monad transformer (Liang et al., 1995) is a higher-order monad that is parameterized
by another monad. Monad transformers are needed because monads do not compose wellon their own. With monad transformers, different kinds of monads can be layered on topof each other to compose the functionality provided by each monad. A monad transformer
is defined by the following type class:class MonadTrans t where
lift :: Monad m ⇒ m a → t m a
The lift operation takes a monadic computation m a, and lifts it into the transformed monadt m. For each particular type of effect (such as state or exceptions) there is an associatedmonad transformer type and type class. Figure 2 shows a number of monad and monadtransformer (Liang et al., 1995) definitions that are used throughout the paper. Note thatclasses such as SM s m use functional dependencies (Jones, 2000). The annotation m → sstates that there is a functional dependency between the type m and s (the type m determines
the type s). This additional information is used by the compiler to improve type-inference.
2.3 Monadic Mixins
The combination of mixins and monads is the key to provide a purely functional modelof IP with effects. For practical applications, pure mixins are of limited use. For instance,
most well-known examples of AOP advice, including logging, tracing, backups, and memoization, are effectful. A setting without effects is severely limited. Take the example in
Section 2.1. Ideally it should be possible to dynamically construct a lookup table for thecalls of the Fibonacci function. However, without effects, the best we can do is to build ina static lookup table for some of the calls. Effectful mixins are useful to provide a better
solution for this problem, allowing the creation of a dynamic memo table where previously
computed calls can be looked up.
A simple effectful memoization mixin is presented in Figure 3. The SM class, whichmodels state, is used by the memo mixin to read and update the cached values in the memo
table. The memo table is implemented using a (finite) map from integers to integers. If the
input value to the function exists in the memo table, then the associated value is returned.
Otherwise, the call proceeds and the memo table is updated with the input value and theresult of the call.
The introduction of effects requires a change to the Fibonacci component: it too must
be written in a monadic manner, though it is fully parametric in the monad type. We caninstantiate different monads, using the corresponding run functions in Figure 2, to recover

ZU064-05-FPR

paper

22 August 2012

14:18

MRI: Modular Reasoning about Interference in Incremental Programming

9

memo :: SM (Map Int Int) m ⇒ Open (Int → m Int)
memo super x = do m ← get
if member x m then return (m ! x)else do y ← super x
m0 ← getput (insert x y m0 )return yfib2 :: Monad m ⇒ Open (Int → m Int)fib2 this n = case n of 0 → return 0
1 → return 1→ do y ← this (n − 1)x ← this (n − 2)
return (x + y)
Fig. 3. Memoization

data Expr= Lit Int
| Var String| Plus Expr Expr
| Assign String Expr
| Sequence [Expr ]| While Expr Expr
type Env = [(String, Int)]
Fig. 4. Types for a simple imperative language.

variations of the Fibonacci function. For example, the identity monad I recovers the effectfree function
slowfib2 :: Int → Int
slowfib2 = runI ◦ new fib2
while a fast Fibonacci function is obtained by adding the memo mixin and suitably instantiating the state monad:
evalS :: S s a → s → aevalS m s = fst $ runS m s
fastfib :: Int → Int
fastfib n = evalS (new (memo ⊕ fib2 ) n) empty

2.4 Application: Orthogonal Aspects of Interpreters
In this section we show how monadic mixins can capture various orthogonal aspects ofinterpreters (and, more generally, programs) like logging or improved error handling.
Figure 4 shows the datatype for the abstract syntax of a simple imperative language. In
Figure 5 the interpreter for that language is presented. The interpreter’s type Open (Expr →m Int) indicates that it is an open function of type Expr → m Int. The type variable m

ZU064-05-FPR

paper

10

22 August 2012

14:18

B. Oliveira, T. Schrijvers and W. Cookbeval :: SM Env m ⇒ Open (Expr → m Int)beval this exp = case exp ofLit x→ return x
Var s→ do e ← getcase lookup s e ofJust x → return x→ error msg
Plus l r→ do x ← this ly ← this r
return (x + y)
Assign x r→ do y ← this re ← getput ((x, y) : e)return y
Sequence [ ]→ return 0
Sequence [x]→ this x
Sequence (x : xs) → this x >> this (Sequence xs)
While c b
→ do x ← this c
if (x ≡ 0) then return 0else (this b >> this exp)
where msg = "Variable not found!"Fig. 5. A mixin-based monadic evaluator.

means that mixins may introduce effects. However, the constraint on m is not Monad m,
for an unknown type of effect, but SM Env m: the effect must involve an updateable state oftype Env, the environment used by the interpreter. In other words, the interpreter itself is
effectful. In dealing with the Var and Assign cases it reads and writes the environment withthe get and put functions.
A basic unadvised monadic evaluator is recovered as follows:
eval :: Expr → S Env Int
eval = new beval
The self-reference in the open function is closed, and m is instantiated to the state monad.
Figure 6 shows how to define various mixins that capture aspects which are orthogonal
to the base computations. These mixins are described next.
Logging mixin This mixin defines logging modularly. It writes a log message when entering the function call, delegates to super and finally writes another log message when
exiting. It uses the writer monad WM of Figure 2 for writing logging messages.
Dumping mixin This mixin shows how to modularly dump the environment at each
evaluation step, which is useful for debugging. The mixin intercepts the evaluation of
every expression, retrieves the current environment, writes it out using a writer monadand delegates the actual evaluation to super. This example is interesting because it showsthat the mixin not only introduces its own writer effect WM , but also relies on the presenceof the state effect SM .

ZU064-05-FPR

paper

22 August 2012

14:18

MRI: Modular Reasoning about Interference in Incremental Programming

11-- the logging mixinlog :: (WM String m, Show a, Show b) ⇒ String → Open (a → m b)
log name super x = dotell ("Entering " ++ name ++ "with" ++ show x ++ "\n")y ← super x
tell ("Exiting " ++ name ++ "with" ++ show y ++ "\n")return y-- the environment dumping mixin
dump :: (SM s m, WM String m, Show s) ⇒ Open (a → m b)
dump super arg = do s ← gettell (show s ++ "\n")super arg-- the exception handling mixin
type Exc = (String, Expr, Env)
eeval :: (SM Env m, EM Exc m) ⇒ Open (Expr → m Int)eeval super exp = case exp of
Var s → do e ← getcase lookup s e ofJust x → return x→ throwError (msg, exp, e)→ super exp
where msg = "Variable not found!"Fig. 6. Logging, environment dumping and exception handling mixins.

Exception handling mixin A last example of a useful mixin is a better error handlingfacility for the interpreter. In the interpreter, an error can occur when a variable is looked
up in the environment. The exception handling mixin overrides the case for variables andreplaces the error primitive by throwError (see Figure 2). There are two advantages ofusing throwError instead of error. The first advantage is that additional useful information
can be returned together with the exception (with error it is only possible to provide astring error message). For example, it may be useful to return the current environment, orthe expression where the error has occurred so that the user can more easily identify the
locale in the program that is to blame. The second advantage is that the exception is now
explicit in the type of the evaluator, and the client code must handle the exception, which
ensures that the main program remains in a usable state. As in the dumping mixin, twodifferent types of monads are involved: state SM and error EM .
Weaving in functionality The different mixins can be combined in various ways, bringing
together different effects or shared uses of the same effect:debug1 , debug2 :: (WM String m, SM Env m) ⇒ Expr → m Int
debug1 = new (log "eval" ⊕ beval)debug2 = new (log "eval" ⊕ dump ⊕ beval)exc :: (EM Exc m, WM String m, SM Env m) ⇒ Expr → m Int
exc = new (eeval ⊕ log "eval" ⊕ beval)

ZU064-05-FPR

paper

12

22 August 2012

14:18

B. Oliveira, T. Schrijvers and W. Cook

The debug1 program adds logging of function calls to the evaluator, while debug2 is moreverbose and also dumps the environment at each call. Finally, the third program logs calls
and may throw an exception if a variable that does not exist in the environment is used.
These programs can be run by picking suitable monads and extracting the relevant
information. For example, in the programs shown next, the log string is returned (except if
an error occurs).
test1 e = evalS (execWT (debug1 e)) [ ]test2 e = evalS (execWT (debug2 e)) [ ]test3 e = extract (evalST (execWT (exc e)) [ ])whereextract (Left (msg, exp, )) = "Error: " ++ msg ++"\nIn Expression: " ++ show exp
extract (Right t)=tWhile the first two programs may silently give an error if a variable is not in the environment, the last program has to handle the exception explicitly, and it can report an error
message with the faulty expression.
3 Interference and Equational Reasoning
In IP it is often the intent of the programmer that inheritance extends or augments but does
not modify the behavior of a base component. This property is called non-interference.
The opposite, interference, means that inheritance causes the components to interact in a
way that essentially changes the behavior of the base component. Knowing whether two
components interfere directly contributes to programmer understanding: If components do
not interfere, then they can be understood individually. If the components do interfere,
then the programmer should more carefully investigate what the impact of interference
is. Moreover, in many applications, the programmer intends to implement non-interfering
inheritance; interference is then a programming error. Either way, the programmer’s understanding (or confidence in his understanding) is greatly improved when he can establish
whether two components do or do not interfere.
3.1 Equational Reasoning about Interference
As a formal model of inheritance, MRI does allow us to reason formally about (non-)interference. This does not require special-purpose mechanisms such as Aldrich’s logicalequivalence laws (Aldrich, 2005). Instead, Haskell’s equational reasoning allows us toestablish non-interference from the equality of two expressions. Furthermore, the use of
simple equational reasoning steps allows us to mechanize such non-interference proofs intheorem provers like Coq. The proofs for the two theorems presented in this section havebeen formalized in Coq and are available at http://users.ugent.be/~tschrijv/MRI.
To formally reason about non-interference, we must first be able to formally capture thisoften quite informal notion. MRI allows us to do so. For instance, we may want to express
that the logging log component does not interfere with the fib2 component. In the spirit ofequational reasoning, we capture this informal statement in a formal equality:

ZU064-05-FPR

paper

22 August 2012

14:18

MRI: Modular Reasoning about Interference in Incremental Programming

13

Theorem 1 (L OGGING N ON -I NTERFERENCE)
For all n > 0, we have that
evalW (logfib n) ≡ runI (slowfib2 n)
where we use the following definition of logfib, slightly simplified for the sake ofbrevity:logfib = new (log ⊕ fib2 )
where
log :: WM String m ⇒ Open (Int → m Int)log super n = do tell "entering fib"super nThis theorem relates the composition of log and fib2 to fib2 by itself. On the right-handside, we have the pure Fibonacci function. On the left-hand side, we ignore the side-effectsof the logging mixin with the help of evalW :: W a → a, which projects a computation in
the W monad on its return value.
Proof
The proof of this formal statement with equational reasoning proceeds by induction. The
two base cases, 0 and 1, are trivial: evaluate the left- and right-hand sides and observe thatthey are equal. The inductive case is more interesting.
evalW (logfib (n + 2))≡ {-unfold logfib and fix -}evalW (log ◦ fib2 ◦ logfib (n + 2))≡ {-unfold log -}evalW (do tell "entering fib."
fib2 logfib (n + 2))≡ {-unfold fib2 & reduce case -}evalW (do tell "entering fib"f1 ← logfib (n + 1)
f2 ← logfib nreturn (f1 + f2 ))≡ {-unfold return -}evalW (do tell "entering fib"f1 ← logfib (n + 1)
f2 ← logfib n
W (f1 + f2 , ""))
≡ {-unfold >>= -}evalW (do tell "entering fib"f1 ← logfib (n + 1)
W (evalW (W (f1 + evalW (logfib n), ""))
, execW (logfib n) ++execW (W (f1 + evalW (logfib n), ""))))

ZU064-05-FPR

paper

14

22 August 2012

14:18

B. Oliveira, T. Schrijvers and W. Cook
≡ {-(1) evalW (W (x, y)) ≡ x and (2) execW (W (x, y)) ≡ y -}evalW (do tell "entering fib"f1 ← logfib (n + 1)
W (f1 + evalW (logfib n), execW (logfib n) ++ ""))
≡ {-(3) l ++ "" ≡ l -}evalW (do tell "entering fib"f1 ← logfib (n + 1)
W (f1 + evalW (logfib n), execW (logfib n)))≡ {-unfold >>= -}evalW (do tell "entering fib"W (evalW (W (evalW (logfib (n + 1)) + evalW (logfib n), execW (logfib n))), execW (logfib (n + 1)) ++execW (W (evalW (logfib (n + 1)) + evalW (logfib n), execW (logfib n)))))≡ {-evalW (W (x, y)) ≡ x and execW (W (x, y)) ≡ y -}evalW (do tell "entering fib"W (evalW (logfib (n + 1)) + evalW (logfib n), execW (logfib (n + 1)) ++ execW (logfib n)))≡ {-unfold >>= -}evalW (W (evalW (W (evalW (logfib (n + 1)) + evalW (logfib n), execW (logfib (n + 1)) ++ execW (logfib n))), execW (tell "entering fib.") ++execW (W (evalW (logfib (n + 1)) + evalW (logfib n), execW (logfib (n + 1)) ++ execW (logfib n)))))≡ {-evalW (W (x, y)) ≡ x -}evalW (logfib (n + 1)) + evalW (logfib n)≡ {-induction hypotheses -}runI (slowfib2 (n + 1)) + runI (slowfib2 n)≡ {-(4) runI (slowfib2 (n + 1)) + runI (slowfib2 n) ≡ runI (slowfib2 (n + 2) -}runI (slowfib2 (n + 2))

This proof fairly straightforwardly unfolds the monadic operations >>= and return, andsimplifies intermediate computations with a few well-chosen auxiliary lemmas (1)–(4).
These lemmas can also be proven with equational reasoning.
Some proofs are more complex than others. Take for instance a proof for the statementthat the memoized and non-memoized variants of the Fibonacci function are equivalent:
Theorem 2 (N ON -I NTERFERENCE OF M EMOIZATION)
slowfib2 ≡ fastfib2

ZU064-05-FPR

paper

22 August 2012

14:18

MRI: Modular Reasoning about Interference in Incremental Programming

15

The proof of this theorem is more complex as it mutually depends on an invariant of thememo table t that we must also show to be preserved by fastfib2 :∀n. lookup n t ‘mplus‘ Just (slowfib2 n) ≡ Just (slowfib2 n)
which expresses that, if the table t contains an entry for n, this entry equals slowfib2 n. When
proofs become more intricate like this, it is useful to turn to a proof assistant, like Coq or
Isabelle, that directly supports proving statements about purely functional programs. These
assistants add formal rigor to the process, and bolster our confidence in the validity of theproof we write.

4 Functional Programming Tools for Modular Reasoning
The equational reasoning approach followed in the previous section has three obvious
disadvantages that stem from the non-modularity of the reasoning approach:
Whole Program Knowledge The approach is a non-modular whole-program approach.
The proof involves the definitions of all three parts of the program: that of the basecomponent, the mixin and the monad.
Hence, the approach does not work in the case one of the component’s implementations
is not available. Moreover, if the implementations are available, it requires sufficientfamiliarity of the programmer who writes the proof.
Non-Trivial Activity Even though the proofs are fairly straightforward for simple situations like the logging example, they are rather longwinded and do require an effort fromthe programmer. Moreover, not all programers are familiar with a theorem proving tool
like Coq, and, even if they are, its use does complicate the program development process.
Limited Proof Scope At the same time the gain is limited. For example, we establishthat the logging mixin does not interfere with the Fibonacci component, but we cannot
conclude anything about how it interferes with other base components. That requires
additional proofs, one for each base component that we want to pair it with.
As we shall see in Section 5 it is possible to state very general harmless mixin theorems
that only require the definition of the mixin. With those theorems we can avoid tiresome
proofs like that of logfib entirely.
This section shows a number of useful reasoning tools that make such general harmlessmixins theorems possible:• Effectful Reasoning: we can avoid having to know the definitions of monadic operations by looking only at the algebraic properties of these operations.
• Parametricity Properties of Effectful Components: we can know which effects acomponent uses just by looking at the type of the component.
• Interference Combinators: we can enforce various control and data flow patterns
using combinators.
The remainder of this section discusses each of these in more detail.

ZU064-05-FPR

paper

22 August 2012

14:18

16

B. Oliveira, T. Schrijvers and W. Cook
4.1 Effectful Reasoning

Effectful reasoning relies only on the algebraic properties of effectful operations to reason
about programs. This avoids the use of concrete monad definitions for monadic operations
like >>=, return, get or put; and breaking the abstraction provided by the general monadinterface. Moreover, effectful reasoning has the advantage that it is possible to reason
about polymorphically typed programs, where the monad type is only constrained andnot instantiated to a monomorphic type. For example, consider the program:tick = get >>= put ◦ (+1)
The most general type for tick (and the type that Haskell infers) is:tick :: SM Int m ⇒ m ()This type nicely abstracts from any concrete state monad implementation. All that weneed to know to type-check this program is that whatever instantiation of m we pick, thisinstantiation supports the stateful operations get and put (which are members of the SMclass). Possible instantiations of m are, for example:
type M1 = S Int ()type M2 = ST Int (R String) ()type M3 = RT String (S Int) ()We want to reason about tick in a way that is valid for all possible instantiations of m.
This is ultimately crucial for dealing with polymorphic monadic components as the ones
discussed in this paper. For this purpose we already have presented algebraic properties forthe operations >>= and return, known as the monad laws, in Section 2.2; these are valid
for any instantiation of the monad m. What is still missing are the algebraic properties forthe state-specific monadic operations get and put.
Algebraic Properties for Stateful Effects Five laws govern the semantics of the get andput methods:
Definition 2 (S TATE L AWS)
get >> m ≡ m(G ET-Q UERY)

get >>= λ s → get >>= f s ≡ get >>= λ s → f s s(G ET-G ET)

put x >> put y ≡ put y(P UT-P UT)

put x >> get ≡ put x >> return x(P UT-G ET)

get >>= put ≡ return ()(G ET-P UT)Informally, the (G ET-Q UERY ) law expresses that a get whose result is not used has no
impact at all. The (G ET-G ET ) law states that successive get operations return the samevalue, while (P UT-P UT ) captures that successive put operations overwrite one another.
Finally, (P UT-G ET ) says that get returns the value just written by put, and (G ET-P UT )states that writing the value just read has no impact.

ZU064-05-FPR

paper

22 August 2012

14:18

MRI: Modular Reasoning about Interference in Incremental Programming

17

These five laws state the properties that each implementation of SM should conform to.
Provided with these five laws and the three monads laws, it becomes possible to reason
about polymorphic monadic programs like tick.
We illustrate this by following up on an example of Gibbons and Hinze (2011), whoshow, for all implementations of tick where m is any monad (not necessarily a state monad)
and only using the monad laws, that
Theorem 3 (H ANOI T ICKS)
hanoi n ≡ rep (2 ∗ n − 1) tickwhere hanoi and rep are defined as:
hanoi 0= return ()hanoi (n + 1) = hanoi n >> tick >> hanoi n
rep 0
mx = return ()rep (n + 1) mx = mx >> rep n mx
In words, the theorem states that hanoi n is equivalent to 2 ∗ n − 1 successive ticks.
By exploiting the monad state laws above, and the details of our tick implementation, but
not the particular monad state implementation, we can show a more interesting equation,that actually allows us to optimize the program.
Theorem 4 (T ICK F USION)
rep n tick ≡ get >>= put ◦ (+n)
In words, this theorem expresses that n successive ticks are equivalent to adding in asingle step n to the state.
Proof
The proof proceeds by induction on n. For n ≡ 0 we have,
rep 0 (get >>= put ◦ (+1))≡ {-unfold rep 0 -}return ()≡ {-G ET-P UT law -}get >>= put≡ {-id is neutral element of function composition -}get >>= put ◦ id
≡ {-0 is neutral element of addition -}get >>= put ◦ (+0)
and for n + 1, we have:rep (n + 1) (get >>= put ◦ (+1))≡ {-unfold rep -}ZU064-05-FPR

paper

18

22 August 2012

14:18

B. Oliveira, T. Schrijvers and W. Cookget >>= put ◦ (+1) >> rep n (get >>= put ◦ (+1))≡ {-induction hypothesis -}get >>= λ x → put (x + 1) >> get >>= λ y → put (y + n)
≡ {-P UT-G ET law -}get >>= λ x → put (x + 1) >> return (x + 1) >>= λ y → put (y + n)
≡ {-R ETURN -B IND law -}get >>= λ x → put (x + 1) >> put (x + 1 + n)
≡ {-P UT-P UT law -}get >>= λ x → put (x + 1 + n)
≡ {-associativity and commutativity of + and fold (.) -}get >>= put ◦ (n + 1)

Algebraic Properties for Other Types of Effects Other types of effects like exceptions,non-determinism, or the reader and writer monads also have similar laws that can be
exploited when reasoning about effects. Liang et al. (1996) showed laws for the reader
monad. More recently, since the publication of the conference version of our paper (Oliveira
et al., 2010) (where 4 of the above 5 algebraic properties for stateful effects were introduced), Gibbons and Hinze (2011) have explored and significantly extended the frameworkof algebraic properties for monadic effects. We refer to their work for the laws about othertypes of effects.

4.2 Type-based Reasoning: Parametricity
By making effects explicit in the types, we can learn a lot about possible effect interactions
by just looking at the types. For example, just by analyzing types it is possible to discoverthat a component is pure (that is it does not use any side-effects) or that it is an impurecomponent that uses some specific type of effects.
Pure Components We say that a monadic component with a type of the formp :: Monad m ⇒ Open (a → m b)
is pure because no effects can be produced by a component of this type. Voigtländer (2009)
explains that this follows from the type in a language with strong parametricity properties
like Haskell. The explicit effect m is a type variable only constrained to be a monadand, consequently it cannot produce any effects of its own, because it is unaware of theparticular effects used. Although mixin purity comes essentially for free in Haskell, inother languages it is much harder to enforce, and it often requires sophisticated program
analysis (Salcianu & Rinard, 2005). While purity imposes severe limitations on mixin code,
it is also easiest to see that this code will not interact through effects at all.
Following Voigtländer’s parametricity approach (see Appendix A for a summary), we
can derive free formal theorems from pure components. One such theorem is that:

ZU064-05-FPR

paper

22 August 2012

14:18

MRI: Modular Reasoning about Interference in Incremental Programming

19

Theorem 5 (P URE C OMPONENT)
new p ≡ return ◦ runI ◦ new p
which is a formal way of saying that p does not produce any effects itself. The proof follows
directly from Voigtländer’s proof (Voigtländer, 2009).
An example of a pure monadic component is fib2 (Figure 3).
Impure Components We say that a monadic component with a type of the formp :: SM s m ⇒ Open (a → m b)
is impure because the monad m allows a particular kind of effects to be used in the component p. In this case, p is a computation that (potentially) reads and writes a state oftype s, and consequently can perform some effects.We should remark that, although forthis particular example we used state, the assumption of any other kind of effect (likeexceptions, non-determinism or continuations) would make the mixin equally impure forsimilar reasons.
Based on parametricity, we can derive free theorems for impure components too. For
instance,
Theorem 6 (S TATEFUL C OMPONENT)

new p x≡do s0 ← getlet (r, s1 ) = runS (new p x) s0
put s1
return r

expresses the intuition that a stateful component new p can be summarized as a purely
functional core that computes a state change and a single get-put sequence on the outside
to effect the update. Appendix B lists the parametricity-based proof of this theorem.
Examples of impure monadic components are log and memo mixins, or the evaluatorpresented in Figure 5.
4.3 Interference Combinators
MRI provides interference combinators to enforce different interference patterns at component composition time. These interference combinators use type-based reasoning andassociate a particular type shape with an interference pattern. Thus, a composition that
does not meet the type shape required by the combinator fails to type-check. Note that no
special purpose extension of the type system is needed for this approach.
Our interference combinators are inspired by Rinard et al.’s (2004) classification system
for interference patterns that can occur between AOP advice and advised programs. Their
classification system partitions interference forms in two major types: direct interference

ZU064-05-FPR

paper

22 August 2012

20

14:18

B. Oliveira, T. Schrijvers and W. Cook

indicates the presence of control flow manipulations, whereas indirect interference indicates the presence of data flow manipulations.
Note that in order to draw formal conclusions from the use of these interference combinators, they must be combined with the other reasoning techniques presented in thissection. Section 5 will do so and make strong formal statements.
4.3.1 Enforcing Control Flow Properties
Direct interference is related to control flow and how the use of super calls can guaranteethat a program satisfies certain properties. Similarly to Rinard et al. classification foradvice, mixins can be classified as:
Combination: A mixin can call super any number of times.
Replacement: There are no calls to super in mixins.
Augmentation: A mixin that calls super exactly once and does not modify the arguments
to super or the value returned by super.
Narrowing: A mixin that calls super at most once and does not modify the arguments tosuper or the value returned by super.
We discuss next the combinators that capture the above interference patterns for mixins.
Combination The existing ⊕ combinator does not enforce any interference properties.
The ⊕ operator already composes a mixin of the general form Open s with the basecomponent.
Replacement The informal requirement for replacement is that no calls are made to super.
This requirement can be captured by the following combinator:
type Replace s = sreplace :: Replace s → Open s
replace rmxn = λ super → rmxn
A replacement mixin has type Replace s, which is the type of a closed component. This
reflects the fact that the replacement mixin is a proper base component by itself. In otherwords the base component’s behavior is replaced (or overridden) entirely, which has theeffect of destroying the usual control flow of the base component.
Augmentation The informal requirement for an augmentation mixin is that super is calledexactly once and with the same argument as the mixin. This behavior is enforced with theaugment combinator
type Augment a b c m = (a → m c, a → b → c → m ())
augment :: Monad m ⇒ Augment a b c m → Open (a → m b)
augment (bef , aft) super a =do {c ← bef a; b ← super a; aft a b c; return b}
This combinator is responsible for calling super itself, rather than delegating this responsibility to the mixin. The augmentation mixin has type Augment a b c m, and it consists

ZU064-05-FPR

paper

22 August 2012

14:18

MRI: Modular Reasoning about Interference in Incremental Programming

21of two components: the first component is called before super and the second is called
afterwards. Both parts can use the input a, but only the after argument has access to theresult b of super. Moreover, the before part can communicate an auxiliary value c to theafter part. For instance, log1 is a logging mixin
log1 :: (WM String m, Show a, Show b) ⇒ String → Augment a b () mlog1 name = (bef , aft) where
bef x = write "Entering " x
aft y = write "Exiting " ywrite a b = tell (a ++ name ++ show b ++ "\n")such that log ≡ augment ◦ log1 .
Combinators similar to the well-known AOP notions of before and after advice, can be
implemented on top of augment for mixins:
before :: Monad m ⇒ (a → m ()) → Open (a → m b)after :: Monad m ⇒ (a → b → m ()) → Open (a → m b)
before bef = augment (λ a → bef a >> return (), λ a b c → return ())
after aft = augment (\ → return (), λ a b c → aft a b)
Our earlier dumping mixin can be written with before:
dump1 :: (SM s m, WM String m, Show s) ⇒ a → m ()dump1 arg = do s ← gettell (show s ++ "\n")Note that dump ≡ before dump1 .
Narrowing This form of mixin calls super at most once. Hence, a runtime choice can bemade between replacement or augmentation:
type Narrow a b c m = (a → m Bool, Augment a b c m, Replace (a → m b))
narrow :: Monad m ⇒ Narrow a b c m → Open (a → m b)
narrow (p, aug, rep) super x =do b ← p x
if b then replace rep super x
else augment aug super x
The runtime choice is made by the predicate of type a → m Bool, based on the input oftype a and monad m.
A typical example of narrowing is memoization. In the case of a repeated call, normal
evaluation is replaced by a table lookup. In case of a new call, normal evaluation is
augmented with tabulation.
memo1 :: (SM (Map a b) m, Ord a) ⇒ Narrow a b () m
memo1 = (p, (bef , aft), rep) wherepx= do {m ← get; return (member x m)}
bef= return ()ZU064-05-FPR

paper

22 August 2012

22

14:18

B. Oliveira, T. Schrijvers and W. Cookaft x rrep x

= do {m ← get; put (insert x r m)}= do {m ← get; return (m ! x)}

This variant of memo makes it clear that super is called at most once.
4.3.2 Enforcing Data Flow Properties
Indirect interference is related to data flow through the possible interaction of shared effects(or data) between mixin and base component. The most common form of shared effects isthat of shared state. Another conventional form of effectful interaction is the throwing andcatching of exceptions. Rinard et al. (2004) consider five different forms of interference
between advice and method (of the base component), specific to state. Similar forms ofinterference occur with mixins:
Orthogonal: The mixin and method access disjoint fields. In this case we say that thescopes are orthogonal.
Independent: Neither the mixin nor the method may write a field that the other may reador write. In this case we say that the scopes are independent.
Observation: The mixin may read one or more fields that the method may write but they
are otherwise independent. In this case we say that the mixin scope observes the method
scope.
Actuation: The mixin may write one or more fields that the method may read but they
are otherwise independent. In this case we say that the advice scope actuates the method
scope.
Interference: The mixin and method may write the same field. In this case we say thatthe two scopes interfere.
MRI generalizes these notions from state to arbitrary effects. Just as for control flow interference, it provides a number of combinators that enforce the form of effect interference.
Interference Primitives Interference arises by bringing together two components, a mixin
and a base component. MRI builds interference combinators from primitive combinatorsfor individual components. These primitives express whether the mixin with effect t knows
the type of effect m of the base component. If it does not know the type, then it cannot
initiate interference. This absence of knowledge is captured by a higher-ranked type (Peyton Jones et al., 2007) and a corresponding conversion function to the plain mixin form:
type NIMixin a b t = ∀m.(Monad m, Monad (t m)) ⇒ Open (a → t m b)
nimixin :: (Monad m, MonadTrans t, Monad (t m)) ⇒ NIMixin a b t → Open (a → t m b)
nimixin mix = mix
The opposite case does not require a new operator, since the plain type Open (a → t m b)
suggests that interference may be possible.
Similarly, for the base component interference may not be initiated with:
type NIBase a b m = ∀t.(MonadTrans t, Monad (t m)) ⇒ Open (a → t m b)nibase :: (Monad m, MonadTrans t, Monad (t m)) ⇒ NIBase a b m → Open (a → t m b)nibase bse = bse

ZU064-05-FPR

paper

22 August 2012

14:18

MRI: Modular Reasoning about Interference in Incremental Programming

23

The types NIMixin and NIBase allow us to separate the effects that can be manipulatedby the mixin from the effects that can be manipulated by the base component. The typesystem guarantees that this is indeed the case.
The type signatures of the mixin log1 and base component beval are not adequate toestablish non-interference. In fact, it is possible to obtain both non-interference and interference, depending on the instantiation of the monad. The non-interference combinators
confront us with this issue: both nimixin (augment (log1 "eval")) and nibase beval are
ill-typed.
Recall that the type signature of log1 "eval" islog1 "eval" :: (WM String m, Show a, Show b) ⇒ Open (a → m b)
while nimixin expects the type∀m0 .(Monad m0 , Monad (t m0 )) ⇒ Open (a → t m0 b)
The problem is that the former type does not cleanly split the monad m into two parts:
the transformer t which is used by the log1 mixin, and the rest m0 underneath which is
exclusively at the disposal of the base component. To respect the non-interference patternand obtain a well-typed instance, we split the type m by instantiating it to WT String m0 .
This happens when we supply the following signature:log2 :: (Show a, Show b) ⇒ NIMixin a b (WT String)
log2 = augment (log1 "eval")
With this signature all the tell operations in log1 are handled by WT and the underlying
monad is not accessed.
The same problem arises in nibase beval, where beval has type
beval :: SM Env m ⇒ Open (Expr → m Int)and nibase expects∀t.(MonadTrans t, Monad (t m0 )) ⇒ Open (a → t m0 b)
Unfortunately, for technical reasons it is not easy to split the monad for a base component.
Instantiating m to t (S Env) does not mean that the get and put operations in beval arenecessarily resolved against the embedded monad S Env. Whether or not this is the casestill depends on the choice of t and hence is ambiguous if we leave t undetermined. This
ambiguity causes the following code to be ill-typed:
beval1 :: NIBase Expr Int (S Env)
beval1 = beval
We can solve this issue by explicitly defining a variant of beval in which the monad is
explicitly split up in two parts, a monad transformer t and an embedded monad m0 . Bymeans of lift this variant resolves its uses of get and put against the embedded monad m0 .
beval00 :: (MonadTrans t, Monad (t m0 ), SM Env m0 ) ⇒ Open (Expr → t m0 Int)beval00 this exp = case exp of
Var s→ do e ← lift getcase lookup s e of

ZU064-05-FPR

paper

22 August 2012

24

14:18

B. Oliveira, T. Schrijvers and W. Cook
Just x → return x
Nothing → error msg
Assign x r → do y ← this re ← lift get
lift (put ((x, y) : e))return y... -- The other cases identical to those in bevalThis definition clearly fits the NIBase pattern. The downside is that we had to rewrite thedefinition of beval. With the help of the monad zipper (Schrijvers & Oliveira, 2011) thisrewriting could have been avoided, but since that approach is rather technical we won’t got
into details here.
Interference Combinators Using the above primitives, MRI defines four primitive interference combinators:():: (MonadTrans t, Monad m, Monad (t m))⇒ NIMixin a b t → NIBase a b m → Open (a → t m b)
mix  bse = nimixin mix ⊕ nibase bse(5) :: (MonadTrans t, Monad m, Monad (t m))⇒ Open (a → t m b) → NIBase a b m → Open (a → t m b)
mix 5 bse = mix ⊕ nibase bse(4):: (MonadTrans t, Monad m, Monad (t m))⇒ NIMixin a b t → Open (a → t m b) → Open (a → t m b)
mix 4 bse = nimixin mix ⊕ bse():: (MonadTrans t, Monad m, Monad (t m))⇒ Open (a → t m b) → Open (a → t m b) → Open (a → t m b)
mix  bse = mix ⊕ bse
Note that, unlike Rinard’s categories, these combinators are not specific for state: they
are parametric in the type of effect. The combinators  and  closely correspond to
Rinard’s interference and orthogonal categories. The 5 and 4 combinators indicate whichof the two components is aware of the other’s effects, which are thus shared between thetwo components.
For instance, the composition log2  beval1 expresses that the logging mixin and themonadic evaluator do not interfere with each other’s effects.
Stateful Effects Rinard et al. (2004) consider more refined forms of stateful interaction,
based on read-only or read&write access to a shared state. MRI distinguishes between suchforms of interaction by imposing appropriate constraints on the monad type variable m.
For this purpose MRI refines SM to cater for different views:
class Monad m ⇒ MGet s m | m → s where
get :: m sclass Monad m ⇒ MPut s m | m → s where
put :: s → m ()

ZU064-05-FPR

paper

22 August 2012

14:18

MRI: Modular Reasoning about Interference in Incremental Programming

25

class (MGet s m, MPut s m) ⇒ SM s m
The constraint MGet s m only allows reading the state s of monad m, while the class
MPut only allows writing it. The new SM s m allows both reading and writing by subclassing both MGet and MPut. The methods get and put obey the laws presented in Section 4.1.
The new classes allow more accurate types, for instance the dumping mixin only requires
reading the state:
dump2 :: (MGet s m, WM String m, Show s) ⇒ a → m ()dump2 = do {s ← get; tell (show s ++ "\n")}With the two new constraints, MRI also defines relaxed versions of NIMixin:
type ROMixin a b t s = ∀m.(MGet s m, Monad (t m)) ⇒ Open (a → t m b)
type WOMixin a b t s = ∀m.(MPut s m, Monad (t m)) ⇒ Open (a → t m b)
Each of these forms of mixin assumes one operation on the underlying monad m, get for
ROMixin and put for WOMixin, and both obviously assume that t m is a monad.
The dump3 mixin instantiates dump2 as a ROMixin:
dump3 :: Show s ⇒ ROMixin a b (WT String) s
dump3 = before dump2
The new interference primitives in turn allow Rinard’s state-specific interference classes tobe expressed as combinators:
observation :: (MGet s m, MonadTrans t, Monad (t m)) ⇒ROMixin a b t s → NIBase a b m → Open (a → t m b)observation mix bse = mix ⊕ bse
actuation :: (MPut s m, MonadTrans t, Monad (t m)) ⇒WOMixin a b t s → NIBase a b m → Open (a → t m b)
actuation mix bse = mix ⊕ bse
MRI puts similar constraints on the base component and distinguishes nine different forms
of interference. The following table connects these nine forms to the corresponding fourterms used by Rinard et al.:Base Component
MGet

MPut

SM

MGet

Independent

Observation

Observation

MPut

Actuation

Interference

InterferenceSM

Actuation

Interference

Interference

Mixin

By distinguishing between SM and MPut, MRI has a more fine-grained classification.
MPut × MPut, for instance, is only a weak form of interference. While both components
write to the same state, neither’s computations are affected; only the resulting state is.

ZU064-05-FPR

paper

26

22 August 2012

14:18

B. Oliveira, T. Schrijvers and W. Cook

While Rinard’s classification is specific for state, MRI allows similar classifications
for other kinds of effects. For example, with exceptions the rights to throw and catch
exceptions are separated into different monad subclasses: MonadThrow e m for throwing
an exception e, MonadCatch e m for catching, and EM e m for both. By considering thepermitted operations of the mixin and base component, the possible interference patterns
between them are established.

5 Harmless Mixins: Strong Guarantees of Non-InterferenceThis section explains how to enforce strong guarantees of non-interference for mixins
with direct and indirect non-interference combinators. These strong guarantees of noninterference are inspired by Dantas and Walker (2006) notion of harmless advice:
A piece of harmless advice is a computation that, like ordinary aspect-oriented
advice, executes when control reaches a designated control-flow point. However,unlike ordinary advice, harmless advice is designed to obey a weak noninterference property. Harmless advice may change the termination behavior ofcomputations and use I/O, but it does not otherwise influence the final result of
the mainline code.

5.1 Harmless Mixins
The harmless composition combinator  ensures both control and data flow properties.
type NIAugment a b c t = ∀m.(Monad m, Monad (t m)) ⇒ Augment a b c (t m)() :: (Monad m, MonadTrans t, Monad (t m)) ⇒NIAugment a b c t → NIBase a b m → Open (a → t m b)
mix  bse = augment mix  bse
Harmless composition requires a special type of non-interfering augmentation mixin, which
is defined by NIAugment. It is important that the mixin used by  is augmentation since,
for instance, if an effectful base component could be called twice by the mixin, it could
give different results than if called only once. This is because the result may depend on theeffects of the base component. The  combinator used by  ensures that the mixin and thebase component have non-interfering effects.
The full non-interference provided by the  combinator enforces that the mixin isharmless. Let us cast the informal notion in a formal theorem:

ZU064-05-FPR

paper

22 August 2012

14:18

MRI: Modular Reasoning about Interference in Incremental Programming

27

Theorem 7 (H ARMLESS M IXIN)
Consider a base component bse and mixin mix with the types:
bse :: ∀t.(MonadTrans t, Monad (t m1 )) ⇒ Open (a → t m1 b)
mix :: ∀m.(Monad m, Monad (t1 m)) ⇒ Augment a b c (t1 m)
where a, b, c, m1 and t1 are arbitrary given types with m1 a monad and t1 a monadtransformer. Then mixin mix is harmless with respect to bse:π ◦ (new (mix  bse)) ≡ runIT ◦ (new bse)
for any projection function π :: ∀m a.Monad m ⇒ t1 m a → m a that satisfies the law:π ◦ lift ≡ id

(P ROJECT-L IFT)

Informally, the theorem states that, if we ignore the effects introduced by the mixin, theadvised program is equivalent to the unadvised program. The role of the projection function
π is to ignore the effects introduced by the mixin. The P ROJECT-L IFT law expresses theintuition that projection has no impact if there are no effects.
Proof The proof essentially combines the three important reasoning principles: 1) equational reasoning over the combinator definitions, 2) algebraic reasoning with the monadlaws and the P ROJECT-L IFT law, and 3) parametricity of the mixin and base component
types. Here we sketch the three high-level steps of the proof; Appendix C provides the fulldetails:
1. First, we show how to convert between the self-explanatory form of augmentation
mixin we have used so far and the more dense form a → t m (b → t m c) that isconvenient for writing proofs. The connection between the two forms is captured by
the convert function, which translates from the former to the latter.
convert :: (Monad m, MonadTrans t, Monad (t m))⇒ (a → t m c, a → b → c → t m ())→ (a → t m (b → t m ()))
convert (bef , aft) =λ a → bef a >>= (λ c → return (λ b → aft a b c))
The counterpart of the augment function isaround :: (Monad m, MonadTrans t, Monad (t m))⇒ (a → t m (b → t m ()))
→ Open (a → t m b)
around mix = λ super →λ a → mix a >>= λ aft →super a >>= λ r →aft r>>= \ →
return r

ZU064-05-FPR

paper

28

22 August 2012

14:18

B. Oliveira, T. Schrijvers and W. Cook
Lemma 1
Consider augmentation mixin (bef , aft) :: (a → t1 m1 c, a → b → c → t1 m1 ()),
then we have that:augment (bef , aft) ≡ around (convert (bef , aft))where m1 is a Monad and t1 is a MonadTrans.
The proof of this lemma is based on equational reasoning and the monad laws.
2. Then, exploiting parametricity, we derive two free theorems, one for the aroundmixin:3
Lemma 2
Consider a function f :: ∀m.Monad m ⇒ a → m (b → m c), then we have that:fm1 ≡ (out (return ◦ out (return ◦ runI) ◦ runI)) fI
and one for the base component:
Lemma 3
Consider a function f ::∀t.MonadTrans t ⇒ (a → t m1 (b → t m1 ())) → a → t m1 b
with m1 an arbitrary monad, then we have that:out π ◦ f ≡out runIT ◦ f ◦ out (IT ◦ fmap (out (IT ◦ π)) ◦ π)
for any π :: ∀m, a.Monad m ⇒ t1 m a → m a, with t1 an arbitrary monadtransformer, that satisfies the P ROJECT-L IFT law.
While parametricity is the core technique for proving these two theorems, the necessary logical relations are established by means of equational reasoning, the P ROJECTL IFT law and the monad laws.
Note that parametricity in its simplest form only holds for total, i.e. fully defined andterminating, programs. If partial and non-terminating programs are also allowed, themixin may introduce non-termination and partiality. This is our counterpart of “maychange the termination behavior” in Dantas’s and Walker’s definition.
3. Finally, we prove the main theorem in a big equational reasoning proof. This proof
relates the left-hand side to the right-hand side of the theorem’s equality in a numberof successive equality-preserving steps. These steps involve folding and unfolding
combinator definitions, the three lemmas above, the monad laws, the P ROJECT-L IFT
law, and simple β - and η reductions.

3Here, out = (◦) applies a function to the output of another function.

ZU064-05-FPR

paper

22 August 2012

14:18

MRI: Modular Reasoning about Interference in Incremental Programming

29

5.1.1 Harmless Effects
In order to suit the Harmless Mixin theorem, the mixin cannot introduce arbitrary effects.
There must be a suitable projection function for ignoring the effects. Such projection
functions do indeed exist for several state-related monad transformers.
Writer For the WT monad transformer we define the following projection function:
πW :: ∀w m a.(Monad m, Monoid w) ⇒ WT w m a → m a
πW m = runWT m >>= return ◦ fst
It is indeed suitable:
Lemma 4
The function πW is a suitable function for the Harmless Mixin theorem:
πW ◦ lift ≡ id
See Appendix D.1 for the proof.
With the help of πW , the Harmless Mixin theorem establishes that the logging mixin isharmless:
πW ◦ new (log2 "eval"  beval1 ) ≡ runIT ◦ new beval1
State We can also define a suitable projection function for the ST monad transformer:
πS :: ∀s m a.Monad m ⇒ s → ST s m a → m a
πS s0 m = runST m s0 >>= return ◦ fst
Indeed, the required property holds:
Lemma 5
The function πS s0 is a suitable function for the Harmless Mixin theorem:
πS s0 ◦ lift ≡ idfor any s0 .
See Appendix D.2 for the proof.
Other Harmless Effects There are several other harmless effects, such as IT with trivial
projection function runIT , RT and variations on these.

5.1.2 Harmful effects
An interesting aspect of our theorem is that harmless mixins may not introduce arbitraryeffects. Only those effects for which a suitable projection function π exists, may be usedin harmless mixins. Some types of effects can be harmful.

ZU064-05-FPR

paper

30

22 August 2012

14:18

B. Oliveira, T. Schrijvers and W. Cook

Error Consider again the ET e monad transformer of Figure 2. We can only partially define
the projection function:
πE :: ∀e m a.Monad m ⇒ ET e m a → m a
πE m = runET m >>= λ x → case x ofLeft e → ???
Right x → return x
In the case of an error, we cannot produce a value. We could attempt to fix this issue by
parametrizing πE with a default value d:πE :: ∀e m a.Monad m ⇒ a → ET e m a → m a
πE d m = runET m >>= λ x → case x ofLeft e → return dRight x → return x
but now πE d :: ∀e m.Monad m ⇒ ET e m a → m a fixes the type parameter a to the type ofd, which is inappropriate.
Intuitively, the reason why errors are not a harmless effect is because they can change
the normal control flow of a program if an error (exception) occurs.

I/O Dantas and Walker mention that “Harmless advice may . . . use I/O.” However, undiscriminated use of I/O may definitely interfere with I/O in the base component. In Haskell,
this manifests itself in the fact that there is no safe way to project from the IO monad. Only
more disciplined effects, such as WT , RT and ST are possible.

5.2 Harmless Observation Mixins
In the main Harmless Mixin theorem, we have used the  operator which enforces that the
mixin and base component are orthogonal. While orthogonality is a sufficient condition, it
is certainly not a necessary one. For instance, observation mixins may be harmless too. A
combinator that forces harmless observation mixins is:
type NIOAugment a b c s t = ∀m.(MGet s m, Monad (t m)) ⇒ Augment a b c (t m)() :: (MGet s m, MonadTrans t, MGet s (t m)) ⇒NIOAugment a b c s t → NIBase a b m → Open (a → t m b)
mix  bse = augment mix ‘observation‘ bse
Now we can adapt the theorem accordingly:

ZU064-05-FPR

paper

22 August 2012

14:18

MRI: Modular Reasoning about Interference in Incremental Programming

31

Theorem 8 (H ARMLESS O BSERVATION M IXIN)
Consider a base component bse and mixin mix with the types:
bse :: ∀t.(MonadTrans t, Monad (t m1 )) ⇒ Open (a → t m1 b)
mix :: ∀m.(MGet s m, Monad (t1 m)) ⇒ Augment a b c (t1 m)
where a, b, c, s, m1 and t1 are arbitrary given types with m1 a SM s and t1 a monadtransformer. Then the mixin mix is harmless with respect to bse:π ◦ (new (mix  bse)) ≡ runIT ◦ (new bse)
for any projection function π :: ∀m a.Monad m ⇒ t1 m a → m a that satisfies the
P ROJECT-L IFT law.
Proof The proof is similar in style to that of the Harmless Mixin theorem. The maindifference lies in the fact that the mixin knows more about the m type parameter. As aconsequence, weaker parametricity results are obtained. The core insight is that we canmake up for this loss of parametricity by exploiting the G ET-Q UERY and G ET-G ET laws.
We refer to Appendix E for the proof details.
Example Theorem 8 establishes that the dumping mixin is harmless:πW ◦ new (dump3  beval1 ) ≡ runIT ◦ new beval1
6 Related Work
6.1 Reasoning in Functional Programming
Our work shows how functional programming reasoning techniques can be applied to anotoriously hard problem: modularly reasoning about inheritance in the presence of sideeffects. To address this challenging problem we have had to cast it in the right combinatorbased formulation in which we could bring the synergy of parametricity, equational reasoning and algebraic laws to bear. We next discuss in more detail related work on thesereasoning techniques for purely functional programs.
Equational Reasoning There is a long tradition of reasoning about purely functional
programs. A great benefit of purity is that it allows equational reasoning: that is reasoning
about programs using simple algebraic equations (much like high-school algebra). The
seminal book on “The Algebra of Programming” (Bird & De Moor, 1997) is a highlight ofthis reasoning approach.
Non-modular monadic reasoning However, only recently there has been some intereston exploring such reasoning techniques for monadic programs. Although monads (Wadler,
1992b) are a purely functional way to encapsulate computational-effects, programs using monads are challenging to reason about. The main issue is that monads provide an
abstraction over purely functional models of effects, allowing functional programmers
to write programs in terms of abstract operations like >>=, return, or get and put. One

ZU064-05-FPR

paper

32

22 August 2012

14:18

B. Oliveira, T. Schrijvers and W. Cook

way to reason about monadic programs is to remove the abstraction provided by suchoperations (Hutton & Fulger, 2008). We follow this approach in our reasoning techniquepresented in Section 3. However, as discussed in more detail in Section 4, there are several
drawbacks to this approach. Most importantly this approach is fundamentally non-modular.
Modular monadic reasoning Using parametricity (Reynolds, 1983; Wadler, 1989) andalgebraic laws about effectful operations it is possible to modularly reason about monadic
programs. Voigtländer (2009) has shown how to derive parametricity theorems for type
constructor classes such as Monad. This technique plays a crucial role in our modular
reasoning approach, as it allows us to derive theorems about effectful programs without
knowing the concrete effects used. However, parametricity alone is not enough to establish
theorems such as the Harmless Observation Mixin theorem (see Section 5.2), which allows
mixins to read the state of the base component. To account for this theorem we needalgebraic laws about stateful effects (see Section 4.1). Liang et al. (1996) presented laws forreader monads. In the conference version of this paper (Oliveira et al., 2010) we presented
4 laws about state. Since then, Gibbons and Hinze (2011) presented an additional law forstate (the G ET-P UT law) and have significantly explored algebraic laws for many othertypes of effects.
Non-modular monadic reasoning about FOP In the context of Feature-Oriented Programming (FOP) Prehofer (1999) defines a notion similar to Harmless Mixin, but with
two important differences. Firstly in Prehofer’s monadic model there is no use of open
recursion, which makes it hard to model tightly coupled mixins such as memoization. Secondly, the approach used to reason about harmlessness is quite different. Instead of usingparametricity, Prehofer requires a certain syntactic pattern for his form of Harmless Mixin.
Exploiting this syntactic pattern enables reasoning by induction on operation sequencesand equational reasoning to prove a Harmless Mixin-like theorem. Prehofer’s reasoning
approach is closest to the reasoning techniques presented in Section 3, in the sense that
it is a non-modular approach (requires all the definitions), and it can only be used toreason about individual compositions of mixin and base component. Like our non-modular
reasoning techniques, his approach supports reasoning about harmlessness that is subject
to preconditions and invariants. We believe that given sufficiently polymorphic mixins
it should be possible to use parametricity in Prehofer’s setting to prove that a mixin isconservative regardless of the base component, thus allowing for more modular reasoning
techniques similar to the ones in Section 4.
Prehofer (2006) also considers when the composition of two conservative extensions isconservative: not always, because the form of composition depends in an ad-hoc manner on
the involved mixins. Using our approach, the uniformity of composition seems to suggestthat the composition of two harmless mixins is always harmless, but this needs further
investigation.
6.2 Monads and Modularity
Monad Transformers and Modular Interpreters Liang et al. (1995) proposed Monad
Transformers and Modular Interpreters (MTMI) to show the benefits of monads and monad

ZU064-05-FPR

paper

22 August 2012

14:18

MRI: Modular Reasoning about Interference in Incremental Programming

33

transformers for modularity purposes. With this technique, modular development of components is possible. While our approach is similar in several ways, there are two importantdifferences. The first difference is that Liang et al. focus on modularization of an interpreter’s basic behavior according to the different language features, while we consider themodularization of orthogonal concerns on top of base programs.
The second, and more fundamental, difference between the two works concerns reasoning and abstraction (or encapsulation) properties. We discuss these in more detail next:• Modular Reasoning - Our technique supports modular reasoning and, in particular,
it supports separate compilation. In MTMI, separate compilation is not supported.
In their approach there are three types (Value, Term and InterpM) whose definitions
need to be changed whenever a new component is added. However, these types areused by all modular components and, consequently, a change in one of these types
implies recompilation of all components. This renders modular reasoning about
individual components impossible since the static types may vary depending on
particular instantiations of the components.
• Encapsulation and Interference - The type InterpM denotes the monad that is usedby all the components in MTMI. The different parts of the monad are visible toall components (every component knows the type InterpM), which means that every components can interact with any part of the monad stack. In contrast, in our
approach, parametric polymorphism ensures that a component can only access theparts of the monad stack that it is supposed to. In other words our approach offers
encapsulation of effects while MTMI does not. As a consequence, MTMI cannot
provide non-interference guarantees.
In conclusion, while MTMI supports (to a large extent) modular development of components, it does not support modular reasoning or reasoning about non-interference.
Modularity issues with Monads Transformers There are several modularity issues (andsolutions), related to monad transformers, reported in the literature. In our work we rely on
the monad transformer library (MTL), which is based on Liang et al.’s (1995) work and assuch suffers from these issues.
The most relevant issue for us is that programs that use stacks of monads transformers(usually) have to impose very strong constraints on the orderings of the transformers in thestack. In general, components in a program that uses a monad stack with more than one
monad layer of the same type (for example two state monad layers) have to be aware of thestructure of the monad stack, in order to access the right monad layer. This issue was the
motivation for Schrijvers and Oliveira’s (2011) proposal for the monad zipper and monadviews, which provide an alternative way to manage the monad stack without imposing atight coupling between a monadic component and the structure of the monad stack. In thatwork a variant of the MTL is proposed. Our work could be readily adapted to work withthat variant of the MTL and as such avoid this problem.
Jaskelioff (2008) reports various other issues related to the design of the MTL. Most
pressingly, a deficiency of the MTL design is that when a new type of monad transformer is added, the interacting behavior between the new transformer and the existingtransformers must be defined individually for each case. This is ad-hoc, non-modular andZU064-05-FPR

paper

34

22 August 2012

14:18

B. Oliveira, T. Schrijvers and W. Cookrequires a growing number of instances each time a new monad transformer is added to
the framework. Fortunately this issue is not so pressing for us because we (usually) workwith existing effects (like state, IO or exceptions) and, as such, do not have to add newtransformers to the framework.
Other Effect Models In this article we have focused on the predominant model of effects
in purely functional programming: monads and monad transformers. However, other usefulmodels have been proposed, such as applicative functors (McBride & Paterson, 2008) andarrows (Hughes, 1998), with their own axioms and modularity properties. It makes forinteresting future work to adapt the developments of this article to those alternatives.
6.3 Modular Reasoning and Interference in AOP
In this paper we have focused on inheritance of functions, which is closely related to AOP
advice. Next we discuss work on modular reasoning and interference in the context of AOP.
Modular Reasoning Kiczales and Mezini (2005) argue that modular reasoning aboutcross-cutting aspects is not possible. Instead they propose a global analysis that infers
interfaces of deployed systems. Changing one component may lead to pervasive changes
of interfaces.
In contrast, Aldrich (2005) does define the concept of Open Modules that allows modular
reasoning. However, this approach is severely limited: reasoning of equivalence is limited
to pure base components with respect to impure advice. Reasoning about effectful basecomponents or advice is not covered. Moreover, it is not clear at all what forms of effectare allowed in advice because the advice language is not part of the formal framework.
Translucid contracts (Bagherzadeh et al., 2011) are grey-box specifications which describe control-flow properties required by advice and advised code. Using structural refinement, the specifications are used to enforce the control-flow properties in implementations.
As such translucid contracts allow programmers to understand interactions between advice
and advised code without requiring them to know about implementations. Our control-flow
interference combinators play a similar role to translucid contracts by statically enforcing
control-flow patterns using the type system.
Interference Many authors have identified (non-)interference as an important factor inreasoning about advice.
Dantas and Walker (2006) propose a type-and-effect system for identifying harmless
advice on the MinAML core language (Ligatti et al., 2006): protection domains prevent
information flow from advice to base component. Their modular analysis supports a formal
result similar to our Harmless Observation Mixin theorem. Orthogonal data flow interference cannot be enforced, and it is not clear how non-stateful effects like exceptions fit intheir approach. Because MinAML is impure, effects are needed in addition to types.
Clifton and Leavens (2002) identify that observers (harmless observation mixins) do
not change the specification of the advised module. Later, Clifton et al. (2007) propose
an extension of AspectJ with (optional) annotations for control and heap effects, which
are similar to Rinard et al.’s two forms of interference. A type-and-effect system is used

ZU064-05-FPR

paper

22 August 2012

14:18

MRI: Modular Reasoning about Interference in Incremental Programming35

to modularly verify the annotations. Spectator advice is their counterpart of harmlessobservation mixin, and they prove that it does not modify the base program’s state. No
formal statement is made about the lack of control-flow interference.
Douence et al. (2004) present a formal approach for determining strong independence ofstateful aspects: when aspects commute, they do not interfere with each other. Equational
reasoning laws are used to determine (non-modularly) whether two given aspect implementations commute. However, their language is only partially defined, no equational laws
for effects are provided and no theorem is stated. There are two important differences with
MRI. Firstly, to reason about non-interference, they require the aspect definitions to apply
their equational laws, while MRI only looks at the types of mixins. Secondly, they focus on
aspect/aspect interaction and overlapping pointcuts and do not address aspect/base programinteraction. While this article focuses on the mixin/base component interference, the same
approach applies equally to the interaction of two mixins.
Rinard et al. (2004) formulate a classification scheme for different forms of interference
and combine a number of program analyses for automated classification. No formal results
are proved.
Katz (1993) presents a much earlier classification, for superimpositions in the context of
distributed programming, which he later refines (Katz, 2006). He distinguishes spectative,
regulative invasive superimpositions. Spectative superimpositions are akin to harmlessobservation mixins; regulative superimpositions affect which actions happen, but do notchange the nature of the actions themselves; and invasive superimpositions can change
anything.
In summary, existing approaches to non-interference formulate special-purpose program
analyses or type systems. A major advantage of MRI over all of these is its extremely
light-weight nature. Everything is built on top of existing and familiar language features;no new analysis or type system is required. Moreover, it is possible to reason formallyand modularly about programs using familiar techniques such as equational reasoning andparametricity.
6.4 Modular Reasoning and Interference in OOP
The problems of modular reasoning and interference are closely related and often cometogether hand-in-hand. Because of this, in object-oriented programming the two problems
are usually not clearly distinguished. Normally, when referring to modular reasoning in
OOP, what is meant is the problem of being able to reason about a class in the presenceof subclassing (Stata & Guttag, 1995; Leino, 1998; Ruby & Leavens, 2000; Müller et al.,2003). One problem is that it is often the case that, in order to define a new subclass, either
knowledge about the implementation or some undocumented behavioral assumptions about
the superclass are needed (Kiczales & Lamping, 1992; Lamping, 1993). Additionally, it isoften unclear whether the essential behavior of the superclass is going to be preserved bysubclasses because both data and control flow interference can be introduced.
Following some observations by Lamping (1993) on how methods in classes are related
to each other, Stata and Guttag (1995) proposed to address the problems above using
specifications extended with a notion of groups. Groups capture all methods in a class that
directly manipulate some private field. With Stata and Guttag’s approach a subclass that

ZU064-05-FPR

paper

36

22 August 2012

14:18

B. Oliveira, T. Schrijvers and W. Cookoverrides one method in a group also needs to override all the other methods in the samegroup. Furthermore, the behavior of methods is ensured using traditional specifications that
describe possible class invariants and pre and post conditions of the methods. A similar
approach was proposed by Ruby and Leavens (2000). Their approach consist of an extension of JML with subclassing contracts, for which each method states the protected andpublic fields that it accesses and the method calls required by the method. This approachallows more flexibility when subclassing when compared to the groups proposed by Stataand Guttag, since it is sometimes possible to override a method without overriding all themethods that access the same private fields. Like with Stata and Guttag’s approach ensuringthat the behaviour of methods is preserved is achieved with traditional method specifications. Interestingly, specifications themselves are prone to modular reasoning problems,
which leads to a related line of work aimed at providing modular specification of properties(Leino, 1998; Müller et al., 2003).
The main difference between our work and the existing work on modular reasoning in
OOP is that we focus on providing a generic model for inheritance that supports reasoning
from inception, while most previous work tries to develop specification and reasoning principles a posteriori for existing OOP technologies. Our approach is aimed at understanding
the essential problems that lead to the difficulties in reasoning in existing IP languages;
and fostering the development of new programming languages in which such problems are
addressed from scratch. A difficulty that we have not yet addressed in our model, but which
is highly relevant for OOP, relates to control flow interference. As shown in Section 5, it
is possible to have strong-guarantees of non-interference for functions, but in the caseof objects matters are a bit more complicated because each method can interfere withother methods of the same object. Nevertheless, we do not think this poses a fundamental
difficulty.

6.5 Functional AOP systems
There has been some interest on integrating AOP and functional programming. However,this poses quite different and new challenges compared to integrating AOP in an OO
language, especially if the functional language is pure (Wang & Oliveira, 2009).
Two main approaches to functional AOP exist, both following the pointcut-advice model:
1) statically typed language-based approaches such as Aspectual Caml (Masuhara et al.,2005), AspectFun ((Chen et al., 2011); (Chen et al., 2007)) and AspectML (Dantas et al.,2008), and 2) lightweight dynamically typed approaches like AspectScheme (Dutchyn
et al., 2006). While the statically typed approach has obvious benefits, dynamically typed
languages usually allow more lightweight library-based solutions. This has benefits interms of reusable aspects (De Fraine & Braem, 2007) and expressing dynamically deployedaspects (Tanter, 2008). In some sense, MRI combines the best of both worlds: it is avery lightweight statically typed library-based approach. However, it uses a model of
explicit composition of mixins instead of the pointcut model. In MRI, “features” (such as
first-class, polymorphic and inferable types for mixins) come for free. In language-based
approaches adding support for each of these features is non-trivial, and only AspectML
supports all of them.

ZU064-05-FPR

paper

22 August 2012

14:18

MRI: Modular Reasoning about Interference in Incremental Programming

37

Chen et al. (2011) proposed a monadic semantics for AspectFun. The idea is to have asource language with private, local state for advice. Programs with local state are translated
into monadic programs using a type-directed algorithm. Thus, like our work, monads
model (stateful) effects, however, unlike our work (non-modular) code transformation isused instead of mixins for weaving components. Although the focus of their work is
not modular reasoning, a consequence of only allowing local, private state for advice isthat data-flow interference between advice and other components cannot occur. However
control-flow interference can still happen. This gives them some non-interference guarantees (at the cost of expressiveness), but it is insufficient to automatically establish harmless
advice.

7 Conclusion
MRI promotes the idea that effects should be an integral part of the interface of components, avoiding hidden data flows between components. This has important benefits:• Modular reasoning is possible, since only the implementation of a program and theinterfaces of the components used by that program are needed to understand that
program locally.
• Reasoning about the interference between components is possible by looking at theinterfaces only.
MRI provides a purely functional model of inheritance with effects. The benefit ofbeing purely functional is that many powerful reasoning techniques become available.
Parametricity and algebraic laws about effects are powerful forms of modular reasoningthat complement basic equational reasoning. Together they allow MRI to provide effective modular reasoning techniques for non-interference of tightly coupled IP components,
which is a notoriously hard problem in the literature.
Besides providing a modular reasoning framework, an additional benefit of MRI is thatit provides a simple and lightweight model of inheritance as a Haskell library. Monadic
mixins are a useful concept for functional programming and, in some sense, they can beviewed as a simple approach to AOP in Haskell.

Acknowledgments
We are grateful to Jonathan Aldrich, Benjamin Delaware, Marko van Dooren, Jeremy
Gibbons, Simon Peyton Jones, Steven Keuchel, Shriram Krishnamurthi, Adriaan Moors,
Janis Voigtländer, Meng Wang and the anonymous reviewers for their useful comments;
and to Andres Löh for supporting lhs2tex.
Bruno Oliveira was supported by the Engineering Research Center of Excellence Program of Korea Ministry of Education, Science and Technology (MEST) / Korea Scienceand Engineering Foundation (KOSEF) grant number R11-2008-007-01002-0, the Midcareer Researcher Program (2010-0022061) through NRF grant funded by the MEST, andby a grant from the Portugal-UT Austin CoLab program.

ZU064-05-FPR

paper

38

22 August 2012

14:18

B. Oliveira, T. Schrijvers and W. Cook
References

Aldrich, J. (2005). Open modules: Modular reasoning about advice. Pages 144–168 of: ECOOP’05:
19th European Conference on Object-Oriented Programming.
Bagherzadeh, M., Rajan, H., Leavens, G. T., & Mooney, S. (2011). Translucid contracts: Expressive
specification and modular verification for aspect-oriented interfaces. Pages 141–152 of: AOSD’11:
10th International Conference on Aspect-Oriented Software Development.
Bird, R. S., & De Moor, O. (1997). Algebra of programming. International Series in Computing
Science, vol. 100.
Bracha, G., & Cook, W. (1990). Mixin-based inheritance. Pages 303–311 of: Proceedings of theeuropean conference on object-oriented programming on object-oriented programming systems,
languages, and applications. OOPSLA/ECOOP ’90. New York, NY, USA: ACM.
Chen, K., Weng, S., Wang, M., Khoo, S., & Chen, C. (2007). A compilation model for aspectoriented polymorphically typed functional languages. Pages 34–51 of: SAS’07: 14th international
symposium on static analysis.
Chen, K., Weng, S.-C., Lin, J.-Y., Wang, M., & Khoo, S.-C. (2011). Side-effect localization for lazy,
purely functional languages via aspects. Higher-order and symbolic computation, 1–39.
Clifton, C., & Leavens, G. T. (2002). Observers and Assistants: A Proposal for Modular AspectOriented Reasoning. Pages 33–44 of: FOAL’02: 1st Workshop on Foundations of Aspect-Oriented
Languages.
Clifton, C., Leavens, G. T., & Noble, J. (2007). MAO: Ownership and effects for more effective
reasoning about aspects. Pages 451–475 of: ECOOP’07: 21sth European Conference on ObjectOriented Programming.
Cook, W., & Palsberg, J. (1989). A denotational semantics of inheritance and its correctness. Pages
433–443 of: Conference proceedings on object-oriented programming systems, languages andapplications. OOPSLA ’89.
Cook, W. R. (1989). A denotational semantics of inheritance. Ph.D. thesis, Brown University.
Dahl, O.-J., & Nygaard, K. (1966).
Simula: An ALGOL-based simulation language.
Communications of the acm, 9(9), 671–678.
Dantas, D. S., & Walker, D. (2006). Harmless advice. Pages 383–396 of: POPL’06: 33rd Symposiumon Principles of Programming Languages.
Dantas, D. S., Walker, D., Washburn, G., & Weirich, S. (2008). AspectML: A polymorphic aspectoriented functional programming language. ACM Transactions on Programming Languages andSystems, 30(3), 1–60.
De Fraine, B., & Braem, M. (2007). Requirements for reusable aspect deployment. Pages 176–
183 of: Lumpe, Markus, & Vanderperren, Wim (eds), Software composition. Lecture Notes in
Computer Science, vol. 4829. Springer Berlin / Heidelberg.
Douence, R., Fradet, P., & Südholt, M. (2004). Composition, reuse and interaction analysis of statefulaspects. Pages 141–150 of: AOSD’04: 3rd International Conference on Aspect-Oriented Software
Development.
Dutchyn, C., Tucker, D. B., & Krishnamurthi, S. (2006). Semantics and scoping of aspects in higherorder languages. Science of computer programming, 63(3), 207–239.
Flatt, M., Krishnamurthi, S., & Felleisen, M. (1998). Classes and mixins. Pages 171–183 of: Popl.
Gibbons, J., & Hinze, R. (2011). Just do it: Simple monadic equational reasoning. Pages 2–14 of:
ICFP’11: 16th International Conference on Functional Programming.
Hughes, J. (1998). Generalising monads to arrows. Science of computer programming, 37, 67–111.
Hutton, G., & Fulger, D. (2008). Reasoning About Effects: Seeing the Wood Through the Trees.
Proceedings of the symposium on trends in functional programming.

ZU064-05-FPR

paper

22 August 2012

14:18

MRI: Modular Reasoning about Interference in Incremental Programming

39

Jaskelioff, Mauro. (2008). Monatron: An Extensible Monad Transformer Library. Pages 233–248 of:
IFL’08: 20th international conference on Implementation and application of functional languages.
Jones, Mark P. (2000). Type classes with functional dependencies. Pages 230–244 of: Esop’00.
Katz, S. (1993). A superimposition control construct for distributed systems. Acm trans. program.
lang. syst., 15(2), 337–356.
Katz, S. (2006). Aspect categories and classes of temporal properties. Transactions on aspectoriented software development I, 3880, 106–134.
Kiczales, G., & Lamping, J. (1992). Issues in the design and specification of class libraries. Pages
435–451 of: OOPSLA’92: 7th Annual Conference on Object-Oriented Programming Systems,
Languages, and Applications.
Kiczales, G., & Mezini, M. (2005). Aspect-oriented programming and modular reasoning. Pages
49–58 of: ICSE’05: 27th International Conference on Software Engineering.
Kiczales, G., Lamping, J., Menhdhekar, A., Maeda, C., Lopes, C., Loingtier, J., & Irwin, J. (1997).
Aspect-oriented programming. Pages 220–242 of: ECOOP’97: 17th European Conference on
Object-Oriented Programming.
Lamping, J. (1993). Typing the specialization interface. Pages 201–214 of: OOPSLA’93: 8th Annual
Conference on Object-Oriented Programming Systems, Languages, and Applications.
Leino, K. Rustan M. (1998). Data groups: specifying the modification of extended state. Pages
144–153 of: OOPSLA’98: 13th Annual Conference on Object-Oriented Programming Systems,
Languages, and Applications.
Lewis, J. R., Launchbury, J., Meijer, E., & Shields, M. B. (2000). Implicit parameters: dynamic
scoping with static types. Pages 108–118 of: POPL’00: 27th Symposium on Principles ofProgramming Languages.
Liang, S., & Hudak, P. (1996). Modular denotational semantics for compiler construction. Pages
219–234 of: ESOP’96: European Symposium on Programming. Springer-Verlag.
Liang, S., Hudak, P., & Jones, M. (1995). Monad transformers and modular interpreters. Pages
333–343 of: POPL’95: 22nd Symposium on Principles of Programming Languages.
Ligatti, J., Walker, D., & Zdancewic, S. (2006). A type-theoretic interpretation of pointcuts andadvice. Science of computer programming, 63(3), 240–266.
Lopez-Herrejon, R., Batory, D., & Lengauer, C. (2006). A disciplined approach to aspectcomposition. Pages 68–77 of: PEPM’06: Symposium on Partial evaluation and semantics-based
program manipulation.
Masuhara, H., Tatsuzawa, H., & Yonezawa, A. (2005). Aspectual Caml: an aspect-oriented
functional language. Pages 320–330 of: ICFP’05: 10th International Conference on Functional
Programming.
McBride, Conor, & Paterson, Ross. (2008). Applicative programming with effects. Journal of
Functional Programming, 18(01), 1–13.
Müller, P., Poetzsch-Heffter, A., & Leavens, G. T. (2003). Modular specification of frame properties
in jml. Concurrency and computation: Practice and experience, 15(2), 117–154.
Oliveira, B. C. d. S., Schrijvers, T., & Cook, W. R. (2010). EffectiveAdvice: disciplined advice with
explicit effects. Pages 109–120 of: AOSD’10: 9th International Conference on Aspect-Oriented
Software Development.
Peyton Jones, S., Vytiniotis, D., Weirich, S., & Shields, M. (2007). Practical type inference forarbitrary-rank types. Journal of Functional Programming, 17(01), 1–82.
Prehofer, C. (1997). Feature-oriented programming: A fresh look at objects. Pages 419–443 of:
ECOOP’97: 11th European Conference on Object-Oriented Programming.
Prehofer, C. (1999). Flexible construction of software components: A feature oriented approach.
Habilitation Thesis, Fakultät für Informatik der Technischen Universität München.

ZU064-05-FPR

paper

40

22 August 2012

14:18

B. Oliveira, T. Schrijvers and W. Cook

Prehofer, C. (2006). Semantic reasoning about feature composition via multiple aspect-weavings.
Pages 237–242 of: GPCE’06: 5th International conference on Generative programming andcomponent engineering.
Reynolds, J. C. (1974). Towards a theory of type structure. Pages 408–423 of: Programming
symposium. Lecture Notes in Computer Science, vol. 19. Springer-Verlag.
Reynolds, John C. (1983). Types, abstraction and parametric polymorphism. Pages 513–523 of:IFIP Congress.
Rinard, M., Salcianu, A., & Bugrara, S. (2004). A classification system and analysis for aspectoriented programs. ACM SIGSOFT Software Engineering Notes, 29(6), 147–158.
Ruby, C., & Leavens, G. T. (2000). Safely creating correct subclasses without seeing superclasscode. Pages 208–228 of: OOPSLA’00: 15th Annual Conference on Object-Oriented Programming
Systems, Languages, and Applications.
Salcianu, A., & Rinard, M. C. (2005). Purity and side effect analysis for java programs. Pages 199–
215 of: VMCAI’05: 6th International Conference on Verification, Model Checking, and Abstract
Interpretation. Lecture Notes in Computer Science, vol. 3385.
Schrijvers, T., & Oliveira, B. C. d. S. (2011). Monads, zippers and views: Virtualizing the monadstack. Pages 32–44 of: ICFP’11: 16th International Conference on Functional Programming.
Stata, R., & Guttag, J. V. (1995). Modular reasoning in the presence of subclassing. Pages 200–214
of: OOPSLA’95: 10th Annual Conference on Object-Oriented Programming Systems, Languages,
and Applications.
Tanter, É. (2008). Expressive scoping of dynamically-deployed aspects. Pages 168–179 of:
AOSD’08: 7th International Conference on Aspect-Oriented Software Development.
Voigtländer, J. (2009). Free theorems involving type constructor classes. Pages 173–184 of:
ICFP’09: 14th International Conference on Functional Programming.
Wadler, P. (1989). Theorems for free! Pages 347–359 of: FPLCA’89: 4th International Conference
on Functional Programming and Computer Architecture.
Wadler, P. (1992a). The essence of functional programming. Pages 1–14 of: POPL’92: 19th
Symposium on Principles of Programming Languages.
Wadler, P. (1992b). Monads for functional programming. Program design calculi: Marktoberdorf
international summer school on program design calculi.
Wang, M., & Oliveira, B. C. d. S. (2009). What does aspect-oriented programming mean forfunctional programmers? Pages 37–48 of: Wgp’09: 8th workshop on generic programming.

ZU064-05-FPR

paper

22 August 2012

14:18

MRI: Modular Reasoning about Interference in Incremental Programming

41

A Background on Parametricity-based Proofs
In the following sections we present a number of parametricity-based proofs related tomonads and monad transformers. For this purpose, we closely follow the style and formalism set out by Voigtländer (2009), who specifically covers the technique of deriving freetheorems for type constructors restricted by type class constraints.
We recommend the reader to look at Voigtländer’s work for the details, but summarize
the essence of the formalism here. In a nutshell, parametricity derives a free theorem forevery expression x with a polymorphic type such as ∀a.τ. This free theorem consists of a
relation R between instances of the expression xτ1 and xτ2 . This relation R is parameterized
by a relation R between the types τ1 and τ2 . Typically, when a function is chosen for R,
R becomes an equational relation. Voigtländer’s work captures two extensions: 1) dealing
with type constructors and 2) dealing with type class constraints.
Type Constructors In Wadler’s methodology for deriving free theorems (1989), free typevariables are interpreted as relations between arbitrarily chosen closed types (and thenquantified over via relation variables, formally denoted R). Similarly, Voigtländer interpretes free type constructor variables as functions on such relations tied to arbitrarily
chosen type constructors. These functions are also called relational actions.
Let κ1 and κ2 be type constructors (of kind ∗ → ∗). Then formally, a relational action forthem, denoted F : κ1 ⇔ κ2 , is a function F on relations between closed types such thatevery R : τ1 ⇔ τ2 (for arbitrary τ1 and τ2 ) is mapped to an F R : κ1 τ1 ⇔ κ2 τ2 .
Type Class Constraints Wadler (1989) shows how to treat type class constraints forordinary types. Basically, the relation R chosen as interpretation for the constrained typevariable is restricted to those that relate types that are instances of the type class. Furthermore, every type class method (seen as a new constant in the language) must be related toitself by the relational interpretation.
The same approach applies to type constructor classes, where we now speak of C actions
for relational actions restricted to type class C. For instance, for type variables constrainedby the Monad type class, we speak of Monad actions. Formally, relational action F : κ1 ⇔
κ2 is a Monad action iff:
• The type constructors κ1 and κ2 are instances of Monad,• (returnκ1 , returnκ2 ) ∈ ∀R.R → F R, and• ((>>=κ1 ), (>>=κ2 )) ∈ ∀R.∀S .F R → ((R → F S ) → F S ).
Monad Transformer actions and MonadState actions are defined in a similar way.

B Proof of Free Theorem for Stateful Components
Instead of the specific theorem for new p x, we prove a more general theorem:

ZU064-05-FPR

paper

42

22 August 2012

14:18

B. Oliveira, T. Schrijvers and W. Cook
Theorem 9 (S TATEFUL C ODE)
For any mx :: ∀m.SM s m ⇒ m b we have:mx≡

do s0 ← getlet (r, s1 ) = runS mx s0
put s1
return r

Then mx = new p x is a special case.
Proof
Let F : κ ⇔ S s be defined as
F R = κ R; h−1
whereh mx = get >>= λ s0 → let (s1 , r) = runS mx s0
in put s1 >> return rand ; is relation composition:
R1 ; R2 = {(x, z) | (x, y) ∈ R1 , (y, z) ∈ R2 }We show that F is both a Monad and a MonadState action. Then if we choose R to be
the identity function id, the theorem follows.
Firstly, F is a Monad action. Indeed,• (returnκ , returnState s ) ∈ R → F R since for every (a, b) ∈ R :— (returnκ a, returnκ b) ∈ κ R, and— (returnκ b, returnState s b) ∈ h−1 , asgetκ >>= λ s0 → let (r1 , s1 ) = runS (returnState s b) s0
in putκ s1 >> returnκ r1≡ {-reduce runS (returnState s b) s0 -}getκ >>= λ s0 → let (r1 , s1 ) = (b, s0 ) in putκ s1 >> returnκ r1≡ {-eliminate let binding -}getκ >>= λ s0 → putκ s0 >> returnκ b≡ {-G ET-P UT law -}returnκ () >> returnκ b≡ {-R ETURN -B IND law -}returnκ b• (>>=κ , >>=State s ) ∈ F R → (R → F S ) → F S , since for every (mx2 , mx1 ) ∈F R and (f2 , f1 ) ∈ R → F S we have that (mx2 >>=κ f2 , mx1 >>=State s f1 ) ∈ F S ,as:getκ >>= λ s0 → let (r1 , s1 ) = runS (mx1 >>=State s f1 ) s0
in putκ s1 >> returnκ r1

ZU064-05-FPR

paper

22 August 2012

14:18

MRI: Modular Reasoning about Interference in Incremental Programming≡ {-unfold >>=State s -}getκ >>= λ s0 → let (r1 , s1 ) =runS (S (λ s2 → let (r3 , s3 ) = runS mx1 s2
in runS (f1 r3 ) s3 )) s0
in putκ s1 >> returnκ r1≡ {-reduce runS -}getκ >>= λ s0 → let (r1 , s1 ) = let (r3 , s3 ) = runS mx1 s0
in runS (f1 r3 ) s3
in putκ s1 >> returnκ r1≡ {-let floating -}getκ >>= λ s0 → let (r3 , s3 ) = runS mx1 s0
in let (r1 , s1 ) = runS (f1 r3 ) s3
in putκ s1 >> returnκ r1≡ {-P UT-P UT law -}getκ >>= λ s0 → let (r3 , s3 ) = runS mx1 s0 in putκ s3 >>let (r1 , s1 ) = runS (f1 r3 ) s3 in putκ s1 >> returnκ r1≡ {-R ETURN -B IND law -}getκ >>= λ s0 → let (r3 , s3 ) = runS mx1 s0 in putκ s3 >> returnκ s3>>= λ s4 → let (r1 , s1 ) = runS (f1 r3 ) s4 in putκ s1 >> returnκ r1≡ {-G ET-P UT law -}getκ >>= λ s0 → let (r3 , s3 ) = runS mx1 s0 in putκ s3 >> getκ >>= λ s4 →let (r1 , s1 ) = runS (f1 r3 ) s4 in putκ s1 >> returnκ r1≡ {-R ETURN -B IND law -}getκ >>= λ s0 → let (r3 , s3 ) = runS mx1 s0 in putκ s3 >> returnκ r3>>=κ λ r4 →getκ >>= λ s4 → let (r1 , s1 ) = runS (f1 r4 ) s4 in putκ s1 >> returnκ r1≡ {-fold h -}h mx1 >>=κ h ◦ f1
and (h mx2 >>=κ h ◦ f2 , h mx1 >>=κ h ◦ f1 ) ∈ κ S .
Moreover, it is a MonadState action. Indeed,• (getκ , getState s ) ∈ F ids since:getκ >>= λ s0 → let (r1 , s1 ) = runS getState s s0 in putκ s1 >> returnκ r1≡ {-reduce runS getState s s0 -}getκ >>= λ s0 → let (r1 , s1 ) = (s0 , s0 ) in putκ s1 >> returnκ r1≡ {-eliminate let binding -}getκ >>= λ s0 → putκ s0 >> returnκ s0≡ {-G ET-G ET law -}getκ >>= λ s0 → getκ >>= λ s1 → putκ s1 >> returnκ s0≡ {-G ET-P UT law -}getκ >>= λ s0 → return () >> returnκ s0≡ {-R ETURN -B IND law -}getκ >>= λ s0 → returnκ s043

ZU064-05-FPR

paper

44

22 August 2012

14:18

B. Oliveira, T. Schrijvers and W. Cook
≡ {-B IND -R ETURN law -}getκ• (putκ , putState s ) ∈ ids → F id() since for every s:getκ >>= λ s0 → let (r1 , s1 ) = runS (putState s s) s0 in putκ s1 >> returnκ r1≡ {-reduce runS (putState s s) s0 -}getκ >>= λ s0 → let (r1 , s1 ) = ((), s) in putκ s1 >> returnκ r1≡ {-eliminate let binding -}getκ >>= λ s0 → putκ s >> returnκ ()≡ {-G ET-Q UERY law -}putκ s >> returnκ ()≡ {-unit singleton type -}putκ s

ZU064-05-FPR

paper

22 August 2012

14:18

MRI: Modular Reasoning about Interference in Incremental Programming

45

C Proof of Harmlessness Theorem
We have subdivided our proof into five auxiliary lemmas. The core of the proof relies onparametricity: Lemma 2 derives the free theorem for the monad type variable of the mixin
component and Lemma 3 does the same for the monad transformer type variable in thebase component. However, first Lemma 1 introduces an alternative, but equivalent, shapeof augmentation advice that is more suitable for deriving the free theorem, but less suitablefor human consumption. Lemmas 6 and 7 simplify two complex intermediate expressions
using equational reasoning, type class axioms and Lemma 2. Finally, the main proof itself
in Section C.2 ties together the other four lemmas.
C.1 Auxiliary Lemmas
First, we show how to convert between the self-explanatory form of augmentation mixin
used in the paper and the more dense form a → t m (b → t m c) that is convenient for
writing proofs. The connection between the two forms is captured by the convert function,
which translates from the former to the latter.
convert :: (Monad m, MonadTrans t, Monad (t m))⇒ (a → t m c, a → b → c → t m ())→ (a → t m (b → t m ()))
convert (bef , aft) =λ a → bef a >>= (λ c → return (λ b → aft a b c))
The counterpart of the augment function isaround :: (Monad m, MonadTrans t, Monad (t m))⇒ (a → t m (b → t m ()))
→ Open (a → t m b)
around mix = λ super →λ a → mix a >>= λ aft →super a >>= λ r →aft r>>= \ →
return r
Lemma 1
Consider augmentation mixin (bef , aft) :: (a → t m c, a → b → c → t m ()), thenwe have that:augment (bef , aft) ≡ around (convert (bef , aft))where m is a Monad and t is a MonadTrans.
Proofaround (convert (bef , aft))≡ {-unfold around -}(λ super → λ a → convert (bef , aft) a >>= λ aft0

ZU064-05-FPR

paper

46

22 August 2012

14:18

B. Oliveira, T. Schrijvers and W. Cook→ super a >>= λ b→ aft0 b >>= \→ return b)≡ {-unfold convert -}(λ super → λ a → bef a >>= λ c→ return (λ b → aft a b c) >>= λ aft0
→ super a>>= λ b0
→ aft b >>= \→ return b)≡ {-R ETURN -B IND law -}(λ super → λ a → bef a >>= λ c→ super a>>= λ b→ aft a b c >>= \→ return b)≡ {-fold augment -}augment (bef , aft)

Here is the second auxiliary lemma.
Lemma 2
Consider a function f :: ∀m.Monad m ⇒ a → m (b → m c), then we have that:fm ≡ (out (return ◦ out (return ◦ runI) ◦ runI)) fI
Proof
Let F : m ⇔ I be the Monad action
F R = return−1 ; R; I
. This is a Monad action indeed, as was already shown by Voigtländer (see (Voigtländer,2009), p.5, as part of the proof of Theorem 1).
Lemma 3
Consider a function f :: ∀t.MonadTrans t ⇒ (a → t m (b → t m ())) → a → t m bwith m an arbitrary monad, then we have that:out π ◦ f ≡out runIT ◦ f ◦ out (IT ◦ fmap (out (IT ◦ π)) ◦ π)
for any π :: ∀m, a.Monad m ⇒ t m a → m a with t an arbitrary monad transformer
that satisfies the following property:
π ◦ lift≡ idwhere out = (◦) applies a function to the output of another function.
Proof

ZU064-05-FPR

paper

22 August 2012

14:18

MRI: Modular Reasoning about Interference in Incremental Programming47

Let T : τ ⇔ IT be the MonadTrans action
T F R = π; F R; IT. This is a MonadTrans action indeed:• (liftt , liftIT ) ∈ ∀F , R.F R → T F R, since for every (a, b) ∈ F R we have(liftt a, liftIT b) = (liftt a, IT b) ∈ π; F R; IT because of Property (1) of π.
Then we have for all (h, h0 ) ∈ (idb → T m id() ), that h0 ≡ IT ◦ π ◦ h), because m id ≡ id.
Assume that (g, g0 ) ∈ ida → T m (idb → T m id() ), where g0 ≡ out (IT ◦ fmap (out (IT ◦π)) ◦ π) g. Then, for (f g, f g0 ) ∈ ida → T m idb the lemma follows.
Now, we only have to show that the assumption wrt. (g, g0 ) is valid. The assumption isvalid if for all (a, a) ∈ ida , we have that (ga, g0 a) ∈ T m (idb → T m id() ). This holds if,
applying T , we have that (pro j(ga), unIdT (g0 a)) ∈ m (idb → T m id() ). By equational
reasoning, we get(π (g a), runIT (g0 a))≡ {-unfold g0 -}(π (g a), runIT ◦ IT ◦ fmap (out (IT ◦ π)) $ π (g a))≡ {-runIT ◦ IT ≡ id -}(π (g a), fmap (out (IT ◦ π)) $ π (g a))≡ {-unfold fmap and out -}(π (g a), π (g a) >>= λ f → return (IT ◦ π ◦ f ))≡ {-B IND -R ETURN law -}(π (g a) >>= return,
π (g a) >>= λ f → return (IT ◦ π ◦ f ))Note that (π (g a), π (g a)) ∈ m R, and (>>=, >>=) ∈ m R → (R → m S ) → m S , whereR = idb → t m id() = idb→t m () and S = idb → T m id() . Thus, we must show that
(return, λ f → return (IT ◦ π ◦ f )) ∈ (R → m S ). So for any ( f , f ) ∈ R, we must showthat (return f , return (IT ◦ π ◦ f )) ∈ m S . As (return, return) ∈ S → m S , this amounts toshowing that (f , IT ◦ π ◦ f ) ∈ S . Take any (b, b) ∈ idb,b , then (f b, IT ◦ π $ f b) ∈ T m id()should hold. In other words, IT ◦ id ◦ π $ f b ≡ IT ◦ π $ f b should hold. This is indeed true.
Hence the assumption about (g, g0 ) does hold.
Here is the fourth auxiliary lemma.
Lemma 6
Consider a function mix :: ∀m.Monad m ⇒ a → t m (b → t m ()), then we havethat:(out (IT ◦ fmap (out (IT ◦ π)) ◦ π)) mix≡
const (return (const (return ())))
where t is a MonadTrans.
Proof(out (IT ◦ fmap (out (IT ◦ π)) ◦ π)) mix≡ {-out (f ◦ g) ≡ out f ◦ out g -}

ZU064-05-FPR

paper

48

22 August 2012

14:18

B. Oliveira, T. Schrijvers and W. Cook(out (IT ◦ fmap (out IT ◦ out π) ◦ π)) mix≡ {-fmap (g ◦ h) ≡ fmap g ◦ fmap h -}(out (IT ◦ fmap (out IT ) ◦ fmap (out π) ◦ π)) mix≡ {-out (f ◦ g) ≡ out f ◦ out g -}(out (IT ◦ fmap (out IT )) ◦ out (fmap (out π) ◦ π)) mix≡ {-unfold def. of (◦) -}(out (IT ◦ fmap (out IT ))) (out (fmap (out π) ◦ π) mix)
≡ {-Lemma 2 -}(out (IT ◦ fmap (out IT ))) ((out (return ◦ out (return ◦ runI) ◦ runI))(out (fmap (out π) ◦ π) mix))≡ {-out (f ◦ g) ≡ out f ◦ out g (×3) -}(out (IT ◦ fmap (out IT ))) ((out (return ◦ out return)(out (out runI ◦ runI) (out (fmap (out π) ◦ π) mix))))≡ {-Totality assumption -}(out (IT ◦ fmap (out IT ))) ((out (return ◦ out return)) (const (const ())))≡ {-unfold def. of (◦) and out -}(out (IT ◦ fmap (out IT ))) (const (return (const (return ()))))≡ {-unfold def. of out -}const ((IT ◦ fmap (out IT ) ◦ return) (const (return ())))≡ {-fmap h ◦ return ≡ return ◦ h -}const ((IT ◦ return ◦ out IT ) (const (return ())))≡ {-IT ◦ return ≡ return -}const ((return ◦ out IT ) (const (return ())))≡ {-out f (const x) ≡ const (f x) -}const (return (const (IT (return ()))))≡ {-IT ◦ return ≡ return -}const (return (const (return ())))

Define  as the counterpart of :() :: ∀t m a b.(Monad m, MonadTrans t, Monad (t m))⇒ Augment a t m b→ Open (a → t m b)
→ Open (a → t m b)
mixin  base = around mixin  base
Here is the fifth auxiliary lemma.

ZU064-05-FPR

paper

22 August 2012

14:18

MRI: Modular Reasoning about Interference in Incremental Programming

49

Lemma 7
Consider a function bse :: ∀t.MonadTrans t ⇒ Open (a → t m b), then we havethat:
new ((const (return (const (return ()))))  bse)≡
new bsewhere m is a Monad.
Proof
new ((const (return (const (return ()))))  bse)
≡ {-unfold def. of  -}new (λ p x → const (return (const (return ()))) x >>= λ aft → bse p x>>= λ r → aft r >>= \ → return r)≡ {-unfold const -}new (λ p x → return (const (return ())) >>= λ aft → bse p x>>= λ r → aft r >>= \ → return r)≡ {-R ETURN -B IND law -}new (λ p x → bse p x >>= λ r → const (return ()) r >>= \ → return r)≡ {-unfold const -}new (λ p x → bse p x >>= λ r → return () >>= \ → return r)≡ {-R ETURN -B IND law -}new (λ p x → bse p x >>= λ r → return r)≡ {-η-reduction -}new (λ p x → bse p x >>= return)≡ {-B IND -R ETURN law -}new (λ p x → bse p x)
≡ {-η-reduction -}new bseC.2 Main Proof
The main theorem follows from the above lemmas.
Proofπ ◦ new ((bef , aft)  bse)
≡ { Lemma 1 }π ◦ new (convert (bef , aft)  bse)
≡ { let mix = convert (bef , aft) }π ◦ new (mix  bse)
≡ { abstract over mix }π ◦ ((λ x → new (x  bse)) mix)
≡ { fold out }(out π ◦ (λ x → new (x  bse))) mix

ZU064-05-FPR

paper

50

22 August 2012

14:18

B. Oliveira, T. Schrijvers and W. Cook≡

{ Lemma 3 }(out runIT ◦ (λ x → new (x  bse)) ◦ out (IT ◦ fmap (out (IT ◦ π)) ◦ π)) mix≡ { unfold def. of (◦) }(out runIT ◦ (λ x → new (x  bse))) ((out (IT ◦ fmap (out (IT ◦ π)) ◦ π)) mix)
≡ { Lemma 6 }(out runIT ◦ (λ x → new (x  bse))) (const (return (const (return ()))))≡ { unfold def. of (◦) }out runIT ((λ x → new (x  bse)) (const (return (const (return ())))))≡ { β -reduction }out runIT (new ((const (return (const (return ()))))  bse))≡ { Lemma 7 }out runIT (new bse)

D Proofs of Projection Functions
In this section we prove the projection function precondition of the Harmless Mixin theorem for two specific monads. The proofs are fairly straightforward equational reasoning
and application of the monad axioms.
D.1 The πW Function
Proof
πW ◦ lift≡ {-unfold ◦ -}(λ m → πW (lift m))≡ {-unfold lift -}(λ m → πW (WT (m >>= λ x → return (x, mempty))))≡ {-unfold πW -}(λ m → runWT (WT (m >>= λ x → return (x, mempty))) >>= return ◦ fst)
≡ {-runWT (WT m) ≡ m -}(λ m → m >>= λ x → return (x, mempty) >>= return ◦ fst)
≡ {-R ETURN -B IND law -}(λ m → m >>= λ x → (return ◦ fst) (x, mempty))≡ {-unfold ◦ -}(λ m → m >>= λ x → return (fst (x, mempty)))≡ {-unfold fst -}(λ m → m >>= λ x → return x)≡ {-η-reduction -}(λ m → m >>= return)≡ {-B IND -R ETURN law -}(λ m → m)≡ {-fold id -}id

ZU064-05-FPR

paper

22 August 2012

14:18

MRI: Modular Reasoning about Interference in Incremental Programming

51

D.2 The πS Function
Proof
πS s0 ◦ lift
≡ {-unfold ◦ -}(λ m → πS s0 (lift m))≡ {-unfold lift -}(λ m → πS s0 (ST (λ s → m >>= λ x → return (x, s))))≡ {-unfold πS -}(λ m → runST (ST (λ s → m >>= λ x → return (x, s))) s0 >>= return ◦ fst)
≡ {-runST (ST f ) ≡ f -}(λ m → (λ s → m >>= λ x → return (x, s)) s0 >>= return ◦ fst)
≡ {-β -reduction -}(λ m → m >>= λ x → return (x, s0 ) >>= return ◦ fst)
≡ {-R ETURN -B IND law -}(λ m → m >>= λ x → (return ◦ fst) (x, s0 ))≡ {-unfold ◦ -}(λ m → m >>= λ x → return (fst (x, s0 )))≡ {-unfold fst -}(λ m → m >>= λ x → return x)≡ {-η-reduction -}(λ m → m >>= return)≡ {-B IND -R ETURN law -}(λ m → m)≡ {-fold id -}id

E Proof of Harmless Observation Mixin
The structure of the Harmless Observation Mixin proof is the same as that of the Harmless
Mixin proof. We can even reuse two of the five lemmas. The other three need to be adjusted
to the MGet additional constraint. Notably, Lemma 8 derives the corresponding parametricity result which is weaker than that of Lemma 2. Fortunately, Lemma 9 compensates forthis by exploiting the MGet axioms.
E.1 Auxiliary Lemmas
Again we turn to the same convenient intermediate form for augmentation mixins that weused for the proof of orthogonal harmless mixins. We define  as the counterpart of  for:() :: (MGet s m, MonadTrans t, Monad (t m))⇒ (a → t m (b → t m ()))

ZU064-05-FPR

paper

22 August 2012

52

14:18

B. Oliveira, T. Schrijvers and W. Cook
→ Open (a → t m b)
→ Open (a → t m b)
mixin  base = around mixin ‘observation‘ base

Again we first formulate and prove a few lemmas before we proceed with the main
proof.
Lemma 8
Consider a function f :: ∀m.MGet s m ⇒ a → m (b → m c), then we have that:fm ≡ (out (λ m → aux m >>= return ◦ out aux)) f(R s)where
aux :: MGet s m ⇒ R s a → m a
aux m = get >>= λ s → return (runR m s)

Proof
Let F : m ⇔ R s be the MGet s action
F R = (get>>=)−1 ; out return−1 ; ids → R ; R.
This is indeed a MGet s action:• Assume that (a, b) ∈ R. We have that (get>>=)−1 (returnm a) = const (returnm a).
Also, out return−1 (const (returnm a)) = const a. Finally, note that R (const b) =returnR s b. In conclusion, (returnm , returnR s ) ∈ R → F R.
• For getm we do have that (get>>=)−1 getm = returnm , and out return−1 returnm = id.
Moreover, id ◦ id ◦ id = id. Finally, R id = getR s . Ergo, (getm , getR s ) ∈ F ids .
• For all R, S , (f1 , f2 ) ∈ ids → R and for all (k1 , k2 ) ∈ iR → ids → S , We havethat (get >>= λ s → return (f1 s), get >>= λ s → return (f2 s)) ∈ F R. Similarly, we
have that (λ x → get >>= λ s → return (k1 x s), λ x → get >>= λ s → return (k2 x s)) ∈R → F S . Moreover,get >>= λ s → return (f1 s)≡ {-unfold return -}get >>= λ s → R (const (f1 s))≡ {-unfold get -}R id >>= λ s → R (const (f1 s))≡ {-unfold >>= -}R $ λ s → runR (R (const (f1 (runR (R id) s)))) s≡ {-runR (R f ) ≡ f -}R $ λ s → const (f1 (id s)) s≡ {-unfold const -}R $ λ s → f1 (id s)≡ {-unfold id -}R $ λ s → f1 s

ZU064-05-FPR

paper

22 August 2012

14:18

MRI: Modular Reasoning about Interference in Incremental Programming53≡ {-η-reduction -}R f1
Similarly, we can show that
λ x → get >>= λ s → return (k2 x s)
≡ {-... -}λ x → R (k2 x)
Now consider (get >>= λ s → return (f1 s) >>= λ x → get >>= λ s0 → return (k1 x s0 ),R f2 >>= λ x → R (k2 x)). We can rewrite the first component
get >>= λ s → return (f1 s) >>= λ x → get >>= λ s0 → return (k1 x s0 )≡ {-R ETURN -B IND law -}get >>= λ s → get >>= λ s0 → return (k1 (f1 s) s0 )≡ {-get idempotence -}get >>= λ s → return (k1 (f1 s) s)
If we apply (get>>=)−1 ; out return−1 to this, we get λ s → (k1 (f1 s) s).
Similarly, we can rewrite the second component
R f2 >>= λ x → R (k2 x)≡ {-unfold >>= -}R $ λ s → runR (R (k2 (runR (R f2 ) s))) s≡ {-runR (R f ) ≡ f -}R $ λ s → runR (R (k2 (f2 s))) s≡ {-runR (R f ) ≡ f -}R $ λ s → k2 (f2 s) s
Summarizing, the original pair is in F S . Hence, we have that (>>=m , >>=R s ) ∈F R → (R → F S ) → F S .
Note that the function aux captures F id. The theorem follows.
The next lemma is the counterpart of Lemma 6.
Lemma 9Consider a function mix :: ∀m.MGet s m ⇒ a → t m (b → t m ()), then we havethat:(out (IT ◦ fmap (out (IT ◦ π)) ◦ π)) mix≡
const (return (const (return ())))
where t is a MonadTrans.
Proof(out (IT ◦ fmap (out (IT ◦ π)) ◦ π)) mix≡ {-out (f ◦ g) ≡ out f ◦ out g -}(out (IT ◦ fmap (out IT ◦ out π) ◦ π)) mix

ZU064-05-FPR

paper

54

22 August 2012

14:18

B. Oliveira, T. Schrijvers and W. Cook
≡ {-fmap (g ◦ h) ≡ fmap g ◦ fmap h -}(out (IT ◦ fmap (out IT ) ◦ fmap (out π) ◦ π)) mix≡ {-out (f ◦ g) ≡ out f ◦ out g -}(out (IT ◦ fmap (out IT )) ◦ out (fmap (out π) ◦ π)) mix≡ {-unfold def. of (◦) -}(out (IT ◦ fmap (out IT ))) (out (fmap (out π) ◦ π) mix)
≡ {-let adv0 = (out (fmap (out π) ◦ π) mix) -}(out (IT ◦ fmap (out IT ))) adv0
≡ {-Lemma 8 -}(out (IT ◦ fmap (out IT ))) ((out (λ m → aux m >>= return ◦ out aux)) adv0 )≡ {-unfold aux -}(out (IT ◦ fmap (out IT ))) ((out (λ m → aux m>>= return ◦ out (λ n → get >>= λ s → return (runR n s)))) adv0 )≡ {-Totality assumption -}(out (IT ◦ fmap (out IT ))) ((out (λ m → aux m>>= return ◦ out (λ n → get >>= λ s → return ()))) adv0 )≡ {-G ET-Q UERY law -}(out (IT ◦ fmap (out IT ))) ((out (λ m → aux m>>= return ◦ out (λ n → return ()))) adv0 )≡ {-fold const -}(out (IT ◦ fmap (out IT ))) ((out (λ m → aux m>>= return ◦ out (const (return ())))) adv0 )≡ {-unfold aux -}(out (IT ◦ fmap (out IT ))) ((out (λ m → get >>= λ s → return (runR m s)>>= return ◦ out (const (return ())))) adv0 )≡ {-R ETURN -B IND law -}(out (IT ◦ fmap (out IT )))((out (λ m → get >>= λ s → return (out (const (return ())) (runR m s)))) adv0 )≡ {-out (const x) y ≡ const y -}(out (IT ◦ fmap (out IT )))((out (λ m → get >>= λ s → return (const (return ())))) adv0 )≡ {-G ET-Q UERY law -}(out (IT ◦ fmap (out IT ))) ((out (λ m → return (const (return ())))) adv0 )≡ {-fold const -}(out (IT ◦ fmap (out IT ))) ((out (const (return (const (return ()))))) adv0 )≡ {-out (const x) y ≡ const y -}(out (IT ◦ fmap (out IT ))) (const (return (const (return ()))))≡ {-out (f ◦ g) ≡ out f ◦ out g -}(out IT ◦ out (fmap (out IT ))) (const (return (const (return ()))))≡ {-unfold ◦ -}out IT (out (fmap (out IT )) (const (return (const (return ())))))≡ {-out f (const x) == const (f x) -}out IT (const (fmap (out IT ) (return (const (return ())))))≡ {-fmap f (return x) = return (f x) -}ZU064-05-FPR

paper

22 August 2012

14:18

MRI: Modular Reasoning about Interference in Incremental Programming55

out IT (const (return (out IT (const (return ())))))≡ {-out f (const x) ≡ const (f x) -}out IT (const (return (const (IT (return ())))))≡ {-IT (return x) ≡ return x -}out IT (const (return (const (return ()))))≡ {-out f (const x) == const (f x) -}const (IT (return (const (return ()))))≡ {-IT (return x) ≡ return x -}const (return (const (return ())))

Lemma 10Consider a function bse :: ∀t.MonadTrans t ⇒ Open (a → t m b), then we havethat:
new ((const (return (const (return ()))))  bse)≡
new bsewhere m is a Monad.
Proof
new ((const (return (const (return ()))))  bse)
≡ {-unfold def. of  -}new (λ p x → const (return (const (return ()))) x >>= λ aft → bse p x>>= λ r → aft r >>= \ → return r)≡ {-fold def. of  -}new ((const (return (const (return ()))))  bse)
≡ {-Lemma 7 -}new bseE.2 Main proof
The main proof is similar to the Harmless Mixin proof. The only difference lies in the useof Lemma 9, which relies on the G ET-Q UERY law.
Proofπ ◦ new ((bef , aft)  bse)
≡ {-Lemma 1 -}π ◦ new (convert (bef , aft)  bse)
≡ {-let mix = convert (bef , aft) -}π ◦ new (mix  bse)
≡ {-abstract over mix -}π ◦ ((λ x → new (x  bse)) mix)

ZU064-05-FPR

paper

56

22 August 2012

14:18

B. Oliveira, T. Schrijvers and W. Cook
≡ {-fold out -}(out π ◦ (λ x → new (x  bse))) mix≡ {-Lemma 3 -}(out runIT ◦ (λ x → new (x  bse)) ◦ out (IT ◦ fmap (out (IT ◦ π)) ◦ π)) mix≡ {-unfold def. of (◦) -}(out runIT ◦ (λ x → new (x  bse))) ((out (IT ◦ fmap (out (IT ◦ π)) ◦ π)) mix)
≡ {-Lemma 9 -}(out runIT ◦ (λ x → new (x  bse))) (const (return (const (return ()))))≡ {-unfold def. of (◦) -}out runIT ((λ x → new (x  bse)) (const (return (const (return ())))))≡ {-β -reduction -}out runIT (new ((const (return (const (return ()))))  bse))≡ {-Lemma 10 -}out runIT (new bse)