Productive coprogramming with guarded recursion

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

22 Citations (Scopus)

Abstract

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 in- tended to terminate, e.g., servers, we are guaranteed that programs will always be productive. Productivity means that, even if a pro- gram generates an infinite amount of data, each piece will be gen- erated in finite time. The theoretical underpinning for productive programming with infinite output is provided by the category theo- retic notion of final coalgebras. Hence, we speak of coprogramming with non-well-founded codata, as a dual to programming with well- founded data like finite lists and trees.
Systems that offer facilities for productive coprogramming, such as the proof assistants Coq and Agda, currently do so through syntactic guardedness checkers, which ensure that all self-recursive calls are guarded by a use of a constructor. Such a check ensures productivity. Unfortunately, these syntactic checks are not compo- sitional, and severely complicate coprogramming.
Guarded recursion, originally due to Nakano, is tantalising as a basis for a flexible and compositional type-based approach to co- programming. However, as we show, guarded recursion by itself is not suitable for coprogramming due to the fact that there is no way to make finite observations on pieces of infinite data. In this paper, we introduce the concept of clock variables that index Nakano’s guarded recursion. Clock variables allow us to “close over” the generation of infinite codata, and to make finite observations, some- thing that is not possible with guarded recursion alone.
LanguageEnglish
Title of host publicationProceedings of the 2013 ACM SIGPLAN International Conference on Functional Programming
Number of pages12
DOIs
Publication statusAccepted/In press - Sep 2013

Fingerprint

Syntactics
Clocks
Productivity
Functional programming
Servers

Keywords

  • total functional programming
  • coalgebras
  • corecursion
  • guarded recursion

Cite this

Atkey, R., & McBride, C. (Accepted/In press). Productive coprogramming with guarded recursion. In Proceedings of the 2013 ACM SIGPLAN International Conference on Functional Programming https://doi.org/10.1145/2500365.2500597
Atkey, Robert ; McBride, Conor. / Productive coprogramming with guarded recursion. Proceedings of the 2013 ACM SIGPLAN International Conference on Functional Programming . 2013.
@inproceedings{668db9a88d20452f9a9efb31bfd2cf47,
title = "Productive coprogramming with guarded recursion",
abstract = "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 in- tended to terminate, e.g., servers, we are guaranteed that programs will always be productive. Productivity means that, even if a pro- gram generates an infinite amount of data, each piece will be gen- erated in finite time. The theoretical underpinning for productive programming with infinite output is provided by the category theo- retic notion of final coalgebras. Hence, we speak of coprogramming with non-well-founded codata, as a dual to programming with well- founded data like finite lists and trees.Systems that offer facilities for productive coprogramming, such as the proof assistants Coq and Agda, currently do so through syntactic guardedness checkers, which ensure that all self-recursive calls are guarded by a use of a constructor. Such a check ensures productivity. Unfortunately, these syntactic checks are not compo- sitional, and severely complicate coprogramming.Guarded recursion, originally due to Nakano, is tantalising as a basis for a flexible and compositional type-based approach to co- programming. However, as we show, guarded recursion by itself is not suitable for coprogramming due to the fact that there is no way to make finite observations on pieces of infinite data. In this paper, we introduce the concept of clock variables that index Nakano’s guarded recursion. Clock variables allow us to “close over” the generation of infinite codata, and to make finite observations, some- thing that is not possible with guarded recursion alone.",
keywords = "total functional programming, coalgebras, corecursion, guarded recursion",
author = "Robert Atkey and Conor McBride",
year = "2013",
month = "9",
doi = "10.1145/2500365.2500597",
language = "English",
booktitle = "Proceedings of the 2013 ACM SIGPLAN International Conference on Functional Programming",

}

Atkey, R & McBride, C 2013, Productive coprogramming with guarded recursion. in Proceedings of the 2013 ACM SIGPLAN International Conference on Functional Programming . https://doi.org/10.1145/2500365.2500597

Productive coprogramming with guarded recursion. / Atkey, Robert; McBride, Conor.

Proceedings of the 2013 ACM SIGPLAN International Conference on Functional Programming . 2013.

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

TY - GEN

T1 - Productive coprogramming with guarded recursion

AU - Atkey, Robert

AU - McBride, Conor

PY - 2013/9

Y1 - 2013/9

N2 - 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 in- tended to terminate, e.g., servers, we are guaranteed that programs will always be productive. Productivity means that, even if a pro- gram generates an infinite amount of data, each piece will be gen- erated in finite time. The theoretical underpinning for productive programming with infinite output is provided by the category theo- retic notion of final coalgebras. Hence, we speak of coprogramming with non-well-founded codata, as a dual to programming with well- founded data like finite lists and trees.Systems that offer facilities for productive coprogramming, such as the proof assistants Coq and Agda, currently do so through syntactic guardedness checkers, which ensure that all self-recursive calls are guarded by a use of a constructor. Such a check ensures productivity. Unfortunately, these syntactic checks are not compo- sitional, and severely complicate coprogramming.Guarded recursion, originally due to Nakano, is tantalising as a basis for a flexible and compositional type-based approach to co- programming. However, as we show, guarded recursion by itself is not suitable for coprogramming due to the fact that there is no way to make finite observations on pieces of infinite data. In this paper, we introduce the concept of clock variables that index Nakano’s guarded recursion. Clock variables allow us to “close over” the generation of infinite codata, and to make finite observations, some- thing that is not possible with guarded recursion alone.

AB - 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 in- tended to terminate, e.g., servers, we are guaranteed that programs will always be productive. Productivity means that, even if a pro- gram generates an infinite amount of data, each piece will be gen- erated in finite time. The theoretical underpinning for productive programming with infinite output is provided by the category theo- retic notion of final coalgebras. Hence, we speak of coprogramming with non-well-founded codata, as a dual to programming with well- founded data like finite lists and trees.Systems that offer facilities for productive coprogramming, such as the proof assistants Coq and Agda, currently do so through syntactic guardedness checkers, which ensure that all self-recursive calls are guarded by a use of a constructor. Such a check ensures productivity. Unfortunately, these syntactic checks are not compo- sitional, and severely complicate coprogramming.Guarded recursion, originally due to Nakano, is tantalising as a basis for a flexible and compositional type-based approach to co- programming. However, as we show, guarded recursion by itself is not suitable for coprogramming due to the fact that there is no way to make finite observations on pieces of infinite data. In this paper, we introduce the concept of clock variables that index Nakano’s guarded recursion. Clock variables allow us to “close over” the generation of infinite codata, and to make finite observations, some- thing that is not possible with guarded recursion alone.

KW - total functional programming

KW - coalgebras

KW - corecursion

KW - guarded recursion

UR - http://icfpconference.org/icfp2013/

UR - http://bentnib.org/productive.pdf

U2 - 10.1145/2500365.2500597

DO - 10.1145/2500365.2500597

M3 - Conference contribution book

BT - Proceedings of the 2013 ACM SIGPLAN International Conference on Functional Programming

ER -

Atkey R, McBride C. Productive coprogramming with guarded recursion. In Proceedings of the 2013 ACM SIGPLAN International Conference on Functional Programming . 2013 https://doi.org/10.1145/2500365.2500597