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的主要创新在于提出了一种用于异步延迟的新模态，允许每个输出通道在运行时关联其所依赖的输入通道集合，从而使机器仅在必要时计算新输出。我们证明了一系列操作属性，包括因果性、生产性及无空间泄露。此外，我们还表明，尽管与输出通道关联的输入通道集合在执行过程中可能发生变化，但其上界可通过类型系统静态确定。