一句话：用双向类型化仅限制引用规则，在保留分配性交集子类型的同时为组合式编程加入可变引用，并机器化验证类型安全。
组合式编程（CP）以模块化为核心，其理论基础是带交集类型的纯函数式 System F 变体 F_i+，子类型的分配律是模块化能力的关键。然而 Davies 与 Pfenning 曾指出，分配性子类型规则与可变引用结合会导致类型不安全，他们提出的补救办法是删除分配律；但 CP 从根本上依赖分配律，无法照搬。本文重新审视该问题，提出采用双向类型化（bidirectional typing），只需对引用的类型规则施加较轻量的限制，即可同时保留分配律与不受限的交集引入规则，从而恢复类型安全。作者先给出一个基于 Davies–Pfenning 工作的通用演算以说明该方案的普适性，再给出带引用的 F_i+ 扩展，支持命令式组合式编程风格；同时实现了 CP 的引用扩展，并用它建模模块化的活跃变量分析。两个演算及其证明均已在 Coq 证明助手中机器化验证。
Compositional programming is a programming paradigm that emphasizes modularity and is implemented in the CP programming language. The foundations for compositional programming are based on a purely functional variant of System F with intersection types, called F i + , which includes distributivity rules for subtyping. This paper shows how to extend compositional programming and CP with mutable references, enabling a modular, imperative compositional programming style. A technical obstacle solved in our work is the interaction between distributive intersection subtyping and mutable references. Davies and Pfenning [2000] studied this problem in standard formulations of intersection type systems and argued that, when combined with references, distributive subtyping rules lead to type unsoundness. To recover type soundness, they proposed dropping distributivity rules in subtyping. CP cannot adopt this solution, since it fundamentally relies on distributivity for modularity. Therefore, we revisit the problem and show that, by adopting bidirectional typing , a more lightweight and type sound restriction is possible: we can simply restrict the typing rule for references. This solution retains distributivity and an unrestricted intersection introduction rule. We present a first calculus, based on Davies and Pfenning ’s work, which illustrates the generality of our solution. Then we present an extension of F i + with references, which adopts our restriction and enables imperative compositional programming. We implement an extension of CP with references and show how to model a modular live-variable analysis in CP. Both calculi and their proofs are formalized in the Coq proof assistant.
@article{YeSO24,
title = {Imperative Compositional Programming: Type Sound Distributive Intersection Subtyping with References via Bidirectional Typing},
author = {Wenjia Ye and Yaozhu Sun and Bruno C. d. S. Oliveira},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA2},
year = {2024},
doi = {10.1145/3689782}
}