From Monomorphic to Polymorphic Well-Typings and Beyond

Abstract. Type information has many applications, it can be used for optimized compilation, termination analysis, error detection,.... How-ever logic programs are typically untyped. A well-typed program has the property that it behaves identically with or without type checking. Hence the automatic inference of a well-typing is worthwhile. Existing inferences are either cheap and inaccurate, or accurate and ex-pensive. By giving up the concept that all calls to a predicate have types that are instances of a unique polymorphic type but instead allowing multiple polymorphic typings for the same predicate, we obtain a novel strongly-connected-component-based analysis that provides a good com-promise between accuracy and computational cost.