Using Types as Approximations for Type Checking Prolog Programs

Subtyping tends to undermine the eects of parametric poly- morphism as far as the static detection of type errors is concerned. Start- ing with this observation we present a new approach for type checking logic programs to overcome these diculties. The two basic ideas are, rst, to interpret a predicate type declaration as an approximation for the success set of the predicate. Second, declarations are extended with type constraints such that they can be more rened than in other con- ventional type systems. The type system has been implemented in a system called Typical which provides a type checker for Standard Prolog enriched with type annotations.