Effect Safety

Unlike Java (with runtime exceptions) or Scala, in Effekt effects are fully tracked by the type system (that is, effect system). For instance, to track printing on the console, we can define a corresponding effect:

interface Console {
  def log(msg: String): Unit
}
def sayHello(): Unit / { Console } =
  do log("Hello World!")

While the left component (that is, Unit) is the type of values returned by sayHello, the right component of the return type (that is, { Console }) describes the set of effects required by sayHello.

Effects are Requirements

As opposed to other effect systems, where effects communicate the side effects a program has besides computing a result, the notion of effects in the Effekt language is that of a requirement.

We thus read the signature of sayHello as

“The function sayhello computes a value of type Unit requiring a capability for Console in its calling context.”

That is, it can only be run in contexts that allow the Console effect.

For instance, we cannot call it in a “pure” function:

def pureFun(): Unit / {} = sayHello()
//                         ^^^^^^^^^^
//                 Unhandled effects { Console }

Here, we put “pure” in quotes since the difference in our notion of effects also leads to a difference of purity compared to existing languages.

Higher-Order Functions and Relative Purity

Functions can take blocks as arguments. An example, we have seen in the introduction is the function map:

import immutable/list

interface Console {
  def log(msg: String): Unit
}

def each[A](l: List[A]) { f: A => Unit }: Unit = <>

The type of the block argument f is A => Unit indicating that it consumes an element of type A. Actually, A => Unit is syntactic sugar for (A) => Unit / {}. That is, it is a block from A to Unit not using any effects visible to a. The implementation of a is omitted, we are using a hole (<>) that allows type-checking, but will result in a runtime error.

Maybe surprisingly, on the callsite to each, we actually can use other effects:

def printList(l: List[Int]): Unit / { Console } =
  each(l) { x => do log(x.show) }

Here, the block passed to each does use another effect, namely the Console effect. That is, only from the point of view of each, the block f is pure.

This shift in perspective, provides guarantees for the caller of each: the implementation cannot observe (besides global side channeling) any effects used by f.

This comes at the cost of some guarantees for the implementor of each: Calling f can have side-effects observable to the user, losing referential transparency to some extent. We cannot simply replace a call to f by its results. Also, calling it twice is different from calling it once.

We will see this in detail when talking about effect polymorphism.