Over the past decade, a number of languages for functional reactive programming (FRP) have been suggested, which use modal types to ensure properties like causality, productivity and lack of space leaks. So far, almost all of these languages have included a modal operator for delay on a global clock. For some applications, however, the notion of global clock is unnatural and leads to leaky abstractions as well as inefficient implementations. While modal languages without a global clock have been proposed, no operational properties have been proved about them, yet. This paper proposes Async RaTT, a new modal language for asynchronous FRP, equipped with an operational semantics mapping complete programs to machines that take asynchronous input signals and produce output signals. The main novelty of Async RaTT is a new modality for asynchronous delay, allowing each output channel to be associated 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, although the set of input channels associated with an output channel can change during execution, upper bounds on these can be determined statically by the type system.

翻译：在过去的十年中，人们提出了多种函数响应式编程（FRP）语言，这些语言利用模态类型来确保因果关系、生产性和无空间泄漏等属性。迄今为止，几乎所有此类语言都包含一个用于全局时钟延迟的模态算子。然而，对于某些应用而言，全局时钟的概念并不自然，会导致抽象泄漏和低效的实现。尽管已提出无全局时钟的模态语言，但尚未证明其操作性质。本文提出了Async RaTT，一种用于异步FRP的新型模态语言，配备了将完整程序映射为机器的操作语义，这些机器接收异步输入信号并产生输出信号。Async RaTT的主要创新之处在于一种用于异步延迟的新模态，允许每个输出通道在运行时与它所依赖的输入通道集相关联，从而仅当必要时才让机器计算新的输出。我们证明了一系列操作性质，包括因果关系、生产性和无空间泄漏。我们还表明，尽管与输出通道关联的输入通道集可在执行过程中变化，但类型系统可静态确定这些集合的上界。