Instead of using call-by-value (CBV), I often use Call-by-push-value (CBPV) in my core calculi, and many people ask me "why?".
Most reasons relate to the "fine-grained" typed structure that it introduces, and the ability of this structure to describe "low-level" concerns, like the difference between partial and full function application (of curried, higher-order functions).
For example, consider this use of function f:
let g = f 1
let x = g 3
let y = g 4
(x, y)
Without effects the above use is the same as, but when effectful, is different from the following:
let x = f 1 3
let y = f 1 4
(x, y)
In the first version, f is partially applied, then applied twice. By contrast, the second version uses two separate (full) applications.
In CBV and CBN, both versions of function f have the same type (e.g.,
int -> int -> int). In fact, in CBV and
call-by-name (CBN), curried functions used for partial application
always have the same type as ones whose applications are all full.
However, in the presence of effects (or any low-level reasoning), we
may want those functions and uses to have different types.
For instance, suppose we were writing a compiler. We'd want to treat (generalized versions of) these situations differently: as compiler designers, we may care about the difference between applying f to one argument, then getting back a function (as a value), versus the second case, of applying both arguments, and never needing to produce an intermediate closure. Likewise, systems programmers care about this distinction too. Beyond caring about the operational cost of creating closures, these audiences may also want to reason precisely about effects, which are also different in the two cases above.
Notably, in call-by-push-value (CBPV), those two versions of function f (for partial vs full application) have different types. CPBV distinguishes value types from computation types in a way that permits us to describe the difference between applying f to one argument, then getting back a function (as a value), vs in the second case, applying both arguments, and never needing to produce a closure value.
Consider these two distinct (value) types for f in CBPV:
f: U(int -> F(U(int -> F(int)))) // type for partial application
f: U(int -> int -> F(int)) // type for full application (only)
To adopt a CPBV typing mindset, we start by assuming that expressions for value terms and computation terms have distinct syntax, with distinct type syntax representing distinct "spaces" of types.
Value types: A, B ::= 1 | 0 | A x B | A + B | U C
Comp types: C, D ::= A -> C | F A | C x D
While these value vs computation type spaces are distinct, they are
closely related: the U connective injects a computation type into
the space of value types. The F connective injects a value type
into the space of computation types. Intuitively, read U C as "a
thunk value whose suspended computation has type C", and read F A
as "a computation that will produce a value of type A".
Returning to our example function f, and its two CBPV types:
The arrow (A -> C) and int types are otherwise standard, though
the former is a computation type (parameterized by a value type
argument A, and a "result" computation type C) and the latter is a
simple base value type.
As the reader may notice, in CBPV, the version for partial application has one additional occurrence of U and of F (each), to describe the production of the partially-applied function -- a thunk value holding the rest of the function. This type reflects the "fine-grained structure" hidden by CBV: The intermediate closure introduced by partial application.
Furthermore, the full application type in CBPV has no analog in CBV: CBV lacks the necessary distinctions to be sensitive to full versus partial applications in the type structure, and to universally enforce the former. Meanwhile, CBPV has exactly that "extra" type structure.
Q: What's the relationship between CBPV and systems languages?
A: As a C/Rust programmer, I think CBPV gives a particularly nice core calculus for describing the typical programming mindset of a systems programmer: aware of where closures are created and used. Systems programmers think about resources at the level of closures; CBPV can be viewed as adding this "extra" distinction to CBV, though it also adds a bit more too (e.g., co-products).
Q: Aren't curried functions in CBPV the same as uncurried functions, whose arguments consist of a single tuple?
A: In many cases, but not generally. CBPV has more computation type connectives than merely arrow. E.g., CBPV has co-products (CBV lacks them), and the mixture of arrow and co-products permits some computation type patterns involving currying that do not exist directly in CBV, and cannot (easily?) be expressed by uncurried applications.
Q: Where can I read more about CBPV?
- The creator (Paul Blain Levy) has a CBPV FAQ
- Example use: Handlers in Action (Kammar et al 2013, ICFP), uses a syntax, type system and operational semantics that follows CBPV
- Papers on Adapton use CBPV.