Type Checking and Type Inferencing for Logic Programs with Subtypes and Parametric Polymorphism

We analyze basic shortcomings of existing proposals for type checking and type inferencing in logic programming languages. A new type system is presented using simple and declarative type annotations. It includes parametric polymorphism and subtyping. Static type checking and inferencing within the new type system is able to detect more programming errors than in other comparable systems. Our approach is independent of a specific resolution calculus and therefore applicable to a wide range of logic languages. A type inferencing algorithm is presented for reconstructing variable typings. As a concrete instance, the results were applied to unrestricted standard Prolog with type annotations, for which a type checking and type inferencing tool is available. This report is part of the documentation for a type checking tool available at !URL:http://www.fernuni-hagen.de/pi8/typical/?. It is complemented by a report "On the Use of Types in Logic Programming" [Mey96]. Research supported by ..