[Prev][Next][Index][Thread]
Question concerning ideals
Date: Tue, 28 Feb 89 16:25:20 PST
To: types@xx.lcs.mit.edu
Cc: Pavel.pa@xerox.com, Demers.pa@xerox.com, Gilbert.pa@xerox.com
Consider a language of types including some constants and function arrow,
along with "constrained quantification". The latter involves type
expressions of the form
forall a_1,...,a_k such that { ..., tau_i <= tau'_i, ... } . rho
where the a's are type variables and rho and the tau_i and tau'_i are type
expressions. We define the meaning of terms in this language using ideals
in the usual way. The meaning of a constrained quantified type expression
is the intersection over all instantiations of rho such that the given set
of constraints is satisfied. A constraint [[ tau <= tau' ]] is satisfied
iff and only if the meaning of tau is a subset of the meaning of tau'.
Consider a set of constraints of the form
tau_1 <= alpha
.
.
.
tau_n <= alpha
We would like to find values for alpha that satisfy all of these
constraints. If none of the tau_i mention alpha freely, then the type
forall alpha such that { tau_1 <= alpha, ..., tau_n <= alpha } . alpha
is a solution. In fact, it is not difficult to see that this expression
denotes the least upper bound of the tau_i.
This quantified type is still a solution if we allow the tau_i to mention
alpha AND the tau_i are all covariant in alpha.
My question: what about the general case? If the tau_i are allowed to be
arbitrary type expressions, does the above quantified type always represent
a solution to the system? This is equivalent to asking whether or not such
systems of constraints always have a least solution.
More abstractly put, what properties P of ideals contain least elements?
Thank you for your attention.
Pavel Curtis
Xerox PARC/CSL
PS- Please reply to me directly; I am not a member of the TYPES list.