一句话：提出以 web（生产者-消费者集合）为变换单位的中间语言与流导向变换，并用基于合一的类型分析保证变换保持良类型性。
高阶语言中多个函数可能流向同一调用点，它们必须共享接口，这构成 web；修改其中一个成员需改动整个 web，作者主张 web 是程序变换的基本单位。本文设计以 web 为中心的中间语言，把 web 作为注解显式暴露，据此刻画由控制流分析（CFA）引导的 web 基（流导向）过程间变换，并重新解释、泛化了死参数消除、uncurrying、defunctionalization 等变换。web 是 CFA 调用关系的过近似，且与变换解耦：分析越精确可做越多变换，但精确分析可能破坏良类型性。为此作者提出基于合一的轻量类型分析，区分“看似相同”与“必须相同”的类型，使流导向变换保持良类型性。实验表明该分析理论上精度较低，实践中接近 CFA。
We define webs to be the collections of producers and consumers ( e.g ., functions and calls) in a program that are constrained: in higher-order languages, multiple functions can flow to the same call, all of which must agree on an interface (e.g., calling convention). We argue that webs are fundamentally the unit of transformation : a change to one member requires changes across the entire web. We introduce a web-centric intermediate language that exposes webs as annotations, and describe web-based (that is, flow-directed) transformations guided by these annotations. As they affect all members of a web, these transformations are interprocedural, operating over entire modules. Through the lens of webs we reframe and generalize a collection of transformations from the literature, including dead-parameter elimination, uncurrying, and defunctionalization, as well as describe novel transformations. We contrast this approach with rewriting strategies that rely on inlining and cascading rewrites. Webs are an over-approximation of the semantic function-call relationship produced by control-flow analyses (CFA). This information is inherently independent from the transformations; more precise analyses permit more transformations. A limitation of precise analyses is that the transformations may not maintain well-typedness, as the type system is a less-precise static analysis. Our solution is a simple and lightweight typed-based analysis that causes the flow-directed transformations to preserve well-typedness, making flow-directed, type-preserving transformations easily accessible in many compilers. This analysis builds on unification, distinguishing types that look the same from types that have to be the same. Our experiments show that while our analysis is theoretically less precise, in practice its precision is similar to CFAs.
@article{paperbot3134,
title = {Webs and Flow-Directed Well-Typedness Preserving Program Transformations},
author = {Benjamin Quiring and David Van Horn and John Reppy and Olin Shivers},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {PLDI},
year = {2025},
doi = {10.1145/3729280}
}