Simple Modal Types for Functional Reactive Programming
Patrick Bahr
cs.PL
Dec 10, 2025 · v3
TL;DR
The metatheory of the Rizzo FRP language, covering causality, productivity and absence of space leaks, plus all examples is fully formalised in Lean, with a public repository.
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.
Problem
Functional reactive programming languages must guarantee causality, productivity, and absence of space leaks. Existing modal type systems that enforce these properties are complex and restrictive.
Approach
The authors introduce Rizzo, an asynchronous FRP language whose semantics make it impossible to inspect a signal's past: a signal stores only its current value and how to compute future values. This allows a simpler modal type system. The metatheoretical proofs and all examples are formalised in Lean.
Results
Rizzo's type system is simpler and more expressive than previous space-leak-free modal FRP calculi and supports a more modular programming style. It still guarantees causality, productivity and absence of space leaks, and these results are machine-checked in Lean.