| Autor: |
BOSMAN, ROGER, VAN DEN BERG, BIRTHE, WENHAO TANG, SCHRIJVERS, TOM |
| Předmět: |
|
| Zdroj: |
Logical Methods in Computer Science (LMCS); 2024, Vol. 20 Issue 4, p17:1-17:50, 50p |
| Abstrakt: |
Algebraic effects & handlers have become a standard approach for side-effects in functional programming. Their modular composition between different effects and clean separation of syntax and semantics make them attractive to a wide audience. However, not all effects can be classified as algebraic; some need a more sophisticated handling. In particular, effects that have or create a delimited scope need special care, as their continuation consists of two parts--in and out of the scope--and their modular composition introduces additional complexity. These effects are called scoped and have gained attention by their growing applicability and adoption in popular libraries. While calculi have been designed with algebraic effects & handlers built in to facilitate their use, a calculus that supports scoped effects & handlers in a similar manner does not yet exist. This work fills this gap: we present λsc, a calculus with native support for both algebraic and scoped effects & handlers. The most novel part of λsc is the support for modular composition of different scoped effects & handlers by extending handlers with forwarding clauses, which make λsc much more expressive than existing calculi with algebraic effects & handlers. Our calculus is based on Eff, an existing calculus for algebraic effects, extended with Koka-style row polymorphism, and consists of a formal grammar, operational semantics, and a (type-safe) type-and-effect system. We give a prototype implementation of λsc with type inference and demonstrate λsc on a range of examples. [ABSTRACT FROM AUTHOR] |
| Databáze: |
Complementary Index |
| Externí odkaz: |
|
