We explore asynchronous programming with algebraic effects. We complement their 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. We formalise these ideas in a small core calculus and demonstrate its flexibility using examples ranging from a multi-party web application, to pre-emptive multi-threading, to (cancellable) remote function calls, to a parallel variant of runners of algebraic effects. In addition, the paper is accompanied by a formalisation of the calculus's type safety proofs in Agda, and a prototype implementation in OCaml.

翻译：我们探索了基于代数效应的异步编程。通过将操作调用的执行解耦为信号通知操作实现需要被执行，以及用操作结果中断正在进行的计算（计算可通过安装中断处理器对此作出反应），我们在传统同步处理方式基础上，展示了如何自然地在其内部容纳异步性。我们在一个小型核心演算中形式化了这些思想，并通过从多方Web应用到抢占式多线程、从（可取消的）远程函数调用到代数效应运行器的并行变体等示例，展示了其灵活性。此外，本文附带了在Agda中实现的该演算类型安全证明的形式化，以及在OCaml中实现的原型系统。