Polymorphically Typed Logic Programs.
Eyal Yardeni, Thom Frühwirth, Ehud Y. Shapiro · 1991
We introduce polymorphically typed logic programs, an integration of a polymorphic type system with logic programs. The first-order notion of predicates is extended to parametric predicates, which are parameterized by types. The type system accommodates both subtypes and parametric polymorphism. It unifies features of value-based and name-based approaches. The denotation of a typed logic program is given by its type completion, a transformation that incorporates explicit type conditions into a parametric logic program. The result of the transformation is a restricted form of a HiLog program. We give fixpoint semantics to our language (actually to full HiLog). We define a notion of well-typing, which relates type declarations for predicates in the program to an approximation of the denotation of the type completed program. We present a type-checking algorithm for verifying that a program is indeed well-typed. Finally we discuss some extensions to the type system.