Call-by-Push-Value with Algebraic Effects and Handlers
S.A. Dimakos (TU Delft - Electrical Engineering, Mathematics and Computer Science)
Casper Bach Bach Poulsen – Mentor (TU Delft - Programming Languages)
J.S. Reinders – Mentor (TU Delft - Programming Languages)
Annibale Panichella – Graduation committee member (TU Delft - Software Engineering)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
Addressing the challenge of reasoning about programs across different evaluation strategies has long been a concern in functional programming. Levy's introduction of the call-by-push-value (CBPV) calculus represents a significant step forward in tackling this. His paradigm provided a more powerful approach that can encapsulate both call-by-value and call-by-name that was even later extended to include call-by-need. In this paper we present the development of an interface that integrates the theory of CBPV with algebraic effects and handlers. We demonstrate how this technique enables the definition and execution of programs, highlighting its capability to defer computations across different evaluation strategies and define operations in a modular fashion. We then define and prove a set of laws that can be used with our interface to reason about programs under varying evaluation regimes. This approach not only enhances the flexibility and modularity of language and library implementation but also allows for direct reasoning about these implementations, beyond the meta-level abstraction.