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

reversible derivation (Section 2.3.4)

a derivation

Γ, Δ1 ⊢ A1 ⋯ Γ, Δn ⊢ An
-----------------------
        Γ, Δ ⊢ C

such that there are operations

• Θ : Tm(Γ, Δ₁;A₁) × ⋯ × Tm(Γ, Δ_n;A_n) → Tm(Γ, Δ;C)
• Θ' : Tm(Γ, Δ;C) → Tm(Γ, Δ₁;A₁) × ⋯ × Tm(Γ, Δ_n;A_n)

which are

1. natural in Γ
2. mutually inverse

with respect to the equational theory (for instance,

 Γ, A ⊢ B      Γ ⊢ A  Γ ⊢ B       Γ, A, B ⊢ C      Γ, A ⊢ C  Γ, B ⊢ C
--------- →I   ------------ ×I   ------------ ×E   ------------------ +E
Γ ⊢ A → B        Γ ⊢ A × B       Γ, A × B ⊢ C         Γ, A + B ⊢ C

are reversible derivations while the derivations

Γ ⊢ A  Γ ⊢ A → B        Γ ⊢ A           Γ ⊢ B
---------------- →E   --------- +Il   --------- +Ir
      Γ ⊢ B           Γ ⊢ A + B       Γ ⊢ A + B

are not reversible)

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".
4. Eugenio Moggi. 1991. "Notions of Computation and Monads".
5. Andrzej Filinski. 1996. "Controlling Effects".