[Prev][Next][Index][Thread]
Polymorphism for predicate logic programs
Date: Tue, 11 Oct 88 17:52:16 CDT
To: types@theory.LCS.MIT.EDU
Cc: reddy%reddy.cs.uiuc.edu@a.cs.uiuc.edu
Reply-To: reddy@a.cs.uiuc.edu
The following paper was presented at the Logic Programming 88
conference. Unfortunately, it does not appear in the proceedings for
various reasons. (It is due to appear in Jounal of Logic Programming
sometime soon).
An interesting terminology is "prescriptive types" and "descriptive
types" for what Harper and Mitchell call "explicit types" and
"implicit types". I wrote this paper before Harper&Mitchell appeared,
and it sounded quite appropriate at that time. By "type systems based
on type inference" in the abstract below, I mean "implicit type
systems". Harper&Mitchell show that the two characterizations are not
the same.
Even though logic programming may not be of wide interest to this
community, the ideas about types may be of interest. Copies are
available by sending mail to me. Please mention your snail mail
address.
Notions of polymorphism for predicate logic programs
----------------------------------------------------
Uday S. Reddy
A POLYMORPHIC PREDICATE is one that can be used in a number of type
contexts. To perform type inference or type checking, we need a
notion of POLYMORPHIC TYPES which express the types of such
predicates. It is shown here that there are several notions of
polymorphism, each applicable in a different context. The
conventional interpretation of polymorphism, as UNIVERSAL
QUANTIFICATION over types, is useful for type systems based on
DECLARATIONS. For type systems based on TYPE INFERENCE, this
interpretation is not adequate [for predicate logic programs]. We
present two methods to express inferred types of polymorphic
predicates. The first is EXISTENTIAL QUANTIFICATION over predicate
types, which gives valid types but does not capture sufficient type
information in general. The second method uses both the kinds of
quantification, but over a richer language of types that includes an
IMPLICATION type constructor. The type systems for which these
methods are useful are characterized.