Simply RaTT: A Fitch-style Modal Calculus for Reactive Programming without Space Leaks

TL;DR

Simply RaTT introduces a Fitch-style modal calculus for reactive programming that ensures causality and prevents space and time leaks, simplifying type systems and improving program safety.

Contribution

It presents a novel Fitch-style modal calculus for FRP that simplifies type systems and guarantees causality without space or time leaks.

Findings

Operational semantics prevent space leaks in Simply RaTT.

Type system eliminates time leaks caused by fixed point unfolding.

Simplified type system leads to more concise reactive programs.

Abstract

Functional reactive programming (FRP) is a paradigm for programming with signals and events, allowing the user to describe reactive programs on a high level of abstraction. For this to make sense, an FRP language must ensure that all programs are causal, and can be implemented without introducing space leaks and time leaks. To this end, some FRP languages do not give direct access to signals, but just to signal functions. Recently, modal types have been suggested as an alternative approach to ensuring causality in FRP languages in the synchronous case, giving direct access to the signal and event abstractions. This paper presents Simply RaTT, a new modal calculus for reactive programming. Unlike prior calculi, Simply RaTT uses a Fitch-style approach to modal types, which simplifies the type system and makes programs more concise. Echoing a previous result by Krishnaswami for a different language, we devise an operational semantics that safely executes Simply RaTT programs without space leaks. We also identify a source of time leaks present in other modal FRP languages: The unfolding of fixed points in delayed computations. These time leaks are eliminated by the Simply RaTT type system.