Simple Modal Types for Functional Reactive Programming

TL;DR

This paper introduces a simplified modal type system for functional reactive programming that enhances expressiveness and efficiency while ensuring causality, productivity, and no space leaks through controlled mutability of signals.

Contribution

It presents a new FRP language with a less restrictive modal type system and altered semantics for signals, improving expressiveness and enabling efficient in-place updates.

Findings

More programs can type-check due to relaxed restrictions.

Signals modeled as mutable references with controlled mutability.

Maintains causality, productivity, and space leak freedom.

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 alter the semantics of signals so that the type system can safely allow more programs to type-check, thereby making the language more expressive, too. With this new semantics, signals are modelled as mutable references whose mutability is tightly controlled by the 'later' type modality. This disciplined form of mutability also enables more efficient in-place updates of signals, all while preserving a functional programming style.