Deforestation is the act of optimizing functional programs by removing the allocation of intermediate data structure. In previous work, we showed that a relatively flexible form of deforestation can be achieved in practical settings through a technique we called type-inference-and-elaboration: we first infer some types and, based on them, perform program transformation. This approach is correct by construction, as we showed semantic preservation through step-indexed logical relations based on this type system. In this talk, I will reframe this approach by showing that its core transformation is a refunctionalization, the dual of defunctionalization. Refunctionalization is a known technique, but we are not aware of any prior use of it in compiler optimization. We also show that the best application of our technique probably mixes phases of deforestation by refunctionalization followed by defunctionalization. Indeed, eagerly applying deforestation will result in recursive functions written in accumulator-parameter style to be transformed into functions that accumulate continuations, which is often less efficient.

I am an Assistant Professor at the HKUST CSE department since February 2021. I am looking for students to join my research group! Please contact me (first-name dot last-name at gmail.com) if you’d like to work on something related to programming languages, type systems, or compiler optimization.

I obtained my PhD in 2020 from EPFL, in the Data Analysis Theory and Applications Laboratory (DATA), where I created the Squid type-safe metaprogramming library for Scala.