基于求解器的渐进式迁移
Solver-based Gradual Type Migration
摘要：
渐进类型语言允许程序员混合静态和动态类型代码，使他们能够在向代码添加类型注释时逐渐获得静态类型的好处。然而，这种类型的迁移过程通常是具有有限工具支持的手动工作。本文探讨了问题的\emph{automated type migration}：给定一个动态程序，推断额外的或改进的类型注释。现有的类型迁移算法优先考虑不同的目标，如最大限度地提高类型精度，保持与未迁移代码的兼容性，并保留原始程序的语义。我们认为，类型迁移问题涉及到根本的妥协：优化一个单一的目标往往是以牺牲他人。理想情况下，类型迁移工具将灵活地适应一系列用户优先级。我们提出了TypeWhich，一种新的方法来自动类型迁移的渐进类型的λ演算的一些扩展。与之前依赖于自定义求解器的工作不同，TypeWhich为现成的MaxSMT求解器产生约束。这使我们能够轻松地表达目标，例如最小化必要的语法转换器的数量，并约束迁移的类型以与未迁移的代码兼容。我们提出了GTLC类型的迁移算法的第一次全面评估，并比较TypeWhich的其他四个工具从文献中。我们的评估使用以前的基准，和一组新的“挑战问题”。此外，我们设计了一种新的评估方法，突出了渐进类型迁移的微妙之处。此外，我们应用TypeWhich的一套基准Grift，一个程序设计语言的基础上GTLC。TypeWhich能够在除了一个程序之外的所有程序上重建所有人类编写的注释。
英文摘要：
Gradually typed languages allow programmers to mix statically and dynamically typed code, enabling them to incrementally reap the benefits of static typing as they add type annotations to their code. However, this type migration process is typically a manual effort with limited tool support. This paper examines the problem of \emph{automated type migration}: given a dynamic program, infer additional or improved type annotations. Existing type migration algorithms prioritize different goals, such as maximizing type precision, maintaining compatibility with unmigrated code, and preserving the semantics of the original program. We argue that the type migration problem involves fundamental compromises: optimizing for a single goal often comes at the expense of others. Ideally, a type migration tool would flexibly accommodate a range of user priorities. We present TypeWhich, a new approach to automated type migration for the gradually-typed lambda calculus with some extensions. Unlike prior work, which relies on custom solvers, TypeWhich produces constraints for an off-the-shelf MaxSMT solver. This allows us to easily express objectives, such as minimizing the number of necessary syntactic coercions, and constraining the type of the migration to be compatible with unmigrated code. We present the first comprehensive evaluation of GTLC type migration algorithms, and compare TypeWhich to four other tools from the literature. Our evaluation uses prior benchmarks, and a new set of ``challenge problems.'' Moreover, we design a new evaluation methodology that highlights the subtleties of gradual type migration. In addition, we apply TypeWhich to a suite of benchmarks for Grift, a programming language based on the GTLC. TypeWhich is able to reconstruct all human-written annotations on all but one program.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
