Content deleted Content added
→Translation: call-by-need |
modifications section |
||
Line 29:
It is also possible to extend CBPV to model call-by-need, by introducing a <code>M need x. N</code> construct that allows visible sharing. This construct has semantics similar to <code>M name x. N = (λy.N[x ↦ (force y)])(thunk M)</code>, except that with the <code>need</code> construct, the thunk of <code>M</code> is evaluated at most once.<ref>{{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}}</ref>
== 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 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 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 ==
| |||