skip to main content
10.1145/1411204.1411232acmconferencesArticle/Chapter ViewAbstractPublication PagesicfpConference Proceedingsconference-collections
research-article

Functional pearl: streams and unique fixed points

Published: 20 September 2008 Publication History

Abstract

Streams, infinite sequences of elements, live in a coworld: they are given by a coinductive data type, operations on streams are implemented by corecursive programs, and proofs are conducted using coinduction. But there is more to it: suitably restricted, stream equations possess unique solutions, a fact that is not very widely appreciated. We show that this property gives rise to a simple and attractive proof technique essentially bringing equational reasoning to the coworld. In fact, we redevelop the theory of recurrences, finite calculus and generating functions using streams and stream operators building on the cornerstone of unique solutions. The development is constructive: streams and stream operators are implemented in Haskell, usually by one-liners. The resulting calculus or library, if you wish, is elegant and fun to use. Finally, we rephrase the proof of uniqueness using generalised algebraic data types.

Supplementary Material

JPG File (1411232.jpg)
index.html (index.html)
Slides from the presentation
ZIP File (p189-slides.zip)
Supplemental material for: Functional pearl: streams and unique fixed points
Audio only (1411232.mp3)
Video (1411232.mp4)

References

[1]
P. Aczel and N. Mendler. A final coalgebra theorem. In D.H. Pitt, D.E. Rydeheard, P. Dybjer, and A. Poigné, editors, Category Theory and Computer Science (Manchester), LNCS 389, pages 357--365, 1989. Springer.
[2]
Thierry Coquand. Infinite objects in type theory. In H. Barendregt and T. Nipkow, editors, Types for Proofs and Programs, International Workshop TYPES'93, Nijmegen, The Netherlands, May 24-28, 1993, Selected Papers, LNCS 806, pages 62--78, 1994. Springer.
[3]
Jeremy Gibbons and Graham Hutton. Proof methods for corecursive programs. Fundamenta Informaticae, (XX): 1--14, 2005.
[4]
Ronald L. Graham, Donald E. Knuth, and Oren Patashnik. Concrete mathematics. Addison-Wesley, 2nd edition, 1994.
[5]
Ralf Hinze. Fun with antom types. In Jeremy Gibbons and Oege de Moor, editors, The Fun of Programming, pages 245--262. Palgrave Macmillan, 2003. ISBN 1-4039-0772-2 hardback, ISBN 0-333-99285-7 paperback.
[6]
Ralf Hinze and Andres Löh. Guide2lhs2tex (for version 1.13), February 2008. http://people.cs.uu.nl/andres/lhs2tex/.
[7]
Jerzy Karczmarczuk. Generating power of lazy semantics. Theoretical Computer Science, (187): 203--219, 1997.
[8]
M. Douglas McIlroy. The music of streams. Information Processing Letters, (77): 189--195, 2001.
[9]
M. Douglas McIlroy. Power series, power serious. J. Functional Programming, 3 (9): 325--337, May 1999.
[10]
Simon Peyton Jones. Haskell 98 Language and Libraries. Cambridge University Press, 2003.
[11]
S. Peyton Jones, D. Vytiniotis, S. Weirich, and G. Washburn. Simple unification-based type inference for GADTs. In J. Lawall, editor, Proceedings of the 11th ACM SIGPLAN international conference on Functional programming, Portland, 2006, pages 50--61. ACM Press, 2006.
[12]
J.J.M.M. Rutten. Fundamental study - Behavioural differential equations: a coinductive calculus of streams, automata, and power series. Theoretical Computer Science, (308): 1--53, 2003.
[13]
J.J.M.M. Rutten. A coinductive calculus of streams. Math. Struct. in Comp. Science, (15): 93--147, 2005.
[14]
Neil J.A. Sloane. The on-line encyclopedia of integer sequences. http://www.research.att.com/ njas/sequences/.

Cited By

View all
  • (2024)Forward- or reverse-mode automatic differentiationScience of Computer Programming10.1016/j.scico.2023.103010231:COnline publication date: 1-Jan-2024
  • (2016)Contractive Functions on Infinite Data StructuresProceedings of the 28th Symposium on the Implementation and Application of Functional Programming Languages10.1145/3064899.3064900(1-13)Online publication date: 31-Aug-2016
  • (2015)Hardware synthesis from a recursive functional languageProceedings of the 10th International Conference on Hardware/Software Codesign and System Synthesis10.5555/2830840.2830850(83-93)Online publication date: 4-Oct-2015
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
ICFP '08: Proceedings of the 13th ACM SIGPLAN international conference on Functional programming
September 2008
422 pages
ISBN:9781595939197
DOI:10.1145/1411204
  • cover image ACM SIGPLAN Notices
    ACM SIGPLAN Notices  Volume 43, Issue 9
    ICFP '08
    September 2008
    399 pages
    ISSN:0362-1340
    EISSN:1558-1160
    DOI:10.1145/1411203
    Issue’s Table of Contents
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 ACM 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

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 20 September 2008

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. coinduction
  2. finite calculus
  3. generating functions
  4. recurrences
  5. streams
  6. unique fixed points

Qualifiers

  • Research-article

Conference

ICFP08
Sponsor:

Acceptance Rates

Overall Acceptance Rate 333 of 1,064 submissions, 31%

Upcoming Conference

ICFP '25
ACM SIGPLAN International Conference on Functional Programming
October 12 - 18, 2025
Singapore , Singapore

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)12
  • Downloads (Last 6 weeks)2
Reflects downloads up to 18 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2024)Forward- or reverse-mode automatic differentiationScience of Computer Programming10.1016/j.scico.2023.103010231:COnline publication date: 1-Jan-2024
  • (2016)Contractive Functions on Infinite Data StructuresProceedings of the 28th Symposium on the Implementation and Application of Functional Programming Languages10.1145/3064899.3064900(1-13)Online publication date: 31-Aug-2016
  • (2015)Hardware synthesis from a recursive functional languageProceedings of the 10th International Conference on Hardware/Software Codesign and System Synthesis10.5555/2830840.2830850(83-93)Online publication date: 4-Oct-2015
  • (2013)The Under-Performing UnfoldProceedings of the 25th symposium on Implementation and Application of Functional Languages10.1145/2620678.2620679(4321-4332)Online publication date: 28-Aug-2013
  • (2011)Scans and Convolutions— A Calculational Proof of Moessner’s TheoremImplementation and Application of Functional Languages10.1007/978-3-642-24452-0_1(1-24)Online publication date: 2011
  • (2010)Adjoint folds and unfoldsProceedings of the 10th international conference on Mathematics of program construction10.5555/1886619.1886634(195-228)Online publication date: 21-Jun-2010
  • (2010)Well-definedness of Streams by Transformation and TerminationLogical Methods in Computer Science10.2168/LMCS-6(3:21)20106:3Online publication date: 7-Sep-2010
  • (2010)Concrete stream calculusJournal of Functional Programming10.1017/S095679681000021320:5-6(463-535)Online publication date: 1-Nov-2010
  • (2010)Reasoning about CodataCentral European Functional Programming School10.1007/978-3-642-17685-2_3(42-93)Online publication date: 2010
  • (2010)Adjoint Folds and UnfoldsMathematics of Program Construction10.1007/978-3-642-13321-3_13(195-228)Online publication date: 2010
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media