Call-by-push-value: Difference between revisions

Revision as of 05:14, 15 April 2024

Revision as of 19:51, 12 May 2024

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 journal |last1=Ehrhard |first1=Thomas |title=Call-By-Push-Value from a Linear Logic Point of View |journal=Programming Languages and Systems |date=2016 |volume=9632 |pages=202–228 |doi=10.1007/978-3-662-49498-1_9|doi-access=free}}</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"/> Erhard in contrast omits the F type constructor, making values a subset of computations. Erhard 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 journal |last1=Chouquet |first1=Jules |last2=Tasson |first2=Christine |title=Taylor expansion for Call-By-Push-Value |journal=CSL |date=2020 |doi=10.4230/LIPIcs.CSL.2020.16 |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>

== See also ==