[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.