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.

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