On the Use of Types in Logic Programming
In procedural and functional languages it is rather clear what a type error is and the main purpose of typing ist to detect programming errors automatically. Furthermore, in these languages the semantics of a program is usually independent of types. Type systems for logic programming languages differ considerably on these aspects. We will show that these differences lead to several theoretical an practical problems. The mixture of static type checking purposes on the one hand and computations with type constraints in the CLP(X) style on the other hand will be marked as the central source of problems. As a solution we propose a typing scheme which separates these issues. We distinguish three almost independent dimensions ot types in logic programming: those as approximations, types as constraints and types for proving partial correctness. Based on the notion of useless expressions, we develop a method that allows static program analysis for finding type errors, which enables error detection to be more precise than hitherto possible.
Nutzung und Vervielfältigung:
Alle Rechte vorbehalten