基于注释的静态类型推断的有效性
Effectiveness of Annotation-Based Static Type Inference
摘要：
静态类型系统的好处是众所周知的：它们提供了在运行时不会发生类型错误的保证，并且本质上，推断类型充当了函数如何调用的文档。另一方面，许多类型系统不得不限制语言的表达能力，因为一般来说，给定的程序在类型方面是否正确是不可判定的。到目前为止还没有解决的另一个问题是，对于逻辑程序设计语言，如Prolog，如果没有额外的注释，就不可能区分预期的和非预期的失败，更糟糕的是，不可能区分预期的和非预期的成功。在本文中，我们将详细阐述和讨论上述问题。作为替代方案，我们提出了一个静态类型分析，这是基于plspec。而不是确保完全的类型安全，我们的目标是静态识别类型错误的最大努力的基础上，而不限制Prolog程序的表达能力。最后，我们评估我们的方法在现实世界中的SWI社区包和一个大型项目实现模型检查器的代码。
英文摘要：
Benefits of static type systems are well-known: they offer guarantees that no type error will occur during runtime and, inherently, inferred types serve as documentation on how functions are called. On the other hand, many type systems have to limit expressiveness of the language because, in general, it is undecidable whether a given program is correct regarding types. Another concern that was not addressed so far is that, for logic programming languages such as Prolog, it is impossible to distinguish between intended and unintended failure and, worse, intended and unintended success without additional annotations. In this paper, we elaborate on and discuss the aforementioned issues. As an alternative, we present a static type analysis which is based on plspec. Instead of ensuring full type-safety, we aim to statically identify type errors on a best-effort basis without limiting the expressiveness of Prolog programs. Finally, we evaluate our approach on real-world code featured in the SWI community packages and a large project implementing a model checker.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
