Predictable Deforestation: A Typed Approach to Eliminating Virtual Aggregates

点击翻译按钮获取中文摘要

9804053 Expressing programs as the composition of mix-and-match parts that communicate via aggregate data structures (lists, trees, arrays, etc.) is a well-known modularity technique that simplifies the construction, modification, and verification of software systems. Unfortunately, programmers often eschew this technique to avoid the time and space costs of creating, manipulating, and disposing of intermediate aggregates. Deforestation is an optimization that reduces these costs by automatically eliminating some of these aggregates. With existing deforestation mechanisms, (1) it is difficult to predict which aggregates will be eliminated, and thus difficult to reason about the time and space requirements of the optimized program, and (2) only simple aggregates and/or producer/consumer topologies can be handled. The goal of this project is to design a predictable deforestation technique that addresses these limitations via a type system that distinguishes between real aggregates present at run-time and virtual aggregates eliminated at compile-time. The type system will (1) indicate that deforestation is possible (or warn the programmer when it is not); (2) permit the programmer to reason confidently about the time and space requirements of the optimized program; and (3) handle a wide range of aggregates and producer/consumer topologies. Predictable deforestation will be implemented in a compiler for the ML programming language.***