March Docs

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:

  • LinearMap is always_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

fndisposedispose(m : LinearMap(k, v)) : Result((), LinearMap(k, v))#
fndraindrain(m : LinearMap(k, v), acc : a, f : a -> k -> v -> a) : a#
fnemptyempty(cmp : k -> k -> Bool) : LinearMap(k, v)#

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.

fnempty_intempty_int() : LinearMap(Int, v)#

An empty map keyed by Int.

fnempty_stringempty_string() : LinearMap(String, v)#

An empty map keyed by String.

fnfillfill(s : LinearSlot(k, v), val : v) : LinearMap(k, v)#
fnkeyskeys(m : LinearMap(k, v)) : (List(k), LinearMap(k, v))#
fnmembermember(m : LinearMap(k, v), key : k) : (Bool, LinearMap(k, v))#
fnputput(m : LinearMap(k, v), key : k, val : v) : (Option(v), LinearMap(k, v))#
fnsizesize(m : LinearMap(k, v)) : (Int, LinearMap(k, v))#
fntaketake(m : LinearMap(k, v), key : k) : (Option(v), LinearMap(k, v))#
fntake_slottake_slot(m : LinearMap(k, v), key : k) : (Option(v), LinearSlot(k, v))#
fnto_listto_list(m : LinearMap(k, v)) : List((k, v))#
fnvacatevacate(s : LinearSlot(k, v)) : LinearMap(k, v)#