A good object-oriented effects system gives the ability to define abstract regions (or "data groups") of state within objects that can be extended in subclasses. Then one can specify (for instance) read and write effects on these abstract regions. Additionally, effects on "wholly owned subsidiary" objects should be seen as effects on regions of the owning object. For instance, an assignment within a bucket of a hash table should be seen as an effect on the hash table alone. Correctness of this transfer of effects depends on the bucket being accessible only through the hash table; it must be unique.

Uniqueness can be guaranteed using destructive reads (in which a unique variable can be used at most once). Destructive reads are inconvenient, so most uniqueness systems permit borrowing reads as well, in which a temporary alias of a unique variable is permitted. But if the unique variable is read during the lifetime of this alias, the uniqueness invariant fails. So we wish to ensure that this read eect does not happen. For modularity reasons, we use effects annotations on methods to check for such read effects.

Thus we see that effects and uniqueness depend on each other. Our position is that the use of annotations breaks the cyclic dependence as long as the annotations are given semantics independent of the analyses. As a semantics of uniqueness annotations is already available, we then sketch a semantics of eects annotations independent of uniqueness. Thus decoupled, one can prove the correctness of a uniqueness analysis and an effects analysis without regard for the other.