Call-by-push-value

The CBPV paradigm is based on the slogan "a value is, a computation does". One complication in the presentation is distinguishing type variables ranging over value types from those ranging over computation types. This article follows Levy in using underlines to denote computations, so $B$ is an (arbitrary) value type but $\backslash underline\{B\}$ is a computation type. Some authors use other conventions, such as distinct sets of letters.{{cite journal |last1=Pédrot |first1=Pierre-Marie |last2=Tabareau |first2=Nicolas |title=The fire triangle: how to mix substitution, dependent elimination, and effects |journal=Proceedings of the ACM on Programming Languages |date=January 2020 |volume=4 |issue=POPL |pages=1–28 |doi=10.1145/3371126}}

The exact set of constructs varies by author and desired use for the calculus, but the following constructs are typical:

• Lambdas λx.M are computations of type $A\; \backslash to\; \backslash underline\{B\}$, where $x\; :\; A$ and $M\; :\; \backslash underline\{B\}$. A lambda application F V or V'F is a computation of type $\backslash underline\{B\}$, where $V\; :\; A$ and $F\; :\; A\; \backslash to\; \backslash underline\{B\}$. The let-binding construct let { x_1 = V_1; ... }. M binds values x_1 to values V_1, of matching types $A\_1$, inside a computation M : $\backslash underline\{B\}$.
• A thunk thunk M is a value of type $U\; \backslash underline\{A\}$ constructed from a computation M of type $\backslash underline\{A\}$. Forcing a thunk is a computation, force X : $\backslash underline\{A\}$ for a thunk X : $U\; \backslash underline\{A\}$.
• It is also possible to wrap a value V of type $A$ as a computation return V : $F\; A$. Such a computation can be used inside another computation as M to x. N : $\backslash underline\{B\}$, where M : $F\; A$, and N : $\backslash underline\{B\}$ is a computation.
• Values can also include algebraic data types constructed from a tag and zero or more sub-values, while computations include a deconstructing pattern-match match V as { (1,...) in M_1, ... }. Depending on presentation, ADTs may be limited to binary sums and products, Booleans only, or be omitted altogether.

A program is a closed computation of type $F\; A$, where $A$ is a ground ADT type.

Expressions such as not true : bool make sense denotationally. But, following the rules above, not can only be encoded using pattern-matching, which would make it a computation, and therefore the overall expression must also be a computation, giving not true : F bool. Similarly, there is no way to obtain 1 from (1,2) without constructing a computation. When modelling CBPV in the equational or category theory, such constructs are indispensable. Levy therefore defines an extended IR, "CBPV with complex values". This IR extends let-binding to bind values within a value expression, and also to pattern-match a value with each clause returning a value expression. Besides modelling, such constructs also make writing programs in CBPV more natural.

Complex values complicate the operational semantics, in particular requiring an arbitrary decision of when to evaluate the complex value. Such a decision has no semantic significance because evaluating complex values has no side effects. Also, it is possible to syntactically convert any computation or closed expression to one of the same type and denotation without complex values. Therefore, many presentations omit complex values.

The CBV translation produces CBPV values for each expression. A CBV function λx.M : $A\; \backslash to\_v\; B$ is translated to thunk λx.Mv : $U\; (A^v\; \backslash to\; F\; B^v)$. A CBV application M N : $A$ is translated to a computation Mv to f in Nv to x in x'(force f) of type $F\; A$, making the order of evaluation explicit. A pattern match match V as { (1,...) in M_1, ... } is translated as Vv to z in match z as { (1,...) in M_1v, ... }. Values are wrapped with return when necessary, but otherwise remain unmodified. In some translations, sequencing may be required, such as translating inl M to M to x. return inl x.

The CBN translation produces CBPV computations for each expression. A CBN function λx.M : $A\; \backslash to\; B$ translates unaltered, λx.MN : $(U\; A^n)\; \backslash to\; X^n$. A CBN application M N : $C$ is translated to a computation Mv (thunk Nv) of type $C^n$. A pattern match match V as { (1,...) in M_1, ... } is translated similarly to CBN as Vn to z in match z as { (1,...) in M_1n, ... }. ADT values are wrapped with return, but force and thunk are also necessary on internal structure. Levy's translation assumes that M = force (thunk M), which does indeed hold.

It is also possible to extend CBPV to model call-by-need, by introducing a M need x. N construct that allows visible sharing. This construct has semantics similar to M name x. N = (λy.N[x ↦ (force y)])(thunk M), except that with the need construct, the thunk of M is evaluated at most once.{{cite book |last1=McDermott |first1=Dylan |last2=Mycroft |first2=Alan |chapter=Extended Call-by-Push-Value: Reasoning About Effectful Programs and Evaluation Order |title=Programming Languages and Systems |date=2019 |pages=235–262 |doi=10.1007/978-3-030-17184-1_9 |isbn=978-3-030-17184-1 |publisher=Springer International Publishing |language=en}}

Some authors have noted that CBPV can be simplified, by removing either the U type constructor (thunks){{cite journal |last1=Egger |first1=J. |last2=Mogelberg |first2=R. E. |last3=Simpson |first3=A. |title=The enriched effect calculus: syntax and semantics |journal=Journal of Logic and Computation |date=1 June 2014 |volume=24 |issue=3 |pages=615–654 |doi=10.1093/logcom/exs025 |url=https://www.pure.ed.ac.uk/ws/portalfiles/portal/12289301/eec.pdf}} or the F type constructor (computations returning values).{{cite book |last1=Ehrhard |first1=Thomas |chapter=Call-By-Push-Value from a Linear Logic Point of View |title=Programming Languages and Systems |series=Lecture Notes in Computer Science |date=2016 |volume=9632 |pages=202–228 |doi=10.1007/978-3-662-49498-1_9|doi-access=free|isbn=978-3-662-49497-4 }} Egger and Mogelberg justify omitting U on the grounds of streamlined syntax and avoiding the clutter of inferable conversions from computations to values. This choice makes computation types a subset of value types, and it is then natural to expand function types to a full function space between values. They term their calculus the "Enriched Effects Calculus". This modified calculus is equivalent to a superset of CBPV via a bidirectional semantics-preserving translation. Ehrhard in contrast omits the F type constructor, making values a subset of computations. Ehrhard renames computations to "general types" to better reflect their semantics. This modified calculus, the "half-polarized lambda calculus", has close connections to linear logic.{{cite book |last1=Chouquet |first1=Jules |last2=Tasson |first2=Christine |title=Taylor expansion for Call-By-Push-Value |date=2020 |publisher=Schloss Dagstuhl – Leibniz-Zentrum für Informatik |series=Leibniz International Proceedings in Informatics |volume=152 |pages=16:1–16:16 |doi=10.4230/LIPIcs.CSL.2020.16 |doi-access=free |isbn=978-3-95977-132-0 |url=https://hal.science/hal-02318600/document}} It can be translated bidirectionally to a subset of a fully-polarized variant of CBPV.{{citation |last1=Ehrhard |first1=Thomas |title=A Call-By-Push-Value FPC and its interpretation in Linear Logic |date=July 2015 |url=https://hal.science/hal-01176033/document}}

• Programming Computable Functions

{{reflist}}

Category:Lambda calculus

Category:Programming language semantics