Mode-Sensitive Type Analysis for Prolog Programs

Type systems are popular tools programmers use to write bug-free programs easily. In many cases, type systems also offer the benefit of theoretical guarantees with respect to the program's behavior; such statements are usually phrased in type-system slang as "Well-typed programs can't go wrong". In the context of Prolog, two different treatments of types have been employed in various type systems. Descriptive (or regular) types, which are over-approximations of the success set of a program, characterize programs as well-typed based on the program's contents, in a way that everything true in the program is also well-typed. A common application of type systems with descriptive types is in termination analysis. On the other hand, prescriptive types are used to best describe legitimate ways of calling Prolog predicates, hence provide a better discrimination on well-typedness versus success/failure in Prolog. Prescriptively typed systems are most commonly used for helping users in debugging their programs.;In this thesis we present the design and operational semantics of a new type system with parametric and subtyping polymorphism for Prolog in the context of prescriptive types, called P<:. What distinguishes P<: from other type systems proposed for Prolog, mode information is used along with the types of the predicates' arguments for ensuring well-typedness. In its initial design, P <: uses zero-context mode information, and is extended to use type-mode information from any custom inferencer later on. We use Bounded Quantification in the form of Universal and Existential types to define a richer language of expressing type signatures. We also introduce the notion of annotations to type variables as a natural way to represent typings in P<:, which allows us to express (sub)type checking using standard unification, and appropriate definitions for replacements and substitutions. Furthermore, we provide a well-typedness argument specifically tailored for Prolog programs, guaranteeing that for a given well-typed program-query pair, all answers inferred will be well-typed. Finally, we make P<: easily used in practice with an inference algorithm for the types of program variables, in order to ensure well-typedness with minimal annotations in the program.