Modal FRP for all: Functional reactive programming without space leaks in Haskell

Functional reactive programming (FRP) provides a high-level
interface for implementing reactive systems in a declarative
manner. However, this high-level interface has to be carefully
reined in to ensure that programs can in fact be executed in
practice. Specifically, one must ensure that FRP programs are
productive, causal, and can be implemented without introducing space
leaks. In recent years, modal types have been demonstrated to be an
effective tool to ensure these operational properties.

In this paper, we present Rattus, a modal FRP language that extends
and simplifies previous modal FRP calculi while still maintaining
the operational guarantees for productivity, causality, and space
leaks. The simplified type system makes Rattus a practical
programming language that can be integrated with existing functional
programming languages. To demonstrate this, we have implemented a
shallow embedding of Rattus in Haskell that allows the programmer
to write Rattus code in familiar Haskell syntax and seamlessly
integrate it with regular Haskell code. Thus Rattus combines the
benefits enjoyed by FRP libraries such as Yampa, namely access to a
rich library ecosystem (e.g. for graphics programming), with the
strong operational guarantees offered by a bespoke type system.

To establish the productivity, causality, and memory properties of
the language, we prove type soundness using a logical relations
argument fully mechanised in the Coq proof assistant.