Skip to content

Abstracts.2019.CBPV

Jump to bottom
Fabian edited this page Mar 10, 2020 · 28 revisions

Call-By-Push-Value (CBPV)

Plan

TBD

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