Simple Modal Types for Functional Reactive Programming

Abstract

Functional reactive programming (FRP) is a declarative programming paradigm for implementing reactive programs at a high level of abstraction. It applies functional programming principles to construct and manipulate time-varying values, also known as signals. However, for this programming paradigm to work in practice, an FRP language must ensure that programs are causal, productive, and free of space leaks. Over the past fifteen years, several modal type systems to enforce these operational properties have been developed.

We present a new FRP language with a significantly simplified modal type system that imposes fewer restrictions than previous modal FRP languages while still guaranteeing the central operational properties of causality, productivity, and absence of space leaks. The key enabling idea is to define the language's semantics so that it is impossible to inspect a signal's past. In particular, a signal only stores its current value and how to compute its future values, but it cannot retain its past values. As a result, we obtain a language with a simpler modal type system that is also more expressive and supports a more modular programming style compared to previous modal FRP calculi without space leaks. While the central idea applies to both synchronous and asynchronous FRP, we focus here on the more challenging asynchronous case.

Keywords: Functional Reactive Programming, Modal Types, Type Systems