Alternative implementations of record contracts

[yannham]

In #169 (related issue #157), contracts for records have been implemented. This gives a first working implementation, but the PR led to some discussion about other possible designs or implementation. This issues gathers ideas about alternatives.

Context

The non-trivial part about record contracts is polymorphism. Take a function of type forall a. {field: Num | a} -> {field: Num, field2: Str | a}. Checking the non-polymorphic part of the type is simple: check that the argument has a field field of type Num and that the return value have the same field, plus a field field2 of type Str. But the function can violate the polymorphic part of the contract in several ways. Here are some examples:

//1: remove a field from the polymorphic part
let wrong = fun r =>
  let r = if hasField "foo" r then r -$ "foo" else r in
  r$["field2" = "some string"]

//2: add a field to the polymorphic part
let wrong = fun r =>
  let r = if !(hasField "foo" r) then r$["foo"=2] else r in
  r$["field2" = "some string"]

//3: rewrite a field from the polymorphic part, possibly changing the type
let wrong = fun r =>
  let r = if hasField "foo" r then r -$ "foo" $["foo"="rewritten"] in
  r$["field2" = "some string"]

//4: rewrite a field from the polymorphic part without changing the type
let wrong = fun r =>
  let r = if hasField "foo" r && isNum r.foo then r -$ "foo" $["foo"=0] in
  r$["field2" = "some string"]

//5: make the result depend on the polymorphic part
let wrong = fun r =>
  let str = if hasField "foo" r then "haz foo!" else "not haz foo" in
  r$["field2" = str]

Examples 1, 2 and 3 are clear violations of type soundness, as they change the meaning of a between the input and the output. Examples 4 and 5 are less clear-cut: they violate parametricity, which is in general expected from parametric polymorphism, but they don't break type soundness. They are also not of the same severity: 4. changes a value from the polymorphic part, while 5. just inspects it and makes its return result depend on the shape of the polymorphic part.

Question

The common wisdom is that contracts should ensure parametricity [1], as is already the case for non-record types in Nickel. A standard technique to achieve this is dynamic sealing: for example, the contract of forall a. a -> a seals the argument with a special construct (turning M to Wrapped(a,M)), which prevents inspection. It can only be passed to other functions or returned. At the end, the contract tries to unseal the result, checking that type variables correspond (in this case this is useless, but in types containing several variables, this forbids ill-typed functions like let f = Assume(forall a b. a -> b -> a, fun x y => y)).

Implementing this for records raises the following questions:

• At what granularity do we enforce parametricity ? In particular, while 4. looks like it should not be possible, is 5. really a problem ?
• how do we implement it ?

Proposals

The criterion are the following:

• invasiveness: does it require to change the current abstract machine ? Does it add complexity?
• performance: does it inflict a penalty performance on non-polymorphic code ?
• parametricity: what level of parametricity does it ensure ?
• error reporting

Coarse sealing through magic field

This is the implementation of #169. Coarse alludes to the fact that the polymorphic tail is hidden as a whole. It is stored as a new record in a special field _%wrapped.

• invasiveness: minimal, it uses only existing features.
• performance: it does not affect non-polymorphic code, and the operations used are rather simple.
• parametricity: it enforces full parametricity, as the tail is totally inaccessible.
• error reporting: one questionable consequence is that accessing a field of the tail creates a missing field error, instead of a blame error, for example in this case Assume(forall a. { | a} -> Num, fun r => r.foo).

Another consequence is that it add a fields _%wrapped which can be observed via hasField and fieldsOf. Its content is sealed, and it is always present for polymorphic record arguments, so no information leaks, but it may interfere with standard user code (say, one that relies on the precise result of fieldsOf).

Coarse sealing built-in

This is the same solution as above, but where the magic field of record becomes a built-in feature.

• invasiveness: need to add a Option<Box<Term>> field to records, and rewrite in consequence all records operations (though in a pretty mechanical way). We need to add primitive operators to set or get the content of this field.
• performance: non-polymorphic contracts have an additional pointer. Other than that, usual operations should not suffer any penalty.
• parametricity: as above, full parametricity.
• error reporting: this gives the possibility to raise a blame error when accessing a field which exists but is sealed in the polymorphic part.

Fine-grained sealing

Another approach is to be more granular, and seal each field of the tail independently. A naive implementation would allow a function to inspect at least the shape of the polymorphic row. On the other hand, one can maintain say an access table of the sealed fields to prevent this. In this case, it is easier to control what can be done on sealed fields: we could make them appear in the fieldsOf list or not independently of them being accessible or not.

• invasiveness: this approach is more invasive, as all records operation needs to be aware that some fields are different from others, and to adopt a different behavior accordingly. Records must also be extended with an access table.
• performance: same as for invasiveness, this approach require additional checks for all record operations, and probably interact with merging as well.
• parametricity: customizable.
• error reporting: customizable.

Conclusion

The fine-grained approach is cited for exhaustiveness, but I don't think it's worth the trouble as there is currently no incentive to allow some operations on the sealed part. The first approach is now implemented, and if the drawbacks (presence of an additional magic field in sealed records plus non-blame errors in some cases) are found to be problematic, the second approach mitigates them.

[aspiwack]

At the very least, this is not urgent.

That being said, it is a good question: what should the semantics of merging two records with a parametric row be?

And in fact, all these are good questions: what should listing the fields of a parametric record return? What should querying for the existence of a field return?

These are not implementation questions: we do want these things specified.

We can take our time to flesh this out. But we shouldn't let an arbitrary implementation choice dictate our semantics.