DROPS

Document

DOI: 10.4230/LIPIcs.TYPES.2019.9

Is Impredicativity Implicitly Implicit?

Authors: Stefan Monnier and Nathaniel Bos

Published in: LIPIcs, Volume 175, 25th International Conference on Types for Proofs and Programs (TYPES 2019)

Abstract

Of all the threats to the consistency of a type system, such as side effects and recursion, impredicativity is arguably the least understood. In this paper, we try to investigate it using a kind of blackbox reverse-engineering approach to map the landscape. We look at it with a particular focus on its interaction with the notion of implicit arguments, also known as erasable arguments. More specifically, we revisit several famous type systems believed to be consistent and which do include some form of impredicativity, and show that they can be refined to equivalent systems where impredicative quantification can be marked as erasable, in a stricter sense than the kind of proof irrelevance notion used for example for Prop terms in systems like Coq. We hope these observations will lead to a better understanding of why and when impredicativity can be sound. As a first step in this direction, we discuss how these results suggest some extensions of existing systems where constraining impredicativity to erasable quantifications might help preserve consistency.

Cite as

Stefan Monnier and Nathaniel Bos. Is Impredicativity Implicitly Implicit?. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 9:1-9:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{monnier_et_al:LIPIcs.TYPES.2019.9,
  author =	{Monnier, Stefan and Bos, Nathaniel},
  title =	{{Is Impredicativity Implicitly Implicit?}},
  booktitle =	{25th International Conference on Types for Proofs and Programs (TYPES 2019)},
  pages =	{9:1--9:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-158-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{175},
  editor =	{Bezem, Marc and Mahboubi, Assia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.9},
  URN =		{urn:nbn:de:0030-drops-130730},
  doi =		{10.4230/LIPIcs.TYPES.2019.9},
  annote =	{Keywords: Impredicativity, Pure type systems, Inductive types, Erasable arguments, Proof irrelevance, Implicit arguments, Universe polymorphism}
}

Search Results

Documents authored by Bos, Nathaniel

Is Impredicativity Implicitly Implicit?

Abstract

Cite as

Thanks for your feedback!

Could not send message