research-article

Higher-order functional reactive programming in bounded space

Authors:

Neelakantan R. Krishnaswami,

Jan HoffmannAuthors Info & Claims

ACM SIGPLAN Notices, Volume 47, Issue 1

Pages 45 - 58

https://doi.org/10.1145/2103621.2103665

Published: 25 January 2012 Publication History

Abstract

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 programs whose resource usage is excessive and hard to predict. In this paper, we address the problem of space leaks in discrete-time functional reactive programs. We present a functional reactive programming language that statically bounds the size of the dataflow graph a reactive program creates, while still permitting use of higher-order functions and higher-type streams such as streams of streams. We achieve this with a novel linear type theory that both controls allocation and ensures that all recursive definitions are well-founded.

We also give a denotational semantics for our language by combining recent work on metric spaces for the interpretation of higher-order causal functions with length-space models of space-bounded computation. The resulting category is doubly closed and hence forms a model of the logic of bunched implications.

Supplementary Material

JPG File (popl_1b_1.jpg)

Download
12.93 KB

MP4 File (popl_1b_1.mp4)

Download
192.45 MB

References

[1]

U. A. Acar, G. E. Blelloch, R. Ley-Wild, K. Tangwongsan, and D. Türkoglu. Traceable data types for self-adjusting computation. In PLDI, pages 483--496, 2010.

Digital Library

[2]

A. W. Appel, P.-A. Melliès, C. D. Richards, and J. Vouillon. A very modal model of a modern, major, general type system. In M. Hofmann and M. Felleisen, editors, POPL, pages 109--122. ACM, 2007. ISBN 1--59593--575--4.

Digital Library

[3]

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

Digital Library

[4]

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

Digital Library

[5]

G. Cooper. Integrating dataflow evaluation into a practical higher-order call-by-value language. PhD thesis, Brown University, 2008.

Digital Library

[6]

G. Cooper and S. Krishnamurthi. Embedding dynamic dataflow in a call-by-value language. Programming Languages and Systems, pages 294--308, 2006.

Digital Library

[7]

D. Dreyer, A. Ahmed, and L. Birkedal. Logical step-indexed logical relations. In LICS, pages 71--80. IEEE, 2009.

Digital Library

[8]

C. Elliott and P. Hudak. Functional reactive animation. In ICFP, 1997.

Digital Library

[9]

M. Hofmann. A type system for bounded space and functional in-place update. Nordic Journal of Computing, 7 (4), 2000.

Digital Library

[10]

M. Hofmann. Linear types and non-size-increasing polynomial time computation. Information and Computation, 183 (1), 2003.

Digital Library

[11]

P. Hudak, A. Courtney, H. Nilsson, and J. Peterson. Arrows, robots and functional reactive programming. In Advanced Functional Programming, volume 2638 of LNCS. Springer, 2003.

[12]

J. Hughes. Generalizing monads to arrows. Sci. Comput. Program., 37 (1--3), 2000.

Digital Library

[13]

N. Krishnaswami and N. Benton. Ultrametric semantics of reactive programs. In LICS. IEEE, 2011.

Digital Library

[14]

N. Krishnaswami and N. Benton. A semantic model of graphical user interfaces. In ICFP, 2011.

Digital Library

[15]

U. D. Lago and M. Hofmann. Realizability models and implicit complexity. Theor. Comput. Sci., 412 (20): 2029--2047, 2011.

Digital Library

[16]

R. Ley-Wild, U. A. Acar, and M. Fluet. A cost semantics for self-adjusting computation. In Z. Shao and B. C. Pierce, editors, POPL, pages 186--199. ACM, 2009. ISBN 978--1--60558--379--2.

Digital Library

[17]

H. Liu, E. Cheng, and P. Hudak. Causal commutative arrows and their optimization. In ICFP, 2009.

Digital Library

[18]

H. Nakano. A modality for recursion. In LICS, pages 255--266, 2000.

Digital Library

[19]

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

Digital Library

[20]

P. W. O'Hearn and D. J. Pym. The logic of bunched implications. Bulletin of Symbolic Logic, 5 (2), 1999.

[21]

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

[22]

N. Sculthorpe and H. Nilsson. Safe functional reactive programming through dependent types. In ICFP, 2009.

Digital Library

[23]

D. Spoonhower, G. E. Blelloch, R. Harper, and P. B. Gibbons. Space profiling for parallel functional programs. In J. Hook and P. Thiemann, editors, ICFP, pages 253--264. ACM, 2008. ISBN 978--1--59593--919--7.

Digital Library

[24]

T. Uustalu and V. Vene. The essence of dataflow programming. In K. Yi, editor, APLAS, volume 3780 of Lecture Notes in Computer Science, pages 2--18. Springer, 2005. ISBN 3--540--29735--9.

Digital Library

[25]

Z. Wan, W. Taha, and P. Hudak. Real-time FRP. In ICFP, pages 146--156, 2001.

Digital Library

[26]

Z. Wan, W. Taha, and P. Hudak. Event-driven FRP. In PADL, pages 155--172, 2002.

Digital Library

Cited By

Blaabjerg JAskarov A(2023)OblivIO: Securing Reactive Programs by Oblivious Execution with Bounded Traffic Overheads2023 IEEE 36th Computer Security Foundations Symposium (CSF)10.1109/CSF57540.2023.00014(292-307)Online publication date: Jul-2023
https://doi.org/10.1109/CSF57540.2023.00014
Yokoyama AMoriguchi SWatanabe T(2021)A Functional Reactive Programming Language for Small-Scale Embedded Systems with Recursive Data TypesJournal of Information Processing10.2197/ipsjjip.29.68529(685-706)Online publication date: 2021
https://doi.org/10.2197/ipsjjip.29.685
Cardoso DVizzotto JPiveta ECamarão CSulzmann M(2018)AsyncRFJProceedings of the XXII Brazilian Symposium on Programming Languages10.1145/3264637.3264642(35-42)Online publication date: 20-Sep-2018
https://dl.acm.org/doi/10.1145/3264637.3264642
Show More Cited By

Index Terms

Higher-order functional reactive programming in bounded space
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 without spacetime leaks
ICFP '13: Proceedings of the 18th ACM SIGPLAN international conference on Functional programming

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 ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 47, Issue 1

POPL '12

January 2012

569 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/2103621

Issue’s Table of Contents

POPL '12: Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2012
602 pages
ISBN:9781450310833
DOI:10.1145/2103656
General Chair:
John Field
Google, USA
,
Program Chair:
Michael Hicks
University of Maryland, College Park, USA

Copyright © 2012 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 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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 25 January 2012

Published in SIGPLAN Volume 47, Issue 1

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

39
Total Citations
View Citations
560
Total Downloads

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

Reflects downloads up to 17 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Blaabjerg JAskarov A(2023)OblivIO: Securing Reactive Programs by Oblivious Execution with Bounded Traffic Overheads2023 IEEE 36th Computer Security Foundations Symposium (CSF)10.1109/CSF57540.2023.00014(292-307)Online publication date: Jul-2023
https://doi.org/10.1109/CSF57540.2023.00014
Yokoyama AMoriguchi SWatanabe T(2021)A Functional Reactive Programming Language for Small-Scale Embedded Systems with Recursive Data TypesJournal of Information Processing10.2197/ipsjjip.29.68529(685-706)Online publication date: 2021
https://doi.org/10.2197/ipsjjip.29.685
Cardoso DVizzotto JPiveta ECamarão CSulzmann M(2018)AsyncRFJProceedings of the XXII Brazilian Symposium on Programming Languages10.1145/3264637.3264642(35-42)Online publication date: 20-Sep-2018
https://dl.acm.org/doi/10.1145/3264637.3264642
Severi PPadovani LTuosto EDezani-Ciancaglini M(2016)On Sessions and Infinite DataCoordination Models and Languages10.1007/978-3-319-39519-7_15(245-261)Online publication date: 24-May-2016
https://doi.org/10.1007/978-3-319-39519-7_15
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
Accattoli BDal Lago UVanoni G(2022)Reasonable Space for the λ-Calculus, LogarithmicallyProceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3531130.3533362(1-13)Online publication date: 2-Aug-2022
https://dl.acm.org/doi/10.1145/3531130.3533362
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
Accattoli BDal Lago UVanoni G(2021)The (In)Efficiency of interactionProceedings of the ACM on Programming Languages10.1145/34343325:POPL(1-33)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434332
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
Bahr PGraulund CMøgelberg R(2019)Simply RaTT: a fitch-style modal calculus for reactive programming without space leaksProceedings of the ACM on Programming Languages10.1145/33417133:ICFP(1-27)Online publication date: 26-Jul-2019
https://dl.acm.org/doi/10.1145/3341713
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 Issue’s Table of Contents