paperbot · PL 论文追踪

全部论文 待读 收藏

P2 The Long Way to Deforestation: A Type Inference and Elaboration Technique for Removing Intermediate Data Structures

去森林化的漫漫长路:一种移除中间数据结构的类型推断与 elaboration 技术
ICFP 8(ICFP)2024匹配度 2/10 · 该论文属于编程语言与编译器优化方向(类型推断与 elaboration 驱动的去森林化),虽兼具形式化(step-indexed logical relations 的可靠性证明)与工程评估(nofib 基准),但完全不涉及用户画像的核心问题:既不是对 ML/Agentic 程序做静态分析(PL→AI),也未用 LLM/Agent 改进分析或验证(AI→PL),更与浮点程序分析、贝叶斯程序分析无交集。仅在最宽泛的“程序语言/静态分析理论”层面上有微弱关联。引用 0 inbox
Yijia Chen, Lionel Parreaux
dblp: 2026-09-10crossref: 2026-09-10arxiv: 2026-09-10

AI 速览

一句话:提出 Lumberhack,用子类型推断与 elaboration 融合递归定义,实现通用去森林化,在 nofib 上平均加速 8.2%。

去森林化能消除函数式程序中的中间数据结构,但已有方法要么只支持预定义组合子,要么依赖递归定义的激进展开,导致复杂度过高和代码重复。本文提出 Lumberhack,一种面向纯函数式 call-by-need 与 call-by-value 程序的通用去森林化方法:用子类型推断分析数据结构的产生与消费,并通过 elaboration 融合递归定义,避免无益复制。作者用 step-indexed logical relations 证明可靠性。实验将 nofib 程序适配为 call-by-value 并用 OCaml 编译:38 个基准平均加速 8.2%,代码量约增至 1.79 倍。其中 17 个平均加速 16.6%,19 个基本不变,2 个平均变慢 1.8%;GHC 列表融合平均加速 6.5%。

问题
如何通用地消除纯函数式程序中的中间数据结构,同时避免已有方法(shortcut fusion、激进展开)的局限与代码复制。
方法
Lumberhack 使用子类型推断分析数据结构的产生与消费,并通过 elaboration 融合递归定义,支持 call-by-need 与 call-by-value 程序。
评估
用 step-indexed logical relations 证明可靠性,在手工适配为 call-by-value 的 nofib 基准上用 OCaml 编译测试,平均加速 8.2%,并与 GHC 列表融合对比。
原文摘要(Abstract)

Deforestation is a compiler optimization that removes intermediate data structure allocations from functional programs to improve their efficiency. This is an old idea, but previous approaches have proved limited or impractical — they either only worked on compositions of predefined combinators (shortcut fusion), or involved the aggressive unfolding of recursive definitions until a depth limit was reached or a reoccurring pattern was found to tie the recursive knot, resulting in impractical algorithmic complexity and large amounts of code duplication. We present Lumberhack, a general-purpose deforestation approach for purely functional call-by-need and call-by-value programs. Lumberhack uses subtype inference to reason about data structure production and consumption and uses an elaboration pass to fuse the corresponding recursive definitions. It fuses large classes of mutually recursive definitions while avoiding much of the unproductive (and sometimes counter-productive) code duplication inherent in previous approaches. We prove the soundness of Lumberhack using step-indexed logical relations and experimentally demonstrate significant speedups in the standard nofib benchmark suite. We manually adapted nofib programs to call-by-value semantics and compiled them using the OCaml compiler. The average speedup over the 38 benchmarked programs is 8.2 % while the average code size increases by just about 1 . 79 x . In particular, 19 programs see their performance mostly unchanged, 17 programs improve significantly (by an average speedup of 16.6 % ), and only two programs visibly worsen (by an average slowdown of 1.8 % ). As a point of comparison, we measured that the well-proven but semi-manual list fusion technique of the Glasgow Haskell Compiler (GHC), which only works for call-by-need programs, had an average speedup of 6.5 % . Our technique is still in its infancy and misses some deforestation opportunities. We are confident that further refinements will yield greater performance improvements in the future.

链接与引用

DOI 原文 · arXiv · PDF(开放获取) · DBLP

BibTeX
@article{ChenP24,
  title = {The Long Way to Deforestation: A Type Inference and Elaboration Technique for Removing Intermediate Data Structures},
  author = {Yijia Chen and Lionel Parreaux},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {8},
  number = {ICFP},
  year = {2024},
  doi = {10.1145/3674634}
}