Safe functional reactive programming through dependent types

Sculthorpe, N ORCID: https://orcid.org/0000-0002-7244-0916 and Nilsson, H, 2009. Safe functional reactive programming through dependent types. ACM SIGPLAN Notices, 44 (9), pp. 23-34. ISSN 0362-1340

Preview

Text PS29355_Sculthorpe.pdf - Post-print Download (197kB) | Preview

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

Item Type:	Journal article
Publication Title:	ACM SIGPLAN Notices
Creators:	Sculthorpe, N. and Nilsson, H.
Publisher:	ACM
Date:	2009
Volume:	44
Number:	9
ISSN:	0362-1340
Identifiers:	Number Type 10.1145/1631687.1596558 DOI
Divisions:	Schools > School of Science and Technology
Record created by:	Richard Cross
Date Added:	13 Dec 2016 14:21
Last Modified:	09 Jun 2017 14:09
URI:	https://irep.ntu.ac.uk/id/eprint/29355

Actions (login required)

Edit View

Statistics

Views

Downloads