Subtyping Existential Types

Stefan Wehr and Peter Thiemann

In 10th Workshop on Formal Techniques for Java-like Programs FTfJP 2008, informal proceedings. Paphos, Cyprus. 2008.

Abstract

Constrained existential types are a powerful language feature that subsumes Java-like interface and wildcard types. But existentials do not mingle well with subtyping: subtyping is already undecidable for very restrictive settings. This paper defines two subtyping relations by extracting the features specific to existentials from current language proposals (JavaGI, WildFJ, Scala). Both subtyping relations are undecidable. The paper also discusses the consequences of removing existentials from JavaGI and possible amendments to regain their features.

Bibtex

@INPROCEEDINGS{WehrThiemann2008,
  author = {Stefan Wehr and Peter Thiemann},
  title = {Subtyping Existential Types},
  year = 2008,
  booktitle = {10th Workshop on Formal Techniques for {Java}-like Programs {FTfJP} 2008, informal proceedings},
  address = {Paphos, Cyprus},
  url = {http://www.informatik.uni-freiburg.de/~wehr/publications/Wehr_Subtyping_existential_types.pdf}
}

Resources

• Preprint: .pdf
• An extended version, including proofs, appeard as TR 240 of the Department of Computer Science, University of Freiburg (.pdf version of the TR).
• Talk at FTfJP 2008: .pdf
• FTfJP 2008 homepage
• Acceptance rate: 68.7 % (16 papers reviewed, 11 accepted)
• Project homepage
• Superseded by a paper at APLAS 2009.