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 of Moggi and Filinski into an adjunction.

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 = 𝟏 + 𝟏)

Bibliography

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