License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2019.9
URN: urn:nbn:de:0030-drops-130730
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/13073/
Go to the corresponding LIPIcs Volume Portal

Monnier, Stefan ; Bos, Nathaniel

Is Impredicativity Implicitly Implicit?

pdf-format:
LIPIcs-TYPES-2019-9.pdf (0.6 MB)

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.

BibTeX - Entry

@InProceedings{monnier_et_al:LIPIcs:2020:13073,
  author =	{Stefan Monnier and Nathaniel Bos},
  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 =	{Marc Bezem and Assia Mahboubi},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/13073},
  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}
}

Keywords: Impredicativity, Pure type systems, Inductive types, Erasable arguments, Proof irrelevance, Implicit arguments, Universe polymorphism
Collection: 25th International Conference on Types for Proofs and Programs (TYPES 2019)
Issue Date: 2020
Date of publication: 24.09.2020

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI