Is Impredicativity Implicitly Implicit?

Authors Stefan Monnier , Nathaniel Bos



PDF
Thumbnail PDF

File

LIPIcs.TYPES.2019.9.pdf
  • Filesize: 0.55 MB
  • 19 pages

Document Identifiers

Author Details

Stefan Monnier
  • Université de Montréal - DIRO, Canada
Nathaniel Bos
  • McGill University - SOCS, Montréal, Canada

Acknowledgements

We would like to thank Chris League for his comments on earlier drafts of the paper, as well as the reviewers for their careful reading and very helpful feedback.

Cite AsGet BibTex

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)
https://doi.org/10.4230/LIPIcs.TYPES.2019.9

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Higher order logic
  • Software and its engineering → Functional languages
Keywords
  • Impredicativity
  • Pure type systems
  • Inductive types
  • Erasable arguments
  • Proof irrelevance
  • Implicit arguments
  • Universe polymorphism

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. Andreas Abel and Thierry Coquand. Failure of normalization in impredicative type theory with proof-irrelevant propositional equality, February 2020. Submitted to Logical Methods in Computer Science. URL: http://arxiv.org/abs/1911.08174.
  2. Andreas Abel and Gabriel Scherer. On irrelevance and algorithmic equality in predicative type theory. Logical Methods in Computer Science, 8(1:29):1-36, 2012. URL: https://doi.org/10.2168/LMCS-8(1:29)2012.
  3. Lennart Augustsson. Cayenne - a language with dependent types. In International Conference on Functional Programming, page 239–250. ACM Press, September 1998. URL: https://doi.org/10.1145/291251.289451.
  4. Henk P. Barendregt. Introduction to generalized type systems. Journal of Functional Programming, 1(2):121-154, April 1991. URL: https://doi.org/10.1017/S0956796800020025.
  5. Bruno Barras and Bruno Bernardo. Implicit calculus of constructions as a programming language with dependent types. In Conference on Foundations of Software Science and Computation Structures, volume 4962 of Lecture Notes in Computer Science, Budapest, Hungary, April 2008. URL: https://doi.org/10.1007/978-3-540-78499-9_26.
  6. Bruno Bernardo. Towards an implicit calculus of inductive constructions. extending the implicit calculus of constructions with union and subset types. In International Conference on Theorem Proving in Higher-Order Logics, volume 5674 of Lecture Notes in Computer Science, August 2009. URL: https://hal.inria.fr/inria-00432649.
  7. Jean-Philippe Bernardy, Patrik Jansson, and Ross Paterson. Proofs for free: Parametricity for dependent types. Journal of Functional Programming, 22(2):1-46, 2012. URL: https://doi.org/10.1017/S0956796812000056.
  8. Ana Bove, Peter Dybjer, and Ulf Norell. A brief overview of Agda – a functional language with dependent types. In International Conference on Theorem Proving in Higher-Order Logics, volume 5674 of Lecture Notes in Computer Science, pages 73-78, August 2009. URL: https://doi.org/10.1007/978-3-642-03359-9_6.
  9. Luca Cardelli. Phase distinctions in type theory. DEC-SRC manuscript, 1988. URL: https://pdfs.semanticscholar.org/4cb5/7987b78c5124bc0857155f99c11aa321546d.pdf.
  10. Adam Chlipala. Parametric higher-order abstract syntax for mechanized semantics. In International Conference on Functional Programming, Victoria, BC, September 2008. URL: https://doi.org/10.1145/1411204.1411226.
  11. Thierry Coquand. An analysis of Girard’s paradox. In Annual Symposium on Logic in Computer Science, 1986. Also published as INRIA tech-report RR-0531. URL: https://hal.inria.fr/inria-00076023.
  12. Thierry Coquand. A new paradox in type theory. In Logic, Methodology, and Philosophy of Science, pages 7-14, 1994. URL: https://doi.org/10.1016/S0049-237X(06)80062-5.
  13. Thomas Fruchart and Guiseppe Longo. Carnap’s remarks on impredicative definitions and the genericity theorem. Technical Report LIENS-96-22, ENS, Paris, 1996. URL: ftp://ftp.di.ens.fr/pub/reports/liens-96-22.A4.ps.Z.
  14. Herman Geuvers. (In)consistency of extensions of higher order logic and type theory. In Types for Proofs and Programs, pages 140-159, 2006. URL: https://doi.org/10.1007/978-3-540-74464-1_10.
  15. Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, and Nicolas Tabareau. Definitional proof-irrelevance without K. In Symposium on Principles of Programming Languages, pages 3:1-3:28. ACM Press, 2019. URL: https://doi.org/10.1145/3290316.
  16. Eduardo Giménez. Codifying guarded definitions with recursive schemes. Technical Report RR1995-07, École Normale Supérieure de Lyon, 1994. URL: ftp://ftp.ens-lyon.fr/pub/LIP/Rapports/RR/RR1995/RR1995-07.ps.Z.
  17. J. Y. Girard. Interprétation Fonctionnelle et Élimination des Coupures dans l'Arithmétique d'Ordre Supérieur. PhD thesis, University of Paris VII, 1972. URL: https://pdfs.semanticscholar.org/e1a1/c345ce8ab4c11f176f1c42bcfc6a62ef4e3c.pdf.
  18. Gérard P. Huet, Christine Paulin-Mohring, et al. The Coq proof assistant reference manual. Part of the Coq system version 6.3.1, May 2000. Google Scholar
  19. Antonius Hurkens. A simplification of Girard’s paradox. In International conference on Typed Lambda Calculi and Applications, pages 266-278, 1995. URL: https://doi.org/10.1007/BFb0014058.
  20. Zhaohui Luo. A unifying theory of dependent types: the schematic approach. In Logical Foundations of Computer Science, 1992. URL: https://doi.org/10.1007/BFb0023883.
  21. Alexandre Miquel. The implicit calculus of constructions: extending pure type systems with an intersection type binder and subtyping. In International conference on Typed Lambda Calculi and Applications, pages 344-359, 2001. URL: https://doi.org/10.1007/3-540-45413-6_27.
  22. Nathan Mishra-Linger and Tim Sheard. Erasure and polymorphism in pure type systems. In Conference on Foundations of Software Science and Computation Structures, volume 4962 of Lecture Notes in Computer Science, pages 350-364, Budapest, Hungary, April 2008. URL: https://doi.org/10.1007/978-3-540-78499-9_25.
  23. Stefan Monnier. The Swiss coercion. In Programming Languages meets Program Verification, pages 33-40, Freiburg, Germany, September 2007. ACM Press. URL: https://doi.org/10.1145/1292597.1292604.
  24. Stefan Monnier. Typer: ML boosted with type theory and Scheme. In Journées Francophones des Langages Applicatifs, pages 193-208, 2019. URL: https://hal.inria.fr/hal-01985195/.
  25. Kasper Svendsen and Lars Birkedal. Impredicative concurrent abstract predicates. In European Symposium on Programming, pages 149-168, 2014. URL: https://doi.org/10.1007/978-3-642-54833-8_9.
  26. Matúš Tejiščák. Erasure in Dependently Typed Programming. PhD thesis, University of St Andrews, 2020. Google Scholar
  27. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, 2013. URL: http://arxiv.org/abs/1308.0729.
  28. Taichi Uemura. Cubical assemblies, a univalent and impredicative universe and a failure of propositional resizing. In Types for Proofs and Programs, volume 130 of Leibniz International Proceedings in Informatics (LIPIcs), pages 7:1-7:20, 2019. URL: https://doi.org/10.4230/LIPIcs.TYPES.2018.7.
  29. Benjamin Werner. Une Théorie des Constructions Inductives. PhD thesis, A L'Université Paris 7, Paris, France, 1994. URL: https://hal.inria.fr/tel-00196524/.
  30. Benjamin Werner. On the strength of proof-irrelevant type theories. Logical Methods in Computer Science, 4(3):1-20, 2008. URL: https://doi.org/10.1007/11814771_49.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail