论文标题
基于注释的静态类型推理的有效性
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.
