Liberating Merges via Apartness and Guarded Subtyping

HKU PL Group Papers - Index

Metadata

• Title: Liberating Merges via Apartness and Guarded Subtyping
• Venue: OOPSLA’25
• Area: Merge operator and disjointness
• Source URL: https://doi.org/10.1145/3763057
• Downloaded PDF: Liberating-Merges-via-Apartness-and-Guarded-Subtyping.pdf
• Extracted assets: _assets/Liberating-Merges-via-Apartness-and-Guarded-Subtyping/
• Pages: 27
• Embedded image count reported by PyMuPDF: 0

Why this note exists

This note is part of the HKU PL Group literature knowledge base for work on iso-recursive subtyping, intersection types, union types, disjointness, merge operators, and compositional programming. It is designed for later Coding Agent / Proof Agent use during proof search, design brainstorming, and comparison against prior systems.

Extraction quality note

This is the fast pass generated with pymupdf4llm, not the heavier marker-pdf pass. The original PDF is linked above and kept in _pdfs/. Figures/images detected by PyMuPDF are saved under _assets/. Some mathematical notation may still require checking against the PDF, especially inference rules with complex layouts.

Technical landmarks detected automatically

These are line references into the converted Markdown below. They are meant as a quick navigation layer for rules, lemmas, theorems, proofs, algorithms, examples, and counterexamples.

• line 2:
• line 5: Liberating Merges via Apartness and Guarded Subtyping
• line 19: Han Xu, Xuejing Huang, and Bruno C. d. S. Oliveira. 2025. Liberating Merges via Apartness and Guarded Subtyping. Proc. ACM Program. Lang. 9, OOPSLA2, Article 279 (October 2025), 27 pages. https://doi.org/10. 1145/3763057
• line 21: 1 Introduction
• line 51: - Type apartness , which enables function overloading, return type overloading, extensible records, and nested composition while maintaining determinism.
• line 53: - A formalization of source and target calculi , proving their soundness and correspondence.
• line 59: 2 Overview
• line 67: Liberating Merges via Apartness and Guarded Subtyping
• line 73: that supports all these features while ensuring determinism. We also highlight the role of type well-formedness and type normalization in constructing sound calculi with apart merges.
• line 75: 2.1 C++ Method Resolution: A Source of Inspiration
• line 81: 2.2 Background
• line 93: Table 1. Four applications of the merge operator with examples.
• line 95: |Features|Examples|Previous Works|
• line 104: |Extensible records|l1 =“hello”,,l2 =“world”|Bi et al. [2018]; Huang et al. [2021]; Xue
  et al.[2022]|
• line 122: Liberating Merges via Apartness and Guarded Subtyping
• line 136: It is possible to disambiguate calls to read from the use context. For example, (read “1”) + 1 should select readInt, since an integer is expected from the use of read.
• line 144: - Extensible records. Extensible records were among the first applications of merges [Reynolds 1988]. The key observation is that multi-field records can be simply encoded as merges of single-field records, such as:
• line 148: The merge of single-field records should have the same behaviour as a multi-field record. That is to say, the merge should project the associated content of the single field that is designated.
• line 151:
• line 157:
• line 172: Definition 2.1 (Disjointness Specification). A ∗ 𝑑 B ≜ ∀ C, if A ≤ C ∧ B ≤ C, then ⊤≤ C.
• line 177:
• line 180: Next we show a few more examples to illustrate disjointness on different types.
• line 186: Limitations of disjointness. While disjointness is a valuable approach, it comes with limitations. For instance, disjointness prevents conventional function overloading, such as:
• line 198: 2.3 Apartness: Relaxing Disjointness
• line 206: Liberating Merges via Apartness and Guarded Subtyping
• line 211:
• line 218: Fig. 2. Cases: A disjoint with B , A (completely) shadows B , and A apart (or partly overlaps) with B .
• line 228: So the show merge should be accepted. However, if we have:
• line 238: 2.4 Technical Overview
• line 240: In this section, we will give a more technical overview towards the key design and mechanisms for apartness, guarded subtyping as well as the features in source and target calculi.
• line 256: |Bool&String|Bool&String|✗asBis an intersection type|
• line 282: Unlike the usual subtyping relation, the guarded subtyping relation A ≾ B is not transitive. This means that even if A ≾ B and B ≾ C , it does not necessarily follow that A ≾ C . For example:
• line 290: Liberating Merges via Apartness and Guarded Subtyping
• line 301:
• line 323:
• line 330: Fig. 3. Interface inheritance hierarchy with unrestricted intersections.
• line 341:
• line 350: Liberating Merges via Apartness and Guarded Subtyping
• line 369:
• line 378: 3 Apartness and Guarded Subtyping for Intersection Types
• line 380: This section shows how to derive algorithmic formulations of apartness and how to formulate guarded subtyping with intersection types and a merge operator.
• line 382: 3.1 Syntax and Subtyping
• line 398: ||||Record encoding||||||||𝑙1|:𝐴1, |… , |𝑙𝑛:𝐴𝑛 ≜𝑙1|||:𝐴1& . .|. &𝑙𝑛:𝐴𝑛||||
• line 399: ||𝐴≤𝐵|||(Declarative BCD Subtyping)|||||||||||A <:B||||(Algorithmic BCD Subtyping)|||
• line 408: ||⊢𝑠A||||||||(Type Well-Formedness (Strict))||||||||A≃B&C|||(Type Splitting)||
• line 417: Fig. 4. BCD subtyping, ordinary types, splittable types and the strict type well-formedness.
• line 427: Liberating Merges via Apartness and Guarded Subtyping
• line 431: 3.2 Type Well-Formedness
• line 437: Theorem 3.1 (Well-Formed Types have Apart Components). If ⊢ 𝑠 A, and A ≃ B & C, then A = B & C, B ∗ C, ⊢ 𝑠 B and ⊢ 𝑠 C .
• line 441: 3.3 Apartness
• line 477: Theorem 3.2 (Soundness of Apartness). If A ∗ B, then A ∗ 𝑠 B.
• line 479: Theorem 3.3 (Completeness of Apartness). If ⊢ 𝑠 A, ⊢ 𝑠 B, and A ∗ 𝑠 B, then A ∗ B.
• line 481: 3.4 Guarded Subtyping
• line 487: To provide more intuition, we can illustrate the guarded subtyping with some concrete examples:
• line 502: Liberating Merges via Apartness and Guarded Subtyping
• line 512: Fig. 6. Guarded subtyping.
• line 520: Theorem 3.4 (Soundness of Guarded Subtyping). If A ≾ B, then A ≤ B.
• line 522: Theorem 3.5 (Safe Casting). If A ∗ B and A ≤ C and B ≤ C, then ¬( A & B ≾ C ) or ⊤≤ C.
• line 524: 4 The 𝜆 ∗ Calculus
• line 536: (Syntax of Expressions)
• line 542: ||⊢𝑟A|||||(Relaxed Type||Well-Formedness)
  ⊢Γ|||(Well-Formedness of Typing Environments)||||
• line 545: ||Γ ⊢𝑡e ⇔A||||||||||||(Typing|Rules of 𝜆∗)|
• line 549: ||||||||||TTyp-app||TTyp-merge||TTyp-sub||
• line 557: Fig. 7. The syntax, type well-formedness and typing rules for 𝜆 ∗.
• line 559: 4.1 Syntax and the Type System of 𝜆 ∗
• line 567: Theorem 4.1 (Soundness of Relaxed Well-Formedness). If ⊢ 𝑠 A then ⊢ 𝑟 A.
• line 573: Liberating Merges via Apartness and Guarded Subtyping
• line 585: Theorem 4.2 (Well-formed Types Respect Apartness). If ⊢ 𝑟 A and A ≃ B & C, then B ∗ C.
• line 587: Theorem 4.3 (Completeness for Relaxed Well-Formedness). For all 𝐴𝐵 that ⊢ 𝑟 A and ⊢ 𝑟 B, if A ∗ 𝑠 B then A ∗ B.
• line 589: Theorem 4.4 (Round-Trip Coercion). For all 𝐴𝐵, if ⊢ 𝑟 A, ⊢ 𝑟 B, A ≤ B, and B ≤ A, then A ≾ B.
• line 593: Theorem 4.5 (Typing Respects Type Well-Formedness). If Γ ⊢ 𝑡 e ⇔ A, then ⊢ 𝑟 A.
• line 611: Fig. 9. The operational semantics of 𝜆 ∗.
• line 615: Theorem 4.6 (Soundness and Minimality of Type Dispatching). If B ⊢ A � C, then:
• line 625: 4.2 Operational Semantics
• line 633: Liberating Merges via Apartness and Guarded Subtyping
• line 645: Theorem 4.7 (Determinism of Casting in 𝜆 ∗). If v : A and A ≾ B, then from v ↩ → B v 1 and v ↩ → B v 2 we can derive v 1 = v 2 .
• line 649: Theorem 4.8 (Behavioral Eqivalence of Round-Trip Coercion). If for all 𝑖 ∈[1 ,𝑛 ] , ⊢ 𝑟 𝐴𝑖 , and v𝑖 −1 can be coerced to v𝑖 via v𝑖 −1 ↩ → 𝐴𝑖 v𝑖 , then if 𝐴 𝑗 = 𝐴𝑘 , then � 𝑣 𝑗 � = � 𝑣𝑘 � .
• line 651: 4.3 Type Safety
• line 655: Theorem 4.9 (Preservation of 𝜆 ∗).

Full converted paper text

Liberating Merges via Apartness and Guarded Subtyping

HAN XU, Princeton University, United States

XUEJING HUANG, The University of Hong Kong, China and IRIF, Université Paris Cité, France BRUNO C. D. S. OLIVEIRA, The University of Hong Kong, China

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.

CCS Concepts: • Theory of computation → Type theory .

Additional Key Words and Phrases: functional languages, object oriented languages, type systems

ACM Reference Format:

Han Xu, Xuejing Huang, and Bruno C. d. S. Oliveira. 2025. Liberating Merges via Apartness and Guarded Subtyping. Proc. ACM Program. Lang. 9, OOPSLA2, Article 279 (October 2025), 27 pages. https://doi.org/10. 1145/3763057

1 Introduction

The merge operator [Reynolds 1997] is a powerful construct that enables flexible composition of functions, records, and classes. Dunfield [2014] argued that the merge operator is valuable for language design because it allows encoding various language features within a general-purpose calculus, rather than crafting specialized calculi for each feature. The merge operator composes any two values, with extraction determined by their types. For instance, the merge 1 ,, True combines an integer and a boolean, giving it the intersection type Int & Bool. Many applications of the merge operator exist, including function overloading [Castagna et al. 1995], return type overloading [Xue et al. 2022], record concatenation [Reynolds 1988], nested composition and dynamic inheritance [Bi and Oliveira 2018], and composition of runtime environments [Tan and Oliveira 2023].

Due to its power, the merge operator is hard to control. In particular, merging values with overlapping types can introduce ambiguity. For example, in the merge 1 ,, 2, extracting an integer is ambiguous since either 1 or 2 could be chosen. Disjoint intersection types [Oliveira et al. 2016] were introduced to address this issue by restricting the types of values that can be merged based on their

Authors’ Contact Information: Han Xu, hx3501@princeton.edu, Princeton University, Princeton, United States; Xuejing Huang, Xuejing.Huang@irif.fr, The University of Hong Kong, China and IRIF, Université Paris Cité, France; Bruno C. d. S. Oliveira, The University of Hong Kong, China, bruno@cs.hku.hk.

This work is licensed under a Creative Commons Attribution 4.0 International License.

© 2025 Copyright held by the owner/author(s). ACM 2475-1421/2025/10-ART279 https://doi.org/10.1145/3763057

Proc. ACM Program. Lang., Vol. 9, No. OOPSLA2, Article 279. Publication date: October 2025.

--- end of page.page_number=1 ---

Han Xu, Xuejing Huang, and Bruno C. d. S. Oliveira

279:2

shared supertypes, ensuring a deterministic and well-behaved semantics [Huang et al. 2021]. The disjoint merge operator paves the way for a compositional style of statically typed programming where solutions to the expression problem [Wadler 1998] emerge naturally. A prototype programming language, called CP, illustrating this compositional programming style, has been implemented based on a core calculus with the merge operator [Zhang et al. 2021].

While disjoint intersection types prevent ambiguity, they are often too restrictive. The main issue is that disjointness requires all possible future upcasts to be unambiguous, limiting expressiveness, particularly for function overloading. For example, consider two functions 𝑓 and 𝑔 of types Int → String and Bool → String. Since they share a common supertype (Int & Bool) → String, their merge f ,, g is rejected under disjointness, as applying it to a value of type Int & Bool would be ambiguous. However, such strictness unnecessarily prevents valid cases , where a function call can be safely disambiguated by the calling context.

To overcome these limitations, we introduce type apartness , a relaxed alternative to disjointness. Apartness allows overlapping types as long as the overlapping parts remain distinguishable at the point of use. This is enough to prevent ambiguity while increasing flexibility. For example, under apartness, the merge f ,, g is accepted, and it can be applied unambiguously to an integer or a boolean. However, applying it to a merged argument, such as 1 ,, True, yields an ambiguous merge of 2 strings. Guarded subtyping complements apartness to detect ambiguity, by ensuring that all upcasts are safe. If a function application could produce an ambiguous result, guarded subtyping rejects the application. For example, guarded subtyping would reject (f ,, g) (1 ,, True) while allowing (f ,, g) 1.

Apartness also improves type difference [Xu et al. 2023], a conflict resolution method based on type subtraction. Under apartness, type difference becomes a total operation, in contrast to its partial nature under disjointness. This new formulation of type difference ensures that conflicts between types can always be resolved, enhancing the flexibility and expressiveness of the merge operator. Additionally, we introduce the concept of type normalization , which systematically handles unrestricted intersection types by transforming them into a canonical form where all intersections are apart. This process eliminates redundant and conflicting type components, ensuring that the resulting types are well-formed and unambiguous. Consequently, this provides greater flexibility and convenience for programmers, allowing them to write programs with unrestricted intersection types, which is particularly useful in scenarios involving multiple inheritance.

By combining type apartness with guarded subtyping and the new formulation of type difference, our approach provides the first calculus that supports function overloading [Castagna et al. 1995], return type overloading [Xue et al. 2022], extensible records [Reynolds 1988], and nested composition [Bi and Oliveira 2018], while preserving determinism. Unlike prior work [Xue et al. 2022], which supports these features but is non-deterministic, our approach ensures a fully deterministic calculus, making it more practical and robust. Our main contributions are:

• Type apartness , which enables function overloading, return type overloading, extensible records, and nested composition while maintaining determinism.

• A formalization of source and target calculi , proving their soundness and correspondence.

• A Coq formalization , verifying our results.

• A new formulation of total type difference , improving upon previous work [Xu et al. 2023].

2 Overview

We aim to develop an expressive and deterministic calculus that supports four key features: function overloading , return type overloading , extensible records , and nested composition . This section provides background information and demonstrates how apartness and guarded subtyping enable a solution

Proc. ACM Program. Lang., Vol. 9, No. OOPSLA2, Article 279. Publication date: October 2025.

--- end of page.page_number=2 ---

Liberating Merges via Apartness and Guarded Subtyping

279:3

class Deck { public: virtual void draw() { std::cout << “Draw a card.” << std::endl; } }; class Drawable { public: virtual void draw() { std::cout << “Create a blank canvas.” << std::endl; } }; class DrawableDeck : public Drawable, public Deck {}; // This class is accepted! int main() { DrawableDeck dd; static_cast<Deck&>(dd).draw(); // Output: Draw a card. dd.draw(); //error: request for member ‘draw’ is ambiguous return 0; } Fig. 1. C++’s relaxed approach to conflict resolution.

that supports all these features while ensuring determinism. We also highlight the role of type well-formedness and type normalization in constructing sound calculi with apart merges.

2.1 C++ Method Resolution: A Source of Inspiration

Name, method, and class conflicts frequently arise in programming languages. Various approaches exist to resolve such conflicts, including forbidding redefinitions or overriding previous definitions. For instance, in many object-oriented languages, defining two methods with the same name (and signature) in the same class is (rightfully) prohibited. A related situation arises in multiple inheritance, when two parent classes define a method with the same name. A common approach is to reject such programs entirely, which avoids ambiguity but can be overly restrictive. Conservative strategies for conflict resolution limit the expressiveness of a language by disallowing many useful programs. To mitigate this, some languages take a more flexible approach by delaying conflict resolution until a method or value is used.

The relaxed conflict resolution approach of C++. A well-known example of delayed conflict resolution is found in C++’s multiple inheritance model. To illustrate, we adapt an example from Wang et al. [2018]. In Fig. 1, we develop two components Deck and Drawable in one system. Deck implements a deck of cards and defines a method draw for drawing a card from the deck. Drawable is an interface for graphics and also implements a method called draw for visual display. We happen to encounter a name conflict when we implement the derived class DrawableDeck. Here C++ adopts a delayed approach to conflict resolution. Instead of rejecting DrawableDeck at the point of definition, it defers ambiguity detection to the method’s use site. If a method call is unambiguous, it proceeds as usual. However, calling dd.draw() is ambiguous because both Deck::draw and Drawable::draw are valid candidates, causing the compiler to reject the call. Nonetheless, ambiguity can be resolved by explicitly upcasting dd to a parent class, as shown in static_cast<Deck&>(dd).draw(). Such a conflict resolution strategy not only accepts a broader range of safe programs, but also allows users to use classes and methods polymorphically. Inspired by this approach, we adapt similar ideas to calculi based on intersection types and the merge operator [Dunfield 2014; Oliveira et al. 2016].

2.2 Background

The merge operator, coercive subtyping and intersection types. The merge operator [Dunfield 2014; Reynolds 1988] generalizes record concatenation to concatenation of arbitrary terms. It composes terms and allows implicit elimination based on types. For example, the following merge 1 ,, True ,, not (not is a function representing the negation on booleans) is well-typed. The type of this merge is the intersection type Int & Bool & (Bool → Bool).

Proc. ACM Program. Lang., Vol. 9, No. OOPSLA2, Article 279. Publication date: October 2025.

--- end of page.page_number=3 ---

Han Xu, Xuejing Huang, and Bruno C. d. S. Oliveira

279:4

Table 1. Four applications of the merge operator with examples.

Features	Examples	Previous Works
Function overloading	showInt_,,_showBool	Castagna et al.[1995];Dunfeld[2014];Xue et al.[2022]
Return type overloading	readInt_,,_readBool	Marntirosian et al.[2020];Xue et al.[2022]
Nested composition	({l =“hello”},,{l =1}).l	Reynolds[1988];Xue et al.[2022];Zhang et al.[2021]
Extensible records	{l_1 =“hello”},,_{_l_2 =“world”}	Bi et al. [2018]; Huang et al. [2021]; Xue et al.[2022]

Calculi with a merge operator use a coercive interpretation [Luo 1999; Reynolds 1991] of subtyping, instead of the traditional subsumptive interpretation of subtyping. In the coercive view, each subtyping judgment denotes an implicit conversion function. When a value is used in a context that expects a supertype, it is coerced by the corresponding function. Typically (and in our setting) the conversion function is injective , which means that information can be lost when converting a value to another value of a supertype. For example, in our setting the maximal type ⊤ (Top) has only one canonical value; every type is a subtype of ⊤, and every expression is converted into the top value when ⊤ is required. This is unlike subsumptive subtyping, which reflects the intuition that types correspond to sets of values, and the values of a subtype and its supertype are in a subset relation. This implies that subsumptive subtyping does not have runtime effects, and leads to the safe substitution principle [Liskov and Wing 1994]. Reynolds referred to the two interpretations as intrinsic semantics and extrinsic semantics of subtyping [Reynolds 1998]. Coercive subtyping is considered to match the intrinsic view of types because the meaning of an expression depends on how it is typed. With subsumptive subtyping, a value can be assigned multiple types.

Coherence is a key property in coercive subtyping: while multiple derivations exist for one subtyping conclusion, they are supposed to produce equivalent coercions. This is important for the language semantics to be independent from how a type derivation for an expression is constructed. Proving coherence is tricky, and intersection types make it harder. Consider types A and B that share a supertype C : for any subtype of A & B , there are at least two paths that lead to C , one through A and the other through B , which may lead to possible ambiguity. Intersection types are also studied under the subsumptive interpretation with a set-theoretic model [Frisch et al. 2008]. In this model, there is no term of the type Int & Bool because Int and Bool do not share any values. But with the merge operator, we can construct terms such as 1 ,, True explicitly. Coercions arising from upcasts may have a runtime effect. In addition, any coercion to the ⊤ type is safe as ⊤ represents a singleton value. For example, the merge operator with disjoint intersection types [Huang et al. 2021; Oliveira et al. 2016] adopts the following semantics:

(1 ,, True) : Int ↩ → 1 (1 ,, True) : ⊤ ↩ →⊤ ( 𝜆[Int][→][Int] x. x ) (1 ,, True) ↩ → 1

Upcasts have a runtime effect as they drop components from the merge. To be clear in the following discussions, we say that two coercions are equivalent when they reach the same value in the end, even if the sequence of evaluation steps dropping components may be different. We say that there is a unique coercion from one type to another when all possible coercions are equivalent.

Applications of merges. The merge operator has several applications. We summarize four applications, identified by Xue et al. [2022], in Table 1. The last entry of the table identifies works in the literature that build on such applications. We briefly explain these applications next.

Proc. ACM Program. Lang., Vol. 9, No. OOPSLA2, Article 279. Publication date: October 2025.

--- end of page.page_number=4 ---

Liberating Merges via Apartness and Guarded Subtyping

279:5

• Function overloading. Function overloading is one kind of polymorphism, which allows choosing functions or methods according to the type or argument being applied to. For example, function overloading can choose showInt or showBool according to the argument that is applied.

  • (showInt ,, showBool) 1 ↩ → “1”

(showInt ,, showBool) True ↩ → “True”

• Return type overloading. Return type overloading is a feature that enables choosing an implementation from a merge depending on the context involved. A classic example is the read function in Haskell. Like show, we can define a version of read with the merge operator as

read : (String → Int) & (String → Bool) = readInt ,, readBool

It is possible to disambiguate calls to read from the use context. For example, (read “1”) + 1 should select readInt, since an integer is expected from the use of read.

• Nested composition. Nested composition reflects the distributivity behaviour of intersection types at the term level. Merges with nested composition were first proposed by Bi et al. [2018], allowing distributive extraction of nested terms such as

({ 𝑙 = “hello”} ,, { 𝑙 = 1}) .𝑙 ↩ → “hello” ,, 1

Nested composition serves as a key feature in Compositional Programming [Zhang et al. 2021]. Techniques based on nested composition help solving modularity problem such as the Expression Problem [Wadler 1998] and also enable forms of family polymorphism [Ernst 2001].

• Extensible records. Extensible records were among the first applications of merges [Reynolds 1988]. The key observation is that multi-field records can be simply encoded as merges of single-field records, such as:

{ l 1 = “hello” , l 2 = “world”} ≜ { l 1 = “hello”} ,, { l 2 = “world”}

The merge of single-field records should have the same behaviour as a multi-field record. That is to say, the merge should project the associated content of the single field that is designated.

Problem: Ambiguity of merges. Though the merge operator is powerful and expressive, without restrictions it easily leads to ambiguity. In Dunfield [2014]’s calculus, we can merge two arbitrary terms e 1 and e 2 together. Then a non-deterministic semantics of merge operator e 1 ,, e 2 is adopted where e 1 ,, e 2 can be evaluated to either e 1 and e 2. Thus, for example, we can have the following non-deterministic evaluation for the same expression:

Note that both (1 ,, 2) ↩ → 1 and (1 ,, 2) ↩ → 2 are type-safe here. However, such cases mean that reduction is ambiguous, as multiple results are possible.

Disjoint intersection types. To address the problem of ambiguous merges Oliveira et al. [2016] proposed disjoint intersection types. The idea is that only merges of expressions with disjoint types are allowed. The design philosophy of disjoint intersection types is that a merge should be able to be used in any context that expects a supertype of its type. A typical example of a context is being wrapped with a type annotation. Consider f and g as two functions. For (f ,, g) : ⊤→ Bool to exhibit unambiguous behavior, it needs to select either f or g. If their types are disjoint , they cannot share a common supertype like ⊤→ Bool, meaning that only one of them can be used to determine the behavior. Therefore casting a merge to any supertype is acceptable. This idea leads to the definition of disjointness in the line of work on disjoint intersection types [Oliveira et al. 2016]:

Proc. ACM Program. Lang., Vol. 9, No. OOPSLA2, Article 279. Publication date: October 2025.

--- end of page.page_number=5 ---

Han Xu, Xuejing Huang, and Bruno C. d. S. Oliveira

279:6

Definition 2.1 (Disjointness Specification). A ∗ 𝑑 B ≜ ∀ C, if A ≤ C ∧ B ≤ C, then ⊤≤ C.

If the only common supertype between two types is the top type (and types that are equivalent to top), then the only value that can have both types is the canonical top value (i.e. in the coercive interpretation the top type is interpreted as a unit type). Other values can either have type 𝐴 or 𝐵 but not both types at once. With disjointness, we can unambiguously extract each (non-⊤) component under different type contexts.

Next we show a few more examples to illustrate disjointness on different types.

𝐴 = Int 𝐵 = Bool Disjoint (no common non-top supertype) 𝐴 = Int & String 𝐵 = Bool & String Common supertype: String 𝐴 = Int → String 𝐵 = Bool → String Common supertype: Int & Bool → String Only in the first example the types Int and Bool are disjoint with each other, as their only common supertype is ⊤. But the subsequent two examples are not as we can find a common supertype for them. To guarantee that upcasting is always valid and type-safe, semantically different components in merges cannot share any supertype, except for types that are equivalent to ⊤.

Definition 2.2 (Type Equivalence). A = 𝑠 B ≜ A ≤ B ∧ B ≤ A .

Limitations of disjointness. While disjointness is a valuable approach, it comes with limitations. For instance, disjointness prevents conventional function overloading, such as:

show = (showInt : Int → String) ,, (showBool : Bool → String)

Here, this merge is not disjoint because the return type is the same. Thus, we can find a common supertype, such as Int & Bool → String, which would make extracting one of the functions ambiguous (both functions could be extracted). A limitation of disjointness is that it tries to ensure that all future casts on the merge are unambiguous. While this is a nice property to have, in some cases, like the above, it is too limiting. For example, we can use the merge above without ambiguity as:

show 1 ↩ → “1” show True ↩ → “True”

The argument 1 and True can uniquely determine the function we want to apply is showInt or showBool. Ambiguity should be triggered in cases such as:

show (1 ,, True) ↩ → “1” show (1 ,, True) ↩ → “True” show (1 ,, True) ↩ → “1” ,, “True” Here 1 ,, True can be an argument to both showInt and showBool. Disjointness rejects many forms of overloaded functions because of this issue, and calculi with disjoint intersection types cannot fully support overloading. More generally, there is currently no deterministic calculus with merges that supports all four features in Table 1.

2.3 Apartness: Relaxing Disjointness

To admit a wider range of useful programs, and support all four features in Table 1, we introduce apartness. Apartness replaces disjointness and delays the ambiguity check in some cases. Fig. 2 graphically contrasts apartness and disjointness. Disjointness accepts no ambiguity at all, while apartness allows some levels of ambiguity like showInt ,, showBool, even if there is a common supertype Int & Bool → String. Though apartness is more relaxed, it does not allow ambiguity where one type completely shadows (i.e., it is a subtype of) the other. The term shadowing denotes that a value of subtype A can always be used in place of a value of supertype B under the coercive subtyping view described in Section 2.2. When type A shadows B it is impossible to have a context that extracts the term of type B without matching the term of type A .

Proc. ACM Program. Lang., Vol. 9, No. OOPSLA2, Article 279. Publication date: October 2025.

--- end of page.page_number=6 ---

Liberating Merges via Apartness and Guarded Subtyping

279:7

----- Start of picture text -----
Int & Bool
Int Bool ⊤→ Bool Int→Bool Int→String → Bool→String
String
----- End of picture text -----

Fig. 2. Cases: A disjoint with B , A (completely) shadows B , and A apart (or partly overlaps) with B .

For instance, the merge 1 ,, 2 ,, True is ambiguous when it is used as a value of type Int and there is no supertype that can be used to remove ambiguity for extracting an integer. Thus, in this case, apartness (as well as disjointness) rejects the merge.

Guarded subtyping. By shifting from disjointness to apartness, we gain the ability to support function overloading. In such cases, the ambiguous casts can still be rejected later by our type system, through the guarded subtyping relation. From a coercive point of view, the subtyping relation denotes the existence of a coercion, while guarded subtyping denotes the existence of a unique coercion. Thus, both (showInt ,, showBool) : Int & Bool → String and (showInt ,, showBool)(1 ,, True) are ill-typed. Apartness accepts merges if there are casts that allow us to extract every piece of information in the merge. For the show example, we can find casts that can extract both functions:

show : Int → String (extracts showInt)

show : Bool → String (extracts showBool)

So the show merge should be accepted. However, if we have:

badShow1 = (showInt1 : Int → String) ,, (showInt2 : Int → String)

badShow2 = (showInt1 : Int → String) ,, (showInt2 : (Int & String) → String)

we should reject those merges. In the first case we cannot extract showInt1 or showInt2 without ambiguity. In the second case, we can extract showInt1 without ambiguity using badShow2 : Int → String. However, we cannot extract showInt2 without ambiguity, since badShow2 : (Int & String) → String is ambiguous and can match both showInt1 and showInt2. Apartness only guarantees that we can choose components from a merge depending on the context. In contrast, disjointness guarantees that we can choose a component regardless of the context. Nevertheless, apartness (with guarded subtyping) is still able to achieve determinism, as we shall see later in Section 2.4.

Encoding records via overloading. An advantage of apartness is support for a more lightweight encoding of records via first-class labels [Leijen 2004] and function overloading. This encoding of records was first proposed by Castagna et al. [1995]. In this encoding a record type { 𝑙 : 𝐴 } is viewed as a function type Sig l → A from a singleton type to the value. Such feature is helpful to simplify a calculus with the merge operator. The notable point is that such simplification is not possible with disjoint intersection types because merging Sig l 1 → Int with Sig l 2 → Int will be illegal since the functions have the same return type, like in the show example. Thus calculi with disjointness have to use the primitive record encoding as { 𝑙 1 : Int} and { 𝑙 2 : Int} to model multi-field records. With the weaker notion of apartness, we can simplify the record encoding inside the whole system, and model records as functions where the input type is the label to be projected.

2.4 Technical Overview

In this section, we will give a more technical overview towards the key design and mechanisms for apartness, guarded subtyping as well as the features in source and target calculi.

Proc. ACM Program. Lang., Vol. 9, No. OOPSLA2, Article 279. Publication date: October 2025.

--- end of page.page_number=7 ---

Han Xu, Xuejing Huang, and Bruno C. d. S. Oliveira

279:8

Apartness specification. For apartness, the specification becomes harder, compared to disjointness. We need to specify that if type A is apart with type B , then every type component inside A and B should not shadow or be a subtype of the other. We define a (minimal) type component through the notion of a minimal ordinary type MinOrd B A , which states that type B is a type component (i.e., supertype and being non-intersection) of A . Here minimal is in terms of subtyping relations. We provide an intuition of MinOrd B A with some simple examples first:

A=	B=	MinOrd_B A_
Bool	⊤	✗as⊤is not a minimal component (Boolcomponent subsumes it)
Bool&String	String	�
Bool&String	Bool&String	✗as_B_is an intersection type

For type Bool, the only type component is Bool itself, while for type Bool & String, a type component can be either Bool or String. Note that an intersection type can never be a minimal type component. Next we show some more complex examples, where A and B themselves contain overlapping or shadowing.

A=	B=	MinOrd_B A_
(Int→String)&(Bool→String)	Int→String	�
(Int→String)&(Bool→String)	(Int&Bool) →String	✗
(Int→String)&((Int&Bool) →String)	Int→String	�

For (Int → String) & (Bool → String), the type component can be either Int → String or Bool → String. But the supertype Int & Bool → String cannot be a type component as it completely shadows (is the supertype) of Int → String. The type (Int → String) & ((Int & Bool) → String), is equivalent to the type Int → String in terms of the subtyping relation. Thus the type component can only be Int → String. We can now give a formal definition of MinOrd:

Definition 2.3 (Minord). MinOrd B A ≜ B[◦] ∧ A ≤ B ∧(∀ C, if C[◦] ∧ A ≤ C ∧ C ≤ B, then B ≤ C ) .

Here B[◦] denotes an ordinary type (i.e. B cannot be an intersection type), and A ≤ B restricts B to be a supertype of A . The condition stating that if A ≤ C ∧ C[◦] ∧ C ≤ B, then B ≤ C , suggests that B is a minimal type component of A as any other type that satisfies the same requirement should be equivalent to type B . With MinOrd we can give the specification of apartness:

Definition 2.4 (Apartness Specification). A ∗ 𝑠 B ≜ ∀ C 1 C 2 , if MinOrd C 1 A ∧ MinOrd C 2 B , then either C 1 = ⊤ or C 2 = ⊤ or (¬( C 1 ≤ C 2) ∧¬( C 2 ≤ C 1)).

Such specification checks that all the type components C 1 in A and C 2 in B do not contain any shadowing (¬( C 1 ≤ C 2) ∧¬( C 2 ≤ C 1)), unless one of them is ⊤.

Guarded subtyping and lack of transitivity. Since apartness is guaranteed through merges, and it delays the check of ambiguity in some cases, we need another relation that performs a final safety check to ensure no ambiguity. This check is done via the guarded subtyping relation A ≾ B . The guarded subtyping relation A ≾ B is a restricted version of subtyping that ensures that a coercion from type A to type B is unique .

Unlike the usual subtyping relation, the guarded subtyping relation A ≾ B is not transitive. This means that even if A ≾ B and B ≾ C , it does not necessarily follow that A ≾ C . For example:

(Int → String) & (Bool → String) ≾ (Int → String) (Int → String) ≾ (Int & Bool → String) ¬((Int → String) & (Bool → String) ≾ Int & Bool → String)

Proc. ACM Program. Lang., Vol. 9, No. OOPSLA2, Article 279. Publication date: October 2025.

--- end of page.page_number=8 ---

Liberating Merges via Apartness and Guarded Subtyping

279:9

(Int → String) & (Bool → String) is a guarded subtype of Int → String, and Int → String is a guarded subtype of Int & Bool → String. However, (Int → String) & (Bool → String) is not a guarded subtype of Int & Bool → String because both components in the intersection are subtypes of Int & Bool → String. This demonstrates that directly replacing a type annotation with its guarded supertype can lead to ill-typed programs.

Consequently, more type information needs to be preserved at runtime to ensure type correctness. We address this by allowing type annotations to be accumulated within function-like values. By keeping track of intermediate types, we ensure that a unique path exists for future welltyped function application. To make this concrete, suppose we have a function annotated as 𝜆[A][→] [A][′] x. e : ( B → B[′] ) : ( C → C[′] ), even though the function itself is uniquely determined (there is no ambiguity that 𝜆[A][→] [A][′] x. e implements C → C[′] and we do not need to choose from merges of functions), we cannot drop B → B[′] because B maintains the path for converting the function argument from C to A , and B[′] is essential for converting the function application result as well.

Transitivity, determinism, and flexibility. In sufficiently rich type systems with merges, achieving transitivity, determinism, and flexibility simultaneously often proves impossible. Prior work illustrates this tension through different design trade-offs: Dunfield [2014]; Xue et al. [2022]’s calculi preserve flexibility and transitivity but sacrifice determinism; calculi based on disjoint intersection types [Oliveira et al. 2016] maintain transitivity and determinism by sacrificing flexibility. Our work takes a different approach by sacrificing transitivity to preserve determinism and flexibility. There is an analogous issue in gradual type systems, in calculi like the blame calculus [Wadler and Findler 2009]. Gradual typing systems use a consistency relation (∼) that checks the compatibility of types by relaxing equality, accepting an unknown type ( ★ ) in type components. However, this relation is inherently non-transitive. For example:

Gradual typing systems also employ a consistent subtyping relation (≲) that combines subtyping with type consistency. While ≲ supports flexibility by allowing some loss of information, it too is non-transitive. For instance:

𝐼𝑛𝑡 ≲ ★ is true, ★ ≲ 𝐵𝑜𝑜𝑙 is true, but 𝐼𝑛𝑡 ≲ 𝐵𝑜𝑜𝑙 is false.

This trade-off between flexibility and transitivity is discussed by Siek and Taha [2007]. By dropping transitivity, we align with these established principles, ensuring determinism and flexibility without sacrificing type safety.

Type well-formedness. To achieve a calculus with the desirable properties of determinism and flexibility, we impose well-formedness constraints on types. These constraints ensure that types are constructed in a manner that avoids ambiguities, since all types in intersections must be apart. Well-formedness disallows unrestricted intersections such as Int & Int because they can lead to non-deterministic behavior when merged values are projected in different contexts. Moreover the use of guarded subtyping, instead of subtyping, prevents any remaining ambiguity arising from types that are apart, but overlapping. The calculus presented in Sec. 4 adopts this design with type well-formedness and is proven to be both type safe and deterministic.

Type normalization and unrestricted intersections. While well-formedness constraints are a simple way to ensure determinism, there are compelling reasons to allow unrestricted intersection types in a language with merges. Unrestricted intersection types provide greater convenience for programmers by enabling more expressive and flexible type constructions. For instance, in a language with unrestricted intersections we can write 1 : Int & Int, but there is still an apartness check on merges, so the terms (1 ,, 2) : Int & Int or (1 ,, 1) : Int & Int would be forbidden. Unrestricted intersection

Proc. ACM Program. Lang., Vol. 9, No. OOPSLA2, Article 279. Publication date: October 2025.

--- end of page.page_number=9 ---

Han Xu, Xuejing Huang, and Bruno C. d. S. Oliveira

279:10

----- Start of picture text -----
A:
{x: Int}
B: C:
{x: Int, y: Bool} {x: Int, z: Char}
D:
{x: Int, y: Bool, z: Char}
----- End of picture text -----

Fig. 3. Interface inheritance hierarchy with unrestricted intersections.

types are useful, but we need to be careful to make them safe during coercions. For example, 1 : Int & Int can be safely uniquely coerced into the term 1 ,, 1, but 1 ,, 1 is not well-formed as it represents multiple choice of 1 on both sides of the merge. Instead of forbidding such terms in the first calculus 𝜆 ∗, in second calculus 𝜆 |∗| we normalize types into a well-formed canonical form, and then coerce the terms with normalized types. This calculus 𝜆 |∗| , which is presented in Sec. 5, does not have type well-formedness restrictions and allows unrestricted intersections.

The unrestricted type system allows types like Int & Int. Such non-apart types are especially useful in modeling object-oriented programming style multiple (interface) inheritance. For example, consider the following class hierarchy in Fig. 3. In this scenario, it would be useful to use B & C to denote the type of class D . However, the intersection B & C is not apart, so it is not possible to use B & C to denote the type D in the calculus with type well-formedness. It could be cumbersome to manually write the type D directly or using type difference/annotations to resolve the conflict [Xu et al. 2023]. Instead, the calculus with normalization allows programmers to more naturally and intuitively express the combination of multiple inherited types directly as type B & C .

To enable unrestricted intersections, we need to normalize types into a well-formed canonical form. For instance, a type like Int & (Bool & Int) can be normalized to Int & Bool, which is a wellformed type under the type system in Sec. 4. Similarly, we could normalize B & C to end up with the type D . Before type checking and execution, we translate programs from the source calculus 𝜆 |∗| in Sec. 5 to the target calculus 𝜆 ∗ in Sec. 4. The target calculus 𝜆 ∗ enforces stricter well-formedness constraints and ensures that all types are normalized. Notably this translation process shows that, while there is a restriction on types in the target calculus 𝜆 ∗, no expressive power is lost by this restriction on type well-formedness. The unrestricted syntax of intersection types has been given a constrained meaning by translation to well-formed intersection types, established by type normalization and a value-to-value mapping between 𝜆 |∗| and 𝜆 ∗ in Sec. 5.

Type difference as type normalization. Type difference is an approach to conflict resolution proposed by Xu et al. [2023] to eliminate conflicts between terms of type A and type B . This mechanism for conflict resolution is based on coercive subtyping. In our calculus, type annotations can be used to manually resolve conflicts arising from overlapping types. For example, consider the variables x of type Int & Bool and y of type Int & String. Attempting to merge x and y (i.e., x ,, y ) results in a conflict because they share the type Int. To resolve this conflict, we can use type annotations to explicitly exclude the conflicting type from either x or y :

While type annotations effectively resolve conflicts, they can become impractical with large or complex types, requiring extensive manual annotations. For instance, with multiple inheritance,

Proc. ACM Program. Lang., Vol. 9, No. OOPSLA2, Article 279. Publication date: October 2025.

--- end of page.page_number=10 ---

Liberating Merges via Apartness and Guarded Subtyping

279:11

we may need to resolve conflicts in C 1 and C 2 when merging them:

e1	of	type:	e2 of type:	e2 of type:
C1	=	{ l1:Int,	C2 =	{ l1:Bool,
		l2:Bool,		l2:Bool,
		…		…
		ln1:String→Int		ln2:Bool→Int,
};			}

Manually resolving such conflicts becomes laborious and sometimes extremely hard. To address such problems, type difference was designed to automate the annotations needed, enabling us to programmatically exclude conflicting parts without verbose annotations. Using type difference, we can resolve conflicts succinctly:

where e \ A suggests removing all the type A components from e , and e 1\ e 2 suggests removing all conflicting parts of e 1 and e 2 from e 1.

Though Xu et al.’s type difference is expressive, it is not total. Type difference under disjointness cannot resolve all the merge conflicts. For example, if we have type Int → String and Bool → String, Xu et al.’s type difference cannot find a type C = (Int → String)(Bool → String) such that C is mergeable (disjoint) with Bool → String, while keeping all the other information in type Int → String. In their work, Xu et al. proposed a specification for type difference, denoted as A \ 𝑠 B = 𝐶 , along with a partial algorithm that is sound and complete with respect to this specification. In contrast, our work introduces a relaxation of disjointness using a one-sided apartness relation A < ∗ B . This relation ensures that the type components of B are not shadowed by those of A , but not necessarily vice versa (formally defined in Definition 6.1). Under this relaxed notion, we obtain a total specification for type difference. Besides, we present type normalization as a different algorithm that is both sound and complete with respect to the new specification. In this framework, a type A is normalized to | A | through an auxiliary process that normalizes one type with respect to another, denoted | A | B . Full normalization is a special case: | A |⊤, which resolves all conflicts in A relative to the top type.

Type normalization | A | B is sound and complete with respect to the new type difference specification: A \ 𝑠 B = | A | B , and for all C , if A \ 𝑠 B = C , then C ≤| A | B and | A | B ≤ C . Importantly, under our new formulation, | A | B is algorithmic and total, and provides an algorithm for type difference. All conflicts in two non-apart types can be resolved by applying type normalization twice: first compute | A | B , then compute | B | | A | B .

3 Apartness and Guarded Subtyping for Intersection Types

This section shows how to derive algorithmic formulations of apartness and how to formulate guarded subtyping with intersection types and a merge operator.

3.1 Syntax and Subtyping

Types. Our type syntax follows the syntax of 𝜆[+] 𝑖[by][ Huang et al][.][ [][2021][], extended with a bottom] type and a singleton type. The top and bottom types are crucial here to support type difference and normalization, as suggested by Xu et al. [2023]. Singleton types Sig l are included for encoding record types. A labelled type (or single-field record type) { 𝑙 : 𝐴 } is represented by the function type Sig l → A . A multi-field record type is then represented as an intersection of labelled types. A record type is an overloaded function, where the input type is the label to be projected.

Proc. ACM Program. Lang., Vol. 9, No. OOPSLA2, Article 279. Publication date: October 2025.

--- end of page.page_number=11 ---

Han Xu, Xuejing Huang, and Bruno C. d. S. Oliveira

279:12

||||Types|||||||||||𝐴, 𝐵,𝐶_�Int|𝐴, 𝐵,𝐶_�Int|𝐴, 𝐵,𝐶_�Int|| ⊤| ⊥|A|&B|A_→_B|Sig_l|&B|A_→_B|Sig_l|&B|A_→_B|Sig_l|&B|A_→_B|Sig_l_| |---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---| ||||Ordinary Types||||||||||A_◦, B_◦_, C_◦�Int||||| ⊤| ⊥|A||→_B_◦|Sig|l|| ||||Labelled type encoding|||||||||||{𝑙:𝐴} ≜Sig|||l →_A_||||| ||||Record encoding||||||||{𝑙_1|:𝐴_1, |… , |𝑙𝑛:𝐴𝑛} ≜{𝑙_1|||:𝐴_1}& . .|. &{𝑙𝑛:𝐴𝑛}|||| ||𝐴_≤_𝐵|||(Declarative BCD Subtyping)|||||||||||A <:B||||(Algorithmic BCD Subtyping)||| ||||||||||||||||||||||| |||A|≤_A_|⊥≤_A_|||||A|≤⊤|||||A <:A|||⊥_<:A|||A <:⊤| ||B ≤_A
C ≤_D_|||||A ≤_B_||||B|≤_C_|||||C_◦
D_◦|||B <:A|C <:D|| ||A_→_C ≤_B_→_D||||||A||≤_C||||||||A_→_C <:B_→_D||||| ||||||A|≤_B_1|||A ≤_B_2||||||||_A_≃_A_1&_A_2
𝐴𝑖<:B||||| ||_A_1||&A_2 ≤_𝐴𝑖|||A ≤_B_1|||&|B_2|||||||||A <:B||| ||||||||||||||||B_≃_B_1&B_2||||A <:B_1|A |<:B_2| |||(A_→_B_1)&(A||→_B_2)|≤_A_→(B_1&B_2)||||||||||||||A <:B||| ||⊢_𝑠A||||||||(Type Well-Formedness (Strict))||||||||A_≃_B&C|||(Type Splitting)|| |||||||||||||⊢_𝑠A|⊢_𝑠B||B_◦||||A&B_≃_A&B||| |⊢_𝑠_Int|||⊢_𝑠_Sig_l|⊢_𝑠_⊥||||⊢_𝑠_⊤|||||⊢_𝑠A_→_B||||||||| ||||||||||||||||||||B_≃_B_1&B_2||| ||||⊢_𝑠A
⊢_𝑠B|||_A_≠⊤||||B_≠⊤||A|∗_B||||A_→_B|≃(_A_→_B_1)||&(A_→_B_2)|| |||||||⊢_𝑠A&B||||||||||||||||

Fig. 4. BCD subtyping, ordinary types, splittable types and the strict type well-formedness.

Subtyping, ordinary and splittable types. BCD subtyping [Barendregt et al. 1983] is a widely used subtyping relation for intersection types. BCD subtyping includes common intersection type rules that ensure the commutativity ( A & B ≤ B & A ) and associativity ( A & ( B & C ) ≤( A & B ) & C ) of subtyping, which allows us to handle multi-field record types as intersection types without any loss of precision. The most important feature of BCD-style subtyping is that it allows function types to distribute over intersection types. We have all the types in the original BCD type system. The declarative subtyping rules, presented at Fig. 4, extend BCD subtyping with rules for singleton types and the bottom type, but exclude the top arrow rule ⊤≤⊤→⊤, which does not appear to be particularly practical—though such a rule can be added with a valid coercion. The extension of singleton and bottom types is easy as they do not interact with the intersection subtyping rules.

On the right of the middle of Fig. 4 shows an algorithmic formulation of subtyping, that eliminates transitivity and is equivalent to the declarative formulation [Huang et al. 2021]. This algorithmic formulation relies on two notions, ordinary types and splittable types , which are shown in Fig. 4. Ordinary types [Davies and Pfenning 2000], are types that do not contain top level intersections. In BCD subtyping, arrow types such as A → B & C may behave like intersection types due to distributivity. In the algorithmic formulation ( A < : B ) of subtyping ( A ≤ B ) we restrict the notion of ordinary types to exclude such types. Splittable types are the complement of ordinary types. Type splitting separates the intersection components inside intersection-like types. Though a splittable type may not always have intersection at its top-level, the type is still equivalent to an intersection. To fully analyze the subtyping behaviour, we define splittable types as shown in Fig. 4.

Proc. ACM Program. Lang., Vol. 9, No. OOPSLA2, Article 279. Publication date: October 2025.

--- end of page.page_number=12 ---

Liberating Merges via Apartness and Guarded Subtyping

279:13

3.2 Type Well-Formedness

Type well-formedness ensures that a type always has at most one unique coercion to another well-formed type. These conditions, along with the guarded subtyping introduced later in Sec. 3.4, prevent the casting result from being ill-typed. Type well-formedness is algorithmic, and therefore uses the algorithmic apartness in Sec. 3.3 instead of apartness specification A ∗ 𝑠 B in its definition.

We will motivate the design of type well-formedness through an intersection type example. First, we want to avoid overlap within types, specifically avoiding situations where A & B exists without A ∗ B . For example, Int & Int leads to ambiguity inside types, since there is more than one coercion to type Int. Second, to ensure that coercions are unique, we require that the splitting results of the type are always apart. In particular, for a type like A → B & C , we need ( A → B ) ∗( A → C ) given that A → B & C ≃( A → B ) & ( A → C ). This requires a more rigorous approach than simply checking the apartness of intersections structurally, as B ∗ C does not imply ( A → B ) ∗( A → C ). An example occurs when B equals ⊤. Function types like Int →⊤ & Bool may seem harmless if we only verify the apartness of the intersection in the function’s return type. However, it splits into overlapping types Int →⊤ and Int → Bool. To achieve an algorithmic version of apartness (shown in Figure 5) satisfying the requirement of uniqueness that every type component being apart, we introduce a type well-formedness definition that possesses the following properties:

Theorem 3.1 (Well-Formed Types have Apart Components). If ⊢ 𝑠 A, and A ≃ B & C, then A = B & C, B ∗ C, ⊢ 𝑠 B and ⊢ 𝑠 C .

With this property, we can later show completeness of the apartness algorithm in Sec. 3.3. Type well-formedness may seem restrictive here, as it requires arrow types (like A → B & C ) to be written in its equivalent form ( A → B ) & ( A → C ). However, this restriction will be partially resolved in Sec. 4 by relaxing well-formedness and fully resolved in Sec. 5 by transforming every type into a well-formed type by type normalization.

3.3 Apartness

Our goal is to define an algorithmic formulation of apartness that is equivalent to the specification in Sec. 2.4. Our algorithmic apartness relation ( A ∗ B ) is defined for BCD subtyping [Barendregt et al. 1983], and it essentially expresses that for types 𝐴 and 𝐵 , it is always possible to extract all the information from values of both types without ambiguity. To formally define apartness and ambiguity, we use an auxiliary relation A ≬ B that expresses whether two types A and B contain shadowing (i.e. if one’s component is a subtype of the other’s). We want to define our apartness A ∗ B based on the negation of the shadowing relation A ≬ B (i.e., A ∗ B = ¬( A ≬ B )).

Shadowing. The shadowing relation determines whether the type components of two types A and B shadow each other, and whether there is ambiguity between A and B . Some examples of types A and B and their shadowing relations are:

𝐴=Int	𝐵=Bool	¬(A ≬_B_)
𝐴=Int&Bool	𝐵=Bool	A ≬_B_
𝐴=Int	𝐵=⊤	¬(A ≬_B_)
𝐴=Int→String	𝐵=Bool→String	¬(A ≬_B_)
𝐴=Int→String	𝐵= (Int&Bool) →String	A ≬_B_

Most of these examples are straightforward. Notably, in the third example where B is ⊤, we consider ⊤ to have no type component. Therefore, shadowing of type A over type ⊤ cannot occur as the two types do not share any type component. Besides, ⊤ cannot shadow any type. The negation of this judgement then always allows the ⊤ type to be apart with any type.

Proc. ACM Program. Lang., Vol. 9, No. OOPSLA2, Article 279. Publication date: October 2025.

--- end of page.page_number=13 ---

Han Xu, Xuejing Huang, and Bruno C. d. S. Oliveira

279:14

_A_◦ B_≃_B_1&B_2 A ≬_𝐵𝑖 A ≬_B	_A_◦ _B_◦ A <:B B_≠⊤ A ≬_B	(Type Shadowing) _A_◦ _B_◦ B <:A A_≠⊤ A ≬_B

Fig. 5. Shadowing.

We provide an inductive definition of A ≬ B in Fig. 5. Ignoring the gray conditions, we can see that shadowing is defined when one type is a subtype of the other, or when any of their splitting components have a shadowing relationship. These gray-colored side conditions reduce overlap between the rules and help make the implementation more efficient. We have proved that adding these conditions leads to an equivalent definition. With these conditions, intersection-like types are always split, and only the ordinary components are compared in subtyping checks to decide whether there is a conflict. Now we can write our algorithmic apartness A ∗ B as ¬( A ≬ B ).

Soundness and completeness of algorithmic apartness. The formulation of apartness A ∗ B via the negation of A ≬ B is sound with respect to the specification A ∗ 𝑠 B given in Sec. 2.4. Completeness requires more work. We have (Int → String) ∗ 𝑠 (Bool → String) & ((Int & Bool) → String) but not (Int → String) ∗(Bool → String) & ((Int & Bool) → String). As suggested in Section 2.4, Int → String has one minimal ordinary type component, namely itself, while (Bool → String) & ((Int & Bool) → String) also has only one minimal ordinary type component Bool → String. Then, since the only type components are unrelated by subtyping, the specification apartness holds. However, for algorithmic apartness, we recursively decompose the types and try to find the subtyping relation between them. Therefore we do not have (Int → String) ∗(Bool → String) & ((Int & Bool) → String) for (Int & Bool → String) ≤ Int → String. To address such incompleteness, we introduce a notion of well-formed types ⊢ 𝑠 A which restricts intersections to apart types. Under this restriction, we are now able to formulate a form of completeness.

Theorem 3.2 (Soundness of Apartness). If A ∗ B, then A ∗ 𝑠 B.

Theorem 3.3 (Completeness of Apartness). If ⊢ 𝑠 A, ⊢ 𝑠 B, and A ∗ 𝑠 B, then A ∗ B.

3.4 Guarded Subtyping

Next we introduce the guarded subtyping relation. With disjointness, a term of type A can always be cast to a term of type B when A ≤ B , without introducing ambiguity. However, with apartness, this is no longer true. Since apartness allows more ambiguity, we need to have a notion to validate casting. The guarded subtyping relation is essentially a restricted version of subtyping. Unlike subtyping, guarded subtyping is not transitive .

Definition. Guarded subtyping, denoted as A ≾ B , ensures that a term of type A can be unambiguously cast to a term of type B . This unambiguity arises not merely because A is a subtype of B , but importantly because there is a unique way to coerce a value of type A into a value of type B . In other words, any value of type A can be unambiguously mapped to a value of type B .

To provide more intuition, we can illustrate the guarded subtyping with some concrete examples:

𝐴=	(Int→String)&(Bool→String)	𝐵=	Bool→String	A_≾_B
𝐴=	(Int→String)&(Bool→String)	𝐵=	(Int&Bool) →String	¬(A_≾_B)
𝐴=	(Int→String)&(Bool→String)	𝐵=	(Bool→String)&(Int→String)	A_≾_B
𝐴=	(Int→String)&(Bool→String)	𝐵=	String	¬(A_≾_B)
𝐴=	(Int→String)&(Bool→String)	𝐵=	⊤	A_≾_B

Proc. ACM Program. Lang., Vol. 9, No. OOPSLA2, Article 279. Publication date: October 2025.

--- end of page.page_number=14 ---

Liberating Merges via Apartness and Guarded Subtyping

279:15

	C-andL _B_◦ _A_≃_A_1&_A_2 A_1 ≾_B ¬(_A_2 <:B) A_≾_B C-andR _B_◦ _A_≃_A_1&_A_2 A_2 ≾_B ¬(_A_1 <:B) A_≾_B (_A_2 →_B_2)◦ _A_2 ≾_A_1 _B_1 ≾_B_2 _A_1 →_B_1 ≾_A_2 →_B_2 C-int Int≾Int	C-sig

Fig. 6. Guarded subtyping.

In the first example, we can find a unique coercion from (Int → String) & (Bool → String) to Bool → String, since only the term of type Bool → String can be coerced to a term of type Bool → String. However, when casting a term of (Int → String) & (Bool → String) to (Int & Bool) → String, we are unable to tell whether the resulting (Int & Bool) → String comes from the term that implements Int → String or the one that implements Bool → String. Therefore, it is rejected by the guarded subtyping relation. In the last three examples we consider cases where B is an intersection type, a type that is apart from A , and the type ⊤. For intersection type cases, we only need to check whether every type component in type B is a guarded supertype of A . For types that do not have a subtyping relation, such coercion is not permissible as terms of B cannot provide sufficient information to build a value of A . For the ⊤ type, as there is only one value ⊤ associated with it, mapping from any set of values to it is always unique and never leads to ambiguity.

Guarded subtyping is defined in Fig. 6. Rules C-andL and C-andR suggest that only one of the two parts of an intersection-like type could contribute to the supertype, otherwise ambiguity is introduced. For example, we are not able to choose from a merge of (Int → String) & (Bool → String) for the type (Int & Bool) → String. Note that these two rules use the negation of subtyping rather than guarded subtyping, since they are checking if there exists a unique path from the subtype to the supertype. If the condition is relaxed to be ¬( A 1 ≾ B ) or ¬( A 2 ≾ B ), we will be able to derive Int & Int & Int ≾ Int due to ¬(Int & Int ≾ Int). Rule C-and is unsurprising: when the supertype is an intersection-like type, the unique coercion exists when there exists unique coercions to both of its intersection components. Finally rules C-int, C-sig, C-top, and C-ord define the behaviour of casting for non-intersection types. The notable case is the function rule C-ord, where we also enforce that the relation is contravariant on the input types of functions.

Soundness. The guarded subtyping relation always leads to safe casting as the casting is an upcast, and there is no ambiguity. No casting from both A and B is available unless they are cast to type ⊤. Thus, no ambiguity is caused during casting.

Theorem 3.4 (Soundness of Guarded Subtyping). If A ≾ B, then A ≤ B.

Theorem 3.5 (Safe Casting). If A ∗ B and A ≤ C and B ≤ C, then ¬( A & B ≾ C ) or ⊤≤ C.

4 The 𝜆 ∗ Calculus

In this section, we introduce a lambda calculus with a merge operator, referred to as 𝜆 ∗. Similar to previous calculi featuring disjoint intersection types (e.g. F 𝑖[+][[][Fan][et][al][.][2022][]),] [𝜆][∗][uses][type] annotations to trigger dynamic casts that coerce values. These values are often aggregated through merges that are statically checked for conflicts. We will first explain how the type system employs the concept of apartness to validate merges and support overloaded functions. Following this, we will explore dynamic dispatching as demonstrated in the reduction rules.

Proc. ACM Program. Lang., Vol. 9, No. OOPSLA2, Article 279. Publication date: October 2025.

--- end of page.page_number=15 ---

Han Xu, Xuejing Huang, and Bruno C. d. S. Oliveira

279:16

(Syntax of Expressions)

|||Expressions|Expressions|Expressions|Expressions|||e �_x_|| i | ⊤| {l} | 𝜆A_→_Bx. e|| i | ⊤| {l} | 𝜆A_→_Bx. e|| fix_A x. e_ | e_1_e_2 ||e :A|| e_1,, e_2|| |---|---|---|---|---|---|---|---|---|---|---|---|---|---|---| |||Function-Like Values||||||u �_𝜆A_→_Bx. e | u:A_→_B||||||| |||Values||||||v �_u_|| i | ⊤| {l} | v_1,, |v_2||||| ||⊢_𝑟A|||||(Relaxed Type_||Well-Formedness)
⊢Γ|||(Well-Formedness of Typing Environments)|||| ||⊢_𝑠A_|⊢_𝑟A_|||⊢_𝑠B_||⊢_𝑟A_|⊢_𝑟B_|A_∗_B||⊢Γ
⊢_𝑟A_||x ∉domΓ|| ||⊢_𝑟A_|||⊢_𝑟A_|→_B_|||⊢_𝑟A_&B||⊢·||⊢Γ_, x_ :A||| ||Γ ⊢_𝑡e_ ⇔_A_||||||||||||(Typing|Rules of 𝜆_∗)| ||TTyp-top|||||TTyp-lit||TTyp-sig||TTyp-fix|||TTyp-anno|| |||⊢Γ||||⊢Γ|||⊢Γ|Γ, x_ :A_⊢_𝑡e ⇐_A_|||Γ ⊢_𝑡e_|⇐_A_| ||Γ|⊢_𝑡_⊤⇒⊤||||Γ ⊢_𝑡i_⇒Int||Γ ⊢_𝑡_{l} ⇒Sig_l_||Γ ⊢_𝑡_fix_A x. e_ ⇒_A_|||Γ ⊢_𝑡e_ :|A_⇒_A| ||||||||||TTyp-app||TTyp-merge||TTyp-sub|| ||TTyp-var||||TTyp-abs||||B_⊢_A_�_C||A_∗_B|||⊢_𝑟B_| |||⊢Γ||||⊢_𝑟A_|→_B_||Γ ⊢_𝑡e_1 ⇒_A_||Γ ⊢_𝑡e_1 ⇒_A_||Γ|⊢_𝑡e_ ⇒_A_| ||x :|A ∈Γ||||Γ_, x_ :A_⊢_𝑡e ⇐_B_|||Γ ⊢_𝑡e_2 ⇒_B_||Γ ⊢_𝑡e_2 ⇒_B_|||A_≾_B| ||Γ ⊢_𝑡x_ ⇒_A_||||Γ ⊢_𝑡𝜆A_→_Bx. ||e ⇒_A_→_B||Γ ⊢_𝑡e_1_e_2 ⇒_C_||Γ ⊢_𝑡e_1_,, e_2 ⇒_A_|&B|Γ|⊢_𝑡e_ ⇐_B_|

Fig. 7. The syntax, type well-formedness and typing rules for 𝜆 ∗.

4.1 Syntax and the Type System of 𝜆 ∗

Expressions and values. We define the syntax of expressions and values at the top of Fig. 7. Every function in 𝜆 ∗ must be accompanied by annotations, including the parameter and return type. These annotations can be nested layer by layer. We refer to lambdas with multiple annotation layers as function-like values and use the meta-variable u to represent them. In addition to functions, 𝜆 ∗ supports singleton values ({ l }), fixpoints (fix [A] x. e ) and merges ( e 1 ,, e 2). The top value ⊤ can be viewed as a merge with zero components.

Relaxed type well-formedness. We use a specially crafted type well-formedness definition in 𝜆 ∗, defined in the middle of Fig. 7. In the strict type well-formedness ⊢ 𝑠 A (see Fig. 4), intersections cannot contain ⊤, and arrow types A → B must enforce that the type B is a non-intersection type. The relaxed well-formedness ⊢ 𝑟 A loosens the strict criteria, allowing top types ⊤ to be intersected, and arrow types to have intersection types as the return types. Though the relaxed type well-formedness offers greater flexibility, its primary purpose is to enable a value-to-value mapping between 𝜆 |∗| and 𝜆 ∗. If a value in 𝜆 |∗| were mapped to a non-value in 𝜆 ∗, then the correspondence would also need to extend substitution in 𝜆 |∗| (with values) to substitution in 𝜆 ∗ (with non-values), making it nearly impossible to track equivalence between the source and target calculi.

To ensure this value-to-value mapping, function-like values are allowed to have only arrow type annotations, such as 𝜆[A][→] [B][ &] [ C] x. e . In contrast, annotations like 𝜆x. e : ( A → B ) & ( A → C ) are disallowed, as they could evaluate to a merge of functions, e.g., 𝜆[A][→] [B] x. e ,, 𝜆[A][→] [C] x. e , which is not a value in the target calculus. Therefore, it is crucial to permit arrow types that return intersections—such as A → B & C —to be well-formed, while avoiding intersection types at the top level of function annotations. Although relaxed type well-formedness admits more components, it remains safe due to completeness with respect to apartness. Moreover, it ensures that equivalent types can always be uniquely and safely coerced.

Theorem 4.1 (Soundness of Relaxed Well-Formedness). If ⊢ 𝑠 A then ⊢ 𝑟 A.

Proc. ACM Program. Lang., Vol. 9, No. OOPSLA2, Article 279. Publication date: October 2025.

--- end of page.page_number=16 ---

Liberating Merges via Apartness and Guarded Subtyping

279:17

	⊢Int � B_⊢Sig_l � A_1∗_B_1 D ⊢_A_�_A_1 D ⊢_B_�_B_1 D ⊢_A&_B_�_A_1&_B_1	B_⊢⊤� D ⊢_A_�_A_1 D ⊢_B � D ⊢_A_&_B_�_A_1	(Inapplicability) D ⊢_A_ � D ⊢_B_ � D ⊢_A_&B � (Type Dispatching) D ⊢_A_ � D ⊢_B_�_B_1 D ⊢_A_&_B_�_B_1
B

Fig. 8. The type dispatching relation for 𝜆 ∗.

Theorem 4.2 (Well-formed Types Respect Apartness). If ⊢ 𝑟 A and A ≃ B & C, then B ∗ C.

Theorem 4.3 (Completeness for Relaxed Well-Formedness). For all 𝐴𝐵 that ⊢ 𝑟 A and ⊢ 𝑟 B, if A ∗ 𝑠 B then A ∗ B.

Theorem 4.4 (Round-Trip Coercion). For all 𝐴𝐵, if ⊢ 𝑟 A, ⊢ 𝑟 B, A ≤ B, and B ≤ A, then A ≾ B.

Typing rules. As shown at the bottom of Fig. 7, a bidirectional type system [Dunfield and Krishnaswami 2021; Pierce and Turner 2000] is designed to characterize the static aspects of 𝜆 ∗. Its typing judgments operate in two modes: under inference mode ⇒, a unique type is deduced from the typing context for the expression; while in checking mode ⇐, the type is given (along with the typing context and the expression), and the expression is verified against the type. In our calculus, every typed expression has an inferred type (e.g. A ). Thus being checked (e.g., by B ) is equivalent to examining the subtyping relationship between A and B . All checked and inferred types are all guaranteed to be well-formed.

Theorem 4.5 (Typing Respects Type Well-Formedness). If Γ ⊢ 𝑡 e ⇔ A, then ⊢ 𝑟 A.

This formulation is also algorithmic, ensuring that no information is hidden via subtyping. In other words, we are fully aware of what e can contain from Γ ⊢ 𝑡 e ⇒ A . Therefore, we can determine that two expressions are free of conflicts simply by comparing their inferred types using apartness (defined in 3.3) in rule TTyp-merge. This approach is typical for type systems featuring disjoint intersection types with an unbiased merge operator. In such type systems, expressions can be composed via merging directly, as long as they do not create ambiguity, such as in 1 ,, True ,, f (f represents any legal function). Since apart types are not distinguishable in every possible context, our subsumption rule (rule TTyp-sub) is equipped with the guarded subtyping relation (defined in 3.4) to reject ambiguous casts. Merges can also be used directly as functions. For example, (f : Int → Bool) ,, (g : Bool → Bool) type-checks when applied to an integer or boolean argument. In rule TTyp-app, the two inference types of the applied term and the argument are passed to the type dispatching relation , which computes the return type.

Type dispatching. Type dispatching is defined in Fig. 8. In 𝜆 |∗| and 𝜆 ∗, type dispatching is only used for well-formed types. So, in the following text, we can assume the input type A and B are well-formed, and we try to get a well-formed type as return type.

First we define B ⊢ A � to denote that A cannot serve as a function type that takes a value of type B as an argument: there is no type C such that A < : B → C . For conciseness, We use B ⊢ A � to represent the negation of B ⊢ A �. We use the subtyping judgment in inapplicability instead of ¬( B ≾ A ) because we want to forbid all possible coercions instead of all unique coercions from B to A . Then we define the type dispatching relation B ⊢ A � C which does two more things: It computes the minimal return type, and also ensures that there is no ambiguity in the application process. B ⊢ A � C indicates that applying a term of type A to a term of type B should return a term

Proc. ACM Program. Lang., Vol. 9, No. OOPSLA2, Article 279. Publication date: October 2025.

--- end of page.page_number=17 ---

Han Xu, Xuejing Huang, and Bruno C. d. S. Oliveira

279:18

v 1 ↩ → A v 2 (Casting) A ≃ B & C v ↩ → B v 1 v ↩ → C v 2 u : A → B ( C → D )[◦] C < : A B < : D v ↩ → A v 1 ,, v 2 u ↩ → C → D u : C → D A[◦] v 1 ↩ → A v 1[′] A[◦] v 2 ↩ → A v 2[′] v 1 ,, v 2 ↩ → A v 1[′] v 1 ,, v 2 ↩ → A v 2[′] i ↩ →Int i { l } ↩ →(Sig l ) { l } v ↩ →⊤ ⊤ v 1 • v 2 ⇒ e (Parallel Application) B ⊢ A 1 � B ⊢ A 2� v 1 : A 1 v 2 : A 2 v : B v 2 : A v : B B ⊢ A � v 1 : A v : B B ⊢ A � v 1 ,, v 2 • v ⇒ ( v 1 v ) ,, ( v 2 v ) v 1 ,, v 2 • v ⇒ v 1 v v 1 ,, v 2 • v ⇒ v 2 v e 1 ↩ → e 2 (Small-Step Semantics for 𝜆 ∗ ) StepN-beta StepN-absanno StepN-papp v ↩ → A v[′] v ↩ → A v[′] ( v 1 ,, v 2 ) • v 3 ⇒ e ( 𝜆[A][→] [B] x. e ) v ↩ →( e [ x ↦→ v[′] ]) : B ( u : A → B ) v ↩ →( u v[′] ) : B ( v 1 ,, v 2 ) v 3 ↩ → e StepN-annov StepN-anno StepN-appl ¬(value v : A ) v ↩ → A v[′] e ↩ → e[′] StepN-fix e 1 ↩ → e 1[′] v : A ↩ → v[′] e : A ↩ → e[′] : A fix [A] x. e ↩ → e [ x ↦→ fix [A] x. e ] : A e 1 e 2 ↩ → e 1[′] [e][2] StepN-appr StepN-mergel StepN-merger e 2 ↩ → e 2[′] e 1 ↩ → e 1[′] e 2 ↩ → e 2[′] v 1 e 2 ↩ → v 1 e 2[′] e 1 ,, e 2 ↩ → e 1[′] [,,][ e][2] v 1 ,, e 2 ↩ → v 1 ,, e 2[′]

Fig. 9. The operational semantics of 𝜆 ∗.

of type C . Since the function argument is cast before beta reduction, we need to verify that the argument type is a guarded subtype of the parameter type. Thus, type dispatching formalizes the behaviour of an applicative intersection type. The soundness theorems for type dispatching, which computes the most specific return type given a function type A and an argument type B , are:

Theorem 4.6 (Soundness and Minimality of Type Dispatching). If B ⊢ A � C, then:

• If ⊢ 𝑟 A, then ⊢ 𝑟 C.

• A < : B → C

• ∀ D, if A < : B → D then C < : D

However, completeness is intractable here because guarded subtyping poses a unique coercion requirement on the argument type. This is hard to track in the subtyping relation; therefore we leave it here as an open problem. Note that for every well-typed expression in 𝜆 ∗, its type is determined in a syntax-directed way. In the following text, we use v : A to denote such a syntactic lookup, meaning that the inferred type of v is A .

4.2 Operational Semantics

In Fig. 9, we introduce three reduction relations to define the operational semantics of 𝜆 ∗. The casting relation v 1 ↩ → A v 2 takes a value v 1 and a type A and generates a value v 2, upcasting v 1 to match type A . The parallel application relation v 1 • v 2 ⇒ e distributes the argument v 2 into the merge v 1 and achieves dynamic dispatching. The small-step reduction e 1 ↩ → e 2 indicates that e 1 evaluates to e 2. At runtime, we replace all occurrences of guarded subtyping A ≾ B by subtyping A ≤ B since type checking is performed prior to evaluation. Moreover, A ≤ B is computationally cheaper than A ≾ B , since it merely checks for the existence of a coercion whereas guarded subtyping verifies the uniqueness of coercions.

Proc. ACM Program. Lang., Vol. 9, No. OOPSLA2, Article 279. Publication date: October 2025.

--- end of page.page_number=18 ---

Liberating Merges via Apartness and Guarded Subtyping

279:19

Function application. The evaluation rules are presented at the bottom of Fig. 9. There are three rules for function application: rule StepN-beta, rule StepN-absanno, and rule StepN-papp, which cover lambdas, function-like values, and merges, respectively. In rule StepN-beta, we first cast the application argument by the parameter annotation, and then use the result for beta reduction. The entire term is then wrapped by the function return type annotation, which denotes a delayed cast. Rule StepN-absanno handles the type annotations of a function-like value similarly. Eventually, when all outer annotations are decomposed, a function-like value becomes a lambda function, which then follows the beta rule. In addition to function-like values, merges can also be at the function position. Dynamic dispatching in rule StepN-papp is achieved via parallel application .

Parallel application and casting. Defined in the middle of Fig. 9, the parallel application relation v 1 • v 2 ⇒ e constructs an application expression e for each function contained in v 1, provided that the resulting application is well-typed. The unwanted parts of merges are filtered out. This type matching is performed dynamically because functions always have explicit type annotations. By comparing the parameter type with the type of the argument, it is straightforward to determine whether the requirements for a function are satisfied. As the type system already ensures the welltypedness of the application results, we only need to apply the function whenever the argument type matches (denoted by B ⊢ A �).

The definition of casting is shown at the top of Fig. 9. All annotations can be interpreted as a cast-to-do, unless they are part of values, as indicated by rule StepN-annov (while annotated values can only be function-like values). Type annotations may be decomposed (rules StepN-beta and StepN-absanno) or duplicated (rule StepN-fix), similar to what occurs in a cast calculus within the gradual typing setting [Wadler and Findler 2009]. Casting of splittable types ensures that no intersection types remain at the top level or in the function return type. Then, for each such ordinary type, a value is selected and refined (in the case of functions) so that the inference type of the value matches that type (recall that type splitting relation is defined in Fig. 4). Finally, all these values are merged. For example, ‘a’ ,, 1 ,, True ↩ →Bool & Int True ,, 1.

This process involves treating a merge as a function. For instance, Int →(Int & Bool) ≃(Int → Int) & (Int → Bool) means that a merge of type (Int → Int) & (Int → Bool) will be generated instead of a value of type Int →(Int & Bool) in v 1 ↩ →Int→(Int & Bool) v 2. To characterize the relationship between the actual type and the desired type, we use runtime subtyping in our type preservation theorem, which we will explain later. Without any constraints, the casting rule for ordinary types is non-deterministic: both 1 ,, 2 ↩ →Int 1 and 1 ,, 2 ↩ →Int 2 are derivable. However, a well-typed cast always produces a unique result.

Theorem 4.7 (Determinism of Casting in 𝜆 ∗). If v : A and A ≾ B, then from v ↩ → B v 1 and v ↩ → B v 2 we can derive v 1 = v 2 .

As one can observe, our casting always attaches new annotation to function-like values. However, the roundtrip coercion still preserves behavioral equivalence after erasing the type annotations. We define the type annotation erasing function be � 𝑒 �, then we have the behavioral equivalence as:

Theorem 4.8 (Behavioral Eqivalence of Round-Trip Coercion). If for all 𝑖 ∈[1 ,𝑛 ] , ⊢ 𝑟 𝐴𝑖 , and v𝑖 −1 can be coerced to v𝑖 via v𝑖 −1 ↩ → 𝐴𝑖 v𝑖 , then if 𝐴 𝑗 = 𝐴𝑘 , then � 𝑣 𝑗 � = � 𝑣𝑘 � .

4.3 Type Safety

Although each well-typed program has a unique inferred type, this type is not precisely preserved during evaluation. We use the runtime subtyping relation A ≪ 𝑇 B to connect the type of the reduced term with that of the redex. The definition and full details of it can be found in the Appendix.

Theorem 4.9 (Preservation of 𝜆 ∗).

Proc. ACM Program. Lang., Vol. 9, No. OOPSLA2, Article 279. Publication date: October 2025.

--- end of page.page_number=19 ---

Han Xu, Xuejing Huang, and Bruno C. d. S. Oliveira

279:20

• If · ⊢ 𝑡 v 1 ⇒ A, A ≾ B, ⊢ 𝑟 B, and v 1 ↩ → B v 2 , then ∃ C, s.t. · ⊢ 𝑡 v 2 ⇒ C and C ≪ 𝑇 B.

• If · ⊢ 𝑡 e ⇒ A and e ↩ → e[′] then ∃ A[′] , A[′] ≪ 𝑇 A, and · ⊢ 𝑡 e[′] ⇒ A[′] .

• If · ⊢ 𝑡 e ⇐ A and e ↩ → e[′] then · ⊢ 𝑡 e ⇐ A.

The operational semantics of 𝜆 ∗ is deterministic for well-typed expressions.

Theorem 4.10 (Determinism of the Small-Step Reduction in 𝜆 ∗). If · ⊢ 𝑡 e ⇒ A and e ↩ → e 1 and e ↩ → e 2 then e 1 = e 2 .

Moreover, our calculus adheres to the principle: Well-typed programs do not go wrong. We can establish type soundness through a progress theorem and the above preservation theorems.

Theorem 4.11 (Progress). If · ⊢ 𝑡 e ⇒ A then e is a value or ∃ 𝑒[′] , e ↩ → e[′] .

Theorem 4.12 (Type Soundness of 𝜆 ∗). If · ⊢ 𝑡 e ⇔ A and e ↩ →[∗] e[′] then e[′] is a value or ∃ e[′′] , e[′] ↩ → e[′′] .

5 The Source Calculus 𝜆 |∗|

In this section, we introduce the lambda calculus 𝜆 |∗| together with a type normalization procedure. The target calculus 𝜆 ∗ imposes strong type well-formedness restrictions. Here, we demonstrate that 𝜆 |∗| can model a source calculus without these restrictions. Through type normalization, all well-typed 𝜆 |∗| programs can be translated into well-typed 𝜆 ∗ programs, indicating that 𝜆 ∗’s type restrictions are not fundamental but merely simplify the design of a calculus with apartness.

5.1 Type Normalization

Though type apartness A ∗ B along with the well-formedness condition ⊢ 𝑟 A provides a sound calculus 𝜆 ∗, unrestricted intersection types can be useful in certain cases, as illustrated in Fig. 3. To accommodate such cases, we impose a weaker restriction on types: instead of requiring A and B to be apart directly, we check their normalized forms for apartness. We use type normalization to compute these normalized forms so that any types satisfying apartness specification A ∗ 𝑠 B will have their normalized form algorithmically apart. The formulation of type normalization process is not unique, as long as the return type has all of its type components apart and being equivalent to the original type. However, as suggested by Theorems 4.4 and 4.8, the coercion between any two equivalent types is unique, type-safe and behaviour preserving, therefore any type normalization process exhibit no observable difference.

Normalization as a divide-and-conquer process. | A | B denotes that the type A will be normalized under the type B . A denotes the type we want to normalize, and we want to produce a result that does not overlap with B . B also interacts with the intermediate result during the divide-and-conquer process to avoid unnecessary elimination, which will be shown below. We do the normalization of each component of a type A from left to right. The intuition behind type normalization of A under B is that A can be viewed as a series (or a list) of type components concatenated together with the type operator & . During normalization, we aim to eliminate duplicated components. The process follows a divide-and-conquer strategy by splitting A into two intersection components, A 1 and A 2.

In our algorithm, we first normalize the right-hand side series of components A 2 under A 1 & B , producing an intermediate result C . We then normalize the left-hand side A 1 using the type context B & C . This approach avoids repeated normalization. For instance, given Int & Int, we do not normalize the right-hand Int by the left-hand Int and then repeat the process for the reverse. Repeated normalization could erroneously result in ⊤ & ⊤. By leveraging the intermediate result C , the normalization remains deterministic and avoids such issues. To ensure determinism and avoid reducing to ⊤ & ⊤, we define specific cases for handling the result C produced from normalizing A 2 under A 1 & B . While the cases differ, they follow the same underlying principles.

Proc. ACM Program. Lang., Vol. 9, No. OOPSLA2, Article 279. Publication date: October 2025.

--- end of page.page_number=20 ---

Liberating Merges via Apartness and Guarded Subtyping

279:21

Rules of | A | B , where we take the normalization result | A | = | A |⊤

(Type Normalization)

Fig. 10. Type normalization, (selected) typing and reduction rules for 𝜆 |∗| .

For example, consider normalizing Int & (Bool & Int) under ⊤. The process proceeds as follows:

The final result is Int & Bool, demonstrating how the process avoids ambiguity and ensures a deterministic outcome. This divide-and-conquer approach operates bottom up. At step (5), we aim to normalize Int & (Bool & Int) under type ⊤. To do so, we split Int & (Bool & Int) and normalize both Int and Bool & Int separately. Following a similar strategy, we observe that at step (3), Bool & Int normalizes to Bool under ⊤ & Int, while Int normalizes to Int under ⊤ & Bool. As a result, after normalization, we obtain Int & Bool. This approach is essential for achieving complete and sound normalization while preserving determinism.

Normalization starts from an empty context (⊤). The operation | A |⊤ = C takes A as input and ⊤ as context, producing C as the normalized form of A . We use | A | to denote the result of | A |⊤. The normalization process is idempotent, complete, deterministic, and sound.

Theorem 5.1 (Normalization is Idempotent). || A | B | B = | A | B.

Theorem 5.2 (Totality of Normalization). For all A B, there exists C such that | A | B = C.

Theorem 5.3 (Determinism of Normalization). | A | B results in at most one C.

Theorem 5.4 (Soundness of Normalization). For all A, we have A ≤| A | and | A | ≤ A.

Theorem 5.5 (Soundness of Guarded Subtyping). For all A B, if A ≤ B and B ≤ A, then | A | ≾ | B | .

Proc. ACM Program. Lang., Vol. 9, No. OOPSLA2, Article 279. Publication date: October 2025.

--- end of page.page_number=21 ---

Han Xu, Xuejing Huang, and Bruno C. d. S. Oliveira

279:22

The normalization procedure provides another way to show the completeness of apartness, since normalization eliminates shadowed components in types, as suggested in Section 3.3.

Theorem 5.6 (Completeness of Apartness). For all A B, | A | ∗| B | iff A ∗ 𝑠 B.

5.2 Source Typing and Operational Semantics

Source typing is not very different from the target typing of 𝜆 ∗. The key difference is that we check whether the normalized result type checks. We can perform a weaker check on all the types as long as their normalized form satisfies the constraints, instead of requiring types to be well-formed and then checking the constraints. For instance, (String → Bool) & ((String & Int) → Bool) is not mergeable with Int → Bool in 𝜆 ∗. However, that type is mergeable in 𝜆 |∗| since the normalization process erases the (String & Int) → Bool component during the normalization process. Likewise, we do the normalization in the reduction of 𝜆 |∗| . The only difference in the source reduction semantics with 𝜆 ∗ reduction is that, we do a type normalization whenever casting occurs.

After carefully dealing with the normalized component in typing and evaluation, we can setup the determinism and soundness properties of 𝜆 |∗| . Here the runtime subtyping relation A[′] ≪ A , is used for preservation of the source calculus, and works just as A[′] ≪ 𝑇 A in 𝜆 ∗.

Theorem 5.7 (Determinism). If · ⊢ e ⇒ A and e ↩ → 𝑆 e 1 and e ↩ → 𝑆 e 2 then e 1 = e 2 .

Theorem 5.8 (Progress). If · ⊢ e ⇒ A then e is a value or ∃ 𝑒[′] , e ↩ → 𝑆 e[′] . Theorem 5.9 (Preservation).

• If · ⊢ e ⇒ A and e ↩ → 𝑆 e[′] then ∃ A[′] , A[′] ≪ A, and · ⊢ e[′] ⇒ A[′] .

• If · ⊢ e ⇐ A and e ↩ → 𝑆 e[′] then · ⊢ e ⇐ A.

5.3 Translation to Target and Operational Correspondence

Before establishing a value-to-value mapping between the source calculus and the target calculus, we first define the relationship between well-formedness and type normalization. Specifically, well-formedness ⊢ 𝑠 A corresponds directly to normalization.

The source calculus permits more expressive terms—such as 1 ,, ⊤ ,, ⊤ or 𝜆[Int][→][Int][ &][ Int] x. e —that would be rejected by the more restrictive type system of the target calculus. To bridge this gap, we introduce a normalization process and design the target type system of 𝜆 ∗ to accept all normalized source types as well-formed. This approach enables a smooth and consistent translation from source to target, freeing us from the rigid constraints of 𝜆 ∗. Moreover, assuming that all type annotations are normalized during translation into 𝜆 ∗, the reduction rules in the target calculus can be simplified. For example, rules like rule StepN-annov no longer require runtime type normalization (like in 𝜆 |∗| ), simplifying evaluation in the target language.

Theorem 5.10 (Eqivalence of Normalization and Well-Formedness). ⊢ 𝑠 A iff | A | = A.

We are now ready to establish the correspondence between 𝜆 |∗| and 𝜆 ∗. To incorporate type normalization into type annotations in 𝜆 |∗| , we introduce a term normalization process, denoted | e |, which translates type annotations into normalized types. Specifically, during translation, | e | normalizes all type annotations: non-arrow types A become | A |, and arrow types A → B become | A | →| B |. For instance, the term e : (Int & Int) is normalized to | e | : Int, while 𝜆[A][→] [B][ &] [ C] x. e is normalized to 𝜆[|] [A][|][→][|] [B][ &] [ C][|] x. e . so that a value-to-value mapping from 𝜆 |∗| to 𝜆 ∗ is preserved, while the full details are in the Appendix. With term normalization in place, we can now formally state and prove the soundness of both typing and evaluation:

Theorem 5.11 (Type-Safety of Translation). If · ⊢ e ⇒ A then ∃ B, · ⊢ 𝑡 | e | ⇒ B and | B | = | A | .

Theorem 5.12 (Operational Correspondence). If e ↩ → 𝑆[∗] [e][′] [then][ |] [e][|] [↩][→] 𝑇[∗][|] [e][′][|] [.]

Proc. ACM Program. Lang., Vol. 9, No. OOPSLA2, Article 279. Publication date: October 2025.

--- end of page.page_number=22 ---

Liberating Merges via Apartness and Guarded Subtyping

279:23

6 Type Difference

A key consequence of using apartness instead of disjointness is that type difference [Xu et al. 2023] becomes a total operation rather than a partial one. This section defines type difference in terms of apartness and proves its totality.

6.1 Partial Type Difference with Disjointness

Type difference, introduced by Xu et al. [2023], provides a way to resolve conflicts in merges with disjoint intersection types. The idea behind type difference, denoted as A \ B , is to remove conflicting type components from A , allowing the resolution of a conflicting merge of type A & B by rewriting it as ( A \ B ) & B . The following examples illustrate how type difference operates.

Type difference eliminates overlapping components of A with respect to B . For instance, Int → Bool is completely removed when B is Int → Bool (or a subtype). However, when subtracting Int, the function type Int → Bool remains unchanged because Int does not overlap with it.

More interesting cases arise with function types. In (Int → Bool)(Bool → String), subtraction has no effect on Int → Bool since the two types are disjoint. However, subtracting Bool → String from Int → String presents a conflict: Int → String is neither fully shadowed by Bool → String nor completely disjoint from it. Removing Int → String would result in information loss, while keeping it would leave the conflict unresolved.

Despite its expressive power, type difference remains a partial operation since it cannot resolve conflicts between types like Int → String and Bool → String. Our observation is that type difference is tightly coupled with the disjointness relation. The previous definition of disjointness may be too strict in identifying conflicts. As we will show, apartness allows us to define a total type difference.

6.2 Total Type Difference with Apartness

Interestingly, type difference in our setting actually corresponds to the type normalization process, and can be specified as a variant of apartness. Recall the apartness specification in Sec. 2.4.

Definition 2.4 (Apartness Specification). A ∗ 𝑠 B ≜ ∀ C 1 C 2 , if MinOrd C 1 A ∧ MinOrd C 2 B , then either C 1 = ⊤ or C 2 = ⊤ or (¬( C 1 ≤ C 2) ∧¬( C 2 ≤ C 1)).

Type normalization cannot resolve all the conflicts inside type A through the process | A | B . We can glance through a few examples next:

As we can see, the normalization process resolves conflicts well in the first three examples, as we have the normalization result | A | B to be apart from B . We can use the merge of | A | B and B to replace the ambiguous merge A with B . But in the fourth case, the conflict is still not resolved as Int → Bool shadows (Int & String) → Bool. Under the normalization process, supertype (Int & String) → Bool cannot normalize Int → Bool, thus the conflict remains unsolved after the normalization process.

A closer glance at normalization shows that it removes all the conflicting components of type A that are shadowed by type B . In some sense, it is a one-sided conflict resolution that cleans things only in type A . Based on this observation, we can define the notion of half apartness as:

Definition 6.1 (Half Apart Specification). A < ∗ B ≜ ∀ C 1 C 2 , if MinOrd C 1 A ∧ MinOrd C 2 B , then C 2 = ⊤∨¬( C 1 ≤ C 2).

Proc. ACM Program. Lang., Vol. 9, No. OOPSLA2, Article 279. Publication date: October 2025.

--- end of page.page_number=23 ---

Han Xu, Xuejing Huang, and Bruno C. d. S. Oliveira

279:24

which suggests that every component in the type B is not shadowed by the components in A , representing a one-side apartness. Half apartness A < ∗ B represents exactly the asymmetric variant of apartness, as we can set up the equivalence of two variants of apartness as follows:

Theorem 6.2 (Apartness in terms of Half-Apartness). A < ∗ B and B < ∗ A, iff A ∗ 𝑠 B.

During type normalization | A | B = C , only type A is normalized while type B only serves as contextual information guiding through the process. Thus, we can now set up the type normalization exactly as the type difference specification [Xu et al. 2023] based on our one-sided apartness A < ∗ B :

Definition 6.3 (Type Difference Specification). A \ 𝑠 B = C ≜ A ≤ C ∧ B & C ≤ A ∧ B < ∗ C .

Furthermore, the type normalization process directly gives us an algorithmic formulation for this type difference specification:

Theorem 6.4 (Type Difference as Type Normalization).

• A \ 𝑠 B = | A | B.

• For all C, if A \ 𝑠 B = C, then C ≤| A | B and | A | B ≤ C.

The two properties imply that results produced by the type difference of type 𝐴 and 𝐵 are equivalent to | A | B . Thus we can use type normalization as an algorithm to compute type difference. Additionally, type normalization process is total: we are always able to resolve conflicts in two arbitrary types. This contrasts with the prior formulation disjointness-based type difference. Due to half apartness, we have to do the type difference twice (on both A and B ), to resolve conflicts on two types.

Theorem 6.5 (Conflict Resolution). if | A | B = C and | B | C = D, then C ∗ 𝑠 D.

To resolve conflicts in A and B , we first do the normalization | A | B = 𝐶 to get the conflict-free version of A (i.e. C ). Then we do the normalization | B | C = 𝐷 to get the conflict-free version of B (i.e. D ). Finally, we know that the resulting conflict-free types are apart C ∗ D . We do not lose information as we have A & B ≤ C & D and C & D ≤ A & B from the type difference specification.

7 Related Work

Function Overloading and the Merge Operator. Function overloading (or method overloading) is the ability to create multiple functions of the same name with different implementations. In our context, function overloading is usually achieved by the merge operator to create an overloaded function. The calculus 𝜆 & proposed by Castagna et al. [1995] has a restricted version of the merge operator for functions only. The merge operator is indexed by a list of types of its components. Its operational semantics uses the runtime types of values to select the “best approximate” branch of an overloaded function, but 𝜆 & requires runtime subtype checking to support such mechanisms.

Dunfield [2014] presented the first calculus with an unrestricted merge operator, based on Reynolds [1997]’s merge operator. Though her calculus is powerful and supports function overloading, it lacks determinism and type preservation. Xue et al. [2022] presents a calculus with a merge operator with preservation, with all 4 features discussed in Sec. 2.2. However, Xue et al. [2022]’s calculus is still non-deterministic. Other calculi with intersection types and function overloading have been proposed [Castagna et al. 2015, 2014; Castagna and Xu 2011], but these calculi do not support a merge operator, and thus avoid the ambiguity problems caused by merges.

Disjoint Intersection Types. Oliveira et al. [2016] proposed the 𝜆𝑖 calculus, which only allows terms of disjoint types to be merged. The goal of the disjointness restriction was to address the ambiguity in Dunfield [2014]’s calculus and to create a deterministic calculus. Various extensions [Alpuim et al. 2017; Bi and Oliveira 2018; Bi et al. 2018] were later proposed to strengthen 𝜆𝑖 with relaxed restrictions, nested composition and disjoint polymorphism.

Proc. ACM Program. Lang., Vol. 9, No. OOPSLA2, Article 279. Publication date: October 2025.

--- end of page.page_number=24 ---

Liberating Merges via Apartness and Guarded Subtyping

279:25

Huang and Oliveira [2020] propose a type-directed operational semantics (TDOS) to specify the semantics of calculi with disjoint intersection types and a merge operator. TDOS employs parallel application to support merging multiple functions and applying them simultaneously to a single input. Additionally, TDOS does not require runtime subtype checking and allows merging and applying values of types beyond just function types. Our work also employs TDOS, leveraging apartness to allow certain ambiguous types. This relaxation enables the merging of function types such as Int → Bool and String → Bool, thereby supporting overloading—previously prohibited under strict disjointness conditions. Moreover, by combining overloading with first-class labels, we achieve a lightweight encoding of records [Castagna et al. 1995].

𝐹⊲⊳ [Rioux et al. 2023] is a powerful calculus that supports deterministic merges. 𝐹⊲⊳ employs two dual disjointness relations, called mergeable and distinguishable , to empower the merge operator not only with intersection types but also union types. However, such expressiveness comes with trade-offs. In 𝐹⊲⊳ merges of values with primitive types, such as Int and Bool, are not allowed. As a consequence of this restriction, return type overloading is not supported either. Thus, we are not able to merge String → Int and String → Bool together, even though values of those types can always be disambiguated. In contrast, our 𝜆 |∗| and 𝜆 ∗ calculi do not support union types, but support merges of primitive types, as well as return type overloading.

Conflict Resolution in OOP and the Merge Operator. In OOP, mixin classes [Ancona et al. 2003; Bracha and Cook 1990; Duggan and Sourelis 1996; Flatt et al. 1998] and traits [Fisher and Reppy 2004; Schärli et al. 2003] are two composition mechanisms for code reuse and multiple inheritance. Name conflicts are a common problem for both the merge operator and OOP. Usually, the mixin model allows overlapping fields and omits the one with lower priority. Instead, traits only allow no conflicting merges. Conflicts have to be resolved before composition by renaming or restriction.

Compositional Programming [Zhang et al. 2021] is a recently proposed modular programming paradigm based on first-class traits [Bi and Oliveira 2018], and implemented by the CP language. CP is built on top of a core calculus with disjoint intersection types and the merge operator [Fan et al. 2022]. In CP, parallel application is employed to support merging multiple functions and apply them together to one input. The use of the merge operator in CP allows it to naturally solve the Expression Problem [Wadler 1998] and offers modular pattern matching and dependency injection. Ye et al. [2024] later extend CP to imperative computational effects.

Type difference [Xu et al. 2023] was proposed to resolve conflicts in merges in settings with disjoint intersection types. Our work uses apartness instead of disjointness, and sets up type difference as type normalization. Type normalization under apartness not only retains all of the soundness and completeness properties, but also achieves totality. This enables resolving conflicts in all terms to be merged.

8 Conclusion

In this paper, we introduce type apartness , a weaker form of disjointness, for calculi with intersection types and a merge operator. Apartness preserves type soundness and determinism, while enabling key features: function overloading , return type overloading , extensible records , and nested composition . We develop two calculi, 𝜆 |∗| and 𝜆 ∗, which incorporate apartness and guarded subtyping. We establish connection between them via type normalization , which also establishes a total type difference operator [Xu et al. 2023] within the apartness framework. Besides, all the properties and theorems are verified in Coq. Future work will explore extending apartness notion to other type system constructs, such as union types [Barbanera et al. 1995] and disjoint polymorphism [Alpuim et al. 2017], broadening its applicability.

Proc. ACM Program. Lang., Vol. 9, No. OOPSLA2, Article 279. Publication date: October 2025.

--- end of page.page_number=25 ---

Han Xu, Xuejing Huang, and Bruno C. d. S. Oliveira

279:26

Data-Availability Statement

The companion artifact [Xu et al. 2025] includes the Coq development and the appendix.

Acknowledgments

Xuejing Huang acknowledges support from the MathInGreaterParis Fellowship Programme, funded by the HORIZON EUROPE Marie Sklodowska-Curie Actions and the Fondation Sciences Mathtématiques de Paris.

References

João Alpuim, Bruno C. d. S. Oliveira, and Zhiyuan Shi. 2017. Disjoint Polymorphism. In European Symposium on Programming (ESOP) . https://doi.org/10.1145/1391289.1391293

Davide Ancona, Giovanni Lagorio, and Elena Zucca. 2003. Jam—designing a Java extension with mixins. ACM Transactions on Programming Languages and Systems (TOPLAS) 25, 5 (2003), 641–712. doi:10.1145/937563.937567 Franco Barbanera, Mariangiola Dezani-Ciancaglini, and Ugo de’Liguoro. 1995. Intersection and Union Types: Syntax and Semantics. Information and Computation 119, 2 (June 1995), 202–230.

Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. 1983. A Filter Lambda Model and the Completeness of Type Assignment. The Journal of Symbolic Logic 48, 4 (1983), 931–940. http://www.jstor.org/stable/2273659 Xuan Bi and Bruno C. d. S. Oliveira. 2018. Typed First-Class Traits. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018) . doi:10.4230/LIPIcs.ECOOP.2018.9

Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers. 2018. The Essence of Nested Composition. In 32nd European Conference on Object-Oriented Programming, ECOOP 2018, July 16-21, 2018, Amsterdam, The Netherlands (LIPIcs, Vol. 109) , Todd D. Millstein (Ed.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 22:1–22:33. doi:10.4230/LIPIcs.ECOOP.2018.22 Gilad Bracha and William Cook. 1990. Mixin-based inheritance. ACM Sigplan Notices 25, 10 (1990), 303–311. doi:10.1145/ 97945.97982

Giuseppe Castagna, Giorgio Ghelli, and Giuseppe Longo. 1995. A Calculus for Overloaded Functions with Subtyping. Information and Computation 117, 1, 115–135. doi:10.1006/inco.1995.1033 Giuseppe Castagna, Kim Nguyen, Zhiwu Xu, and Pietro Abate. 2015. Polymorphic Functions with Set-Theoretic Types: Part 2: Local Type Inference and Type Reconstruction. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Mumbai, India) (POPL ’15) . Association for Computing Machinery, New York, NY, USA, 289–302. doi:10.1145/2676726.2676991

Giuseppe Castagna, Kim Nguyen, Zhiwu Xu, Hyeonseung Im, Sergueï Lenglet, and Luca Padovani. 2014. Polymorphic Functions with Set-Theoretic Types: Part 1: Syntax, Semantics, and Evaluation. In Proceedings of the 41st ACM SIGPLANSIGACT Symposium on Principles of Programming Languages (San Diego, California, USA) (POPL ’14) . Association for Computing Machinery, New York, NY, USA, 5–17. doi:10.1145/2535838.2535840

Giuseppe Castagna and Zhiwu Xu. 2011. Set-Theoretic Foundation of Parametric Polymorphism and Subtyping. In Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming (Tokyo, Japan) (ICFP ’11) . Association for Computing Machinery, New York, NY, USA, 94–106. doi:10.1145/2034773.2034788

Rowan Davies and Frank Pfenning. 2000. Intersection Types and Computational Effects. In Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP ’00) . Association for Computing Machinery, New York, NY, USA, 198–208. doi:10.1145/351240.351259

Dominic Duggan and Constantinos Sourelis. 1996. Mixin modules. ACM SIGPLAN Notices 31, 6 (1996), 262–273. Jana Dunfield. 2014. Elaborating intersection and union types. Journal of Functional Programming (JFP) 24, 2-3 (2014), 133–165. doi:10.1006/inco.1995.1086

Jana Dunfield and Neel Krishnaswami. 2021. Bidirectional Typing. ACM Comput. Surv. 54, 5, Article 98 (May 2021), 38 pages. doi:10.1145/3450952

Erik Ernst. 2001. Family polymorphism. In European Conference on Object-Oriented Programming . Springer, 303–326. Andong Fan, Xuejing Huang, Han Xu, Yaozhu Sun, and Bruno C. d. S. Oliveira. 2022. Direct Foundations for Compositional Programming. In 36th European Conference on Object-Oriented Programming (ECOOP 2022) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 222) , Karim Ali and Jan Vitek (Eds.). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 18:1–18:28. doi:10.4230/LIPIcs.ECOOP.2022.18

Kathleen Fisher and John Reppy. 2004. A typed calculus of traits. In Electronic proceedings of FOOL , Vol. 2004.

Matthew Flatt, Shriram Krishnamurthi, and Matthias Felleisen. 1998. Classes and mixins. In Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages . 171–183. doi:10.1145/268946.268961

Alain Frisch, Giuseppe Castagna, and Véronique Benzaken. 2008. Semantic Subtyping: Dealing Set-Theoretically with Function, Union, Intersection, and Negation Types. J. ACM 55, 4, Article 19 (Sept. 2008), 64 pages. doi:10.1145/1391289.

Proc. ACM Program. Lang., Vol. 9, No. OOPSLA2, Article 279. Publication date: October 2025.

--- end of page.page_number=26 ---

279:27

Liberating Merges via Apartness and Guarded Subtyping

1391293 Xuejing Huang and Bruno C. d. S. Oliveira. 2020. A type-directed operational semantics for a calculus with a merge operator. In The 34th European Conference on Object-Oriented Programming (ECOOP 2020 . Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik GmbH. The Journal’s web … Xuejing Huang, Jinxu Zhao, and Bruno C. d. S. Oliveira. 2021. Taming the Merge Operator. 31 (2021). doi:10.1017/ S0956796821000186 Publisher: Cambridge University Press. Daan Leijen. 2004. First-class labels for extensible rows (technical report uu-cs-2004-51 ed.). Technical Report UU-CS-2004-51. https://www.microsoft.com/en-us/research/publication/first-class-labels-for-extensible-rows/ UTCS Technical Report. Barbara H. Liskov and Jeannette M. Wing. 1994. A behavioral notion of subtyping. ACM Trans. Program. Lang. Syst. 16, 6 (Nov. 1994). Zhaohui Luo. 1999. Coercive Subtyping. J. Log. Comput. 9, 1 (1999), 105–130. doi:10.1093/logcom/9.1.105 Koar Marntirosian, Tom Schrijvers, Bruno C. d. S. Oliveira, and Georgios Karachalias. 2020. Resolution as Intersection Subtyping via Modus Ponens. Proc. ACM Program. Lang. 4, OOPSLA, Article 206 (nov 2020). doi:10.1145/3428274 Bruno C. d. S. Oliveira, Zhiyuan Shi, and João Alpuim. 2016. Disjoint intersection types. In International Conference on Functional Programming (ICFP) . doi:10.1145/2951913.2951945 Benjamin C. Pierce and David N. Turner. 2000. Local Type Inference. ACM Trans. Program. Lang. Syst. 22, 1 (jan 2000), 1–44. doi:10.1145/345099.345100 John C Reynolds. 1988. Preliminary design of the programming language Forsythe . Technical Report. Carnegie Mellon University. John C. Reynolds. 1991. The coherence of languages with intersection types. In Lecture Notes in Computer Science (LNCS) . Springer Berlin Heidelberg, 675–700. John C Reynolds. 1997. Design of the programming language Forsythe. In ALGOL-like languages . 173–233. John C Reynolds. 1998. Theories of programming languages . Cambridge University Press. Nick Rioux, Xuejing Huang, Bruno C d S Oliveira, and Steve Zdancewic. 2023. A Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data Types in F ⊲⊳ . Proceedings of the ACM on Programming Languages 7, POPL (2023), 515–543. Nathanael Schärli, Stéphane Ducasse, Oscar Nierstrasz, and Andrew P Black. 2003. Traits: Composable units of behaviour. In European Conference on Object-Oriented Programming (ECOOP) . Jeremy Siek and Walid Taha. 2007. Gradual Typing for Objects. In Proceedings of the 21st European Conference on ECOOP 2007: Object-Oriented Programming (Berlin, Germany) (ECOOP ’07) . Springer-Verlag, Berlin, Heidelberg, 2–27. doi:10.1007/9783-540-73589-2_2 Jinhao Tan and Bruno C d S Oliveira. 2023. Dependent Merges and First-Class Environments. In 37th European Conference on Object-Oriented Programming (ECOOP 2023) . Schloss Dagstuhl-Leibniz-Zentrum für Informatik. Philip Wadler. 1998. The expression problem. Java-genericity mailing list (1998). Philip Wadler and Robert Bruce Findler. 2009. Well-typed programs can’t be blamed. In European Symposium on Programming . Springer, 1–16. Yanlin Wang, Haoyuan Zhang, Bruno C. d. S. Oliveira, and Marco Servetto. 2018. FHJ: A Formal Model for Hierarchical Dispatching and Overriding. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 109) , Todd Millstein (Ed.). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 20:1–20:30. doi:10.4230/LIPIcs.ECOOP.2018.20 Han Xu, Xuejing Huang, and Bruno C. d. S. Oliveira. 2023. Making a Type Difference: Subtraction on Intersection Types as Generalized Record Operations. Proc. ACM Program. Lang. 7, POPL, Article 31 (jan 2023), 28 pages. doi:10.1145/3571224 Han Xu, Xuejing Huang, and Bruno C. d. S. Oliveira. 2025. Liberating Merges via Apartness and Guarded Subtyping (Artifact). doi:10.5281/zenodo.16921686 Xu Xue, Bruno C. d. S. Oliveira, and Ningning Xie. 2022. Applicative Intersection Types. In Programming Languages and Systems , Ilya Sergey (Ed.). Springer Nature Switzerland, Cham, 155–174. Wenjia Ye, Yaozhu Sun, and Bruno C. d. S. Oliveira. 2024. Imperative Compositional Programming: Type Sound Distributive Intersection Subtyping with References via Bidirectional Typing. Proc. ACM Program. Lang. 8, OOPSLA2, Article 342 (Oct. 2024), 30 pages. doi:10.1145/3689782

Weixin Zhang, Yaozhu Sun, and Bruno C. d. S. Oliveira. 2021. Compositional Programming. ACM Transactions on Programming Languages and Systems (TOPLAS) 43, 3 (2021), 1–61. doi:10.1145/3460228

Received 2024-10-15; accepted 2025-08-12

Proc. ACM Program. Lang., Vol. 9, No. OOPSLA2, Article 279. Publication date: October 2025.

--- end of page.page_number=27 ---