Union types with disjoint switches

authors: Baber Rehman, Xuejing Huang, Ningning Xie, Bruno C d S Oliveira
year: 2022
url: https://i.cs.hku.hk/ bruno/papers/ecoop22switches.pdf
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
abstract: Union types are nowadays a common feature in many modern programming languages. This paper investigates a formulation of union types with an elimination construct that enables case analysis (or switches) on types. The interesting aspect of this construct is that each clause must operate on disjoint types. By using disjoint switches, it is possible to ensure exhaustiveness (i.e. all possible cases are handled), and that none of the cases overlap. In turn, this means that the order of the cases does not matter and that reordering the cases has no impact on the semantics, helping with program understanding and refactoring. While implemented in the Ceylon language, disjoint switches have not been formally studied in the research literature, although a related notion of disjointness has been studied in the context of disjoint intersection types. We study union types with disjoint switches formally and in a language independent way. We first present a simplified calculus, called the union calculus (λ_u), which includes disjoint switches and prove several results, including type soundness and determinism. The notion of disjointness in λ_u is in essence the dual notion of disjointness for intersection types. We then present a more feature-rich formulation of λ_u, which includes intersection types, distributive subtyping and a simple form of nominal types. This extension reveals new challenges. Those challenges require us to depart from the dual notion of disjointness for intersection types, and use a more general formulation of disjointness instead. Among other applications, we show that disjoint switches provide an alternative to certain forms of overloading, and that they enable a simple approach to nullable (or optional) types. All the results about λ_u and its extensions have been formalized in the Coq theorem prover.