Effekt Language

The Effekt language comes with support for effect handlers (also known as algebraic effects).

Effects Generalize Exceptions

Effect handlers are exception handlers on steroids! Like with exceptions, we first define the type of the exception. In Effekt, a declaration like yield is called an effect signature.

Calling an effect operation (with do yield(42)) is like throwing an exception. It transfers the control-flow to the handler that catches (or "handles") the effect. We can also send values to the handler (here n).

effect yield(n: Int): Bool

def example() = {
  var produce = true;
  var n = 0;
  while (produce) {
    produce = do yield(n)
    n = n + 1
  }
  println("done")
}

Effect Handlers Can Resume

So what's new? Effect handlers now can also resume the program that called the effect!

In our example, we handle the yield effect by printing the number that was sent. Similar to generators, we also resume at the original call to yield!

Our example is type-safe: By declaring yield to take an integer and return a boolean, at the handler we know that we receive integers and have to call resume with a boolean value.

try { example() } with yield { n =>
  println(n); resume(n < 3)
}

Effect handlers are great, but it is easy to forget handling an effect. This is why the Effekt language comes with a static effect system that tells you where you forgot to handle something.

Effects are Part of the Type

The example uses a raise effect to signal that something went wrong. This can be seen in the return type of divide:

//      effect set
//       vvvvvvvvv
   Int / { raise }
// ^^^
// return type

The type says that divide will produce an integer, but it also requires raise to be handled at the call-site! We use curly braces to say that it is a set of effects.

effect raise(msg: String): Unit

def divide(n: Int, m: Int): Int / { raise } =
  if (m == 0) {
    do raise("Cannot divide by zero"); 0
  } else {
    n / m
  }

Effects are Checked

Trying to define a function like typeError that claims it requires no effects leads to a static type error!

Tip. Click "edit" to observe the type error and try to fix it by deleting the type annotated on typeError. Hover over typeError to inspect the inferred type.

def typeError(): Int / {} = divide(4, 0)
//                          ^^^^^^^^^^^^
//                 Unhandled effects: raise

Handling Effects

Only programs that do not have any effects left can be executed.

We can for instance handle the raise effect by printing the message and returning 42 as default value.

try { divide(4, 0)} with raise { msg =>
  println(msg); 42
}

Tracking effects statically in the type is a great way to achieve safety. However, often, as soon as you start writing higher-order functions the type- and effect system starts to get into your way.

Not so in Effekt! It features a new form of effect polymorphism, which we call contextual effect polymorphism.

Effect Polymorphism

A (higher-order) function is effect polymorphic, if it can be used with different argument functions, independent on the effects those argument functions use.

Maybe one of the most famous higher-order functions is map on lists. We can invoke map with different argument functions (called blocks in Effekt).

In our examples, we call the same map function with different blocks that (a) do not use effects, (b) use built-in effects (println), (c) use user-defined effects (raise).

You can notice that the last example cannot be run, since it still has unhandled effects raise.

  import list
  

[1, 2, 3].map { x => x * 2 }

[1, 2, 3].map { x => println(x) }

[1, 2, 3].map { x => if (x > 2) do raise("") else () }

Contextual Effect Polymorphism

In Effekt, the function map has the signature:

//          value argument  block argument
//            vvvvvvvvvv  vvvvvvvvvvvvvvvvvv
def map[A, B](l: List[A]) { f: A => B / {} }: List[B] / {}
//                                      ^^              ^^
//                                   no effects!     no effects!

The function map takes a value argument l and what we call a block argument f. For programmers familiar with effect-systems / effect polymorphism, this signature might come with a surprise: Neither the block argument, nor the overall result type mention any effects!

In Effekt, we read the signature of map as follows:

"Given a list and a block f, map cannot handle any effects of f. Also map itself does not require handling of any effects."

If block arguments, however, do use effects, those have to be handled at the call-site:

try {
  [1, 2, 3, 4].map { x => println(x); if (x > 2) do raise("abort") else () }
  println("done")
} with raise { msg => println("abort") }

Here, the block uses the raise effect, which is handled at the call-site of map.