Re: [Sml-implementers] flexible records

[Andreas R. <ros...@ps...>]

Stephen Weeks wrote:
> 
> Andreas Rossberg:
> > That is an interesting approach. Some things came to my mind, though.
> > First, you have to consider that, in general, there can be arbitrarily
> > many type schemes that you have to back-patch after discovering a new
> > field. For example:
> >
> >       val f = #foo
> >       val g = fn h => h o f
> >       val h = fn x => f x
> >       val _ = f {foo=0, bar=1}
> >
> > So a full solution requires an extendable list of back-pointers with
> > every flexible record type.
> 
> In MLton, updates to the spine are seen by all the flexrecords that
> share the spine.  Thus, there is no need to have a list of
> back-pointers.

But it only works that easily if you have a representation of type
schemes that keeps quantifiers implicit. For various reasons, this is
not the case in the Alice compiler, for example.

> Andreas Rossberg:
> > But the most important question IMHO is whether there is a simple rule
> > describing what programs can be type-checked. If there is no simple rule
> > then the behaviour of the type checker is likely to be unpredictable for
> > the user, which would be rather unfortunate. But I am now pretty
> > convinced that your scheme allows a general and simple rule like "sets
> > of labels must be determined within smallest enclosing strdec".
> 
> I think that the "general and simple rule" is that of the Definition.

Well, the Definition does not restrict the context, so defining it to
only extend to some particular phrase is not exactly the rule of the
Definition. But that's nitpicking.

> Do you have examples that you think will not be properly inferred?

No, if even signature matching is no problem then I am ready to believe
that everything will work for any choice of context. Still I am feeling
a bit uneasy since this does not seem trivial to prove and may be much
harder to implemenent in compilers using different type representations.

> The program context could be specified to be one of many things, and
> as David Matthews says, it probably makes sense for it to be the same
> as overloading.

> I personally would like at least strdec, and even better topdec.  I
> think restricting the scope to be valdec is too painful.

I agree (from a user's POV, that is ;-) ). Note however that the
Definition in fact restricts overloading resolution to strdec.
Unfortunately, choosing strdec also has the disadvantage of being pretty
ambiguous due to the ambiguous grammar. So valdec still seems to be the
only choice that is (1) unambiguous and (2) can be made consistent with
overloading without violating explicit rules (besides being much easier
to implement).

In the light of language evolution I would rather prefer to get rid of
the pain by introducing some simple form of row polymorphism.