Safe functional reactive programming through dependent types

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Safe functional reactive programming through dependent types

Full text

Pdf (425 KB)

Source

International Conference on Functional Programming archive
Proceedings of the 14th ACM SIGPLAN international conference on Functional programming table of contents

Edinburgh, Scotland

SESSION: Session 2 table of contents

Pages 23-34

Year of Publication: 2009

ISBN:978-1-60558-332-7

Also published in ...

Authors

Neil Sculthorpe	University of Nottingham, Nottingham, United Kingdom
Henrik Nilsson	University of Nottingham, Nottingham, United Kingdom

Sponsors

ACM: Association for Computing Machinery
SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 35, Downloads (12 Months): 197, Citation Count: 0

Additional Information:

abstract references index terms

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1596550.1596558 What is a DOI?

ABSTRACT

Functional Reactive Programming (FRP) is an approach to reactive programming where systems are structured as networks of functions operating on signals. FRP is based on the synchronous data-flow paradigm and supports both continuous-time and discrete-time signals (hybrid systems). What sets FRP apart from most other languages for similar applications is its support for systems with dynamic structure and for higher-order reactive constructs.

Statically guaranteeing correctness properties of programs is an attractive proposition. This is true in particular for typical application domains for reactive programming such as embedded systems. To that end, many existing reactive languages have type systems or other static checks that guarantee domain-specific properties, such as feedback loops always being well-formed. However, they are limited in their capabilities to support dynamism and higher-order data-flow compared with FRP. Thus, the onus of ensuring such properties of FRP programs has so far been on the programmer as established static techniques do not suffice.

In this paper, we show how dependent types allow this concern to be addressed. We present an implementation of FRP embedded in the dependently-typed language Agda, leveraging the type system of the host language to craft a domain-specific (dependent) type system for FRP. The implementation constitutes a discrete, operational semantics of FRP, and as it passes the Agda type, coverage, and termination checks, we know the operational semantics is total, which means our type system is safe.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Albert Benveniste, Paul Caspi, Stephen Edwards, Nicolas Halbwachs, Paul Le Guernic, and Robert de Simone. The synchronous languages twelve years later. Proceedings of the IEEE, Special issue on embedded systems, 91(1):64--83, 2003.
	2	Gerard Berry and Georges Gonthier. The Esterel synchronous programming language: Design, semantics, implementation. Science of Computer Programming, 19(2):87--152, 1992.
	3	Paul Caspi and Marc Pouzet. Synchronous Kahn networks. In International Conference on Functional Programming (ICFP '96), pages 226--238. ACM, 1996.
	4	Mun Hon Cheong. Functional programming and 3D games. BEng thesis, University of New South Wales, Sydney, Australia, 2005.
	5	Jean-Louis Colaco, Alain Girault, Gregoire Hamon, and Marc Pouzet. Towards a higher-order synchronous data-flow language. In Embedded Software (EMSOFT '04), pages 230--239. ACM, 2004.
	6	Gregory H. Cooper and Shriram Krishnamurthi. Embedding dynamic dataflow in a call-by-value language. In European Symposium on Programming (ESOP '06), pages 294--308. Springer-Verlag, 2006.
	7	Antony Courtney and Conal Elliott. Genuinely functional user interfaces. In Haskell Workshop (Haskell '01), pages 41--69. Elsevier, 2001.
	8	Antony Courtney, Henrik Nilsson, and John Peterson. The Yampa arcade. In Haskell Workshop (Haskell '03), pages 7--18. ACM, 2003.
	9	Conal Elliott. Simply efficient functional reactivity. http://conal.net/papers/simply-reactive/, 2008.
	10	Conal Elliott and Paul Hudak. Functional reactive animation. In International Conference on Functional Programming (ICFP '97), pages 263--273. ACM, 1997.
	11	George Giorgidze and Henrik Nilsson. Embedding a functional hybrid modelling language in Haskell. In Implementation and Application of Functional Languages (IFL '08), 2008a. To appear.
	12	George Giorgidze and Henrik Nilsson. Switched-on Yampa: Declarative programming of modular synthesizers. In Practical Aspects of Declarative Languages (PADL '08), pages 282--298. Springer-Verlag, 2008b.
	13	Nicolas Halbwachs. Synchronous Programming of Reactive Systems. The Springer International Series in Engineering and Computer Science. Springer-Verlag, 1993.
	14	Nicolas Halbwachs. Synchronous programming of reactive systems, a tutorial and commented bibliography. In Computer Aided Verification (CAV '98), pages 1--16. Springer-Verlag, 1998.
	15	Nicolas Halbwachs, Paul Caspi, Pascal Raymond, and Daniel Pilaud. The synchronous data-flow programming language Lustre. Proceedings of the IEEE, 79(9):1305--1320, 1991.
	16	Thomas A. Henzinger. The theory of hybrid automata. In Logics in Computer Science (LICS '96), pages 278--292. IEEE Computer Society, 1996.
	17	John Hughes. Generalising monads to arrows. Science of Computer Programming, 37(1--3):67--111, 2000.
	18	Sam Lindley, Philip Wadler, and Jeremy Yallop. The arrow calculus. Technical report, University of Edinburgh, School of Informatics, 2008.
	19	Geoffrey Mainland, Greg Morrisett, and Matt Welsh. Flask: Staged functional programming for sensor networks. In International Conference on Functional Programming (ICFP '08), pages 335--345. ACM, 2008.
	20	Henrik Nilsson, Antony Courtney, and John Peterson. Functional reactive programming, continued. In Haskell Workshop (Haskell '02), pages 51--64. ACM, 2002.
	21	Ulf Norell. Towards a Practical Programming Language Based on Dependent Type Theory. PhD thesis, Chalmers University of Technology, 2007.
	22	Andre Pang, Don Stewart, Sean Seefried, and Manuel M. T. Chakravarty. Plugging Haskell in. In Haskell Workshop (Haskell '04), pages 10--21. ACM, 2004.
	23	Ross Paterson. A new notation for arrows. In International Conference on Functional Programming (ICFP '01), pages 229--240. ACM, 2001.
	24	John Peterson, Paul Hudak, and Conal Elliott. Lambda in motion: Controlling robots with Haskell. In Practical Aspects of Declarative Languages (PADL '99), pages 91--105. Springer-Verlag, 1999.
	25	Benjamin C. Pierce. Types and Programming Languages. MIT Press, 2002.
	26	Marc Pouzet. Lucid Synchrone, version 3.0: Tutorial and reference manual. Universite Paris-Sud, LRI, 2006. http://www.lri.fr/pouzet/lucid-synchrone.
	27	Neil Sculthorpe and Henrik Nilsson. Optimisation of dynamic, hybrid signal function networks. In Trends in Functional Programming (TFP '08), pages 97--112. Intellect, 2008.
	28	Simulink. Using Simulink, Version 7.3. 3 Apple Hill Drive, Natick, MA, 2009. http://www.mathworks.com.
	29	Simon Thompson. Type Theory and Functional Programming. Addison-Wesley, 1991.
	30	Zhanyong Wan and Paul Hudak. Functional reactive programming from first principles. In Programming Language Design and Implementation (PLDI '00), pages 242--252. ACM, 2000.
	31	Zhanyong Wan, Walid Taha, and Paul Hudak. Real-time FRP. In International Conference on Functional Programming (ICFP '01), pages 146--156. ACM, 2001.