一句话：提出类型相异性放松 disjointness 约束，并用守卫子类型避免歧义，使 merge 在保持确定性下支持重载与嵌套组合。
合并（merge）算子可灵活组合函数、记录和类，但类型重叠时易导致歧义与非确定性。已有 disjoint intersection types 通过严格 disjointness 约束保证确定性，却牺牲表达力，尤其限制函数重载。本文提出类型相异性（type apartness），放松 disjointness，允许重载函数存在一定重叠，只要调用上下文能消解函数调用中的上转型歧义；并引入守卫子类型（guarded subtyping）在上转型时防止歧义。该方法是首个在单一演算中同时支持函数重载、返回类型重载、可扩展记录和嵌套组合且保持确定性的方案。作者在 Coq 中形式化演算并证明类型可靠性与确定性，还展示类型规范化与类型差如何帮助解决冲突、增强 merge 的灵活性与表达力。
The merge operator is a powerful construct in programming languages, enabling flexible composition of various components such as functions, records, or classes. Unfortunately, its application often leads to ambiguity and non-determinism, especially when dealing with overlapping types. To prevent ambiguity, approaches such as disjoint intersection types have been proposed. However, disjointness imposes strict constraints to ensure determinism, at the cost of limiting expressiveness, particularly for function overloading. This paper introduces a novel concept called type apartness, which relaxes the strict disjointness constraints, while maintaining type safety and determinism. Type apartness allows some overlap for overloaded functions as long as the calling contexts of those functions can be used to disambiguate upcasts in function calls. By incorporating the notion of guarded subtyping to prevent ambiguity when upcasting, our approach is the first to support function overloading, return type overloading, extensible records, and nested composition in a single calculus while preserving determinism. We formalize our calculi and proofs using Coq and prove their type soundness and determinism. Additionally, we demonstrate how type normalization and type difference provide more convenience and help resolve conflicts, enhancing the flexibility and expressiveness of the merge operator.
@article{paperbot2923,
title = {Liberating Merges via Apartness and Guarded Subtyping},
author = {Han Xu and Xuejing Huang and Bruno C. d. S. Oliveira},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763057}
}