On the Decidability of Subtyping with Bounded Existential Types

Stefan Wehr and Peter Thiemann

In Proceedings of the Seventh Asian Symposium on Programming Languages and Systems. Lecture Notes in Computer Science, vol. 5904, Seoul, South Korea. Springer, 2009.

Abstract

Bounded existential types are a powerful language feature for modeling partial data abstraction and information hiding. However, existentials do not mingle well with subtyping as found in current object-oriented 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.

Bibtex

@INPROCEEDINGS{WehrThiemann2009-aplas,
  author = {Stefan Wehr and Peter Thiemann},
  title = {On the Decidability of Subtyping with Bounded Existential Types},
  booktitle = {Proceedings of the Seventh Asian Symposium on Programming Languages and Systems},
  year = 2009,
  volume = 5904,
  address = {Seoul, South Korea},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer}
}

Resources

• Preprint: .pdf (© Springer-Verlag)
• An extended version appeared as TR 250 of the Department of Computer Science, University of Freiburg.
• Acceptance rate: 37.5 % (56 papers reviewed, 21 accepted)
• Project homepage
• Supersedes the corresponding paper at FTfJP 2008.