论文标题
异步效应
Asynchronous Effects
论文作者
论文摘要
我们探索具有代数效应的异步编程。我们通过展示如何自然地适应它们内部的异步方法来补充他们的常规同步处理，即，通过将执行操作呼叫的执行脱钩到信号中，表明操作的实现需要执行，并通过操作结果中断运行的计算，而计算可以通过安装Internrect Handlers做出反应。我们将这些想法形式化在一个小的核心微积分中，称为$λ_ {\ text {ae}} $。我们使用从多方Web应用程序到远程多线程，到远程函数调用，到代数效应的跑步者的平行变体。此外，该论文还伴随着$λ_ {\ text {ae}} $的类型安全证明的形式化，以及OCAML中$λ_{\ text {ae}} $的原型实现。
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, called $λ_{\text{ae}}$. We demonstrate the flexibility of $λ_{\text{ae}}$ using 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. In addition, the paper is accompanied by a formalisation of $λ_{\text{ae}}$'s type safety proofs in Agda, and a prototype implementation of $λ_{\text{ae}}$ in OCaml.
