Inprogramming language theory,call-by-push-value (CBPV) is anintermediate language that embeds thecall-by-value (CBV) andcall-by-name (CBN)evaluation strategies. CBPV is structured as a polarizedλ-calculus with two main types, "values" (+) and "computations" (-).^[1] Restrictions on interactions between the two types enforce a controlled order of evaluation, similar tomonads orCPS. 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.^[2][3][4]

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${\displaystyle B}$ is an (arbitrary) value type but${\displaystyle \underset{\_}{B}}$ is a computation type.^[4] Some authors use other conventions, such as distinct sets of letters.^[5]

The exact set of constructs varies by author and desired use for the calculus, but the following constructs are typical:^[2][4]

• Lambdasλx.M are computations of type${\displaystyle A\to \underset{\_}{B}}$, where${\displaystyle x:A}$ and${\displaystyle M:\underset{\_}{B}}$. A lambda applicationF V orV'F is a computation of type${\displaystyle \underset{\_}{B}}$, where${\displaystyle V:A}$ and${\displaystyle F:A\to \underset{\_}{B}}$. The let-binding constructlet { x_1 = V_1; ... }. M binds valuesx_1 to valuesV_1, of matching types${\displaystyle A_1}$, inside a computationM :${\displaystyle \underset{\_}{B}}$.
• A thunkthunk M is a value of type${\displaystyle U\underset{\_}{A}}$ constructed from a computationM of type${\displaystyle \underset{\_}{A}}$. Forcing a thunk is a computation,force X :${\displaystyle \underset{\_}{A}}$ for a thunkX :${\displaystyle U\underset{\_}{A}}$.
• It is also possible to wrap a valueV of type${\displaystyle A}$ as a computationreturn V :${\displaystyle FA}$. Such a computation can be used inside another computation asM to x. N :${\displaystyle \underset{\_}{B}}$, whereM :${\displaystyle FA}$, andN :${\displaystyle \underset{\_}{B}}$ is a computation.
• Values can also includealgebraic data types constructed from a tag and zero or more sub-values, while computations include a deconstructing pattern-matchmatch V as { (1,...) in M_1, ... }. Depending on presentation, ADTs may be limited to binary sums and products, Booleans only, or be omitted altogether.

A program is a closed computation of type${\displaystyle FA}$, where${\displaystyle A}$ is a ground ADT type.^[4]

Expressions such asnot true : bool make sense denotationally. But, following the rules above,not can only be encoded using pattern-matching, which would make it a computation, and therefore the overall expression must also be a computation, givingnot true : F bool. Similarly, there is no way to obtain1 from(1,2) without constructing a computation. When modelling CBPV in the equational orcategory theory, such constructs are indispensable. Levy therefore defines an extended IR, "CBPV with complex values". This IR extends let-binding to bind values within a value expression, and also to pattern-match a value with each clause returning a value expression.^[3] Besides modelling, such constructs also make writing programs in CBPV more natural.^[2]

Complex values complicate the operational semantics, in particular requiring an arbitrary decision of when to evaluate the complex value. Such a decision has no semantic significance because evaluating complex values has no side effects. Also, it is possible to syntactically convert any computation or closed expression to one of the same type and denotation without complex values.^[3] Therefore, many presentations omit complex values.^[4]

The CBV translation produces CBPV values for each expression. A CBV functionλx.M :${\displaystyle A{\to }_{v}B}$ is translated tothunk λx.Mv :${\displaystyle U(A^v\to F{B}^v)}$. A CBV applicationM N :${\displaystyle A}$ is translated to a computationMv to f in Nv to x in x'(force f) of type${\displaystyle FA}$, making the order of evaluation explicit. A pattern matchmatch V as { (1,...) in M_1, ... } is translated asVv to z in match z as { (1,...) in M_1v, ... }. Values are wrapped withreturn when necessary, but otherwise remain unmodified.^[2] In some translations, sequencing may be required, such as translatinginl M toM to x. return inl x.^[4]

The CBN translation produces CBPV computations for each expression. A CBN functionλx.M :${\displaystyle A\to B}$ translates unaltered,λx.MN :${\displaystyle (U{A}^n)\to X^n}$. A CBN applicationM N :${\displaystyle C}$ is translated to a computationMv (thunk Nv) of type${\displaystyle C^n}$. A pattern matchmatch V as { (1,...) in M_1, ... } is translated similarly to CBN asVn to z in match z as { (1,...) in M_1n, ... }. ADT values are wrapped withreturn, butforce andthunk are also necessary on internal structure. Levy's translation assumes thatM = force (thunk M), which does indeed hold.^[2]

It is also possible to extend CBPV to model call-by-need, by introducing aM need x. N construct that allows visible sharing. This construct has semantics similar toM name x. N = (λy.N[x ↦ (force y)])(thunk M), except that with theneed construct, the thunk ofM is evaluated at most once.^[6]

Some authors have noted that CBPV can be simplified, by removing either the U type constructor (thunks)^[7] or the F type constructor (computations returning values).^[8] 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.^[7] Ehrhard in contrast omits the F type constructor, making values a subset of computations. Ehrhard renames computations to "general types" to better reflect their semantics. This modified calculus, the "half-polarized lambda calculus", has close connections to linear logic.^[8][9] It can be translated bidirectionally to a subset of a fully-polarized variant of CBPV.^[10]

• Programming Computable Functions

• Lambda calculus
• Programming language semantics

• Articles with short description
• Short description matches Wikidata