Union Types for Object-Oriented Programming

We propose union types for statically typed class-based object-oriented languages as a means to enhance the °exibility of subtyping. As its name suggests, a union type can be considered a set union of instances of several types and behaves as their least common supertype. It also plays the role of an interface that `factors out ' commonality of given types|¯elds of the same name and methods with similar signatures. Union types can be useful for implementing heterogeneous collections and for grouping independently developed classes with similar interfaces, which has been considered di±cult in languages like Java. To rigorously show the safety of union types, we formalize them on top of Featherweight Java and prove that the type system is sound.