How to Make Destructive Updates Less Destructive

Martin Odersky ^{∗}

18th ACM Symposium on Principles of Programming Languages, January 1991

Abstract

We present a safe embedding of mutable data structures in functional languages. With safety we mean that confluence and (in some sense) referential transparency are maintained. We develop a static criterion based on abstract interpretation which checks that any side-effect which a function may exert via a destructive update remains invisible. The technique opens up the possibility of designing safe and efficient wide-spectrum languages which combine functional and imperative language constructs.

1 Introduction

We are interested in the design of programming notations which augment a functional core with imperative statements and mutable data structures such as arrays. These wide-spectrum languages [14] promise to bridge the gap between abstract and declarative specifications/prototypes and efficient implementations. There are advantages to having one notation instead of two for both programming activities: We can derive the program from the specification by local transformations (which can be proved correct in advance). Since we do not switch notations in the process, every intermediate step is a well defined program. Moreover, the transformation process can stop as soon as the result is efficient enough. If the strong points of both programming concepts are to be retained, however, their combination must be safe. Safety means that the usual semantics of functional and imperative programs should be preserved. This is the semantics of predicate transformers in the imperative part and lambda-calculus reduction in the functional part. As the semantics carry over to the combinations, so should the main theorems. In particular, even in the presence of assignment, the functional part should remain confluent and referentially transparent.

Combining functional expressions with statements means that, first, statements such as assignments can contain function applications and, second, that function bodies can contain statements. To obtain safety, we must control all side-effects caused by statements in a function body. An obvious first step is to allow only read access to variables which are declared outside the scope of a function. This is not enough, however. A more complex problem, which we attack in this paper, is presented by arguments to a function which are modified in the function’s statement part. Consider the following implementation of function swap:

swap a i j = x := a.i ; a.i := a.j ; a.j := x ; a.

To prevent a side-effect in swap, we either would have to implement array updates non-destructively, or we would have to pass array parameters by value. Both choices have a disastrous effect on efficiency. One could optimize array updates by using reference counts [7] or trailers [1]. However, these optimizations impose a sizable run-time overhead themselves, and it is difficult for a programmer to convince theirself of their effectiveness.

We propose instead to choose the efficient implementation for both parameter passing and array updating. Function side-effects are then possible but we will insist that all such effects remain invisible. This means that we have to impose some restrictions on the contexts in which a side-effecting function may be used. For example,

∗IBM T.J. Watson Research Center, P.O. Box 704, Yorktown Heights, NY 10598.

f (swap a i j) (a.i)

is illegal, since the value of a.i depends on the evaluation order of f’s arguments. A legal application, which avoids the “race condition” would be:

x := a.i ; f (swap a i j) x.

A context is clearly legal if the old value of an updated array a is never again accessed after the update took place. We say in this case: a is single-threaded [15]. To check single-threadedness, we develop a static wellformedness criterion for expressions. The criterion guarantees that:

• the evaluation of a well-formed expression is confluent, and

• if a well-formed expression is transformed in a sequence of substitutions of equals into another wellformed expression, then both expressions denote the same value. This is the case even if the result of some intermediate step is not well-formed.

The criterion is decidable using an abstract interpretation of the source program. Indeed, it can be efficiently computed by a compiler. In general, our effect analysis does not need any user-declared effect specifications, as effects can be reconstructed from the program text.

Related Work

Existing designs of wide-spectrum languages have not yet addressed the problem of maintaining confluence in the presence of destructive array updates. Either loss of confluence is accepted [8, 18], or array updates are presumed to be implemented non-destructively [11, 13, 14].

An alternative way to handle the problem of mutations in functional languages relies on static optimization techniques in the compiler. Data structures are then always conceptually immutable, but the optimizer might transform copying updates into in-place updates whenever it is recognized that the transformation is semantics-preserving. Some published techniques for update optimization are [1, 4, 5, 6].

Optimization techniques have the advantage that they do not change the context-rules of the compiled language. Even if optimization fails, the program is still legal. The downside is that a programmer must have a very good understanding of the optimizer’s capabilities in order to know which program can be optimized and which cannot. Such knowledge is sometimes crucial since unrecognized opportunities for optimization can add a linear factor to resource consumption. An example is the quicksort function whose space requirements can be O(log n) or O(n log n), depending on whether update optimization is successful or not [10].

All published optimization techniques are global optimizations and therefore do not coexist well with separate compilation. Moreover, due to their costs they are applicable only for small programs. Adaptation of any one of these techniques for program-checking purposes would encounter difficulties due to the large (notational and computational) overhead.

Besides optimizations, several program checking techniques have been developed for the update problem. Gifford and Lucassen present in [12] a notational framework which captures information about function sideeffects. Their treatment is based on heaps instead of variables and they do not give an effect reconstruction algorithm. Wadler [16] developed linear data types, which admit destructive updates but require every variable to be used exactly once. Again, type information has to be given explicitly, no reconstruction algorithm is presently known. A more recent approach [17], also presented by Wadler, represents an array as an abstract data type on which only one operation, init, is defined. init creates a fresh array, applies a state transformer (an argument function) to it, and subsequently discards the array while returning a computed result (which is never an array). This interesting approach has the advantage that the single-reference property is established by design. However, arrays can be manipulated only in a restricted manner. They cannot be passed to functions and state transformers can operate only on a single array at a time.

The problem we tried to solve in this paper is very similar to the one addressed by work of Hudak and Guzmán [9]. They present a type-system to capture single-threadedness, whereas our method is based on abstract interpretation. We simplify their approach in that we are able to drop without loss of precision their distinction between single- and multiple-threaded accesses. We extend their results with better approximations to the sharing behavior of a program. We model sharing configurations by an inclusion hierarchy over the storage which is reachable from bound variables. Sharing can be quite complex, as in the case where an array contains a list whose elements are again arrays. Our analysis is able to detect in that case that modifications to the root array do not change the values of the list elements, whereas modifications to a list element do change the values of all variables referring to it. Such accuracy is definitely needed for the analysis of languages with a fully orthogonal type system in which mutable and immutable types can be freely combined. The main restriction with respect to the work of Hudak and Guzmán is that we consider here only first-order languages. The reason for this restriction is that the issues of automatic effect reconstruction in the presence of higher-order functions are not yet fully resolved (this holds for our approach as well as theirs). Automatic effect reconstruction faces the problem that, in contrast to types in the Hindley-Milner system [3], a function does not always have a most general effect.

The rest of this paper is organized as follows: Section 2 presents a small language with both imperative and functional components on which the subsequent treatment is based. Section 3 introduces abstract domains used in the analysis. Section 4 presents the abstract interpretation function. Section 5 discusses humanreadable representations. Section 6 concludes.

2 An Example Language

To base the following discussion on a concrete foundation, we introduce a small single assignment language with the following syntax:

e ::= e where {f {x} = e}
| x
| f{e}
| if e_{1} then e_{2} else e_{3}
| x := e_{1} ; e_{2}.

The first four clauses define a purely functional firstorder language with local definitions, bound variables, function applications, and a conditional expression. The only statement in the language is the assignment, whose syntax is given in the fifth clause. Variables may not be assigned to more than once. Our method can be extended to more general functional/imperative combinations by mapping them into the above language. The transformation is similar in spirit to a translation into single assignment form [2].

We assume lazy evaluation in general, except for the evaluation of sequential composition. The expression x := e_{1} ; e_{2} is evaluated by first reducing e_{1} to normal form and then reducing e_{2}. If reduction terminates, the value of this construct is equal to e_{2} where x = e_{1}. We say that “;” is hyperstrict in its left argument.

Structured data types in our language are lists or arrays. Lists are representatives of more general algebraic data types found in most functional languages. They are constructed with the operator cons and taken apart with the selectors hd and tl. Arrays have dynamic size; their indices are integers. Arrays are created and manipulated with the following operators:

vec l  array of (references to) list l’s elements,
upd a i x  array with (a reference to) element x

at index position i which is otherwise equal to a,

a.i  the i’th component of a.

Our type system is fully orthogonal. The component type of an array may be any type. The elements of a list may also assume any type, including an array type.

3 The Abstract Domains

Since the implementation of updates is intended to be destructive, we have to ascertain that the “old” value of an array is never accessed after an update. A static technique for doing so is presented in this section and the next. We will present an abstract interpretation which yields for every expression a description of its effect on all variables of a program. The effect on a single variable shall be captured in an abstract use. Some requirements for this Use domain can be derived from the following examples, (1) − (7). Assume that f is a function which accesses both of its elements without modifying them. Nothing is known about the order of accesses in f, and hence, because of lazy evaluation, about the order of argument reduction.

(1)  f a a  safe
(2)  f a (upd a i x)  unsafe
(3)  g c c where
g a b = f a (upd b i x)  unsafe
(4)  b := a ; f b (upd a i x)  unsafe
(5)  b := c.(a.i) ; f b (upd a j x)  safe
(6)  b := a.i ; f b (upd a j x)  safe
(7)  b := a.i ; f b (upd a.i j x)  unsafe

(1) is clearly safe since nothing is updated. (2) is unsafe, since the second argument might be evaluated before the first one, thereby producing a visible side-effect. Cases (1) and (2) can be distinguished by having different abstract uses rd for read and wr for write accesses. Line (3) shows that effect information has to be propagated beyond function boundaries. Our abstract interpretation will map every function to an effect signature, which maps argument liabilities to a result liability.

Since (:=) means reference assignment, (4) is essentially the same situation as (2), i.e. unsafe. The similar looking case (5) however, is safe. Because of the hyperstrict evaluation of “;” the read access of value a occurs before a is updated. To distinguish cases (4) and (5) we need to keep information about variable aliases. This is done by having a value id for aliasing reads in the Use domain as well as rd (rd guarantees absence of aliasing).

Line (6) presents some difficulties. In the assignment b := a.i, should a be abstracted to rd or to id? rd seems to be too optimistic, since b does contain a reference to a part of a. Indeed, abstracting a to rd would lead to acceptance of the (unsafe) case (7). If we abstract a to id, however, we get the same analysis as in case (4), leading to a rejection of an expression which is perfectly safe. (6) is safe, because an update of an array does leave (the storage occupied by) its elements unchanged. Hence, the modification of a by evaluation of f’s second argument does not interfere with the first argument, b, which is bound to a.i. This is true in our standard semantics which assumes uniform access by reference. It would also be true if array elements were uniformly updated and retrieved by value. It would not be true for an implementation in which array elements are assigned by value but retrieved by reference, but then, this is not the semantics we consider here.

The example shows that we have to distinguish between variables and their elements in the abstract domain. This is done by mapping every variable to a pair of uses u_{1}.u_{2}, one for the variable itself and another one for its elements. The value of every expression is also split into the value itself and its elements. Hence, there are three combinations of sharing: An entity (which stands for either a variable or the elements of one) might be shared by the expression’s value, or it might be shared by the value’s elements, or it might be shared by both. The cases correspond to the abstract uses id, el, and sh.

To summarize: The effect on an entity x (either a bound variable or the elements of one) of evaluating an expression e is abstracted to:

• ⊥, if x is not accessed,

• rd, if x is read, but does not form part of e’s normal form,

• id, if x is a potential alias of e’s value,

• el, if x is a potential element of e’s value,

• sh, if x is potentially an alias or an element of e’s value,

• wr, if x is potentially updated (overwritten) during evaluation of e (in this case, the old value of x may of course be neither an alias nor an element of the result),

• ⊤, in case of conflicting accesses, where confluence might be lost.

The partial ordering of Use is depicted in Figure 1. The total effect of an expression is abstracted to a liability, a mapping from the program’s bound variables to pairs of uses.

Lia = BV ar → Use × Use

[figure: ⊥; rd; id; el; sh; wr; ⊤]

Figure 1: The Use domain

A pair of uses u_{1} and u_{2} will be written u_{1}.u_{2} Given that the liability of expression e in variable x is u_{1}.u_{2}, u_{1} represents the effect of e on x itself while u_{2} represents the effect on x’s elements. In the product domain, all pairs x.⊤ and ⊤.y are merged into the single error element ⊤.

Remark: The term “liability” (instead of “effect”) emphasizes the point that every non-bottom use in the liability of an expression restricts the contexts in which this expression may occur.

Example: The liabilities of some simple expressions are:

x  : x ↦ id.el
x + y : x ↦ rd.rd, y ↦ rd.rd
cons x y : x ↦ el.el, y ↦ el.el
a.i  : a ↦ rd.sh, i ↦ rd.rd
upd a i x : a ↦ wr.el, i ↦ rd.rd, x ↦ el.el.

4 Computation of Liabilities

This section presents our abstract interpretation for effect analysis. First, we need some operators on uses and liabilities. The liability of a compound expression is computed from the liabilities of its constituents using the combinators ⊔ (least upper bound), || (parallel composition) and ;; (sequential composition). The latter two are defined by:

⊤ || y = ⊤
x || ⊤ = ⊤
⊥ || y = y
x || ⊥ = x
x || y = ⊤,  if x = wr ∨ y = wr
= x ⊔ y,  otherwise

⊤ ;; y = ⊤
x ;; ⊤ = ⊤
⊥ ;; y = y
x ;; ⊥ = wr  if x = wr
= rd,  if x ≠ wr
x ;; y = ⊤,  if x = wr
= y,  if x ≠ wr

All operators defined in this section are assumed to be extended pointwise to the liability domain where appropriate.

A function f x_{1} ... x_{n} is abstracted to an effect signature of the form:

λl_{1}, ..., l_{n}.l_{global} || (lb x_{1}) : l_{1} || ... || (lb x_{n}) : l_{n}.

That is, the effect of a function application is the parallel composition of the function’s effect on every parameter (lb stands for the liability of its body), and its effect l_{global} on non-local variables. This amounts to regarding a function as a “black box”, in which nothing is known about execution paths. The expression x : l represents the result of applying a function with an effect x on its formal parameter to an argument expression whose liability is l. “:” is defined by:

⊤ : x.y = ⊤
u_{1}.u_{2} : ⊤ = ⊤
u_{1}.u_{2} : x.y = (u_{1}.u_{2} : x).(u_{1}.u_{2} : y)
⊥.⊥ : x = ⊥
u_{1}.u_{2} : x = x,  if x ∈ {⊥, rd, wr}
u_{1}.u_{2} : id = u_{1}
u_{1}.u_{2} : el = u_{2}
u_{1}.u_{2} : sh = u_{1} ⊔ u_{2}.

If a function accesses local variables only, we can combine its type and effect signature. We write argument uses before argument types. For example, the signatures of the predefined functions are:

(+) :: rd.rd Int → rd.rd Int → Int

(and likewise for −, *, ...)

cons :: el.el α → el.el [α] → [α]
hd :: rd.sh [α] → α

(and likewise for tl)

vec :: rd.el [α] → Array α
(.) :: rd.sh Array α → rd.rd Int → α
upd :: wr.el Array α → rd.rd Int
→ el.el α → Array α.

The sequential composition x := e_{1}; e_{2} is computed by evaluating first e_{1} and then e_{2}. Accordingly, the liability of the whole expression is the sequential composition of the liability l_{1} of e_{1} and the liability l_{2} of e_{2}. Inside e_{2}, variable x is associated with a liability which reflects the normal form of e_{1}, and which is computed by a composition of the function norm with l_{1}.

\begin{aligned}norm u & = & ⊥, & if u ∈ \{rd, wr\} \\ & = & u, & otherwise \end{aligned}

Note that norm is not monotonic. We will therefore have to give proof that the abstract interpretation as a whole is well-defined. Figure 2 details our effect analysis. There are two abstract interpretation functions: L_{D}, which abstracts sets of function definitions to function environments and L, which abstracts expressions to liabilities. The functions take two environments as parameters, one for bound variables and one for functions. We assume that all bound variable names and all function names in a program are distinct from each other.

Notation: The list abstraction [f x | x ← xs] stands for f applied to all elements x of list xs. Reduction of a list with a binary operator such as || or ⊔ is expressed by prefixing the list with the operator. All operators which we use in this context are associative and have an identity element. Reduction of an empty list yields the identity of the reducing operator. The function zip takes two lists and combines corresponding elements in a list of pairs. Mappings from variable names V to some domain D are expressed as follows: The expression x ↦ d denotes the function which maps variable x ∈ V to d ∈ D and which maps all other variables in V to ⊥_{D}. ⊥_{V →D} stands for the function which maps all variables in V to ⊥_{D}. Other mappings can be constructed from these with the operators ⊔ (pointwise upper bound) and ∘ (function composition). f|_{V} denotes the restriction of function f to sub-domain V.

A program is well-formed if its liability maps no bound variable to ⊤:

wf [[e]] = ∀x ∈ BV ar : L [[e]] initfe ⊥_{BEnv} x ≠ ⊤.

The initial bound variable environment maps all variables to ⊥. The initial function environment has been presented above.

Syntactic Domains

x ∈ BV ar  (bound variables)
f ∈ F V ar  (functions)
e ∈ Exp  (expressions)

Semantic Domains

Use = {⊥, rd, id, el, sh, wr, ⊤}
Lia = BV ar → Use × Use (liabilities)
BEnv = BV ar → Lia  (bound variable environments)
F Env = F V ar → Lia^{⋆} → Lia  (function environments)

Interpretation Functions

\begin{aligned}L_{D} & :: & Dcl^{⋆} → F Env → BEnv → F Env \\ L & :: & Exp → F Env → BEnv → Lia \end{aligned}

L_{D} [[dcls]] fe be  = fe′

whererec

fe′  = ⨆[L_{F} d | d ← dcls] ⊔ fe
L_{F} [[f xs = b]] = f ↦ λys. || [L_{B} x : y | (x, y) ← zip xs ys] || L_{B}|_{BV ar\xs}

where

L_{B}  = L [[b]] fe′ be′
be′  = ⨆[x ↦ (x ↦ id.el) | x ← xs] ⊔ be
ys  is a list of fresh variables, s.t. length ys = length xs
L [[e where dcls]] fe be = L [[e]] (L_{D} [[dcls]] fe be) be
L [[x]] fe be  = be [[x]]
L [[f es]] fe be  = (fe [[f]]) [L [[e]] fe be | e ← es]
L [[x := e1 ; e2]] fe be = L [[e1]] fe be ;; L [[e2]] fe be′

where

be′  = (x ↦ ((x ↦ id.el) ⊔ norm ∘ (L [[e1]] fe be))) ⊔ be

L [[if e1 then e2 else e3]] fe be

= L [[e1]] fe be ;; (L [[e2]] fe be ⊔ L [[e3]] fe be)

Figure 2: Effect Analysis

The non-monotonic behavior of norm might raise some doubts whether our abstract interpretation function is well-defined. Indeed, L_{F} fails to be monotonic. This can be seen by considering the expression

E ≡ x := f y ;

cons (upd x 0 0) (upd x 0 0).

If the function environment fe associates f with λl.(id.el : l) (that is, f is typed id.el T_{1} → T_{2}), we have:

L [[E]] fe be = x ↦ ⊤, y ↦ ⊤

On the other hand, assuming L_{F} [[f]] = λl.(wr.el : l), we get:

L [[E]] fe be = x ↦ ⊤, y ↦ wr

Hence, here is an example where fe < fe′ but L [[E]] fe be > L [[E]] fe′ be. Fortunately, the nonmonotonic behavior of L_{F} is restricted to error cases, i.e. situations where both result values contain ⊤. L_{F} can be shown to be monotonic in a setting where all error states of domain Lia are merged into a single element. This suggests that we should work in a lifted liability domain \overline{Lia} whose elements are equivalence classes of liabilities. The equivalence classes are given by:

\begin{aligned}\overline{l} & = & ⊤\overline{Lia}, & if ∃x : l x = ⊤ \\ & = & \{l\}, & otherwise. \end{aligned}

All functions on liabilities are lifted to \overline{Lia} in the obvious way. The lifting is well-defined, as shown by the following reasoning: ⊤\overline{Lia} is the only equivalence class in \overline{Lia} which corresponds to more than one element of Lia. Since all operators on abstract uses preserve ⊤_{Use}, we have that all operators on liabilities map error liabilities to error liabilities. Hence, every lifted function on \overline{Lia} maps ⊤\overline{Lia} to a unique value, namely itself.

Theorem 1 (Monotonicity) In the lifted domain \overline{Lia}, for all e ∈ Exp, be ∈ BEnv, fe, fe′ ∈ F Env:

fe ≤ fe′ ⇒ L_{F} [[e]] fe be ≤ L_{F} [[e]] fe′ be

The proof of Theorem 1 is given in appendix A. From Theorem 1, and and the fact that all domains are finite, Theorem 2 follows.

Theorem 2 (Computability) wf is well-defined and computable.

Example: We compute the liability of function scatter, which updates array a with elements of array b. The update indices come from list xs and are translated by table c.

scatter xs a b c = if xs = [ ] then a else scatter (tl xs)

(upd a (c.(hd xs)) (b.(hd xs))) b c

According to our rule for function definition, the liability l_{scatter} of scatter is:

l_{scatter} =

λ l_{xs} l_{a} l_{b} l_{c}.

(lb xs) : l_{xs} || (lb a) : l_{a} || (lb b) : l_{b} || (lb c) : l_{c}.

The liability lb of the body of scatter is:

lb = xs ↦ rd.rd ;;
( (a ↦ id.el) ⊔
l_{scatter} (xs ↦ rd.sh)
(a ↦ wr.el, b ↦ rd.el,

c ↦ rd.rd, xs ↦ rd.rd)

(b ↦ id.el)
(c ↦ id.el)
).

Substituting the definition of l_{scatter} and rearranging gives:

lb = ( xs ↦ rd.rd ;;
((lb xs) : rd.sh || (lb a) : rd.rd)

a ↦ id.el ⊔ (lb a) : wr.el

b ↦ (lb a) : rd.el || (lb b) : id.el c ↦ (lb a) : rd.rd || (lb c) : id.el )

The least fixpoint of this equation is:

xs ↦ rd.rd, a ↦ wr.el, b ↦ rd.el, c ↦ rd.rd.

Translated into prose, we have that array a is written, that the elements of array b are elements of the result, and that xs and c are read. This describes precisely our intuitive understanding of the function’s effect.

5 Representation

In this section, we discuss the human-readable representation of liabilities and effect signatures. We would expect that liabilities are in general computed automatically, but there are also situations where their representation in human-readable form is required. First, if single-threadedness is violated, the precise cause of the error has to be pinpointed by the compiler. Communication in the other direction is needed if we adopt a module system like Haskell’s [11]. The compilation rules of Haskell are such that the clients of a module may be submitted to compilation before the module itself is completed; the only requirement is that the module’s interface be defined. In the absence of an implementation, the programmer has to define the types and liabilities of all exported entities. Finally, because our technique is a checking algorithm (as opposed to an optimization), programmers have to anticipate the results of the checker, that is they have to reason about liabilities.

We should therefore look for a notation which is as concise and natural as possible. The UseP air domain which we have employed in the last two sections leaves something to be desired in this respect. It is rather large, comprising 6^{2} + 1 states. Some of these states can never be reached. For example, the element-part of a use-pair can never be id, since the element-part stands for elements of differing nesting depths. Generally, the use-pair notation is better suited for automatic effect analysis than for human reasoning.

We have found it useful to employ another representation, in which all use-pairs of interest are given names of their own. We thus have to write just one identifier instead of two but pay the price of a larger Use domain. Table 1 lists the interesting use-pairs together with their descriptive names and example expressions. Every row describes a use value and contains an example in which the variable x is abstracted to this use.

copy is used if an expression’s result contains the elements of a variable, but not the variable itself. select is used if a selection yields an element of a variable. alias and include are used for variables which are identical to the result or an element of it. share stands for any combination of select, alias, and include. Of the various write− values, only write itself is likely to occur often in liabilities. It describes the effect of an update on a variable. writeread and writeshare stand for cases where an updated variable is subsequently discarded; only its elements are read or shared by the result. deepwrite is used for variables whose elements are modified. Figure 3 presents some examples of effect signatures of predefined and user-defined functions.

Name  Pair Example
⊥  ⊥.⊥
read  rd.rd length x
copy  rd.el vec x
select  rd.sh x.i
include  el.el upd a i x
alias  id.el x
share  sh.sh if p then x else tail x
writeread wr.rd length (upd x i y)
write  wr.el upd x i y
writeshare wr.sh (upd x i y).j
deepwrite wr.wr upd (x.j) i y
⊤  ⊤.⊤

Table 1: Interesting use-pairs

upd :: write Array α → read Int → include α

→ Array α

vec :: copy [α] → Array α
cons :: include α → include [α] → [α]
hd :: select [α] → α

swap :: write Array α → read Int → read Int

→ Array α

scatter :: read [α] → write Array α

→ copy Array α → read Array α → Array α

histogram  :: read Int → copy [(Int, α)]

→ Array α

histogram n xs = accum (vec[0 | i ← [0..n − 1]]) xs
accum  :: write Array Int → copy [(Int, α)]

→ Array Int

accum a []  = a

accum a (Cons (i, x) xs)

= y := a.i ; upd a i (x + y)

Figure 3: Example effect signatures

6 Discussion

We have presented a framework which allows us to reason about side-effects in a language which combines functional expressions with destructive array updates. The framework gives us a criterion for programs without observable side-effects.

The two main simplifications of the abstract semantics relative to the standard semantics are:

• functions are black boxes, outside of which nothing is known about execution paths, and

• all elements of a structured value are treated the same.

One might think of relaxing the second simplification by maintaining more information about structure elements, for example by distinguishing elements according to inclusion level. This might be useful for analyzing updates of structure elements. Our current analysis just marks as written the containing variable and all its elements. However, considerably more knowledge is needed for analyzing these “deep updates”. If we update a structure element we usually want to re-link the updated datum into the enclosing structure. In our example language, this would be achieved by something like

upd a i (upd (a.i) j x)

The expression is safe only if all elements of a are distinct (which could be detected by an extension of our analysis along the lines of Wadler’s linear data types [16]), and the two ’i’ indices agree. Since the indices might be arbitrary expressions, a useful analysis must be able to deduce equality of expressions, at least in some restricted cases.

Also desirable would be an extension of effect analysis to higher order functions. One problem in this area is that functional arguments do not always have a most general effect signature. Consider the function declaration

F f g a = cons (upd a i x) (f (g a))

This function is confluent only if a is not “passed through” f ∘ g. That is, either f or g can have an effect signature id.el τ_{1} → τ_{2}, but not both of them. This shows that effect signatures do not possess the principal type property. Therefore, the best information an effect reconstruction algorithm could produce is a set of admissible signatures.

A more pragmatic immediate fix to the problem is also possible: One could require the effect signatures of function valued parameters to be declared. If no declaration is present, unrestricted sharing but no writing could be assumed as a default, in order to stay compatible with the purely functional case. Our existing analysis could then check conformance with the programmersupplied declarations.

Acknowledgements

This work was inspired by a talk of Paul Hudak in which he presented a preliminary version of [9]. It benefitted greatly from subsequent discussions with Paul Hudak and Juan-Carlos Guzmán.

A Monotonicity of the Abstract Interpretation Functions

The appendix contains a proof of Theorem 1, which states that function L_{F} of Figure 2 is monotonic in its function environment argument. From this theorem the computability of our abstract interpretation function L follows.

The main complication in the proof arises from the non-monotonic behavior of function norm. This prevents a simple structural induction over the form of expressions and mandates an analysis of the context in which norm appears.

Theorem 1 (Monotonicity) In the lifted domain \overline{Lia}, for all e ∈ Exp, be ∈ BEnv, fe, fe′ ∈ F Env:

fe ≤ fe′ ⇒ L_{F} [[e]] fe be ≤ L_{F} [[e]] fe′ be

Proof: We first introduce a simplification. Rather than regarding a liability as a mapping from variables to usepairs, we split every variable into two parts, each of which is mapped to a single use. A variable x is split into x_{id} and x_{el}, and, given that the liability l of x is u_{1}.u_{2}, we define l x_{id} = u_{1} and l x_{el} = u_{2}. This is clearly only a notational modification.

The proof proceeds by structural induction on the form of expressions. With the exception of norm, all operators which construct liabilities are monotonic. The only nontrivial case is hence the sequential composition, which looks in our simplified model as follows:

L [[x = e_{1} ; e_{2}]] fe be = L [[e_{1}]] fe be ;; L [[e_{2}]] fe be′ where

be′ = (x ↦ ((x_{id} ↦ id) ⊔ (x_{el} ↦ el)⊔
norm (L [[e_{1}]] fe be))) ⊔ be.

To give names to the parts of these equations, we define:

\begin{aligned}h & = & λl.(x_{id} ↦ id) ⊔ (x_{el} ↦ el) ⊔ norm l, \\ g & = & λl.L [[e_{2}]] fe ((x ↦ l) ⊔ be), \\ f & = & λl. l ;; (g ∘ h) l. \end{aligned}

We have then:

L [[x = e_{1} ; e_{2}]] fe be = f (L [[e_{1}]] fe be).

In the following, we will mostly reason in the original liability domain Lia but will need sometimes also the lifted domain \overline{Lia}. To distinguish both cases, we will overline operators in \overline{Lia}. Our task is to show that \overline{f} is monotonic in its liability argument. i.e:

l_{1} ≤ l_{2} ⇒ \overline{f} l_{1} ≤ \overline{f} l_{2}.  (1)

To show (1), we take a closer look at the possible forms of f, g, and h. Given fixed environments fe and be, all these functions are L-Mappings, i.e. they satisfy Definition 1.

Definition 1 An L-Mapping is a function Φ : Lia → Lia which is of one of the forms (i) − (v).

(i) Φ = id
(ii) Φ = K l′
(iii) Φ = (u :) ∘ Φ_{1}
(iv) Φ = Φ_{1} ⊙ Φ_{2}
(v) Φ = id ;; (Φ_{1} ∘ (Φ_{2} ⊔ norm ∘ Φ_{3}))

Here, u ∈ Use, l′ ∈ Lia, Φ_{1} and Φ_{2} are L-Mappings, and ⊙ is one of ⊔ , || , ;; .

Two useful properties of L-Mappings are:

Lemma 1 For all L-Mappings Φ, x_{1}, x_{2} ∈ BV ar, u_{1}, u_{2} ∈ Use:

(a) Φ ((x_{1} ↦ u_{1}) ⊔ (x_{2} ↦ u_{2})) =
Φ (x_{1} ↦ u_{1}) ⊔ Φ (x_{2} ↦ u_{2})
(b) x_{1} ≠ x_{2} ⇒
Φ (x_{1} ↦ u_{1}) x_{2} = Φ (x_{1} ↦ u_{2}) x_{2}

The proofs of properties (a) and (b) are simple inductions over the form of L-Mappings given in Definition 1. They are left out here since they present no technical difficulties.

Proof of Theorem 1 continued: Because of property (a), we can rewrite f and \overline{f} as follows:

\begin{aligned}f l & = & ⨆_{z∈BV ar} f (z ↦ l z) \\ \overline{f} l & = & \overline{⨆z∈BV ar} \overline{f} (z ↦ l z) \end{aligned}

Hence, \overline{f} is monotononic if we can show that:

∀z ∈ BV ar, u_{1}, u_{2} ∈ Use :  (2)
u_{1} ≤ u_{2} ⇒ \overline{f} (z ↦ u_{1}) ≤ \overline{f} (z ↦ u_{2})

The only non-trivial case in equation (2) is given by u_{1} ∈ {id, el}, u_{2} = wr. This is the only case where function norm shows non-monotonic behavior, namely norm u_{1} = u_{1} and norm u_{2} = ⊥. We have to show that the decrease in norm is “cancelled out” in the whole of \overline{f}, i.e. that the following holds:

\overline{f} (z ↦ id) ≤ \overline{f} (z ↦ wr)  (3)
\overline{f} (z ↦ el) ≤ \overline{f} (z ↦ wr)  (4)

A case analysis is used to show (3).

Case 1: \overline{f} (z ↦ id) ≠ ⊤\overline{Lia}.

In this case, \overline{f} (z ↦ id) = f (z ↦ id)). Let y ∈ BV ar. We have to show that

f (z ↦ id) y ≤ f (z ↦ wr) y.

If y ≠ z, this follows from Lemma 1(b), with “≤” strengthened to “=”. On the other hand, if y = z, we get:

f (y ↦ id) y
≤ (case assumption)
wr
≤ (properties of ;; )
((y ↦ wr) ;; (g ∘ h) (y ↦ wr)) y
= (definition of f)
f (y ↦ wr) y

Case 2: \overline{f} (z ↦ id) = ⊤\overline{Lia}. To show in this case:

\overline{f} (z ↦ wr) = ⊤\overline{Lia}  (5)

From the case assumption follows that there exists y ∈ BV ar such that f (z ↦ id) y = ⊤_{Use}. If y ≠ z, Lemma 1(b) yields f (z ↦ wr) y = ⊤_{Use}, which implies (5). To prove (5) in case y = z, we need inequality (6):

(g ∘ h) (y ↦ wr) y = ⊥ ⇒  (6)

(g ∘ h) (y ↦ id) y ≤ (g ∘ h) (y ↦ id) x_{id}.

The proof of (6) proceeds by structural induction on the definition of the L-Mapping g.

Case 2.2 (i): g = id

(id ∘ h) (y ↦ id) y

= (definition of h)

((x_{id} ↦ id) ⊔ (x_{el} ↦ el) ⊔ (y ↦ id)) y

= (β-reduction)

id

= (β-abstraction)

((x_{id} ↦ id) ⊔ (x_{el} ↦ el) ⊔ (y ↦ id)) x_{id}

= (definition of h)

(id ∘ h) (y ↦ id) x_{id}

Case 2.2 (ii): g = K l′

(K l′ ∘ h) (y ↦ id) y

= (β-reduction)

l′ y

= (β-abstraction)

(K l′ ∘ h) (y ↦ wr) y

= (premise of (6))

⊥

≤ (K l′ ∘ h) (y ↦ id) x_{id}

Case 2.2 (iii): g = (u :) ∘ Φ

((u :) ∘ Φ) (y ↦ id) y

= (β-reduction)

u : (Φ (y ↦ id) y)

≤ (induction hypothesis, monotonicity of ’:’)

u : (Φ (y ↦ id) x_{id})

= (β-abstraction)

((u :) ∘ Φ) (y ↦ id) x_{id}

The proofs of cases (iv) and (v) are like the proof of case (iii) simple induction steps; we leave them out for brevity. This concludes our proof of proposition (6). But (6) implies (5) as shown by the following reasoning:

f (y ↦ id) y = ⊤

⇒ (definition of f)

((y ↦ id) ;; (g ∘ h) (y ↦ id)) y = ⊤

⇒ (properties of ;; )

(g ∘ h) (y ↦ id) y = ⊤

⇒ (6)

(g ∘ h) (y ↦ wr) y ≠ ⊥ ∨ (g ∘ h) (y ↦ id) x_{id} = ⊤

⇒ (properties of ;; , Lemma 1(b))
((y ↦ wr) ;; (g ∘ h) (y ↦ wr)) y = ⊤ ∨
(g ∘ h) (y ↦ wr) x_{id} = ⊤
⇒ (definition of f)
f (y ↦ wr) y = ⊤ ∨ f (y ↦ wr) x_{id} = ⊤
⇒ (definition of \overline{f})
\overline{f} (y ↦ wr) = ⊤\overline{Lia}

This concludes our proof of (3). The proof of (4) differs only in that occurrences of x_{id} are replaced by x_{el}. (3) and (4) together imply (2) and with it the main theorem.

References

[1] A. Bloss. Update analysis and the efficient implementation of functional aggregates. In Proc. 4th Conf. on Functional Programming and Computer Architecture, August 1989.

[2] R. Cytron, J. Ferrante, B.K. Rosen, M.N. Wegman, and F.K. Zadeck. An efficient method for computing static single assignment form. In Proc. 16th ACM Symposium on Principles of Programming Languages, January 1989.

[3] L. Damas and R. Milner. Principal type schemes for functional programs. In Proc. 9th ACM Symposium on Principles of Programming Languages, pp. 207–212, January 1982.

[4] A. Deutsch. On determining lifetime and aliasing of dynamically allocated data in higher-order functional specifications. In Proc. 17th ACM Symposium on Principles of Programming Languages, January 1990.

[5] M. Draghicescu and S. Purushothaman. A compositional analysis of evaluation order and its application. In Proc. ACM Conference on LISP and Functional Programming, June 1990.

[6] W.L. Harrison. The interprocedural analysis and automatic parallelization of Scheme programs. Lisp and Symbolic Computation 2(3/4), October 1989.

[7] K. Gharachorloo, V. Sarkar and J.L. Hennessy. A simple and efficient implementation approach for single assignment languages. In Proc. ACM Conference on LISP and Functional Programming, 1988.

[8] M. Gordon, R. Milner, L. Morris, M. Newey, and C. Wadsworth. A metalanguage for interactive proof in LCF. In Proc. 5th ACM Symposium on Principles of Programming Languages, 1978.

[9] J.C. Guzmán and P. Hudak. Single-threaded polymorphic lambda calculus. In Proc. 5th IEEE Symposium on Logic in Computer Science, June 1990.

[10] P. Hudak. A semantic model of reference counting and its abstraction. In: S. Abramsky and C. Hankin (eds): Abstract interpretation of declarative languages, Ellis Horwood Ltd., 1987.

[11] P. Hudak and P. Wadler (editors). Report on the functional programming language Haskell. Technical Report YALEU/DCS/RR666, Yale University, Department of Computer Science, November 1988.

[12] J.M. Lucassen and D.K. Gifford. Polymorphic effect systems. In Proc. 15th ACM Symposium on Principles of Programming Languages, January 1988.

[13] J. McGraw et al. SISAL: streams and iterators in a single assignment language, language reference manual. Technical Report M–146, LLNL, March 1985.

[14] The Munich project CIP, volume 1: The wide spectrum language CIP/L. Springer Verlag LNCS 183, 1985.

[15] D.A. Schmidt. Denotational semantics as a programming language. Internal report CSR-100, Computer Science Department, University of Edinburgh, 1982.

[16] P. Wadler. Linear types can change the world! Proc. IFIP TC2 Working Conference on Programming Concepts and Methods, April 1990.

[17] P. Wadler. Comprehending monads. In Proc. ACM Conference on LISP and Functional Programming, June 1990.

[18] J.H. Williams and E.L.Wimmers. Sacrificing simplicity for convenience: Where do you draw the line?. In Proc. 15th ACM Symposium on Principles of Programming Languages, January 1988.