[ICFP24] Call-By-Unboxed-Value

Call-by-Unboxed-Value (Video, ICFP 2024)
Paul Downen
(University of Massachusetts at Lowell, USA)

Abstract: Call-By-Push-Value has famously subsumed both call-by-name and call-by-value by decomposing programs along the axis of 'values' versus 'computations.' Here, we introduce Call-By-Unboxed-Value which further decomposes programs along an orthogonal axis separating 'atomic' versus 'complex.' As the name suggests, these two dimensions make it possible to express the representations of values as boxed or unboxed, so that functions pass unboxed values as inputs and outputs. More importantly, Call-By-Unboxed-Value allows for an unrestricted mixture of polymorphism and unboxed types, giving a foundation for studying compilation techniques for polymorphism based on representation irrelevance. In this regard, we use Call-By-Unboxed-Value to formalize representation polymorphism independently of types; for the first time compiling untyped representation-polymorphic code, while nonetheless preserving types all the way to the machine.

Article: https://doi.org/10.1145/3674654

ORCID: https://orcid.org/0000-0003-0165-9387

Video Tags: Call-by-push-value, focusing, type systems, unboxed types, polymorphism, icfp24main-p90-p, doi:10.1145/3674654, orcid:0000-0003-0165-9387

Presentation at the ICFP 2024 conference, September 2–7, 2024, https://icfp24.sigplan.org/
Sponsored by ACM SIGPLAN,