Sound, heuristic type annotation inference for Ruby
Sound, heuristic type annotation inference for Ruby
复制标题
DOI：
10.1145/3426422.3426985
复制
发表时间：
2020-11
期刊：
影响因子：
--
通讯作者：
Milod Kazerounian;Brianna M. Ren;J. Foster
中科院分区：
文献类型：
--
作者：
Milod Kazerounian;Brianna M. Ren;J. Foster
许多研究人员已经探索了将静态类型系统改造为动态语言。这就产生了一个问题：如何将类型注释添加到以前没有类型的代码中。一个明显的解决方案是类型推断。然而，在复杂的类型系统中，特别是那些具有结构类型的类型系统中，类型推断通常会产生大多数通用类型，这些类型对于程序员来说很大，很难理解并且不自然。为了解决这个问题，我们引入了InferDL，一个新的Ruby类型推理系统，它通过结合猜测类型的语法来推断声音和有用的类型注释。例如，我们可能会猜测名称以“count”结尾的参数是整数。InferDL首先运行标准类型推理，然后对标准类型推理产生过度通用类型的任何位置应用解析。启发式猜测作为约束被添加到类型推断问题中，以确保它们与程序的其余部分和其他启发式猜测一致;不一致的猜测被丢弃。我们正式InferDL在核心类型和约束语言。我们在RDL之上实现了InferDL，RDL是一个现有的Ruby类型检查器。为了评估InferDL，我们将其应用于四个Ruby on Rails应用程序，这些应用程序之前已经使用RDL进行了类型检查，因此具有类型注释。我们发现，当使用解析法时，与没有解析法的标准类型推断相比，InferDL推断出的类型比以前的注释多22%。我们还发现了一个新的类型错误。我们进一步评估了InferDL，将其应用于另外六个应用程序，发现了另外五个类型错误。因此，我们相信InferDL是一种很有前途的方法，在动态语言中推断类型注释。
Many researchers have explored retrofitting static type systems to dynamic languages. This raises the question of how to add type annotations to code that was previously untyped. One obvious solution is type inference. However, in complex type systems, in particular those with structural types, type inference typically produces most general types that are large, hard to understand, and unnatural for programmers. To solve this problem, we introduce InferDL, a novel Ruby type inference system that infers sound and useful type annotations by incorporating heuristics that guess types. For example, we might heuristically guess that a parameter whose name ends in “count” is an integer. InferDL works by first running standard type inference and then applying heuristics to any positions for which standard type inference produces overly-general types. Heuristic guesses are added as constraints to the type inference problem to ensure they are consistent with the rest of the program and other heuristic guesses; inconsistent guesses are discarded. We formalized InferDL in a core type and constraint language. We implemented InferDL on top of RDL, an existing Ruby type checker. To evaluate InferDL, we applied it to four Ruby on Rails apps that had been previously type checked with RDL, and hence had type annotations. We found that, when using heuristics, InferDL inferred 22% more types that were as or more precise than the previous annotations, compared to standard type inference without heuristics. We also found one new type error. We further evaluated InferDL by applying it to six additional apps, finding five additional type errors. Thus, we believe InferDL represents a promising approach for inferring type annotations in dynamic languages.