Skip to content

Abstracts.2019.CBPV

Jump to bottom
Fabian edited this page Oct 6, 2020 · 28 revisions

Call-By-Push-Value (CBPV)

Plan

In this session we will jointly read about the Call-By-Push-Value (CBPV) language. What is CBPV? To quote from Paul Levy's book [1]:

Call-by-push-value is a programming language paradigm that, surprisingly, breaks down the call-by-value and call-by-name paradigms into simple primitives.

The aim of the session is to understand CBPV, its motivation and why it "subsumes" operationally and denotationally call-by-value and call-by-name lambda calculus with effects.

To that matter, we will try to cover the following sections of Paul Levy's thesis [1]:

  • Chapter 1: Introduction
    • Only Section 1.5 but not 1.5.4
  • Chapter 2: Call-By-Value and Call-By-Name
    • Everything except Subsections 2.3.4, 2.6.3, 2.6.4, 2.6.5 and 2.7.5
  • Chapter 3: Call-By-Push-Value: A Subsuming Paradigm
    • Sections 3.1, 3.2, 3.3.1, 3.5, 3.6 and 3.7

Ideally, everybody will have read and tried to understand the selected material in order to improve the discussion during the session.

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.

Inside a ground CBN term, the only way to cause a subterm of type A → B to be evaluated is to apply it.

Definitions

value type (Section 1.5.4)
a type of the form U B, ∑i ∈ I Ai, 𝟏, or A × A for some computation type B, set of tags I, value types A
computation type (Section 1.5.4)
a type of the form F A, ∏i ∈ I Bi, or A → B for some value type A, set of tags I, computation types B
η-law for booleans in the simply typed λ-calculus (Section 2.3.3)
the equation Γ ⊢ M[N/z] = if N then M[true/z] else M[false/z] for Γ, z : bool ⊢ M : A and Γ ⊢ N : bool
reversible derivation (Section 2.3.4)
a derivation 
Γ, Δ1 ⊢ A1 ⋯ Γ, Δn ⊢ An
-----------------------
        Γ, Δ ⊢ C

such that there are operations

  • Θ : Tm(Γ, Δ1;A1) × ⋯ × Tm(Γ, Δn;An) → Tm(Γ, Δ;C)
  • Θ' : Tm(Γ, Δ;C) → Tm(Γ, Δ1;A1) × ⋯ × Tm(Γ, Δn;An)

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)

context (Definition 3, Definition 5)
a closed term C[] with zero or more occurrences of a hole []
ground context (Definition 3, Definition 5, Definition 20)
  • a context C[] of ground type (for CBV)
  • a context C[] of ground type (for CBN)
  • a context C[] of ground producer type (for CBPV)
observational equivalence (Definition 4, Definition 6, Definition 20)
the relation M ≃ M' on terms M, M' in terms of a notion of observations m, terminal terms T, and evaluation M⇓(m,T)
  • ∀ ground contexts C[], observations m, terminal terms T. C[M]⇓(m,T) ⇔ C[M']⇓(m,T) (at ground types)
  • ∀ contexts C[], observations m. (∃ terminal term T. C[M]⇓(m,T)) ⇔ (∃ terminal term T'. C[M']⇓(m,T')) (at all types)
ground type (Definition 14)
a type of the form ∑i ∈ I 𝟏 for some set of tags I (such as bool = 𝟏 + 𝟏)
producer type (Definition 14)
a type of the form F A for some value type A
complex value (Section 4.2)
a term of the form let x be V. W, pm V as { …, (i,x). Wi, … }, or pm V as (x,y). W where the W are values, that is a term pattern-matching into values (as opposed to computations; not allowed by basic CBPV)
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".
Clone this wiki locally