Content area

Abstract

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.

Details

1009240
Title
Higher-Order Asynchronous Effects
Publication title
arXiv.org; Ithaca
Publication year
2024
Publication date
Sep 20, 2024
Section
Computer Science
Publisher
Cornell University Library, arXiv.org
Source
arXiv.org
Place of publication
Ithaca
Country of publication
United States
University/institution
Cornell University Library arXiv.org
e-ISSN
2331-8422
Source type
Working Paper
Language of publication
English
Document type
Working Paper
Publication history
 
 
Online publication date
2024-09-25
Milestone dates
2023-07-25 (Submission v1); 2024-02-07 (Submission v2); 2024-06-27 (Submission v3); 2024-09-20 (Submission v4)
Publication history
 
 
   First posting date
25 Sep 2024
ProQuest document ID
2842691053
Document URL
https://www.proquest.com/working-papers/higher-order-asynchronous-effects/docview/2842691053/se-2?accountid=208611
Full text outside of ProQuest
Copyright
© 2024. This work is published under http://creativecommons.org/licenses/by/4.0/ (the “License”). Notwithstanding the ProQuest Terms and Conditions, you may use this content in accordance with the terms of the License.
Last updated
2024-09-26
Database
ProQuest One Academic