Effects and coeffects in call-by-push-value (extended version)

authors: Cassia Torczon, Emmanuel Suárez Acevedo, Shubh Agrawal, Joey Velez-Ginorio, Stephanie Weirich
year: 2023
url: http://arxiv.org/abs/2311.11795
publisher:
abstract: Effect and coeffect tracking are a useful way to integrate many types of compile-time analysis, such as cost, liveness or dataflow, into a language's type system. However, their interactions with call-by-push-value (CBPV), a computational model useful in compilation for its isolation of effects and its ability to encompass both call-by-name and call-by-value computations, are still poorly understood. We present fundamental results about those interactions, in particular effect and coeffect soundness. The former asserts that our CBPV-with-effects system accurately predicts the effects that the program may trigger during execution, and the latter asserts that our CBPV-with-coeffects system accurately tracks the demands a program makes on its environment. We prove our results for a core CBPV calculus and maintain generality across a broad range of effects and coeffects, laying the groundwork for future investigation.