Type-level computations for Ruby libraries
Type-level computations for Ruby libraries
复制标题
Ruby 库的类型级计算
DOI：
10.1145/3314221.3314630
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Van Horn, David
中科院分区：
文献类型：
--
作者：
Kazerounian, Milod;Guria, Sankha Narayan;Vazou, Niki;Foster, Jeffrey S.;Van Horn, David
许多研究人员探索了将静态类型引入动态语言的方法。然而，到目前为止，当类型依赖于值时，这样的系统还不够精确，这通常是在使用某些Ruby库时出现的。例如，Ruby on rails中数据库查询的类型安全性取决于查询中使用的表名和列名。为了解决这个问题，我们引入了CompRDL，这是一个用于Ruby的类型系统，它允许库方法类型签名包含类型级别的计算(简称为comp类型)。与表名和列名的单例类型相结合，comp类型允许我们提供数据库查询方法的类型签名，这些签名计算表的模式以生成非常精确的类型信息。哈希库、数组库和字符串库的Comp类型还可以提高精度，从而减少类型强制转换的需要。我们形式化地描述了CompRDL，并证明了它的类型系统的可靠性。CompRDL插入运行时检查以确保库方法遵守它们的计算类型，而不是使用Comp类型检查库方法的主体--这些方法可能包括本机代码或很复杂。我们通过为几个Ruby核心库和数据库查询API编写带有类型级计算的注释来评估CompRDL。然后，我们使用这些注释来输入check两个流行的Ruby库和四个Ruby on rails Web应用程序。我们发现注释相对紧凑，可以在我们的主题程序中成功地对132个方法进行类型检查。此外，与没有类型级计算相比，使用类型级计算可以使用更少的手动插入强制转换来检查更具表现力的属性。在这个过程中，我们发现了两个类型错误和一个文档错误，并得到了开发人员的确认。因此，我们相信CompRDL在为动态语言带来精确的静态类型检查方面向前迈出了重要的一步。
Many researchers have explored ways to bring static typing to dynamic languages. However, to date, such systems are not precise enough when types depend on values, which often arises when using certain Ruby libraries. For example, the type safety of a database query in Ruby on Rails depends on the table and column names used in the query. To address this issue, we introduce CompRDL, a type system for Ruby that allows library method type signatures to includetype-level computations(orcomp typesfor short). Combined with singleton types for table and column names, comp types let us give database query methods type signatures that compute a table’s schema to yield very precise type information. Comp types for hash, array, and string libraries can also increase precision and thereby reduce the need for type casts. We formalize CompRDL and prove its type system sound. Rather than type check the bodies of library methods with comp types—those methods may include native code or be complex—CompRDL inserts run-time checks to ensure library methods abide by their computed types. We evaluated CompRDL by writing annotations with type-level computations for several Ruby core libraries and database query APIs. We then used those annotations to type check two popular Ruby libraries and four Ruby on Rails web apps. We found the annotations were relatively compact and could successfully type check 132 methods across our subject programs. Moreover, the use of type-level computations allowed us to check more expressive properties, with fewer manually inserted casts, than was possible without type-level computations. In the process, we found two type errors and a documentation error that were confirmed by the developers. Thus, we believe CompRDL is an important step forward in bringing precise static type checking to dynamic languages.
登录
查看更多内容
DOI：
--
发表时间：
2013
期刊：
ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation
影响因子：
--
作者：
J. Cheney;S. Lindley;Gabriel Radanne;P. Wadler
通讯作者：
P. Wadler
Ruby 中特定领域语言的契约
DOI：
--
发表时间：
2014
期刊：
Dynamic Languages Symposium
影响因子：
--
作者：
T. Stephen Strickland;Brianna M. Ren;Jeffrey S. Foster
通讯作者：
Jeffrey S. Foster
TypeScript 的细化类型
DOI：
10.1145/2908080.2908110
发表时间：
2016
期刊：
Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation
影响因子：
--
作者：
Panagiotis Vekris;B. Cosman;Ranjit Jhala
通讯作者：
Ranjit Jhala
Ruby 的细化类型
DOI：
--
发表时间：
2018
期刊：
and Abstract Interpretation - VMCAI'18
影响因子：
--
作者：
Kazerounian, Milod;Vazou, Niki;Bourgerie, Austin;Foster, Jeff;Torlak, Emina
通讯作者：
Torlak, Emina
将系统类型作为宏
DOI：
10.1145/3009837.3009886
发表时间：
2017
期刊：
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages
影响因子：
--
作者：
Stephen Chang;Alex Knauth;B. Greenman
通讯作者：
B. Greenman