[PLDI'23] Better Defunctionalization through Lambda Set Specialization скачать в хорошем качестве

[PLDI'23] Better Defunctionalization through Lambda Set Specialization

Better Defunctionalization through Lambda Set Specialization (Video, PLDI 2023) William Brandon, Benjamin Driscoll, Frank Dai, Wilson Berkow, and Mae Milano (Massachusetts Institute of Technology, USA; Stanford University, USA; University of California at Berkeley, USA; University of California at Berkeley, USA; University of California at Berkeley, USA) Abstract: Higher-order functions pose a challenge for both static program analyses and optimizing compilers. To simplify the analysis and compilation of languages with higher-order functions, a rich body of prior work has proposed a variety of defunctionalization techniques, which can eliminate higher-order functions from a program by transforming the program to a semantically-equivalent first-order representation. Several modern languages take this a step further, specializing higher-order functions with respect to the functions on which they operate, and in turn allowing compilers to generate more efficient code. However, existing specializing defunctionalization techniques restrict how function values may be used, forcing implementations to fall back on costly dynamic alternatives. We propose lambda set specialization (LSS), the first specializing defunctionalization technique which imposes no restrictions on how function values may be used. We formulate LSS in terms of a polymorphic type system which tracks the flow of function values through the program, and use this type system to recast specialization of higher-order functions with respect to their arguments as a form of type monomorphization. We show that our type system admits a simple and tractable type inference algorithm, and give a formalization and fully-mechanized proof in the Isabelle/HOL proof assistant showing soundness and completeness of the type inference algorithm with respect to the type system. To show the benefits of LSS, we evaluate its impact on the run time performance of code generated by the MLton compiler for Standard ML, the OCaml compiler, and the new Morphic functional programming language. We find that pre-processing with LSS achieves run time speedups of up to 6.85x under MLton, 3.45x for OCaml, and 78.93x for Morphic. Article: https://doi.org/10.1145/3591260 Supplementary archive: https://doi.org/10.5281/zenodo.7712285 (Badges: Artifacts Available, Artifacts Evaluated — Reusable) ORCID: https://orcid.org/0009-0007-9478-8757, https://orcid.org/0000-0002-1901-1880, https://orcid.org/0009-0003-9486-4060, https://orcid.org/0009-0009-7376-7652, https://orcid.org/0000-0003-3126-7771 Video Tags: monomorphization, defunctionalization, type systems, pldi23main-p236-p, doi:10.1145/3591260, doi:10.5281/zenodo.7712285, orcid:0009-0007-9478-8757, orcid:0000-0002-1901-1880, orcid:0009-0003-9486-4060, orcid:0009-0009-7376-7652, orcid:0000-0003-3126-7771, Artifacts Available, Artifacts Evaluated — Reusable Presentation at the PLDI 2023 conference, June 17–21, 2023, https://pldi23.sigplan.org/ Sponsored by ACM SIGPLAN,