WG211/M23Weirich

Effect and coeffect tracking are a useful way to integrate many forms 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 also show that the standard translations from call-by-value and call-by-name languages are type and effect/coeffect preserving.