Purity - lrytz/efftp GitHub Wiki

The purity effect domain checks methods for purity with respect to state modifications. It can be enabled using the compiler option -P:effects:domains:purity.

Purity and Observable Effects

We start by defining what it means for a method to be pure.

The effect system is based on the fact that side-effects on state which is allocated within a method cannot be observed from the outside. For clients invoking such a method, the state that is accessible by the client does not change by executing the method.

This directly leads to our definition of purity: a method is pure if it does not modify any state that existed before its execution.

We distinguish between two kinds of state modifications that a method might perform:

Updates of fields of objects
Assignments to local variables that are either allocated within the method itself, or in the body of an outer method

Modification Effects (Field Updates)

If a method only modifies fields of objects that are freshly allocated within the method body, then those effects cannot be observed from the outside.

As an example we take a method length which returns the number of elements in a list:

class Counter {
  private var x = 0
  def inc(): Unit @mod(this) = {
    x = x + 1
  }
  def get: Int @pure = x
}

def length[T](l: List[T]): Int @pure = {
  val c = new Counter()
  for (_ <- l) { c.inc() }
  c.x
}

Since method length only modifies a freshly allocated counter, it can safely be annotated as @pure.

On a high level, the effect system needs the following pieces of information to determine that method length has no observable effects:

The method inc only modifies the fields of its receiver object, explained just next
The constructor of class Counter returns a freshly allocated object and does not create any aliases to it, explained below in Returned Locality
The for loop has the effect of its body, see Relative Effects

Modification Effect Annotations

The @mod effect annotation restricts field updates to specific objects:

@mod() denotes purity, the absence of observable effects.
@mod(this, a, b) denotes the effect of a method which can modify fields of the this, a and b.
@mod(any) denotes the largest effect (the unknown effect). It is also used for methods that modify global state (fields of source-level objects).

Valid arguments for the @mod annotation are: the receiver this, the parameters of the method, and local variables of outer methods. Method inc in class Counter above is an example with effect @mod(this). The following example illustrates the other cases:

def doInc(c: Counter): Unit @mod(c) = c.inc()     // modifies an argument

def outer: Int @pure = {
  val c = new Counter()
  def inner(): Unit @mod(c) = c.inc()             // modifies a local variable
  inner()                                         // of an outer method
  c.get
}

object t { var x = 1 }
def incGlobal(): Unit @mod(any) = t.x = t.x + 1   // modifies global state

class D {
  private val c: Counter = new Counter()
  def incC(): Unit @mod(any) = this.c.inc()       // modifies the fields of some counter
}                                                 // that might be aliased

We will re-visit the last example later in Section Ownership and Locality.

Freshness and Returned Locality

In the original example, method length can be considered pure because the counter c is known to be a freshly allocated object. The @loc annotations is used to denote the locality (or freshness) of the object returned by a method (or constructor):

@loc() denotes methods that return a fresh object on every invocation
@loc(this, a, b) denotes methods that return an object from the locality of this, a, or b. Localities are explained in the next section Ownership and Locality.
@loc(any) denotes methods that return objects of unknown locality.

Note that the default result locality for methods annotated @pure is @loc(any): by default, a pure method can return any object. Freshness has to be annotated explicitly (it is inferred for methods without return type).

The following example illustrates common uses of the result locality annotation:

def counterFactory(): Counter @loc() = new Counter     // returns a fresh, non-aliased
                                                       // object on every invocation
object t { var c: Counter = ... }
def globalCounter(): Counter @loc(any) = t.c           // returns a global object

def inc(c: Counter): Counter @mod(c) @loc(c) = {       // returns an object of
  c.inc()                                              // locality `c`
  c
}

In the system described so far, the only object with locality @loc(c) would be c itself. The concept of locality is however more general, as explained in the next section.

Ownership and Locality

The system outlines so far fails to express purity of one common programming pattern: if an object uses private, local state which is not shared with any other object, then modifications to that state cannot be observed outside that object.

The following example illustrates this observation:

class D {
  @local private val c: Counter = new Counter()
  def incC(): Unit @mod(this) = this.c.inc()       // modifies an object owned by `this`
  def getC: Int @pure = this.c.get
}

Every instance of class D has its own counter which is not aliased from the outside.

The @local annotation on field c specifies that the field is owned by class D. The effect annotation @mod(this) allows to modify to the fields of this, plus all objects reachable through fields which are annotated @local.

The ultimate goal of the purity effect system is to show that certain methods have no observable state effects. The next example shows how an object of type D can be used within a pure method:

def countSome(): Int @pure = {
  val d = new D()
  d.incC()
  d.getC
}

This method is pure because d is a freshly allocated object which itself has a freshly allocated counter. Modifications of that counter can therefore not be observed from the outside.

In order for this system to be sound, the system ensures that no aliases are created to objects which are stored in @local fields. More precisely, the system maintains the following invariant.

Locality Invariant: An object can only be considered fresh if all objects reachable through @local fields are also fresh.

The Builder class of the Scala collections library is a real world example which requires locality annotations. It has the following interface:

trait Builder[-Elem, +To] {
  def add(e: Elem): Unit @mod(this)
  def result(): To @pure
}

A typical implementation might use an array to store the appended elements:

class ABuilder[-Elem, +To] extends Builder[Elem, To] {
  @local private val buf: Array[Elem] = ...
  def add(e: Elem): Unit @mod(this) = ...
  ...
}

The implementation of add updates the array. Since the builder owns the array (field buf is @local), this effect is allowed by the effect annotation @mod(this).

Assignments Effects (Assignments to Local Variables)

Assignments to local variables allocated within a method can be masked: the state of these variables cannot be observed by a client which calls the method.

As an example we look at an alternative implementation for the method length:

def length[T](l: List[T]): Int @pure = {
  var c = 0
  var ls = l
  while (ls != Nil) {
    c = c + 1
    ls = (ls.tail: @unchecked @pure) // cast to hide @throws[NoSuchElem]. can
  }                                  // not happen, `ls` is non-empty here
  c
}

Since this method does not have any observable effect it can safely be annotated @pure.

For nested methods that modify local variables of their outer method, the assignment effects are annotated using @assign:

@assign() denotes methods that have no assignment effects. Note that top-level methods never have an assignment effect: there are no local variables defined in an outer scope that they could modify.
@assign(x, loc) denotes the effect of assigning to variable x an object of locality loc.
@assign(any) denotes methods with an unknown assignment effect.

The following example shows a nested method which assigns to an outer local variable:

def outer: Int @pure { 
  var i = 0
  def inc(): Unit @assign(i, any) = { i = i + 1 }
  inc()
  i
}

Note that integers always have locality any, so the assignment effect annotation states that inc assigns to variable i a value with locality any.

Interaction with Modification Effects

Object modification effects can be mixed with assignments to local variables:

def incSmaller(a: Counter, b: Counter): Unit @mod(a, b) = {
  var c = a
  if (b.get < a.get) c = b
  c.inc()
}

The body of method incSmaller has effect @assign(c, a) @assign(c, b) @mod(c). Since the local variable c is out of scope at the method interface, effects on c have to be replaced replaced by the corresponding localities. The resulting effect is @mod(a, b).