Abstracts.2019.CBPV

Call-By-Push-Value (CBPV)

Example

The program

print "hello0";
let x be 3.
let y {- : U (nat → F nat) -} be thunk (print "hello1";
                                        λz.                      -- "pop z"
                                        print "we just popped"z;
                                        produce x+z).
print "hello2";
(print "hello3";
 7'                                                              -- "push 7"
 print "we just pushed 7";
 force y) to w.                                                  -- "... >>= λw. ..."
print "w is bound to"w;
produce w+5                                                      -- "return $ w+5"

of type F nat outputs

hello0
hello2
hello3
we just pushed 7
hello1
we just popped 7
w is bound to 10

(see Section 1.5.2 for the example program, Section 3.2 and Figure 3.1 for the syntax of basic/effect-free CBPV, Section 3.4 for the extended syntax of printing CBPV)

Discussion

A value is, a computation does.

CBPV decomposes the monad T of Moggi and Filinski into an adjunction F ⊣ U.

The belief that the categorical semantics of functionspace in call-by-name are easy is a consequence of a longstanding bias (going back to Church) towards functionspace, at the expense of other connectives. Try formulating a categorical semantics for sum type in call-by-name. [..] The perception of CBN's mathematical superiority (CBN satisfies the η-law for functions) is actually due to the fact that function types have been considered more important, and hence received more attention, than sum types (CBN does not satisfy the η-law for booleans) or even ground types.

Definitions

ground type (Definition 14)

a type of the form ∑_{i ∈ I} 𝟏 for some set of tags I (such as bool = 𝟏 + 𝟏)

functor representation (Definition 61)

an object V : 𝒞 (the "vertex") together with a family of bijections 𝒞(V,X) ≅ F(X) natural in X : 𝒞 for a set-valued functor F : 𝒞 → 𝐒𝐞𝐭

oblique morphism (Definition 110)

an element g ∈ O(X,Y) of a set-valued functor O : ℬ^op × 𝒟 → 𝐒𝐞𝐭 such that all functors of the form O(-,Y) : ℬ^op → 𝐒𝐞𝐭 for some Y : 𝒟 and O(X,-) : 𝒟 → 𝐒𝐞𝐭 for some X : ℬ are representable (corresponding to an adjunction from ℬ to 𝒟 given by the two representations)

Notes

Parametrized Representability (Proposition 95)

Let H : 𝒞 × 𝒟 → 𝐒𝐞𝐭 be a set-valued functor such that for each X : 𝒞 the set-valued functor H(X,-) : 𝒟 → 𝐒𝐞𝐭 has a representation F(X) : 𝒟, n(X) : 𝒟(F(X),-) ≅ H(X,-), then F extends uniquely to a functor from 𝒞 to 𝒟^op so as to make n a natural isomorphism between 𝒟(F(-),-) and H.

Bibliography

1. Paul Blain Levy. 2001. "Call-By-Push-Value". FAQ, course notes, tutorial slides, book.
2. Paul Blain Levy. 2006. "Call-By-Push-Value: Decomposing Call-By-Value and Call-By-Name".
3. Andreas Abel and Christian Sattler. 2019. "Normalization by Evaluation for Call-by-Push-Value and Polarized Lambda-Calculus".