Abstract
Intersection and union types are becoming more popular by the day, entering the mainstream in programming languages like TypeScript and Scala 3. But these types are difficult to combine with practical polymorphic type inference and their metatheory has proven difficult to establish, especially in the presence of equirecursive types and distributivity between unions and intersections. We propose Boolean-algebraic subtyping, a new subtyping framework for reasoning about type systems with conjunction (a.k.a. intersection), disjunction (a.k.a. union), and negation (a.k.a. complement) connectives. Our framework is algebraic in that it does not appeal to some underlying model of types and remains generic/extensible with respect to the specific base type constructors of the underlying language. We also present MLstruct, a programming language based on Boolean-algebraic subtyping and the first language to support principal polymorphic type inference in the presence of union and intersection types. MLstruct is structurally typed but also contains a healthy sprinkle of nominality, enabling the expression of a powerful form of extensible variants that does not require row variables and makes pivotal use of negation types. The algebraic nature of our framework is crucial in defining MLstruct: it allows the addition of nonstandard subtyping rules that would not hold in a classical set-theoretic interpretation of subtyping. With this work, we hope to foster the development of better type inference for present and future programming languages with expressive subtyping systems.
