nLab
call-by-push-value

Contents

Contents

Idea

Call-by-push-value is a type theory and programming language which contains full embeddings of call-by-value? and call-by-name?, including their operational semantics and equational theories.

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.

Syntax

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).

Shifts

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 ΓpipeB\Gamma \pipe 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.

References

Last revised on November 30, 2018 at 22:30:44. See the history of this page for a list of all contributions to it.