Re: [Sml-implementers] flexible records

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

David Matthews wrote:
> 
> Poly/ML uses references for type variables (as I guess many
> implementation do) and creating an instance from a generic type involves
> copying the type generating new references for each type variable.  This
> normally loses the connection between an instance and the original
> generic so that unification of an instance does not affect the generic.
> This solution requires a pointer back from each instance to the
> corresponding generic.

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. Lists must be concatenated when unifying two
such types.

Another effect one has to take care of is that there can be monomorphic
type schemes where you must not add quantifiers because of the value
restriction:

	val f = #foo
	val g = valOf o f
	val _ = f {foo=0, bar=1}

Here, back-patching the type scheme of g actually requires
reverse-introduction of a free type variable. This may or may not be
problematic in general, I am not completely sure. At least the
back-pointers have to be decorated with some flag.

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". (A
larger scope may again be problematic because we then had to cope with
interactions between flexible records and signature matching.)

	- Andreas