Predictable Deforestation: A Typed Approach to Eliminating Virtual Aggregates

9804053将程序表示为通过聚合数据结构(列表、树、数组等)进行通信的混合匹配部分的组合是一种众所周知的模块化技术，可简化软件系统的构建、修改和验证。不幸的是，程序员经常回避这项技术，以避免创建、操作和处置中间聚合的时间和空间成本。森林砍伐是一种通过自动消除其中一些聚集体来降低这些成本的优化。对于现有的森林砍伐机制，(1)很难预测哪些聚集体将被消除，因此很难对优化计划的时间和空间要求进行推理，以及(2)只能处理简单的聚集体和/或生产者/消费者拓扑。这个项目的目标是设计一种可预测的森林砍伐技术，通过区分运行时存在的真实聚集和编译时消除的虚拟聚集的类型系统来解决这些限制。类型系统将(1)指示森林砍伐是可能的(或在不可能时警告程序员)；(2)允许程序员自信地推理优化程序的时间和空间要求；以及(3)处理广泛的聚集和生产者/消费者拓扑。可预测的森林砍伐将在ML编程语言的编译器中实现。*

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.***