Subject: Re: [Fwd: at INRIA]
From: Todd D Millstein (todd@cs.washington.edu)
Date: Fri Nov 24 2000 - 14:47:31 PST
Vass,
Sounds like you're getting some great stuff done over there. A few
questions/comments:
> > On the way, however, some interesting things transpired. The very first
> > one was that a constraint system is likely to have multiple solutions
> > sets. By "solution set" I mean a set of simple bounds on type variables
> > (like, int<=T1<=num, T2<=vector[int], etc.) - such bounds express the
> > space of individual substitutions (in this case, the space includes
> > {T1:=int,T2:=vector[int]}, {T1:=num,T2:=m_vector[int]}, etc.). So, it is
> > likely that the solution of a constraint system cannot be expressed by a
> > single set of type variable bounds, but by a collection of such sets.
> >
> > This effect, which I call "multiplicity," obviously arises in case of
> > multiple unrelated signatures for the same message. For example, "where
> > signature copy_empty(T):S" has a bunch of solution sets that look like
> > "T<=vector[Q], S>=m_vector[Q]". OK, so try to disallow multiple
> > signatures for the same message. But then multiplicity comes back due to
> > multiple subtyping. And even if we rule out that one (which I'd argue
> > strongly we want to keep, it's present even in Java), multiplicity comes
> > back again and again in many other places. Which leads me to the
> > conclusion that for the Really Expressive Constraint System (TM),
> > multiplicity should be built-in up-front, and the constraint solver should
> > handle it. (Otherwise we will keep hitting obstacles one after another.)
> >
I'm not understanding this notion of "multiplicity" very well. In your
example above, are you saying that for any type Q, "T<=vector[Q],
S>=m_vector[Q]" is a valid solution? I'm not familiar with copy_empty; is
there another example I'd better understand? Also, is multiplicity the
same thing as saying that the type system does not have principal types?
In what ways can a constraint solver/type system handle such multiplicity?
> > I would also like to mention another research effort here in the Cristal
> > group, by Pierre Weis's student Jun Furuse, with which I became familiar.
> > (Jun is Japanese, but, God, is he bigger than many French!)
> >
> > They develop "extensional polymorphism" for OCaml, a direction started in
> > the POPL'95 paper by Weis et al. I am still unclear why naming is
> > different, but this is pretty darn close to the later "intensional
> > polymorphism" effort at Cornell (Greg Morrisett et al.). The idea is to
> > pass types (represented by values, of course) as additional arguments at
> > runtime and allowing the programmer to match against those; thus achieving
> > overloading. The interesting part is that they ended up representing the
> > type of such overloaded function in a way that's essentially like Cecil's
> > signatures and signature constraints. For example:
> > convert: int->string; float->string; 'a list->'b list where convert:'a->'b.
> >
> > As you can see, recursion is allowed (and is performed at compile-time by
> > the typechecker). To ensure termination of the recursion, the '95 paper
> > suggest the simple criterion that the complexity of the types in the
> > signature's constraint should be smaller than that in the signature itself
> > (eg complexity('a)=1; complexity(ty list)=1+complexity(ty)). I am sure
> > this criterion can be applied towards termination of Cecil constraint-
> > checking.
> >
Sounds interesting. This idea for proving termination is a standard way
of proving termination of a rewrite system: Given a set of rewrite rules,
define some function F from terms to natural numbers such that for every
rewrite rule, F(left-hand-side) >= F(right-hand-side). If you can show
this, then rewriting is guaranteed to terminate. (Actually, F also has to
have a few simple monotonicity properties, like F applied to a term t must
be >= F applied to any sub-term of t.)
This could be a very nice approach to proving termination of
constraint-checking. The hard part, of course, is coming up with the
right F function.
Todd
This archive was generated by hypermail 2b25 : Fri Nov 24 2000 - 14:47:35 PST