RE: [Sml-implementers] flexible records

[David M. <Dav...@pr...>]

On Wednesday, October 17, 2001 6:20 PM, Andreas Rossberg
[SMTP:ros...@ps...] wrote:

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

I didn't give much in the way of implementation details in my previous
message but simply a quick explanation.  There are a number of details
that have to be considered.

The actual implementation of the back-pointers is as a list of
type-variables.  As well as acting as references which can be updated
when fields are added to the record or frozen (made rigid) the
type-variables also carry information such as the equality attribute.
That is important in examples such as:

local
	fun f (x as {a, ...}) = (x=x; a)
	fun g {a, ...} = a
	fun h x = (g x; f x)
	val _ = h{a=1, b=2}
in
	val f = f and g = g and h = h
end;

where fields added to f and h have to be equality types but not those
added to g:

val f = fn : {a: ''a, b: ''b} -> ''a
val g = fn : {a: 'a, b: 'b} -> 'a
val h = fn : {a: ''a, b: ''b} -> ''a

Whenever an instance of flexible record type is found there is a need to
check back to the generic to see if any fields have been added since the
instance was created.  Here again new type variables have to added with
attributes depending on both the generic and the instance.

local
	val f = #foo
	val g = valOf o f
	val _ = f {foo=0, bar=1}
in
	val g = g
end;

In this example the type variable added to g is not bound within g and
so there is a message about free type variables.

Warning:
The type of (g) contains a free type variable.
Setting it to a unique monotype.

val g = fn : {bar: _b, foo: _a option} -> _a

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

I agree.  In Poly/ML at any rate it simplifies the description of what
is accepted.  The rule is the same for overloading, free type-variables
and, now, flexible records: they must be specified within the topdec.
For example:
> structure S = struct val f = #foo end val _ = S.f{foo=1, goo=2};
structure S : sig val f : {foo: 'a, goo: 'b} -> 'a end

> structure S : sig val f : {a: 'a, b: 'b} -> 'a end = struct val f = #a
end;
structure S : sig val f : {a: 'a, b: 'b} -> 'a end

While other implementations may put slightly different restrictions on
the scope I expect it would be the same as their rules for overloading.

David.