依赖类型化的R向量、数组和矩阵
摘要：在大规模数据分析中，R编程语言被广泛使用。它内置了丰富的支持向量、数组和矩阵处理的功能。这些操作在构建R的应用程序中具有重要地位，因此了解它们的行为很重要。而且，为了方便程序员，R中的这些操作与数学中对应的操作有所不同，这给规范和静态验证带来了一些挑战。 我们报道了在R语言中对这方面进行静态类型化的进展。在这种情况下，类型的有趣之处是警告程序员违反边界限制，因此类型必然是相关的。我们解释了R如何扩展标准的数学行为。然后我们展示了如何在LiquidHaskell中指定R的行为，LiquidHaskell是一种依赖类型的Haskell扩展。在一般情况下，实际验证库和客户端代码目前超出了LiquidHaskell的能力范围；因此，这项工作对于R的类型化和依赖类型编程语言的进展都提供了挑战和机会。
作者：John Wrenn, Anjali Pal, Alexa VanHattum, Shriram Krishnamurthi
论文ID：2304.04265
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-04-11