Call-by-push-value: Difference between revisions

Revision as of 13:25, 8 April 2024

Revision as of 20:08, 8 April 2024

Line 1:

{{Redirects here|CBPV|the virus that affects bees|Chronic bee paralysis virus}}

{{technical|date=December 2014}}

In [[programming language theory]], Call-by-Push-Value (CBPV) is an [[intermediate language]] that embeds the [[call-by-value]] (CBV) and [[call-by-name]] (CBV) [[evaluation strategy|evaluation strategies]]. CBPV is structured as a polarized [[λ-calculus]] with two main types, "values" (+) and "computations" (-).<ref name="Kavvos2020">{{cite journal |last1=Kavvos |first1=G. A. |last2=Morehouse |first2=Edward |last3=Licata |first3=Daniel R. |last4=Danner |first4=Norman |title=Recurrence extraction for functional programs through call-by-push-value |journal=Proceedings of the ACM on Programming Languages |date=January 2020 |volume=4 |issue=POPL |pages=1–31 |doi=10.1145/3371083 |url=https://dl.acm.org/doi/pdf/10.1145/3371083 |language=en |issn=2475-1421}}</ref> Restrictions on interactions between the two types enforce a controlled order of evaluation, similar to [[Monad (functional programming)|monad]]s or [[continuation passing style|CPS]]. The calculus can embed computational effects, such as nontermination, mutable state, or nondeterminism. There are natural semantics-preserving translations from CBV and CBN into CBPV. This means that giving a CBPV semantics and proving its properties implicitly establishes CBV and CBN semantics and properties as well. Paul Blain Levy formulated and developed CBPV in several papers and his doctoral thesis.<ref name="Levy99">{{Cite conference |last=Blain Levy |first=Paul |date=April 1999 |title=Call-by-Push-Value: A Subsuming Paradigm |conference=Typed Lambda Calculi and Applications, 4th International Conference, TLCA'99, L'Aquila, Italy |series=Lecture Notes in Computer Science |volume=1581 |pages=228–242|url=https://www.cs.bham.ac.uk/~pbl/papers/tlca99.pdf|title=Call-by-Push-Value: A Subsuming Paradigm}}</ref><ref name="Levy2003">{{cite book |last1=Levy |first1=Paul Blain |title=Call-by-push-value: a functional/imperative synthesis |date=2003 |publisher=Kluwer Academic Publishers |___location=Dordrecht ; Boston |isbn=978-1-4020-1730-8|url=https://www.cs.bham.ac.uk/~pbl/papers/thesisqmwphd.pdf}}</ref><ref name="Levy2022">{{cite journal |last1=Levy |first1=Paul Blain |title=Call-by-push-value |journal=ACM SIGLOG News |date=April 2022 |volume=9 |issue=2 |pages=7–29 |doi=10.1145/3537668.3537670}}</ref>

In [[programming language theory]], the '''call-by-push-value''' ('''CBPV''') paradigm,<ref>{{cite journal|url=https://www.cs.bham.ac.uk/~pbl/papers/tlca99.pdf|title=Call-by-Push-Value: A Subsuming Paradigm|author=Paul Blain Levy}}</ref> inspired by [[Monad (functional programming)|monads]], allows writing semantics for [[Lambda calculus|lambda-calculus]] without writing two variants to deal with the difference between '''[[call-by-name]]''' and '''[[Call by value|call-by-value]]'''. To do so, CBPV introduces a term language that distinguishes computations and values, according to the slogan ''a value is, a computation does''; this term language has a single evaluation order. However, to evaluate a [[lambda-calculus]] term according to either the call-by-name ('''CBN''') or call-by-value ('''CBV''') [[Reduction strategy (lambda calculus)|reduction strategy]], one can translate the term to CBPV using a call-by-name or call-by-value translation strategy, which give rise to different terms. Evaluating the result of the call-by-value translation corresponds to evaluating the original term with the call-by-value strategy; evaluating the result of the call-by-name translation corresponds instead to evaluating the original term with the call-by-name strategy.

== Definition ==

This is especially useful when dealing with the semantics of different side effects, such as nontermination, mutable state or nondeterminism. Instead of giving two variants of the semantics, one for the call-by-name evaluation order and one for the call-by-value one, one can simply give a semantics for the CBPV term language; one gets two semantics for lambda-calculus by composing this CBPV semantics with the same CBV and CBN translations from lambda-calculus.

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 <math>B</math> is an (arbitrary) value type but <math>\underline{B}</math> is a computation type.<ref name="Levy2022"/> Some authors use other conventions, such as distinct sets of letters.<ref>{{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}}</ref>

The exact set of constructs varies by author and desired use for the calculus, but the following constructs are typical:<ref name="Levy99"/><ref name="Levy2022"/>

* Lambdas <code>λx.M</code> are computations of type <math>A \to \underline{B}</math>, where <math>x : A</math> and <math>M : \underline{B}</math>. A lambda application <code>F V</code> or <code>V'F</code> is a computation of type <math>\underline{B}</math>, where <math>V : A</math> and <math>F : A \to \underline{B}</math>. The let-binding construct <code>let { x_1 = V_1; ... }. M</code> binds values <code>x_1</code> to values <code>V_1</code>, of matching types <math>A_1</math>, inside a computation <code>M</code> : <math>\underline{B}</math>.

* A thunk <code>thunk M</code> is a value of type <math>U \underline{A}</math> constructed from a computation <code>M</code> of type <math>\underline{A}</math>. Forcing a thunk is a computation, <code>force X</code> : <math>\underline{A}</math> for a thunk <code>X</code> : <math>U \underline{A}</math>.

* It is also possible to wrap a value <code>V</code> of type <math>A</math> as a computation <code>return V</code> : <math>F A</math>. Such a computation can be used inside another computation as <code>M to x. N</code> : <math>\underline{B}</math>, where <code>M</code> : <math>F A</math>, and <code>N</code> : <math>\underline{B}</math> is a computation.

* Values can also include [[algebraic data type]]s constructed from a tag and zero or more sub-values, while computations include a deconstructing pattern-match <code>match V as { (1,...) in M_1, ... }</code>. 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 <math>F A</math>, where <math>A</math> is a ground ADT type.<ref name="Levy2022"/>

=== Complex values ===

Expressions such as <code>not true : bool</code> make sense denotationally. But, following the rules above, <code>not</code> can only be encoded using pattern-matching, which would make it a computation, and therefore the overall expression must also be a computation, giving <code>not true : F bool</code>. Similarly, there is no way to obtain <code>1</code> from <code>(1,2)</code> 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.<ref name="Levy2003"/> Besides modelling, such constructs also make writing programs in CBPV more natural.<ref name="Levy99"/>

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.<ref name="Levy2003"/> Therefore, many presentations omit complex values.<ref name="Levy2022"/>

== Translation ==

The CBV translation produces CBPV values for each expression. A CBV function <code>λx.M</code> : <math>A \to_v B</math> is translated to <code>thunk λx.M^v</code> : <math>U (A^v \to F B^v)</math>. A CBV application <code>M N</code> : <math>A</math> is translated to a computation <code>M^v to f in N^v to x in x'(force f)</code> of type <math>F A</math>, making the order of evaluation explicit. A pattern match <code>match V as { (1,...) in M_1, ... }</code> is translated as <code>V^v to z in match z as { (1,...) in M_1^v, ... }</code>. Values are wrapped with <code>return</code> when necessary, but otherwise remain unmodified.<ref name="Levy99"/> In some translations, sequencing may be required, such as translating <code>inl M</code> to <code>M to x. return inl x</code>.<ref name="Levy2022"/>

The CBN translation produces CBPV computations for each expression. A CBN function <code>λx.M</code> : <math>A \to B</math> translates unaltered, <code>λx.M^N</code> : <math>(U A^n) \to X^n</math>. A CBN application <code>M N</code> : <math>C</math> is translated to a computation <code>M^v (thunk N^v)</code> of type <math>C^n</math>. A pattern match <code>match V as { (1,...) in M_1, ... }</code> is translated similarly to CBN as <code>Vⁿ to z in match z as { (1,...) in M_1ⁿ, ... }</code>. ADT values are wrapped with <code>return</code>, but <code>force</code> and <code>thunk</code> are also necessary on internal structure. Levy's translation assumes that <code>M = force (thunk M)</code>, which does indeed hold.<ref name="Levy99"/>

== References ==

{{reflist}}

<references/>

{{comp-sci-theory-stub}}

[[Category:Lambda calculus]]

[[Category:Programming language semantics]]