Vega is a popular declarative language for creating interactive data visualizations. It supports reactive data transformations using its streaming dataflow architecture. Despite its widespread adoption, the exact semantics of Vega is subtle and poorly documented. This leads to incorrect or confusing visualizations and difficult-to-understand error messages. This paper makes two contributions. First, we define a graph-based operational semantics, providing a precise model of the streaming dataflow architecture of Vega. Second, we present a type system for the core data transformation language of Vega, which can prevent a range of common errors. We show that our type system is sound with respect to the semantics. While the dataflow architecture of Vega closely resembles well-studied models such as functional reactive programming and adaptive computation, there are important differences. The novelty of our work lies in making these precise and providing static analysis for such a reactive data visualization language. The result is a checker for Vega that can catch common real-world errors.

翻译：Vega是一种用于创建交互式数据可视化的流行声明式语言。它基于流式数据流架构支持响应式数据变换。尽管被广泛采用，但Vega的确切语义既微妙又缺乏充分文档，这导致可视化结果错误或令人困惑，以及难以理解的错误信息。本文做出两项贡献：首先，我们定义了一种基于图的操作语义，为Vega的流式数据流架构提供了精确模型；其次，我们为Vega的核心数据变换语言提出了一个类型系统，能够预防一系列常见错误。我们证明了该类型系统在语义上是可靠的。尽管Vega的数据流架构与函数式响应式编程和自适应计算等经过充分研究的模型高度相似，但仍存在重要差异。我们工作的新颖之处在于使这些差异精确化，并为这种响应式数据可视化语言提供了静态分析手段。最终成果是一个能够捕获常见现实错误的Vega检查器。