Asynchronous modal FRP: Ticking all the boxes

Over the past fifteen years, several languages for functionalreactive programming (FRP) have been suggested that use modaltypes to ensure properties like causality, productivity, and lack ofspace leaks. So far, almost all of these languages have included amodal operator for delay on a global clock. For some applications,however, a global clock is unnatural and leads to leakyabstractions as well as inefficient implementations. While modallanguages without a global clock have been proposed, no operationalproperties have been proved about them yet.This paper proposes Async RaTT, a new modal language for asynchronousFRP, equipped with an operational semantics mapping completeprograms to machines that take asynchronous input signals andproduce output signals. The main novelty of Async RaTT is a new modalityfor asynchronous delay, allowing each output channel to beassociated at runtime with the set of input channels it depends on,thus causing the machine to only compute new output when necessary.We prove a series of operational properties including causality,productivity, and lack of space leaks. We also show that, althoughthe set of input channels associated with an output channel canchange dynamically during execution, upper bounds on these can bedetermined statically by the type system.