Implement contracts for records

[yannham]

Close #157. Partly address #158. Implement contracts for record types. Uses the same kind of "sealing" technique as for polymorphic types to preserve parametric: it forbids the inspection of a polymorphic tail.

Dynamic sealing

Dynamic sealing is the technique used to prevent a function claiming to be polymorphic in some arguments to inspect them, which would violate parametricity. For non-record types, a contract for a polymorphic type, say forall a. a -> a -> a conceals each argument using a special language construct, Wapped(id, term), that seals a term and store an identifier relative to the corresponding type variable (here a).

The same kind of mechanism is required for records. Take a polymorphic type forall r. {foo : Num | r} -> Num. A function of this type must not be able to access the polymorphic tail r: for example, fun x => if hasField "bar" then 0 else x.foo violates parametricity. As for standard polymorphism, the contract of such a function must seals the additional fields of the argument, and restores them when a value "exits" the function (is given as an argument to another function or returned).

Proposed implementation

This PR proposes to put the additional fields to seal in a separate record, which is then wrapped as for non record polymorphic types, and put in a special field of the value. Concretely, take:

let f = Assume(forall r. {foo: Num, foo2: Str | r} -> { foo2: Str | r}, fun r => r -$ "foo") in
f {foo = 1; foo2 = "b"; bar = true; baz = "a"}`

The contract turns the arguments to {foo = 1; foo2 = "b"; _%wrapped = Wrapped(sym, {bar = true; baz = "a"}} which is then handed to the function. The function removes the foo fields, which gives {foo2 = "b"; _%wrapped = ... }. Then the contract checks that the resulting records has only the field foo2 (ignoring _%wrapped), extract and try to unwrap the value inside _%wrapped, and then merge it with the non polymorphic part, giving merge {foo2 = "b"} {bar = true; baz = "a"} which is the desired {foo2 = "b"; bar = true; baz = "a"}. Note that

Pros

• Does not require any modification of the AST of terms or the addition of operators. It just uses current features to implement record contracts, namely "simple" sealing, merging and record.
• Seals thing en masse, instead of each field separately.
• Extra fields appear to be absent from the point of view of the function: the first function will generate "missing field" error. Not sure if it's a pro, but it is a fact.

Cons

• the _%wrapped field is not completely hidden from the function. It will still show up in the result of hasField or fieldsOf, and can be accessed via the dynamic field access operator. It won't violate parametricity though, as it is always there anyway and its content itself is protected by the Wrapped constructor. This does not concern other functions or subcontracts since the original contract will take care of sealing/unsealing a the function boundaries. It can be mitigated by making an ad hoc check inside functions handling record to make it invisible, though this loses a bit the non invasiveness of this approach.

Alternatives

New construct: Add a new node to the AST, SealedRecord(term, sealed). This requires to duplicate most of the code handling records to work on a sealed record. Another solution is to augment all standard records with an Option<Term> field containing a potential sealed part. This also requires to adapt some code. Both requires to add primitive operators to construct and deconstruct such records.

Map on fields: Instead of taking apart all the fields of the tail and put them in a separate record, we could just map the sealing operation on each one of them. The difference with the proposed approach is that such fields still appear in the result hasField or fieldsOf. That is, a polymorphic function would be able to inspect the full structure of its argument, although not the content. I don't really know if this is a violation of parametricity: the function hasField has already this property itself if typed as forall r. { | r} -> Bool.

Summary

what it does

• add Nickel contracts in stdlib/contracts.ncl to handle static record types, using the sealing technique described above.
• implement the generation of record contracts in the contract_open function of Types.

what it does not

• implement the open record contracts described in Dynamic row type for open records #158. This is planned for another PR.

[dpulls]

🎉 All dependencies have been resolved !

[aspiwack]

I think that it will be hard to support any introspection function on the type of a record while maintaining parametricity.

It is likely that the Right Thing™ to do is simply to prevent inspecting the list of fields in a record which is sealed.

I remember, though, that the reason why we went the sealing route for arbitrary variables had to do with some pragmatic constraints, I'm not sure we want to actually enforce parametricity at all cost (valuable though it is). Maybe it was mostly about not having to pass an explicit type application when using a polymorphic function.

---

I do like the idea of a bit array representing the available fields. It's cheap and avoid manipulating the shape of the record.

[aspiwack]

What's happening here? I can't quite follow.

[yannham]

So, h was a hashtable mapping type variables a, b, ... in the environment to the corresponding polymorphic contracts. Said contracts are built with the appropriate information when entering a forall, so that when encountering a type variable occurrence later, one can get the corresponding contract from h. Now we need a second type of polymorphic contract, namely a contract for polymorphic tails { ... | a} to be available, so it is added to this table. Rereading this it's a bit silly to build these contracts in advance just to clone them when they are needed. I should just store the polarity and the unique identifier sy, which are enough to generate corresponding contracts when needed. Let's keep it like that in this PR: it will be taken care of in a related coming cleaning PR (which goal is to address your remark).

[yannham]

I'm not sure we want to actually enforce parametricity at all cost (valuable though it is). Maybe it was mostly about not having to pass an explicit type application when using a polymorphic function.

Yes, I'm not sure allowing the inspection of fields is that bad.

One thing I didn't mention is that sealing is also a simple solution to enforce basic soundness and to reject functions like Assume(forall a. a -> a, fun x => 0). The same holds for records: a function inspecting the name of sealed fields is maybe no big deal, but we certainly don't want functions like Assume(forall a. {field: Num | a} -> {field: Num | a}, fun r => if hasField "other" r then r -$ "other" else r) (which removes the unmentioned field other from the tail) to be accepted, and there too, sealing is a simple solution.

Revisiting this PR, I'm not sure it's the ideal implementation. The contract also allocates quite a bit. Let's roll with this for now, and open an issue with a clear presentation of the different solutions and trade-offs.