Add a freeze primop and stdlib wrapper

[yannham]

Following a confusing behavior around the interaction of recursive fields and dictionary operations reported in #1866 (insert, remove, update), it was proposed in #1877 to freeze recursive records before applying dictionary operations.

This PR adds a primitive operation to do so, which applies pending contracts, flushes them, and remove any dependency data, effectively freezing recursive fields to their current value.

A flag is also added to record attributes, in order to remember that some record has already been frozen. Indeed, freezing is linear in the number of fields and pending contracts: freezing at every dictionary operation thus could be costly. Instead, as for closurization, we do it once and then remember that it's been done in flag. It helps dictionary operations preserve frozenness. Only merging or lazy contract applications might require freezing again.

What's missing to close #1877 is to just add a call to %record/freeze% in preamble of every dictionary operations. This will be addressed in a follow-up PR.

[github-actions]

Bencher Report

Branch	feat/record-freezing
Testbed	ubuntu-latest

Click to view all benchmark results

Benchmark	Latency	nanoseconds (ns)
fibonacci 10	📈 view plot 🚷 view threshold	487,890.00
foldl arrays 50	📈 view plot 🚷 view threshold	1,685,500.00
foldl arrays 500	📈 view plot 🚷 view threshold	6,668,600.00
foldr strings 50	📈 view plot 🚷 view threshold	7,131,700.00
foldr strings 500	📈 view plot 🚷 view threshold	62,579,000.00
generate normal 250	📈 view plot 🚷 view threshold	46,258,000.00
generate normal 50	📈 view plot 🚷 view threshold	2,029,700.00
generate normal unchecked 1000	📈 view plot 🚷 view threshold	3,369,600.00
generate normal unchecked 200	📈 view plot 🚷 view threshold	762,140.00
pidigits 100	📈 view plot 🚷 view threshold	3,184,700.00
pipe normal 20	📈 view plot 🚷 view threshold	1,497,800.00
pipe normal 200	📈 view plot 🚷 view threshold	10,028,000.00
product 30	📈 view plot 🚷 view threshold	833,390.00
scalar 10	📈 view plot 🚷 view threshold	1,511,100.00
sum 30	📈 view plot 🚷 view threshold	831,590.00

🐰 View full continuous benchmarking report in Bencher

[jneem]

Could this raise a back-compat issue once the std.record functions are updated to freeze? I didn't succeed to construct an example that calls std.record.remove on a record with a sealed tail, but maybe it's possible?

[yannham]

I think it's hard to build without referring to primops directly. On paper, you might say that stuff like insert_foo | forall r. {; r} -> { foo : Number; r } or remove_bar | forall a r. {bar: a; r} -> {; r} looks reasonable, but to write those using the stdlib you'd need to cast back the result of dictionary operations - since they operate on dictionary types - but you can't name r, so you can't fill the blank in std.record.insert "foo" 5 record | {foo : Number; ????}.

Granted, it's entirely accidental (due to the absence of something like scoped type variables), but the consequence is that you can't write today without resorting to %record/insert%, and the idea is to not touch the latter, just add freezing in the stdlib wrappers.

Even if we had scoped type variables, a second issue is that stdlib dictionary functions use dictionary types for their input and output. The corresponding contract maps over its argument, but mapping isn't permitted either on a record with a sealed tail:

nickel> let f | forall r. {foo : Number; r} -> {_ : Number} = fun x => x
nickel> f {foo = 1, bar = 2}
error: contract broken by a function
       : cannot map over a record sealed by a polymorphic contract
  ┌─ <repl-input-0>:1:19
  │
1 │ let f | forall r. {foo : Number; r} -> {_ : Number} = fun x => x
  │                   ----------------- expected type of an argument of an inner call
  │
  ┌─ <repl-input-2>:1:3
  │
1 │ f {foo = 1, bar = 2}
  │   ------------------ evaluated to this expression

So right now, it seems that dictionaries are pretty incompatible with polymorphic tails anyway. That being said, we could ask if those maybe should be well-typed / possible to write. Let's say we have scoped type variables or whatnot to make that possible. I think the question of the semantics remain: what should we do upon freezing a record with a sealed tail?

1. We only freeze the non-sealed part. For the caller, it means that you call to some polymorphic function on records, and what you get back is that some of your recursive dependencies are erased, but not all. I think that's really hard to reason about and error-prone.
2. We look under the tail and remove dependencies there as well. We might need to do that recursively, as tails can be nested. This is a bit more reasonable for the caller, but it means that the sacred tail isn't sacred anymore, as it can be touched indirectly by freezing.
3. We refuse to freeze polymorphic tails, as in the current PR.

Another idea that came from a discussion with @sjoerdvisscher is that maybe this idea of either being in dictionary mode or not should be embodied by types/contracts, and not chosen by functions individually. This would have the merit of making it clear from the interface of a function if freezing happens, and freezing would be exerted by the dictionary type {_ : T}. I haven't yet thought about this alternative enough to be sure, but in any case this concerns a follow-up PR. The present PR is about introducing the freezing operation itself; it's not yet used anywhere.

[solson]

What's missing to close #1877 is to [...]

@yannham I think GitHub saw close #1877 and ironically took that as an instruction to auto-close it, which I think was not intended.