RE: [Sml-implementers] flexible records

[Stephen W. <sw...@in...>]

David Matthews:
> I was intrigued by these examples and it set me thinking about whether
> it was possible to get these to work.  After a bit of thought I managed
> to come up with a solution and try it out in Poly/ML.  
...

I also thought about how to make it work in MLton, and came up with a
solution similar to yours.  I added an extra field to each flexrecord
to hold a "spine", which keeps track of the fields that are in the
record and whether or not more fields can be added.  The spine is
shared among all flexrecords that must have the same domain, either
due to instantiation, generalization, or unification.  Spines are easy
to unify when unifying a two flexrecords or a flexrecord and a
rigid record.  In a post-pass after unification, additional type
variables are added for fields in the spine of a generic flexrecords
that weren't originally generalized.

The upshot is that this took about 300 lines of code to implement in
MLton, and works on all the examples that have so far appeared on this
list.  The only case I know of where it fails is due to an unrelated
problem in MLton (types in signatures are ignored), which causes the
following program to fail with an unresolved flexrecord.

structure S:
   sig
      val f: {foo: int} -> int
   end =
   struct
      val f = #foo
   end

Other than examples like this, I believe that what I implemented
meets the requirements of the Definition.

David Matthews:
> On the other hand, I've come across a number of cases where I've
> wanted a function to operate on only one or two fields of a labelled
> record.  I've had to add an explicit type constraint or list all the
> fields just so that the record type is rigid within the function,
> even though the surrounding context would fully specify it.

I am often bitten by this as well, and would love to see all SML
compilers support this more powerful flexrecord inference.

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.

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.
Do you have examples that you think will not be properly inferred?  Of
course, the program context in the following Definition fragment must
be spelled out.

    For each occurrence of a record pattern containing a record
    wildcard, the program context must uniquely determine the domain
    of its row type. 

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.

David Matthews:
> 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.
...
> While other implementations may put slightly different restrictions on
> the scope I expect it would be the same as their rules for overloading.

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

Andreas Rossberg:
> A larger scope may again be problematic because we then had to cope
> with interactions between flexible records and signature matching.

I don't see why this causes problems.  Signature matching can impose
constraints on the domain of a flexrecord just as unification can.