On the Decidability of Subtyping with Bounded Existential Types

Bounded existential types are a powerful language feature ling partial data abstraction and information hiding. However, existentials do not mingle well with subtyping as found in current objectoriented languages: the subtyping relation is already undecidable for very restrictive settings. This paper considers two subtyping relations defined by extracting the features specific to existentials from current language proposals (JavaGI, WildFJ, and Scala) and shows that both subtyping relations are undecidable. One of the two subtyping relations remains undecidable even if bounded existential types are removed. With the goal of regaining decidable type checking for the JavaGI language, the paper also discusses various restrictions including the elimination of bounded existentials from the language as well as possible amendments to regain some of their features.

• Type: Conference
• Year: 2009
• Where: APLAS
• Authors: Stefan Wehr, Peter Thiemann
• Keywords: APLAS 2009, Existential Types, Powerful Language Feature, Programming Languages, Subtyping