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 => () }
interface Console {
def log(msg: String): Unit
}
def runExample[R] { prog: () => R / Console }: R =
try { prog() } with Console { def log(msg) = resume(println(msg)) }
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 the effect Console
from the previous section:
runExample { eachLine(someFile) { line => do log(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.