Document Open Access Logo

Guarded Recursion in Agda via Sized Types

Authors Niccolò Veltri , Niels van der Weide

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2019.32.pdf
  • Filesize: 0.5 MB
  • 19 pages

Document Identifiers

Author Details

Niccolò Veltri
  • Department of Computer Science, IT University of Copenhagen, Denmark
Niels van der Weide
  • Institute for Computation and Information Sciences, Radboud University, Nijmegen, The Netherlands

Funding

  • Veltri, Niccolò: Veltri was supported by a research grant (13156) from VILLUM FONDEN.

Acknowledgements

We are thankful to Andreas Abel, Guillaume Allais, Herman Geuvers, Rasmus Ejlers Møgelberg and Andrea Vezzosi for discussions and valuable hints. We thank the anonymous referees for their useful comments.

Cite As Get BibTex

Niccolò Veltri and Niels van der Weide. Guarded Recursion in Agda via Sized Types. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 32:1-32:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.FSCD.2019.32

Abstract

In type theory, programming and reasoning with possibly non-terminating programs and potentially infinite objects is achieved using coinductive types. Recursively defined programs of these types need to be productive to guarantee the consistency of the type system. Proof assistants such as Agda and Coq traditionally employ strict syntactic productivity checks, which often make programming with coinductive types convoluted. One way to overcome this issue is by encoding productivity at the level of types so that the type system forbids the implementation of non-productive corecursive programs. In this paper we compare two different approaches to type-based productivity: guarded recursion and sized types. More specifically, we show how to simulate guarded recursion in Agda using sized types. We formalize the syntax of a simple type theory for guarded recursion, which is a variant of Atkey and McBride’s calculus for productive coprogramming. Then we give a denotational semantics using presheaves over the preorder of sizes. Sized types are fundamentally used to interpret the characteristic features of guarded recursion, notably the fixpoint combinator.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Categorical semantics
Keywords
  • guarded recursion
  • type theory
  • semantics
  • coinduction
  • sized types

Metrics

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

References

  1. Martín Abadi, Luca Cardelli, Pierre-Louis Curien, and Jean-Jacques Lévy. Explicit Substitutions. J. Funct. Program., 1(4):375-416, 1991. URL: http://dx.doi.org/10.1017/S0956796800000186.
  2. Andreas Abel. MiniAgda: Integrating Sized and Dependent Types. In Partiality and Recursion in Interactive Theorem Provers, PAR@ITP 2010, Edinburgh, UK, July 15, 2010, pages 18-32, 2010. URL: http://www.easychair.org/publications/paper/51657.
  3. Andreas Abel and James Chapman. Normalization by Evaluation in the Delay Monad: A Case Study for Coinduction via Copatterns and Sized Types. In Proceedings 5th Workshop on Mathematically Structured Functional Programming, MSFP@ETAPS 2014, Grenoble, France, 12 April 2014., pages 51-67, 2014. URL: http://dx.doi.org/10.4204/EPTCS.153.4.
  4. Andreas Abel, Brigitte Pientka, David Thibodeau, and Anton Setzer. Copatterns: Programming Infinite Structures by Observations. In The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, Rome, Italy - January 23 - 25, 2013, pages 27-38, 2013. URL: http://dx.doi.org/10.1145/2429069.2429075.
  5. Andreas Abel and Andrea Vezzosi. A Formalized Proof of Strong Normalization for Guarded Recursive Types. In Programming Languages and Systems - 12th Asian Symposium, APLAS 2014, Singapore, November 17-19, 2014, Proceedings, pages 140-158, 2014. URL: http://dx.doi.org/10.1007/978-3-319-12736-1_8.
  6. Andreas Abel, Andrea Vezzosi, and Théo Winterhalter. Normalization by Evaluation for Sized Dependent Types. PACMPL, 1(ICFP):33:1-33:30, 2017. URL: http://dx.doi.org/10.1145/3110277.
  7. Thorsten Altenkirch and Ambrus Kaposi. Type Theory in Type Theory using Quotient Inductive Types. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 18-29, 2016. URL: http://dx.doi.org/10.1145/2837614.2837638.
  8. Robert Atkey and Conor McBride. Productive Coprogramming with Guarded Recursion. In ACM SIGPLAN International Conference on Functional Programming, ICFP'13, Boston, MA, USA - September 25 - 27, 2013, pages 197-208, 2013. Google Scholar
  9. Patrick Bahr, Hans Bugge Grathwohl, and Rasmus Ejlers Møgelberg. The Clocks are Ticking: No More Delays! In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1-12, 2017. URL: http://dx.doi.org/10.1109/LICS.2017.8005097.
  10. Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Jean-Christophe Filliatre, Eduardo Gimenez, Hugo Herbelin, Gerard Huet, Cesar Munoz, Chetan Murthy, et al. The Coq Proof Assistant Reference Manual: Version 6.1. PhD thesis, Inria, 1997. Google Scholar
  11. Lars Birkedal, Rasmus Ejlers Møgelberg, Jan Schwinghammer, and Kristian Støvring. First Steps in Synthetic Guarded Domain Theory: Step-Indexing in the Topos of Trees. Logical Methods in Computer Science, 8(4), 2012. URL: http://dx.doi.org/10.2168/LMCS-8(4:1)2012.
  12. Aleš Bizjak, Hans Bugge Grathwohl, Ranald Clouston, Rasmus E Møgelberg, and Lars Birkedal. Guarded Dependent Type Theory with Coinductive Types. In International Conference on Foundations of Software Science and Computation Structures, pages 20-35. Springer, 2016. Google Scholar
  13. James Chapman. Type Theory Should Eat Itself. Electr. Notes Theor. Comput. Sci., 228:21-36, 2009. URL: http://dx.doi.org/10.1016/j.entcs.2008.12.114.
  14. Ranald Clouston, Ales Bizjak, Hans Bugge Grathwohl, and Lars Birkedal. Programming and Reasoning with Guarded Recursion for Coinductive Types. In Foundations of Software Science and Computation Structures - 18th International Conference, FoSSaCS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, pages 407-421, 2015. URL: http://dx.doi.org/10.1007/978-3-662-46678-0_26.
  15. Thierry Coquand. Infinite Objects in Type Theory. In Types for Proofs and Programs, International Workshop TYPES'93, Nijmegen, The Netherlands, May 24-28, 1993, Selected Papers, pages 62-78, 1993. URL: http://dx.doi.org/10.1007/3-540-58085-9_72.
  16. Nils Anders Danielsson and Thorsten Altenkirch. Subtyping, Declaratively. In Mathematics of Program Construction, 10th International Conference, MPC 2010, Québec City, Canada, June 21-23, 2010. Proceedings, pages 100-118, 2010. URL: http://dx.doi.org/10.1007/978-3-642-13321-3_8.
  17. John Hughes, Lars Pareto, and Amr Sabry. Proving the Correctness of Reactive Systems Using Sized Types. In Conference Record of POPL'96: The 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Papers Presented at the Symposium, St. Petersburg Beach, Florida, USA, January 21-24, 1996, pages 410-423, 1996. URL: http://dx.doi.org/10.1145/237721.240882.
  18. Saunders MacLane and Ieke Moerdijk. Sheaves in geometry and logic: A first introduction to topos theory. Springer Science &Business Media, 1992. Google Scholar
  19. Bassel Mannaa and Rasmus Ejlers Møgelberg. The Clocks They Are Adjunctions Denotational Semantics for Clocked Type Theory. In 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018, July 9-12, 2018, Oxford, UK, pages 23:1-23:17, 2018. URL: http://dx.doi.org/10.4230/LIPIcs.FSCD.2018.23.
  20. Rasmus Ejlers Møgelberg. A Type Theory for Productive Coprogramming via Guarded Recursion. In Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014, pages 71:1-71:10, 2014. URL: http://dx.doi.org/10.1145/2603088.2603132.
  21. Hiroshi Nakano. A Modality for Recursion. In 15th Annual IEEE Symposium on Logic in Computer Science, Santa Barbara, California, USA, June 26-29, 2000, pages 255-266, 2000. URL: http://dx.doi.org/10.1109/LICS.2000.855774.
  22. Ulf Norell. Dependently Typed Programming in Agda. In Proceedings of TLDI'09: 2009 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Savannah, GA, USA, January 24, 2009, pages 1-2, 2009. Google Scholar
  23. Jorge Luis Sacchini. Type-Based Productivity of Stream Definitions in the Calculus of Constructions. In 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013, pages 233-242, 2013. URL: http://dx.doi.org/10.1109/LICS.2013.29.
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact