Lightweight Effect Polymorphism

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.

Effect Polymorphism

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

import immutable/list

effect Break(): Unit

type File = List[String]
def eachLine(file: File) { f: String => Unit / {} }: Unit / {} =
  file.foreach { line => f(line) }

val someFile = ["first line", "second line", "", "third line"]
def printLines(file: File) = try {
    eachLine(file) { line =>
      if (line == "") { do Break() }
      else { println(line) }
    }
  } with Break {
    println("found an empty line, aborting!")
  }

The higher-order function eachLine expects two arguments: firstly, a value argument, which is passed in parenthesis. Secondly, a block argument, which is passed in curly braces. It calls the provided block with each line in the file.

The signature of eachLine in Effekt is:

def eachLine(file: File) { f: String => Unit / {} }: Unit / {}

Note that the signature does not say anything about effects.

The Traditional Reading

In traditional effect systems, this would be read is:

“given a block f that has no effects, eachLine also has no effects”.

Given that reading, we couldn’t use eachLine as in our example, since the block passed to eachLine uses two effects Break and Console (due to println).

The Contextual Reading

In Effekt, we apply a different reading, which we call contextual:

“given a block f without any further requirements, eachLine does not require any effects.”

The function eachLine is effect polymorphic. We can call it with arbitrary blocks, indepedent of the effects the block arguments use.

The type ofthe block parameter f tells us that it does not impose any requirements on its caller within eachLine. However, it can have effects, that simply need to be handled at the call-site of eachLine.

Contextual Effect Polymorphism by Example

Here are some examples of calling eachLine. For example, we can provide a block that does not use any effects:

eachLine(someFile) { line => () }

The type of the block is String => Unit / {} and the overall type of the call is Unit / {}.

Further, we can provide a block that uses builtin effects (Console):

eachLine(someFile) { line => println(line) }

The type of the block is String => Unit / { Console } and the overall type of the call now becomes Unit / { Console }.

We can also provide a block that uses a user-defined effects:

eachLine(someFile) { line => do Break() }

The type of the block is String => Unit / { Break } and the overall type of the call is Unit / { Break }. Since it still has unhandled user effects, it does not type-check and we cannot run it.

To be able to run it, we handle the user-effect at the call-site to eachLine:

try {
  eachLine(someFile) { line => do Break() }
} with Break { println("nothing to see here") }

Now, the effects that are used by the block argument are handled in its lexical scope.