现代化基于 SMT 的类型错误定位

强类型函数式编程语言的传统实现往往无法定位类型错误的根本原因。结果是，类型错误信息常常误导且令人困惑——尤其是对于学习此类语言的学生而言。我们描述了 Tyro，这是一种类型错误定位工具，通过 Pavlinovic 等人的基本思想，对不规范程序找到最优的错误来源：我们首先将类型约束翻译为 SMT (满足模块理论)，使用比实际 SMT 编码更可读的中间表示；在此过程中，我们应用了多态类型的新编码。其次，我们将中间表示翻译为实际的 SMT 编码，并利用最新的即插即用 SMT 求解器优势，有效地找到不规范程序的最优错误来源。我们的设计保持了先前和类似工作中启发式与搜索的分离。此外，我们的体系结构设计增加了模块性、可重复使用性和整体体系结构的可信度，使用中间表示来促进安全的 SMT 编码生成。我们认为这一设计原则将适用于许多其他利用 SMT 求解器的工具。我们的实验评估强化了 SMT 方法在使用专家标记的程序和更大规模分析的自动方法中找到准确错误来源的能力。与先前工作相比，Tyro 为大规模评估错误定位技术奠定了基础，这些技术可以集成到编程环境中，从而使我们能够在实践中了解精确错误信息对学生的影响。