Asynchronous Effects
University of Ljubljana
Abstract:
In this talk I will tell you about my recent work with Matija Pretnar
on asynchronous programming in the context of algebraic effects. I
will explain how we complement algebraic effects' conventional
synchronous treatment by showing how to naturally also accommodate
asynchrony within them, namely, by decoupling the execution of
operation calls into signalling that an operation's implementation
needs to be executed, and interrupting a running computation with the
operation's result, to which the computation can react by installing
interrupt handlers. I will also show you how we capture these ideas in
a small, type-safe, Agda-formalised core lambda-calculus for
programming with asynchronous effects. This calculus is flexible
enough to accommodate a wide range of examples, ranging from a
multi-party web application, to preemptive multi-threading, to remote
function calls, to a parallel variant of runners of algebraic effects,
to Go-like select statements. I will demo these examples using a
prototype implementation of our core calculus.