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

Last modified: 2015-06-10T22:24:05+02:00