|
Abstract : |
We describe a new logic called typed predicate calculus (T PC) that gives declarative meaning to logic programs with type declarations and type inference. T PC supports all popular types of polymorphism, such as parametric, inclusion, and ad hoc polymorphism. The proper interaction between parametric and inclusion varieties of polymorphism is achieved through a new construct, called type dependency, which is reminiscent of implication types of [PR89] but yields more natural and succinct specifications. Unlike other proposals where typing has extra-logical status, in T PC the notion of type-correctness has precise model-theoretic meaning that is independent of any specific type-checking or type-inference procedure. Moreover, many different approaches to typing that were proposed in the past can be studied and compared within the framework of our logic. As an illustration, we apply T PC to interpret and compare the results reported in [MO84, Smo88, HT90, Mis84, XW88]. Another novel feature of T PC is its reflexivity with respect to type declarations; namely, in T PC these declarations can be queried the same way as any other data. This should be contrasted with other proposals where typing is part of meta-specifications about the program, inaccessible from within the program. Type reflexivity is useful for browsing knowledge bases and, potentially, for debugging logic programs., |
