Subject: [Fwd: at INRIA]
From: Craig Chambers (chambers@cs.washington.edu)
Date: Thu Nov 23 2000 - 09:40:25 PST
Interesting stuff from Vass.
-- Craig
Vassily wrote:
>
> Craig,
>
> Meant to write about my work earlier... feel free to forward to
> the Cecil list if appropriate.
>
> Here Didier Remy, Francois Pottier and I started discussing a language
> that's a small extension of lambda+let (is that core ML?) with datatypes
> and generic functions taken from your EML. Didier wants to start from
> some decidable typechecking and see how much expressiveness can be
> obtained. Francois has much more interest in constraint-solving
> technology (so it seems to me).
>
> To make things more concrete, I decided to write up typechecking rules and
> prove soundness for this language (parameterized by the constraint
> system). This should give an idea of the requirements for the constraint
> system, allowing us to play with Francois's constraints and others,
> possibly adjust language design, and investigate type inference. (For the
> soundness proof, I actually took out almost everything from the language,
> including nested functions and let, and made generic functions
> second-class. My idea is that the proof technique for the small language
> will apply straightforwardly to reacher languages.)
>
> I also tried to come up with an easily-decidable constraint solving
> algorithm by restricting expressiveness of Cecil-style constraints. I
> started out by allowing only single subtyping, that led to another
> restriction and then another, and finally I realized that I was working in
> a system less powerful than Francois's. [I should probably explain what
> his system is like, but prefer to do that in person when I am back.] So I
> quit this line.
>
> 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.)
>
> Another thing that resulted from my attempt is appreciation for the work
> on recursively-constrained types by Smith et al. In my attempt at a
> simple constraint solving algorithm I naturally ended up following their
> approach of building constraint closure and using its kernel as an
> efficient and equivalent representation. Although it is not clear whether
> it will work for more complicated constraints.
>
> The difference between the Cecil-style constraints and their constraints
> became clearer to me, also. In particular, they do not provide for
> user-defined hierarchy of type constructors (their only type constructor
> is -> with predefined co-/contra-variance). They go deeper than us,
> however, in handling recursive types. One can argue that Cecil types are
> also recursive, but theirs are more so. In particular, we only consider
> types from the Herbrand universe, which are of the form
> type ::= type_constructor[type1,...,typeN]
> while they also incorporate regular trees, like t->(t->(t->...)).
> The need for such "more recursive" types in Vortex, however, has been
> observed by Craig (namely, for taking fixpoints of mutually-recursive
> families, like Model[Model,View]). This direction has not been explored.
>
> 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.
>
> Cheers,
> Vass
This archive was generated by hypermail 2b25 : Thu Nov 23 2000 - 09:39:48 PST