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