Syntax Overview - lrytz/efftp GitHub Wiki

In general, effect annotations have to be placed on return types:

def inc(i: Int): Int @pure = i + 1

• Effects are inferred only if the return type is also inferred:

def inc(i: Int) = i + 1         // effect is inferred

• If the return type is specified, but no effect annotation is present, the system assumes the largest possible effect (the unknown effect):

def inc(I: Int): Int = i + 1    // impure!

Constructors

Note: the information in this section might change, see #9.

Constructor definitions don't have a return type. Constructor effect annotations are therefore placed on the class (for the primary constructor) or on the constructor method definition (for auxiliary ones):

@pure
class C {
  @io def this(x: Int) = {
    this()
    println(x)
  }
}

Some effect annotations however need to refer to this or to one of the constructor parameters. In the above solution the parameters are not in scope. This issue is overcome by an alternative syntax for constructor effect annotations:

class C(x: Int) {
  @mod(this) type constructorEffect

  def this(x: Int, y: Int) = {
    this(x + y)
    @mod(this) type constructorEffect = Nothing
  }
}

The effect type definition for the primary constructor can appear anywhere in the template. For the secondary constructor, the type definition needs to appear right after the self constructor invocation.

Note that the effect of a primary constructor consists of multiple components:

• Statements in the class body
• Field initialization expressions, including early definitions
• The superclass constructor invocation
• For every other parent, the effect of the trait initializer

Function Types

Note: the information in this section might change, see #11.

Effect annotations only have a meaning if the appear on return types of methods (with a few exceptions listed on this page). A function type A => B is syntactic sugar for Function1[A,B], so both A and B are type arguments, and not return types of a method.

Therefore, effects of function types have to be annotated using a type refinement:

val pureFun: (Int => Int) { def apply(x: Int): Int @pure } = {
  (x: Int) => x + 1
}

Note that effect annotations within refinements are checked by the compiler:

val pureFun: (Int => Int) { def apply(x: Int): Int @pure } = {
  (x: Int) => { println(x); x + 1 }
}

produces a type error.

Default Arguments

For every default argument, the Scala compiler creates a metod which returns the value for that default. To annotate the effect of these methods, the programmer has to provide an effect annotation on the parameter which has a default value:

def f(x: Int, y: Int @pure = 1) = x + y
def g: Int @pure = f(10)

Without the effect annotation on the parameter type of y, the invocation f(10) would not type check as pure.

Annotating multiple Effect Domains

When multiple effect domains are active, the annotations can simply be combined:

def inc(x: Int): Int @noIo @throws[Nothing] = x + 1

For every effect domain which is not annotated, the system will assume the topmost (unknown) effect.

The special @pure annotation marks a method as pure across all effect domains:

def inc(x: Int): Int @pure = x + 1     // no io, no exceptions, no state modified

In order to allow effects only in some specific domains and enforce purity in all others, @pure can be mixed with annotations from other domains. The following function may throw an exception, but is pure in all other effect domains:

def div(x: Int, y: Int): Int @pure @throws[DivByZeroException] = ...

Effect Ascriptions and Effect Casts

Effects are usually only checked at method definitions with explicit effect annotations. Using an annotation ascription allows checking the effects of arbitrary sub-expressions:

def f(x: Int) = {
  println(x)
  (x + 1): @pure
}

In some situations it is necessary to override effect checking with a cast. This can be done by adding the @unchecked annotation to an effect ascription:

def f(it: Iterator): Unit @pure = {
  if (!it.hasNext) ()
  else {
    val e = it.next(): @unchecked @pure   // it.next() cannot throw an exception
    handle(e)                             // here, we know it has a `next`
  }
}

The @unchecked annotation can also be added to an effect declaration on the return type of a method, in which case the effect of that method is not checked at all.