research-article

Open access

A reasonably exceptional type theory

Authors:

Pierre-Marie Pédrot,

Nicolas Tabareau,

Hans Jacob Fehrmann,

Éric TanterAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 3, Issue ICFP

Article No.: 108, Pages 1 - 29

https://doi.org/10.1145/3341712

Published: 26 July 2019 Publication History

Abstract

Traditional approaches to compensate for the lack of exceptions in type theories for proof assistants have severe drawbacks from both a programming and a reasoning perspective.

Pédrot and Tabareau recently extended the Calculus of Inductive Constructions (CIC) with exceptions. The new exceptional type theory is interpreted by a translation into CIC, covering full dependent elimination, decidable type-checking and canonicity. However, the exceptional theory is inconsistent as a logical system. To recover consistency, Pédrot and Tabareau propose an additional translation that uses parametricity to enforce that all exceptions are caught locally. While this enforcement brings logical expressivity gains over CIC, it completely prevents reasoning about exceptional programs such as partial functions.

This work addresses the dilemma between exceptions and consistency in a more flexible manner, with the Reasonably Exceptional Type Theory (RETT). RETT is structured in three layers: (a) the exceptional layer, in which all terms can raise exceptions; (b) the mediation layer, in which exceptional terms must be provably parametric; (c) the pure layer, in which terms are non-exceptional, but can refer to exceptional terms.

We present the general theory of RETT, where each layer is realized by a predicative hierarchy of universes, and develop an instance of RETT in Coq: the impure layer corresponds to the predicative universe hierarchy, the pure layer is realized by the impredicative universe of propositions, and the mediation layer is reified via a parametricity type class. RETT is the first full dependent type theory to support consistent reasoning about exceptional terms, and the CoqRETT plugin readily brings this ability to Coq programmers.

Supplementary Material

WEBM File (a108-pedrot.webm)

Download
104.23 MB

References

[1]

Danel Ahman, Neil Ghani, and Gordon D. Plotkin. 2016. Dependent Types and Fibred Computational Effects. In 19th International Conference on Foundations of Software Science and Computation Structures. Springer Berlin Heidelberg, Eindhoven, The Netherlands, 36–54.

[2]

Gilles Barthe, John Hatcliff, and Morten Heine B. Sørensen. 1999. CPS Translations and Applications: The Cube and Beyond. Higher Order Symbol. Comput. 12, 2 (Sept. 1999), 125–170.

Digital Library

[3]

Jean-Philippe Bernardy and Marc Lasson. 2011. Realizability and Parametricity in Pure Type Systems. In Foundations of Software Science and Computational Structures, Vol. 6604. Saarbrücken, Germany, 108–122.

Digital Library

[4]

Yves Bertot and Pierre Castéran. 2004. Interactive Theorem Proving and Program Development.

Digital Library

[5]

Simon Boulier, Pierre-Marie Pédrot, and Nicolas Tabareau. 2017. The next 700 syntactical models of type theory. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017. 182–194.

Digital Library

[6]

William Bowman, Youyou Cong, Nick Rioux, and Amal Ahmed. 2018. Type-Preserving CPS Translation of Σ and Π Types is Not Not Possible. In Proceedings of the 45st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’18). ACM, New York, NY, USA.

Digital Library

[7]

Edwin Brady. 2013. Idris, a general-purpose dependently typed programming language: Design and implementation. Journal of Functional Programming 23, 05 (2013), 552–593.

[8]

Joachim Breitner, Antal Spector-Zabusky, Yao Li, Christine Rizkallah, John Wiegley, and Stephanie Weirich. 2018. Ready, Set, Verify! Applying hs-to-coq to Real-World Haskell Code (Experience Report). Proceedings of the ACM on Programming Languages 2, ICFP (Sept. 2018), 89:1–89:16.

Digital Library

[9]

Chris Casinghino, Vilhelm Sjöberg, and Stephanie Weirich. 2014. Combining Proofs and Programs in a Dependently Typed Language. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’14). ACM, New York, NY, USA, 33–45.

Digital Library

[10]

Adam Chlipala, Gregory Malecha, Greg Morrisett, Avraham Shinnar, and Ryan Wisnesky. 2009. Effective Interactive Proofs for Higher-order Imperative Programs. In Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming (ICFP ’09). ACM, New York, NY, USA, 79–90.

Digital Library

[11]

Jesper Cockx and Andreas Abel. 2016. Sprinkles of Extensionality for Your Vanilla Type Theory. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016).

[12]

Thierry Coquand and Gérard P. Huet. 1988. The Calculus of Constructions. Inf. Comput. 76, 2/3 (1988), 95–120.

Digital Library

[13]

Guilhem Jaber, Gabriel Lewertowski, Pierre-Marie Pédrot, Matthieu Sozeau, and Nicolas Tabareau. 2016. The Definitional Side of the Forcing. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16, New York, NY, USA, July 5-8, 2016. 367–376.

Digital Library

[14]

Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. 2014. CakeML: A Verified Implementation of ML. In Principles of Programming Languages (POPL). ACM Press, 179–191.

Digital Library

[15]

Xavier Leroy, Sandrine Blazy, Daniel Kästner, Bernhard Schommer, Markus Pister, and Christian Ferdinand. 2016. CompCert – A Formally Verified Optimizing Compiler. In ERTS 2016: Embedded Real Time Software and Systems. SEE.

[16]

Pierre Letouzey. 2004. Programmation fonctionnelle certifiée : l’extraction de programmes dans l’assistant Coq. Ph.D. Dissertation. Université Paris XI.

[17]

Paul Blain Levy. 2001. Call-by-push-value. Ph.D. Dissertation. Queen Mary, University of London.

[18]

Assia Mahboubi and Enrico Tassi. 2008. Mathematical Components.

[19]

Eugenio Moggi. 1991. Notions of Computation and Monads. Information and Computation 93, 1 (July 1991), 55–92.

Digital Library

[20]

Aleksandar Nanevski, Greg Morrisett, and Lars Birkedal. 2008. Hoare type theory, polymorphism and separation. Journal of Functional Programming 18, 5-6 (2008), 865–911.

Digital Library

[21]

Ulf Norell. 2009. Dependently Typed Programming in Agda. In Advanced Functional Programming (AFP 2008) (LNCS), Vol. 5832. Springer, 230–266.

Digital Library

[22]

Pierre-Marie Pédrot and Nicolas Tabareau. 2017. An effectful way to eliminate addiction to dependence. In 32nd Annual Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017. 1–12.

Digital Library

[23]

Pierre-Marie Pédrot and Nicolas Tabareau. 2018. Failure is Not an Option - An Exceptional Type Theory. In Proceedings of the 27th European Symposium on Programming Languages and Systems (ESOP 2018), Amal Ahmed (Ed.), Vol. 10801. Thessaloniki, Greece, 245–271.

[24]

The Coq Development Team. 2019. The Coq Proof Assistant Reference Manual. (2019). https://coq.inria.fr/refman

[25]

John C. Reynolds. 1983. Types, Abstraction and Parametric Polymorphism. In IFIP Congress (2002-01-03). 513–523.

[26]

Matthieu Sozeau and Nicolas Oury. 2008. First-Class Type Classes. In Proceedings of the 21st International Conference on Theorem Proving in Higher-Order Logics. Montreal, Canada, 278–293.

Digital Library

[27]

Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoue, and Santiago Zanella-Béguelin. 2016. Dependent Types and Multi-Monadic Effects in F*. In 43nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). ACM, 256–270. https://www.fstar-lang.org/papers/mumon/

Digital Library

[28]

Univalent Foundations Project. 2013. Homotopy Type Theory: Univalent Foundations for Mathematics. http:// homotopytypetheory.org/book .

[29]

Matthijs Vákár. 2015. A Framework for Dependent Types and Effects. (2015). arXiv: arXiv:1512.08009 draft.

[30]

Freek Wiedijk. 2012. Pollack-inconsistency. Electronic Notes in Theoretical Computer Science 285 (2012), 85 – 100.

Digital Library

[31]

Hongwei Xi and Frank Pfenning. 1999. Dependent Types in Practical Programming. In Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’99). ACM, New York, NY, USA, 214–227.

Digital Library

Cited By

Poiret JGilbert GMaillard KPédrot PSozeau MTabareau NTanter É(2025)All Your Base Are Belong to Us: Sort Polymorphism for Proof AssistantsProceedings of the ACM on Programming Languages10.1145/37049129:POPL(2253-2281)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704912
Torczon CSuárez Acevedo EAgrawal SVelez-Ginorio JWeirich S(2024)Effects and Coeffects in Call-by-Push-ValueProceedings of the ACM on Programming Languages10.1145/36897508:OOPSLA2(1108-1134)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689750
Malewski MMaillard KTabareau NTanter É(2024)Gradual Indexed Inductive TypesProceedings of the ACM on Programming Languages10.1145/36746448:ICFP(544-572)Online publication date: 15-Aug-2024
https://doi.org/10.1145/3674644
Show More Cited By

Index Terms

A reasonably exceptional type theory
1. Theory of computation
  1. Logic
    1. Type theory
  2. Semantics and reasoning
    1. Program constructs
      1. Functional constructs
    2. Program reasoning
      1. Program verification

Recommendations

A reasonably gradual type theory

Gradualizing the Calculus of Inductive Constructions (CIC) involves dealing with subtle tensions between normalization, graduality, and conservativity with respect to CIC. Recently, GCIC has been proposed as a parametrized gradual type theory that admits ...
Type-preserving CPS translation of Σ and Π types is not not possible

Dependently typed languages such as Coq are used to specify and prove functional correctness of source programs, but what we ultimately need are guarantees about correctness of compiled code. By preserving dependent types through each compiler pass, we ...
Parametric quantifiers for dependent type theory

Polymorphic type systems such as System F enjoy the parametricity property: polymorphic functions cannot inspect their type argument and will therefore apply the same algorithm to any type they are instantiated on. This idea is formalized mathematically ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 3, Issue ICFP

August 2019

1054 pages

EISSN:2475-1421

DOI:10.1145/3352468

Issue’s Table of Contents

Copyright © 2019 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 26 July 2019

Published in PACMPL Volume 3, Issue ICFP

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
721
Total Downloads

Downloads (Last 12 months)130
Downloads (Last 6 weeks)23

Reflects downloads up to 16 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Poiret JGilbert GMaillard KPédrot PSozeau MTabareau NTanter É(2025)All Your Base Are Belong to Us: Sort Polymorphism for Proof AssistantsProceedings of the ACM on Programming Languages10.1145/37049129:POPL(2253-2281)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704912
Torczon CSuárez Acevedo EAgrawal SVelez-Ginorio JWeirich S(2024)Effects and Coeffects in Call-by-Push-ValueProceedings of the ACM on Programming Languages10.1145/36897508:OOPSLA2(1108-1134)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689750
Malewski MMaillard KTabareau NTanter É(2024)Gradual Indexed Inductive TypesProceedings of the ACM on Programming Languages10.1145/36746448:ICFP(544-572)Online publication date: 15-Aug-2024
https://doi.org/10.1145/3674644
Maillard KLennon-Bertrand MTabareau NTanter É(2022)A reasonably gradual type theoryProceedings of the ACM on Programming Languages10.1145/35476556:ICFP(931-959)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547655
Lennon-Bertrand MMaillard KTabareau NTanter É(2022)Gradualizing the Calculus of Inductive ConstructionsACM Transactions on Programming Languages and Systems10.1145/349552844:2(1-82)Online publication date: 30-Jun-2022
https://doi.org/10.1145/3495528
Cockx JTabareau NWinterhalter T(2021)The taming of the rew: a type theory with computational assumptionsProceedings of the ACM on Programming Languages10.1145/34343415:POPL(1-29)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434341
VAN STRYDONCK TPIESSENS FDEVRIESE D(2021)Linear capabilities for fully abstract compilation of separation-logic-verified codeJournal of Functional Programming10.1017/S095679682100002231Online publication date: 30-Mar-2021
https://doi.org/10.1017/S0956796821000022

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Figures

Tables

Media

View Issue’s Table of Contents