The R programming language is widely used in large-scale data analyses. It contains especially rich built-in support for dealing with vectors, arrays, and matrices. These operations feature prominently in the applications that form R's raison d'\^etre, making their behavior worth understanding. Furthermore, ostensibly for programmer convenience, their behavior in R is a notable extension over the corresponding operations in mathematics, thereby offering some challenges for specification and static verification. We report on progress towards statically typing this aspect of the R language. The interesting aspects of typing, in this case, warn programmers about violating bounds, so the types must necessarily be dependent. We explain the ways in which R extends standard mathematical behavior. We then show how R's behavior can be specified in LiquidHaskell, a dependently-typed extension to Haskell. In the general case, actually verifying library and client code is currently beyond LiquidHaskell's reach; therefore, this work provides challenges and opportunities both for typing R and for progress in dependently-typed programming languages.

翻译：R编程语言广泛应用于大规模数据分析，其内置的向量、数组和矩阵操作极为丰富。这些操作在构成R语言存在意义的应用中占据核心地位，因此理解其行为具有重要价值。此外，R语言为了程序员便利，对相应数学运算进行了显著扩展，这为规范描述和静态验证带来了挑战。本文报告了在R语言这一特性的静态类型化方面取得的进展。在此场景下，类型化的关键在于警告程序员避免越界操作，因此类型必须具有依赖性。我们阐释了R语言扩展标准数学行为的方式，并展示了如何用依赖类型化的Haskell扩展LiquidHaskell来描述R语言的行为。在一般情况下，实际验证库代码和客户端代码目前仍超出LiquidHaskell的能力范围；因此，本工作为R语言类型化以及依赖类型编程语言的发展同时带来了挑战与机遇。