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 reconctructing 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.
Nutzung und Vervielfältigung:
Alle Rechte vorbehalten