Closed contracts

[yannham]

Depend on #370. Fix #303.

Summary

This PR implements the fix proposed in #303: it makes the contract application operator let Contract = { a | Num } in value | #Contract more restrictive than just value & Contract, in that it now raises a contract violation if value has an extra field other than a.

Contract application having a different behavior than merge for record contracts is nice, because beside contract application now doing the correct thing (by default a schema shouldn't allow extra fields), one can still use standard merging on closed contracts to compose them:

let ContractA = {a | Num} in
let ContractB = {b | Num} in
let Contract= ContractA & ContractB in
{a = 1, b = 2} | #Contract

Open contracts

This PR introduces a new ellipsis syntax .. to stipulate that Contract allows extra field, as in the working let Contract = {a | Num, ..} in {a = 1, b = 2} | #Contract . With the ellipsis, a record contract behaves as before this PR.

The behavior with respect to merging is that if any of the operands is open, then the resulting contract is open. The rationale is that .. can be imagined as a special field that is syntactically merged as any other field: {a | Num} & {..} = {a | Num, ..}.

[dpulls]

🎉 All dependencies have been resolved !

[thufschmitt]

I really like this.

Just a very minor comment that you can feel free to ignore, but otherwise 👍

[thufschmitt]

(nit) This looks a lot like a monoid. Isn’t there a standard trait for that in Rust?

[yannham]

Good point (and typical Haskeller 😛 ), but I can't find one in the standard library, just in some third-party crates, so I guess I'll leave it as it is.