research-article

Higher-order functional reactive programming without spacetime leaks

Author:

Neelakantan R. KrishnaswamiAuthors Info & Claims

ICFP '13: Proceedings of the 18th ACM SIGPLAN international conference on Functional programming

Pages 221 - 232

https://doi.org/10.1145/2500365.2500588

Published: 25 September 2013 Publication History

Abstract

Functional reactive programming (FRP) is an elegant approach to declaratively specify reactive systems. However, the powerful abstractions of FRP have historically made it difficult to predict and control the resource usage of programs written in this style.

In this paper, we give a new language for higher-order reactive programming. Our language generalizes and simplifies prior type systems for reactive programming, by supporting the use of streams of streams, first-class functions, and higher-order operations. We also support many temporal operations beyond streams, such as terminatable streams, events, and even resumptions with first-class schedulers. Furthermore, our language supports an efficient implementation strategy permitting us to eagerly deallocate old values and statically rule out spacetime leaks, a notorious source of inefficiency in reactive programs. Furthermore, these memory guarantees are achieved without the use of a complex substructural type discipline.

We also show that our implementation strategy of eager deallocation is safe, by showing the soundness of our type system with a novel step-indexed Kripke logical relation.

References

[1]

U. A. Acar. Self-Adjusting Computation. PhD thesis, Carnegie Mellon University, 2005.

Digital Library

[2]

A. Ahmed, D. Dreyer, and A. Rossberg. State-dependent representation independence. In Principles of Programming Languages (POPL), pages 340--353, 2009.

Digital Library

[3]

A. Appel and D. McAllester. An indexed model of recursive types for foundational proof-carrying code. ACM Transactions on Programming Languages and Systems (TOPLAS), 23 (5): 657--683, 2001.

Digital Library

[4]

H. Baker and C. Hewitt. The incremental garbage collection of processes. In Symposium on Artificial Intelligence Programming Languages, August 1977.

Digital Library

[5]

G. Berry and L. Cosserat. The ESTEREL synchronous programming language and its mathematical semantics. In Seminar on Concurrency, pages 389--448. Springer, 1985.

[6]

P. Caspi and M. Pouzet. Synchronous Kahn networks. In Proceedings of the first ACM SIGPLAN international conference on Functional programming, ICFP '96, pages 226--238, New York, NY, USA, 1996. ACM. ISBN 0-89791-770-7. 10.1145/232627.232651.

Digital Library

[7]

P. Caspi, D. Pilaud, N. Halbwachs, and J. Plaice. LUSTRE: A declarative language for real-time programming. In Principles of Programming Languages (POPL), 1987.

Digital Library

[8]

A. Cave, F. Ferreira, P. Panangaden, and B. Pientka. Fair reactive programming. Technical report, McGill University, 2013.

[9]

G. H. Cooper. Integrating Dataflow Evaluation into a Practical Higher-Order Call-by-Value Language. PhD thesis, Brown University, 2008.

Digital Library

[10]

G. H. Cooper and S. Krishnamurthi. Embedding dynamic dataflow in a call-by-value language. In European Symposium on Programming (ESOP), pages 294--308, 2006.

Digital Library

[11]

H. B. Curry. The Paradox of Kleene and Rosser. Transactions of the American Mathematical Society, 50 (3): 454--516, Nov. 1941.

[12]

J. Donham. Froc: a library for functional reactive programming in OCaml.texttthttp://jaked.github.com/froc/, 2010.

[13]

D. Dreyer, G. Neis, and L. Birkedal. The impact of higher-order state and control effects on local relational reasoning. In International Conference on Functional Programming (ICFP), pages 143--156, 2010.

Digital Library

[14]

C. Elliott. Push-pull functional reactive programming. In Haskell Symposium, 2009. URL http://conal.net/papers/push-pull-frp.

Digital Library

[15]

C. Elliott and P. Hudak. Functional reactive animation. In International Conference on Functional Programming (ICFP), 1997.

Digital Library

[16]

D. Friedman and D. Wise. The impact of applicative programming on multiprocessing. In International Conference on Parallel Processing, pages 263--272, 1976.

[17]

M. J. Gabbay and A. M. Pitts. A new approach to abstract syntax with variable binding. Formal Aspects of Computing, 13: 341--363, 2001.

Digital Library

[18]

M. Hofmann. Linear types and non-size-increasing polynomial time computation. In Logic in Computer Science (LICS), 1999.

Digital Library

[19]

A. Jeffrey. LTL types FRP: linear-time temporal logic propositions as types, proofs as functional reactive programs. In Programming Languages Meets Program Verification (PLPV), pages 49--60, 2012.

Digital Library

[20]

A. Jeffrey. Causality for free!: parametricity implies causality for functional reactive programs. In Programming Languages Meets Program Verification (PLPV), pages 57--68, 2013.

Digital Library

[21]

W. Jeltsch. Signals, not generators! Trends in Functional Programming, 10: 145--160, 2009.

[22]

W. Jeltsch. Towards a common categorical semantics for linear-time temporal logic and functional reactive programming. Electronic Notes in Theoretical Computer Science, 286: 229--242, Sept. 2012.

Digital Library

[23]

W. Jeltsch. Temporal logic with "until", functional reactive programming with processes, and concrete process categories. In Programming Languages Meets Program Verification (PLPV), pages 69--78, 2013.

Digital Library

[24]

D. Kozen. Results on the propositional μ-calculus. Theoretical Computer Science, 27 (3): 333 -- 354, 1983.

[25]

N. R. Krishnaswami. Proofs for higher-order reactive programming without spacetime leaks (supplementary material). Technical report, Max Planck Institute for Software Systems (MPI-SWS), 2013.

[26]

N. R. Krishnaswami and N. Benton. A semantic model for graphical user interfaces. In International Conference on Functional programming (ICFP), pages 45--57, 2011.

Digital Library

[27]

N. R. Krishnaswami and N. Benton. Ultrametric semantics of reactive programs. In Logic in Computer Science (LICS), pages 257--266, 2011.

Digital Library

[28]

N. R. Krishnaswami, N. Benton, and J. Hoffmann. Higher-order functional reactive programming in bounded space. In Principles of Programming Languages (POPL), pages 45--58, 2012.

Digital Library

[29]

B. S. Lerner, M. J. Carroll, D. P. Kimmel, H. Q.-D. La Vallee, and S. Krishnamurthi. Modeling and reasoning about DOM events. In Conference on Web Application Development (WebApps), 2012.

Digital Library

[30]

H. Liu, E. Cheng, and P. Hudak. Causal commutative arrows and their optimization. In International Conference on Functional Programming (ICFP), 2009.

Digital Library

[31]

I. Maier and M. Odersky. Deprecating the Observer Pattern with Scala.React. Technical report, EPFL, 2012.

[32]

M. Miller. Robust composition: Towards a unified approach to access control and concurrency control. PhD thesis, Johns Hopkins University, 2006.

Digital Library

[33]

T. Murphy VII., K. Crary, and R. Harper. Type-safe distributed programming with ML5. In Conference on Trustworthy Global Computing (TGC), pages 108--123, 2008.

Digital Library

[34]

H. Nakano. A modality for recursion. In Logic in Computer Science (LICS), pages 255--266, 2000.

Digital Library

[35]

H. Nilsson, A. Courtney, and J. Peterson. Functional reactive programming, continued. In ACM Haskell Workshop, page 64, 2002.

Digital Library

[36]

A. Pitts and I. Stark. Operational reasoning for functions with local state. Higher Order Operational Techniques in Semantics, 1998.

Digital Library

[37]

G. D. Plotkin. A powerdomain construction. SIAM Journal of Computation, 5 (3): 452--487, 1976.

Digital Library

[38]

A. Pnueli. The temporal logic of programs. In Foundations of Computer Science (FOCS), pages 46--57, 1977.

Digital Library

[39]

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

[40]

N. Sculthorpe and H. Nilsson. Safe functional reactive programming through dependent types. In International Conference on Functional Programming (ICFP), 2009.

Digital Library

[41]

N. Sculthorpe and H. Nilsson. Keeping calm in the face of change. Higher Order Symbolic Computation, 23 (2): 227--271, June 2010.

Digital Library

[42]

P. Wadler, W. Taha, and D. MacQueen. How to add laziness to a strict language, without even being odd. In Workshop on Standard ML, 1998.

[43]

Z. Wan, W. Taha, and P. Hudak. Event-driven FRP. In Practical Applications of Declarative Languages (PADL), pages 155--172, 2002.

Digital Library

Cited By

Cutler JWatson CNkurumeh EHilliard PGoldstein HStanford CPierce B(2024)Stream TypesProceedings of the ACM on Programming Languages10.1145/36564348:PLDI(1412-1436)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656434
Perez IMilano MLeo J(2023)The Beauty and Elegance of Functional Reactive AnimationProceedings of the 11th ACM SIGPLAN International Workshop on Functional Art, Music, Modelling, and Design10.1145/3609023.3609806(8-20)Online publication date: 30-Aug-2023
https://dl.acm.org/doi/10.1145/3609023.3609806
Bahr PMøgelberg R(2023)Asynchronous Modal FRPProceedings of the ACM on Programming Languages10.1145/36078477:ICFP(476-510)Online publication date: 31-Aug-2023
https://dl.acm.org/doi/10.1145/3607847
Show More Cited By

Index Terms

Higher-order functional reactive programming without spacetime leaks
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language types
        Data flow languages

Recommendations

Higher-order functional reactive programming without spacetime leaks
ICFP '13

Functional reactive programming (FRP) is an elegant approach to declaratively specify reactive systems. However, the powerful abstractions of FRP have historically made it difficult to predict and control the resource usage of programs written in this ...
Higher-order functional reactive programming in bounded space
POPL '12: Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Functional reactive programming (FRP) is an elegant and successful approach to programming reactive systems declaratively. The high levels of abstraction and expressivity that make FRP attractive as a programming model do, however, often lead to ...
Higher-order functional reactive programming in bounded space
POPL '12

Functional reactive programming (FRP) is an elegant and successful approach to programming reactive systems declaratively. The high levels of abstraction and expressivity that make FRP attractive as a programming model do, however, often lead to ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

ICFP '13: Proceedings of the 18th ACM SIGPLAN international conference on Functional programming

September 2013

484 pages

ISBN:9781450323260

DOI:10.1145/2500365

General Chair:
Greg Morrisett
Harvard University, USA
,
Program Chair:
Tarmo Uustalu
Institute of Cybernetics at TUT, Estonia

ACM SIGPLAN Notices Volume 48, Issue 9
ICFP '13
September 2013
457 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2544174
Editor:
Mark W. Bailey
Hamilton College, Clinton, NY
Issue’s Table of Contents

Copyright © 2013 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

SIGPLAN: ACM Special Interest Group on Programming Languages
Northeastern University

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 25 September 2013

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ICFP'13

Sponsor:

SIGPLAN

ICFP'13: ACM SIGPLAN International Conference on Functional Programming

September 25 - 27, 2013

Massachusetts, Boston, USA

Acceptance Rates

ICFP '13 Paper Acceptance Rate 40 of 133 submissions, 30%;

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

Upcoming Conference

ICFP '25

Sponsor:
sigplan

ACM SIGPLAN International Conference on Functional Programming

October 12 - 18, 2025

Singapore , Singapore

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

42
Total Citations
View Citations
446
Total Downloads

Downloads (Last 12 months)28
Downloads (Last 6 weeks)3

Reflects downloads up to 25 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Cutler JWatson CNkurumeh EHilliard PGoldstein HStanford CPierce B(2024)Stream TypesProceedings of the ACM on Programming Languages10.1145/36564348:PLDI(1412-1436)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656434
Perez IMilano MLeo J(2023)The Beauty and Elegance of Functional Reactive AnimationProceedings of the 11th ACM SIGPLAN International Workshop on Functional Art, Music, Modelling, and Design10.1145/3609023.3609806(8-20)Online publication date: 30-Aug-2023
https://dl.acm.org/doi/10.1145/3609023.3609806
Bahr PMøgelberg R(2023)Asynchronous Modal FRPProceedings of the ACM on Programming Languages10.1145/36078477:ICFP(476-510)Online publication date: 31-Aug-2023
https://dl.acm.org/doi/10.1145/3607847
Ahman D(2023)When Programs Have to Watch Paint DryFoundations of Software Science and Computation Structures10.1007/978-3-031-30829-1_1(1-23)Online publication date: 21-Apr-2023
https://doi.org/10.1007/978-3-031-30829-1_1
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
Gallego Arias EJouvelot PRibstein SDesblancs DWinograd-Cort DGiavitto J(2021)The w-calculus: a synchronous framework for the verified modelling of digital signal processing algorithmsProceedings of the 9th ACM SIGPLAN International Workshop on Functional Art, Music, Modelling, and Design10.1145/3471872.3472970(35-46)Online publication date: 27-Aug-2021
https://dl.acm.org/doi/10.1145/3471872.3472970
Ahman DPretnar M(2021)Asynchronous effectsProceedings of the ACM on Programming Languages10.1145/34343055:POPL(1-28)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434305
Spies SKrishnaswami NDreyer D(2021)Transfinite step-indexing for terminationProceedings of the ACM on Programming Languages10.1145/34342945:POPL(1-29)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434294
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
Graulund CSzamozvancev DKrishnaswami N(2021)Adjoint Reactive GUI ProgrammingFoundations of Software Science and Computation Structures10.1007/978-3-030-71995-1_15(289-309)Online publication date: 27-Mar-2021
https://dl.acm.org/doi/10.1007/978-3-030-71995-1_15
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.

Media

Figures

Other

Tables

View Table of Contents