In programming language theory, call-by-push-value (CBPV) is an intermediate language that embeds the call-by-value (CBV) and call-by-name (CBN) evaluation strategies. CBPV is structured as a polarized λ-calculus with two main types, "values" (+) and "computations" (-). Restrictions on interactions between the two types enforce a controlled order of evaluation, similar to monads or CPS. The calculus can embed computational effects, such as nontermination, mutable state, or nondeterminism. There are natural semantics-preserving translations from CBV and CBN into CBPV. This means that giving a CBPV semantics and proving its properties implicitly establishes CBV and CBN semantics and properties as well. Paul Blain Levy formulated and developed CBPV in several papers and his doctoral thesis.
Definition
The CBPV paradigm is based on the slogan "a value is, a computation does". One complication in the presentation is distinguishing type variables ranging over value types from those ranging over computation types. This article follows Levy in using underlines to denote computations, so <math>B</math> is an (arbitrary) value type but <math>\underline{B}</math> is a computation type.
The exact set of constructs varies by author and desired use for the calculus, but the following constructs are typical:
Modifications
Some authors have noted that CBPV can be simplified, by removing either the U type constructor (thunks) or the F type constructor (computations returning values). Egger and Mogelberg justify omitting U on the grounds of streamlined syntax and avoiding the clutter of inferable conversions from computations to values. This choice makes computation types a subset of value types, and it is then natural to expand function types to a full function space between values. They term their calculus the "Enriched Effects Calculus". This modified calculus is equivalent to a superset of CBPV via a bidirectional semantics-preserving translation. It can be translated bidirectionally to a subset of a fully-polarized variant of CBPV.
Award
Paul Blain Levy received the 2025 Alonzo Church Award for his work on CBPV.
See also
- Programming Computable Functions