Effectiveness of Annotation-Based Static Type Inference

TL;DR

This paper proposes a static type analysis method for Prolog that aims to identify type errors without restricting language expressiveness, using plspec, and evaluates it on real-world Prolog code.

Contribution

It introduces a novel static type inference approach for Prolog based on plspec, addressing the challenge of distinguishing success and failure without annotations.

Findings

Effective in detecting type errors in real-world Prolog code

Does not limit the expressiveness of Prolog programs

Applicable to large, complex projects like model checkers

Abstract

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.