一句话：提出 F⋈ 核心语言，用对偶不相交关系驯服 merge，使 union、intersection 和重载共存且类型安全、确定。
类型化 merge 算子可实现组合式静态类型编程并自然解决表达式问题，但处理重叠类型合并时会产生歧义。此前的 disjoint merge 依赖 intersection types，扩展到 union types 或重载函数时又会重新引入歧义：union 与重载的消去形式要求值可区分，而 merge 可能构造出违反该要求的奇异值。本文提出核心语言 F⋈，其设计原则是任意两个可居留类型要么支持值的确定性合并，要么支持值的可区分性，但不能同时支持两者。作者将既有 disjointness 概念分解为两个对偶关系，为每对类型选择合适操作，并尊重类型结构的极化。F⋈ 支持 union、intersection 与重载共存，被证明类型安全且具有确定性。
The typed merge operator offers the promise of a compositional style of statically-typed programming in which solutions to the expression problem arise naturally. This approach, dubbed compositional programming , has recently been demonstrated by Zhang et al. Unfortunately, the merge operator is an unwieldy beast. Merging values from overlapping types may be ambiguous, so disjointness relations have been introduced to rule out undesired nondeterminism and obtain a well-behaved semantics. Past type systems using a disjoint merge operator rely on intersection types, but extending such systems to include union types or overloaded functions is problematic: naively adding either reintroduces ambiguity. In a nutshell: the elimination forms of unions and overloaded functions require values to be distinguishable by case analysis, but the merge operator can create exotic values that violate that requirement. This paper presents F ⋈ , a core language that demonstrates how unions, intersections, and overloading can all coexist with a tame merge operator. The key is an underlying design principle that states that any two inhabited types can support either the deterministic merging of their values, or the ability to distinguish their values, but never both. To realize this invariant, we decompose previously studied notions of disjointness into two new, dual relations that permit the operation that best suits each pair of types. This duality respects the polarization of the type structure, yielding an expressive language that we prove to be both type safe and deterministic.
@article{paperbot2048,
title = {A Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data Types in F⋈},
author = {Nick Rioux and Xuejing Huang and Bruno C. d. S. Oliveira and Steve Zdancewic},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {POPL},
year = {2023},
doi = {10.1145/3571211}
}