nLab call-by-push-value



Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels





Call-by-push-value is a type theory and programming language paradigm which has full embeddings of call-by-value? and call-by-name? lambda-calculi, including their operational semantics, equational theories? and denotational models.

Its semantics decomposes the semantics of effectful languages using a strong monad into a strong adjunction?. Then the embeddings of call-by-value and call-by-name correspond to the construction of Kleisli and co-Kleisli categories from an adjunction.


Judgmental Structure

CBPV has two “kinds” of types: value types — written A,A,A iA,A',A_i — and computation types — written B,B,B iB,B',B_i. As originally presented. there are 3 term judgments of CBPV: Values, Terms, and Stacks.

The value judgment is an ordinary simple type theory. A context Γ\Gamma is a sequence of value typed variables x 1:A 1,x_1:A_1,\ldots and the judgment ΓV:A\Gamma \vdash V : A admits symmetry, contraction, weakening and the corresponding substitution principle: if for every x i:A ix_i:A_i in Γ\Gamma, Γγ(x i):A i\Gamma' \vdash \gamma(x_i) : A_i, then there is a value ΓV[γ]:A\Gamma' \vdash V[\gamma] : A.

The term judgment has again a value typed context Γ\Gamma, but the output type is a computation type ΓM:B\Gamma \vdash M : B. Again it admits symmetry, contraction and weakening, and admits a substitution principle on its inputs, if we have a γ\gamma as above, then there is a term ΓM[γ]:B\Gamma' \vdash M[\gamma] : B.

Finally the stack judgment has a value context Γ\Gamma as input, but also a computation type as input and output: Γ|BS:B\Gamma | B \vdash S : B'. Stacks have an admissible substitution operation S[γ]S[\gamma] as above. Stacks also have a composition operation: if Γ|BS:B\Gamma | B \vdash S : B' and Γ|BS:B\Gamma | B' \vdash S' : B'' then Γ|BS[S]:B\Gamma | B \vdash S'[S] : B'', which is associative and has a unit: the empty stack Γ|B:B\Gamma | B \vdash \bullet : B. Finally, stacks have an action on terms: if ΓM:B\Gamma \vdash M : B and Γ|BS:B\Gamma | B \vdash S : B' then ΓS[M]:B\Gamma \vdash S[M] : B', which is associative with \bullet as identity.

We can get a slightly simpler presentation by combining the stack and term judgments into a single term judgment with a stoup?: a context that is either a single type BB or empty. Then a term as before is a term typed with the empty stoup and a stack is a term typed with a full stoup. This has the benefit of combining the action of stacks on terms and the composition of stacks as one operation. Below we write a stoup as Δ\Delta, and if it is empty we don’t write it at all.

Type Structure

Call-by-push-value is characterized not just by its judgmental structure, but by a specific choice of which connectives to use. Except for the shifts F,UF,U, all value type connectives are left adjoints, and all computation type connectives are right adjoints.

For this reason, some connectives are definable from the judgments but excluded because they violate this discipline. These are a tensor product ABA \otimes B which is a computation type, a unit II computation type, and a linear function space BBB \multimap B' which is a computation type. When these are added, the system is called the Enriched Effect Calculus (modulo some superficial syntactic differences).


The shift types express the adjunction between values and stacks. The type UBUB is a value type that is pronounced as “thunk of BB”, and can be thought of as the type of closures that when called behave as BB. It is a value type, but a right adjoint, with invertible introduction rule

ΓM:BΓthunkM:UB \frac { \Gamma \vdash M : B } { \Gamma \vdash thunk M : UB }

and elimination rule:

ΓV:UBΓforceV:B \frac { \Gamma \vdash V : UB } { \Gamma \vdash force V : B }

With β\beta rule forcethunkM=Mforce thunk M = M and η\eta rule V=thunkforceVV = thunk force V.

The type FAFA is a computation type that is the type of “returners of AAs”. It is a computation type, but a left adjoint, with invertible elimination rule that enables the sequencing of effects:

Γ|ΔM:FAΓ,x:AN:BΓ|ΔMtox.N:B \frac { \Gamma | \Delta \vdash M : F A \qquad \Gamma, x : A \vdash N : B} { \Gamma | \Delta \vdash M to x. N : B }

with introduction rule:

ΓV:AΓreturnV:FA \frac {\Gamma \vdash V : A } { \Gamma \vdash return V : F A }

with β\beta rule (returnV)tox.N=N[V/x](return V) to x. N = N[V/x] and η\eta rule that for any stack Γ|FAS:B\Gamma | F A \vdash S : B, we have S=tox.S[returnx]S = \bullet to x. S[return x].

As an Adjoint Logic

The semantics of Call-by-push-value was originally presented using fibred categories, but we can get a presentation of its semantics in a more multi-categorical flavor by expressing it as an adjoint logic from a specific mode theory in the sense of LSR.

As a summary, the mode theory of CBPV is the theory of a cartesian monoid acting on a pointed object. In more detail, we have two modes: vv for values and cc for computations. Then the vv mode is axiomatized as a cartesian monoid (v,×,1)(v,\times,1), which gives the value judgment. To axiomatize the term and stack judgments, we add an asymmetric tensor product

a:v,b:cab:ca:v,b:c \vdash a\otimes b : c

to represent the combined context Γ|B\Gamma | B and also a “point” for the computation types:

i:c\vdash i : c

which represents the empty stoup.

To correctly model the substitution structure, we add equations that say that the tensor product constitutes an action of the monoid, i.e., associativity and unitality:

(a×a)b=a(ab)1b=b(a \times a') \otimes b = a \otimes (a' \otimes b) \qquad 1 \otimes b = b

Then for example, the FF type above is F xiF_{x \otimes i} and the UU type is U x.xiU_{x. x \otimes i}.

Furthermore, the mode theory also gives the “missing” types of the Enriched Effect Calculus. The tensor product is F xyF_{x \otimes y}, the unit is F iF_{i} and the linear function space is U x.xyU_{x. x\otimes y}.

Note that this mode theory is equivalent to the one given for a strong monad in LSR, which instead of the point ii adds a morphism a:vg(a):ca : v \vdash g(a) : c, and requires this be a homomorphism of vv-actions in that

g(a×b)=ag(b) g(a \times b) = a \otimes g(b)

However, this is equivalent to our above presentation because for any a:va:v, we have a=a×1a = a \times 1, so g(a)=g(a×1)=ag(1)g(a) = g(a \times 1) = a\otimes g(1), so gg is completely determined by where it takes 11, so we can axiomatize that directly as the point ii.

  • The linear term judgment in linear-non-linear logic can be seen as extending the call-by-push-value stack judgment to allow for “multi-hole” stacks.


Last revised on February 11, 2023 at 14:47:08. See the history of this page for a list of all contributions to it.