Call-by-push-value: Difference between revisions

Revision as of 08:58, 11 April 2024

Latest revision as of 17:10, 23 June 2025

(8 intermediate revisions by 6 users not shown)

Line 1:

{{Short description|Intermediate language}}

In [[programming language theory]], '''call-by-push-value''' (CBPV) is an [[intermediate language]] that embeds the [[call-by-value]] (CBV) and [[call-by-name]] (CBN) [[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|arxiv=1911.04588 }}</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}}</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>

== Definition ==

Line 31:

== Modifications ==

Some authors have noted that CBPV can be simplified, by removing either the U type constructor (thunks)<ref name="Egger2014">{{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}}</ref> or the F type constructor (computations returning values).<ref name="Ehrhard2016">{{cite journalbook |last1=Ehrhard |first1=Thomas |titlechapter=Call-By-Push-Value from a Linear Logic Point of View |journaltitle=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 }}</ref>. 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.<ref name="Egger2014"/> ErhardEhrhard in contrast omits the F type constructor, making values a subset of computations. ErhardEhrhard renames computations to "general types" to better reflect their semantics. This modified calculus, the "half-polarized lambda calculus", has close connections to linear logic.<ref name="Ehrhard2016"/><ref>{{cite journalbook |last1=Chouquet |first1=Jules |last2=Tasson |first2=Christine |title=Taylor expansion for Call-By-Push-Value |journaldate=CSL2020 |datepublisher=2020Schloss 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}}</ref> It can be translated bidirectionally to a subset of a fully-polarized variant of CBPV.<ref>{{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}}</ref>

== Award ==

Paul Blain Levy received the 2025 [[Alonzo Church Award]] for his work on CBPV.<ref>https://siglog.org/winner-of-the-2025-alonzo-church-award/</ref>

== See also ==