Better Defunctionalization through Lambda Set Specialization
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 it 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. 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 of soundness for this type inference algorithm in the Isabelle/HOL proof assistant. 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.85× under MLton, 3.45× under OCaml, and 78.93× under Morphic.
Tue 20 JunDisplayed time zone: Eastern Time (US & Canada) change
13:40 - 15:40 | PLDI: Analysis & OptimizationsPLDI Research Papers at Cypress 2 Chair(s): Fredrik Kjolstad Stanford University | ||
13:40 20mTalk | Collecting Cyclic Garbage across Foreign Function Interfaces: Who Takes the Last Piece of Cake? PLDI Research Papers Tetsuro Yamazaki University of Tokyo, Tomoki Nakamaru University of Tokyo, Ryota Shioya University of Tokyo, Tomoharu Ugawa University of Tokyo, Shigeru Chiba The University of Tokyo DOI | ||
14:00 20mTalk | Modular Hardware Design with Timeline Types PLDI Research Papers Rachit Nigam Cornell University, Pedro Henrique Azevedo de Amorim Cornell University, Adrian Sampson Cornell University DOI Pre-print | ||
14:20 20mTalk | Efficient Parallel Functional Programming with Effects PLDI Research Papers Jatin Arora Carnegie Mellon University, Sam Westrick Carnegie Mellon University, Umut A. Acar Carnegie Mellon University DOI | ||
14:40 20mTalk | Better Defunctionalization through Lambda Set Specialization PLDI Research Papers William Brandon MIT CSAIL, Benjamin Driscoll Stanford University, Wilson Berkow UC Berkeley, Frank Dai UC Berkeley, Mae Milano University of California at Berkeley DOI | ||
15:00 20mTalk | Sound Dynamic Deadlock Prediction in Linear Time PLDI Research Papers Hünkar Can Tunç Aarhus University, Umang Mathur National University of Singapore, Andreas Pavlogiannis Aarhus University, Mahesh Viswanathan University of Illinois at Urbana-Champaign DOI Pre-print | ||
15:20 20mTalk | Context Sensitivity without Contexts: A Cut-Shortcut Approach to Fast and Precise Pointer Analysis PLDI Research Papers Wenjie Ma Nanjing University, Shengyuan Yang Nanjing University, Tian Tan Nanjing University, Xiaoxing Ma Nanjing University, Chang Xu Nanjing University, Yue Li Nanjing University DOI Pre-print |