First-class names for effect handlers
Citations Over TimeTop 21% of 2022 papers
Abstract
Algebraic effects and handlers are a promising technique for incorporating composable computational effects into functional programming languages. Effect handlers enable concisely programming with different effects, but they do not offer a convenient way to program with different instances of the same effect. As a solution to this inconvenience, previous studies have introduced _named effect handlers_, which allow the programmer to distinguish among different effect instances. However, existing formalizations of named handlers are both involved and restrictive, as they employ non-standard mechanisms to prevent the escaping of handler names. In this paper, we propose a simple and flexible design of named handlers. Specifically, we treat handler names as first-class values, and prevent their escaping while staying within the ordinary λ-calculus. Such a design is enabled by combining named handlers with _scoped effects_, a novel variation of effects that maintain a scope via rank-2 polymorphism. We formalize two combinations of named handlers and scoped effects, and implement them in the Koka programming language. We also present practical applications of named handlers, including a neural network and a unification algorithm.
Related Papers
- → Unification Strategies in Cognitive Science(2016)26 cited
- → Separation and Unification of Individuality and Collectivity and Its Application to Explicit Class Structure in Self-Organizing Maps(2012)3 cited
- → Cooperative Unification: Highlights From 1989 To Early 1999(1999)6 cited
- Unification of Asian Economy that Lacks a Unified Institutional Framework(2008)
- The Framework and the Education for the Programmer(2005)