Existential types

A type system features existential types when it is able to existentially quantify over a type variable.

Existential types can be used to abstract away the implementation of an interface, thereby enabling the construction of abstract data types.

In System F

System F only has universal quantification over types, not existential. However, existential quantification is definable:

\exists X. F(X) \triangleq \forall Y. (\forall X. F(X) \to Y) \to Y

In a language that has both, it can be shown that these two types are bijective up to contextual equivalence Pitts 2000, §7.

References

There is a textbook presentation of existential types in Chapter 24 of TAPL, and Chapter 17 of PFPL.
The connection between existential types and abstract data types was first made in a POPL 1985 paper. The journal version of this paper appeared in TOPLAS in 1988.

Mitchell, John C., and Gordon D. Plotkin. ‘Abstract Types Have Existential Types’. In Proceedings of the 12th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages - POPL ’85, 37–51. Association for Computing Machinery, 1985. https://doi.org/10.1145/318593.318606.

@inproceedings{mitchell_1985,
	title = {Abstract types have existential types},
	doi = {10.1145/318593.318606},
	pages = {37--51},
	booktitle = {Proceedings of the 12th {ACM} {SIGACT}-{SIGPLAN} symposium on Principles of Programming Languages  - {POPL} '85},
	publisher = {Association for Computing Machinery},
	author = {Mitchell, John C. and Plotkin, Gordon D.},
	date = {1985},
}

Mitchell, John C., and Gordon D. Plotkin. ‘Abstract Types Have Existential Type’. ACM Transactions on Programming Languages and Systems 10, no. 3 (1988): 470–502. https://doi.org/10.1145/44501.45065. pdf

@article{mitchell_abstract_1988,
	title = {Abstract types have existential type},
	volume = {10},
	doi = {10.1145/44501.45065},
	pages = {470--502},
	number = {3},
	journaltitle = {{ACM} Transactions on Programming Languages and Systems},
	author = {Mitchell, John C. and Plotkin, Gordon D.},
	date = {1988},
	file = {Full Text:C\:\\Users\\Alex\\Zotero\\storage\\9XL9UJHE\\Mitchell and Plotkin - 1988 - Abstract types have existential type.pdf:application/pdf},
}

A method for reasoning operationally about a language with existential types and recursion is presented in

Pitts, A. M. ‘Typed Operational Reasoning’. In Advanced Topics in Types and Programming Languages, edited by B. C. Pierce, 245–89. The MIT Press, 2005. pdf

@incollection{pitts_typed_2005,
	title = {Typed Operational Reasoning},
	pages = {245--289},
	booktitle = {Advanced Topics in Types and Programming Languages},
	publisher = {The {MIT} Press},
	author = {Pitts, A. M.},
	editor = {Pierce, B. C.},
	date = {2005},
}

The equivalence between existential types and their alternative definition through universal types is shown in

Pitts, Andrew M. ‘Parametric Polymorphism and Operational Equivalence’. Mathematical Structures in Computer Science 10, no. 3 (2000): 321–59. https://doi.org/10.1017/S0960129500003066. pdf

@article{pitts_2000,
	title = {Parametric polymorphism and operational equivalence},
	volume = {10},
	url = {https://www.cambridge.org/core/product/identifier/S0960129500003066/type/journal_article},
	doi = {10.1017/S0960129500003066},
	pages = {321--359},
	number = {3},
	journaltitle = {Mathematical Structures in Computer Science},
	author = {Pitts, Andrew M.},
	date = {2000}
}