Sciweavers

APLAS
2009
ACM

On the Decidability of Subtyping with Bounded Existential Types

13 years 10 months ago
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.
Stefan Wehr, Peter Thiemann
Added 27 May 2010
Updated 27 May 2010
Type Conference
Year 2009
Where APLAS
Authors Stefan Wehr, Peter Thiemann
Comments (0)