research-article

A Generalized Modality for Recursion

Author:

Adrien GuattoAuthors Info & Claims

LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science

Pages 482 - 491

https://doi.org/10.1145/3209108.3209148

Published: 09 July 2018 Publication History

Abstract

Nakano's later modality allows types to express that the output of a function does not immediately depend on its input, and thus that computing its fixpoint is safe. This idea, guarded recursion, has proved useful in various contexts, from functional programming with infinite data structures to formulations of step-indexing internal to type theory. Categorical models have revealed that the later modality corresponds in essence to a simple reindexing of the discrete time scale.

Unfortunately, existing guarded type theories suffer from significant limitations for programming purposes. These limitations stem from the fact that the later modality is not expressive enough to capture precise input-output dependencies of functions. As a consequence, guarded type theories reject many productive definitions.

Combining insights from guarded type theories and synchronous programming languages, we propose a new modality for guarded recursion. This modality can apply any well-behaved reindexing of the time scale to a type. We call such reindexings time warps. Several modalities from the literature, including later, correspond to fixed time warps, and thus arise as special cases of ours.

References

[1]

Nada Amin and Tiark Rompf. 2017. Type Soundness Proofs with Definitional Interpreters. Principles of Programming Languages (POPL'17).

Digital Library

[2]

Robert Atkey. 2006. Substructural Simple Type Theories for Separation and In-place Update. Ph.D. Dissertation. University of Edinburgh.

[3]

Robert Atkey and Conor McBride. 2013. Productive Coprogramming with Guarded Recursion. In International Conference on Functional Programming (ICFP 2013). ACM.

Digital Library

[4]

Patrick Bahr, Hans Bugge Grathwohl, and Rasmus Ejlers Møgelberg. 2017. The Clocks Are Ticking: No More Delays! Reduction Semantics for Type Theory with Guarded Recursion. In Logic in Computer Science (LICS'17). Springer.

[5]

Gavin Bierman and Valeria de Paiva. 2000. On an Intuitionistic Modal Logic. Studia Logica 65, 3 (2000), 383--416.

[6]

Lars Birkedal, Ales Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, and Andrea Vezzosi. 2016. Guarded Cubical Type Theory: Path Equality for Guarded Recursion. In Computer Science Logic (CSL'16).

[7]

Lars Birkedal, Rasmus Ejlers Møgelberg, Jan Schwinghammer, and Kristian Støvring. 2012. First steps in synthetic guarded domain theory: step-indexing in the topos of trees. Logical Methods in Computer Science 8, 4 (2012).

Digital Library

[8]

Ale Bizjak, Hans Bugge Grathwohl, Ranald Clouston, Rasmus E. Møgelberg, and Lars Birkedal. 2016. Guarded Dependent Type Theory with Coinductive Types. In Foundations of Software Science and Computation Structures (FoSSaCS'16). Springer.

[9]

Val Breazu-Tannen, Thierry Coquand, Carl A. Gunther, and Andre Scedrov. 1991. Inheritance as Implicit Coercion. Information and Computation (1991).

Digital Library

[10]

Jean Bénabou. 2000. Distributors at Work. (2000).

[11]

Paul Caspi, Daniel Pilaud, Nicolas Halbwachs, and John Plaice. 1987. LUSTRE: A declarative language for programming synchronous systems. In Principles of Programming Languages (POPL'87).

Digital Library

[12]

Paul Caspi and Marc Pouzet. 1996. Synchronous Kahn Networks. In International Conference on Functional Programming (ICFP'96). ACM.

Digital Library

[13]

Ranald Clouston, Ales Bizjak, Hans Bugge Grathwohl, and Lars Birkedal. 2016. The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types. Logical Methods in Computer Science (2016).

[14]

Albert Cohen, Marc Duranton, Christine Eisenbeis, Claire Pagetti, Florence Plateau, and Marc Pouzet. 2006. N-synchronous Kahn networks: a relaxed model of synchrony for real-time systems. In Principles of Programming Languages (POPL '06).

Digital Library

[15]

Pierre-Louis Curien, Marcelo Fiore, and Guillaume Munch-Maccagnoni. 2016. A Theory of Effects and Resources: Adjunction Models and Polarised Calculi. In Principles of Programming Languages (POPL'16). ACM.

Digital Library

[16]

Pierre-Louis Curien and Giorgio Ghelli. 1990. Coherence of subsumption. In Colloquium on Trees in Algebra and Programming (CAAP'90). Springer.

Digital Library

[17]

Julien Forget, Fréderic Boniol, Daniel Lesens, and Claire Pagetti. 2008. A Multi-Periodic Synchronous Data-Flow Language. In High-Assurance Systems Engineering (HASE'08). IEEE.

Digital Library

[18]

Adrien Guatto. 2016. A Synchronous Functional Language with Integer Clocks. Ph.D. Dissertation. École normale supérieure.

[19]

Martin Hyland. 2010. Some Reasons for Generalising Domain Theory. Mathematical Structures in Computer Science 20, 02 (Mar 2010), 239.

Digital Library

[20]

Neelakantan R Krishnaswami. 2013. Higher-Order Functional Reactive Programming without Spacetime Leaks. In International Conference on Functional Programming (ICFP'13). ACM.

Digital Library

[21]

Neelakantan R. Krishnaswami and Nick Benton. 2011. Ultrametric Semantics of Reactive Programs. In Logic in Computer Science (LICS'11). IEEE.

Digital Library

[22]

Joachim Lambek and Philip J. Scott. 1986. Introduction to Higher-Order Categorical Logic. Cambridge University Press.

Digital Library

[23]

Conor McBride and Ross Paterson. 2008. Applicative Programming with Effects. Journal of Functional Programming 18, 1 (2008), 1--13.

Digital Library

[24]

Paul-André Melliès and Noam Zeilberger. 2015. Functors Are Type Refinement Systems. In Principles of Programming Languages (POPL '15). ACM.

Digital Library

[25]

Paul-André Melliès and Noam Zeilberger. 2016. A bifibrational reconstruction of Lawveres presheaf hyperdoctrine. In Logic in Computer Science (LICS'16). IEEE.

Digital Library

[26]

Rasmus Ejlers Møgelberg. 2014. A type theory for productive coprogramming with guarded recursion. In Logic in Computer Science (LICS'14). IEEE.

[27]

Hiroshi Nakano. 2000. A Modality for Recursion. In Logic in Computer Science (LICS '00). IEEE.

Digital Library

[28]

Frank Pfenning and Rowan Davies. 2001. A Judgmental Reconstruction of Modal Logic. Mathematical Structures in Computer Science 11, 04 (Jul 2001).

Digital Library

[29]

Florence Plateau. 2010. Modèle n-synchrone pour la programmation de réseaux de Kahn à mémoire bornée. Ph.D. Dissertation. Université Paris-Sud.

[30]

Marc Pouzet. 2006. Lucid Synchrone, version 3. Tutorial and reference manual. Université Paris-Sud, LRI.

[31]

Paula Severi. 2017. A Light Modality for Recursion. In Foundations of Software Science and Computation Structures (FoSSaCS'17). Springer.

Digital Library

Cited By

Gratzer D(2025)A Modal Deconstruction of Löb InductionProceedings of the ACM on Programming Languages10.1145/37048669:POPL(864-892)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704866
Ceulemans JNuyts ADevriese D(2025)BiSikkel: A Multimode Logical Framework in AgdaProceedings of the ACM on Programming Languages10.1145/37048449:POPL(210-240)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704844
Fukaishi RKobayashi NSato RKeller GWang M(2024)Productivity Verification for Functional Programs by Reduction to Termination VerificationProceedings of the 2024 ACM SIGPLAN International Workshop on Partial Evaluation and Program Manipulation10.1145/3635800.3636963(70-82)Online publication date: 11-Jan-2024
https://dl.acm.org/doi/10.1145/3635800.3636963
Show More Cited By

Recommendations

Productive coprogramming with guarded recursion
ICFP '13: Proceedings of the 18th ACM SIGPLAN international conference on Functional programming

Total functional programming offers the beguiling vision that, just by virtue of the compiler accepting a program, we are guaranteed that it will always terminate. In the case of programs that are not intended to terminate, e.g., servers, we are ...
A type theory for productive coprogramming via guarded recursion
CSL-LICS '14: Proceedings of the 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)

To ensure consistency and decidability of type checking, proof assistants impose a requirement of productivity on corecursive definitions. In this paper we investigate a type-based alternative to the existing syntactic productivity checks of Coq and ...
A functional programmer's guide to homotopy type theory
ICFP '16

Dependent type theories are functional programming languages with types rich enough to do computer-checked mathematics and software verification. Homotopy type theory is a recent area of work that connects dependent type theory to the mathematical ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science

July 2018

960 pages

ISBN:9781450355834

DOI:10.1145/3209108

Copyright © 2018 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGLOG: ACM Special Interest Group on Logic and Computation
EACSL: European Association for Computer Science Logic
IEEE-CS\DATC: IEEE Computer Society

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 09 July 2018

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed limited

Funding Sources

Deutsche Forschungsgemeinschaft

Conference

LICS '18

Sponsor:

SIGLOG
EACSL
IEEE-CS\DATC

LICS '18: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science

July 9 - 12, 2018

Oxford, United Kingdom

Acceptance Rates

Overall Acceptance Rate 215 of 622 submissions, 35%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

12
Total Citations
View Citations
157
Total Downloads

Downloads (Last 12 months)13
Downloads (Last 6 weeks)2

Reflects downloads up to 19 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Gratzer D(2025)A Modal Deconstruction of Löb InductionProceedings of the ACM on Programming Languages10.1145/37048669:POPL(864-892)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704866
Ceulemans JNuyts ADevriese D(2025)BiSikkel: A Multimode Logical Framework in AgdaProceedings of the ACM on Programming Languages10.1145/37048449:POPL(210-240)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704844
Fukaishi RKobayashi NSato RKeller GWang M(2024)Productivity Verification for Functional Programs by Reduction to Termination VerificationProceedings of the 2024 ACM SIGPLAN International Workshop on Partial Evaluation and Program Manipulation10.1145/3635800.3636963(70-82)Online publication date: 11-Jan-2024
https://dl.acm.org/doi/10.1145/3635800.3636963
Broy M(2023)Specification and verification of concurrent systems by causality and realizabilityTheoretical Computer Science10.1016/j.tcs.2023.114106974(114106)Online publication date: Sep-2023
https://doi.org/10.1016/j.tcs.2023.114106
Bazerman GPolikarpova N(2022)A totally predictable outcome: an investigation of traversals of infinite structuresProceedings of the 15th ACM SIGPLAN International Haskell Symposium10.1145/3546189.3549915(39-53)Online publication date: 6-Sep-2022
https://dl.acm.org/doi/10.1145/3546189.3549915
BAHR P(2022)Modal FRP for all: Functional reactive programming without space leaks in HaskellJournal of Functional Programming10.1017/S095679682200013232Online publication date: 26-Dec-2022
https://doi.org/10.1017/S0956796822000132
Bahr PGraulund CMøgelberg R(2021)Diamonds are not forever: liveness in reactive programming with guarded recursionProceedings of the ACM on Programming Languages10.1145/34342835:POPL(1-28)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434283
van Gool SGuatto AMetcalfe GSantschi S(2021)Time Warps, from Algebra to AlgorithmsRelational and Algebraic Methods in Computer Science10.1007/978-3-030-88701-8_19(309-324)Online publication date: 2-Nov-2021
https://dl.acm.org/doi/10.1007/978-3-030-88701-8_19
Jaber GRiba C(2021)Temporal Refinements for Guarded Recursive TypesProgramming Languages and Systems10.1007/978-3-030-72019-3_20(548-578)Online publication date: 27-Mar-2021
https://dl.acm.org/doi/10.1007/978-3-030-72019-3_20
Gratzer DKavvos GNuyts ABirkedal LHermanns HZhang LKobayashi NMiller D(2020)Multimodal Dependent Type TheoryProceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3373718.3394736(492-506)Online publication date: 8-Jul-2020
https://dl.acm.org/doi/10.1145/3373718.3394736
Show More Cited By

View Options

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 Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten