LinearMap
LinearMap: a keyed collection that can hold LINEAR values.
A Map cannot hold a linear value: Map.get copies the value out while the map keeps it, and Map.insert over an existing key drops the old one. LinearMap(k, v) is the collection for values that must be used exactly once, such as the parked session state an actor keeps per session (Parked_<Role>, from @[endpoints]).
The rules, all checked statically at the caller:
LinearMapisalways_linear: every binding of one must be consumed,
whatever it holds. A map in actor state is a linear field, so every
handler turn that reads it must store one back.
* Every operation consumes the map and returns it. `take` (or
`take_slot`) is the only way a value leaves; `put` returns the value it
displaced instead of dropping it.
* A map ends in `drain` (every value goes through a callback that must
consume it), `to_list`, or `dispose`, which hands a non-empty map back in
`Err` rather than losing what is inside.
* Keys are ordinary values: they are hashed, compared and copied, so a
linear key type is rejected. Equality comes from the less-than
comparator given to `empty`, stored in the map (as for `Map`, it must be
a strict total order consistent with `==` on the key type).Implementation: a count, the comparator, and a Map underneath. The functions below carry @[trusted_linear(v)]: callers may instantiate v with a linear type, and each body is REVIEWED, not checked, to move every value exactly once. The invariants, per function:
put Map.get the old value out, then Map.insert over it: the trie's
reference to the old value is released and the caller holds the
only one.
take Map.get + Map.remove of the same key.
take_slot as take; the slot remembers the key, now absent.
fill Map.insert into the slot's key, which take_slot removed.
drain Map.fold hands each value to the callback once; the trie is
not used again.
to_list Map.to_list of a trie that is not used again.
size, member, keys, vacate, dispose
move no value.Values are reference-counted at runtime like any other; linearity is a discipline over the references March code can see, and the kernel keeps it by never keeping a value it has handed out.
Performance: put/take/take_slot/fill O(log32 n) (a get plus an insert or a remove); size O(1); keys/drain/to_list O(n), in hash order.
Functions
An empty map whose keys are ordered by the curried less-than comparator cmp (cmp(a)(b) is true when a < b). The comparator is stored, so no later call takes one.
An empty map keyed by Int.
An empty map keyed by String.