Liberating Merges via Apartness and Guarded Subtyping
This program is tentative and subject to change.
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 \emph{type apartness}, which relaxes the strict disjointness constraints, while maintaining type safety and determinism. Type apartness allows some overlap between types as long as overlapping parts can be \emph{distinguished through specific upcasts}. By further incorporating the notion of guarded subtyping to prevent ambiguity when upcasting, our approach is the first to support \emph{function overloading}, \emph{return type overloading}, \emph{extensible records}, and \emph{nested composition} all at once 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 can be used to ensure consistency and resolve conflicts, enhancing the flexibility and expressiveness of the merge operator.