A Calculus for Scoped Effects Handlers
arXiv (Cornell University)(2023)
摘要
Algebraic effects handlers have become a standard approach for side-effects
in functional programming. Their modular composition with other 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
λ_𝑠𝑐, a calculus with native support for both algebraic and
scoped effects handlers. It addresses the need for polymorphic handlers and
explicit clauses for forwarding unknown scoped operations to other 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, a (type-safe) type-and-effect system and type inference.
We demonstrate λ_𝑠𝑐 on a range of examples.
更多查看译文
关键词
scoped effects
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要