Efficient run-time type checking of typed logic programs

AbstractThis paper presents a new approach to the problem of guaranteeing that definite logic programs are free of type errors. Previously, two approaches to this problem have been considered. The first approach is static type checking, in which predicate types are inferred from the program and checked for self-consistency and for consistency with declared types. Static type checking, however, is in general incomplete, as it can neither only reject programs with type errors nor only accept programs which are type-error free. The second approach is dynamic type checking, in which types are checked against type declarations at run-time. Dynamic type checking, however, is prohibitively expensive.Our approach combines static and dynamic type checking so that, not only is completeness attained but the overhead of run-time type checking is substantially reduced. This is achieved by taking advantage of any redundancy between type declarations and types enforced by the program itself. Type checks are added to a clause only where redundancy cannot be shown to exist. In particular, only local variables ever need be type checked, and type checks on some variables may be shown redundant by use of type inference and analysis of type dependencies; to implement such analysis, we have developed new algorithms for intersecting and comparing types and for unifying types and terms. Hence, programs with declared types may be transformed into programs with a small number of explicit type checks. We argue that the overhead of the remaining type checks is generally small and is justified by the benefits of having effective type checking for logic programs