Call-by-Push-Value

Origin. Paul Blain Levy, "Call-by-push-value: a subsuming paradigm" (TLCA 1999, Springer LNCS 1581, pp. 228–242), developed through his thesis (Queen Mary, University of London, 2001) into the book Call-By-Push-Value: A Functional/Imperative Synthesis (Springer, Semantic Structures in Computation, 2003); the journal statement of the subsumption is "Call-by-push-value: decomposing call-by-value and call-by-name" (Higher-Order and Symbolic Computation 19(4), 2006, pp. 377–414). The adjoint decomposition has a precedent in Nick Benton's mixed linear/non-linear logic LNL (CSL 1994), which split linear logic's ! into an adjunction; Levy's calculus does the same to the monad of Moggi's "Notions of computation and monads" (Information and Computation, 1991).

Models. A calculus with two kinds of type, under Levy's slogan "a value is, a computation does": value types classify data, computation types classify behaviour, and two shifts connect the kinds — F A, the computations that return a value of type A, and U B̲, the values that hold a suspended computation of type B̲. Call-by-value and call-by-name stop being rival languages and become two translations into this one, each a pattern of where the shifts fall. The decomposition is the point: Moggi's monad T is not primitive but the composite U F of an adjunction, and the finer structure is what a semantics of effects actually uses.

Formalism.

Types: value types A ::= U B̲ | ∑{i∈I} Aᵢ | 1 | A × A computation types B̲ ::= F A | A → B̲ | ∏{i∈I} B̲ᵢ (index sets finite or countable; underlining marks computation types)

Judgments: Γ ⊢ᵛ V : A for values, Γ ⊢ᶜ M : B̲ for computations; Γ holds value hypotheses only.

The shifts:

Γ ⊢ᵛ V : A ─────────────────── F-intro Γ ⊢ᶜ return V : F A

Γ ⊢ᶜ M : F A Γ, x : A ⊢ᶜ N : B̲ ───────────────────────────────── F-elim Γ ⊢ᶜ M to x. N : B̲

Γ ⊢ᶜ M : B̲ ──────────────────── U-intro Γ ⊢ᵛ thunk M : U B̲

Γ ⊢ᵛ V : U B̲ ──────────────────── U-elim Γ ⊢ᶜ force V : B̲

Reduction: force (thunk M) ⇝ M (return V) to x. N ⇝ N[V/x] (λx.M) V ⇝ M[V/x]

Functions: λx.M : A → B̲ is a computation; an application pushes its operand before the body runs. A → B̲ is a computation type because a function does something when applied.

Subsuming translations: call-by-value: (A → B)ᵛ = U(Aᵛ → F Bᵛ); a CBV term of type B becomes a computation of type F Bᵛ call-by-name: (A → B)ⁿ = U Aⁿ → Bⁿ; a CBN type becomes a computation type, and variables bind thunks Both preserve observable behaviour, and the standard CBV and CBN semantics factor through them.

Stack semantics: The CK-machine runs a pair ⟨M, K⟩ of a computation and a stack: application pushes an operand, λ pops one, M to x. N pushes the frame to x. N, return V pops it. Stacks are typed from one computation type to another and, in the models, denote algebra homomorphisms.

Adjunction semantics: A model is a value category and a computation category with a strong adjunction F ⊣ U, plus the products, sums and exponentials the types demand, with no coherence conditions (Levy, "Adjunction models for call-by-push-value with stacks", CTCS 2002; Theory and Applications of Categories 14(5), 2005, pp. 75–110). U F is Moggi's monad on values; the call-by-value translation lands in the Kleisli part of the adjunction and the call-by-name translation in the co-Kleisli part; computation types denote algebras in the Eilenberg–Moore semantics.

Polarization: Value types are the positives, computation types the negatives, and U and F are the shifts ↓ and ↑ — a focused proof is a CBPV typing derivation (Polarized Logic, Focusing).

Symbols.

Symbol	Unicode	Name	Meaning
⊣	U+22A3	Left tack / Adjoint	The adjunction F ⊣ U
⊢	U+22A2	Turnstile	Typing judgment
ᵛ	U+1D5B	Modifier letter small v	Marks the value judgment
ᶜ	U+1D9C	Modifier letter small c	Marks the computation judgment
→	U+2192	Rightwards arrow	The computation-type function space
×	U+00D7	Multiplication sign	Product of value types
∑	U+2211	N-ary summation	Sum of value types
∏	U+220F	N-ary product	Product of computation types
∈	U+2208	Element of	Indexes the branches of sums and products
ᵢ	U+1D62	Subscript small i	Branch index
↑	U+2191	Upwards arrow	Polarized logic's name for F
↓	U+2193	Downwards arrow	Polarized logic's name for U
λ	U+03BB	Greek small lamda	Computation-level abstraction
Γ	U+0393	Greek capital gamma	Context of value hypotheses
⇝	U+21DD	Rightwards squiggle arrow	Reduction
⟨	U+27E8	Left angle bracket	Opens a CK-machine configuration
⟩	U+27E9	Right angle bracket	Closes it
F	—	Returner shift	F A: computations returning a value of type A; the left adjoint
U	—	Thunk shift	U B̲: values holding a suspended computation; the right adjoint
T	—	The monad	T = U F, Moggi's monad on value types
A	—	Value metavariable	Ranges over value types
B̲	—	Underlined metavariable	Ranges over computation types
1	—	Unit type	Nullary product of value types
thunk, force	—	U intro and elim	Freeze and unfreeze a computation
return, to	—	F intro and elim	Return a value; sequence on a returned value
K	—	Stack	The CK-machine's evaluation context
::=	—	Grammar production	Defines the two type grammars

Metatheory. The subsumption is a theorem: Levy (1999; 2003) proves that the call-by-value and call-by-name translations preserve operational behaviour and that the known denotational semantics of each — for divergence, state, control, printing — factor through CBPV's, so one calculus carries the semantics previously built twice. The adjunction analysis sharpens Moggi: every monad arises from an adjunction, but the monadic metalanguage sees only the composite U F, while CBPV's syntax names the two halves, and the choice the monad leaves open — which resolution to compute in, with Kleisli initial and Eilenberg–Moore terminal (Monads) — is settled by the stack judgment, since stacks denote homomorphisms and force the algebra reading of computation types. The algebraic-effects account enters at the same place: an effect operation acts on every computation type because every computation type is an algebra, and a handler is a homomorphism out of a free one (Algebraic Effects). Under Curry–Howard the calculus is the term assignment of focused intuitionistic logic, the inversion and focus phases matching the two judgments; Focusing and Polarized Logic record the same structure from the proof-search and LC sides.

Applies to. The working metalanguage of effect semantics: monadic, adjunction-based and algebraic accounts of effects are stated over its value/computation split (Monads, Algebraic Effects). Compiler intermediate representations that separate data from control. The Curry–Howard face of focusing and polarization (Focusing, Polarized Logic). Adjoint and modal type theories, which generalize the U–F pattern to other adjunctions (Modal Type Theory). Semantics of call-by-value and call-by-name languages by translation. Dependent and graded extensions of effect typing.

Limitations. Call-by-need is not subsumed: forcing a thunk twice runs its computation twice and nothing in the calculus memoizes, so lazy evaluation with sharing needs an extension rather than a translation. Complex values — value terms built by case analysis on sums — complicate the equational theory, and Levy's development handles them with separate machinery. The calculus is intuitionistic: there are terms and stacks but no symmetric coterm syntax, so classical control is handled indirectly — Levy's treatment routes it through the separate Jump-With-Argument calculus — and the fully symmetric picture belongs to the polarized sequent calculi descended from λ̄μμ̃ (Lambda-Mu Calculus). And the fine grain is syntactic overhead: thunk, force, return and to make even effect-free programs more verbose than their λ-calculus originals, which is why CBPV serves as metalanguage and intermediate representation rather than surface language.